The Coq mailing list

[t x <txrev319 AT gmail.com>]

I've so far managed to get away with:

Ltac subst_all :=
  match goal with
    | H: ?a = _, H2: context[?a] |- _=>  rewrite H in H2 by intuition
    | H: ?a = _ |- context[?a] => rewrite H by intuition
  end.

and then ensuring that whenever I have a "=" in any lemma, the RHS is always "more fundamental" than the LHS.

On Wed, Sep 25, 2013 at 11: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/