不能用断言重写目标？

Question

我不确定我是否理解为什么重写 H 在某些情况下有效，而在某些情况下却无效。这里例如：

Theorem add_assoc2 : forall n m: nat, n + m = m + n.
Proof. intros. rewrite add_comm. reflexivity. Qed.

Theorem plus_4: forall n m p q: nat,
  n + (n * p) + m + (m * p) = n + m + (n * p) + (m * p).
Proof.
  intros.
  assert (H: n * p + m = m + n * p).
  {  rewrite <- add_assoc2. reflexivity. }
  rewrite H.

给出：

1 goal
n, m, p, q : nat
H : n * p + m = m + n * p
______________________________________(1/1)
n + n * p + m + m * p = n + m + n * p + m * p

但是 Coq 抱怨：Found no subterm matching "n * p + m" in the current goal. 为什么？

我清楚地看到一个，在左边。使用归纳时，用 IHn 重写不会造成任何问题，即使 rewriteable 表达式前面有一些其他项。

Answer 1

您可以“看到”子项 n * p + m，但这是一种误导：Coq 不会向您显示所有 + 表达式周围的隐式括号。

使用

Set Printing Parentheses.

让它们可见。你的证明状态真的是：

  n, m, p, q : nat
  H : ((n * p) + m) = (m + (n * p))
  ============================
  (((n + (n * p)) + m) + (m * p)) = (((n + m) + (n * p)) + (m * p))

Coq 是正确的，没有子项匹配 H 的左侧表达式 ((n * p) + m)。您需要使用一些关联性引理来重写以移动括号。

此外，add_assoc2 不是引理 forall n m: nat, n + m = m + n 的好名称。这是交换性属性，不是结合性

不能用断言重写目标？

Cannot rewrite goal with assertion?

coq