manual.org 39.9 KB
Newer Older
Raphael Cauderlier's avatar
Raphael Cauderlier committed
1 2 3 4 5
#+Title: Dktactics User Manual

* Introduction

This is a user manual for Dktactics. Dktactics is a Meta Dedukti
Raphael Cauderlier's avatar
Raphael Cauderlier committed
6 7
implementation of a typed tactic language and an untyped tactic
language.
Raphael Cauderlier's avatar
Raphael Cauderlier committed
8

Raphael Cauderlier's avatar
Raphael Cauderlier committed
9 10 11
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.
Raphael Cauderlier's avatar
Raphael Cauderlier committed
12 13 14 15

* Installation

Dktactics can be downloaded from
Raphael Cauderlier's avatar
Raphael Cauderlier committed
16
[[https://gitlab.math.univ-paris-diderot.fr/cauderlier/dktactics]]. Dependencies
Raphael Cauderlier's avatar
Raphael Cauderlier committed
17 18 19 20
and installation instructions are detailed in the file [[./README.org][README.org]].

* Multi-sorted first-order logic in Dedukti

Raphael Cauderlier's avatar
Raphael Cauderlier committed
21 22 23
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,
Raphael Cauderlier's avatar
Raphael Cauderlier committed
24 25 26 27 28 29
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
Raphael Cauderlier's avatar
Raphael Cauderlier committed
30
well studied so our choice of basing Dktactics on first-order logic
Raphael Cauderlier's avatar
Raphael Cauderlier committed
31 32 33 34 35 36 37 38 39 40 41
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
Raphael Cauderlier's avatar
Raphael Cauderlier committed
42
about [[* Resolution][resolution]].
Raphael Cauderlier's avatar
Raphael Cauderlier committed
43 44 45 46

** Why a multi-sorted logic?

We have chosen to use a multi-sorted version of first-order logic. In
Raphael Cauderlier's avatar
Raphael Cauderlier committed
47 48
this setting, the domain of a predicate or function symbol is a list
of sorts and each function symbol has a codomain sort.
Raphael Cauderlier's avatar
Raphael Cauderlier committed
49

Raphael Cauderlier's avatar
Raphael Cauderlier committed
50 51
We use a multi-sorted logic for two reasons. First, some automatic
provers such as Zenon Arith and Zipperposition work in this
Raphael Cauderlier's avatar
Raphael Cauderlier committed
52 53
setting. Second, multi-sorted logic ease the combination of
theories. Merging for example a theory of booleans containing the
Raphael Cauderlier's avatar
Raphael Cauderlier committed
54 55
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.
Raphael Cauderlier's avatar
Raphael Cauderlier committed
56 57 58 59

** Syntax

 The syntax of multi-sorted first-order logic is composed of four
Raphael Cauderlier's avatar
Raphael Cauderlier committed
60
 syntactic categories: sorts, terms, formulae, and proofs.
Raphael Cauderlier's avatar
Raphael Cauderlier committed
61

Raphael Cauderlier's avatar
Raphael Cauderlier committed
62
*** Sorts
Raphael Cauderlier's avatar
Raphael Cauderlier committed
63

Raphael Cauderlier's avatar
Raphael Cauderlier committed
64 65 66 67
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.
Raphael Cauderlier's avatar
Raphael Cauderlier committed
68

Raphael Cauderlier's avatar
Raphael Cauderlier committed
69 70 71 72 73
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=
Raphael Cauderlier's avatar
Raphael Cauderlier committed
74 75

For convenience, the file [[./fol/fol.dk][fol/fol.dk]] also defines an n-ary function
Raphael Cauderlier's avatar
Raphael Cauderlier committed
76 77
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)…)=
Raphael Cauderlier's avatar
Raphael Cauderlier committed
78

Raphael Cauderlier's avatar
Raphael Cauderlier committed
79
The first parameter =n= of =fol.read_sorts= is a natural number of
Raphael Cauderlier's avatar
Raphael Cauderlier committed
80 81 82 83 84 85 86 87 88 89 90
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

Raphael Cauderlier's avatar
Raphael Cauderlier committed
91 92 93
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=.
Raphael Cauderlier's avatar
Raphael Cauderlier committed
94 95 96

A function symbol is a Dedukti term of type =fol.function=.

Raphael Cauderlier's avatar
Raphael Cauderlier committed
97
A domain and a codomain are respectively associated to each function
Raphael Cauderlier's avatar
Raphael Cauderlier committed
98
symbol by the functions
Raphael Cauderlier's avatar
Raphael Cauderlier committed
99
- =fol.fun_domain : fol.function -> fol.sorts= and
Raphael Cauderlier's avatar
Raphael Cauderlier committed
100
- =fol.fun_codomain : fol.function -> fol.sort=
Raphael Cauderlier's avatar
Raphael Cauderlier committed
101

Raphael Cauderlier's avatar
Raphael Cauderlier committed
102 103 104
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
Raphael Cauderlier's avatar
Raphael Cauderlier committed
105
  of terms
