Coq leb <=?在案例或归纳之后没有给我一个假设

如何解决Coq leb <=?在案例或归纳之后没有给我一个假设

我已将我的情况简化为以下代码，希望这可以更容易理解。

我想证明以下引理：

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

在证明中执行以下步骤

Proof.
intros.

给我结果

1 subgoal
a,b : nat
______________________________________(1/1)
if a <=? b then a <= b else a > b

a 小于或等于 b 似乎微不足道，在这种情况下我可以证明 a<=b。在 b 大于 a 的另一种情况下，我可以证明 a>b。

我试图用 induction(a<=?b) 或 case (a<=?b) 证明这一点，但两者都给了我以下结果。

2 subgoals
a,b : nat
______________________________________(1/2)
a <= b
______________________________________(2/2)
a > b

现在我无法证明这些目标。我希望在第二种情况下获得一个假设，例如 H: a <= b 和 H: a > b。这样，我就能证明我的目标。

有人能告诉我如何解决不出现假设的问题吗？

编辑： 整个引理可以证明如下：

Require Import Arith.
Lemma example: forall a b,if a<=?b then a<=b else a > b.
Proof.
intros.
Check Nat.leb_spec.
case (Nat.leb_spec a b);intuition.

解决方法

发生的事情是 <=? 是返回布尔值的函数，true 或 false。当您要求 Coq 对表达式 a <=? b 进行归纳或案例分析时，它确实会这样做并将证明减少到两种情况：一种是 a <=? b 被 true 替代，另一种是它被 false 代替。如果您想跟踪被破坏的值，您应该使用 destruct (a <=? b) eqn:H. 明确要求它（请参阅 documentation）。

,

要区分您正在寻找的大小写，您可以使用

Nat.leb_spec : forall x y : nat,BoolSpec (x <= y) (y < x) (x <=? y)

类型 BoolSpec 准确地体现了您要执行的操作：如果 (x <=? y) 是 布尔值 true，则 命题 x <= y 为真，如果 (x <=? y 为 false，则 y < x 为真。因此，Nat.leb_spec 体现了函数 x <=? y 的规范，顾名思义。

现在使用 case (Nat.leb_spec a b) 与您尝试使用 case (a <=? b) 完全一样：它为您提供了两个子目标，其中一个 x <=? y 被 true 替换并且您有 { {1}} 作为一个额外的假设，另一个 x <= y 被 x <=? y 替换，而你有 false 作为一个假设。您区分大小写的事实是基于 y < x 类型的术语，而不是简单的 BoolSpec 类型。