manual.org 30.4 KB
Newer Older
Raphael Cauderlier's avatar
Raphael Cauderlier committed
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15
#+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
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
Dktactics is a tactic and certificate language for multi-sorted
Raphael Cauderlier's avatar
Raphael Cauderlier committed
22 23 24 25 26 27 28 29
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
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 47 48 49 50

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

Raphael Cauderlier's avatar
Raphael Cauderlier committed
51 52
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
53 54
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
55 56
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
57 58 59 60 61 62 63 64 65 66 67

** 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
Raphael Cauderlier's avatar
Raphael Cauderlier committed
68
to declare the various types she needs.
Raphael Cauderlier's avatar
Raphael Cauderlier committed
69 70 71 72 73 74 75 76 77

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:
Raphael Cauderlier's avatar
Raphael Cauderlier committed
78
- =fol.read_types n A1 … An= is defined as =fol.cons_type A1 (… (fol.cons_type An fol.nil_type)…)=
Raphael Cauderlier's avatar
Raphael Cauderlier committed
79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106

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
Raphael Cauderlier's avatar
Raphael Cauderlier committed
107
- =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)=
Raphael Cauderlier's avatar
Raphael Cauderlier committed
108 109 110 111

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=.
Raphael Cauderlier's avatar
Raphael Cauderlier committed
112
- =fol.apply_fun : f : fol.function -> fol.terms (fol.fun_arity f) -> fol.term (fol.fun_codomain f)=
Raphael Cauderlier's avatar
Raphael Cauderlier committed
113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132

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
Raphael Cauderlier's avatar
Typos  
Raphael Cauderlier committed
133
type =fol.predicate=. An artity is associated to each predicate
Raphael Cauderlier's avatar
Raphael Cauderlier committed
134 135 136 137 138
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:
Raphael Cauderlier's avatar
Raphael Cauderlier committed
139
- =fol.apply_pred : p : fol.predicate -> fol.terms (fol.pred_arity p) -> fol.prop=
Raphael Cauderlier's avatar
Raphael Cauderlier committed
140 141 142 143 144 145 146 147 148 149 150 151 152 153 154

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
Raphael Cauderlier's avatar
Raphael Cauderlier committed
155
all other connectives are binary.
Raphael Cauderlier's avatar
Raphael Cauderlier committed
156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171

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=
Raphael Cauderlier's avatar
Raphael Cauderlier committed
172
and =fol.ex=. They have the same Dedukti type: =A : fol.type -> (fol.term A -> fol.prop) -> fol.prop=.
Raphael Cauderlier's avatar
Raphael Cauderlier committed
173 174 175 176 177 178 179 180 181 182 183 184 185

*** 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=
Raphael Cauderlier's avatar
Raphael Cauderlier committed
186 187 188 189 190 191 192 193 194 195 196 197
- =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=
Raphael Cauderlier's avatar
Raphael Cauderlier committed
198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222

** 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
Raphael Cauderlier's avatar
Typos  
Raphael Cauderlier committed
223
[[./fol/eq.dk][fol/eq.dk]]. Equality is a family of predicate symbols parameterized by
Raphael Cauderlier's avatar
Raphael Cauderlier committed
224 225 226 227 228 229 230 231 232 233 234 235
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:
Raphael Cauderlier's avatar
Raphael Cauderlier committed
236 237 238 239 240 241
- 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))))))=
Raphael Cauderlier's avatar
Raphael Cauderlier committed
242
- Equality is a congruence with respect to all function symbols:
Raphael Cauderlier's avatar
Raphael Cauderlier committed
243 244
  =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=.
Raphael Cauderlier's avatar
Raphael Cauderlier committed
245
- Equality is a congruence with respect to all predicate symbols:
Raphael Cauderlier's avatar
Raphael Cauderlier committed
246 247
  =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=
Raphael Cauderlier's avatar
Raphael Cauderlier committed
248 249 250 251 252 253

* 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
Raphael Cauderlier's avatar
Typos  
Raphael Cauderlier committed
254
  and terminating.
Raphael Cauderlier's avatar
Raphael Cauderlier committed
255
- Subject-reduction: Typing is preserved by reduction according to
Raphael Cauderlier's avatar
Typos  
Raphael Cauderlier committed
256
  this rewrite-system.
Raphael Cauderlier's avatar
Raphael Cauderlier committed
257 258 259 260
- 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
261
  obtained by encoding an inconsistent first-order theory.
Raphael Cauderlier's avatar
Raphael Cauderlier committed
262 263 264 265 266 267 268 269 270 271 272 273 274 275 276 277 278 279

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
280
  inductive constructions.
Raphael Cauderlier's avatar
Raphael Cauderlier committed
281 282
- 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
283
  already use rewriting for these tasks.
