A reflection-based proof tactic for lattices in Coq
Trends in Functional Programming, June 2–4, 2009, Komárno, Slovakia
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.
proof by reflection, Coq, lattice theory, Whitman's algorithm