Raphael Cauderlier's avatar
Raphael Cauderlier committed
106
- =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)=
Raphael Cauderlier's avatar
Raphael Cauderlier committed
107 108

The only constructor of =fol.term A= is application of a function
Raphael Cauderlier's avatar
Raphael Cauderlier committed
109
symbol =f= whose codomain is =A= to a list of terms whose sorts match
Raphael Cauderlier's avatar
Raphael Cauderlier committed
110 111
the domain of =f=.
- =fol.apply_fun : f : fol.function -> fol.terms (fol.fun_domain f) -> fol.term (fol.fun_codomain f)=
Raphael Cauderlier's avatar
Raphael Cauderlier committed
112 113 114

For convenience, the file [[./fol/fol.dk][fol/fol.dk]] also defines an n-ary function
for applying a function symbol to terms:
Raphael Cauderlier's avatar
Raphael Cauderlier committed
115
- if =f= is a function symbol of domain =fol.read_sorts n A1 … An= and
Raphael Cauderlier's avatar
Raphael Cauderlier committed
116 117
  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=.
Raphael Cauderlier's avatar
Raphael Cauderlier committed
118 119 120 121 122 123 124 125 126 127 128

*** 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

Raphael Cauderlier's avatar
Raphael Cauderlier committed
129
An atom is a predicate symbol applied to terms respecting the domain of
Raphael Cauderlier's avatar
Raphael Cauderlier committed
130 131
the predicate symbol. Predicate symbols and their arities are defined
similarly to function symbols. A predicate symbol is a Dedukti term of
Raphael Cauderlier's avatar
Typos  
Raphael Cauderlier committed
132
type =fol.predicate=. An artity is associated to each predicate
Raphael Cauderlier's avatar
Raphael Cauderlier committed
133
symbol by the function
Raphael Cauderlier's avatar
Raphael Cauderlier committed
134
- =fol.pred_domain : fol.predicate -> fol.sorts=
Raphael Cauderlier's avatar
Raphael Cauderlier committed
135

Raphael Cauderlier's avatar
Raphael Cauderlier committed
136
Applying a predicate symbol on a list of terms respecting its domain
Raphael Cauderlier's avatar
Raphael Cauderlier committed
137
produces a formula:
Raphael Cauderlier's avatar
Raphael Cauderlier committed
138
- =fol.apply_pred : p : fol.predicate -> fol.terms (fol.pred_domain p) -> fol.prop=
Raphael Cauderlier's avatar
Raphael Cauderlier committed
139 140 141

For convenience, the file [[./fol/fol.dk][fol/fol.dk]] also defines an n-ary function
for applying a predicate symbol to terms:
Raphael Cauderlier's avatar
Raphael Cauderlier committed
142
- if =p= is a predicate symbol of domain =fol.read_sorts n A1 … An= and
Raphael Cauderlier's avatar
Raphael Cauderlier committed
143
  if =a1=, …, =an= are =n= terms of sort =A1=, …, =An= respectively,
Raphael Cauderlier's avatar
Raphael Cauderlier committed
144 145 146 147 148 149 150 151 152 153
  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
Raphael Cauderlier's avatar
Raphael Cauderlier committed
154
all other connectives are binary.
Raphael Cauderlier's avatar
Raphael Cauderlier committed
155 156 157 158 159 160 161 162 163 164 165

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
Raphael Cauderlier's avatar
Raphael Cauderlier committed
166
binds a single variable of a given sort. As we promised in [[* Terms][the section
Raphael Cauderlier's avatar
Raphael Cauderlier committed
167 168 169 170
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=
Raphael Cauderlier's avatar
Raphael Cauderlier committed
171
and =fol.ex=. They have the same Dedukti type: =A : fol.sort -> (fol.term A -> fol.prop) -> fol.prop=.
Raphael Cauderlier's avatar
Raphael Cauderlier committed
172

Raphael Cauderlier's avatar
Raphael Cauderlier committed
173 174 175 176 177
**** 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
Raphael Cauderlier's avatar
Raphael Cauderlier committed
178
sorts:
Raphael Cauderlier's avatar
Raphael Cauderlier committed
179 180 181
- =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=
Raphael Cauderlier's avatar
Raphael Cauderlier committed
182 183
- =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=
Raphael Cauderlier's avatar
Raphael Cauderlier committed
184 185 186 187 188 189 190 191 192

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ₙ)…))=
193

Raphael Cauderlier's avatar
Raphael Cauderlier committed
194 195 196 197 198 199 200 201
*** 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
Raphael Cauderlier's avatar
Raphael Cauderlier committed
202
corresponding tactics presented in [[* Reasoning][the reasoning section]]):
Raphael Cauderlier's avatar
Raphael Cauderlier committed
203 204
- =fol.false_elim : A : fol.prop -> fol.proof fol.false -> fol.proof A=
- =fol.true_intro : fol.proof fol.true=
Raphael Cauderlier's avatar
Raphael Cauderlier committed
205 206 207 208 209 210 211 212
- =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=
Raphael Cauderlier's avatar
Raphael Cauderlier committed
213 214 215 216
- =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=
Raphael Cauderlier's avatar
Raphael Cauderlier committed
217 218 219 220 221

