A reflection−based proof tactic for lattices in Coq

Abstract

This paper presents a new proof tactic that decides equalities and in­equalities 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.