如何有效简化具有上一个引理的coq目标？

Question

为什么我的证明的最后一行没有丢下一个后继者，而不是增加一个。注意：我在课堂环境之外做这些练习，不要纵容人们使用它来欺骗硬件，我只是不知道还有什么要问的。摘自Pierce的“战术”一章。

Theorem plus_n_n_injective : forall n m,
     n + n = m + m ->
     n = m.
Proof.
  intros n. induction n as [| n'].
  intros.
  simpl in H.
  destruct m.
  reflexivity.
  discriminate.
  intros.
  rewrite <- plus_n_Sm in H.
  destruct m.
  discriminate.
  rewrite <- plus_n_Sm in H.
  apply S_injective in H.
  simpl in H.
  apply S_injective in H.
  apply S_injective.

使用这些辅助引理的地方

Theorem S_injective : forall (n m : nat),
  S n = S m ->
  n = m.
Proof.
  intros n m H1.
  assert (H2: n = pred (S n)). { reflexivity. }
  rewrite H2. rewrite H1. reflexivity.
Qed.
Theorem plus_n_Sm : forall n m : nat,
    S (n + m) = n + (S m).
Proof.
  intros n m. induction n as [| n' IHn'].
  simpl.
  reflexivity.
  simpl.
  rewrite -> IHn'.
  reflexivity.
Qed.

Answer 1

如果您查看S_injective的陈述：

Theorem S_injective : forall (n m : nat),
  S n = S m ->
  n = m.

您会看到它说证明n = m足以证明S n = S m。在应用它之前，您必须证明S n' = S m，然后说您只需要证明S (S n') = S (S m)。这是因为目标中的apply正在做一些向后思考。

您想要的是能够说n = m -> S n = S m。您可以像以前一样手动证明引理，或者可以使用f_equal策略（通常用于从f n = f m证明n = m中的f（大致））。