** 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
Raphael Cauderlier's avatar
Raphael Cauderlier committed
222
=fol.sort=, =fol.predicate=, and =fol.function= respectively. We then
Raphael Cauderlier's avatar
Raphael Cauderlier committed
223
define the domain of each function and predicate symbol and the
Raphael Cauderlier's avatar
Raphael Cauderlier committed
224
codomain sort of each function symbol by extending the definitions of
Raphael Cauderlier's avatar
Raphael Cauderlier committed
225
=fol.pred_domain=, =fol.fun_domain=, and =fol.fun_codomain= respectively.
Raphael Cauderlier's avatar
Raphael Cauderlier committed
226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241

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
Raphael Cauderlier's avatar
Typos  
Raphael Cauderlier committed
242
[[./fol/eq.dk][fol/eq.dk]]. Equality is a family of predicate symbols parameterized by
Raphael Cauderlier's avatar
Raphael Cauderlier committed
243
a sort:
Raphael Cauderlier's avatar
Raphael Cauderlier committed
244
- =eq.Eq : fol.sort -> fol.predicate=
Raphael Cauderlier's avatar
Raphael Cauderlier committed
245

Raphael Cauderlier's avatar
Raphael Cauderlier committed
246
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=.
Raphael Cauderlier's avatar
Raphael Cauderlier committed
247

Raphael Cauderlier's avatar
Raphael Cauderlier committed
248
The shortcut notation =eq.eq A a b= where =A= has type =fol.sort= and
Raphael Cauderlier's avatar
Raphael Cauderlier committed
249 250 251 252 253 254
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:
Raphael Cauderlier's avatar
Raphael Cauderlier committed
255
- Equality is reflexive:
Raphael Cauderlier's avatar
Raphael Cauderlier committed
256
  =eq.eq_refl : A : fol.sort -> fol.proof (fol.all A (x => eq.eq A x x))=
Raphael Cauderlier's avatar
Raphael Cauderlier committed
257
- Equality is symmetric:
Raphael Cauderlier's avatar
Raphael Cauderlier committed
258
  =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))))=
Raphael Cauderlier's avatar
Raphael Cauderlier committed
259
- Equality is transitive:
Raphael Cauderlier's avatar
Raphael Cauderlier committed
260
  =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))))))=
Raphael Cauderlier's avatar
Raphael Cauderlier committed
261
- Equality is a congruence with respect to all function symbols:
Raphael Cauderlier's avatar
Raphael Cauderlier committed
262
  =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)))) …))))=
Raphael Cauderlier's avatar
Raphael Cauderlier committed
263
  where =f= has domain =fol.read_sorts n A1 … An= and codomain =B=.
Raphael Cauderlier's avatar
Raphael Cauderlier committed
264
- Equality is a congruence with respect to all predicate symbols:
Raphael Cauderlier's avatar
Raphael Cauderlier committed
265
  =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)))) …))))=
Raphael Cauderlier's avatar
Raphael Cauderlier committed
266
  where =p= has domain =fol.read_yypes n A1 … An=
Raphael Cauderlier's avatar
Raphael Cauderlier committed
267

Raphael Cauderlier's avatar
Raphael Cauderlier committed
268
* The typed tactic language
Raphael Cauderlier's avatar
Raphael Cauderlier committed
269 270 271 272

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
Raphael Cauderlier's avatar
Typos  
Raphael Cauderlier committed
273
  and terminating.
Raphael Cauderlier's avatar
Raphael Cauderlier committed
274
- Subject-reduction: Typing is preserved by reduction according to
Raphael Cauderlier's avatar
Typos  
Raphael Cauderlier committed
275
  this rewrite-system.
Raphael Cauderlier's avatar
Raphael Cauderlier committed
276 277 278 279
- 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
Raphael Cauderlier's avatar
Typos  
Raphael Cauderlier committed
280
  obtained by encoding an inconsistent first-order theory.
Raphael Cauderlier's avatar
Raphael Cauderlier committed
281 282 283 284 285 286 287 288 289 290 291 292 293 294 295 296 297 298

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
Raphael Cauderlier's avatar
Typos  
Raphael Cauderlier committed
299
  inductive constructions.
Raphael Cauderlier's avatar
Raphael Cauderlier committed
300 301
- In Dedukti it is not necessary to encode pattern matching and
  recursion directly in the tactic language because the user can
Raphael Cauderlier's avatar
Typos  
Raphael Cauderlier committed
302
  already use rewriting for these tasks.
Raphael Cauderlier's avatar
Raphael Cauderlier committed
303 304 305 306 307 308 309
- 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
Raphael Cauderlier's avatar
Raphael Cauderlier committed
310
inside a monad defined in the file [[./meta/tac.dk][meta/mtac.dk]] whose main purpose is
Raphael Cauderlier's avatar
Raphael Cauderlier committed
311 312
to handle failure and backtracking.

