Coq自然数不等式反向证明卡壳，求指导及战术说明列表疑问

一、目标命题的证明方法 #

你要证明的命题是：

forall i j : nat, i <= j -> forall w : nat, i <= w -> j <= w -> w - i >= w - j

1. 先证明关键引理 #

你提到的w - m >= w - S m是核心子目标，先单独证明这个引理：

Lemma sub_S_le : forall w n : nat, w - n >= w - S n.
Proof.
  intros w n.
  induction w as [|w IH].
  - simpl. reflexivity. (* w=0时，0-n=0，0-Sn=0，0>=0成立 *)
  - induction n as [|n IHn].
    + simpl. apply le_n. (* n=0时，w - 0 = w，w - S0 = w-1，w >= w-1对任意w成立 *)
    + simpl. apply le_trans with (m := w - n). (* 用传递性，把w - S n转化为(w - n) -1，结合归纳假设 *)
      * apply IH.
      * apply IHn.
Qed.

2. 基于引理完成原命题证明 #

利用<=的归纳定义（直接对i<=j的证明项做归纳），结合上面的引理：

Theorem sub_le_rev : forall i j : nat, i <= j -> forall w : nat, i <= w -> j <= w -> w - i >= w - j.
Proof.
  intros i j Hle.
  induction Hle as [|j' Hle' IH].
  - intros w Hi Hj. simpl. apply le_refl. (* 基例：j=i时，w-i >=w-i自反成立 *)
  - intros w Hi Hj.
    (* 归纳步骤：j=S j'，此时i<=j'，用归纳假设得到w-i >=w-j'，再结合引理w-j' >=w-S j'，传递得结论 *)
    apply le_trans with (m := w - j').
    * apply IH.
      (* 验证归纳假设的前提：i<=w和j'<=w *)
      apply le_trans with (m := j'). apply Hi. apply Hle'.
      apply le_trans with (m := j). apply Hj. apply le_S. apply Hle'.
    * apply sub_S_le.
Qed.

3. 更简便的方法：使用omega战术 #

Coq内置的omega战术可以自动解决大部分线性算术问题，直接一步搞定：

Theorem sub_le_rev : forall i j : nat, i <= j -> forall w : nat, i <= w -> j <= w -> w - i >= w - j.
Proof.
  intros i j Hle w Hi Hj. omega.
Qed.

二、关于Coq战术资源的说明 #

• 官方的《Coq Reference Manual》包含完整的战术列表，但内容偏学术化，新手入门门槛高。
• 常用战术可以按场景整理：
  • 基础交互：intros（引入变量/假设）、simpl（化简表达式）、reflexivity（自反性证明）、apply（应用定理/假设）
  • 归纳证明：induction（结构归纳）、destruct（拆分结构）
  • 逻辑推理：split（拆分合取）、left/right（拆分析取）、exfalso（归谬法）
  • 算术专用：omega（线性算术自动证明）、lia（更通用的线性整数算术）
• 中文社区的入门教程会整理常用战术的极简说明，适合新手快速查阅。

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