manual.org 39.9 KB
 Raphael Cauderlier committed Mar 07, 2017 1 2 3 4 5 ``````#+Title: Dktactics User Manual * Introduction This is a user manual for Dktactics. Dktactics is a Meta Dedukti `````` Raphael Cauderlier committed Feb 02, 2018 6 7 ``````implementation of a typed tactic language and an untyped tactic language. `````` Raphael Cauderlier committed Mar 07, 2017 8 `````` `````` Raphael Cauderlier committed Feb 02, 2018 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 committed Mar 07, 2017 12 13 14 15 `````` * Installation Dktactics can be downloaded from `````` Raphael Cauderlier committed Mar 07, 2017 16 ``````[[https://gitlab.math.univ-paris-diderot.fr/cauderlier/dktactics]]. Dependencies `````` Raphael Cauderlier committed Mar 07, 2017 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 committed Feb 02, 2018 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 committed Mar 07, 2017 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 committed Mar 07, 2017 30 ``````well studied so our choice of basing Dktactics on first-order logic `````` Raphael Cauderlier committed Mar 07, 2017 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 committed Mar 07, 2017 42 ``````about [[* Resolution][resolution]]. `````` Raphael Cauderlier committed Mar 07, 2017 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 committed Feb 02, 2018 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 committed Mar 07, 2017 49 `````` `````` Raphael Cauderlier committed Mar 07, 2017 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 committed Mar 07, 2017 52 53 ``````setting. Second, multi-sorted logic ease the combination of theories. Merging for example a theory of booleans containing the `````` Raphael Cauderlier committed Mar 07, 2017 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 committed Mar 07, 2017 56 57 58 59 `````` ** Syntax The syntax of multi-sorted first-order logic is composed of four `````` Raphael Cauderlier committed Feb 02, 2018 60 `````` syntactic categories: sorts, terms, formulae, and proofs. `````` Raphael Cauderlier committed Mar 07, 2017 61 `````` `````` Raphael Cauderlier committed Feb 02, 2018 62 ``````*** Sorts `````` Raphael Cauderlier committed Mar 07, 2017 63 `````` `````` Raphael Cauderlier committed Feb 02, 2018 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 committed Mar 07, 2017 68 `````` `````` Raphael Cauderlier committed Feb 02, 2018 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 committed Mar 07, 2017 74 75 `````` For convenience, the file [[./fol/fol.dk][fol/fol.dk]] also defines an n-ary function `````` Raphael Cauderlier committed Feb 02, 2018 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 committed Mar 07, 2017 78 `````` `````` Raphael Cauderlier committed Feb 02, 2018 79 ``````The first parameter =n= of =fol.read_sorts= is a natural number of `````` Raphael Cauderlier committed Mar 07, 2017 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 committed Feb 02, 2018 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 committed Mar 07, 2017 94 95 96 `````` A function symbol is a Dedukti term of type =fol.function=. `````` Raphael Cauderlier committed Feb 02, 2018 97 ``````A domain and a codomain are respectively associated to each function `````` Raphael Cauderlier committed Mar 07, 2017 98 ``````symbol by the functions `````` Raphael Cauderlier committed Feb 02, 2018 99 ``````- =fol.fun_domain : fol.function -> fol.sorts= and `````` Raphael Cauderlier committed Feb 02, 2018 100 ``````- =fol.fun_codomain : fol.function -> fol.sort= `````` Raphael Cauderlier committed Mar 07, 2017 101 `````` `````` Raphael Cauderlier committed Feb 02, 2018 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 committed Mar 07, 2017 105 `````` of terms `````` Raphael Cauderlier committed Feb 02, 2018 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 committed Mar 07, 2017 107 108 `````` The only constructor of =fol.term A= is application of a function `````` Raphael Cauderlier committed Feb 02, 2018 109 ``````symbol =f= whose codomain is =A= to a list of terms whose sorts match `````` Raphael Cauderlier committed Feb 02, 2018 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 committed Mar 07, 2017 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 committed Feb 02, 2018 115 ``````- if =f= is a function symbol of domain =fol.read_sorts n A1 … An= and `````` Raphael Cauderlier committed Feb 02, 2018 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 committed Mar 07, 2017 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 committed Feb 02, 2018 129 ``````An atom is a predicate symbol applied to terms respecting the domain of `````` Raphael Cauderlier committed Mar 07, 2017 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 committed Dec 01, 2017 132 ``````type =fol.predicate=. An artity is associated to each predicate `````` Raphael Cauderlier committed Mar 07, 2017 133 ``````symbol by the function `````` Raphael Cauderlier committed Feb 02, 2018 134 ``````- =fol.pred_domain : fol.predicate -> fol.sorts= `````` Raphael Cauderlier committed Mar 07, 2017 135 `````` `````` Raphael Cauderlier committed Feb 02, 2018 136 ``````Applying a predicate symbol on a list of terms respecting its domain `````` Raphael Cauderlier committed Mar 07, 2017 137 ``````produces a formula: `````` Raphael Cauderlier committed Feb 02, 2018 138 ``````- =fol.apply_pred : p : fol.predicate -> fol.terms (fol.pred_domain p) -> fol.prop= `````` Raphael Cauderlier committed Mar 07, 2017 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 committed Feb 02, 2018 142 ``````- if =p= is a predicate symbol of domain =fol.read_sorts n A1 … An= and `````` Raphael Cauderlier committed Feb 02, 2018 143 `````` if =a1=, …, =an= are =n= terms of sort =A1=, …, =An= respectively, `````` Raphael Cauderlier committed Mar 07, 2017 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 committed Mar 07, 2017 154 ``````all other connectives are binary. `````` Raphael Cauderlier committed Mar 07, 2017 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 committed Feb 02, 2018 166 ``````binds a single variable of a given sort. As we promised in [[* Terms][the section `````` Raphael Cauderlier committed Mar 07, 2017 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 committed Feb 02, 2018 171 ``````and =fol.ex=. They have the same Dedukti type: =A : fol.sort -> (fol.term A -> fol.prop) -> fol.prop=. `````` Raphael Cauderlier committed Mar 07, 2017 172 `````` `````` Raphael Cauderlier committed Dec 14, 2017 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 committed Feb 02, 2018 178 ``````sorts: `````` Raphael Cauderlier committed Dec 14, 2017 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 committed Feb 02, 2018 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 committed Dec 14, 2017 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ₙ)…))= `````` Raphael Cauderlier committed Dec 13, 2017 193 `````` `````` Raphael Cauderlier committed Mar 07, 2017 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 committed Feb 02, 2018 202 ``````corresponding tactics presented in [[* Reasoning][the reasoning section]]): `````` Raphael Cauderlier committed Mar 07, 2017 203 204 ``````- =fol.false_elim : A : fol.prop -> fol.proof fol.false -> fol.proof A= - =fol.true_intro : fol.proof fol.true= `````` Raphael Cauderlier committed Mar 07, 2017 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 committed Feb 02, 2018 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 committed Mar 07, 2017 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 committed Feb 02, 2018 222 ``````=fol.sort=, =fol.predicate=, and =fol.function= respectively. We then `````` Raphael Cauderlier committed Feb 02, 2018 223 ``````define the domain of each function and predicate symbol and the `````` Raphael Cauderlier committed Mar 07, 2017 224 ``````codomain sort of each function symbol by extending the definitions of `````` Raphael Cauderlier committed Feb 02, 2018 225 ``````=fol.pred_domain=, =fol.fun_domain=, and =fol.fun_codomain= respectively. `````` Raphael Cauderlier committed Mar 07, 2017 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 committed Dec 01, 2017 242 ``````[[./fol/eq.dk][fol/eq.dk]]. Equality is a family of predicate symbols parameterized by `````` Raphael Cauderlier committed Mar 07, 2017 243 ``````a sort: `````` Raphael Cauderlier committed Feb 02, 2018 244 ``````- =eq.Eq : fol.sort -> fol.predicate= `````` Raphael Cauderlier committed Mar 07, 2017 245 `````` `````` Raphael Cauderlier committed Feb 02, 2018 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 committed Mar 07, 2017 247 `````` `````` Raphael Cauderlier committed Feb 02, 2018 248 ``````The shortcut notation =eq.eq A a b= where =A= has type =fol.sort= and `````` Raphael Cauderlier committed Mar 07, 2017 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 committed Mar 07, 2017 255 ``````- Equality is reflexive: `````` Raphael Cauderlier committed Feb 02, 2018 256 `````` =eq.eq_refl : A : fol.sort -> fol.proof (fol.all A (x => eq.eq A x x))= `````` Raphael Cauderlier committed Mar 07, 2017 257 ``````- Equality is symmetric: `````` Raphael Cauderlier committed Feb 02, 2018 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 committed Mar 07, 2017 259 ``````- Equality is transitive: `````` Raphael Cauderlier committed Feb 02, 2018 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 committed Mar 07, 2017 261 ``````- Equality is a congruence with respect to all function symbols: `````` Raphael Cauderlier committed Mar 07, 2017 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 committed Feb 02, 2018 263 `````` where =f= has domain =fol.read_sorts n A1 … An= and codomain =B=. `````` Raphael Cauderlier committed Mar 07, 2017 264 ``````- Equality is a congruence with respect to all predicate symbols: `````` Raphael Cauderlier committed Mar 07, 2017 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 committed Feb 02, 2018 266 `````` where =p= has domain =fol.read_yypes n A1 … An= `````` Raphael Cauderlier committed Mar 07, 2017 267 `````` `````` Raphael Cauderlier committed Feb 02, 2018 268 ``````* The typed tactic language `````` Raphael Cauderlier committed Mar 07, 2017 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 committed Dec 01, 2017 273 `````` and terminating. `````` Raphael Cauderlier committed Mar 07, 2017 274 ``````- Subject-reduction: Typing is preserved by reduction according to `````` Raphael Cauderlier committed Dec 01, 2017 275 `````` this rewrite-system. `````` Raphael Cauderlier committed Mar 07, 2017 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 committed Dec 01, 2017 280 `````` obtained by encoding an inconsistent first-order theory. `````` Raphael Cauderlier committed Mar 07, 2017 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 committed Dec 01, 2017 299 `````` inductive constructions. `````` Raphael Cauderlier committed Mar 07, 2017 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 committed Dec 01, 2017 302 `````` already use rewriting for these tasks. `````` Raphael Cauderlier committed Mar 07, 2017 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 committed Feb 02, 2018 310 ``````inside a monad defined in the file [[./meta/tac.dk][meta/mtac.dk]] whose main purpose is `````` Raphael Cauderlier committed Mar 07, 2017 311 312 ``````to handle failure and backtracking. `````` Raphael Cauderlier committed Feb 02, 2018 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 committed Mar 07, 2017 316 `````` `````` Raphael Cauderlier committed Feb 02, 2018 317 ``````If =A= is a formula, =mtac.mtactic A= is the Dedukti type of the tactics `````` Raphael Cauderlier committed Dec 01, 2017 318 ``````attempting to prove =A=. It forms a monad whose return and bind `````` Raphael Cauderlier committed Feb 02, 2018 319 ``````operations are =mtac.mret= and =mtac.mbind= respectively. `````` Raphael Cauderlier committed Mar 07, 2017 320 `````` `````` Raphael Cauderlier committed Feb 02, 2018 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 committed Mar 07, 2017 323 324 `````` It is defined by the following rewrite rule: `````` Raphael Cauderlier committed Feb 02, 2018 325 ``````- =[a] mtac.mrun _ (mtac.mret _ a) --> a= `````` Raphael Cauderlier committed Mar 07, 2017 326 327 328 `````` ** Exceptions and backtracking `````` Raphael Cauderlier committed Feb 02, 2018 329 ``````Exceptions form an open inductive type =mtac.exc=. `````` Raphael Cauderlier committed Mar 07, 2017 330 ``````A tactic can fail to prove its goal by raising an exception: `````` Raphael Cauderlier committed Feb 02, 2018 331 ``````- =mtac.mraise : A : fol.prop -> mtac.exc -> mtac.mtactic A= `````` Raphael Cauderlier committed Mar 07, 2017 332 `````` `````` Raphael Cauderlier committed Feb 02, 2018 333 ``````Exceptions can be caught by the =mtac.mtry= tactic combinator `````` Raphael Cauderlier committed Mar 07, 2017 334 ``````implementing backtracking: `````` Raphael Cauderlier committed Feb 02, 2018 335 ``````- =mtac.mtry : A : fol.prop -> mtac.mtactic A -> (mtac.exc -> mtac.mtactic A) -> tactic A= `````` Raphael Cauderlier committed Mar 07, 2017 336 `````` `````` Raphael Cauderlier committed Feb 02, 2018 337 ``````The tactic =mtac.mtry A t f= first tries the tactic =t=, if it succeeds `````` Raphael Cauderlier committed Mar 07, 2017 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 committed Feb 02, 2018 345 ``````context, we use non-linear higher-order rewriting to define the symbols =mtac.mintro_term= and =mtac.mintro_proof=: `````` Raphael Cauderlier committed Mar 07, 2017 346 ``````#+BEGIN_SRC dedukti `````` Raphael Cauderlier committed Feb 02, 2018 347 `````` def intro_term : A : fol.sort -> `````` Raphael Cauderlier committed Mar 07, 2017 348 `````` B : (fol.term A -> fol.prop) -> `````` Raphael Cauderlier committed Feb 02, 2018 349 350 `````` (x : fol.term A -> mtac.mtactic (B x)) -> mtac.mtactic (fol.all A B). `````` Raphael Cauderlier committed Mar 07, 2017 351 352 `````` def intro_proof : A : fol.prop -> B : fol.prop -> `````` Raphael Cauderlier committed Feb 02, 2018 353 354 `````` (fol.proof A -> mtac.mtactic B) -> mtac.mtactic (fol.imp A B). `````` Raphael Cauderlier committed Mar 07, 2017 355 `````` `````` Raphael Cauderlier committed Feb 02, 2018 356 `````` [A,B,b] mtac.mintro_term A B (x => mtac.mret (B x) (b x)) `````` Raphael Cauderlier committed Mar 07, 2017 357 `````` --> `````` Raphael Cauderlier committed Feb 02, 2018 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 committed Mar 07, 2017 360 `````` --> `````` Raphael Cauderlier committed Feb 02, 2018 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 committed Mar 07, 2017 363 `````` --> `````` Raphael Cauderlier committed Feb 02, 2018 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 committed Mar 07, 2017 366 `````` --> `````` Raphael Cauderlier committed Feb 02, 2018 367 `````` mtac.mraise (fol.imp A B) e. `````` Raphael Cauderlier committed Mar 07, 2017 368 369 ``````#+END_SRC `````` Raphael Cauderlier committed Feb 02, 2018 370 ``````* The untyped tactic language `````` Raphael Cauderlier committed Mar 07, 2017 371 `````` `````` Raphael Cauderlier committed Feb 02, 2018 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 committed Mar 07, 2017 376 `````` `````` Raphael Cauderlier committed Feb 02, 2018 377 ``````The untyped tactic language is defined in file [[./meta/tactic.dk][meta/tactic.dk]]. `````` Raphael Cauderlier committed Mar 07, 2017 378 `````` `````` Raphael Cauderlier committed Feb 02, 2018 379 ``````** Contexts and tactic evaluation `````` Raphael Cauderlier committed Mar 07, 2017 380 `````` `````` Raphael Cauderlier committed Feb 02, 2018 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 committed Mar 07, 2017 385 `````` `````` Raphael Cauderlier committed Feb 02, 2018 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 committed Mar 07, 2017 388 `````` `````` Raphael Cauderlier committed Feb 02, 2018 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 committed Mar 07, 2017 393 `````` `````` Raphael Cauderlier committed Feb 02, 2018 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= `````` Raphael Cauderlier committed Feb 02, 2018 399 ``````- =tactic.eval_tactic : tactic.context -> A : fol.prop -> tactic.tactic -> mtac.mtactic A= `````` Raphael Cauderlier committed Feb 02, 2018 400 ``````- =tactic.prove : A : fol.prop -> tactic.tactic -> fol.proof A= `````` Raphael Cauderlier committed Mar 07, 2017 401 `````` `````` Raphael Cauderlier committed Feb 02, 2018 402 ``````** Tactic primitives `````` Raphael Cauderlier committed Mar 07, 2017 403 `````` `````` Raphael Cauderlier committed Feb 02, 2018 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 committed Mar 07, 2017 409 `````` `````` Raphael Cauderlier committed Feb 02, 2018 410 411 ``````The simplest primitives reflect the two constructors =mtac.mret= and =mtac.mraise= of the tactic monad: `````` Raphael Cauderlier committed Mar 07, 2017 412 `````` `````` Raphael Cauderlier committed Feb 02, 2018 413 414 ``````- =tactic.exact : A : fol.prop -> fol.proof A -> tactic.tactic= - =tactic.raise : mtac.exc -> tactic.tactic= `````` Raphael Cauderlier committed Mar 07, 2017 415 `````` `````` Raphael Cauderlier committed Feb 02, 2018 416 ``````The =tactic.exact A a= tactic succeeds if and only if its goal is `````` Raphael Cauderlier committed Feb 02, 2018 417 ``````=A= in which case =mtac.mret A a= is returned. Otherwise the exception `````` Raphael Cauderlier committed Feb 02, 2018 418 ``````=tactic.exact_mismatch= is raised. `````` Raphael Cauderlier committed Mar 07, 2017 419 `````` `````` Raphael Cauderlier committed Feb 02, 2018 420 ``````The =tactic.raise e= tactic always raises the exception =e=. `````` Raphael Cauderlier committed Mar 07, 2017 421 `````` `````` Raphael Cauderlier committed Feb 02, 2018 422 423 ``````The other operations of the monad, =mtac.mtry=, =mtac.mbind=, =mtac.mintro_term= and =mtac.mintro_proof= are also reflected: `````` Raphael Cauderlier committed Feb 02, 2018 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 committed Mar 07, 2017 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 committed Feb 02, 2018 436 437 ``````sort =A=. On any other goal, the tactic =tactic.intro c= raises the exception =tactic.not_a_product=. `````` Raphael Cauderlier committed Mar 07, 2017 438 `````` `````` Raphael Cauderlier committed Feb 02, 2018 439 ``````Moreover, the file [[./meta/cert.dk][meta/tactic.dk]] defines tactic primitives for `````` Raphael Cauderlier committed Mar 07, 2017 440 ``````manipulating the proof state: `````` Raphael Cauderlier committed Feb 02, 2018 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 committed Mar 07, 2017 444 `````` `````` Raphael Cauderlier committed Feb 02, 2018 445 ``````The =tactic.with_goal f= tactic successfully proves the goal =A= in `````` Raphael Cauderlier committed Mar 07, 2017 446 ``````context =G= if and only if =f A= does so. Similarly, `````` Raphael Cauderlier committed Feb 02, 2018 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 committed Mar 07, 2017 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 committed Feb 02, 2018 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 committed Mar 07, 2017 455 `````` `````` Raphael Cauderlier committed Feb 02, 2018 456 ``````The tactic =tactic.repeat f= is equivalent to the tactic =f (tactic.repeat f)=. `````` Raphael Cauderlier committed Mar 07, 2017 457 458 459 460 `````` ** Trying assumptions or variables Instead of abstracting over the full context using `````` Raphael Cauderlier committed Feb 02, 2018 461 ``````=tactic.with_context=, it is often more convenient to try all `````` Raphael Cauderlier committed Mar 07, 2017 462 ``````assumptions or all variables in parallel. This behaviour is provided `````` Raphael Cauderlier committed Feb 02, 2018 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 committed Mar 07, 2017 466 `````` `````` Raphael Cauderlier committed Feb 02, 2018 467 ``````The =tactic.with_assumption f= tactic is successful if =f A a= is `````` Raphael Cauderlier committed Mar 07, 2017 468 ``````successful for any assumption =a : fol.proof A=. Otherwise, it raises `````` Raphael Cauderlier committed Feb 02, 2018 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 committed Mar 07, 2017 471 ``````variable =a : fol.term A=. Otherwise it raises the exception `````` Raphael Cauderlier committed Feb 02, 2018 472 ``````=tactic.no_successful_variable=. `````` Raphael Cauderlier committed Mar 07, 2017 473 474 `````` A particular case is looking for the current goal among the `````` Raphael Cauderlier committed Feb 02, 2018 475 476 ``````assumptions. This is provided by the =tactic.assumption= tactic: - =tactic.assumption : tactic.tactic= `````` Raphael Cauderlier committed Mar 07, 2017 477 478 479 `````` ** Pattern matching `````` Raphael Cauderlier committed Feb 02, 2018 480 ``````A lot of tactics perform different actions depending on the shape `````` Raphael Cauderlier committed Mar 07, 2017 481 ``````of the goal or of assumptions. We have seen an example with the `````` Raphael Cauderlier committed Feb 02, 2018 482 483 ``````=tactic.intro c= tactic in [[* Certificate primitives][the section about tactic primitives]]. In general, the tactic combinator =tactic.match_prop= `````` Raphael Cauderlier committed Mar 07, 2017 484 485 486 ``````can be used for this purpose: #+BEGIN_SRC dedukti `````` Raphael Cauderlier committed Feb 02, 2018 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 committed Mar 07, 2017 494 `````` (p : fol.predicate -> `````` Raphael Cauderlier committed Feb 02, 2018 495 `````` fol.terms (fol.pred_domain p) -> `````` Raphael Cauderlier committed Feb 02, 2018 496 497 `````` tactic.tactic) -> tactic.tactic `````` Raphael Cauderlier committed Mar 07, 2017 498 499 500 `````` #+END_SRC `````` Raphael Cauderlier committed Feb 02, 2018 501 ``````The tactic =tactic.match_prop C cfalse cand cor cimp call cex `````` Raphael Cauderlier committed Mar 07, 2017 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 committed Feb 02, 2018 512 ``````possible so [[./meta/cert.dk][meta/tactic.dk]] provides the following combinators matching `````` Raphael Cauderlier committed Mar 07, 2017 513 ``````on each of the cases: `````` Raphael Cauderlier committed Feb 02, 2018 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 committed Mar 07, 2017 521 `````` `````` Raphael Cauderlier committed Feb 02, 2018 522 ``````** Sort and formulae comparison `````` Raphael Cauderlier committed Mar 07, 2017 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 committed Feb 02, 2018 526 ``````sorts are identical and obtain coercion functions when they are. `````` Raphael Cauderlier committed Mar 07, 2017 527 528 `````` This behaviour is provided by the following combinators: `````` Raphael Cauderlier committed Feb 02, 2018 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 committed Mar 07, 2017 531 532 533 `````` ** Reasoning `````` Raphael Cauderlier committed Feb 02, 2018 534 ``````In this section, we list the tactic combinators that are used to `````` Raphael Cauderlier committed Mar 07, 2017 535 ``````perform reasoning steps. In fact we already met some of them, namely `````` Raphael Cauderlier committed Feb 02, 2018 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 committed Mar 07, 2017 538 539 540 541 542 ``````implications and universal quantifications. *** Applying a lemma The following combinators are used to apply a lemma: `````` Raphael Cauderlier committed Feb 02, 2018 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 committed Mar 07, 2017 548 `````` `````` Raphael Cauderlier committed Feb 02, 2018 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 committed Mar 07, 2017 551 `````` `````` Raphael Cauderlier committed Feb 02, 2018 552 ``````The tactic =tactic.refine2 A B C f c1 c2= is similar for a lemma `````` Raphael Cauderlier committed Mar 07, 2017 553 554 ``````with two assumptions =A= and =B= proved respectively by =c1= and =c2=. `````` Raphael Cauderlier committed Feb 02, 2018 555 ``````The tactic =tactic.refinen n A1 … An B f c1 … cn= is similar for a `````` Raphael Cauderlier committed Mar 07, 2017 556 557 558 ``````lemma with =n= assumptions =A1= … =An= proved respectively by =c1= … =cn=. `````` Raphael Cauderlier committed Feb 02, 2018 559 ``````The tactic =tactic.assert A c1 c2= proves the current goal =B= in `````` Raphael Cauderlier committed Mar 07, 2017 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 committed Feb 02, 2018 563 ``````The tactic =tactic.apply A B a c= proves =B a= if =c= proves `````` Raphael Cauderlier committed Mar 07, 2017 564 565 566 567 ``````=fol.all A B=. *** Reasoning on the goal `````` Raphael Cauderlier committed Feb 02, 2018 568 ``````The following tactics are used to reason on the current goal, `````` Raphael Cauderlier committed Dec 01, 2017 569 ``````each proves the current goal if it has a particular shape: `````` Raphael Cauderlier committed Feb 02, 2018 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 committed Mar 07, 2017 581 582 583 584 ``````A B= if =c= proves =B a=. *** Reasoning on the assumptions `````` Raphael Cauderlier committed Feb 02, 2018 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 committed Dec 01, 2017 596 ``````the context contains a pair of contradictory assumptions (an `````` Raphael Cauderlier committed Feb 02, 2018 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 committed Dec 01, 2017 599 ``````=G= if =c1= proves =fol.and A B= in context =G= and =c2= proves =C= in `````` Raphael Cauderlier committed Feb 02, 2018 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 committed Dec 01, 2017 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 committed Feb 02, 2018 604 ``````=G= with extra assumption =B=. The tactic =tactic.destruct_imp A B `````` Raphael Cauderlier committed Dec 01, 2017 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 committed Feb 02, 2018 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 committed Dec 01, 2017 609 ``````=G= if =c1= proves =fol.ex A B= and =c2= proves =C= in context =G= `````` Raphael Cauderlier committed Feb 02, 2018 610 ``````with an extra variable =x= of sort =A= and an extra assumption =B x=. `````` Raphael Cauderlier committed Mar 07, 2017 611 `````` `````` Raphael Cauderlier committed Feb 02, 2018 612 ``````** Equality Tactics `````` Raphael Cauderlier committed Mar 07, 2017 613 `````` `````` Raphael Cauderlier committed Feb 02, 2018 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 committed Feb 02, 2018 621 `````` (where the domain of =f= has length =n=) `````` Raphael Cauderlier committed Feb 02, 2018 622 ``````- =eqtac.rewrite : A : fol.sort -> fol.term A -> fol.term A -> tactic.tactic -> tactic.tactic= `````` Raphael Cauderlier committed Mar 07, 2017 623 `````` `````` Raphael Cauderlier committed Feb 02, 2018 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 committed Mar 07, 2017 629 ``````goals of the form =eq.eq A a c= if =c1= proves =eq.eq A a b= and =c2= `````` Raphael Cauderlier committed Feb 02, 2018 630 ``````proves =eq.eq A b c=. The tactic =eqtac.f_equal f c1 … cn= `````` Raphael Cauderlier committed Mar 07, 2017 631 ``````proves =eq.eq B (fol.fun_apply f a1 … an) (fol.fun_apply f a1' … an')= `````` Raphael Cauderlier committed Feb 02, 2018 632 ``````if each =ci= proves =eq.eq Ai ai ai'=. The tactic =eqtac.rewrite `````` Raphael Cauderlier committed Mar 07, 2017 633 ``````A a a' c1 c2= proves =B= if =c1= proves =eq.eq A a a'= and =c2= proves `````` Raphael Cauderlier committed Feb 02, 2018 634 ``````=B= in which each occurrence of =a= has been replaced by =a'= (see [[* Substitutions][the `````` Raphael Cauderlier committed Mar 07, 2017 635 636 ``````section on substitution]]). `````` Raphael Cauderlier committed Dec 01, 2017 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 committed Feb 02, 2018 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= `````` Raphael Cauderlier committed Dec 01, 2017 645 `````` `````` Raphael Cauderlier committed Feb 02, 2018 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= `````` Raphael Cauderlier committed Dec 01, 2017 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 committed Feb 02, 2018 652 653 ``````=classical_tactics.contradict= is used to prove by contradiction using double-negation elimination. =classical_tactics.contradict c= proves the `````` Raphael Cauderlier committed Dec 01, 2017 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 committed Feb 02, 2018 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)))= `````` Raphael Cauderlier committed Dec 01, 2017 661 662 `````` * Examples `````` Raphael Cauderlier committed Mar 07, 2017 663 ``````** Drinker paradox `````` Raphael Cauderlier committed Dec 01, 2017 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 committed Feb 02, 2018 682 ``````a classical reasoning by case (using the =classical_tactics.prop_case= `````` Raphael Cauderlier committed Dec 01, 2017 683 ``````combinator) and then uses the classical lemma `````` Raphael Cauderlier committed Feb 02, 2018 684 ``````=classical_tactics.not_all_is_ex_not= in the second branch. `````` Raphael Cauderlier committed Dec 01, 2017 685 686 `````` ** TODO Decision procedures `````` Raphael Cauderlier committed Mar 07, 2017 687 688 689 ``````*** Minimal logic *** Presburger arithmetic * TODO Interactive proof development `````` Raphael Cauderlier committed Jan 25, 2018 690 691 ``````* Checking output of automatic theorem provers ** TODO Reasoning modulo AC, ACU, symmetry `````` Raphael Cauderlier committed Mar 07, 2017 692 `````` `````` Raphael Cauderlier committed Dec 14, 2017 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 committed Feb 02, 2018 708 `````` having the same sort). `````` Raphael Cauderlier committed Dec 14, 2017 709 710 711 `````` - =unif.substition : Type= - =unif.empty_subst : unif.substitution= `````` Raphael Cauderlier committed Feb 02, 2018 712 `````` - =unif.cons_subst : A : fol.sort -> fol.term A -> fol.term A -> unif.substitution -> unif.substitution= `````` Raphael Cauderlier committed Dec 14, 2017 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 committed Feb 02, 2018 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= `````` Raphael Cauderlier committed Dec 14, 2017 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= `````` Raphael Cauderlier committed Jan 25, 2018 741 ``````*** Unification `````` Raphael Cauderlier committed Dec 14, 2017 742 743 `````` A (first-order) unification problem is a list of pairs of terms `````` Raphael Cauderlier committed Feb 02, 2018 744 `````` (both terms having the same sort). Unification can either fail or `````` Raphael Cauderlier committed Dec 14, 2017 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 committed Feb 02, 2018 750 `````` - =unif.unify_cons : A : fol.sort -> fol.term A -> fol.term A -> unif.unify_problem -> unif.unify_problem= `````` Raphael Cauderlier committed Dec 14, 2017 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 committed Mar 07, 2017 760 761 ``````** Resolution `````` Raphael Cauderlier committed Jan 25, 2018 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. `````` Raphael Cauderlier committed May 05, 2018 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 `````` Raphael Cauderlier committed Jan 25, 2018 770 771 772 `````` variables which are to be interpreted as universally quantified. A *quantified clause* is an explicitly universally quantified clause. `````` Raphael Cauderlier committed May 05, 2018 773 `````` The types for atoms, literals, clauses, and quantified clauses are `````` Raphael CAUDERLIER committed Jan 26, 2018 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 `````` Raphael Cauderlier committed Jan 25, 2018 776 777 778 `````` proposition using the partial function =resolution.qclause_of_prop=: `````` Raphael CAUDERLIER committed Jan 26, 2018 779 `````` - =resolution.qclause_of_prop : fol.prop -> clauses.qclause= `````` Raphael Cauderlier committed Jan 25, 2018 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ⱼ) `````` Raphael CAUDERLIER committed Jan 26, 2018 788 `````` ————————————————————————————————— Factorisation `````` Raphael Cauderlier committed Jan 25, 2018 789 790 791 `````` (l₁ ∨ … ∨ lⱼ₋₁ ∨ lⱼ₊₁ ∨ … ∨ lₙ)σ l₁ ∨ … ∨ lₙ l'₁ ∨ … ∨ l'ₘ σ = mgu(lᵢ, ¬l'ⱼ) `````` Raphael CAUDERLIER committed Jan 26, 2018 792 `````` ——————————————————————————————————————————————————————————————————————— Resolution `````` Raphael Cauderlier committed Jan 25, 2018 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]].``````