The Coq mailing list

[Daniel Schepler <dschepler AT gmail.com>]

On Mon, Nov 17, 2014 at 2:21 PM, CHAUVIN Barnabe <barnabe.chauvin AT gmail.com> wrote:

I am currently exploring the standard library, and I feel like the different theories (Like for example Reals, Sets, Logic ...) are not really working together ..

I was actually looking for a type of the reals set (Exactly like the inductive type Integers), to be able to use the Sets theories (Ensembles.v ... and especially the order theorems/lemmas).
In Rdefinitions, I found the is_upper_bound definition, which represent the R set with the type R->Prop. It would be more understandable if it would be "Ensemble R", isn't it ? (This is the reason why I said I feel like the theories are not working together ..)

By definition, Ensemble R is identical to R->Prop, so if you had a set in Ensemble R you could use it as an argument to is_upper_bound.  I agree that it would be a bit cleaner to use Ensemble R in the declaration of is_upper_bound from the start, though.

 

Nevertheless, I didn't find such a defintion (the R set). Is-it my mistake, or it is impossible to define such a type, because of the definition of the reals in coq (with axioms) ?
Or maybe I am free to use almost the same definition as Integers, i.e. "Inductive Reals : Ensemble R := Reals_defn : forall x:nat, In R Reals x." and then define a partial order on this set ("PO R") ?

Would that even work as it is?  Or would you need to make it "forall x:nat, In _ Reals (INR x)"?  And then, I'm not sure "Reals" is a very descriptive name for it.  You could also certainly define a partial order on R using Rle - though I'm not sure why you're combining that in the same sentence with the other question.

-- 

Daniel Schepler