Как в coq использовать лемму a = b в обратном порядке?

Question

Предположим, у меня есть лемма L, в которой говорится:

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

Если моя цель имеет форму a + 1 + 1 = b

, я могу написать команду rewrite L, чтобы получить цель формы a + 2 = b

Однако, если моя цель имеет вид a + 2 = b

, как применить лемму в обратном порядке, чтобы получить цель a + 1 + 1 = b?

Answer 1

Скажите

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

Для симметрии есть также rewrite -> L, что совпадает с rewrite L (перезаписать слева направо).

Это задокументировано в Coq's tacti c ссылка .