Julien Puydt (Nov 29 2022 at 08:24): Julien Puydt (Nov 29 2022 at 08:24):I was stuck in one of my proofs because I couldn't compare extended real numbers correctly ; the existing ereal_comparable looks pretty weak ; did I miss something obvious?
From mathcomp Require Import all_ssreflect all_algebra.
From mathcomp.analysis Require Import boolp classical_sets constructive_ereal reals.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Import Num.Theory Order.POrderTheory.
Open Scope real_scope.
Open Scope ring_scope.
Section Missing.
Context {R : realType}.
Check ereal_comparable. (* forall x y : \bar ?R, (0%E >=< x)%O -> (0%E >=< y)%O -> (x >=< y)%O *)
Lemma ereal_really_comparable (a b: \bar R): (a >=< b)%O.
Proof.
case: a.
- move=> a.
case: b.
+ move=>b.
by apply: real_comparable; apply: num_real.
+ by apply: le_comparable; apply: leey.
+ rewrite comparable_sym.
by apply: le_comparable; apply: leNye.
- rewrite comparable_sym.
by apply: le_comparable; apply: leey.
- by apply: le_comparable; apply: leNye.
Qed.
End Missing.
mathcomp.analysis in the From of Require but simply mathcomp (we ensure that there is no file collision in this namespace already, and we reserve the right to change a module from one submodule to another, so it's not a good idea to rely on a too precise location)Import Order.TheorycomparableT. Cyril Cohen (Nov 29 2022 at 13:22):From mathcomp Require Import all_ssreflect all_algebra.
From mathcomp Require Import constructive_ereal reals.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Import Order.Theory.
Fact ereal_really_comparable {R : realType} (a b : \bar R) : (a >=< b)%O.
Proof. exact: comparableT. Qed.
I realize I hadn't answered: yes, that's it! Thanks!
Notification Bot (Dec 05 2022 at 08:36):Julien Puydt has marked this topic as resolved.
Last updated: Nov 29 2023 at 06:01 UTC