coq - 为什么遵循 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 H , 只更改 LHS S (n + S n)至 S (S n + n)但不是 RHS S (m + S m) . ll应该适用于所有类型为 nat 的变量。这里有什么问题？

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 ?H和 rewrite !H .这仅在第一个替换物暴露以前不可用的其他替换位置时显示。例如，如果您使用 a + 0 = a 重写，就会出现这种情况。在目标 (a + 0) + 0 = a ; rewrite H离开目标 a + 0 = 0 .