This project contains a simple formalisation of soundness and completeness of intuitionistic propositional logic (in the natural-deduction presentation) with respect to its algebraic semantics (i.e., Heyting algebras). The contents of the modules are as follows:
Syntaxcontains the syntax of IPL propositions and some notations;Deductioncontains the definition of natural deduction for IPL, and the proof of a weakening lemma;Heytingcontains an axiomatisation of Heyting algebras, as well as some derived facts; note that the algebra is defined as a pre-order, with elements ordered in both directions taken as equivalent;Interpdefines an interpretation of IPL propositions in a Heyting algebra;Soundnessproves the interpretation sound with respect to natural deduction;Completenesscontains the construction of the Lindenbaum algebra and the proof of completeness.
To compile the project, run make -f CoqMakefile. Tested with Coq v8.19.1.