Raphael Cauderlier's avatar
Raphael Cauderlier committed
313 314 315
- =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=
Raphael Cauderlier's avatar
Raphael Cauderlier committed
316

Raphael Cauderlier's avatar
Raphael Cauderlier committed
317
If =A= is a formula, =mtac.mtactic A= is the Dedukti type of the tactics
Raphael Cauderlier's avatar
Typos  
Raphael Cauderlier committed
318
attempting to prove =A=. It forms a monad whose return and bind
Raphael Cauderlier's avatar
Raphael Cauderlier committed
319
operations are =mtac.mret= and =mtac.mbind= respectively.
Raphael Cauderlier's avatar
Raphael Cauderlier committed
320

Raphael Cauderlier's avatar
Raphael Cauderlier committed
321 322
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=
Raphael Cauderlier's avatar
Raphael Cauderlier committed
323 324

It is defined by the following rewrite rule:
325
- =[a] mtac.mrun _ (mtac.mret _ a) --> a=
Raphael Cauderlier's avatar
Raphael Cauderlier committed
326 327 328

** Exceptions and backtracking

Raphael Cauderlier's avatar
Raphael Cauderlier committed
329
Exceptions form an open inductive type =mtac.exc=.
Raphael Cauderlier's avatar
Raphael Cauderlier committed
330
A tactic can fail to prove its goal by raising an exception:
Raphael Cauderlier's avatar
Raphael Cauderlier committed
331
- =mtac.mraise : A : fol.prop -> mtac.exc -> mtac.mtactic A=
Raphael Cauderlier's avatar
Raphael Cauderlier committed
332

Raphael Cauderlier's avatar
Raphael Cauderlier committed
333
Exceptions can be caught by the =mtac.mtry= tactic combinator
Raphael Cauderlier's avatar
Raphael Cauderlier committed
334
implementing backtracking:
Raphael Cauderlier's avatar
Raphael Cauderlier committed
335
- =mtac.mtry : A : fol.prop -> mtac.mtactic A -> (mtac.exc -> mtac.mtactic A) -> tactic A=
Raphael Cauderlier's avatar
Raphael Cauderlier committed
336

Raphael Cauderlier's avatar
Raphael Cauderlier committed
337
The tactic =mtac.mtry A t f= first tries the tactic =t=, if it succeeds
Raphael Cauderlier's avatar
Raphael Cauderlier committed
338 339 340 341 342 343 344
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
Raphael Cauderlier's avatar
Raphael Cauderlier committed
345
context, we use non-linear higher-order rewriting to define the symbols =mtac.mintro_term= and =mtac.mintro_proof=:
Raphael Cauderlier's avatar
Raphael Cauderlier committed
346
#+BEGIN_SRC dedukti
Raphael Cauderlier's avatar
Raphael Cauderlier committed
347
  def intro_term : A : fol.sort ->
Raphael Cauderlier's avatar
Raphael Cauderlier committed
348
                   B : (fol.term A -> fol.prop) ->
Raphael Cauderlier's avatar
Raphael Cauderlier committed
349 350
                   (x : fol.term A -> mtac.mtactic (B x)) ->
                   mtac.mtactic (fol.all A B).
Raphael Cauderlier's avatar
Raphael Cauderlier committed
351 352
  def intro_proof : A : fol.prop ->
                    B : fol.prop ->
Raphael Cauderlier's avatar
Raphael Cauderlier committed
353 354
                    (fol.proof A -> mtac.mtactic B) ->
                    mtac.mtactic (fol.imp A B).
Raphael Cauderlier's avatar
Raphael Cauderlier committed
355

Raphael Cauderlier's avatar
Raphael Cauderlier committed
356
  [A,B,b] mtac.mintro_term A B (x => mtac.mret (B x) (b x))
Raphael Cauderlier's avatar
Raphael Cauderlier committed
357
        -->
Raphael Cauderlier's avatar
Raphael Cauderlier committed
358 359
     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)
Raphael Cauderlier's avatar
Raphael Cauderlier committed
360
        -->
Raphael Cauderlier's avatar
Raphael Cauderlier committed
361 362
     mtac.mraise (fol.all A B) e.
  [A,B,b] mtac.mintro_proof A B (x => mtac.mret B (b x))
Raphael Cauderlier's avatar
Raphael Cauderlier committed
363
        -->
Raphael Cauderlier's avatar
Raphael Cauderlier committed
364 365
     mtac.mret (fol.imp A B) (x : fol.proof A => b x)
  [A,B,e] mtac.mintro_proof A B (x => mtac.mraise _ e)
Raphael Cauderlier's avatar
Raphael Cauderlier committed
366
        -->
Raphael Cauderlier's avatar
Raphael Cauderlier committed
367
     mtac.mraise (fol.imp A B) e.
Raphael Cauderlier's avatar
Raphael Cauderlier committed
368 369
#+END_SRC

Raphael Cauderlier's avatar
Raphael Cauderlier committed
370
* The untyped tactic language
Raphael Cauderlier's avatar
Raphael Cauderlier committed
371

