coq - 对目标有效的 Coq 反转策略？

Question

我想知道 Coq 中是否存在一种类似倒置的策略，它适用于目标而不是其中一个假设？也就是说，如果有某种策略可以在目标上反转相同的构造函数。

举个愚蠢的例子，

Goal forall x :nat, 2 + x + 3 = x + 5.
 intros. simpl.

， 这使

S ( S (x + 3) ) = S ( S ( S ( ... x)...)

我想反转前两个 S，所以剩下要证明的是

  x + 3 = 3 + x

我的问题是

1. 构造函数的这种“反转”是否合理？

2. 如果逻辑是合理的，那么 Coq 中是否有这样做的策略？

Answer 1

几天前回答了同样的问题。您想做的事情不涉及“反转”，简单的相等就可以了：

Goal forall x :nat, 2 + x + 3 = 5 + x.
Proof.
intros; simpl.
assert (x + 3 = 3 + x). admit.
now rewrite H.

为了简化这种模式，Coq 提供了一个简单的目标一致性策略，试试：

intros; simpl; repeat f_equal.