为什么下面的 Coq 重写不适用于假设的右侧？

Question

我有以下 Coq 环境。

    1 subgoals
m : nat
IHm : forall n : nat, n + n = m + m -> n = m
n : nat
H : S (n + S n) = S (m + S m)
ll := ll : forall k : nat, k + S k = S k + k

这样做，只改变rewrite ll in HLHS ，而不改变RHS 。 应该适用于 nat 类型的所有变量。这里有什么问题吗？S (n + S n)S (S n + n)S (m + S m)ll

Answer 1

扩展 Emilio 的评论，rewrite H首先rewrite H in H'会找到 的所有（独立）量化变量的实例化H，然后用 RHS 替换该实例化 LHS 的所有出现*。我相信它找到了语法树中最上面/最左边的实例化。因此，例如，如果您这样做：

Goal forall a b, (forall x, x + 0 = x) -> (a + 0) * (a + 0) * (b + 0) = a * a * b.
  intros a b H.
  rewrite H.

将会rewrite H选择实例化x，a最终的目标将是a * a * (b + 0) = a * a * b。您可以在引理前面加上!(如rewrite !H) 来表示“到处重写，尽可能多地选择实例化”，或者使用?(如rewrite ?H) 来表示try rewrite !H，即，您可以选择多个实例化，并且如果您这样做也不会失败找不到任何。

*实际上还有一些细微差别，即替换是通过使用 和 在单遍中完成的，以及rewrite H在多次遍中完成的。仅当第一个替换暴露了以前不可用的其他替换位置时，​​才会出现此情况。例如，如果您在目标中用重写，就会出现这种情况；离开球门。rewrite ?Hrewrite !Ha + 0 = a(a + 0) + 0 = arewrite Ha + 0 = 0