Commit b5fb05c6 authored by Pierre Letouzey's avatar Pierre Letouzey
Browse files

Updated README and copyright notices

parent 65eabe25
(** * An simultaneous definition of substitution for named formulas *)
(** The NatDed development, Pierre Letouzey, 2019.
(** The NatDed development, Pierre Letouzey, 2019-2020.
This file is released under the CC0 License, see the LICENSE file *)
Require Import Defs NameProofs Nam Subst Equiv Toolbox.
......
(** * Ordering the Ascii datatype *)
(** The NatDed development, Pierre Letouzey, 2019.
(** The NatDed development, Pierre Letouzey, 2019-2020.
This file is released under the CC0 License, see the LICENSE file *)
Require Import Bool Ascii BinNat Orders OrdersEx.
......
(** * Explicit enumeration of countable types *)
(** The NatDed development, Pierre Letouzey, 2019.
(** The NatDed development, Pierre Letouzey, 2019-2020.
This file is released under the CC0 License, see the LICENSE file *)
Require Import Ascii NArith Defs Mix NameProofs Meta.
......
(** * Initial definitions for Natural Deduction *)
(** The NatDed development, Pierre Letouzey, 2019.
(** The NatDed development, Pierre Letouzey, 2019-2020.
This file is released under the CC0 License, see the LICENSE file *)
Require Export Setoid Morphisms RelationClasses Arith Omega Bool String
......
(** * Conversion between Named formulas and Locally Nameless formulas *)
(** The NatDed development, Pierre Letouzey, 2019.
(** The NatDed development, Pierre Letouzey, 2019-2020.
This file is released under the CC0 License, see the LICENSE file *)
Require Import Defs NameProofs Nam Subst Toolbox.
......
(** * Conversion from Named derivations to Locally Nameless derivations *)
(** The NatDed development, Pierre Letouzey, 2019.
(** The NatDed development, Pierre Letouzey, 2019-2020.
This file is released under the CC0 License, see the LICENSE file *)
Require Import RelationClasses Arith Omega.
......
(* A link with Lambda Calculus. *)
(** * A link with Lambda Calculus *)
(** The NatDed development, Pierre Letouzey, 2019.
(** The NatDed development, Pierre Letouzey, Samuel Ben Hamou, 2019-2020.
This file is released under the CC0 License, see the LICENSE file *)
Require Import Defs Mix List.
......@@ -103,4 +103,4 @@ Proof.
apply Type_Pi1 with (τ := Atom "B").
apply Type_Var.
intuition.
Qed.
\ No newline at end of file
Qed.
(** * Some meta-properties of the Mix encoding *)
(** The NatDed development, Pierre Letouzey, 2019.
(** The NatDed development, Pierre Letouzey, Samuel Ben Hamou, 2019-2020.
This file is released under the CC0 License, see the LICENSE file *)
Require Import Defs NameProofs Mix Toolbox.
......
(** * Natural deduction, with a Locally Nameless encoding *)
(** The NatDed development, Pierre Letouzey, 2019.
(** The NatDed development, Pierre Letouzey, 2019-2020.
This file is released under the CC0 License, see the LICENSE file *)
Require Import Defs.
......
(** * Models of theories *)
(** The NatDed development, Pierre Letouzey, 2019.
(** The NatDed development, Pierre Letouzey, 2019-2020.
This file is released under the CC0 License, see the LICENSE file *)
Require Import Eqdep_dec Defs Mix NameProofs Toolbox Meta ProofExamples.
......
(** * Natded : a toy implementation of Natural Deduction *)
(** The NatDed development, Pierre Letouzey, 2019.
(** The NatDed development, Pierre Letouzey, 2019-2020.
This file is released under the CC0 License, see the LICENSE file *)
Require Import Defs.
......
(** * Proofs about name sets *)
(** The NatDed development, Pierre Letouzey, 2019.
(** The NatDed development, Pierre Letouzey, 2019-2020.
This file is released under the CC0 License, see the LICENSE file *)
Require Import Ascii MSetFacts MSetProperties StringUtils Defs.
......
(** * N-ary functions *)
(** The NatDed development, Pierre Letouzey, 2019.
(** The NatDed development, Pierre Letouzey, 2019-2020.
This file is released under the CC0 License, see the LICENSE file *)
Require Export List NaryFunctions.
......
(** * The Theory of Peano Arithmetic and its Coq model *)
(** The NatDed development, Pierre Letouzey, 2019.
(** The NatDed development, Pierre Letouzey, Samuel Ben Hamou, 2019-2020.
This file is released under the CC0 License, see the LICENSE file *)
Require Import Defs NameProofs Mix Meta Toolbox.
......
(** * Pre-models of theories *)
(** The NatDed development, Pierre Letouzey, 2019.
(** The NatDed development, Pierre Letouzey, 2019-2020.
This file is released under the CC0 License, see the LICENSE file *)
Require Import Defs Mix NameProofs Toolbox Meta Restrict Theories.
......
(** * Some examples of proofs in the Mix encoding *)
(** The NatDed development, Pierre Letouzey, 2019.
(** The NatDed development, Pierre Letouzey, Samuel Ben Hamou, 2019-2020.
This file is released under the CC0 License, see the LICENSE file *)
Require Import Defs NameProofs Mix Toolbox Meta.
......
......@@ -2,17 +2,18 @@
NatDed : a Coq encoding of Natural Deduction
============================================
## Author
## Authors
Pierre Letouzey (IRIF), 2019
- Pierre Letouzey (IRIF), 2019-2020
- Samuel Ben Hamou (ENS Paris Saclay), internship June-July 2020
## Description
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. I 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.
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.
I have formalized Natural Deduction and some of its meta-theory (such as a subsitution lemma), including classical models (seen as Coq types + functions + propositions), and the completeness theorem (following the Henkin approach).
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).
Trying to be faithful to the original document, I first encode formulas 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 I switch to another encoding (locally nameless) which is immune to these issues, while avoiding most of the technicalities of the approach of De Bruijn indices. I provide a two-way conversion between these named and locally-nameless encodings, and prove it correct. The rest of the meta-theorical study is performed on the locally-nameless representation.
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.
## Summary
......@@ -23,12 +24,19 @@ Main files :
- [Mix](Mix.v) : same, but using a Locally Nameless representation of binders
- [Subst](Subst.v) : basic properties of renamings and substitutions for [Nam](Nam.v)
- [Equiv](Equiv.v), [Equiv2](Equiv2.v) : conversions between the [Nam](Nam.v) and [Mix](Mix.v) encodings
- [Meta](Meta.v) : some meta-theoretical results about [Mix](Mix.v) (e.g. substitution lemma)
- [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
- [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
- [Skolem](Skolem.v) : Skolem theorem stating that any skolem extension is conservative
- [Peano](Peano.v) : example theory (Peano Arithmetic) and its Coq model
- [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
Auxiliary files :
- [AsciiOrder](AsciiOrder.v) [StringOrder](StringOrder.v) [StringUtils](StringUtils.v) : ordering of chars and strings, plus a few things about strings
......@@ -36,11 +44,27 @@ Auxiliary files :
- [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)
- [AltSubst](AltSubst.v) : an earlier substitution and alpha-equivalence for [Nam](Nam.v) via structural simultaneous definitions.
- [Nary](Nary.v) : extension of Coq [NaryFunctions]
## Documentation
- A [talk in french](https://www.irif.fr/\_media/rencontres/pps2019/letouzey.pdf) presenting the state of this development in September 2019 (Journéees PPS).
- Soon, the internship report of Samuel Ben Hamon (summer 2020). In the meanwhile, see [Rapport](Rapport).
## Usage
To be used with Coq 8.8. Just run `make` to compile.
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).
## License
This work is released under the Creative Commons Zero License (CC0). See files [LICENSE](LICENSE) and [COPYING](COPYING) for more.
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).
(** * Restrict a proof or derivation to a signature and/or a level *)
(** The NatDed development, Pierre Letouzey, 2019-2020.
This file is released under the CC0 License, see the LICENSE file *)
Require Import Defs NameProofs Mix Wellformed.
Import ListNotations.
Local Open Scope bool_scope.
......
(** * First-order theories *)
(** The NatDed development, Pierre Letouzey, 2019.
(** The NatDed development, Pierre Letouzey, 2019-2020.
This file is released under the CC0 License, see the LICENSE file *)
Require Import ChoiceFacts.
......
(** * Ordering of the String datatype *)
(** The NatDed development, Pierre Letouzey, 2019.
(** The NatDed development, Pierre Letouzey, 2019-2020.
This file is released under the CC0 License, see the LICENSE file *)
Require Import Bool Orders Ascii AsciiOrder String.
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment