Lemma Overloading

This project contains Hoare Type Theory libraries which demonstrate a series of design patterns for programming with canonical structures that enable one to carefully and predictably coax Coq's type inference engine into triggering the execution of user-supplied algorithms during unification, and illustrates these patterns through several realistic examples drawn from Hoare Type Theory. The project also contains typeclass-based re-implementations for comparison.

Meta

• Author(s):
  • Georges Gonthier (initial)
  • Beta Ziliani (initial)
  • Aleksandar Nanevski (initial)
  • Derek Dreyer (initial)
• Coq-community maintainer(s):
  • Anton Trunov (@anton-trunov)
• License: GNU General Public License v3.0 or later
• Compatible Coq versions: 8.16 or later (use releases for other Coq versions)
• Additional dependencies:
  • Hierarchy Builder 1.5.0 or later
  • MathComp 2.0.0 or later (ssreflect suffices)
• Coq namespace: LemmaOverloading
• Related publication(s):
  • How to make ad hoc proof automation less ad hoc doi:10.1017/S0956796813000051
  • Structuring the verification of heap-manipulating programs doi:10.1145/1706299.1706331

Building and installation instructions

The easiest way to install the latest released version of Lemma Overloading is via OPAM:

opam repo add coq-released https://coq.inria.fr/opam/released
opam install coq-lemma-overloading

To instead build and install manually, do:

git clone https://github.com/coq-community/lemma-overloading.git
cd lemma-overloading
make   # or make -j <number-of-cores-on-your-machine> 
make install

Files described in the paper

The Coq source files mentioned in the paper How to make ad hoc proof automation less ad hoc, Journal of Functional Programming 23(4), pp. 357-401, are described below. See also the coqdoc presentation of the files from the latest release.

indom.v

This file contains the indomR lemma from Section 3 "A simple overloaded lemma"

terms.v, xfind.v, cancel.v, cancelD.v, cancel2.v

These files prove the cancelR lemma from Section 4 "Reflection: Turning semantics into syntax". The first one contains the abstract syntax for heaps along with the lemma cancel_sound. xfind.v has the xfind structure to find an element in a list, return its index, and extend the list if the element is not found. The file cancel.v has the main overloaded lemma cancelR. Finally, cancelD.v contains the simplify lemma from section 4.3 and cancel2.v contains an alternative version of the cancellation function without using reflection.

stlogR.v

File containing a whole bunch of overloaded lemmas to automate the verification of imperative programs using Hoare Type Theory. The main technicalities in this file are covered in Section 5 "Solving for functional instances".

noalias.v

File containing all the automated lemmas described in Section 6 "Flexible composition and application of overloaded lemmas".

Bonus track

The files below didn't make it to the paper but deserve attention.

auto.v

This file contains an adapted example from VeriML (Stampoulist and Shao), to automatically prove propositions in a logic with binders.

llistR.v

Verification of a linked list datatype using the "step" overloaded lemma described in Section 5.2.

noaliasBT.v

There are several ways to attack a problem. Some of them lead to interesting but yet not entirely satisfactory results. Here are two versions of the noalias overloaded lemma with a different look.

indomCTC.v, xfindCTC.v, cancelCTC.v, noaliasCTC.v, stlogCTC.v

These files contains the same automated lemmas as in the files indom, cancel, noalias and stlogR, but done with Coq Type Classes.

Other files

The files not mentioned above are part of the HTT library, introduced in the paper Structuring the Verification of Heap-Manipulating Programs, Proceedings of the Symposium on Principles of Programming Languages (POPL) 2010, pp. 261-274.