如何在Coq中简化证明加法小于定理plus_lt

核心思路 #

这个定理确实不需要复杂的嵌套归纳，本质只需要用到两个自然数基本性质：

• 对任意自然数 a b，都有 a ≤ a + b 且 b ≤ a + b（加法的单调性）
• 小于关系 x < y 等价于 S x ≤ y，且小于关系满足传递性：如果 x < z 且 z < y，则 x < y

最简手动证明代码 #

Require Import PeanoNat.

Theorem plus_lt : forall n1 n2 m,
  n1 + n2 < m ->
  n1 < m /\ n2 < m.
Proof.
  intros n1 n2 m H.
  split.
  (* 证明n1 < m：先证n1 < n1+n2，再结合已知n1+n2 < m用传递性 *)
  - apply Nat.lt_le_trans with (m := n1 + n2).
    + apply Nat.lt_succ_r, Nat.le_plus_r.
    + exact H.
  (* 证明n2 < m：逻辑完全对称 *)
  - apply Nat.lt_le_trans with (m := n1 + n2).
    + apply Nat.lt_succ_r, Nat.le_plus_l.
    + exact H.
Qed.

如果允许使用自动算术策略，一行就能完成证明：

Proof. intros; lia. Qed.

你当前卡住的目标解决方案 #

你当前的目标 S (S n2') <= S m' 可以直接用上下文中的 H1 和加法单调性证明：

(* 先简化目标：S a <= S b 等价于 a <= b *)
apply le_Sn_le.
(* 由H1得S(n1 + S n2') <= m'，而S(S n2') <= S(n1 + S n2')，用传递性即可 *)
apply le_trans with (m := S (n1 + S n2')).
- apply le_S, Nat.le_plus_l.
- exact H1.

原证明冗余原因 #

你嵌套了n2和m两层归纳，属于把简单问题复杂化了。这个结论不需要归纳，只用基础的序关系传递性和加法性质就能直接推导，后续做证明前可以先理清楚数学逻辑，再对应到Coq的引理调用，能少走很多弯路。

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