Raphael Cauderlier's avatar
Raphael Cauderlier committed
372 373 374 375
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.
Raphael Cauderlier's avatar
Raphael Cauderlier committed
376

Raphael Cauderlier's avatar
Raphael Cauderlier committed
377
The untyped tactic language is defined in file [[./meta/tactic.dk][meta/tactic.dk]].
Raphael Cauderlier's avatar
Raphael Cauderlier committed
378

Raphael Cauderlier's avatar
Raphael Cauderlier committed
379
** Contexts and tactic evaluation
Raphael Cauderlier's avatar
Raphael Cauderlier committed
380

Raphael Cauderlier's avatar
Raphael Cauderlier committed
381 382 383 384
=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.
Raphael Cauderlier's avatar
Raphael Cauderlier committed
385

Raphael Cauderlier's avatar
Raphael Cauderlier committed
386 387
Our untyped tacitc language is inspired by the LTac language which is
the default tactic language of the Coq proof assistant.
Raphael Cauderlier's avatar
Raphael Cauderlier committed
388

Raphael Cauderlier's avatar
Raphael Cauderlier committed
389 390 391 392
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.
Raphael Cauderlier's avatar
Raphael Cauderlier committed
393

Raphael Cauderlier's avatar
Raphael Cauderlier committed
394 395 396 397 398
- =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=
399
- =tactic.eval_tactic : tactic.context -> A : fol.prop -> tactic.tactic -> mtac.mtactic A=
Raphael Cauderlier's avatar
Raphael Cauderlier committed
400
- =tactic.prove : A : fol.prop -> tactic.tactic -> fol.proof A=
Raphael Cauderlier's avatar
Raphael Cauderlier committed
401

Raphael Cauderlier's avatar
Raphael Cauderlier committed
402
** Tactic primitives
Raphael Cauderlier's avatar
Raphael Cauderlier committed
403

Raphael Cauderlier's avatar
Raphael Cauderlier committed
404 405 406 407 408
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.
Raphael Cauderlier's avatar
Raphael Cauderlier committed
409

Raphael Cauderlier's avatar
Raphael Cauderlier committed
410 411
The simplest primitives reflect the two constructors =mtac.mret= and
=mtac.mraise= of the tactic monad:
Raphael Cauderlier's avatar
Raphael Cauderlier committed
412

Raphael Cauderlier's avatar
Raphael Cauderlier committed
413 414
- =tactic.exact : A : fol.prop -> fol.proof A -> tactic.tactic=
- =tactic.raise : mtac.exc -> tactic.tactic=
Raphael Cauderlier's avatar
Raphael Cauderlier committed
415

Raphael Cauderlier's avatar
Raphael Cauderlier committed
416
The =tactic.exact A a= tactic succeeds if and only if its goal is
Raphael Cauderlier's avatar
Raphael Cauderlier committed
417
=A= in which case =mtac.mret A a= is returned. Otherwise the exception
Raphael Cauderlier's avatar
Raphael Cauderlier committed
418
=tactic.exact_mismatch= is raised.
Raphael Cauderlier's avatar
Raphael Cauderlier committed
419

Raphael Cauderlier's avatar
Raphael Cauderlier committed
420
The =tactic.raise e= tactic always raises the exception =e=.
Raphael Cauderlier's avatar
Raphael Cauderlier committed
421

Raphael Cauderlier's avatar
Raphael Cauderlier committed
422 423
The other operations of the monad, =mtac.mtry=, =mtac.mbind=,
=mtac.mintro_term= and =mtac.mintro_proof= are also reflected:
Raphael Cauderlier's avatar
Raphael Cauderlier committed
424 425 426 427 428 429 430 431 432
- =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
Raphael Cauderlier's avatar
Raphael Cauderlier committed
433 434 435
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
Raphael Cauderlier's avatar
Raphael Cauderlier committed
436 437
sort =A=. On any other goal, the tactic =tactic.intro c= raises the
exception =tactic.not_a_product=.
Raphael Cauderlier's avatar
Raphael Cauderlier committed
438

Raphael Cauderlier's avatar
Raphael Cauderlier committed
439
Moreover, the file [[./meta/cert.dk][meta/tactic.dk]] defines tactic primitives for
Raphael Cauderlier's avatar
Raphael Cauderlier committed
440
manipulating the proof state:
Raphael Cauderlier's avatar
Raphael Cauderlier committed
441 442 443
- =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=
Raphael Cauderlier's avatar
Raphael Cauderlier committed
444

Raphael Cauderlier's avatar
Raphael Cauderlier committed
445
The =tactic.with_goal f= tactic successfully proves the goal =A= in
Raphael Cauderlier's avatar
Raphael Cauderlier committed
446
context =G= if and only if =f A= does so. Similarly,
Raphael Cauderlier's avatar
Raphael Cauderlier committed
447 448
=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=
Raphael Cauderlier's avatar
Raphael Cauderlier committed
449 450 451
succeeds in context =G= if and only if =c= succeeds in the context
obtained from =G= by removing all the assumptions proving =A=.

