coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] congruence closure on arbitrary equivalence relations?

From: Frédéric Blanqui <frederic.blanqui AT inria.fr>
To: coq-club AT inria.fr
Subject: [Coq-Club] congruence closure on arbitrary equivalence relations?
Date: Wed, 10 Feb 2016 10:20:59 +0100

Hello.

Does anyone know a tactic for solving goals of the form "R t u" where R is an Equivalence relation and t and u are terms built from function symbols compatible with R, that is, a tactic similar to congruence but for arbitrary equivalence relations?

Frédéric.

[Coq-Club] congruence closure on arbitrary equivalence relations?, Frédéric Blanqui, 02/10/2016