Lang-n-Prove: A Proof Language for Language Proofs

Author: Matteo Cimini (matteo_cimini@uml.edu)

Subtyping support: Seth Galasso (seth.galasso@gmail.com)

Instructions

Requirements:

• To compile and run: Ocaml with the Batteries and Menhir packages is required.
• To test the output of Lang-n-Prove: the Abella proof assistant is required.

You can install these dependencies in thier own Opam switch with this command:

opam switch import dependencies.txt --switch lnp && eval $(opam env)

Quick usage:

• make
• ./lnp

What it does:

• loads the following lnp proofs in the folder of the project:
  • canonical.lnp (to generate canonical form lemmas)
  • progress-op.lnp (to generate operator-specific progress theorems)
  • progress.lnp (to generate the progress theorem)
  • preservation.lnp (to generate the type preservation theorem)
• loads all the languages with extension .lan in the folder "repo"
• applies the lnp proofs to the languages, and generates the Abella proof assistant files in the folder "generated"

To test the results of ./lnp (i.e. to test the proofs that Lang-n-Prove has generated):

• ./testAll.sh
  This is a bash script. The command "abella" must be in the $PATH.
  The script runs the command "abella" on all the Abella proofs (.thm files) in the folder "generated".
  The script prints a success message, or points out the Abella proof files that failed.
• Alternatively, users can manually run Abella on the Abella proofs they are interested to check. Example: run command "abella generated/fpl_cbv.thm"

To clean:

• make clean
  (removes compilation files and executable)
  (removes Abella files in "generated")

Substitution Lemmas

We do not support substitution lemmas at the moment.
The Lang-n-Prove proof preservation.lnp generates "skip" where substitution lemmas should be applied.
That is, some .thm files have "skip." in proof of theorem Type-preservation.

To complete those proofs, replace the "skip." instruction in

• Mapp case with: Hyp1 : case Hyp1(keep). CutHyp : assert ({typeOf E2 T1}). ToCut : inst Hyp3 with n1 = E2. cut ToCut with CutHyp. clear CutHyp. clear ToCut. search.
• MappT case with: Hyp1 : case Hyp1(keep). inst Hyp2 with n1 = X. search.
• Mlet case with: CutHyp : assert ({typeOf E T1}). ToCut : inst Hyp2 with n1 = E. cut ToCut with CutHyp. clear CutHyp. clear ToCut. search.
• Mcase, the first "skip.", with: Hyp1 : case Hyp1(keep). CutHyp : assert ({typeOf E T1}). ToCut : inst Hyp2 with n1 = E. cut ToCut with CutHyp. clear CutHyp. clear ToCut. search.
• Mcase, the second "skip.", with: Hyp1 : case Hyp1(keep). CutHyp : assert ({typeOf E T2}). ToCut : inst Hyp3 with n1 = E. cut ToCut with CutHyp. clear CutHyp. clear ToCut. search.
• Mletrec case with: CutHyp : assert ({typeOf (fix (abs T1 R1)) T1}). ToCut : inst Hyp2 with n1 = (fix (abs T1 R1)). cut ToCut with CutHyp. clear CutHyp. clear ToCut. search.

Example: Lang-n-Prove generates stlc_cbv.thm with the following Type Preservation theorem:

Theorem Type-preservation: forall e1, forall e2, forall typ, {typeOf e1 typ} -> {step e1 e2} -> {typeOf e2 typ}. IH0 : induction on 1. intros Main Step. Typing0: case Main.
...
Mapp: case Step. skip.
...

Replace "skip." as shown below.

Theorem Type-preservation: forall e1, forall e2, forall typ, {typeOf e1 typ} -> {step e1 e2} -> {typeOf e2 typ}. IH0 : induction on 1. intros Main Step. Typing0: case Main.
...
Mapp: case Step. Hyp1 : case Hyp1(keep). CutHyp : assert ({typeOf E2 T1}). ToCut : inst Hyp3 with n1 = E2. cut ToCut with CutHyp. clear CutHyp. clear ToCut. search.
...