Raphael Cauderlier's avatar
Raphael Cauderlier committed
452 453 454
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=
Raphael Cauderlier's avatar
Raphael Cauderlier committed
455

Raphael Cauderlier's avatar
Raphael Cauderlier committed
456
The tactic =tactic.repeat f= is equivalent to the tactic =f (tactic.repeat f)=.
Raphael Cauderlier's avatar
Raphael Cauderlier committed
457 458 459 460

** Trying assumptions or variables

Instead of abstracting over the full context using
Raphael Cauderlier's avatar
Raphael Cauderlier committed
461
=tactic.with_context=, it is often more convenient to try all
Raphael Cauderlier's avatar
Raphael Cauderlier committed
462
assumptions or all variables in parallel. This behaviour is provided
Raphael Cauderlier's avatar
Raphael Cauderlier committed
463 464 465
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=
Raphael Cauderlier's avatar
Raphael Cauderlier committed
466

Raphael Cauderlier's avatar
Raphael Cauderlier committed
467
The =tactic.with_assumption f= tactic is successful if =f A a= is
Raphael Cauderlier's avatar
Raphael Cauderlier committed
468
successful for any assumption =a : fol.proof A=. Otherwise, it raises
Raphael Cauderlier's avatar
Raphael Cauderlier committed
469 470
the exception =tactic.no_successful_assumption=. Similarly,
=tactic.with_variable f= is successful if =f A a= is successful for any
Raphael Cauderlier's avatar
Raphael Cauderlier committed
471
variable =a : fol.term A=. Otherwise it raises the exception
Raphael Cauderlier's avatar
Raphael Cauderlier committed
472
=tactic.no_successful_variable=.
Raphael Cauderlier's avatar
Raphael Cauderlier committed
473 474

A particular case is looking for the current goal among the
Raphael Cauderlier's avatar
Raphael Cauderlier committed
475 476
assumptions. This is provided by the =tactic.assumption= tactic:
- =tactic.assumption : tactic.tactic=
Raphael Cauderlier's avatar
Raphael Cauderlier committed
477 478 479

** Pattern matching

Raphael Cauderlier's avatar
Raphael Cauderlier committed
480
A lot of tactics perform different actions depending on the shape
Raphael Cauderlier's avatar
Raphael Cauderlier committed
481
of the goal or of assumptions. We have seen an example with the
Raphael Cauderlier's avatar
Raphael Cauderlier committed
482 483
=tactic.intro c= tactic in [[* Certificate primitives][the section about tactic
primitives]]. In general, the tactic combinator =tactic.match_prop=
Raphael Cauderlier's avatar
Raphael Cauderlier committed
484 485 486
can be used for this purpose:

#+BEGIN_SRC dedukti
Raphael Cauderlier's avatar
Raphael Cauderlier committed
487 488 489 490 491 492 493
  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) ->
Raphael Cauderlier's avatar
Raphael Cauderlier committed
494
                    (p : fol.predicate ->
Raphael Cauderlier's avatar
Raphael Cauderlier committed
495
                     fol.terms (fol.pred_domain p) ->
Raphael Cauderlier's avatar
Raphael Cauderlier committed
496 497
                     tactic.tactic) ->
                    tactic.tactic
Raphael Cauderlier's avatar
Raphael Cauderlier committed
498 499 500

#+END_SRC

Raphael Cauderlier's avatar
Raphael Cauderlier committed
501
The tactic =tactic.match_prop C cfalse cand cor cimp call cex
Raphael Cauderlier's avatar
Raphael Cauderlier committed
502 503 504 505 506 507 508 509 510 511
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
Raphael Cauderlier's avatar
Raphael Cauderlier committed
512
possible so [[./meta/cert.dk][meta/tactic.dk]] provides the following combinators matching
Raphael Cauderlier's avatar
Raphael Cauderlier committed
513
on each of the cases:
Raphael Cauderlier's avatar
Raphael Cauderlier committed
514 515 516 517 518 519 520
- =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=
Raphael Cauderlier's avatar
Raphael Cauderlier committed
521

Raphael Cauderlier's avatar
Raphael Cauderlier committed
522
** Sort and formulae comparison
Raphael Cauderlier's avatar
Raphael Cauderlier committed
523 524 525

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
Raphael Cauderlier's avatar
Raphael Cauderlier committed
526
sorts are identical and obtain coercion functions when they are.
Raphael Cauderlier's avatar
Raphael Cauderlier committed
527 528

This behaviour is provided by the following combinators:
Raphael Cauderlier's avatar
Raphael Cauderlier committed
529 530
- =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=
Raphael Cauderlier's avatar
Raphael Cauderlier committed
531 532 533

** Reasoning

Raphael Cauderlier's avatar
Raphael Cauderlier committed
534
In this section, we list the tactic combinators that are used to
Raphael Cauderlier's avatar
Raphael Cauderlier committed
535
perform reasoning steps. In fact we already met some of them, namely
Raphael Cauderlier's avatar
Raphael Cauderlier committed
536 537
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
Raphael Cauderlier's avatar
Raphael Cauderlier committed
538 539 540 541 542
implications and universal quantifications.

