Online : https://veri-bbb.imag.fr/b/pie-zc2-ji9
30 June 2020 - 14h00
A Decision Procedure for Equivalence Relations
by Sébastien Michelland from ENS de Lyon
Abstract: Equality or equivalence between objects is a typical kind of Coq goal that regularly appears in theories. When it is a consequence of the context, one can simply rewrite their way through, but it is more convenient to handle it with a tactic. The congruence tactic by Pierre Corbineau is a decision procedure designed to solve these problems.
We propose to generalize congruence by supporting hierarchies of equivalence relations in the congruence closure algorithm (this is, to the best of our knowledge, a new extension). This new tactic would be used to decide ground relations of the form (R x y) using relations in the context. When universally-quantified relation hypotheses are involved, we can only hope to have a semi-decision procedure.
The tactic, still under development, started as a command-line tool written in Ocaml and is currently being integrated into Coq as a plugin. This tool generates standalone Coq proof scripts which can be checked independently. It implements the extended congruence closure algorithm, along with inclusion hierarchies and PERs. Universally-quantified relation hypotheses can be instantiated by the matching algorithm, which makes it possible to describe simple first-order theories.
joint work with P. Corbineau, L. Rieg, K. Altisen
Accepted for presentation at the Coq Workshop 2020
