#+Title: Dktactics User Manual
* Introduction
This is a user manual for Dktactics. Dktactics is a Meta Dedukti
implementation of a typed tactic language and an untyped tactic
language.
The untyped tactic language is intended to be used both for
interactive theorem proving and to turn the output of automatic
theorem provers into formal proofs.
* Installation
Dktactics can be downloaded from
[[https://gitlab.math.univ-paris-diderot.fr/cauderlier/dktactics]]. Dependencies
and installation instructions are detailed in the file [[./README.org][README.org]].
* Multi-sorted first-order logic in Dedukti
Dktactics is a pair of tactic languages for multi-sorted first-order
logic. In this section, we explain why we have focused on this
particular logic, and then explain how to write terms, formulae,
proofs, and theories to be used with Dktactics.
** Why first-order logic?
Interactive proof assistants often propose expressive higher-order
logics and translations to Dedukti for these expressive logics are
well studied so our choice of basing Dktactics on first-order logic
might surprise.
We have chosen to work with first-order logic because it is powerful
enough to express the certificates that most automatic tools are able
to produce. Proof systems for more expressive logics can usually
produce very detailed proofs that can be exported to Dedukti without
needing an intermediate tactic language.
By restricting our attention to first-order logic, we can rely on
first-order unification which is very efficient and very predictable
compared to higher-order unification. See for example The section
about [[* Resolution][resolution]].
** Why a multi-sorted logic?
We have chosen to use a multi-sorted version of first-order logic. In
this setting, the domain of a predicate or function symbol is a list
of sorts and each function symbol has a codomain sort.
We use a multi-sorted logic for two reasons. First, some automatic
provers such as Zenon Arith and Zipperposition work in this
setting. Second, multi-sorted logic ease the combination of
theories. Merging for example a theory of booleans containing the
axiom \forall b. b = =true= \vee b = =false= with arithmetic can only
be soundly done if we have a way to distinguish booleans from numbers.
** Syntax
The syntax of multi-sorted first-order logic is composed of four
syntactic categories: sorts, terms, formulae, and proofs.
*** Sorts
First-order sorts are the elements of the Dedukti type =fol.sort=.
The file [[./fol/fol.dk][fol/fol.dk]] does not provide any function to build sorts;
instead the definer of a theory is expected to declare the various
sorts she needs.
However, once some sorts have been declared, the file [[./fol/fol.dk][fol/fol.dk]]
provides functions for building lists of sorts. The Dedukti type of
lists of sorts is =fol.sorts= and its constructors are
- =fol.nil_sort : fol.sorts= and
- =fol.cons_sort : fol.sort -> fol.sorts -> fol.sorts=
For convenience, the file [[./fol/fol.dk][fol/fol.dk]] also defines an n-ary function
for building lists of sorts:
- =fol.read_sorts n A1 … An= is defined as =fol.cons_sort A1 (… (fol.cons_sort An fol.nil_sort)…)=
The first parameter =n= of =fol.read_sorts= is a natural number of
type =nat.Nat=. It can be built from
- =nat.O : nat.Nat= representing 0 and
- =nat.S : nat.Nat -> nat.Nat= representing the successor operation
*** Terms
Our encoding of first-order logic in Dedukti is shallow in the
following sense:
- Dedukti typing judgment is used to represent first-order typing
- Dedukti variables are used to represent first-order variables
If =A= is a sort, the Dedukti type of first-order terms of
sort =A= is =fol.term A=; in other words, the Dedukti symbol
=fol.term= has type =fol.sort -> Type=.
A function symbol is a Dedukti term of type =fol.function=.
A domain and a codomain are respectively associated to each function
symbol by the functions
- =fol.fun_domain : fol.function -> fol.sorts= and
- =fol.fun_codomain : fol.function -> fol.sort=
If =As= is a list of sorts, then =fol.terms As= is the Dedukti type of
lists of terms whose sorts match =As=. This type has two constructors:
- =fol.nil_term : fol.terms fol.nil_sort= representing the empty list
of terms
- =fol.cons_term : A : fol.sort -> fol.term A -> tail_sorts : fol.sorts -> fol.terms tail_sorts -> fol.terms (fol.cons_sort A tail_sorts)=
The only constructor of =fol.term A= is application of a function
symbol =f= whose codomain is =A= to a list of terms whose sorts match
the domain of =f=.
- =fol.apply_fun : f : fol.function -> fol.terms (fol.fun_domain f) -> fol.term (fol.fun_codomain f)=
For convenience, the file [[./fol/fol.dk][fol/fol.dk]] also defines an n-ary function
for applying a function symbol to terms:
- if =f= is a function symbol of domain =fol.read_sorts n A1 … An= and
of codomain =B=, and if =a1=, …, =an= are =n= terms of sort =A1=, …,
=An= respectively, then =fol.fun_apply f a1 … an= has sort =B=.
*** Formulae
First-order formulae are also defined in file [[./fol/fol.dk][fol/fol.dk]]. The Dedukti
type of first-order formulae is =fol.prop=.
In first-order logic, formulae are built from atoms connected together
by logical connectives and quantifiers.
**** Atoms
An atom is a predicate symbol applied to terms respecting the domain of
the predicate symbol. Predicate symbols and their arities are defined
similarly to function symbols. A predicate symbol is a Dedukti term of
type =fol.predicate=. An artity is associated to each predicate
symbol by the function
- =fol.pred_domain : fol.predicate -> fol.sorts=
Applying a predicate symbol on a list of terms respecting its domain
produces a formula:
- =fol.apply_pred : p : fol.predicate -> fol.terms (fol.pred_domain p) -> fol.prop=
For convenience, the file [[./fol/fol.dk][fol/fol.dk]] also defines an n-ary function
for applying a predicate symbol to terms:
- if =p= is a predicate symbol of domain =fol.read_sorts n A1 … An= and
if =a1=, …, =an= are =n= terms of sort =A1=, …, =An= respectively,
then =fol.pred_apply p a1 … an= has type =fol.prop=.
**** Logical connectives
We consider the following logical connectives: falsehood =fol.false=,
truth =fol.true=, negation =fol.not=, conjunction =fol.and=,
disjunction =fol.or=, implication =fol.imp=, and equivalence
=fol.eqv=.
Falsehood and truth are constant connectives, negation is unary, and
all other connectives are binary.
Falsehood, conjunction, disjunction, and implication are primitive
connectives whereas negation, truth, and equivalence are derived
connectives respectively defined by:
| =fol.not A= | =:== | =fol.imp A fol.false= |
| =fol.true= | =:== | =fol.not fol.false= |
| =fol.eqv A B= | =:== | =fol.and (fol.imp A B) (fol.imp B A)= |
**** Quantifiers
We consider universal and existential quantifiers. Each quantifier
binds a single variable of a given sort. As we promised in [[* Terms][the section
about terms]], variable binding is shallow in the sense that variables
are represented by Dedukti variables.
The universal and existential quantifiers are respectively =fol.all=
and =fol.ex=. They have the same Dedukti type: =A : fol.sort -> (fol.term A -> fol.prop) -> fol.prop=.
**** n-ary connectives and quantifiers
For convenience, n-ary versions =fol.nand=, =fol.nor=, =fol.nimp=,
=fol.nall=, and =fol.nex= of respectively =fol.or=, =fol.and=,
=fol.imp=, =fol.all=, and =fol.ex= are also defined with the following
sorts:
- =fol.nand : n : nat.Nat -> A₁ : prop -> … -> Aₙ : prop -> prop=
- =fol.nor : n : nat.Nat -> A₁ : prop -> … -> Aₙ : prop -> prop=
- =fol.nimp : n : nat.Nat -> A₁ : prop -> … -> Aₙ : prop -> prop -> prop=
- =fol.nall : n : nat.Nat -> A₁ : sort -> … -> Aₙ : sort -> (term A₁ -> … -> term Aₙ -> prop) -> prop=
- =fol.nex : n : nat.Nat -> A₁ : sort -> … -> Aₙ : sort -> (term A₁ -> … -> term Aₙ -> prop) -> prop=
They are defined by nesting the corresponding connectives and quantifiers as follows:
- =fol.nand 0 = fol.true=
- =fol.nand n A₁ A₂ … Aₙ = fol.and A₁ (fol.and A₂ (…Aₙ…))=
- =fol.nor 0 = fol.false=
- =fol.nor n A₁ A₂ … Aₙ = fol.or A₁ (fol.or A₂ (…Aₙ…))=
- =fol.imp n A₁ A₂ … Aₙ B = fol.imp A₁ (fol.imp A₂ (… (fol.imp Aₙ B)…))=
- =fol.nall n A₁ A₂ … Aₙ P = fol.all A₁ (a₁ : fol.term A₁ => fol.all A₂ (a₂ : fol.term A₂ => … fol.all Aₙ (aₙ : fol.term Aₙ => P a₁ … aₙ)…))=
- =fol.nex n A₁ A₂ … Aₙ P = fol.ex A₁ (a₁ : fol.term A₁ => fol.ex A₂ (a₂ : fol.term A₂ => … fol.ex Aₙ (aₙ : fol.term Aₙ => P a₁ … aₙ)…))=
*** Proofs
We use an intuitionistic natural deduction proof system. If =A= is a
formula, the Dedukti type of all proofs of =A= is =fol.proof A=. The
function =fol.proof= is defined using an impredicative encoding but we
usually do not use the definition directly but rather rely on the
following theorems proved in the file [[./fol/fol.dk][fol/fol.dk]] and representing
natural deduction introduction and elimination rules (or the
corresponding tactics presented in [[* Reasoning][the reasoning section]]):
- =fol.false_elim : A : fol.prop -> fol.proof fol.false -> fol.proof A=
- =fol.true_intro : fol.proof fol.true=
- =fol.and_intro : A : fol.prop -> B : fol.prop -> fol.proof A -> fol.proof B -> fol.proof (fol.and A B)=
- =fol.and_elim_1 : A : fol.prop -> B : fol.prop -> fol.proof (fol.and A B) -> fol.proof A=
- =fol.and_elim_2 : A : fol.prop -> B : fol.prop -> fol.proof (fol.and A B) -> fol.proof B=
- =fol.or_intro_1 : A : fol.prop -> B : fol.prop -> fol.proof A -> fol.proof (fol.or A B)=
- =fol.or_intro_2 : A : fol.prop -> B : fol.prop -> fol.proof B -> fol.proof (fol.or A B)=
- =fol.or_elim : A : fol.prop -> B : fol.prop -> C : fol.prop -> fol.proof (fol.or A B) -> (fol.proof A -> fool.proof C) -> (fol.proof B -> fool.proof C) -> fol.proof C=
- =fol.imp_intro : A : fol.prop -> B : fol.prop -> (fol.proof A -> fol.proof B) -> fol.proof (fol.imp A B)=
- =fol.imp_elim : A : fol.prop -> B : fol.prop -> fol.proof (fol.imp A B) -> fol.proof A -> fol.proof B=
- =fol.all_intro : A : fol.sort -> B : (fol.term A -> fol.prop) -> (a : fol.term A -> fol.proof (B a)) -> fol.proof (fol.all A B)=
- =fol.all_elim : A : fol.sort -> B : (fol.term A -> fol.prop) -> fol.proof (fol.all A B) -> a : fol.term A -> fol.proof (B a)=
- =fol.ex_intro : A : fol.sort -> B : (fol.term A -> fol.prop) -> a : fol.term A -> fol.proof (B a) -> fol.proof (fol.ex A B)=
- =fol.ex_elim : A : fol.sort -> B : (fol.term A -> fol.prop) -> C : fol.prop -> fol.proof (fol.ex A B) -> (a : fol.term A -> fol.proof (B a) -> fol.proof C) -> fol.proof C=
** Defining a first-order theory
To define a new first-order theory, we start by declaring the sorts,
predicate symbols, and function symbols as new constants of type
=fol.sort=, =fol.predicate=, and =fol.function= respectively. We then
define the domain of each function and predicate symbol and the
codomain sort of each function symbol by extending the definitions of
=fol.pred_domain=, =fol.fun_domain=, and =fol.fun_codomain= respectively.
Finally we declare constants for the axioms and axiom schemes of the
theory.
For a complete example, see the file [[./fol/presburger.dk][fol/presburger.dk]].
** Deduction modulo
The main advantage of using a rewriting-based logical framework such
as Dedukti is the ease with which rewriting can be added into the
theories. In fact the symbols =fol.apply_fun= and =fol.apply_pred= are
definable so Deduction Modulo first-order theories can be defined.
** Equality
We treat equality as a first-order theory defined in the file
[[./fol/eq.dk][fol/eq.dk]]. Equality is a family of predicate symbols parameterized by
a sort:
- =eq.Eq : fol.sort -> fol.predicate=
The predicate symbol =eq.Eq A= expects two terms of sort =A= so the domain of the symbol =eq.Eq A= is =fol.read_sorts (nat.S (nat.S nat.O)) A A=.
The shortcut notation =eq.eq A a b= where =A= has type =fol.sort= and
both =a= and =b= have type =fol.term A= denotes the formula
=fol.pred_apply (eq.Eq A) a b=.
Equality is defined impredicatively as all the logical connectives and
quantifiers. The file [[./fol/eq.dl][fol/eq.dk]] also contains proofs of the following
facts:
- Equality is reflexive:
=eq.eq_refl : A : fol.sort -> fol.proof (fol.all A (x => eq.eq A x x))=
- Equality is symmetric:
=eq.eq_symm : A : fol.sort -> fol.proof (fol.all A (x => fol.all A (y => fol.imp (eq.eq A y x) (eq.eq A x y))))=
- Equality is transitive:
=eq.eq_trans : A : fol.sort -> fol.proof (fol.all A (x => fol.all A (y => fol.all A (z => fol.imp (eq.eq A x y) (fol.imp (eq.eq A y z) (eq.eq A x z))))))=
- Equality is a congruence with respect to all function symbols:
=eq.eq_fun_equal : f : fol.function -> fol.proof (fol.all A1 (x1 => fol.all A1 (y1 => fol.imp (eq.eq A1 x1 y1) (… fol.all An (xn => fol.all An (yn => fol.imp (eq.eq An xn yn) (eq.eq B (fol.apply_fun f x1 … xn) (fol.apply_fun f y1 … yn)))) …))))=
where =f= has domain =fol.read_sorts n A1 … An= and codomain =B=.
- Equality is a congruence with respect to all predicate symbols:
=eq.eq_pred_equal : p : fol.predicate -> fol.proof (fol.all A1 (x1 => fol.all A1 (y1 => fol.imp (eq.eq A1 x1 y1) (… fol.all An (xn => fol.all An (yn => fol.imp (eq.eq An xn yn) (fol.imp (fol.apply_pred p x1 … xn) (fol.apply_pred p y1 … yn)))) …))))=
where =p= has domain =fol.read_yypes n A1 … An=
* The typed tactic language
The Dedukti theory presented in [[* Multi-sorted first-order logic in Dedukti][the previous section]] is sound in the
following sense:
- Convergence: The rewrite system that defines it is both confluent
and terminating.
- Subject-reduction: Typing is preserved by reduction according to
this rewrite-system.
- Decidability of type-checking: The type-checking problem for terms
in this Dedukti theory is decidable and the Dedukti type checker is
a decision procedure for it.
- Consistency: a closed term of type =fol.proof fol.false= can only be
obtained by encoding an inconsistent first-order theory.
Thanks to these good properties, a term of type =fol.proof A= can be
considered as a proof witnessing the truth of the proposition =A=. We
now consider rewrite systems breaking some or all of these properties
in order to help the user write short proof scripts. The bad rewrite
systems are used to normalize these scripts into proofs to be checked
in the good rewrite system of the previous section.
To ease the selection of either the good rewrite system or both good
and bad ones, Dktactics is organised in several directories: the
directory [[./fol][fol]] contains the good system, the directory [[./meta][meta]] contains
the bad ones and the directory [[./example][example]] contains examples to be first
normalized using the bad system and then checked using the good one.
The first bad system is a dependently-typed tactic language. It is
very similar to the typed tactic languages of Lean and [[http://plv.mpi-sws.org/mtac/][Mtac]] but it is
simpler for the following reasons:
- It deals with first-order logic instead of the full calculus of
inductive constructions.
- In Dedukti it is not necessary to encode pattern matching and
recursion directly in the tactic language because the user can
already use rewriting for these tasks.
- We have chosen to keep a shallow encoding of terms and formulae so
some features such as testing whether a term is a variable are
omitted.
** The tactic monad
Like in Lean and Mtac, our tactic language encapsulates computation
inside a monad defined in the file [[./meta/tac.dk][meta/mtac.dk]] whose main purpose is
to handle failure and backtracking.
- =mtac.mtactic : fol.prop -> Type=
- =mtac.mret : A : fol.prop -> fol.proof A -> mtac.mtactic A=
- =mtac.mbind : A : fol.prop -> B : fol.prop -> mtac.mtactic A -> (fol.proof A -> mtac.mtactic B) -> mtac.mtactic B=
If =A= is a formula, =mtac.mtactic A= is the Dedukti type of the tactics
attempting to prove =A=. It forms a monad whose return and bind
operations are =mtac.mret= and =mtac.mbind= respectively.
When a tactic successfully proves a formula, we can extract a proof of the formula using the partial function =mtac.mrun=:
- =mtac.mrun : A : fol.prop -> mtac.mtactic A -> fol.proof A=
It is defined by the following rewrite rule:
- =[a] mtac.mrun _ (mtac.mret _ a) --> a=
** Exceptions and backtracking
Exceptions form an open inductive type =mtac.exc=.
A tactic can fail to prove its goal by raising an exception:
- =mtac.mraise : A : fol.prop -> mtac.exc -> mtac.mtactic A=
Exceptions can be caught by the =mtac.mtry= tactic combinator
implementing backtracking:
- =mtac.mtry : A : fol.prop -> mtac.mtactic A -> (mtac.exc -> mtac.mtactic A) -> tactic A=
The tactic =mtac.mtry A t f= first tries the tactic =t=, if it succeeds
then the corresponding proof of =A= is returned otherwise =t= has
failed with an exception =e= and we backtrack to try =f e=.
** Introducing variables and assumptions
The tactic language uses a shallow representation of variables and
contexts. In order to introduce a new variable or assumption in
context, we use non-linear higher-order rewriting to define the symbols =mtac.mintro_term= and =mtac.mintro_proof=:
#+BEGIN_SRC dedukti
def intro_term : A : fol.sort ->
B : (fol.term A -> fol.prop) ->
(x : fol.term A -> mtac.mtactic (B x)) ->
mtac.mtactic (fol.all A B).
def intro_proof : A : fol.prop ->
B : fol.prop ->
(fol.proof A -> mtac.mtactic B) ->
mtac.mtactic (fol.imp A B).
[A,B,b] mtac.mintro_term A B (x => mtac.mret (B x) (b x))
-->
mtac.mret (fol.all A B) (x : fol.term A => b x)
[A,B,e] mtac.mintro_term A B (x => mtac.mraise (B x) e)
-->
mtac.mraise (fol.all A B) e.
[A,B,b] mtac.mintro_proof A B (x => mtac.mret B (b x))
-->
mtac.mret (fol.imp A B) (x : fol.proof A => b x)
[A,B,e] mtac.mintro_proof A B (x => mtac.mraise _ e)
-->
mtac.mraise (fol.imp A B) e.
#+END_SRC
* The untyped tactic language
Because Dedukti lacks implicit arguments, the typed tactic language
that we just described is very verbose because a lot of type arguments
have to be provided. To improve usability, we construct an untyped
tactic language on top of the typed tactic language.
The untyped tactic language is defined in file [[./meta/tactic.dk][meta/tactic.dk]].
** Contexts and tactic evaluation
=tactic.tactic= is the Dedukti type of untyped tactics. Contrary to
typed tactics, the Dedukti type of an untyped tactic does not indicate
which formula it is supposed to prove and the same untyped tactic can
in fact prove several formulae.
Our untyped tacitc language is inspired by the LTac language which is
the default tactic language of the Coq proof assistant.
Tactics can be evaluated in a given state. The state is composed of a
goal formula and of an explicit context composed of variable
declarations and proven assumptions. Evaluating an untyped tactic
produces a typed tactic attempting to prove the goal formula.
- =tactic.context : Type=
- =tactic.nil_ctx : tactic.context=
- =tactic.cons_ctx_var : A : fol.sort -> fol.term A -> tactic.context -> tactic.context=
- =tactic.cons_ctx_proof : A : fol.prop -> fol.proof A -> tactic.context -> tactic.context=
- =tactic.tactic : Type=
- =tactic.eval_tactic : tactic.context -> A : fol.prop -> tactic.tactic -> mtac.mtactic A=
- =tactic.prove : A : fol.prop -> tactic.tactic -> fol.proof A=
** Tactic primitives
Most of the tactics and tacticals that we are going to introduce in
this section are defined from other tactics and tacticals. The few
that are not have their semantics directly defined in term of
evaluation by the =tactic.eval_tactic= function. We call them tactic
primitives.
The simplest primitives reflect the two constructors =mtac.mret= and
=mtac.mraise= of the tactic monad:
- =tactic.exact : A : fol.prop -> fol.proof A -> tactic.tactic=
- =tactic.raise : mtac.exc -> tactic.tactic=
The =tactic.exact A a= tactic succeeds if and only if its goal is
=A= in which case =mtac.mret A a= is returned. Otherwise the exception
=tactic.exact_mismatch= is raised.
The =tactic.raise e= tactic always raises the exception =e=.
The other operations of the monad, =mtac.mtry=, =mtac.mbind=,
=mtac.mintro_term= and =mtac.mintro_proof= are also reflected:
- =tactic.try : tactic.tactic -> (mtac.exc -> tactic.tactic) -> tactic.tactic=
- =tactic.bind : A : fol.prop -> tactic.tactic -> (fol.proof A -> tactic.tactic) -> tactic.tactic=
- =tactic.intro : tactic.tactic -> tactic.tactic=
The =tactic.try c f= tactic succeeds if either =c= succeeds or if
=c= raises an exception =e= and =f e= succeeds. The =tactic.bind A c f=
tactic succeeds if =c= successfully proves =A= and =f a= succeeds
where =a= is the proof of =A= generated by =c=. The =tactic.intro c=
tactic succeeds if the goal is either an implication =fol.imp A
B= such that =c= successfully proves =B= in a context extended by the
assumption =A= or a universal statement =fol.all A B= such that =c=
successfully proves =B a= in a context extended by the variable =a= of
sort =A=. On any other goal, the tactic =tactic.intro c= raises the
exception =tactic.not_a_product=.
Moreover, the file [[./meta/cert.dk][meta/tactic.dk]] defines tactic primitives for
manipulating the proof state:
- =tactic.with_goal : (fol.prop -> tactic.tactic) -> tactic.tactic=
- =tactic.with_context : (tactic.context -> tactic.tactic) -> tactic.tactic=
- =tactic.clear : fol.prop -> tactic.tactic -> tactic.tactic=
The =tactic.with_goal f= tactic successfully proves the goal =A= in
context =G= if and only if =f A= does so. Similarly,
=tactic.with_context f= successfully proves the goal =A= in context =G=
if and only if =f G= does so. The tactic =tactic.clear A c=
succeeds in context =G= if and only if =c= succeeds in the context
obtained from =G= by removing all the assumptions proving =A=.
Finally, the tactic language is made Turing-complete by the
addition of the fixpoint combinator =tactic.repeat=:
- =tactic.repeat : (tactic.tactic -> tactic.tactic) -> tactic.tactic=
The tactic =tactic.repeat f= is equivalent to the tactic =f (tactic.repeat f)=.
** Trying assumptions or variables
Instead of abstracting over the full context using
=tactic.with_context=, it is often more convenient to try all
assumptions or all variables in parallel. This behaviour is provided
by the =tactic.with_assumption= and =tactic.with_variable= tacticals:
- =tactic.with_assumption : (A : fol.prop -> fol.proof A -> tactic.tactic) -> tactic.tactic=
- =tactic.with_variable : (A : fol.sort -> fol.term A -> tactic.tactic) -> tactic.tactic=
The =tactic.with_assumption f= tactic is successful if =f A a= is
successful for any assumption =a : fol.proof A=. Otherwise, it raises
the exception =tactic.no_successful_assumption=. Similarly,
=tactic.with_variable f= is successful if =f A a= is successful for any
variable =a : fol.term A=. Otherwise it raises the exception
=tactic.no_successful_variable=.
A particular case is looking for the current goal among the
assumptions. This is provided by the =tactic.assumption= tactic:
- =tactic.assumption : tactic.tactic=
** Pattern matching
A lot of tactics perform different actions depending on the shape
of the goal or of assumptions. We have seen an example with the
=tactic.intro c= tactic in [[* Certificate primitives][the section about tactic
primitives]]. In general, the tactic combinator =tactic.match_prop=
can be used for this purpose:
#+BEGIN_SRC dedukti
tactic.match_prop : fol.prop ->
tactic.tactic ->
(fol.prop -> fol.prop -> tactic.tactic) ->
(fol.prop -> fol.prop -> tactic.tactic) ->
(fol.prop -> fol.prop -> tactic.tactic) ->
(A : fol.sort -> (fol.term A -> fol.prop) -> tactic.tactic) ->
(A : fol.sort -> (fol.term A -> fol.prop) -> tactic.tactic) ->
(p : fol.predicate ->
fol.terms (fol.pred_domain p) ->
tactic.tactic) ->
tactic.tactic
#+END_SRC
The tactic =tactic.match_prop C cfalse cand cor cimp call cex
cpred= is equivalent to
- =cfalse= if =C= is =fol.false=
- =cand A B= if =C= is =fol.and A B=
- =cor A B= if =C= is =fol.or A B=
- =cimp A B= if =C= is =fol.imp A B=
- =call A B= if =C= is =fol.all A B=
- =cex A B= if =C= is =fol.ex A B=
- =cpred p l= if =C= is =fol.apply_pred p l=.
Most of the time, we are interested in just one shape among the 7
possible so [[./meta/cert.dk][meta/tactic.dk]] provides the following combinators matching
on each of the cases:
- =tactic.match_false : fol.prop -> tactic.tactic -> tactic.tactic -> tactic.tactic=
- =tactic.match_and : fol.prop -> (fol.prop -> fol.prop -> tactic.tactic) -> tactic.tactic -> tactic.tactic=
- =tactic.match_or : fol.prop -> (fol.prop -> fol.prop -> tactic.tactic) -> tactic.tactic -> tactic.tactic=
- =tactic.match_imp : fol.prop -> (fol.prop -> fol.prop -> tactic.tactic) -> tactic.tactic -> tactic.tactic=
- =tactic.match_all : fol.prop -> (A : fol.sort -> (fol.term A -> fol.prop) -> tactic.tactic) -> tactic.tactic -> tactic.tactic=
- =tactic.match_ex : fol.prop -> (A : fol.sort -> (fol.term A -> fol.prop) -> tactic.tactic) -> tactic.tactic -> tactic.tactic=
- =tactic.match_pred : fol.prop -> (p : fol.predicate -> fol.terms (fol.pred_domain p) -> tactic.tactic) -> tactic.tactic -> tactic.tactic=
** Sort and formulae comparison
We have seen how to inspect the structure of a formula but this is of
little use until we are able to test whether or not two formulae or
sorts are identical and obtain coercion functions when they are.
This behaviour is provided by the following combinators:
- =tactic.ifeq_sort : A : fol.sort -> B : fol.sort -> ((fol.term A -> fol.term B) -> tactic.tactic) -> tactic.tactic -> tactic.tactic=
- =tactic.ifeq_prop : A : fol.prop -> B : fol.prop -> ((fol.proof A -> fol.proof B) -> tactic.tactic) -> tactic.tactic -> tactic.tactic=
** Reasoning
In this section, we list the tactic combinators that are used to
perform reasoning steps. In fact we already met some of them, namely
the =tactic.exact A a= tactic used to provide a proof term for the
current goal =A= and the =tactic.intro= combinator used to introduce
implications and universal quantifications.
*** Applying a lemma
The following combinators are used to apply a lemma:
- =tactic.refine : A : fol.prop -> B : fol.prop -> (fol.proof A -> fol.proof B) -> tactic.tactic -> tactic.tactic=
- =tactic.refine2 : A : fol.prop -> B : fol.prop -> C : fol.prop -> (fol.proof A -> fol.proof B -> fol.proof C) -> tactic.tactic -> tactic.tactic -> tactic.tactic=
- =tactic.refinen : n : nat.Nat -> A1 : fol.prop -> … -> An : fol.prop -> B : fol.prop -> (fol.proof A1 -> … -> fol.proof An -> fol.proof B) -> c1 : tactic.tactic -> … -> cn : tactic.tactic -> tactic.tactic=
- =tactic.assert : fol.prop -> tactic.tactic -> tactic.tactic -> tactic.tactic=
- =tactic.apply : A : fol.sort -> (fol.term A -> fol.prop) -> fol.term A -> tactic.tactic -> tactic.tactic=
The tactic =tactic.refine A B f c= proves =B= by applying the lemma
=f= which has an assumption =A= proved by the tactic =c=.
The tactic =tactic.refine2 A B C f c1 c2= is similar for a lemma
with two assumptions =A= and =B= proved respectively by =c1= and =c2=.
The tactic =tactic.refinen n A1 … An B f c1 … cn= is similar for a
lemma with =n= assumptions =A1= … =An= proved respectively by =c1= …
=cn=.
The tactic =tactic.assert A c1 c2= proves the current goal =B= in
the current context =G= if =c1= proves =A= in context =G= and =c2=
proves =B= in context =G= with =A= as extra assumption.
The tactic =tactic.apply A B a c= proves =B a= if =c= proves
=fol.all A B=.
*** Reasoning on the goal
The following tactics are used to reason on the current goal,
each proves the current goal if it has a particular shape:
- =tactic.trivial : tactic.tactic=
- =tactic.split : tactic.tactic -> tactic.tactic -> tactic.tactic=
- =tactic.left : tactic.tactic -> tactic.tactic=
- =tactic.right : tactic.tactic -> tactic.tactic=
- =tactic.exists : A : fol.sort -> fol.term A -> tactic.tactic -> tactic.tactic=
The tactic =tactic.trivial= proves the goal =fol.true=. The
tactic =tactic.split c1 c2= proves =fol.and A B= if =c1= proves =A=
and =c2= proves =B=. The tactic =tactic.left c= proves =fol.or A B=
if =c= proves =A=. The tactic =tactic.right c= proves =fol.or A B=
if =c= proves =B=. The tactic =tactic.exists A a c= proves =fol.ex
A B= if =c= proves =B a=.
*** Reasoning on the assumptions
The following tactics are used to reason from assumptions:
- =tactic.exfalso : tactic.tactic -> tactic.tactic=
- =tactic.absurd : tactic.tactic=
- =tactic.destruct_and : fol.prop -> fol.prop -> tactic.tactic -> tactic.tactic -> tactic.tactic=
- =tactic.destruct_or : fol.prop -> fol.prop -> tactic.tactic -> tactic.tactic -> tactic.tactic -> tactic.tactic=
- =tactic.destruct_imp : fol.prop -> fol.prop -> tactic.tactic -> tactic.tactic -> tactic.tactic -> tactic.tactic=
- =tactic.destruct_all : A : fol.sort -> (fol.term A -> fol.prop) -> fol.term A -> tactic.tactic -> tactic.tactic -> tactic.tactic=
- =tactic.destruct_ex : A : fol.sort -> (fol.term A -> fol.prop) -> tactic.tactic -> tactic.tactic -> tactic.tactic=
The tactic =tactic.exfalso c= proves the current goal if =c= proves
=fol.false=. The tactic =tactic.absurd= proves the current goal if
the context contains a pair of contradictory assumptions (an
assumption together with its negation). The tactic
=tactic.destruct_and A B c1 c2= proves the current goal =C= in context
=G= if =c1= proves =fol.and A B= in context =G= and =c2= proves =C= in
context =G= with extra assumptions =A= and =B=. The tactic
=tactic.destruct_or A B c1 c2 c3= proves the current goal =C= in context
=G= if =c1= proves =fol.or A B= in context =G=, =c2= proves =C= in
context =G= with extra assumption =A=, and =c3= proves =C= in context
=G= with extra assumption =B=. The tactic =tactic.destruct_imp A B
c1 c2 c3= proves the current goal =C= in context =G= if =c1= proves
=fol.imp A B= in context =G=, =c2= proves =A= in context =G= and =c3=
proves =C= in context =G= with extra assumption =B=. The tactic
=tactic.destruct_ex A B c1 c2= proves the current goal =C= in context
=G= if =c1= proves =fol.ex A B= and =c2= proves =C= in context =G=
with an extra variable =x= of sort =A= and an extra assumption =B x=.
** Equality Tactics
The file [[./meta/eqcert.dk][meta/eqtac.dk]] defines a few tacticals to reason about
equality:
- =eqtac.match_equality : fol.prop -> (A : fol.sort -> fol.term A -> fol.term A -> tactic.tactic) -> tactic.tactic -> tactic.tactic=
- =eqtac.reflexivity : tactic.tactic=
- =eqtac.symmetry : tactic.tactic -> tactic.tactic=
- =eqtac.transitivity : A : fol.sort -> fol.term A -> tactic.tactic -> tactic.tactic -> tactic.tactic=
- =eqtac.f_equal : f : fol.function -> c1 : tactic.tactic -> … -> cn : tactic.tactic -> tactic.tactic=
(where the domain of =f= has length =n=)
- =eqtac.rewrite : A : fol.sort -> fol.term A -> fol.term A -> tactic.tactic -> tactic.tactic=
The tactic =eqtac.match_equality A f c= is equivalent to =f B b1
b2= if =A= is =eq.eq B b1 b2= and to =c= otherwise. The tactic
=eqtac.reflexivity= proves goals of the form =eq.eq A a a=. The
tactic =eqtac.symmetry c= proves =eq.eq A a b= if =c= proves
=eq.eq A b a=. The tactic =eqtac.transitivity A b c1 c2= proves
goals of the form =eq.eq A a c= if =c1= proves =eq.eq A a b= and =c2=
proves =eq.eq A b c=. The tactic =eqtac.f_equal f c1 … cn=
proves =eq.eq B (fol.fun_apply f a1 … an) (fol.fun_apply f a1' … an')=
if each =ci= proves =eq.eq Ai ai ai'=. The tactic =eqtac.rewrite
A a a' c1 c2= proves =B= if =c1= proves =eq.eq A a a'= and =c2= proves
=B= in which each occurrence of =a= has been replaced by =a'= (see [[* Substitutions][the
section on substitution]]).
** Classical Reasoning
The file [[./fol/classical.dk][fol/classical.dk]] declares the axiom scheme of excluded middle:
=classical.excluded_middle : P : fol.prop -> fol.proof (fol.or P (fol.not P))=
The file [[./meta/classical_cert.dk][meta/classical_tactics.dk]] contains tacticals to ease reasoning in classical logic:
- =classical_tactics.prop_case : fol.prop -> tactic.tactic -> tactic.tactic -> tactic.tactic=
- =classical_tactics.contradict : tactic.tactic -> tactic.tactic=
=classical_tactics.prop_case= is used to reason by case on a the truth of
a formula using excluded middle; =classical_tactics.prop_case A c1 c2=
proves the current goal =B= in context =G= if =c1= proves =B= in
context =G= with extra assumption =A= and =c2= proves =B= in context
=G= with extra assumption =fol.not A=.
=classical_tactics.contradict= is used to prove by contradiction using
double-negation elimination. =classical_tactics.contradict c= proves the
current goal =A= in context =G= if =c= proves =fol.false= in context
=G= with extra assumption =fol.not A=.
These combinators are used to prove the following classical facts:
- =classical_tactics.nnpp : P : fol.prop -> fol.proof (fol.imp (fol.not (fol.not P)) P)=
- =classical_tactics.not_and_is_or_not : A : fol.prop -> B : fol.prop -> fol.proof (fol.imp (fol.not (fol.and A B)) (fol.or (fol.not A) (fol.not B)))=
- =classical_tactics.not_all_is_ex_not (A : fol.sort) (P : fol.term A -> fol.prop) : fol.proof (fol.imp (fol.not (fol.all A (x => P x)))=
* Examples
** Drinker paradox
The file [[./example/drinker.dkm][example/drinker.dkm]] is an example of classical reasoning. It
shows how to prove Smullyan's famous "drinker paradox": in an
non-empty bar, there is somebody such that, if he is drinking then
everyone in the bar is drinking.
The =.dkm= extension indicates that this file is intended to be
normalized by Meta Dedukti to produce the file =example/drinker.dk= to
be checked in the safe encoding of classical first-order logic.
This problem uses a single sort representing the person present in the
bar that we write =drinker.BAR=. Since the bar is assumed non-empty,
we know that somedy, call it Joe, is in the bar hence we declare a
constant =drinker.JOE= of codomain =drinker.BAR=. Finally the
signature is achieved with the unary predicate =drinker.DRINK=
representing drinking.
The proof of the theorem uses classical features twice: it starts with
a classical reasoning by case (using the =classical_tactics.prop_case=
combinator) and then uses the classical lemma
=classical_tactics.not_all_is_ex_not= in the second branch.
** TODO Decision procedures
*** Minimal logic
*** Presburger arithmetic
* TODO Interactive proof development
* Checking output of automatic theorem provers
** TODO Reasoning modulo AC, ACU, symmetry
** Shallow substitutions and unification
This section describes the features provided by the file
[[./meta/unif.dk][meta/unif.dk]] related to the handling of substitution and
unification. Usually, substitutions are not defined in shallow
embeddings relying on Higher-Order Abstract Syntax (HOAS) because
we have no access to the variables. However, unification is an
important tool for checking proof certificates that are not precise
enough to tell us which substitution to apply.
*** Substitutions
A substitution is usually defined as a finite mapping from
variables to terms. Since we have no precise type for variables in
our shallow embedding, we use lists of pairs of terms (both terms
having the same sort).
- =unif.substition : Type=
- =unif.empty_subst : unif.substitution=
- =unif.cons_subst : A : fol.sort -> fol.term A -> fol.term A -> unif.substitution -> unif.substitution=
Substitutions can be applied on propositions, terms, and list of terms.
- =unif.subst_prop : unif.substitution -> fol.prop -> fol.prop=
- =unif.subst_term : unif.substitution -> B : fol.sort -> fol.term B -> fol.term B=
- =unif.subst_terms : unif.substitution -> Bs : fol.sorts -> fol.terms Bs -> fol.terms Bs=
These functions are defined by a non-confluent rewrite system
which means that the behaviour of substitution depends on the
order in which the rewrite rules are given. The rules with the
highest priorities are those traversing the structure of the term
or formula such as
=[s,a,b] unif.subst_prop s (fol.and a b) --> fol.and (unif.subst_prop s a) (unif.subst_prop s b)=
If none of these rules is applicable, the term is assumed to be a
variable so we look into the substitution (seen as a list) for
corresponding pair. The comparison is performed by a non-linear
rewrite rule (the second rule):
- =[a] unif.subst_term unif.empty_subst _ a --> a=
- =[A,x,a] unif.subst_term (unif.cons_subst A x a _) A x --> a=
- =[As,s,A,x] unif.subst_term (unif.cons_subst _ _ As s) A x -->
unif.subst_term s A x=
Finally, for technical reasons (see the next section about
unification), the following two rewrite rules are added:
- =[A,a,s,p] unif.subst_prop (unif.cons_subst A a a s) p --> unif.subst_prop s p=
- =[A,a,s,p] unif.subst_prop unif.empty_subst p --> p=
*** Unification
A (first-order) unification problem is a list of pairs of terms
(both terms having the same sort). Unification can either fail or
return a substitution, the most general unifier of the unification
problem.
- =unif.unify_problem : Type=
- =unif.unify_nil : unif.unify_problem=
- =unif.unify_cons : A : fol.sort -> fol.term A -> fol.term A -> unif.unify_problem -> unif.unify_problem=
- =unif.unify_result : Type=
- =unif.unify_success : unif.substitution -> unif.unify_result=
- =unif.unify_failure : unif.unify_result=
We will not enter the details of the unification algorithm here,
the entry-point of the unification procedure is =unif.unify :
unif.unify_problem -> unif.unify_result=.
** Resolution
The resolution calculus is a very simple proof calculus for
classical first-order logic. It is a clausal calculus; this means
that it does not handle the full syntax of first-order formulae but
only the CNF (clausal normal form) fragment.
A *literal* is either an atom (a positive literal) or the
negation of an atom (a negative literal), a *clause* is a
disjunction of literals. Literals and clauses may contain free
variables which are to be interpreted as universally quantified. A
*quantified clause* is an explicitly universally quantified clause.
The types for atoms, literals, clauses, and quantified clauses are
declared with their constructors in [[./fol/clauses.dk][fol/clauses.dk]]. However, the
simplest way to define a clause is by parsing the corresponding
proposition using the partial function
=resolution.qclause_of_prop=:
- =resolution.qclause_of_prop : fol.prop -> clauses.qclause=
- =resolution.qclause_of_prop_correct : p : fol.prop -> fol.proof p -> resolution.qcproof (resolution.qclause_of_prop p)=
A resolution proof is a derivation of the empty clause
(representing falsehood) from assumed clauses using the following
two reasoning rules:
#+BEGIN_example
l₁ ∨ … ∨ lₙ σ = mgu(lᵢ, lⱼ)
————————————————————————————————— Factorisation
(l₁ ∨ … ∨ lⱼ₋₁ ∨ lⱼ₊₁ ∨ … ∨ lₙ)σ
l₁ ∨ … ∨ lₙ l'₁ ∨ … ∨ l'ₘ σ = mgu(lᵢ, ¬l'ⱼ)
——————————————————————————————————————————————————————————————————————— Resolution
(l₁ ∨ … ∨ lᵢ₋₁ ∨ lᵢ₊₁ ∨ … ∨ lₙ ∨ l'₁ ∨ … ∨ l'ⱼ₋₁ ∨ l'ⱼ₊₁ ∨ … ∨ l'ₘ)σ
#+END_example
These two rules are implemented by the following functions:
- =resolution.factor : Nat.nat -> Nat.nat -> resolution.qclause -> resolution.qclause=
- =resolution.factor_correct : i : Nat.nat -> j : Nat.nat -> Q : resolution.qclause -> resolution.qcproof Q -> resolution.qcproof (resolution.factor i j Q)=
- =resolution.resolve : Nat.nat -> Nat.nat -> resolution.qclause -> resolution.qclause -> resolution.qclause=
- =resolution.resolve_correct : i : Nat.nat -> j : Nat.nat -> Q : resolution.qclause -> Q' : resolution.qclause -> resolution.qcproof Q -> resolution.qcproof Q' -> resolution.qcproof (resolution.resolve i j Q Q')=
For an example of use of the =resolution= module, see the file [[./example/resolution_examples.dk][example/resolution_examples.dk]].