README.md 5.1 KB
Newer Older
 Pierre Letouzey committed May 10, 2019 1 2 3 4 `````` NatDed : a Coq encoding of Natural Deduction ============================================ `````` Pierre Letouzey committed Aug 05, 2020 5 ``````## Authors `````` Pierre Letouzey committed May 10, 2019 6 `````` `````` Pierre Letouzey committed Aug 05, 2020 7 8 `````` - Pierre Letouzey (IRIF), 2019-2020 - Samuel Ben Hamou (ENS Paris Saclay), internship June-July 2020 `````` Pierre Letouzey committed May 10, 2019 9 10 11 `````` ## Description `````` Pierre Letouzey committed Aug 05, 2020 12 ``````This Coq development is an attempt to formalize as directly as possible a typical logic course about 1st-order predicate calculus using the Natural Deduction style. We followed here a [logic course](http://www.irif.fr/~letouzey/preuves/cours.pdf) (in French) due to Alexandre Miquel. Showing parts of this Coq development to Master students (at least the definitions and proof statements and proof sketchs) is now an teaching alternative instead of using the original course pdf, or in complement of it. `````` Pierre Letouzey committed May 10, 2019 13 `````` `````` Pierre Letouzey committed Aug 05, 2020 14 ``````Natural Deduction and some of its meta-theory have been formalized (such as a subsitution lemma), including classical models (seen as Coq types + functions + propositions), and the completeness theorem (following the Henkin approach). `````` Pierre Letouzey committed May 10, 2019 15 `````` `````` Pierre Letouzey committed Aug 05, 2020 16 ``````Trying to be faithful to the original document, formulas are first encoded using names (i.e. strings) in quantifiers. As expected, this triggers difficulties (name capture) during substitutions, and leads to the use of alpha-equivalence. Then another encoding is proposed (locally nameless) which is immune to these issues, while avoiding most of the technicalities of the approach of De Bruijn indices. A two-way conversion between these named and locally-nameless encodings is provided and proved correct. The rest of the meta-theorical study is performed on the locally-nameless representation. `````` Pierre Letouzey committed May 10, 2019 17 18 19 20 21 `````` ## Summary Main files : `````` Pierre Letouzey committed May 10, 2019 22 23 24 `````` - [Defs](Defs.v) : common basic structures (names, variables, signatures, ...) - [Nam](Nam.v) : encoding of Natural Deduction (terms, formulas, derivations ...) using names as binders - [Mix](Mix.v) : same, but using a Locally Nameless representation of binders `````` Pierre Letouzey committed Jun 04, 2019 25 `````` - [Subst](Subst.v) : basic properties of renamings and substitutions for [Nam](Nam.v) `````` Pierre Letouzey committed May 10, 2019 26 `````` - [Equiv](Equiv.v), [Equiv2](Equiv2.v) : conversions between the [Nam](Nam.v) and [Mix](Mix.v) encodings `````` Pierre Letouzey committed Aug 05, 2020 27 28 29 30 31 `````` - [Toolbox](Toolbox.v) : basic properties of [Mix](Mix.v) utility functions like lift, bsubst, vmap, ... - [Meta](Meta.v) : some meta-theoretical results about [Mix](Mix.v), e.g. substitution lemma and some admissible rules - [ProofExamples](ProofExemples.v) : some usual 1st-order proofs via [Mix](Mix.v), both intuitionistic or classical - [Wellformed](Wellformed.v) : well-formed terms, formula, ... corrrectly use a signature and binders - [Restrict](Restrict.v) : restrict a proof or derivation to a signature and/or a binder level `````` Pierre Letouzey committed May 10, 2019 32 33 34 `````` - [Theories](Theories.v) : notion of 1st-order theory, consistency, extensions, Henkin theorem, completion, ... - [PreModels](PreModels.v) : interpretation of formulas as Coq propositions, validity theorem - [Models](Models.v) : notion of model, build of a syntactic model for a consistent theory, completeness theorem `````` Pierre Letouzey committed Aug 05, 2020 35 `````` - [Skolem](Skolem.v) : Skolem theorem stating that any skolem extension is conservative `````` Pierre Letouzey committed Aug 09, 2019 36 `````` - [Peano](Peano.v) : example theory (Peano Arithmetic) and its Coq model `````` Pierre Letouzey committed Aug 05, 2020 37 38 39 `````` - [ZF](ZF.v) : example theory (Zermelo-Fraenkel set theory) and its Coq model (based on Benjamin Werner [ZFC contribution](https://github.com/coq-contribs/zfc)) - [Lambda](Lambda.v) : relate propositional proofs in [Mix](Mix.v) with a (extended) lambda-calculus, Curry-Howard theorem `````` Pierre Letouzey committed May 10, 2019 40 41 ``````Auxiliary files : `````` Pierre Letouzey committed May 10, 2019 42 43 44 45 `````` - [AsciiOrder](AsciiOrder.v) [StringOrder](StringOrder.v) [StringUtils](StringUtils.v) : ordering of chars and strings, plus a few things about strings - [Utils](Utils.v) : a generic notion of boolean equalities, some utility functions and proofs about lists, ... - [NameProofs](NameProofs.v) : proofs about name set (i.e. sets of strings) - [Countable](Countable.v) : explicit enumeration of countable types (such as strings or terms or formulas) `````` Pierre Letouzey committed Jun 04, 2019 46 `````` - [AltSubst](AltSubst.v) : an earlier substitution and alpha-equivalence for [Nam](Nam.v) via structural simultaneous definitions. `````` Pierre Letouzey committed Aug 05, 2020 47 48 49 50 `````` - [Nary](Nary.v) : extension of Coq [NaryFunctions] ## Documentation `````` Pierre Letouzey committed Aug 05, 2020 51 52 `````` - A [talk](https://www.irif.fr/\_media/rencontres/pps2019/letouzey.pdf) presenting the state of this development in September 2019 (Journéees PPS). The [markdown file](talk/expose.md) of these slides `````` Pierre Letouzey committed Aug 05, 2020 53 54 `````` - Soon, the internship report of Samuel Ben Hamon (summer 2020). In the meanwhile, see [Rapport](Rapport). `````` Pierre Letouzey committed May 10, 2019 55 56 57 `````` ## Usage `````` Pierre Letouzey committed Aug 05, 2020 58 59 60 61 62 63 64 ``````To be used with Coq >= 8.8. Just run `make` to compile. ## External dependencies This work reuse a file from Benjamin Werner's ZFC contribution https://github.com/coq-contribs/zfc See also the [corresponding article](http://www.lix.polytechnique.fr/Labo/Benjamin.Werner/publis/tacs97.pdf). For now, we have chosen to embed here a copy of the only necessary file, see [contribs/zfc](contribs/zfc). `````` Pierre Letouzey committed May 10, 2019 65 66 67 `````` ## License `````` Pierre Letouzey committed Aug 05, 2020 68 69 70 71 ``````This work is released under the Creative Commons Zero License (CC0), except the file [contribs/zfc/zfc.v](contribs/zfc/zfc.v). See files [LICENSE](LICENSE) and [COPYING](COPYING) for more about the CC0 license. The file [contribs/zfc/zfc.v](contribs/zfc/zfc.v) is an excerpt of Benjamin Werner's [ZFC contribution](https://github.com/coq-contribs/zfc) released under the [LGPL >= 2.1 License](https://github.com/coq-contribs/zfc/blob/master/LICENSE).``````