Coq中使用case/induction处理leb（<=?）时无法生成对应假设的问题求助

你遇到的问题其实很典型：a<=?b是一个布尔值计算（返回bool类型），而你需要的是它对应的逻辑命题（a <= b或a > b）。直接用case (a<=?b)或者induction只会拆分布尔值的两个分支，但不会自动把布尔结果和逻辑命题关联起来，所以自然拿不到你需要的假设。

核心原因 #

Coq里的布尔比较算子（比如<=?）和逻辑命题（比如<=）是分开设计的：

• a <=? b : bool：执行计算得到真或假的布尔值
• a <= b : Prop：表示一个可证明的逻辑断言

要把这两者的含义绑定起来，需要用到规格引理（spec lemma）——这类引理专门描述布尔算子对应的逻辑语义。对于自然数的小于等于比较，对应的就是Nat.leb_spec。

完整解决步骤 #

我们一步步修正你的证明流程：

1. 先导入库并声明引理：

Require Import Arith.
Lemma example: forall a b, if a<=?b then a<=b else a > b.
Proof.
intros.

2. 先查看Nat.leb_spec的类型，确认它的作用：

Check Nat.leb_spec.
(* 输出：Nat.leb_spec : forall n m : nat, (n <=? m) = true <-> n <= m *)

这个引理明确告诉我们：n <=? m为真当且仅当n <= m；反过来，当n <=? m为假时，结合自然数的全序性，自然就能推出n > m。

3. 使用case策略应用这个规格引理，它会帮我们生成带对应假设的分支：

case (Nat.leb_spec a b); intuition.

• 第一个分支会得到假设H: (a <=? b) = true，intuition会自动结合Nat.leb_spec推导出a <= b
• 第二个分支会得到假设H: (a <=? b) = false，此时Nat.leb_spec的逆否命题意味着~(a <= b)，自然数的全序性会让intuition自动得出a > b

这样就能顺利完成两个子目标的证明了。

拓展写法：更细分的引理应用 #

你也可以用更细分的引理手动完成推导，步骤更清晰：

Proof.
intros a b.
destruct (a <=? b) as [H|H].
- (* 分支1：a <=? b = true *)
  apply Nat.leb_le in H; assumption.
- (* 分支2：a <=? b = false *)
  apply Nat.leb_gt in H; assumption.
Qed.

这里Nat.leb_le直接将布尔真映射为命题a <= b，Nat.leb_gt直接将布尔假映射为命题a > b，同样能快速完成证明。

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