如何证明加法的单射性？Coq证明过程遇阻求助

你要证明的add_n_injective是加法左消去律，但你实际编写的代码是在证明另一个命题plus_injective（即若n+n=m+m则n=m）。下面分别给出两个命题的解决方法：

1. 加法左消去律add_n_injective的简便证明 #

这个定理有两种高效证明方式：

方法一：直接调用内置定理 #

Coq标准库中已经内置了加法左消去的定理plus_reg_l，直接复用即可：

Theorem add_n_injective : forall n m p, n + m = n + p -> m = p.
Proof.
  intros n m p H.
  apply plus_reg_l in H. assumption.
Qed.

方法二：手动归纳证明 #

如果不想依赖内置定理，用基础归纳法也能快速完成：

Theorem add_n_injective : forall n m p, n + m = n + p -> m = p.
Proof.
  intros n m p H.
  induction n as [|n IHn].
  - simpl in H. assumption. (* n=0时，0+m=m、0+p=p，H直接等价于m=p *)
  - simpl in H. apply IHn in H. assumption. (* n=S n'时，S(n'+m)=S(n'+p)，由S的单射性得n'+m=n'+p，再用归纳假设 *)
Qed.

2. 你的plus_injective定理卡住的解决方法 #

你当前的证明卡在最后一个子目标，问题出在归纳步骤的等式转换上。重新整理后的完整证明如下：

Theorem plus_injective : forall n m, n + n = m + m -> n = m.
Proof.
  intros n m H.
  induction n as [|n IHn].
  - simpl in H. induction m as [|m IHm].
    + reflexivity. (* n=0、m=0时直接成立 *)
    + discriminate H. (* n=0、m=S m'时，0+0=0，而m+m=S(m'+S m')，两者类型矛盾 *)
  - induction m as [|m IHm].
    + discriminate H. (* n=S n'、m=0时，n+n=S(n'+S n')，0+0=0，类型矛盾 *)
    + simpl in H. inversion H. (* 消去外层S，得到n'+S n' = m'+S m' *)
      rewrite <- plus_n_Sm in H0. rewrite plus_n_Sm in H0. (* 把S n'转换为n'+1，重写等式 *)
      simpl in H0. inversion H0. (* 消去S，得到n'+n' = m'+m' *)
      apply IHn in H1. rewrite H1. reflexivity. (* 用归纳假设得n'=m'，进而S n'=S m' *)
Qed.

关键步骤说明：

• 当n=S n'且m=S m'时，先用inversion H消去外层的构造子S，得到内层等式
• 借助plus_n_Sm（即n + S m = S(n + m)）将n'+S n'重写为S(n'+n')，同理处理m的部分
• 再次用inversion得到n'+n'=m'+m'，调用归纳假设IHn得到n'=m'，最后重写完成证明

内容的提问来源于stack exchange，提问作者wulalala