Coq 中的“等于”意味着小于或等于

Question

我试图证明 Coq 中最简单的事情：

Require Import Coq.Structures.OrdersFacts.
Require Import Coq.Structures.Orders.
Lemma easy: forall a b : nat, (a = b) -> (a <= b).
Proof.
  intros.
  apply le_lteq.          (* doesn't work *)
  apply LeIsLtEq.le_lteq. (* doesn't work *)

但我收到以下错误：

The reference le_lteq
was not found in the current
environment.

这有点奇怪，因为我确实在Coq.Structures.Orders中看到了它

Answer 1

正如您在提供的链接中看到的， 的定义le_lteq不在顶层，而是隐藏在其他模块后面。遇到这个问题的一般解决方案是使用Locate.

Locate le_lteq.

会告诉您哪些定义（在范围内，在 后可用Require）具有该名称以及如何调用它们。

请注意，它也适用于符号。

Locate "=".

在这种特殊情况下，它确实不起作用，因为le_lteq它不仅隐藏在模块后面，而且隐藏在函子后面。例如它出现在

Module OT_to_Full (O:OrderedType') <: OrderedTypeFull.
 Include O.
 Definition le x y := x<y \/ x==y.
 Lemma le_lteq : forall x y, le x y <-> x<y \/ x==y.
End OT_to_Full.

这意味着您必须OT_to_Full使用类型的模块进行实例化OrderedType'。

如果没有特殊的理由使用Coq.Structures.Orders那么我宁愿直接寻找自然数的引理。

Search "=" "<=".

不会产生你想要的。相反，我们将在目标中使用subst b替换。这很好，因为我们有一个证明，我们发现使用baa <= a

Search (?x <= ?x).

打印

le_n: forall n : nat, n <= n

那么证明就是：

Lemma easy :
  forall (a b : nat),
    a = b ->
    a <= b.
Proof.
  intros a b e.
  subst b.
  apply le_n.
Qed.