如何申请（S n' <=? m) = true to S n' <= m?

Question

试图完成 Coq 证明，但我最终陷入了最后一个目标。我把目标变成了S n' <= m and have a hypothesis (S n' <=? m) = true, but am unable to unify these.

我尝试定义一个额外的引理 leb_true 来解决这个问题，但没有成功。我缺少一些简单的东西吗？

Answer 1

<=?

和

<=

是两个不同的东西，但是将这两个东西包含在库中的 Coq 程序员知道它们是相关的。这些知识存储在有关算术的库中。

因此您应该执行以下操作：

Require Import Arith.

Search (_ <=? _) (_ <= _).

这为您提供了可以在证明中使用的定理集合。

Nat.leb_spec0: forall x y : nat, Bool.reflect (x <= y) (x <=? y)
Nat.leb_spec: forall x y : nat, BoolSpec (x <= y) (y < x) (x <=? y)
leb_complete: forall m n : nat, (m <=? n) = true -> m <= n
leb_correct: forall m n : nat, m <= n -> (m <=? n) = true
Nat.leb_le: forall n m : nat, (n <=? m) = true <-> n <= m
Nat.leb_nle: forall x y : nat, (x <=? y) = false <-> ~ x <= y

现在，您可以使用这 6 个定理中的任何一个来证明您所需要的。例如，如果你的目标结论具有形状

formula1 <= formula2

并且你有一个假设为

(formula1 <=? formula2) = true

，那么通过重写语句使用

Nat.leb_le

中的等价物会很有用：

rewrite <- Nat.leb_le.

新生成的目标将包含

(formula1 <=? formula2) = true

，您将能够得出结论。