如何在Coq中证明偏序归纳谓词le的可判定性？

我来帮你搞定这个Coq里的偏序证明难题～先梳理下你的场景：你用归纳关系le定义了A ≤ B ≤ C的偏序，现在想绕开布尔函数leb，直接证明它的反对称性和可判定性，目前卡在了le C A这个假前提的推导上。

你的三个问题，逐个解答： #

1. 如何证明le C A是假前提？ #

核心思路是反演（inversion）le的归纳定义，拆解所有可能构造出le C A的情况，然后逐个戳破矛盾：
le的构造子只有四个：自反性、传递性、A→B、B→C。我们假设存在H: le C A，对H做inversion后会得到四个子目标：

• 子目标1：H0: C = A——直接用discriminate，因为C和A是不同的构造子，不可能相等；
• 子目标2：存在某个z，使得le C z且le z A——先对le C z反演，能构造出le C z的只有le_refl C（即z=C），但此时le z A就是le C A，回到原问题，再反演一次就会发现没有合法构造子，直接矛盾；
• 子目标3、4：H是le_A_B或le_B_C——这两个构造子的左参数是A/B，不可能等于C，用discriminate直接排除。

写成代码就是：

Theorem le_C_A_false : ~le C A.
Proof.
  intros H. inversion H.
  - discriminate. (* C≠A *)
  - inversion H2. (* 拆解le C z，只能是le_refl C *)
    + subst z. inversion H3. (* 拆解le C A，无合法构造子 *)
      discriminate.
  - discriminate. (* H不可能是le_A_B，左边是A≠C *)
  - discriminate. (* H不可能是le_B_C，左边是B≠C *)
Qed.

2. 更高效的直接证明策略 #

不需要依赖leb，直接用**分情况（destruct）+ 反演（inversion）+ 矛盾排除（discriminate/contradiction）**就能搞定所有证明：

改进后的le_antisym直接证明

Theorem le_antisym : forall x y, le x y -> le y x -> x = y.
Proof.
  intros x y Hxy Hyx.
  destruct x, y; simpl in *.
  (* 相同元素的情况直接自反 *)
  - reflexivity.
  - reflexivity.
  - reflexivity.
  (* A≤B但B≤A的情况：反演B≤A，无合法构造子 *)
  - inversion Hyx; discriminate.
  (* A≤C但C≤A的情况：用之前证明的le_C_A_false导出矛盾 *)
  - apply le_C_A_false in Hyx; contradiction.
  (* B≤A的情况：反演B≤A，无合法构造子 *)
  - inversion Hxy; discriminate.
  (* B≤C但C≤B的情况：反演C≤B，无合法构造子 *)
  - inversion Hyx; discriminate.
  (* C≤A的情况：用le_C_A_false导出矛盾 *)
  - apply le_C_A_false in Hxy; contradiction.
  (* C≤B的情况：反演C≤B，无合法构造子 *)
  - inversion Hxy; discriminate.
Qed.

改进后的le_dec直接证明

Theorem le_dec : forall x y, { le x y } + { ~le x y }.
Proof.
  intros x y.
  destruct x, y.
  (* 所有能直接构造le的情况 *)
  - left; apply le_refl.
  - left; apply le_A_B.
  - left; apply le_trans with B; auto. (* A≤C通过传递性推导 *)
  - left; apply le_refl.
  - left; apply le_B_C.
  - left; apply le_refl.
  (* 所有需要证明~le的情况 *)
  - right; intros H; inversion H; discriminate. (* ~B≤A *)
  - right; intros H; inversion H; discriminate. (* ~C≤A *)
  - right; intros H; inversion H; discriminate. (* ~C≤B *)
Qed.

这里的关键是：当要证明~le X Y时，假设存在le X Y，反演后所有构造子都会导出矛盾——要么是元素不相等，要么是构造子的前提根本不成立，用discriminate就能快速排除。

3. 是否需要重新定义le？ #

完全不需要！你的le定义是Coq中定义归纳谓词的标准方式，非常适合进行逻辑推理。如果想让证明更简洁，可以考虑添加le_A_C作为直接构造子（比如le_A_C : le A C），但这不是必须的，因为le_trans已经能推导出来。基于布尔函数的leb适合计算，但归纳定义的le更适合抽象证明，二者各有优势，你当前的定义完全没问题。

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