如何使用勒柯克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

我进口与要求导入Coq.Structures.GenericMinMax

但是，我仍然得到“参考min_glb_lt”当我尝试使用它时没有找到？我怀疑我需要打开一个范围，但我不知道哪个范围。

Answer 1

首先，在GenericMinMax库定义通用结构，所以你不能直接使用它们来解决具体问题。该库大部分包含仿函数。换句话说，它提供了你需要实现的接口，以便能够使用它们。

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

几个Coq标准库提供了这样的实现。幸运的是，它已经完成了文件Rminmax.v的实数，模块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。