Coq标准库中定义的Z.le是否具有证明无关性？

我完全理解你的困扰——负定义的谓词确实不像<这种正定义的形式那样能直接套用Hedberg定理（UIP_dec）。不过我们可以通过两种清晰的思路解决这个问题：要么直接处理否定命题的证明无关性，要么把<=转化为等价的正谓词再复用你已掌握的结论。

思路1：直接处理否定命题的证明无关性 #

Z.le的定义是m <= n := m ?= n <> Gt，也就是逻辑上的~(m ?= n = Gt)。要证明它的证明无关性，我们可以借助函数扩展性和comparison类型的可判定相等性来推导：

Require Import ZArith.
Open Scope Z_scope.

Lemma le_proof_irrel : forall m n (p q : m <= n), p = q.
Proof.
  intros m n p q.
  unfold Z.le in p q. (* 展开定义为 ~(m ?= n = Gt) *)
  
  (* 分情况讨论 m ?= n 是否等于 Gt *)
  destruct (decide (m ?= n = Gt)) as [H_eq_Gt | H_not_eq_Gt].
  - (* 如果 m ?= n = Gt 成立，那么 p 是 False 的证明，直接导出矛盾 *)
    contradiction p.
  - (* 如果 m ?= n ≠ Gt，p 和 q 都是 (m ?= n = Gt) → False 的函数 *)
    apply functional_extensionality. (* 函数扩展性：若对所有输入x，f x = g x，则f = g *)
    intros x.
    (* x 是 m ?= n = Gt 的证明，但我们有 H_not_eq_Gt 否定它，因此x会导出矛盾 *)
    destruct (H_not_eq_Gt x).
Qed.

这里的核心逻辑是：当~Q为真时，所有~Q的证明都是从Q到False的函数，而函数扩展性保证这些函数必然相等——因为它们的输入本身就是矛盾的，输出自然也完全一致。

思路2：将<=转化为等价的正谓词 #

由于comparison是枚举类型，m ?= n只能是Eq、Lt、Gt三者之一，所以m <= n等价于(m ?= n = Lt) ∨ (m ?= n = Eq)。我们先证明这个等价关系，再利用你已经证过的<的证明无关性来推导：

步骤1：证明等价关系 #

Lemma le_equiv : forall m n, m <= n <-> (m ?= n = Lt) \/ (m ?= n = Eq).
Proof.
  intros m n.
  split; intro H.
  - (* 从 m <= n 推导析取式 *)
    destruct (m ?= n) as [| |]; simpl in H.
    + right; reflexivity. (* 情况1：m ?= n = Eq *)
    + left; reflexivity. (* 情况2：m ?= n = Lt *)
    + contradiction H. (* 情况3：m ?= n = Gt，与 m <= n 矛盾 *)
  - (* 从析取式推导 m <= n *)
    intro H_or.
    destruct H_or as [H_lt | H_eq].
    + unfold Z.le; rewrite H_lt; discriminate. (* 利用 Lt ≠ Gt 导出 ~(m ?=n = Gt) *)
    + unfold Z.le; rewrite H_eq; discriminate. (* 利用 Eq ≠ Gt 导出 ~(m ?=n = Gt) *)
Qed.

步骤2：证明析取式的证明无关性 #

我们已经知道m ?= n = Lt和m ?= n = Eq的证明都是无关的（由UIP_dec和comparison的可判定相等性保证），接下来证明它们的析取式也满足证明无关性：

(* 先证明 comparison 类型的等式具有证明无关性 *)
Lemma eq_comparison_proof_irrel : forall c1 c2 (p q : c1 = c2), p = q.
Proof.
  intros c1 c2 p q.
  apply UIP_dec.
  apply comparison_eq_dec. (* comparison 类型的相等是可判定的 *)
Qed.

(* 证明析取式的证明无关性 *)
Lemma or_proof_irrel : forall (P Q : Prop),
    (forall (p q : P), p = q) -> (forall (p q : Q), p = q) ->
    forall (p q : P \/ Q), p = q.
Proof.
  intros P Q HP HQ [p1 | p1] [p2 | p2].
  - f_equal; apply HP. (* 两个证明都来自 P 分支 *)
  - contradiction. (* 一个来自P，一个来自Q，矛盾 *)
  - contradiction. (* 同上 *)
  - f_equal; apply HQ. (* 两个证明都来自 Q 分支 *)
Qed.

步骤3：推导<=的证明无关性 #

Lemma le_proof_irrel' : forall m n (p q : m <= n), p = q.
Proof.
  intros m n p q.
  rewrite <- le_equiv in p q. (* 把 <= 替换为等价的析取式 *)
  apply or_proof_irrel.
  - (* 复用你已证的 m < n 的证明无关性 *)
    intros p q. unfold Z.lt; apply eq_comparison_proof_irrel.
  - (* 证明 m ?=n = Eq 的证明无关性 *)
    intros p q. apply eq_comparison_proof_irrel.
Qed.

两种方法都能完成证明：思路1更直接，适合快速推导；思路2通过转化为正谓词复用了你已有的结论，逻辑上更贴合你熟悉的Hedberg定理应用场景。

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