如何使用 Coq GenericMinMax 证明关于实数的事实

Question

我要证明

Theorem T20d :forall (x y:R), (0<x /\ 0<y) -> 0 < Rmin x y.

和

Lemma min_glb_lt n m p : p < n -> p < m -> p < min n m.

在Coq.Structures.GenericMinMax

我用 Require Import 导入的 Coq.Structures.GenericMinMax

然而，当我尝试使用它时，我仍然得到 "reference min_glb_lt" 未找到？我怀疑我需要打开一个范围，但我不知道是哪个范围。

Answer 1

首先，GenericMinMax 库定义了 generic 结构，所以你不能直接使用它们来解决 concrete 问题。该库主要包含仿函数。换句话说，它提供了您需要实现才能使用它们的接口。

在我们的例子中，我们需要实现 MinMaxLogicalProperties 仿函数（或其他包含此仿函数的函数），因为它包含所需的引理。

几个 Coq 标准库提供了这样的实现。对我们来说幸运的是，文件 Rminmax.v, inside the module R 中的实数已经完成，这一行具体为：

Include UsualMinMaxProperties R_as_OT RHasMinMax.

所以，我们可以这样使用它：

Require Import Reals.
Require Import Rminmax. Import R.

Local Open Scope R_scope.

Theorem T20d (x y : R) :
   (0 < x /\ 0 < y) -> 0 < Rmin x y.
Proof.
  intros [? ?].
  now apply min_glb_lt.
Qed.

或者，我们可以通过限定名称 R.min_glb_lt 引用引理——这样我们就可以摆脱 Import R.

如何使用 Coq GenericMinMax 证明关于实数的事实

How to use Coq GenericMinMax to prove facts about the reals

coq