manual.org 30.4 KB
 Raphael Cauderlier committed Mar 07, 2017 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 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 Mar 07, 2017 21 ``````Dktactics is a tactic and certificate language for multi-sorted `````` Raphael Cauderlier committed Mar 07, 2017 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 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 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 committed Mar 07, 2017 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 committed Mar 07, 2017 53 54 ``````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 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 committed Mar 07, 2017 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 committed Mar 07, 2017 68 ``````to declare the various types she needs. `````` Raphael Cauderlier committed Mar 07, 2017 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 committed Mar 07, 2017 78 ``````- =fol.read_types n A1 … An= is defined as =fol.cons_type A1 (… (fol.cons_type An fol.nil_type)…)= `````` Raphael Cauderlier committed Mar 07, 2017 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 committed Mar 07, 2017 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 committed Mar 07, 2017 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 committed Mar 07, 2017 112 ``````- =fol.apply_fun : f : fol.function -> fol.terms (fol.fun_arity f) -> fol.term (fol.fun_codomain f)= `````` Raphael Cauderlier committed Mar 07, 2017 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 committed Dec 01, 2017 133 ``````type =fol.predicate=. An artity is associated to each predicate `````` Raphael Cauderlier committed Mar 07, 2017 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 committed Mar 07, 2017 139 ``````- =fol.apply_pred : p : fol.predicate -> fol.terms (fol.pred_arity p) -> fol.prop= `````` Raphael Cauderlier committed Mar 07, 2017 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 committed Mar 07, 2017 155 ``````all other connectives are binary. `````` Raphael Cauderlier committed Mar 07, 2017 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 committed Mar 07, 2017 172 ``````and =fol.ex=. They have the same Dedukti type: =A : fol.type -> (fol.term A -> fol.prop) -> fol.prop=. `````` Raphael Cauderlier committed Mar 07, 2017 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 committed Mar 07, 2017 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 committed Mar 07, 2017 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 committed Dec 01, 2017 223 ``````[[./fol/eq.dk][fol/eq.dk]]. Equality is a family of predicate symbols parameterized by `````` Raphael Cauderlier committed Mar 07, 2017 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 committed Mar 07, 2017 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 committed Mar 07, 2017 242 ``````- Equality is a congruence with respect to all function symbols: `````` Raphael Cauderlier committed Mar 07, 2017 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 committed Mar 07, 2017 245 ``````- Equality is a congruence with respect to all predicate symbols: `````` Raphael Cauderlier committed Mar 07, 2017 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 committed Mar 07, 2017 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 committed Dec 01, 2017 254 `````` and terminating. `````` Raphael Cauderlier committed Mar 07, 2017 255 ``````- Subject-reduction: Typing is preserved by reduction according to `````` Raphael Cauderlier committed Dec 01, 2017 256 `````` this rewrite-system. `````` Raphael Cauderlier committed Mar 07, 2017 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 committed Dec 01, 2017 261 `````` obtained by encoding an inconsistent first-order theory. `````` Raphael Cauderlier committed Mar 07, 2017 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 committed Dec 01, 2017 280 `````` inductive constructions. `````` Raphael Cauderlier committed Mar 07, 2017 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 committed Dec 01, 2017 283 `````` already use rewriting for these tasks. `````` Raphael Cauderlier committed Mar 07, 2017 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 committed Dec 01, 2017 299 ``````attempting to prove =A=. It forms a monad whose return and bind `````` Raphael Cauderlier committed Mar 07, 2017 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 committed Dec 01, 2017 362 ``````=cert.certificate= is the Dedukti type of certificates. Contrary to `````` Raphael Cauderlier committed Mar 07, 2017 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 committed Mar 07, 2017 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 committed Mar 07, 2017 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 committed Mar 07, 2017 421 422 ``````- =cert.with_goal : (fol.prop -> cert.certificate) -> cert.certificate= - =cert.with_context : (cert.context -> cert.certificate) -> cert.certificate= `````` Raphael Cauderlier committed Mar 07, 2017 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 committed Mar 07, 2017 434 ``````- =cert.repeat : (cert.certificate -> cert.certificate) -> cert.certificate= `````` Raphael Cauderlier committed Mar 07, 2017 435 `````` `````` Raphael Cauderlier committed Mar 07, 2017 436 ``````The certificate =cert.repeat f= is equivalent to the certificate =f (cert.repeat f)=. `````` Raphael Cauderlier committed Mar 07, 2017 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 committed Mar 07, 2017 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 committed Mar 07, 2017 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 committed Mar 07, 2017 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 committed Mar 07, 2017 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 committed Mar 07, 2017 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 committed Mar 07, 2017 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 committed Dec 01, 2017 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 committed Mar 07, 2017 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 committed Mar 07, 2017 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 committed Mar 07, 2017 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 committed Mar 07, 2017 594 ``````- =eqcert.match_equality : fol.prop -> (A : fol.type -> fol.term A -> fol.term A -> cert.certificate) -> cert.certificate -> cert.certificate= `````` Raphael Cauderlier committed Mar 07, 2017 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 committed Mar 07, 2017 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 committed Mar 07, 2017 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 ``````