Coq中≤传递律的归纳法证明求助（初学者）

针对你定义的le_Nat关系，我们可以通过对自然数m进行归纳来证明传递律，全程只用基础策略，步骤如下：

完整证明代码 #

Inductive Nat := O : Nat | S : Nat -> Nat.

Fixpoint le_Nat (m n : Nat) : bool :=
  match m with 
  | O => true
  | S m' => match n with 
            | O => false
            | S n' => (le_Nat m' n')
            end
  end.

Lemma le_Trans :
  forall m n p,
    le_Nat m n = true -> le_Nat n p = true -> le_Nat m p = true.
Proof.
  intros m n p Hmn Hnp.
  induction m as [| m' IHm'].
  - (* 情况1：m = O *)
    simpl. reflexivity.
  - (* 情况2：m = S m' *)
    destruct n as [| n'].
    + (* 子情况2.1：n = O *)
      simpl in Hmn. discriminate Hmn.
    + (* 子情况2.2：n = S n' *)
      simpl in Hmn. rewrite <- Hmn in IHm'.
      simpl in Hnp. rewrite <- Hnp.
      apply IHm'.
Qed.

逐步骤解释 #

1. 引入变量与前提：intros m n p Hmn Hnp 将所有全称量词变量（m,n,p）和两个前提（m≤n、n≤p）放入上下文。
2. 对m进行归纳：induction m as [| m' IHm'] 拆分出两种核心情况：
   • 当m是O：根据le_Nat的定义，le_Nat O p直接返回true，simpl化简后目标变为true = true，用reflexivity直接得证。
   • 当m是S m'：此时需要对n进一步拆分：
     • 如果n是O：le_Nat (S m') O的结果是false，但前提Hmn说它等于true，矛盾，用discriminate排除该情况。
     • 如果n是S n'：
       • 对Hmn化简得到le_Nat m' n' = true，将其代入归纳假设IHm'；
       • 对Hnp化简得到le_Nat n' p = true；
       • 归纳假设IHm'正好需要这两个前提，因此apply IHm'即可推出le_Nat m' p = true，而这正是化简后的目标。

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