The Coq mailing list

[Daniel Schepler <dschepler AT gmail.com>]

The "congruence" tactic should be able to solve any such situation (and in fact can manage to find solutions in some more complex situations, as well).

On Wed, Sep 25, 2013 at 4:43 PM, Abhishek Anand <abhishek.anand.iitg AT gmail.com> wrote:

Hi,
Often I have to prove an equality that can be proven by merely applying transitivity and symmetry on other equalities of the same type in my hypotheses.
I think someone must have already written a tactic which builds an undirected graph of equalities(hypotheses) of the same type and then finds whether a path exists, and build its proof object.
If not, any ideas on the easiest way to achieve this would be appreciated.
Thanks,

-- Abhishek
http://www.cs.cornell.edu/~aa755/