Coq如何证明自然数<=关系完全性定理：forall n m, n <= m \/ m <= n

证明思路 #

我们采用自然数归纳法对变量n做归纳，将m保留为全称量化状态，确保归纳假设可以覆盖任意m的情况，再结合已有的le_le_S、O_le_n定理即可完成推导，不需要额外引入新的辅助引理。

逐步骤证明过程 #

1. 引入变量并启动归纳
   首先引入变量n，对n应用归纳法，拆分为基例（n=0）和归纳步（n = S n'）两个分支：

Theorem le_total : forall n m, n <= m \/ m <= n.
Proof.
  intros n. induction n as [| n' IHn].

2. 处理基例（n=0）
   基例下需要证明对任意m，0 <= m \/ m <= 0，直接调用已有定理O_le_n即可证明左分支成立：

- (* n = 0 的情况 *)
    intros m. left. apply O_le_n.

3. 处理归纳步（n = S n'）
   此时我们有归纳假设IHn : forall m, n' <= m \/ m <= n'，需要证明对任意m，S n' <= m \/ m <= S n'。我们对m做结构拆分，分为m=0和m = S m'两个分支：

- (* n = S n' 的情况 *)
    intros m. destruct m as [| m'].
    + (* m = 0 的情况 *)
      right. apply O_le_n.
    + (* m = S m' 的情况 *)
      (* 调用归纳假设获取n'和m'的序关系 *)
      destruct (IHn m') as [Hle | Hge].
      * (* 子情况1：n' <= m'，用le_le_S推导S n' <= S m' *)
        left. apply le_le_S. apply Hle.
      * (* 子情况2：m' <= n'，用le_le_S推导S m' <= S n' *)
        right. apply le_le_S. apply Hge.
Qed.

完整可运行证明代码 #

把所有步骤合并后，完整证明如下：

Theorem le_total : forall n m,
n <= m \/ m <= n.
Proof.
  intros n. induction n as [|n' IHn].
  - intros m. left. apply O_le_n.
  - intros m. destruct m as [|m'].
    + right. apply O_le_n.
    + destruct (IHn m') as [H | H].
      * left. apply le_le_S. apply H.
      * right. apply le_le_S. apply H.
Qed.

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