*** Applying a lemma

The following combinators are used to apply a lemma:
Raphael Cauderlier's avatar
Raphael Cauderlier committed
543 544 545 546 547
- =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=
Raphael Cauderlier's avatar
Raphael Cauderlier committed
548

Raphael Cauderlier's avatar
Raphael Cauderlier committed
549 550
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=.
Raphael Cauderlier's avatar
Raphael Cauderlier committed
551

Raphael Cauderlier's avatar
Raphael Cauderlier committed
552
The tactic =tactic.refine2 A B C f c1 c2= is similar for a lemma
Raphael Cauderlier's avatar
Raphael Cauderlier committed
553 554
with two assumptions =A= and =B= proved respectively by =c1= and =c2=.

Raphael Cauderlier's avatar
Raphael Cauderlier committed
555
The tactic =tactic.refinen n A1 … An B f c1 … cn= is similar for a
Raphael Cauderlier's avatar
Raphael Cauderlier committed
556 557 558
lemma with =n= assumptions =A1= … =An= proved respectively by =c1= …
=cn=.

Raphael Cauderlier's avatar
Raphael Cauderlier committed
559
The tactic =tactic.assert A c1 c2= proves the current goal =B= in
Raphael Cauderlier's avatar
Raphael Cauderlier committed
560 561 562
the current context =G= if =c1= proves =A= in context =G= and =c2=
proves =B= in context =G= with =A= as extra assumption.

Raphael Cauderlier's avatar
Raphael Cauderlier committed
563
The tactic =tactic.apply A B a c= proves =B a= if =c= proves
Raphael Cauderlier's avatar
Raphael Cauderlier committed
564 565 566 567
=fol.all A B=.

*** Reasoning on the goal

Raphael Cauderlier's avatar
Raphael Cauderlier committed
568
The following tactics are used to reason on the current goal,
Raphael Cauderlier's avatar
Typos  
Raphael Cauderlier committed
569
each proves the current goal if it has a particular shape:
Raphael Cauderlier's avatar
Raphael Cauderlier committed
570 571 572 573 574 575 576 577 578 579 580
- =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
Raphael Cauderlier's avatar
Raphael Cauderlier committed
581 582 583 584
A B= if =c= proves =B a=.

*** Reasoning on the assumptions

Raphael Cauderlier's avatar
Raphael Cauderlier committed
585 586 587 588 589 590 591 592 593 594 595
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
Raphael Cauderlier's avatar
Raphael Cauderlier committed
596
the context contains a pair of contradictory assumptions (an
Raphael Cauderlier's avatar
Raphael Cauderlier committed
597 598
assumption together with its negation). The tactic
=tactic.destruct_and A B c1 c2= proves the current goal =C= in context
Raphael Cauderlier's avatar
Raphael Cauderlier committed
599
=G= if =c1= proves =fol.and A B= in context =G= and =c2= proves =C= in
Raphael Cauderlier's avatar
Raphael Cauderlier committed
600 601
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
Raphael Cauderlier's avatar
Raphael Cauderlier committed
602 603
=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
Raphael Cauderlier's avatar
Raphael Cauderlier committed
604
=G= with extra assumption =B=. The tactic =tactic.destruct_imp A B
Raphael Cauderlier's avatar
Raphael Cauderlier committed
605 606
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=
Raphael Cauderlier's avatar
Raphael Cauderlier committed
607 608
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
Raphael Cauderlier's avatar
Raphael Cauderlier committed
609
=G= if =c1= proves =fol.ex A B= and =c2= proves =C= in context =G=
Raphael Cauderlier's avatar
Raphael Cauderlier committed
610
with an extra variable =x= of sort =A= and an extra assumption =B x=.
Raphael Cauderlier's avatar
Raphael Cauderlier committed
611

Raphael Cauderlier's avatar
Raphael Cauderlier committed
612
** Equality Tactics
Raphael Cauderlier's avatar
Raphael Cauderlier committed
613

Raphael Cauderlier's avatar
Raphael Cauderlier committed
614 615 616 617 618 619 620
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=
Raphael Cauderlier's avatar
Raphael Cauderlier committed
621
  (where the domain of =f= has length =n=)
Raphael Cauderlier's avatar
Raphael Cauderlier committed
622
- =eqtac.rewrite : A : fol.sort -> fol.term A -> fol.term A -> tactic.tactic -> tactic.tactic=
Raphael Cauderlier's avatar
Raphael Cauderlier committed
623

