How in coq to use lemma a=b backwards?

user_4929809 0
Viewed 128

Suppose I have a lemma L that says

forall x, x + 1 + 1 = x + 2.

If my goal is of the form a + 1 + 1 = b

I can write a command rewrite L to get a goal of the form a + 2 = b

However, if my goal is of the form a + 2 = b

how to apply the lemma backwards to get a goal a + 1 + 1 = b?

coq proof logic
1 Answers

Say

rewrite <- L. (* Rewrite right to left *)

For symmetry, there's also rewrite -> L, which is the same as rewrite L (rewrite left to right).

This is documented in Coq's tactic reference.

user_56842570
Related