A first-order logic proof mode in Coq

Update: We presented this work at the 2021 Coq Workshop. Here is the extended abstract and the latest version for Coq 8.13.

See the documentation for a users guide and a description of how the proof mode works.

Requirements

Simply run make.

Have a look at the demo files DemaPA.v and DemoZF.v where the proof mode is applied to Peano arithmetic and Zermelo-Fraenkel set theory.

Name		Name	Last commit message	Last commit date
Latest commit History 65 Commits
documentation		documentation
.gitignore		.gitignore
Deduction.v		Deduction.v
DemoPA.v		DemoPA.v
DemoZF.v		DemoZF.v
FOL.v		FOL.v
Hoas.v		Hoas.v
Ltac2StringIdent.v		Ltac2StringIdent.v
Makefile		Makefile
PA.v		PA.v
ProofMode.v		ProofMode.v
README.md		README.md
Tarski.v		Tarski.v
Theories.v		Theories.v
VectorTech.v		VectorTech.v
ZF.v		ZF.v
_CoqProject		_CoqProject