Raphael Cauderlier's avatar
Raphael Cauderlier committed
624 625 626 627 628
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
Raphael Cauderlier's avatar
Raphael Cauderlier committed
629
goals of the form =eq.eq A a c= if =c1= proves =eq.eq A a b= and =c2=
Raphael Cauderlier's avatar
Raphael Cauderlier committed
630
proves =eq.eq A b c=. The tactic =eqtac.f_equal f c1 … cn=
Raphael Cauderlier's avatar
Raphael Cauderlier committed
631
proves =eq.eq B (fol.fun_apply f a1 … an) (fol.fun_apply f a1' … an')=
Raphael Cauderlier's avatar
Raphael Cauderlier committed
632
if each =ci= proves =eq.eq Ai ai ai'=. The tactic =eqtac.rewrite
Raphael Cauderlier's avatar
Raphael Cauderlier committed
633
A a a' c1 c2= proves =B= if =c1= proves =eq.eq A a a'= and =c2= proves
Raphael Cauderlier's avatar
Raphael Cauderlier committed
634
=B= in which each occurrence of =a= has been replaced by =a'= (see [[* Substitutions][the
Raphael Cauderlier's avatar
Raphael Cauderlier committed
635 636
section on substitution]]).

637 638 639 640 641
** 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))=

Raphael Cauderlier's avatar
Raphael Cauderlier committed
642 643 644
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=
645

Raphael Cauderlier's avatar
Raphael Cauderlier committed
646 647
=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=
648 649 650 651
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=.

Raphael Cauderlier's avatar
Raphael Cauderlier committed
652 653
=classical_tactics.contradict= is used to prove by contradiction using
double-negation elimination. =classical_tactics.contradict c= proves the
654 655 656 657
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:
Raphael Cauderlier's avatar
Raphael Cauderlier committed
658 659 660
- =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)))=
661 662

* Examples
Raphael Cauderlier's avatar
Raphael Cauderlier committed
663
** Drinker paradox
664 665 666 667 668 669 670 671 672 673 674 675 676 677 678 679 680 681

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
Raphael Cauderlier's avatar
Raphael Cauderlier committed
682
a classical reasoning by case (using the =classical_tactics.prop_case=
683
combinator) and then uses the classical lemma
Raphael Cauderlier's avatar
Raphael Cauderlier committed
684
=classical_tactics.not_all_is_ex_not= in the second branch.
685 686

** TODO Decision procedures
Raphael Cauderlier's avatar
Raphael Cauderlier committed
687 688 689
*** Minimal logic
*** Presburger arithmetic
* TODO Interactive proof development
690 691
* Checking output of automatic theorem provers
** TODO Reasoning modulo AC, ACU, symmetry
Raphael Cauderlier's avatar
Raphael Cauderlier committed
692

693 694 695 696 697 698 699 700 701 702 703 704 705 706 707
** 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
Raphael Cauderlier's avatar
Raphael Cauderlier committed
708
    having the same sort).
709 710 711

    - =unif.substition : Type=
    - =unif.empty_subst : unif.substitution=
Raphael Cauderlier's avatar
Raphael Cauderlier committed
712
    - =unif.cons_subst : A : fol.sort -> fol.term A -> fol.term A -> unif.substitution -> unif.substitution=
713 714 715

    Substitutions can be applied on propositions, terms, and list of terms.
    - =unif.subst_prop : unif.substitution -> fol.prop -> fol.prop=
Raphael Cauderlier's avatar
Raphael Cauderlier committed
716 717
    - =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=
718 719 720 721 722 723 724 725 726 727 728 729 730 731 732 733 734 735 736 737 738 739 740

    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=

741
*** Unification
742 743

    A (first-order) unification problem is a list of pairs of terms
Raphael Cauderlier's avatar
Raphael Cauderlier committed
744
    (both terms having the same sort). Unification can either fail or
745 746 747 748 749
    return a substitution, the most general unifier of the unification
    problem.

    - =unif.unify_problem : Type=
    - =unif.unify_nil : unif.unify_problem=
Raphael Cauderlier's avatar
Raphael Cauderlier committed
750
    - =unif.unify_cons : A : fol.sort -> fol.term A -> fol.term A -> unif.unify_problem -> unif.unify_problem=
751 752 753 754 755 756 757 758 759

    - =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=.

Raphael Cauderlier's avatar
Raphael Cauderlier committed
760 761
** Resolution

762 763 764 765 766
   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.

767 768 769
   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
770 771 772
   variables which are to be interpreted as universally quantified. A
   *quantified clause* is an explicitly universally quantified clause.

773
   The types for atoms, literals, clauses, and quantified clauses are
774 775
   declared with their constructors in [[./fol/clauses.dk][fol/clauses.dk]]. However, the
   simplest way to define a clause is by parsing the corresponding
776 777 778
   proposition using the partial function
   =resolution.qclause_of_prop=:

779
   - =resolution.qclause_of_prop : fol.prop -> clauses.qclause=
780 781 782 783 784 785 786 787
   - =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ⱼ)
788
  ————————————————————————————————— Factorisation
789 790 791
  (l₁ ∨ … ∨ lⱼ₋₁ ∨ lⱼ₊₁ ∨ … ∨ lₙ)σ

  l₁ ∨ … ∨ lₙ              l'₁ ∨ … ∨ l'ₘ             σ = mgu(lᵢ, ¬l'ⱼ)
792
  ——————————————————————————————————————————————————————————————————————— Resolution
793 794 795 796 797 798 799 800 801 802 803
  (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]].