A reflection-based proof tactic for lattices in Coq
Daniel W.H. James, Ralf Thomas Walter Hinze · Intellect Books · 2014
Coq is a proof assistant featuring a tactic-based interactive theorem prover. The latest incarnation comes with over 150 tactics that assist the user in developing a formal proof. These tactics range from the simple and mundane to the ‘allpowerful’. Some examples from the latter category are the omega tactic that solves a goal in Presburger arithmetic and the ring and field tactics that solve identities modulo associativity and commutativity in ring and field structures. This paper presents a new proof tactic that decides equalities and inequalities between terms over lattices. It uses a decision procedure that is a variation on Whitman’s algorithm and is implemented using a technique known as proof by reflection. We will paint the essence of the approach in broad strokes and discuss the use of certified functional programs to aid the automation of formal reasoning. This paper makes three contributions. Firstly it serves an an introduction to using proof by reflection approach Coq. This utilizes the Ltac language and two recent extensions to the Coq system: type classes and the PROGRAM extension. Secondly it gives a certified implementation of Whitman’s algorithm in Coq, with proofs of correctness and termination. Thirdly, the final product of this work is a useable proof tactic that can be applied to proof goals involving equalities and inequalities in lattice theory. The rest of the paper is organized as follows: Section 2 will give a short introduction to Coq, highlighting the concept of a proof term, and will refresh the necessary details of lattice theory. We will give a motivation for the problem in Section 3, and a Coq-based introduction to free lattices along with the decision