How to use Coq GenericMinMax to prove facts about the reals

Question

I'm trying to prove

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

with

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

which is in Coq.Structures.GenericMinMax

which I imported with Require Import Coq.Structures.GenericMinMax

however, I still get "reference min_glb_lt" not found when I try to use it? I suspect I need to open a scope, but I don't know which scope.

Answer 1

First of all, the GenericMinMax library defines generic structures, so you can't use them directly to solve a concrete problem. That library mostly contains functors. In other words, it provides interfaces which you need to implement to be able to use them.

In our case, we need to implement the MinMaxLogicalProperties functor (or some other functor that includes this one), because it includes the required lemma.

Several Coq standard libraries provide such implementations. Luckily for us, it has already been done for the reals in the file Rminmax.v, inside the module R, this line specifically:

Include UsualMinMaxProperties R_as_OT RHasMinMax.

So, we can use it like so:

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.

Alternatively, we could've referred to the lemma by its qualified name R.min_glb_lt -- that would've let us get rid of Import R.