CODEWITHSUNDEEP
logiccoqproof
mercury0114
mercury0114

Reputation: 1449

How in coq to use lemma a=b backwards?

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?

Upvotes: 2

Views: 387

Answers (1)

HTNW
HTNW

Reputation: 29148

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.

Upvotes: 2

Related Questions