Raphael Cauderlier's avatar
Raphael Cauderlier committed
284 285 286 287 288 289 290 291 292 293 294 295 296 297 298
- 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
Raphael Cauderlier's avatar
Typos  
Raphael Cauderlier committed
299
attempting to prove =A=. It forms a monad whose return and bind
Raphael Cauderlier's avatar
Raphael Cauderlier committed
300 301 302 303 304 305 306 307 308 309 310 311 312 313 314 315 316 317 318 319 320 321 322 323 324 325 326 327 328 329 330 331 332 333 334 335 336 337 338 339 340 341 342 343 344 345 346 347 348 349 350 351 352 353 354 355 356 357 358 359 360 361
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

Raphael Cauderlier's avatar
Typos  
Raphael Cauderlier committed
362
=cert.certificate= is the Dedukti type of certificates. Contrary to
Raphael Cauderlier's avatar
Raphael Cauderlier committed
363 364 365 366 367 368 369 370 371 372 373 374 375 376 377 378 379 380 381 382 383 384 385 386 387 388 389 390 391 392 393 394 395 396 397 398 399 400 401 402 403
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:
Raphael Cauderlier's avatar
Raphael Cauderlier committed
404 405
- =cert.try : cert.certificate -> (tac.exc -> cert.certificate) -> cert.certificate=
- =cert.bind : A : fol.prop -> cert.certificate -> (fol.proof A -> cert.certificate) -> cert.certificate=
Raphael Cauderlier's avatar
Raphael Cauderlier committed
406 407 408 409 410 411 412 413 414 415 416 417 418 419 420
- =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:
Raphael Cauderlier's avatar
Raphael Cauderlier committed
421 422
- =cert.with_goal : (fol.prop -> cert.certificate) -> cert.certificate=
- =cert.with_context : (cert.context -> cert.certificate) -> cert.certificate=
Raphael Cauderlier's avatar
Raphael Cauderlier committed
423 424 425 426 427 428 429 430 431 432 433
- =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=:
Raphael Cauderlier's avatar
Raphael Cauderlier committed
434
- =cert.repeat : (cert.certificate -> cert.certificate) -> cert.certificate=
Raphael Cauderlier's avatar
Raphael Cauderlier committed
435

Raphael Cauderlier's avatar
Raphael Cauderlier committed
436
The certificate =cert.repeat f= is equivalent to the certificate =f (cert.repeat f)=.
Raphael Cauderlier's avatar
Raphael Cauderlier committed
437 438 439 440 441 442 443 444

** 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:
Raphael Cauderlier's avatar
Raphael Cauderlier committed
445 446
- =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=
Raphael Cauderlier's avatar
Raphael Cauderlier committed
447 448 449 450 451 452 453 454 455 456 457 458 459 460 461 462 463 464 465 466 467 468 469 470 471 472 473 474 475 476 477 478 479 480 481 482 483 484 485 486 487 488 489 490 491 492 493 494 495

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=
Raphael Cauderlier's avatar
Raphael Cauderlier committed
496 497 498 499 500 501
- =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=
Raphael Cauderlier's avatar
Raphael Cauderlier committed
502 503 504 505 506 507 508 509

** 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:
Raphael Cauderlier's avatar
Raphael Cauderlier committed
510 511
- =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=
Raphael Cauderlier's avatar
Raphael Cauderlier committed
512 513 514 515 516 517 518 519 520 521 522 523 524 525 526 527 528 529 530 531 532 533 534 535 536 537 538 539 540 541 542 543 544 545 546 547 548

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

Raphael Cauderlier's avatar
Typos  
Raphael Cauderlier committed
549 550
The following certificates are used to reason on the current goal,
each proves the current goal if it has a particular shape:
Raphael Cauderlier's avatar
Raphael Cauderlier committed
551 552 553 554 555 556 557 558 559 560 561 562 563 564 565 566 567
- =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=
Raphael Cauderlier's avatar
Raphael Cauderlier committed
568 569 570 571 572
- =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=
Raphael Cauderlier's avatar
Raphael Cauderlier committed
573 574 575 576 577 578 579 580 581 582 583 584 585 586 587 588 589 590 591 592 593

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:
Raphael Cauderlier's avatar
Raphael Cauderlier committed
594
- =eqcert.match_equality : fol.prop -> (A : fol.type -> fol.term A -> fol.term A -> cert.certificate) -> cert.certificate -> cert.certificate=
Raphael Cauderlier's avatar
Raphael Cauderlier committed
595 596 597
- =eqcert.reflexivity : cert.certificate=
- =eqcert.symmetry : cert.certificate -> cert.certificate=
- =eqcert.transitivity : A : fol.type -> fol.term A -> cert.certificate -> cert.certificate -> cert.certificate=
Raphael Cauderlier's avatar
Raphael Cauderlier committed
598 599 600
- =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=
Raphael Cauderlier's avatar
Raphael Cauderlier committed
601 602 603 604 605 606 607 608 609 610 611 612 613 614 615 616 617 618 619 620 621 622 623 624 625 626

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