README.md 3.02 KB
Newer Older
Pierre Letouzey's avatar
Pierre Letouzey committed
1 2 3 4 5 6 7 8 9 10

NatDed : a Coq encoding of Natural Deduction
============================================

## Author

Pierre Letouzey (IRIF), 2019

## Description

Pierre Letouzey's avatar
Pierre Letouzey committed
11
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.
Pierre Letouzey's avatar
Pierre Letouzey committed
12 13 14

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).

Pierre Letouzey's avatar
Pierre Letouzey committed
15
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.
Pierre Letouzey's avatar
Pierre Letouzey committed
16 17 18 19 20

## Summary

Main files :

Pierre Letouzey's avatar
Pierre Letouzey committed
21 22 23
 - [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
24
 - [Alpha](Alpha.v) : equivalence between various definitions of substitutions and alpha-equivalences for [Nam](Nam.v)
Pierre Letouzey's avatar
Pierre Letouzey committed
25 26 27 28 29
 - [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)
 - [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's avatar
Pierre Letouzey committed
30 31 32
 
Auxiliary files :

Pierre Letouzey's avatar
Pierre Letouzey committed
33 34 35 36
 - [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's avatar
Pierre Letouzey committed
37 38 39 40 41 42 43

## Usage

To be used with Coq 8.8. Just run `make` to compile.

## License

Pierre Letouzey's avatar
Pierre Letouzey committed
44
This work is released under the Creative Commons Zero License (CC0). See files [LICENSE](LICENSE) and [COPYING](COPYING) for more.