不能用断言重写目标吗？

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. 为什么？

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

Answer 1

您可以“看到” subterm 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。这是交换律性质，而不是结合律。