#+Title: Dktactics User Manual
* Introduction
This is a user manual for Dktactics. Dktactics is a Meta Dedukti
implementation of a tactic typed language.
On top of this language, an untyped language of certificates is
defined and 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 tactic and certificate language 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 arity of a predicate or function symbol is not
simply a natural number but a list of types (also known as /sorts/)
and each function symbol has a codomain type.
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: types, terms, formulae, and proofs.
*** Types
First-order types (also known as /sorts/) are the elements of the
Dedukti type =fol.type=. The file [[./fol/fol.dk][fol/fol.dk]] does not provide any
function to build types; instead the definer of a theory is expected
to declare the various types she needs.
However, once some types have been declared, the file [[./fol/fol.dk][fol/fol.dk]]
provides functions for building lists of types. The Dedukti type of
lists of types is =fol.types= and its constructors are
- =fol.nil_type : fol.types= and
- =fol.cons_type : fol.type -> fol.types -> fol.types=
For convenience, the file [[./fol/fol.dk][fol/fol.dk]] also defines an n-ary function
for building lists of types:
- =fol.read_types n A1 … An= is defined as =fol.cons_type A1 (… (fol.cons_type An fol.nil_type)…)=
The first parameter =n= of =fol.read_types= 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 first-order type, the Dedukti type of first-order terms of
type =A= is =fol.term A=; in other words, the Dedukti symbol
=fol.term= has type =fol.type -> Type=.
A function symbol is a Dedukti term of type =fol.function=.
A codomain and an arity are respectively associated to each function
symbol by the functions
- =fol.fun_arity : fol.function -> fol.types= and
- =fol.fun_codomain : fol.function -> fol.type=
If =As= is a list of types, then =fol.terms As= is the Dedukti type of
lists of terms whose types match =As=. This type has two constructors:
- =fol.nil_term : fol.terms fol.nil_type= representing the empty list
of terms
- =fol.cons_term : A : fol.type -> fol.term A -> tail_types : fol.types -> fol.terms tail_types -> fol.terms (fol.cons_type A tail_types)=
The only constructor of =fol.term A= is application of a function
symbol =f= whose codomain is =A= to a list of terms whose types match
the arity of =f=.
- =fol.apply_fun : f : fol.function -> fol.terms (fol.fun_arity 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 arity =fol.read_types n A1 … An= and
of codomain =B=, and if =a1=, …, =an= are =n= terms of type =A1=, …,
=An= respectively, then =fol.fun_apply f a1 … an= has type =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 arity 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_arity : fol.predicate -> fol.types=
Applying a predicate symbol on a list of terms respecting its arity
produces a formula:
- =fol.apply_pred : p : fol.predicate -> fol.terms (fol.pred_arity 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 arity =fol.read_types n A1 … An= and
if =a1=, …, =an= are =n= terms of type =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 type. 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.type -> (fol.term A -> fol.prop) -> fol.prop=.
*** 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 certificates constructors 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.type -> 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.type -> 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.type -> 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.type -> 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.type=, =fol.predicate=, and =fol.function= respectively. We then
define the arity of each function and predicate symbol and the
codomain sort of each function symbol by extending the definitions of
=fol.pred_arity=, =fol.fun_arity=, 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.type -> fol.predicate=
The predicate symbol =eq.Eq A= expects two terms of type =A= so the arity of the symbol =eq.Eq A= is =fol.read_types (nat.S (nat.S nat.O)) A A=.
The shortcut notation =eq.eq A a b= where =A= has type =fol.type= 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.type -> fol.proof (fol.all A (x => eq.eq A x x))=
- Equality is symmetric:
=eq.eq_symm : A : fol.type -> 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.type -> 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 arity =fol.read_types 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 arity =fol.read_yypes n A1 … An=
* The 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/tac.dk]] whose main purpose is
to handle failure and backtracking.
- =tac.tactic : fol.prop -> Type=
- =tac.ret : A : fol.prop -> fol.proof A -> tac.tactic A=
- =tac.bind : A : fol.prop -> B : fol.prop -> tac.tactic A -> (fol.proof A -> tac.tactic B) -> tac.tactic B=
If =A= is a formula, =tac.tactic A= is the Dedukti type of the tactics
attempting to prove =A=. It forms a monad whose return and bind
operations are =tac.ret= and =tac.bind= respectively.
When a tactic successfully proves a formula, we can extract a proof of the formula using the partial function =tac.run=:
- =tac.run : A : fol.prop -> tac.tactic A -> fol.proof A=
It is defined by the following rewrite rule:
- =[a] run _ (ret _ a) --> a=
** Exceptions and backtracking
Exceptions form an open inductive type =tac.exc=.
A tactic can fail to prove its goal by raising an exception:
- =tac.raise : A : fol.prop -> tac.exc -> tac.tactic A=
Exceptions can be caught by the =tac.try= tactic combinator
implementing backtracking:
- =tac.try : A : fol.prop -> tac.tactic A -> (tac.exc -> tac.tactic A) -> tactic A=
The tactic =tac.try 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 =tac.intro_term= and =tac.intro_proof=:
#+BEGIN_SRC dedukti
def intro_term : A : fol.type ->
B : (fol.term A -> fol.prop) ->
(x : fol.term A -> tac.tactic (B x)) ->
tac.tactic (fol.all A B).
def intro_proof : A : fol.prop ->
B : fol.prop ->
(fol.proof A -> tac.tactic B) ->
tac.tactic (fol.imp A B).
[A,B,b] tac.intro_term A B (x => tac.ret (B x) (b x))
-->
tac.ret (fol.all A B) (x : fol.term A => b x)
[A,B,e] tac.intro_term A B (x => tac.raise (B x) e)
-->
tac.raise (fol.all A B) e.
[A,B,b] tac.intro_proof A B (x => tac.ret B (b x))
-->
tac.ret (fol.imp A B) (x : fol.proof A => b x)
[A,B,e] tac.intro_proof A B (x => tac.raise _ e)
-->
tac.raise (fol.imp A B) e.
#+END_SRC
* The certificate language
Because Dedukti lacks implicit arguments, the 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 certificate
language on top of the tactic language.
The certificate language is described in file [[./meta/cert.dk][meta/cert.dk]].
** Contexts and certificate evaluation
=cert.certificate= is the Dedukti type of certificates. Contrary to
tactics, the type of a certificate does not indicate which formula it
is supposed to prove and the same certificate can in fact prove
several formulae.
Our certificate language is inspired by the LTac language which is the
default tactic language of the Coq proof assistant.
Certificates 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 a certificate produces
a tactic attempting to prove the goal formula.
- =cert.context : Type=
- =cert.nil_ctx : cert.context=
- =cert.cons_ctx_var : A : fol.type -> fol.term A -> cert.context -> cert.context=
- =cert.cons_ctx_proof : A : fol.prop -> fol.proof A -> cert.context -> cert.context=
- =cert.certificate : Type=
- =cert.run : A : fol.prop -> cert.context -> cert.certificate -> tac.tactic A=
** Certificate primitives
Most of the certificates and certificate combinators that we are going
to introduce in this section are defined from other certificates and
certificates combinators. The few that are not have their semantics
directly defined in term of evaluation by the =cert.run= function. We
call them certificate primitives.
The simplest primitives reflect the two constructors =tac.ret= and
=tac.raise= of the tactic monad:
- =cert.exact : A : fol.prop -> fol.proof A -> cert.certificate=
- =cert.raise : tac.exc -> cert.certificate=
The =cert.exact A a= certificate succeeds if and only if its goal is
=A= in which case =tac.ret A a= is returned. Otherwise the exception
=cert.exact_mismatch= is raised.
The =cert.raise e= certificate always raises the exception =e=.
The other operations of the monad, =tac.try=, =tac.bind=,
=tac.intro_term= and =tac.intro_proof= are also reflected:
- =cert.try : cert.certificate -> (tac.exc -> cert.certificate) -> cert.certificate=
- =cert.bind : A : fol.prop -> cert.certificate -> (fol.proof A -> cert.certificate) -> cert.certificate=
- =cert.intro : cert.certificate -> cert.certificate=
The =cert.try c f= certificate succeeds if either =c= succeeds or if
=c= raises an exception =e= and =f e= succeeds. The =cert.bind A c f=
certificate succeeds if =c= successfully proves =A= and =f a= succeeds
where =a= is the proof of =A= generated by =c=. The =cert.intro c=
certificate 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
type =A=. On any other goal, the tactic =cert.intro c= raises the
exception =cert.not_a_product=.
Moreover, the file [[./meta/cert.dk][meta/cert.dk]] defines certificate primitives for
manipulating the proof state:
- =cert.with_goal : (fol.prop -> cert.certificate) -> cert.certificate=
- =cert.with_context : (cert.context -> cert.certificate) -> cert.certificate=
- =cert.clear : fol.prop -> cert.certificate -> cert.certificate=
The =cert.with_goal f= certificate successfully proves the goal =A= in
context =G= if and only if =f A= does so. Similarly,
=cert.with_context f= successfully proves the goal =A= in context =G=
if and only if =f G= does so. The certificate =cert.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 certificate language is made Turing-complete by the
addition of the fixpoint combinator =cert.repeat=:
- =cert.repeat : (cert.certificate -> cert.certificate) -> cert.certificate=
The certificate =cert.repeat f= is equivalent to the certificate =f (cert.repeat f)=.
** Trying assumptions or variables
Instead of abstracting over the full context using
=cert.with_context=, it is often more convenient to try all
assumptions or all variables in parallel. This behaviour is provided
by the =cert.with_assumption= and =cert.with_variable= certificate
combinators:
- =cert.with_assumption : (A : fol.prop -> fol.proof A -> cert.certificate) -> cert.certificate=
- =cert.with_variable : (A : fol.type -> fol.term A -> cert.certificate) -> cert.certificate=
The =cert.with_assumption f= certificates is successful if =f A a= is
successful for any assumption =a : fol.proof A=. Otherwise, it raises
the exception =cert.no_successful_assumption=. Similarly,
=cert.with_variable f= is successful if =f A a= is successful for any
variable =a : fol.term A=. Otherwise it raises the exception
=cert.no_successful_variable=.
A particular case is looking for the current goal among the
assumptions. This is provided by the =cert.assumption= certificate:
- =cert.assumption : cert.certificate=
** Pattern matching
A lot of certificates perform different actions depending on the shape
of the goal or of assumptions. We have seen an example with the
=cert.intro c= certificate in [[* Certificate primitives][the section about certificate
primitives]]. In general, the certificate combinator =cert.match_prop=
can be used for this purpose:
#+BEGIN_SRC dedukti
cert.match_prop : fol.prop ->
cert.certificate ->
(fol.prop -> fol.prop -> cert.certificate) ->
(fol.prop -> fol.prop -> cert.certificate) ->
(fol.prop -> fol.prop -> cert.certificate) ->
(A : fol.type -> (fol.term A -> fol.prop) -> cert.certificate) ->
(A : fol.type -> (fol.term A -> fol.prop) -> cert.certificate) ->
(p : fol.predicate ->
fol.terms (fol.pred_arity p) ->
cert.certificate) ->
cert.certificate
#+END_SRC
The certificate =cert.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/cert.dk]] provides the following combinators matching
on each of the cases:
- =cert.match_false : fol.prop -> cert.certificate -> cert.certificate -> cert.certificate=
- =cert.match_and : fol.prop -> (fol.prop -> fol.prop -> cert.certificate) -> cert.certificate -> cert.certificate=
- =cert.match_or : fol.prop -> (fol.prop -> fol.prop -> cert.certificate) -> cert.certificate -> cert.certificate=
- =cert.match_imp : fol.prop -> (fol.prop -> fol.prop -> cert.certificate) -> cert.certificate -> cert.certificate=
- =cert.match_all : fol.prop -> (A : fol.type -> (fol.term A -> fol.prop) -> cert.certificate) -> cert.certificate -> cert.certificate=
- =cert.match_ex : fol.prop -> (A : fol.type -> (fol.term A -> fol.prop) -> cert.certificate) -> cert.certificate -> cert.certificate=
- =cert.match_pred : fol.prop -> (p : fol.predicate -> fol.terms (fol.pred_arity p) -> cert.certificate) -> cert.certificate -> cert.certificate=
** Type 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
types are identical and obtain coercion functions when they are.
This behaviour is provided by the following combinators:
- =cert.ifeq_type : A : fol.type -> B : fol.type -> ((fol.term A -> fol.term B) -> cert.certificate) -> cert.certificate -> cert.certificate=
- =cert.ifeq_prop : A : fol.prop -> B : fol.prop -> ((fol.proof A -> fol.proof B) -> cert.certificate) -> cert.certificate -> cert.certificate=
** Reasoning
In this section, we list the certificates combinators that are used to
perform reasoning steps. In fact we already met some of them, namely
the =cert.exact A a= certificate used to provide a proof term for the
current goal =A= and the =cert.intro= combinator used to introduce
implications and universal quantifications.
*** Applying a lemma
The following combinators are used to apply a lemma:
- =cert.refine : A : fol.prop -> B : fol.prop -> (fol.proof A -> fol.proof B) -> cert.certificate -> cert.certificate=
- =cert.refine2 : A : fol.prop -> B : fol.prop -> C : fol.prop -> (fol.proof A -> fol.proof B -> fol.proof C) -> cert.certificate -> cert.certificate -> cert.certificate=
- =cert.refinen : n : nat.Nat -> A1 : fol.prop -> … -> An : fol.prop -> B : fol.prop -> (fol.proof A1 -> … -> fol.proof An -> fol.proof B) -> c1 : cert.certificate -> … -> cn : cert.certificate -> cert.certificate=
- =cert.assert : fol.prop -> cert.certificate -> cert.certificate -> cert.certificate=
- =cert.apply : A : fol.type -> (fol.term A -> fol.prop) -> fol.term A -> cert.certificate -> cert.certificate=
The certificate =cert.refine A B f c= proves =B= by applying the lemma
=f= which has an assumption =A= proved by the certificate =c=.
The certificate =cert.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 certificate =cert.refinen n A1 … An B f c1 … cn= is similar for a
lemma with =n= assumptions =A1= … =An= proved respectively by =c1= …
=cn=.
The certificate =cert.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 certificate =cert.apply A B a c= proves =B a= if =c= proves
=fol.all A B=.
*** Reasoning on the goal
The following certificates are used to reason on the current goal,
each proves the current goal if it has a particular shape:
- =cert.trivial : cert.certificate=
- =cert.split : cert.certificate -> cert.certificate -> cert.certificate=
- =cert.left : cert.certificate -> cert.certificate=
- =cert.right : cert.certificate -> cert.certificate=
- =cert.exists : A : fol.type -> fol.term A -> cert.certificate -> cert.certificate=
The certificate =cert.trivial= proves the goal =fol.true=. The
certificate =cert.split c1 c2= proves =fol.and A B= if =c1= proves =A=
and =c2= proves =B=. The certificate =cert.left c= proves =fol.or A B=
if =c= proves =A=. The certificate =cert.right c= proves =fol.or A B=
if =c= proves =B=. The certificate =cert.exists A a c= proves =fol.ex
A B= if =c= proves =B a=.
*** Reasoning on the assumptions
The following certificates are used to reason from assumptions:
- =cert.exfalso : cert.certificate -> cert.certificate=
- =cert.destruct_and : fol.prop -> fol.prop -> cert.certificate -> cert.certificate -> cert.certificate=
- =cert.destruct_or : fol.prop -> fol.prop -> cert.certificate -> cert.certificate -> cert.certificate -> cert.certificate=
- =cert.destruct_imp : fol.prop -> fol.prop -> cert.certificate -> cert.certificate -> cert.certificate -> cert.certificate=
- =cert.destruct_all : A : fol.type -> (fol.term A -> fol.prop) -> fol.term A -> cert.certificate -> cert.certificate -> cert.certificate=
- =cert.destruct_ex : A : fol.type -> (fol.term A -> fol.prop) -> cert.certificate -> cert.certificate -> cert.certificate=
The certificate =cert.exfalso c= proves the current goal if =c= proves
=fol.false=. The certificate =cert.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 certificate =cert.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
certificate =cert.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 certificate =cert.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 type
=A= and an extra assumption =B x=.
** Equality Certificates
The file [[./meta/eqcert.dk][meta/eqcert.dk]] defines a few certificate combinators to
reason about equality:
- =eqcert.match_equality : fol.prop -> (A : fol.type -> fol.term A -> fol.term A -> cert.certificate) -> cert.certificate -> cert.certificate=
- =eqcert.reflexivity : cert.certificate=
- =eqcert.symmetry : cert.certificate -> cert.certificate=
- =eqcert.transitivity : A : fol.type -> fol.term A -> cert.certificate -> cert.certificate -> cert.certificate=
- =eqcert.f_equal : f : fol.function -> c1 : cert.certificate -> … -> cn : cert.certificate -> cert.certificate=
(where the arity of =f= has length =n=)
- =eqcert.rewrite : A : fol.type -> fol.term A -> fol.term A -> cert.certificate -> cert.certificate=
The certificate =eqcert.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 certificate
=eqcert.reflexivity= proves goals of the form =eq.eq A a a=. The
certificate =eqcert.symmetry c= proves =eq.eq A a b= if =c= proves
=eq.eq A b a=. The certificate =eqcert.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 certificate =eqcert.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 certificate =eqcert.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 [[* Substitution and unification][the
section on substitution]]).
* TODO Examples
** Drinker paradox
** Decision procedures
*** Minimal logic
*** Presburger arithmetic
* TODO Interactive proof development
* TODO Checking output of automatic theorem provers
** Reasoning modulo AC, ACU, symmetry
** Substitution and unification
** Resolution