Coq如何证明SFv1中的plus_le_compat_l加法左保序定理？

核心优化思路 #

你当前选择对n做归纳的路径会引入不必要的复杂度，建议优先对*左侧的加数p*做归纳——因为Coq标准库中加法是对第一个参数做结构递归定义的，归纳p刚好匹配p + n的化简方向，证明流程会非常简洁。

最简证明实现 #

Theorem plus_le_compat_l : forall n m p,
  n <= m ->
  p + n <= p + m.
Proof.
  intros n m p H.
  (* 对左侧加数p做归纳 *)
  induction p as [| p' IHp].
  - (* 基例：p = 0 *)
    simpl. (* 化简后目标为 n <= m，直接应用前提即可 *)
    apply H.
  - (* 归纳步：p = S p' *)
    simpl. (* 化简后目标为 S (p' + n) <= S (p' + m) *)
    apply n_le_m__Sn_le_Sm. (* 消去两侧的S构造子 *)
    apply IHp. (* 直接应用归纳假设即可得证 *)
Qed.

你当前卡住分支的补全方案 #

如果要继续沿你原有对n归纳的路径走，当前子目标n + S n' <= n + m可以按以下步骤处理：

1. 用rewrite (plus_comm n (S n'))和rewrite (plus_comm n m)将目标重写为S n' + n <= m + n
2. 此时目标等价于右侧加数保序的性质，如果你已经证明过plus_le_compat_r（右侧加固定数保序），直接应用该定理加前提H即可完成证明

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