This repository contains experiments with different (automatic) binding techniques (ott + lngen, autosubst2) in proving simple properties (type safety) for some simple type systems (STLC, System F, Fsub).
README.v is a comprehensive entry file that lists all the mechanized properties.
*/autosubst2/language.sig contains the syntax definition for autosubst2, and */autosubst2/def_as2.v contains the generated Coq definitions.
*/lngen/language.ott contains the syntax definition for ott + lngen, and */lngen/def_ott.v contains the definitions the generated Coq definitions and */lngen/prop_ln.v contains the generated Coq properties.
(Recommended): use opam switch to create a new opam environment.
coq-8.19.2
opam pin add coq 8.19.2Metalib(tested on version dev)
opam repo add coq-extra-dev https://coq.inria.fr/opam/extra-dev
opam install coq-metalibCoqHammer(tested on version 1.3.2)
opam repo add coq-released https://coq.inria.fr/opam/released
opam install coq-hammer-tactics(The following dependencies are not required if you only want to check the proofs.)
ott(tested on version 0.34)
opam repo add coq-released https://coq.inria.fr/opam/released
opam install coq-ottlngen(tested on version 0.3.2)
Please follow the instruction in its repository.
autosubst-ocaml(tested on version 1.1)
opam repo add coq-core-dev https://coq.inria.fr/opam/core-dev
opam install coq-autosubst-ocamlThe Coq definitions generated by ott + lngen and autosubst2 are already provided in the repository. You can run the following commands to check the proofs without installing them:
- Run
make coq-onlyto check the proof.
If you would like to regenerate the definitions using language.ott and language.sig, you can run the following commands:
-
Run
make ottandmake lngento regenerate the Coq definitions usingott + lngen. -
Run
make autosubst2to regenerate the Coq definitions usingautosubst2.