请求协助证明Coq中“若m≤n则max(m,n)=n”的引理

昨天我在这里提问了一个Coq相关的证明问题，得到的解答帮助极大，让我能够独立完成诸多练习并探索新特性。今天我有另一项练习，要求证明“对所有自然数m、n，若m≤n则max(m,n)=n”。我尝试对m进行归纳，但遇到了瓶颈，恳请各位提供帮助！

相关定义与待证引理 #

自然数的max函数定义 #

Fixpoint max (m n : Nat) : Nat :=
  match m with
  | O => n
  | S m' => match n with
            | O => m
            | S n' => S (max m' n')
            end
  end.

自然数的小于等于判断函数定义 #

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_max_true :
  forall m n,
    le_Nat m n = true ->
    max m n = n.
Proof.
    ...
Qed.

完整证明过程 #

我们可以通过对m进行归纳，结合le_Nat的定义分情况讨论n的构造来完成证明：

Lemma le_max_true :
  forall m n,
    le_Nat m n = true ->
    max m n = n.
Proof.
  induction m as [|m' IHm'].
  - (* m = O 的情况 *)
    intros n H.
    simpl max.
    reflexivity.
  - (* m = S m' 的情况 *)
    intros n H.
    destruct n as [|n'].
    + (* n = O 的情况 *)
      simpl le_Nat in H.
      contradiction.
    + (* n = S n' 的情况 *)
      simpl le_Nat in H.
      simpl max.
      rewrite IHm' with (n := n').
      reflexivity.
Qed.

证明思路说明 #

• 基例（m=O）：当m为0时，根据max的定义，max O n直接等于n，和前提le_Nat O n = true完全匹配，用reflexivity即可直接完成证明。
• 归纳步（m=S m'）：
  • 若n为0，le_Nat (S m') O的结果是false，和前提le_Nat m n = true矛盾，用contradiction直接终结该分支。
  • 若n为S n'，le_Nat (S m') (S n')等价于le_Nat m' n' = true，此时max (S m') (S n')展开为S (max m' n')，应用归纳假设IHm'（即当le_Nat m' n' = true时max m' n' = n'），替换后目标变为S n' = S n'，再用reflexivity完成证明。

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