diff --git a/manual.org b/manual.org index 5b0f39f483a08166a777d707a29e3a45449008cc..80e4a2d75a7549f4796fe3348fd28694ce4944c5 100644 --- a/manual.org +++ b/manual.org @@ -130,7 +130,7 @@ by logical connectives and quantifiers. An atom is a predicate symbol applied to terms respecting the arity of the predicate symbol. Predicate symbols and their arities are defined similarly to function symbols. A predicate symbol is a Dedukti term of -type =fol.predicate=. An artity is is associated to each predicate +type =fol.predicate=. An artity is associated to each predicate symbol by the function - =fol.pred_arity : fol.predicate -> fol.types= @@ -220,7 +220,7 @@ definable so Deduction Modulo first-order theories can be defined. ** Equality We treat equality as a first-order theory defined in the file -[[./fol/eq.dl][fol/eq.dk]]. Equality is a family of predicate symbols parameterized by +[[./fol/eq.dk][fol/eq.dk]]. Equality is a family of predicate symbols parameterized by a sort: - =eq.Eq : fol.type -> fol.predicate= @@ -251,14 +251,14 @@ facts: The Dedukti theory presented in [[* Multi-sorted first-order logic in Dedukti][the previous section]] is sound in the following sense: - Convergence: The rewrite system that defines it is both confluent - and terminating + and terminating. - Subject-reduction: Typing is preserved by reduction according to - this rewrite-system + this rewrite-system. - Decidability of type-checking: The type-checking problem for terms in this Dedukti theory is decidable and the Dedukti type checker is a decision procedure for it. - Consistency: a closed term of type =fol.proof fol.false= can only be - obtained by encoding an inconsistent first-order theory + obtained by encoding an inconsistent first-order theory. Thanks to these good properties, a term of type =fol.proof A= can be considered as a proof witnessing the truth of the proposition =A=. We @@ -277,10 +277,10 @@ The first bad system is a dependently-typed tactic language. It is very similar to the typed tactic languages of Lean and [[http://plv.mpi-sws.org/mtac/][Mtac]] but it is simpler for the following reasons: - It deals with first-order logic instead of the full calculus of - inductive constructions + inductive constructions. - In Dedukti it is not necessary to encode pattern matching and recursion directly in the tactic language because the user can - already use rewriting for these tasks + already use rewriting for these tasks. - We have chosen to keep a shallow encoding of terms and formulae so some features such as testing whether a term is a variable are omitted. @@ -296,7 +296,7 @@ to handle failure and backtracking. - =tac.bind : A : fol.prop -> B : fol.prop -> tac.tactic A -> (fol.proof A -> tac.tactic B) -> tac.tactic B= If =A= is a formula, =tac.tactic A= is the Dedukti type of the tactics -attempting to prove =A=. It forms a monad whise return and bind +attempting to prove =A=. It forms a monad whose return and bind operations are =tac.ret= and =tac.bind= respectively. When a tactic successfully proves a formula, we can extract a proof of the formula using the partial function =tac.run=: @@ -359,7 +359,7 @@ The certificate language is described in file [[./meta/cert.dk][meta/cert.dk]]. ** Contexts and certificate evaluation -=certificate= is the Dedukti type of certificates. Contrary to +=cert.certificate= is the Dedukti type of certificates. Contrary to tactics, the type of a certificate does not indicate which formula it is supposed to prove and the same certificate can in fact prove several formulae. @@ -546,8 +546,8 @@ The certificate =cert.apply A B a c= proves =B a= if =c= proves *** Reasoning on the goal -The following certificates each prove the current goal if it has a -particular shape: +The following certificates are used to reason on the current goal, +each proves the current goal if it has a particular shape: - =cert.trivial : cert.certificate= - =cert.split : cert.certificate -> cert.certificate -> cert.certificate= - =cert.left : cert.certificate -> cert.certificate= diff --git a/meta/tac.dk b/meta/tac.dk index aee1e0109f22a19f4748bebc158a502150b2f7dc..d52881d1364c7549e98ec0861bdd0822fa80b68f 100644 --- a/meta/tac.dk +++ b/meta/tac.dk @@ -7,7 +7,7 @@ (setq-local dedukti-compile-options '("-nc" "-e" "-nl" "-I" "../fol")) ;) -(; This is a Meta Dedukti port Mtac with the following simpifications: +(; This is a Meta Dedukti port of Mtac with the following simpifications: - works on first-order logic instead of CIC This implies a bit of duplication between terms and proofs. - nu and abs are replaced by the less powerful but simpler to implement intro