如何在特定子表达式中应用重写？

Question

我正在使用在线书籍“软件基础”来了解 Coq。

第二章要求证明“plus_assoc”定理：

Theorem plus_assoc : forall n m p : nat, n + (m + p) = (n + m) + p.

我利用了两个先前证明的定理：

Theorem plus_comm : forall n m : nat, n + m = m + n.
Theorem plus_n_Sm : forall n m : nat, S (n + m) = n + (S m).

我在 n 上使用归纳证明了 plus_assoc 定理：

Proof.
  intros n m p.
  induction n as [ | n' ].
    reflexivity.

    rewrite plus_comm.
    rewrite <- plus_n_Sm.
    rewrite plus_comm.
    rewrite IHn'.
    symmetry.
    rewrite plus_comm.

此时，上下文 (*) 为：

1 subgoals
case := "n = S n'" : String.string
n' : nat
m : nat
p : nat
IHn' : n' + (m + p) = n' + m + p
______________________________________(1/1)
p + (S n' + m) = S (n' + m + p)

我想使用 plus_comm 来获取

p + (m + S n') = S (n' + m + p)

然后加上_n_sm

p + S (m + n') = S (n' + m + p)

然后再plus_n_sm

S (p + (m + n')) = S (n' + m + p)

并使用 plus_comm 两次完成证明，然后自反性

S (p + (n' + m)) = S (n' + m + p)
S (n' + m + p) = S (n' + m + p)

小问题是我不知道如何将 plus_comm 应用于 (S n' + m)。

重要的问题是：为什么要发行

apply plus_comm.

立即完成证明（在给定的上下文中（*））？

预先感谢您的任何澄清！

法比安·皮克

Answer 1

您可以通过使用 (S n') 和 m 将 plus_comm 实例化到 (S n' + m)。

    Check plus_comm.
    Check plus_comm (S n').
    Check plus_comm (S n') m.
    rewrite (plus_comm (S n') m).
    rewrite <- plus_n_Sm.
    rewrite <- plus_n_Sm.
    rewrite (plus_comm m n').
    rewrite plus_comm.
    reflexivity.
Qed.

我认为使用Require Import Coq.Setoids.Setoid.然后使用rewrite plus_comm at 2.应该具有相同的效果，但它不起作用。

之所以apply plus_comm完成目标是因为apply进行统一模转换。也就是说，p + (S n' + m) = S (n' + m + p)可以转换为 p + (S n' + m) = S n' + m + p，并且p + (S n' + m) = S n' + m + p可以与 统一 ?1 + ?2 = ?2 + ?1。

事实上，如果你使用这个simpl策略进行归约，证明会变得更短。

Theorem plus_assoc : forall n m p : nat, n + (m + p) = (n + m) + p.
Proof.
induction n.
  reflexivity.

  intros.
  simpl.
  apply f_equal.
  apply IHn.
Qed.