Using "symmetry" within Coq expressions

Question

I'm trying to figure out how to do the following in Coq. Say we have proved the following:

trans_lemma: a = b -> b = c -> a = c

and we want to use it to deduce that

b = a -> c = b -> a = c.

I can't seem to be able to get "apply trans_lemma with ..." to work whatever I do. It would seem like I would need to rewrite equations in trans_lemma, so that the variables would match in the same order. Is there some trivial way of doing this without reproving the lemma, i.e. can I somehow apply the "symmetry" tactic on an equation within an expression?

(I know I can prove what I want without using the lemma by just using a few intros and rewrites, but I would like to know if there's a syntactic way of reusing the result that I already have.)

Ptival Ptival · Accepted Answer · 2012-12-27T23:21:57

You cannot apply something to your lemma that will change its shape magically. What you can do here is to introduce your equalities b = a and c =b, then apply your lemma, leaving you with two goals that can easily be proven by symmetry of =.

In general, I don't think you can apply tactics to terms in the way you wished you could.

Now a few additional things:

if the = here is Coq's equality, you actually don't need a lemma, as transitivity is given to you by the system.
your lemma should be polymorphic : trans_lemma : forall {T} (a b c : T), a = b -> b = c -> c = d. Maybe you show us this one because you are in a section, but then you should probably deduce that second goal once you've closed the section.

(you might also be interested in reusing the Transitive type class from Coq.Classes.RelationClasses...)

Using "symmetry" within Coq expressions

1 Answers