Record mixin_of (
R :
ringType) :=
Mixin {
-
norm_op :
R → R;
-
le_op :
rel R;
-
lt_op :
rel R;
-
_ :
∀ x y,
le_op (
norm_op (
x + y)) (
norm_op x + norm_op y);
-
_ :
∀ x y,
lt_op 0
x → lt_op 0
y → lt_op 0 (
x + y);
-
_ :
∀ x,
norm_op x = 0
→ x = 0;
-
_ :
∀ x y,
le_op 0
x → le_op 0
y → le_op x y || le_op y x;
-
_ :
{morph norm_op : x y / x × y};
-
_ :
∀ x y,
(le_op x y) = (norm_op (
y - x)
== y - x);
-
_ :
∀ x y,
(lt_op x y) = (y != x) && (le_op x y)
+
norm_op :
R → R;
+
le_op :
rel R;
+
lt_op :
rel R;
+
_ :
∀ x y,
le_op (
norm_op (
x + y)) (
norm_op x + norm_op y);
+
_ :
∀ x y,
lt_op 0
x → lt_op 0
y → lt_op 0 (
x + y);
+
_ :
∀ x,
norm_op x = 0
→ x = 0;
+
_ :
∀ x y,
le_op 0
x → le_op 0
y → le_op x y || le_op y x;
+
_ :
{morph norm_op : x y / x × y};
+
_ :
∀ x y,
(le_op x y) = (norm_op (
y - x)
== y - x);
+
_ :
∀ x y,
(lt_op x y) = (y != x) && (le_op x y)
}.
@@ -247,25 +257,27 @@
base :
GRing.IntegralDomain.class_of T;
mixin :
mixin_of (
ring_for T base)
}.
-
Structure type :=
Pack {
sort;
_ :
class_of sort;
_ :
Type}.
+
Structure type :=
Pack {
sort;
_ :
class_of sort}.
Variables (
T :
Type) (
cT :
type).
-
Definition class :=
let:
Pack _ c _ as cT' :=
cT return class_of cT' in c.
-
Let xT :=
let:
Pack T _ _ :=
cT in T.
-
Notation xclass := (
class : class_of xT).
-
Definition clone c of phant_id class c := @
Pack T c T.
+
Definition class :=
let:
Pack _ c as cT' :=
cT return class_of cT' in c.
+
Let xT :=
let:
Pack T _ :=
cT in T.
+
Notation xclass := (
class : class_of xT).
+
+
+
Definition clone c of phant_id class c := @
Pack T c.
Definition pack b0 (
m0 :
mixin_of (
ring_for T b0)) :=
-
fun bT b &
phant_id (
GRing.IntegralDomain.class bT)
b ⇒
-
fun m &
phant_id m0 m ⇒
Pack (@
Class T b m)
T.
+
fun bT b &
phant_id (
GRing.IntegralDomain.class bT)
b ⇒
+
fun m &
phant_id m0 m ⇒
Pack (@
Class T b m).
-
Definition eqType := @
Equality.Pack cT xclass xT.
-
Definition choiceType := @
Choice.Pack cT xclass xT.
-
Definition zmodType := @
GRing.Zmodule.Pack cT xclass xT.
-
Definition ringType := @
GRing.Ring.Pack cT xclass xT.
-
Definition comRingType := @
GRing.ComRing.Pack cT xclass xT.
-
Definition unitRingType := @
GRing.UnitRing.Pack cT xclass xT.
-
Definition comUnitRingType := @
GRing.ComUnitRing.Pack cT xclass xT.
-
Definition idomainType := @
GRing.IntegralDomain.Pack cT xclass xT.
+
Definition eqType := @
Equality.Pack cT xclass.
+
Definition choiceType := @
Choice.Pack cT xclass.
+
Definition zmodType := @
GRing.Zmodule.Pack cT xclass.
+
Definition ringType := @
GRing.Ring.Pack cT xclass.
+
Definition comRingType := @
GRing.ComRing.Pack cT xclass.
+
Definition unitRingType := @
GRing.UnitRing.Pack cT xclass.
+
Definition comUnitRingType := @
GRing.ComUnitRing.Pack cT xclass.
+
Definition idomainType := @
GRing.IntegralDomain.Pack cT xclass.
End ClassDef.
@@ -293,10 +305,10 @@
Canonical idomainType.
Notation numDomainType :=
type.
Notation NumMixin :=
Mixin.
-
Notation NumDomainType T m := (@
pack T _ m _ _ id _ id).
-
Notation "[ 'numDomainType' 'of' T 'for' cT ]" := (@
clone T cT _ idfun)
+
Notation NumDomainType T m := (@
pack T _ m _ _ id _ id).
+
Notation "[ 'numDomainType' 'of' T 'for' cT ]" := (@
clone T cT _ idfun)
(
at level 0,
format "[ 'numDomainType' 'of' T 'for' cT ]") :
form_scope.
-
Notation "[ 'numDomainType' 'of' T ]" := (@
clone T _ _ id)
+
Notation "[ 'numDomainType' 'of' T ]" := (@
clone T _ _ id)
(
at level 0,
format "[ 'numDomainType' 'of' T ]") :
form_scope.
End Exports.
@@ -308,26 +320,26 @@
Module Import Def.
Section Def.
Import NumDomain.
Context {
R :
type}.
-
Implicit Types (
x y :
R) (
C :
bool).
+
Implicit Types (
x y :
R) (
C :
bool).
-
Definition normr :
R → R :=
norm_op (
class R).
-
Definition ler :
rel R :=
le_op (
class R).
-
Definition ltr :
rel R :=
lt_op (
class R).
+
Definition normr :
R → R :=
norm_op (
class R).
+
Definition ler :
rel R :=
le_op (
class R).
+
Definition ltr :
rel R :=
lt_op (
class R).
-
Definition ger :
simpl_rel R :=
[rel x y | y ≤ x].
-
Definition gtr :
simpl_rel R :=
[rel x y | y < x].
-
Definition lerif x y C :
Prop := (
(x ≤ y) × ((x == y) = C))%
type.
-
Definition sgr x :
R :=
if x == 0
then 0
else if x < 0
then -1
else 1.
-
Definition minr x y :
R :=
if x ≤ y then x else y.
-
Definition maxr x y :
R :=
if y ≤ x then x else y.
+
Definition ger :
simpl_rel R :=
[rel x y | y ≤ x].
+
Definition gtr :
simpl_rel R :=
[rel x y | y < x].
+
Definition lerif x y C :
Prop := (
(x ≤ y) × ((x == y) = C))%
type.
+
Definition sgr x :
R :=
if x == 0
then 0
else if x < 0
then -1
else 1.
+
Definition minr x y :
R :=
if x ≤ y then x else y.
+
Definition maxr x y :
R :=
if y ≤ x then x else y.
-
Definition Rpos :
qualifier 0
R :=
[qualify x : R | 0
< x].
-
Definition Rneg :
qualifier 0
R :=
[qualify x : R | x < 0
].
-
Definition Rnneg :
qualifier 0
R :=
[qualify x : R | 0
≤ x].
-
Definition Rreal :
qualifier 0
R :=
[qualify x : R | (0
≤ x) || (x ≤ 0
)].
+
Definition Rpos :
qualifier 0
R :=
[qualify x : R | 0
< x].
+
Definition Rneg :
qualifier 0
R :=
[qualify x : R | x < 0
].
+
Definition Rnneg :
qualifier 0
R :=
[qualify x : R | 0
≤ x].
+
Definition Rreal :
qualifier 0
R :=
[qualify x : R | (0
≤ x) || (x ≤ 0
)].
End Def.
End Def.
@@ -353,15 +365,15 @@
Module Keys.
Section Keys.
Variable R :
numDomainType.
-
Fact Rpos_key :
pred_key (@
pos R).
-
Definition Rpos_keyed :=
KeyedQualifier Rpos_key.
-
Fact Rneg_key :
pred_key (@
real R).
-
Definition Rneg_keyed :=
KeyedQualifier Rneg_key.
-
Fact Rnneg_key :
pred_key (@
nneg R).
-
Definition Rnneg_keyed :=
KeyedQualifier Rnneg_key.
-
Fact Rreal_key :
pred_key (@
real R).
-
Definition Rreal_keyed :=
KeyedQualifier Rreal_key.
-
Definition ler_of_leif x y C (
le_xy : @
lerif R x y C) :=
le_xy.1 : le x y.
+
Fact Rpos_key :
pred_key (@
pos R).
+
Definition Rpos_keyed :=
KeyedQualifier Rpos_key.
+
Fact Rneg_key :
pred_key (@
real R).
+
Definition Rneg_keyed :=
KeyedQualifier Rneg_key.
+
Fact Rnneg_key :
pred_key (@
nneg R).
+
Definition Rnneg_keyed :=
KeyedQualifier Rnneg_key.
+
Fact Rreal_key :
pred_key (@
real R).
+
Definition Rreal_keyed :=
KeyedQualifier Rreal_key.
+
Definition ler_of_leif x y C (
le_xy : @
lerif R x y C) :=
le_xy.1 : le x y.
End Keys.
End Keys.
@@ -375,48 +387,48 @@
Import Def Keys.
-
Notation "`| x |" := (
norm x) :
ring_scope.
+
Notation "`| x |" := (
norm x) :
ring_scope.
-
Notation "<%R" :=
lt :
ring_scope.
-
Notation ">%R" :=
gt :
ring_scope.
-
Notation "<=%R" :=
le :
ring_scope.
-
Notation ">=%R" :=
ge :
ring_scope.
-
Notation "<?=%R" :=
lerif :
ring_scope.
+
Notation "<%R" :=
lt :
ring_scope.
+
Notation ">%R" :=
gt :
ring_scope.
+
Notation "<=%R" :=
le :
ring_scope.
+
Notation ">=%R" :=
ge :
ring_scope.
+
Notation "<?=%R" :=
lerif :
ring_scope.
-
Notation "< y" := (
gt y) :
ring_scope.
-
Notation "< y :> T" := (
< (y : T)) :
ring_scope.
-
Notation "> y" := (
lt y) :
ring_scope.
-
Notation "> y :> T" := (
> (y : T)) :
ring_scope.
+
Notation "< y" := (
gt y) :
ring_scope.
+
Notation "< y :> T" := (
< (y : T)) :
ring_scope.
+
Notation "> y" := (
lt y) :
ring_scope.
+
Notation "> y :> T" := (
> (y : T)) :
ring_scope.
-
Notation "<= y" := (
ge y) :
ring_scope.
-
Notation "<= y :> T" := (
≤ (y : T)) :
ring_scope.
-
Notation ">= y" := (
le y) :
ring_scope.
-
Notation ">= y :> T" := (
≥ (y : T)) :
ring_scope.
+
Notation "<= y" := (
ge y) :
ring_scope.
+
Notation "<= y :> T" := (
≤ (y : T)) :
ring_scope.
+
Notation ">= y" := (
le y) :
ring_scope.
+
Notation ">= y :> T" := (
≥ (y : T)) :
ring_scope.
-
Notation "x < y" := (
lt x y) :
ring_scope.
-
Notation "x < y :> T" := (
(x : T) < (y : T)) :
ring_scope.
-
Notation "x > y" := (
y < x) (
only parsing) :
ring_scope.
-
Notation "x > y :> T" := (
(x : T) > (y : T)) (
only parsing) :
ring_scope.
+
Notation "x < y" := (
lt x y) :
ring_scope.
+
Notation "x < y :> T" := (
(x : T) < (y : T)) :
ring_scope.
+
Notation "x > y" := (
y < x) (
only parsing) :
ring_scope.
+
Notation "x > y :> T" := (
(x : T) > (y : T)) (
only parsing) :
ring_scope.
-
Notation "x <= y" := (
le x y) :
ring_scope.
-
Notation "x <= y :> T" := (
(x : T) ≤ (y : T)) :
ring_scope.
-
Notation "x >= y" := (
y ≤ x) (
only parsing) :
ring_scope.
-
Notation "x >= y :> T" := (
(x : T) ≥ (y : T)) (
only parsing) :
ring_scope.
+
Notation "x <= y" := (
le x y) :
ring_scope.
+
Notation "x <= y :> T" := (
(x : T) ≤ (y : T)) :
ring_scope.
+
Notation "x >= y" := (
y ≤ x) (
only parsing) :
ring_scope.
+
Notation "x >= y :> T" := (
(x : T) ≥ (y : T)) (
only parsing) :
ring_scope.
-
Notation "x <= y <= z" := (
(x ≤ y) && (y ≤ z)) :
ring_scope.
-
Notation "x < y <= z" := (
(x < y) && (y ≤ z)) :
ring_scope.
-
Notation "x <= y < z" := (
(x ≤ y) && (y < z)) :
ring_scope.
-
Notation "x < y < z" := (
(x < y) && (y < z)) :
ring_scope.
+
Notation "x <= y <= z" := (
(x ≤ y) && (y ≤ z)) :
ring_scope.
+
Notation "x < y <= z" := (
(x < y) && (y ≤ z)) :
ring_scope.
+
Notation "x <= y < z" := (
(x ≤ y) && (y < z)) :
ring_scope.
+
Notation "x < y < z" := (
(x < y) && (y < z)) :
ring_scope.
-
Notation "x <= y ?= 'iff' C" := (
lerif x y C) :
ring_scope.
-
Notation "x <= y ?= 'iff' C :> R" := (
(x : R) ≤ (y : R) ?= iff C)
+
Notation "x <= y ?= 'iff' C" := (
lerif x y C) :
ring_scope.
+
Notation "x <= y ?= 'iff' C :> R" := (
(x : R) ≤ (y : R) ?= iff C)
(
only parsing) :
ring_scope.
@@ -438,15 +450,15 @@
Variable R :
numDomainType.
-
Definition real_axiom :
Prop :=
∀ x :
R,
x \is real.
+
Definition real_axiom :
Prop :=
∀ x :
R,
x \is real.
-
Definition archimedean_axiom :
Prop :=
∀ x :
R,
∃ ub, `|x| < ub%:R.
+
Definition archimedean_axiom :
Prop :=
∀ x :
R,
∃ ub, `|x| < ub%:R.
Definition real_closed_axiom :
Prop :=
-
∀ (
p :
{poly R}) (
a b :
R),
-
a ≤ b → p.[a] ≤ 0
≤ p.[b] → exists2 x, a ≤ x ≤ b & root p x.
+
∀ (
p :
{poly R}) (
a b :
R),
+
a ≤ b → p.[a] ≤ 0
≤ p.[b] → exists2 x, a ≤ x ≤ b & root p x.
End ExtensionAxioms.
@@ -471,28 +483,30 @@
Definition base2 R (
c :
class_of R) :=
NumDomain.Class (
mixin c).
-
Structure type :=
Pack {
sort;
_ :
class_of sort;
_ :
Type}.
+
Structure type :=
Pack {
sort;
_ :
class_of sort}.
Variables (
T :
Type) (
cT :
type).
-
Definition class :=
let:
Pack _ c _ as cT' :=
cT return class_of cT' in c.
-
Let xT :=
let:
Pack T _ _ :=
cT in T.
-
Notation xclass := (
class : class_of xT).
+
Definition class :=
let:
Pack _ c as cT' :=
cT return class_of cT' in c.
+
Let xT :=
let:
Pack T _ :=
cT in T.
+
Notation xclass := (
class : class_of xT).
+
+
Definition pack :=
-
fun bT b &
phant_id (
GRing.Field.class bT) (
b : GRing.Field.class_of T) ⇒
-
fun mT m &
phant_id (
NumDomain.class mT) (@
NumDomain.Class T b m) ⇒
-
Pack (@
Class T b m)
T.
+
fun bT b &
phant_id (
GRing.Field.class bT) (
b : GRing.Field.class_of T) ⇒
+
fun mT m &
phant_id (
NumDomain.class mT) (@
NumDomain.Class T b m) ⇒
+
Pack (@
Class T b m).
-
Definition eqType := @
Equality.Pack cT xclass xT.
-
Definition choiceType := @
Choice.Pack cT xclass xT.
-
Definition zmodType := @
GRing.Zmodule.Pack cT xclass xT.
-
Definition ringType := @
GRing.Ring.Pack cT xclass xT.
-
Definition comRingType := @
GRing.ComRing.Pack cT xclass xT.
-
Definition unitRingType := @
GRing.UnitRing.Pack cT xclass xT.
-
Definition comUnitRingType := @
GRing.ComUnitRing.Pack cT xclass xT.
-
Definition idomainType := @
GRing.IntegralDomain.Pack cT xclass xT.
-
Definition numDomainType := @
NumDomain.Pack cT xclass xT.
-
Definition fieldType := @
GRing.Field.Pack cT xclass xT.
-
Definition join_numDomainType := @
NumDomain.Pack fieldType xclass xT.
+
Definition eqType := @
Equality.Pack cT xclass.
+
Definition choiceType := @
Choice.Pack cT xclass.
+
Definition zmodType := @
GRing.Zmodule.Pack cT xclass.
+
Definition ringType := @
GRing.Ring.Pack cT xclass.
+
Definition comRingType := @
GRing.ComRing.Pack cT xclass.
+
Definition unitRingType := @
GRing.UnitRing.Pack cT xclass.
+
Definition comUnitRingType := @
GRing.ComUnitRing.Pack cT xclass.
+
Definition idomainType := @
GRing.IntegralDomain.Pack cT xclass.
+
Definition numDomainType := @
NumDomain.Pack cT xclass.
+
Definition fieldType := @
GRing.Field.Pack cT xclass.
+
Definition join_numDomainType := @
NumDomain.Pack fieldType xclass.
End ClassDef.
@@ -522,8 +536,9 @@
Canonical numDomainType.
Coercion fieldType : type >-> GRing.Field.type.
Canonical fieldType.
+
Canonical join_numDomainType.
Notation numFieldType :=
type.
-
Notation "[ 'numFieldType' 'of' T ]" := (@
pack T _ _ id _ _ id)
+
Notation "[ 'numFieldType' 'of' T ]" := (@
pack T _ _ id _ _ id)
(
at level 0,
format "[ 'numFieldType' 'of' T ]") :
form_scope.
End Exports.
@@ -540,9 +555,9 @@
Record imaginary_mixin_of (
R :
numDomainType) :=
ImaginaryMixin {
imaginary :
R;
-
conj_op :
{rmorphism R → R};
-
_ :
imaginary ^+ 2
= - 1;
-
_ :
∀ x,
x × conj_op x = `|x| ^+ 2;
+
conj_op :
{rmorphism R → R};
+
_ :
imaginary ^+ 2
= - 1;
+
_ :
∀ x,
x × conj_op x = `|x| ^+ 2;
}.
@@ -554,36 +569,38 @@
Definition base2 R (
c :
class_of R) :=
NumField.Class (
mixin c).
-
Structure type :=
Pack {
sort;
_ :
class_of sort;
_ :
Type}.
+
Structure type :=
Pack {
sort;
_ :
class_of sort}.
Variables (
T :
Type) (
cT :
type).
-
Definition class :=
let:
Pack _ c _ as cT' :=
cT return class_of cT' in c.
-
Let xT :=
let:
Pack T _ _ :=
cT in T.
-
Notation xclass := (
class : class_of xT).
+
Definition class :=
let:
Pack _ c as cT' :=
cT return class_of cT' in c.
+
Let xT :=
let:
Pack T _ :=
cT in T.
+
Notation xclass := (
class : class_of xT).
+
+
Definition pack :=
-
fun bT b &
phant_id (
GRing.ClosedField.class bT)
- (
b : GRing.ClosedField.class_of T) ⇒
-
fun mT m &
phant_id (
NumField.class mT) (@
NumField.Class T b m) ⇒
-
fun mc ⇒
Pack (@
Class T b m mc)
T.
-
Definition clone :=
fun b &
phant_id class (
b : class_of T) ⇒
Pack b T.
-
-
-
Definition eqType := @
Equality.Pack cT xclass xT.
-
Definition choiceType := @
Choice.Pack cT xclass xT.
-
Definition zmodType := @
GRing.Zmodule.Pack cT xclass xT.
-
Definition ringType := @
GRing.Ring.Pack cT xclass xT.
-
Definition comRingType := @
GRing.ComRing.Pack cT xclass xT.
-
Definition unitRingType := @
GRing.UnitRing.Pack cT xclass xT.
-
Definition comUnitRingType := @
GRing.ComUnitRing.Pack cT xclass xT.
-
Definition idomainType := @
GRing.IntegralDomain.Pack cT xclass xT.
-
Definition numDomainType := @
NumDomain.Pack cT xclass xT.
-
Definition fieldType := @
GRing.Field.Pack cT xclass xT.
-
Definition numFieldType := @
NumField.Pack cT xclass xT.
-
Definition decFieldType := @
GRing.DecidableField.Pack cT xclass xT.
-
Definition closedFieldType := @
GRing.ClosedField.Pack cT xclass xT.
-
Definition join_dec_numDomainType := @
NumDomain.Pack decFieldType xclass xT.
-
Definition join_dec_numFieldType := @
NumField.Pack decFieldType xclass xT.
-
Definition join_numDomainType := @
NumDomain.Pack closedFieldType xclass xT.
-
Definition join_numFieldType := @
NumField.Pack closedFieldType xclass xT.
+
fun bT b &
phant_id (
GRing.ClosedField.class bT)
+ (
b : GRing.ClosedField.class_of T) ⇒
+
fun mT m &
phant_id (
NumField.class mT) (@
NumField.Class T b m) ⇒
+
fun mc ⇒
Pack (@
Class T b m mc).
+
Definition clone :=
fun b &
phant_id class (
b : class_of T) ⇒
Pack b.
+
+
+
Definition eqType := @
Equality.Pack cT xclass.
+
Definition choiceType := @
Choice.Pack cT xclass.
+
Definition zmodType := @
GRing.Zmodule.Pack cT xclass.
+
Definition ringType := @
GRing.Ring.Pack cT xclass.
+
Definition comRingType := @
GRing.ComRing.Pack cT xclass.
+
Definition unitRingType := @
GRing.UnitRing.Pack cT xclass.
+
Definition comUnitRingType := @
GRing.ComUnitRing.Pack cT xclass.
+
Definition idomainType := @
GRing.IntegralDomain.Pack cT xclass.
+
Definition numDomainType := @
NumDomain.Pack cT xclass.
+
Definition fieldType := @
GRing.Field.Pack cT xclass.
+
Definition numFieldType := @
NumField.Pack cT xclass.
+
Definition decFieldType := @
GRing.DecidableField.Pack cT xclass.
+
Definition closedFieldType := @
GRing.ClosedField.Pack cT xclass.
+
Definition join_dec_numDomainType := @
NumDomain.Pack decFieldType xclass.
+
Definition join_dec_numFieldType := @
NumField.Pack decFieldType xclass.
+
Definition join_numDomainType := @
NumDomain.Pack closedFieldType xclass.
+
Definition join_numFieldType := @
NumField.Pack closedFieldType xclass.
End ClassDef.
@@ -624,11 +641,11 @@
Canonical join_numDomainType.
Canonical join_numFieldType.
Notation numClosedFieldType :=
type.
-
Notation NumClosedFieldType T m := (@
pack T _ _ id _ _ id m).
-
Notation "[ 'numClosedFieldType' 'of' T 'for' cT ]" := (@
clone T cT _ id)
+
Notation NumClosedFieldType T m := (@
pack T _ _ id _ _ id m).
+
Notation "[ 'numClosedFieldType' 'of' T 'for' cT ]" := (@
clone T cT _ id)
(
at level 0,
format "[ 'numClosedFieldType' 'of' T 'for' cT ]") :
form_scope.
-
Notation "[ 'numClosedFieldType' 'of' T ]" := (@
clone T _ _ id)
+
Notation "[ 'numClosedFieldType' 'of' T ]" := (@
clone T _ _ id)
(
at level 0,
format "[ 'numClosedFieldType' 'of' T ]") :
form_scope.
End Exports.
@@ -647,26 +664,28 @@
Class {
base :
NumDomain.class_of R;
_ : @
real_axiom (
num_for R base)}.
-
Structure type :=
Pack {
sort;
_ :
class_of sort;
_ :
Type}.
+
Structure type :=
Pack {
sort;
_ :
class_of sort}.
Variables (
T :
Type) (
cT :
type).
-
Definition class :=
let:
Pack _ c _ as cT' :=
cT return class_of cT' in c.
-
Let xT :=
let:
Pack T _ _ :=
cT in T.
-
Notation xclass := (
class : class_of xT).
-
Definition clone c of phant_id class c := @
Pack T c T.
+
Definition class :=
let:
Pack _ c as cT' :=
cT return class_of cT' in c.
+
Let xT :=
let:
Pack T _ :=
cT in T.
+
Notation xclass := (
class : class_of xT).
+
+
+
Definition clone c of phant_id class c := @
Pack T c.
Definition pack b0 (
m0 :
real_axiom (
num_for T b0)) :=
-
fun bT b &
phant_id (
NumDomain.class bT)
b ⇒
-
fun m &
phant_id m0 m ⇒
Pack (@
Class T b m)
T.
+
fun bT b &
phant_id (
NumDomain.class bT)
b ⇒
+
fun m &
phant_id m0 m ⇒
Pack (@
Class T b m).
-
Definition eqType := @
Equality.Pack cT xclass xT.
-
Definition choiceType := @
Choice.Pack cT xclass xT.
-
Definition zmodType := @
GRing.Zmodule.Pack cT xclass xT.
-
Definition ringType := @
GRing.Ring.Pack cT xclass xT.
-
Definition comRingType := @
GRing.ComRing.Pack cT xclass xT.
-
Definition unitRingType := @
GRing.UnitRing.Pack cT xclass xT.
-
Definition comUnitRingType := @
GRing.ComUnitRing.Pack cT xclass xT.
-
Definition idomainType := @
GRing.IntegralDomain.Pack cT xclass xT.
-
Definition numDomainType := @
NumDomain.Pack cT xclass xT.
+
Definition eqType := @
Equality.Pack cT xclass.
+
Definition choiceType := @
Choice.Pack cT xclass.
+
Definition zmodType := @
GRing.Zmodule.Pack cT xclass.
+
Definition ringType := @
GRing.Ring.Pack cT xclass.
+
Definition comRingType := @
GRing.ComRing.Pack cT xclass.
+
Definition unitRingType := @
GRing.UnitRing.Pack cT xclass.
+
Definition comUnitRingType := @
GRing.ComUnitRing.Pack cT xclass.
+
Definition idomainType := @
GRing.IntegralDomain.Pack cT xclass.
+
Definition numDomainType := @
NumDomain.Pack cT xclass.
End ClassDef.
@@ -694,10 +713,10 @@
Coercion numDomainType : type >-> NumDomain.type.
Canonical numDomainType.
Notation realDomainType :=
type.
-
Notation RealDomainType T m := (@
pack T _ m _ _ id _ id).
-
Notation "[ 'realDomainType' 'of' T 'for' cT ]" := (@
clone T cT _ idfun)
+
Notation RealDomainType T m := (@
pack T _ m _ _ id _ id).
+
Notation "[ 'realDomainType' 'of' T 'for' cT ]" := (@
clone T cT _ idfun)
(
at level 0,
format "[ 'realDomainType' 'of' T 'for' cT ]") :
form_scope.
-
Notation "[ 'realDomainType' 'of' T ]" := (@
clone T _ _ id)
+
Notation "[ 'realDomainType' 'of' T ]" := (@
clone T _ _ id)
(
at level 0,
format "[ 'realDomainType' 'of' T ]") :
form_scope.
End Exports.
@@ -717,30 +736,33 @@
Definition base2 R (
c :
class_of R) :=
RealDomain.Class (@
mixin R c).
-
Structure type :=
Pack {
sort;
_ :
class_of sort;
_ :
Type}.
+
Structure type :=
Pack {
sort;
_ :
class_of sort}.
Variables (
T :
Type) (
cT :
type).
-
Definition class :=
let:
Pack _ c _ as cT' :=
cT return class_of cT' in c.
-
Let xT :=
let:
Pack T _ _ :=
cT in T.
-
Notation xclass := (
class : class_of xT).
+
Definition class :=
let:
Pack _ c as cT' :=
cT return class_of cT' in c.
+
Let xT :=
let:
Pack T _ :=
cT in T.
+
Notation xclass := (
class : class_of xT).
+
+
Definition pack :=
-
fun bT b &
phant_id (
NumField.class bT) (
b : NumField.class_of T) ⇒
-
fun mT m &
phant_id (
RealDomain.class mT) (@
RealDomain.Class T b m) ⇒
-
Pack (@
Class T b m)
T.
-
-
-
Definition eqType := @
Equality.Pack cT xclass xT.
-
Definition choiceType := @
Choice.Pack cT xclass xT.
-
Definition zmodType := @
GRing.Zmodule.Pack cT xclass xT.
-
Definition ringType := @
GRing.Ring.Pack cT xclass xT.
-
Definition comRingType := @
GRing.ComRing.Pack cT xclass xT.
-
Definition unitRingType := @
GRing.UnitRing.Pack cT xclass xT.
-
Definition comUnitRingType := @
GRing.ComUnitRing.Pack cT xclass xT.
-
Definition idomainType := @
GRing.IntegralDomain.Pack cT xclass xT.
-
Definition numDomainType := @
NumDomain.Pack cT xclass xT.
-
Definition realDomainType := @
RealDomain.Pack cT xclass xT.
-
Definition fieldType := @
GRing.Field.Pack cT xclass xT.
-
Definition numFieldType := @
NumField.Pack cT xclass xT.
-
Definition join_realDomainType := @
RealDomain.Pack numFieldType xclass xT.
+
fun bT b &
phant_id (
NumField.class bT) (
b : NumField.class_of T) ⇒
+
fun mT m &
phant_id (
RealDomain.class mT) (@
RealDomain.Class T b m) ⇒
+
Pack (@
Class T b m).
+
+
+
Definition eqType := @
Equality.Pack cT xclass.
+
Definition choiceType := @
Choice.Pack cT xclass.
+
Definition zmodType := @
GRing.Zmodule.Pack cT xclass.
+
Definition ringType := @
GRing.Ring.Pack cT xclass.
+
Definition comRingType := @
GRing.ComRing.Pack cT xclass.
+
Definition unitRingType := @
GRing.UnitRing.Pack cT xclass.
+
Definition comUnitRingType := @
GRing.ComUnitRing.Pack cT xclass.
+
Definition idomainType := @
GRing.IntegralDomain.Pack cT xclass.
+
Definition numDomainType := @
NumDomain.Pack cT xclass.
+
Definition realDomainType := @
RealDomain.Pack cT xclass.
+
Definition fieldType := @
GRing.Field.Pack cT xclass.
+
Definition numFieldType := @
NumField.Pack cT xclass.
+
Definition join_fieldType := @
GRing.Field.Pack realDomainType xclass.
+
Definition join_numFieldType := @
NumField.Pack realDomainType xclass.
End ClassDef.
@@ -774,9 +796,10 @@
Canonical fieldType.
Coercion numFieldType : type >-> NumField.type.
Canonical numFieldType.
-
Canonical join_realDomainType.
+
Canonical join_fieldType.
+
Canonical join_numFieldType.
Notation realFieldType :=
type.
-
Notation "[ 'realFieldType' 'of' T ]" := (@
pack T _ _ id _ _ id)
+
Notation "[ 'realFieldType' 'of' T ]" := (@
pack T _ _ id _ _ id)
(
at level 0,
format "[ 'realFieldType' 'of' T ]") :
form_scope.
End Exports.
@@ -795,30 +818,32 @@
Class {
base :
RealField.class_of R;
_ :
archimedean_axiom (
num_for R base) }.
-
Structure type :=
Pack {
sort;
_ :
class_of sort;
_ :
Type}.
+
Structure type :=
Pack {
sort;
_ :
class_of sort}.
Variables (
T :
Type) (
cT :
type).
-
Definition class :=
let:
Pack _ c _ as cT' :=
cT return class_of cT' in c.
-
Let xT :=
let:
Pack T _ _ :=
cT in T.
-
Notation xclass := (
class : class_of xT).
-
Definition clone c of phant_id class c := @
Pack T c T.
+
Definition class :=
let:
Pack _ c as cT' :=
cT return class_of cT' in c.
+
Let xT :=
let:
Pack T _ :=
cT in T.
+
Notation xclass := (
class : class_of xT).
+
+
+
Definition clone c of phant_id class c := @
Pack T c.
Definition pack b0 (
m0 :
archimedean_axiom (
num_for T b0)) :=
-
fun bT b &
phant_id (
RealField.class bT)
b ⇒
-
fun m &
phant_id m0 m ⇒
Pack (@
Class T b m)
T.
+
fun bT b &
phant_id (
RealField.class bT)
b ⇒
+
fun m &
phant_id m0 m ⇒
Pack (@
Class T b m).
-
Definition eqType := @
Equality.Pack cT xclass xT.
-
Definition choiceType := @
Choice.Pack cT xclass xT.
-
Definition zmodType := @
GRing.Zmodule.Pack cT xclass xT.
-
Definition ringType := @
GRing.Ring.Pack cT xclass xT.
-
Definition comRingType := @
GRing.ComRing.Pack cT xclass xT.
-
Definition unitRingType := @
GRing.UnitRing.Pack cT xclass xT.
-
Definition comUnitRingType := @
GRing.ComUnitRing.Pack cT xclass xT.
-
Definition idomainType := @
GRing.IntegralDomain.Pack cT xclass xT.
-
Definition numDomainType := @
NumDomain.Pack cT xclass xT.
-
Definition realDomainType := @
RealDomain.Pack cT xclass xT.
-
Definition fieldType := @
GRing.Field.Pack cT xclass xT.
-
Definition numFieldType := @
NumField.Pack cT xclass xT.
-
Definition realFieldType := @
RealField.Pack cT xclass xT.
+
Definition eqType := @
Equality.Pack cT xclass.
+
Definition choiceType := @
Choice.Pack cT xclass.
+
Definition zmodType := @
GRing.Zmodule.Pack cT xclass.
+
Definition ringType := @
GRing.Ring.Pack cT xclass.
+
Definition comRingType := @
GRing.ComRing.Pack cT xclass.
+
Definition unitRingType := @
GRing.UnitRing.Pack cT xclass.
+
Definition comUnitRingType := @
GRing.ComUnitRing.Pack cT xclass.
+
Definition idomainType := @
GRing.IntegralDomain.Pack cT xclass.
+
Definition numDomainType := @
NumDomain.Pack cT xclass.
+
Definition realDomainType := @
RealDomain.Pack cT xclass.
+
Definition fieldType := @
GRing.Field.Pack cT xclass.
+
Definition numFieldType := @
NumField.Pack cT xclass.
+
Definition realFieldType := @
RealField.Pack cT xclass.
End ClassDef.
@@ -854,10 +879,10 @@
Coercion realFieldType : type >-> RealField.type.
Canonical realFieldType.
Notation archiFieldType :=
type.
-
Notation ArchiFieldType T m := (@
pack T _ m _ _ id _ id).
-
Notation "[ 'archiFieldType' 'of' T 'for' cT ]" := (@
clone T cT _ idfun)
+
Notation ArchiFieldType T m := (@
pack T _ m _ _ id _ id).
+
Notation "[ 'archiFieldType' 'of' T 'for' cT ]" := (@
clone T cT _ idfun)
(
at level 0,
format "[ 'archiFieldType' 'of' T 'for' cT ]") :
form_scope.
-
Notation "[ 'archiFieldType' 'of' T ]" := (@
clone T _ _ id)
+
Notation "[ 'archiFieldType' 'of' T ]" := (@
clone T _ _ id)
(
at level 0,
format "[ 'archiFieldType' 'of' T ]") :
form_scope.
End Exports.
@@ -876,30 +901,32 @@
Class {
base :
RealField.class_of R;
_ :
real_closed_axiom (
num_for R base) }.
-
Structure type :=
Pack {
sort;
_ :
class_of sort;
_ :
Type}.
+
Structure type :=
Pack {
sort;
_ :
class_of sort}.
Variables (
T :
Type) (
cT :
type).
-
Definition class :=
let:
Pack _ c _ as cT' :=
cT return class_of cT' in c.
-
Let xT :=
let:
Pack T _ _ :=
cT in T.
-
Notation xclass := (
class : class_of xT).
-
Definition clone c of phant_id class c := @
Pack T c T.
+
Definition class :=
let:
Pack _ c as cT' :=
cT return class_of cT' in c.
+
Let xT :=
let:
Pack T _ :=
cT in T.
+
Notation xclass := (
class : class_of xT).
+
+
+
Definition clone c of phant_id class c := @
Pack T c.
Definition pack b0 (
m0 :
real_closed_axiom (
num_for T b0)) :=
-
fun bT b &
phant_id (
RealField.class bT)
b ⇒
-
fun m &
phant_id m0 m ⇒
Pack (@
Class T b m)
T.
+
fun bT b &
phant_id (
RealField.class bT)
b ⇒
+
fun m &
phant_id m0 m ⇒
Pack (@
Class T b m).
-
Definition eqType := @
Equality.Pack cT xclass xT.
-
Definition choiceType := @
Choice.Pack cT xclass xT.
-
Definition zmodType := @
GRing.Zmodule.Pack cT xclass xT.
-
Definition ringType := @
GRing.Ring.Pack cT xclass xT.
-
Definition comRingType := @
GRing.ComRing.Pack cT xclass xT.
-
Definition unitRingType := @
GRing.UnitRing.Pack cT xclass xT.
-
Definition comUnitRingType := @
GRing.ComUnitRing.Pack cT xclass xT.
-
Definition idomainType := @
GRing.IntegralDomain.Pack cT xclass xT.
-
Definition numDomainType := @
NumDomain.Pack cT xclass xT.
-
Definition realDomainType := @
RealDomain.Pack cT xclass xT.
-
Definition fieldType := @
GRing.Field.Pack cT xclass xT.
-
Definition numFieldType := @
NumField.Pack cT xclass xT.
-
Definition realFieldType := @
RealField.Pack cT xclass xT.
+
Definition eqType := @
Equality.Pack cT xclass.
+
Definition choiceType := @
Choice.Pack cT xclass.
+
Definition zmodType := @
GRing.Zmodule.Pack cT xclass.
+
Definition ringType := @
GRing.Ring.Pack cT xclass.
+
Definition comRingType := @
GRing.ComRing.Pack cT xclass.
+
Definition unitRingType := @
GRing.UnitRing.Pack cT xclass.
+
Definition comUnitRingType := @
GRing.ComUnitRing.Pack cT xclass.
+
Definition idomainType := @
GRing.IntegralDomain.Pack cT xclass.
+
Definition numDomainType := @
NumDomain.Pack cT xclass.
+
Definition realDomainType := @
RealDomain.Pack cT xclass.
+
Definition fieldType := @
GRing.Field.Pack cT xclass.
+
Definition numFieldType := @
NumField.Pack cT xclass.
+
Definition realFieldType := @
RealField.Pack cT xclass.
End ClassDef.
@@ -935,10 +962,10 @@
Coercion realFieldType : type >-> RealField.type.
Canonical realFieldType.
Notation rcfType :=
Num.RealClosedField.type.
-
Notation RcfType T m := (@
pack T _ m _ _ id _ id).
-
Notation "[ 'rcfType' 'of' T 'for' cT ]" := (@
clone T cT _ idfun)
+
Notation RcfType T m := (@
pack T _ m _ _ id _ id).
+
Notation "[ 'rcfType' 'of' T 'for' cT ]" := (@
clone T cT _ idfun)
(
at level 0,
format "[ 'rcfType' 'of' T 'for' cT ]") :
form_scope.
-
Notation "[ 'rcfType' 'of' T ]" := (@
clone T _ _ id)
+
Notation "[ 'rcfType' 'of' T ]" := (@
clone T _ _ id)
(
at level 0,
format "[ 'rcfType' 'of' T ]") :
form_scope.
End Exports.
@@ -970,25 +997,25 @@
@@ -999,34 +1026,34 @@
@@ -1037,9 +1064,9 @@
-
Lemma posrE x :
(x \is pos) = (0
< x).
-
Lemma nnegrE x :
(x \is nneg) = (0
≤ x).
-
Lemma realE x :
(x \is real) = (0
≤ x) || (x ≤ 0
).
+
Lemma posrE x :
(x \is pos) = (0
< x).
+
Lemma nnegrE x :
(x \is nneg) = (0
≤ x).
+
Lemma realE x :
(x \is real) = (0
≤ x) || (x ≤ 0
).
Fact pos_divr_closed :
divr_closed (@
pos R).
@@ -1079,7 +1106,7 @@
End Domain.
-
Lemma num_real (
R :
realDomainType) (
x :
R) :
x \is real.
+
Lemma num_real (
R :
realDomainType) (
x :
R) :
x \is real.
Fact archi_bound_subproof (
R :
archiFieldType) :
archimedean_axiom R.
@@ -1093,7 +1120,7 @@
Fact sqrtr_subproof (
x :
R) :
-
exists2 y, 0
≤ y & if 0
≤ x return bool then y ^+ 2
== x else y == 0.
+
exists2 y, 0
≤ y & (if 0
≤ x then y ^+ 2
== x else y == 0
) : bool.
End RealClosed.
@@ -1164,14 +1191,14 @@
@@ -1182,12 +1209,12 @@
@@ -1198,38 +1225,38 @@
@@ -1238,19 +1265,19 @@
Integer comparisons and characteristic 0.
@@ -1261,60 +1288,60 @@
@@ -1325,15 +1352,15 @@
@@ -1344,53 +1371,53 @@
-
Lemma ler_asym :
antisymmetric (
<=%R : rel R).
+
Lemma ler_asym :
antisymmetric (
<=%R : rel R).
-
Lemma eqr_le x y :
(x == y) = (x ≤ y ≤ x).
+
Lemma eqr_le x y :
(x == y) = (x ≤ y ≤ x).
-
Lemma ltr_trans :
transitive (@
ltr R).
+
Lemma ltr_trans :
transitive (@
ltr R).
-
Lemma ler_lt_trans y x z :
x ≤ y → y < z → x < z.
+
Lemma ler_lt_trans y x z :
x ≤ y → y < z → x < z.
-
Lemma ltr_le_trans y x z :
x < y → y ≤ z → x < z.
+
Lemma ltr_le_trans y x z :
x < y → y ≤ z → x < z.
-
Lemma ler_trans :
transitive (@
ler R).
+
Lemma ler_trans :
transitive (@
ler R).
-
Definition lter01 :=
(ler01, ltr01).
-
Definition lterr :=
(lerr, ltrr).
+
Definition lter01 :=
(ler01, ltr01).
+
Definition lterr :=
(lerr, ltrr).
-
Lemma addr_ge0 x y : 0
≤ x → 0
≤ y → 0
≤ x + y.
+
Lemma addr_ge0 x y : 0
≤ x → 0
≤ y → 0
≤ x + y.
-
Lemma lerifP x y C :
reflect (
x ≤ y ?= iff C) (
if C then x == y else x < y).
+
Lemma lerifP x y C :
reflect (
x ≤ y ?= iff C) (
if C then x == y else x < y).
-
Lemma ltr_asym x y :
x < y < x = false.
+
Lemma ltr_asym x y :
x < y < x = false.
-
Lemma ler_anti :
antisymmetric (@
ler R).
+
Lemma ler_anti :
antisymmetric (@
ler R).
-
Lemma ltr_le_asym x y :
x < y ≤ x = false.
+
Lemma ltr_le_asym x y :
x < y ≤ x = false.
-
Lemma ler_lt_asym x y :
x ≤ y < x = false.
+
Lemma ler_lt_asym x y :
x ≤ y < x = false.
-
Definition lter_anti :=
(=^~ eqr_le, ltr_asym, ltr_le_asym, ler_lt_asym).
+
Definition lter_anti :=
(=^~ eqr_le, ltr_asym, ltr_le_asym, ler_lt_asym).
-
Lemma ltr_geF x y :
x < y → (y ≤ x = false).
+
Lemma ltr_geF x y :
x < y → (y ≤ x = false).
-
Lemma ler_gtF x y :
x ≤ y → (y < x = false).
+
Lemma ler_gtF x y :
x ≤ y → (y < x = false).
Definition ltr_gtF x y hxy :=
ler_gtF (@
ltrW x y hxy).
@@ -1404,66 +1431,92 @@
-
Lemma normr_le0 x :
(`|x| ≤ 0
) = (x == 0
).
+
Lemma normr_le0 x :
(`|x| ≤ 0
) = (x == 0
).
-
Lemma normr_lt0 x :
`|x| < 0
= false.
+
Lemma normr_lt0 x :
`|x| < 0
= false.
-
Lemma normr_gt0 x :
(`|x| > 0
) = (x != 0
).
+
Lemma normr_gt0 x :
(`|x| > 0
) = (x != 0
).
-
Definition normrE x :=
(normr_id, normr0, normr1, normrN1, normr_ge0, normr_eq0,
-
normr_lt0, normr_le0, normr_gt0, normrN).
+
Definition normrE x :=
(normr_id, normr0, normr1, normrN1, normr_ge0, normr_eq0,
+
normr_lt0, normr_le0, normr_gt0, normrN).
End NumIntegralDomainTheory.
-
Hint Resolve @
ler01 @
ltr01 lerr ltrr ltrW ltr_eqF ltr0Sn ler0n normr_ge0.
+
Hint Resolve @
ler01 @
ltr01 lerr ltrr ltrW ltr_eqF ltr0Sn ler0n normr_ge0 :
core.
Section NumIntegralDomainMonotonyTheory.
Variables R R' :
numDomainType.
-
Implicit Types m n p :
nat.
+
Implicit Types m n p :
nat.
Implicit Types x y z :
R.
Implicit Types u v w :
R'.
+
+
+
+
+ This listing of "Let"s factor out the required premices for the
+ subsequent lemmas, putting them in the context so that "done" solves the
+ goals quickly
+
+
@@ -1472,37 +1525,38 @@
Lemma ltrW_homo_in :
-
{in D & D', {homo f : x y / x < y}} → {in D & D', {homo f : x y / x ≤ y}}.
-
+
{in D & D', {homo f : x y / x < y}} → {in D & D', {homo f : x y / x ≤ y}}.
+
Lemma ltrW_nhomo_in :
-
{in D & D', {homo f : x y /~ x < y}} → {in D & D', {homo f : x y /~ x ≤ y}}.
-
+
{in D & D', {homo f : x y /~ x < y}} → {in D & D', {homo f : x y /~ x ≤ y}}.
+
-
Lemma homo_inj_in_lt :
-
{in D & D', injective f} → {in D & D', {homo f : x y / x ≤ y}} →
-
{in D & D', {homo f : x y / x < y}}.
-
+
Lemma inj_homo_ltr_in :
+
{in D & D', injective f} → {in D & D', {homo f : x y / x ≤ y}} →
+
{in D & D', {homo f : x y / x < y}}.
+
-
Lemma nhomo_inj_in_lt :
-
{in D & D', injective f} → {in D & D', {homo f : x y /~ x ≤ y}} →
-
{in D & D', {homo f : x y /~ x < y}}.
-
+
Lemma inj_nhomo_ltr_in :
+
{in D & D', injective f} → {in D & D', {homo f : x y /~ x ≤ y}} →
+
{in D & D', {homo f : x y /~ x < y}}.
+
-
Lemma mono_inj_in :
{in D &, {mono f : x y / x ≤ y}} → {in D &, injective f}.
-
+
Lemma incr_inj_in :
{in D &, {mono f : x y / x ≤ y}} →
+
{in D &, injective f}.
+
-
Lemma nmono_inj_in :
-
{in D &, {mono f : x y /~ x ≤ y}} → {in D &, injective f}.
-
+
Lemma decr_inj_in :
+
{in D &, {mono f : x y /~ x ≤ y}} → {in D &, injective f}.
+
Lemma lerW_mono_in :
-
{in D &, {mono f : x y / x ≤ y}} → {in D &, {mono f : x y / x < y}}.
-
+
{in D &, {mono f : x y / x ≤ y}} → {in D &, {mono f : x y / x < y}}.
+
Lemma lerW_nmono_in :
-
{in D &, {mono f : x y /~ x ≤ y}} → {in D &, {mono f : x y /~ x < y}}.
-
+
{in D &, {mono f : x y /~ x ≤ y}} → {in D &, {mono f : x y /~ x < y}}.
+
End AcrossTypes.
@@ -1510,56 +1564,167 @@
Section NatToR.
-
Variable (
f :
nat → R).
+
Variables (
D D' :
{pred nat}) (
f :
nat → R).
-
Lemma ltn_ltrW_homo :
-
{homo f : m n / (
m < n)%
N >-> m < n} →
-
{homo f : m n / (
m ≤ n)%
N >-> m ≤ n}.
+
Lemma ltnrW_homo :
{homo f : m n / (
m < n)%
N >-> m < n} →
+
{homo f : m n / (
m ≤ n)%
N >-> m ≤ n}.
-
Lemma ltn_ltrW_nhomo :
-
{homo f : m n / (
n < m)%
N >-> m < n} →
-
{homo f : m n / (
n ≤ m)%
N >-> m ≤ n}.
+
Lemma ltnrW_nhomo :
{homo f : m n / (
n < m)%
N >-> m < n} →
+
{homo f : m n / (
n ≤ m)%
N >-> m ≤ n}.
-
Lemma homo_inj_ltn_lt :
-
injective f → {homo f : m n / (
m ≤ n)%
N >-> m ≤ n} →
-
{homo f : m n / (
m < n)%
N >-> m < n}.
-
+
Lemma inj_homo_ltnr :
injective f →
+
{homo f : m n / (
m ≤ n)%
N >-> m ≤ n} →
+
{homo f : m n / (
m < n)%
N >-> m < n}.
+
-
Lemma nhomo_inj_ltn_lt :
-
injective f → {homo f : m n / (
n ≤ m)%
N >-> m ≤ n} →
-
{homo f : m n / (
n < m)%
N >-> m < n}.
-
+
Lemma inj_nhomo_ltnr :
injective f →
+
{homo f : m n / (
n ≤ m)%
N >-> m ≤ n} →
+
{homo f : m n / (
n < m)%
N >-> m < n}.
+
-
Lemma leq_mono_inj :
{mono f : m n / (
m ≤ n)%
N >-> m ≤ n} → injective f.
+
Lemma incnr_inj :
{mono f : m n / (
m ≤ n)%
N >-> m ≤ n} → injective f.
-
Lemma leq_nmono_inj :
{mono f : m n / (
n ≤ m)%
N >-> m ≤ n} → injective f.
+
Lemma decnr_inj_inj :
{mono f : m n / (
n ≤ m)%
N >-> m ≤ n} → injective f.
-
Lemma leq_lerW_mono :
-
{mono f : m n / (
m ≤ n)%
N >-> m ≤ n} →
-
{mono f : m n / (
m < n)%
N >-> m < n}.
-
+
Lemma lenrW_mono :
{mono f : m n / (
m ≤ n)%
N >-> m ≤ n} →
+
{mono f : m n / (
m < n)%
N >-> m < n}.
+
-
Lemma leq_lerW_nmono :
-
{mono f : m n / (
n ≤ m)%
N >-> m ≤ n} →
-
{mono f : m n / (
n < m)%
N >-> m < n}.
+
Lemma lenrW_nmono :
{mono f : m n / (
n ≤ m)%
N >-> m ≤ n} →
+
{mono f : m n / (
n < m)%
N >-> m < n}.
+
+
+
Lemma lenr_mono :
{homo f : m n / (
m < n)%
N >-> m < n} →
+
{mono f : m n / (
m ≤ n)%
N >-> m ≤ n}.
+
+
+
Lemma lenr_nmono :
{homo f : m n / (
n < m)%
N >-> m < n} →
+
{mono f : m n / (
n ≤ m)%
N >-> m ≤ n}.
+
+
+
Lemma ltnrW_homo_in :
{in D & D', {homo f : m n / (
m < n)%
N >-> m < n}} →
+
{in D & D', {homo f : m n / (
m ≤ n)%
N >-> m ≤ n}}.
+
+
+
Lemma ltnrW_nhomo_in :
{in D & D', {homo f : m n / (
n < m)%
N >-> m < n}} →
+
{in D & D', {homo f : m n / (
n ≤ m)%
N >-> m ≤ n}}.
+
+
+
Lemma inj_homo_ltnr_in :
{in D & D', injective f} →
+
{in D & D', {homo f : m n / (
m ≤ n)%
N >-> m ≤ n}} →
+
{in D & D', {homo f : m n / (
m < n)%
N >-> m < n}}.
+
+
+
Lemma inj_nhomo_ltnr_in :
{in D & D', injective f} →
+
{in D & D', {homo f : m n / (
n ≤ m)%
N >-> m ≤ n}} →
+
{in D & D', {homo f : m n / (
n < m)%
N >-> m < n}}.
+
+
+
Lemma incnr_inj_in :
{in D &, {mono f : m n / (
m ≤ n)%
N >-> m ≤ n}} →
+
{in D &, injective f}.
+
+
+
Lemma decnr_inj_inj_in :
{in D &, {mono f : m n / (
n ≤ m)%
N >-> m ≤ n}} →
+
{in D &, injective f}.
+
+
+
Lemma lenrW_mono_in :
{in D &, {mono f : m n / (
m ≤ n)%
N >-> m ≤ n}} →
+
{in D &, {mono f : m n / (
m < n)%
N >-> m < n}}.
+
+
+
Lemma lenrW_nmono_in :
{in D &, {mono f : m n / (
n ≤ m)%
N >-> m ≤ n}} →
+
{in D &, {mono f : m n / (
n < m)%
N >-> m < n}}.
+
+
+
Lemma lenr_mono_in :
{in D &, {homo f : m n / (
m < n)%
N >-> m < n}} →
+
{in D &, {mono f : m n / (
m ≤ n)%
N >-> m ≤ n}}.
+
+
+
Lemma lenr_nmono_in :
{in D &, {homo f : m n / (
n < m)%
N >-> m < n}} →
+
{in D &, {mono f : m n / (
n ≤ m)%
N >-> m ≤ n}}.
+
+
+
End NatToR.
-
Lemma homo_leq_mono :
-
{homo f : m n / (
m < n)%
N >-> m < n} →
-
{mono f : m n / (
m ≤ n)%
N >-> m ≤ n}.
+
Section RToNat.
-
Lemma nhomo_leq_mono :
-
{homo f : m n / (
n < m)%
N >-> m < n} →
-
{mono f : m n / (
n ≤ m)%
N >-> m ≤ n}.
+
Variables (
D D' :
{pred R}) (
f :
R → nat).
-
End NatToR.
+
Lemma ltrnW_homo :
{homo f : m n / m < n >-> (
m < n)%
N} →
+
{homo f : m n / m ≤ n >-> (
m ≤ n)%
N}.
+
+
+
Lemma ltrnW_nhomo :
{homo f : m n / n < m >-> (
m < n)%
N} →
+
{homo f : m n / n ≤ m >-> (
m ≤ n)%
N}.
+
+
+
Lemma inj_homo_ltrn :
injective f →
+
{homo f : m n / m ≤ n >-> (
m ≤ n)%
N} →
+
{homo f : m n / m < n >-> (
m < n)%
N}.
+
+
+
Lemma inj_nhomo_ltrn :
injective f →
+
{homo f : m n / n ≤ m >-> (
m ≤ n)%
N} →
+
{homo f : m n / n < m >-> (
m < n)%
N}.
+
+
+
Lemma incrn_inj :
{mono f : m n / m ≤ n >-> (
m ≤ n)%
N} → injective f.
+
+
+
Lemma decrn_inj :
{mono f : m n / n ≤ m >-> (
m ≤ n)%
N} → injective f.
+
+
+
Lemma lernW_mono :
{mono f : m n / m ≤ n >-> (
m ≤ n)%
N} →
+
{mono f : m n / m < n >-> (
m < n)%
N}.
+
+
+
Lemma lernW_nmono :
{mono f : m n / n ≤ m >-> (
m ≤ n)%
N} →
+
{mono f : m n / n < m >-> (
m < n)%
N}.
+
+
+
Lemma ltrnW_homo_in :
{in D & D', {homo f : m n / m < n >-> (
m < n)%
N}} →
+
{in D & D', {homo f : m n / m ≤ n >-> (
m ≤ n)%
N}}.
+
+
+
Lemma ltrnW_nhomo_in :
{in D & D', {homo f : m n / n < m >-> (
m < n)%
N}} →
+
{in D & D', {homo f : m n / n ≤ m >-> (
m ≤ n)%
N}}.
+
+
+
Lemma inj_homo_ltrn_in :
{in D & D', injective f} →
+
{in D & D', {homo f : m n / m ≤ n >-> (
m ≤ n)%
N}} →
+
{in D & D', {homo f : m n / m < n >-> (
m < n)%
N}}.
+
+
+
Lemma inj_nhomo_ltrn_in :
{in D & D', injective f} →
+
{in D & D', {homo f : m n / n ≤ m >-> (
m ≤ n)%
N}} →
+
{in D & D', {homo f : m n / n < m >-> (
m < n)%
N}}.
+
+
+
Lemma incrn_inj_in :
{in D &, {mono f : m n / m ≤ n >-> (
m ≤ n)%
N}} →
+
{in D &, injective f}.
+
+
+
Lemma decrn_inj_in :
{in D &, {mono f : m n / n ≤ m >-> (
m ≤ n)%
N}} →
+
{in D &, injective f}.
+
+
+
Lemma lernW_mono_in :
{in D &, {mono f : m n / m ≤ n >-> (
m ≤ n)%
N}} →
+
{in D &, {mono f : m n / m < n >-> (
m < n)%
N}}.
+
+
+
Lemma lernW_nmono_in :
{in D &, {mono f : m n / n ≤ m >-> (
m ≤ n)%
N}} →
+
{in D &, {mono f : m n / n < m >-> (
m < n)%
N}}.
+
+
+
End RToNat.
End NumIntegralDomainMonotonyTheory.
@@ -1580,63 +1745,63 @@
-
Lemma ler_opp2 :
{mono -%R : x y /~ x ≤ y :> R}.
-
Hint Resolve ler_opp2.
-
Lemma ltr_opp2 :
{mono -%R : x y /~ x < y :> R}.
-
Hint Resolve ltr_opp2.
-
Definition lter_opp2 :=
(ler_opp2, ltr_opp2).
+
Lemma ler_opp2 :
{mono -%R : x y /~ x ≤ y :> R}.
+
Hint Resolve ler_opp2 :
core.
+
Lemma ltr_opp2 :
{mono -%R : x y /~ x < y :> R}.
+
Hint Resolve ltr_opp2 :
core.
+
Definition lter_opp2 :=
(ler_opp2, ltr_opp2).
-
Lemma ler_oppr x y :
(x ≤ - y) = (y ≤ - x).
+
Lemma ler_oppr x y :
(x ≤ - y) = (y ≤ - x).
-
Lemma ltr_oppr x y :
(x < - y) = (y < - x).
+
Lemma ltr_oppr x y :
(x < - y) = (y < - x).
-
Definition lter_oppr :=
(ler_oppr, ltr_oppr).
+
Definition lter_oppr :=
(ler_oppr, ltr_oppr).
-
Lemma ler_oppl x y :
(- x ≤ y) = (- y ≤ x).
+
Lemma ler_oppl x y :
(- x ≤ y) = (- y ≤ x).
-
Lemma ltr_oppl x y :
(- x < y) = (- y < x).
+
Lemma ltr_oppl x y :
(- x < y) = (- y < x).
-
Definition lter_oppl :=
(ler_oppl, ltr_oppl).
+
Definition lter_oppl :=
(ler_oppl, ltr_oppl).
-
Lemma oppr_ge0 x :
(0
≤ - x) = (x ≤ 0
).
+
Lemma oppr_ge0 x :
(0
≤ - x) = (x ≤ 0
).
-
Lemma oppr_gt0 x :
(0
< - x) = (x < 0
).
+
Lemma oppr_gt0 x :
(0
< - x) = (x < 0
).
-
Definition oppr_gte0 :=
(oppr_ge0, oppr_gt0).
+
Definition oppr_gte0 :=
(oppr_ge0, oppr_gt0).
-
Lemma oppr_le0 x :
(- x ≤ 0
) = (0
≤ x).
+
Lemma oppr_le0 x :
(- x ≤ 0
) = (0
≤ x).
-
Lemma oppr_lt0 x :
(- x < 0
) = (0
< x).
+
Lemma oppr_lt0 x :
(- x < 0
) = (0
< x).
-
Definition oppr_lte0 :=
(oppr_le0, oppr_lt0).
-
Definition oppr_cp0 :=
(oppr_gte0, oppr_lte0).
-
Definition lter_oppE :=
(oppr_cp0, lter_opp2).
+
Definition oppr_lte0 :=
(oppr_le0, oppr_lt0).
+
Definition oppr_cp0 :=
(oppr_gte0, oppr_lte0).
+
Definition lter_oppE :=
(oppr_cp0, lter_opp2).
-
Lemma ge0_cp x : 0
≤ x → (- x ≤ 0
) × (- x ≤ x).
+
Lemma ge0_cp x : 0
≤ x → (- x ≤ 0
) × (- x ≤ x).
-
Lemma gt0_cp x : 0
< x →
-
(0
≤ x) × (- x ≤ 0
) × (- x ≤ x) × (- x < 0
) × (- x < x).
+
Lemma gt0_cp x : 0
< x →
+
(0
≤ x) × (- x ≤ 0
) × (- x ≤ x) × (- x < 0
) × (- x < x).
-
Lemma le0_cp x :
x ≤ 0
→ (0
≤ - x) × (x ≤ - x).
+
Lemma le0_cp x :
x ≤ 0
→ (0
≤ - x) × (x ≤ - x).
Lemma lt0_cp x :
-
x < 0
→ (x ≤ 0
) × (0
≤ - x) × (x ≤ - x) × (0
< - x) × (x < - x).
+
x < 0
→ (x ≤ 0
) × (0
≤ - x) × (x ≤ - x) × (0
< - x) × (x < - x).
@@ -1647,39 +1812,39 @@
@@ -1688,10 +1853,10 @@
:TODO: add a rpredBC in ssralg
@@ -1702,105 +1867,105 @@
-
CoInductive ler_xor_gt (
x y :
R) :
R → R → bool → bool → Set :=
- |
LerNotGt of x ≤ y :
ler_xor_gt x y (
y - x) (
y - x)
true false
- |
GtrNotLe of y < x :
ler_xor_gt x y (
x - y) (
x - y)
false true.
+
Variant ler_xor_gt (
x y :
R) :
R → R → bool → bool → Set :=
+ |
LerNotGt of x ≤ y :
ler_xor_gt x y (
y - x) (
y - x)
true false
+ |
GtrNotLe of y < x :
ler_xor_gt x y (
x - y) (
x - y)
false true.
-
CoInductive ltr_xor_ge (
x y :
R) :
R → R → bool → bool → Set :=
- |
LtrNotGe of x < y :
ltr_xor_ge x y (
y - x) (
y - x)
false true
- |
GerNotLt of y ≤ x :
ltr_xor_ge x y (
x - y) (
x - y)
true false.
+
Variant ltr_xor_ge (
x y :
R) :
R → R → bool → bool → Set :=
+ |
LtrNotGe of x < y :
ltr_xor_ge x y (
y - x) (
y - x)
false true
+ |
GerNotLt of y ≤ x :
ltr_xor_ge x y (
x - y) (
x - y)
true false.
-
CoInductive comparer x y :
R → R →
-
bool → bool → bool → bool → bool → bool → Set :=
- |
ComparerLt of x < y :
comparer x y (
y - x) (
y - x)
-
false false true false true false
- |
ComparerGt of x > y :
comparer x y (
x - y) (
x - y)
-
false false false true false true
- |
ComparerEq of x = y :
comparer x y 0 0
-
true true true true false false.
+
Variant comparer x y :
R → R →
+
bool → bool → bool → bool → bool → bool → Set :=
+ |
ComparerLt of x < y :
comparer x y (
y - x) (
y - x)
+
false false true false true false
+ |
ComparerGt of x > y :
comparer x y (
x - y) (
x - y)
+
false false false true false true
+ |
ComparerEq of x = y :
comparer x y 0 0
+
true true true true false false.
Lemma real_lerP x y :
-
x \is real → y \is real →
-
ler_xor_gt x y `|x - y| `|y - x| (
x ≤ y) (
y < x).
+
x \is real → y \is real →
+
ler_xor_gt x y `|x - y| `|y - x| (
x ≤ y) (
y < x).
Lemma real_ltrP x y :
-
x \is real → y \is real →
-
ltr_xor_ge x y `|x - y| `|y - x| (
y ≤ x) (
x < y).
+
x \is real → y \is real →
+
ltr_xor_ge x y `|x - y| `|y - x| (
y ≤ x) (
x < y).
-
Lemma real_ltrNge :
{in real &, ∀ x y,
(x < y) = ~~ (y ≤ x)}.
+
Lemma real_ltrNge :
{in real &, ∀ x y,
(x < y) = ~~ (y ≤ x)}.
-
Lemma real_lerNgt :
{in real &, ∀ x y,
(x ≤ y) = ~~ (y < x)}.
+
Lemma real_lerNgt :
{in real &, ∀ x y,
(x ≤ y) = ~~ (y < x)}.
Lemma real_ltrgtP x y :
-
x \is real → y \is real →
-
comparer x y `|x - y| `|y - x|
- (
y == x) (
x == y) (
x ≤ y) (
y ≤ x) (
x < y) (
x > y).
+
x \is real → y \is real →
+
comparer x y `|x - y| `|y - x|
+ (
y == x) (
x == y) (
x ≤ y) (
y ≤ x) (
x < y) (
x > y).
-
CoInductive ger0_xor_lt0 (
x :
R) :
R → bool → bool → Set :=
- |
Ger0NotLt0 of 0
≤ x :
ger0_xor_lt0 x x false true
- |
Ltr0NotGe0 of x < 0 :
ger0_xor_lt0 x (
- x)
true false.
+
Variant ger0_xor_lt0 (
x :
R) :
R → bool → bool → Set :=
+ |
Ger0NotLt0 of 0
≤ x :
ger0_xor_lt0 x x false true
+ |
Ltr0NotGe0 of x < 0 :
ger0_xor_lt0 x (
- x)
true false.
-
CoInductive ler0_xor_gt0 (
x :
R) :
R → bool → bool → Set :=
- |
Ler0NotLe0 of x ≤ 0 :
ler0_xor_gt0 x (
- x)
false true
- |
Gtr0NotGt0 of 0
< x :
ler0_xor_gt0 x x true false.
+
Variant ler0_xor_gt0 (
x :
R) :
R → bool → bool → Set :=
+ |
Ler0NotLe0 of x ≤ 0 :
ler0_xor_gt0 x (
- x)
false true
+ |
Gtr0NotGt0 of 0
< x :
ler0_xor_gt0 x x true false.
-
CoInductive comparer0 x :
-
R → bool → bool → bool → bool → bool → bool → Set :=
- |
ComparerGt0 of 0
< x :
comparer0 x x false false false true false true
- |
ComparerLt0 of x < 0 :
comparer0 x (
- x)
false false true false true false
- |
ComparerEq0 of x = 0 :
comparer0 x 0
true true true true false false.
+
Variant comparer0 x :
+
R → bool → bool → bool → bool → bool → bool → Set :=
+ |
ComparerGt0 of 0
< x :
comparer0 x x false false false true false true
+ |
ComparerLt0 of x < 0 :
comparer0 x (
- x)
false false true false true false
+ |
ComparerEq0 of x = 0 :
comparer0 x 0
true true true true false false.
-
Lemma real_ger0P x :
x \is real → ger0_xor_lt0 x `|x| (
x < 0) (0
≤ x).
+
Lemma real_ger0P x :
x \is real → ger0_xor_lt0 x `|x| (
x < 0) (0
≤ x).
-
Lemma real_ler0P x :
x \is real → ler0_xor_gt0 x `|x| (0
< x) (
x ≤ 0).
+
Lemma real_ler0P x :
x \is real → ler0_xor_gt0 x `|x| (0
< x) (
x ≤ 0).
Lemma real_ltrgt0P x :
-
x \is real →
-
comparer0 x `|x| (0
== x) (
x == 0) (
x ≤ 0) (0
≤ x) (
x < 0) (
x > 0).
+
x \is real →
+
comparer0 x `|x| (0
== x) (
x == 0) (
x ≤ 0) (0
≤ x) (
x < 0) (
x > 0).
-
Lemma real_neqr_lt :
{in real &, ∀ x y,
(x != y) = (x < y) || (y < x)}.
+
Lemma real_neqr_lt :
{in real &, ∀ x y,
(x != y) = (x < y) || (y < x)}.
-
Lemma ler_sub_real x y :
x ≤ y → y - x \is real.
+
Lemma ler_sub_real x y :
x ≤ y → y - x \is real.
-
Lemma ger_sub_real x y :
x ≤ y → x - y \is real.
+
Lemma ger_sub_real x y :
x ≤ y → x - y \is real.
-
Lemma ler_real y x :
x ≤ y → (x \is real) = (y \is real).
+
Lemma ler_real y x :
x ≤ y → (x \is real) = (y \is real).
-
Lemma ger_real x y :
y ≤ x → (x \is real) = (y \is real).
+
Lemma ger_real x y :
y ≤ x → (x \is real) = (y \is real).
-
Lemma ger1_real x : 1
≤ x → x \is real.
-
Lemma ler1_real x :
x ≤ 1
→ x \is real.
+
Lemma ger1_real x : 1
≤ x → x \is real.
+
Lemma ler1_real x :
x ≤ 1
→ x \is real.
-
Lemma Nreal_leF x y :
y \is real → x \notin real → (x ≤ y) = false.
+
Lemma Nreal_leF x y :
y \is real → x \notin real → (x ≤ y) = false.
-
Lemma Nreal_geF x y :
y \is real → x \notin real → (y ≤ x) = false.
+
Lemma Nreal_geF x y :
y \is real → x \notin real → (y ≤ x) = false.
-
Lemma Nreal_ltF x y :
y \is real → x \notin real → (x < y) = false.
+
Lemma Nreal_ltF x y :
y \is real → x \notin real → (x < y) = false.
-
Lemma Nreal_gtF x y :
y \is real → x \notin real → (y < x) = false.
+
Lemma Nreal_gtF x y :
y \is real → x \notin real → (y < x) = false.
@@ -1812,14 +1977,14 @@
Lemma real_wlog_ler P :
-
(∀ a b,
P b a → P a b) → (∀ a b,
a ≤ b → P a b) →
-
∀ a b :
R,
a \is real → b \is real → P a b.
+
(∀ a b,
P b a → P a b) → (∀ a b,
a ≤ b → P a b) →
+
∀ a b :
R,
a \is real → b \is real → P a b.
Lemma real_wlog_ltr P :
-
(∀ a,
P a a) → (∀ a b, (
P b a → P a b)
) →
-
(∀ a b,
a < b → P a b) →
-
∀ a b :
R,
a \is real → b \is real → P a b.
+
(∀ a,
P a a) → (∀ a b, (
P b a → P a b)
) →
+
(∀ a b,
a < b → P a b) →
+
∀ a b :
R,
a \is real → b \is real → P a b.
@@ -1828,21 +1993,21 @@
Monotony of addition
- GG: Domain should precede condition.
-
-
- These lemma are all combinations of mono(LR|RL) with ler [pn]mul2[rl].
+ These lemma are all combinations of mono(LR|RL) with ler [pn]mul2[rl].
-
Lemma mulr_sign_norm x :
(-1
) ^+ (
x < 0)%
R × `|x| = x.
+
Lemma mulr_sign_norm x :
(-1
) ^+ (
x < 0)%
R × `|x| = x.
-
Lemma mulr_Nsign_norm x :
(-1
) ^+ (0
< x)%
R × `|x| = - x.
+
Lemma mulr_Nsign_norm x :
(-1
) ^+ (0
< x)%
R × `|x| = - x.
-
Lemma numEsign x :
x = (-1
) ^+ (
x < 0)%
R × `|x|.
+
Lemma numEsign x :
x = (-1
) ^+ (
x < 0)%
R × `|x|.
-
Lemma numNEsign x :
-x = (-1
) ^+ (0
< x)%
R × `|x|.
+
Lemma numNEsign x :
-x = (-1
) ^+ (0
< x)%
R × `|x|.
-
Lemma normrEsign x :
`|x| = (-1
) ^+ (
x < 0)%
R × x.
+
Lemma normrEsign x :
`|x| = (-1
) ^+ (
x < 0)%
R × x.
End RealDomainTheory.
-
Hint Resolve num_real.
+
Hint Resolve num_real :
core.
Section RealDomainMonotony.
-
Variables (
R :
realDomainType) (
R' :
numDomainType) (
D :
pred R) (
f :
R → R').
-
Implicit Types (
m n p :
nat) (
x y z :
R) (
u v w :
R').
+
Variables (
R :
realDomainType) (
R' :
numDomainType) (
D :
pred R).
+
Variables (
f :
R → R') (
f' :
R → nat).
+
Implicit Types (
m n p :
nat) (
x y z :
R) (
u v w :
R').
-
Hint Resolve (@
num_real R).
+
Hint Resolve (@
num_real R) :
core.
-
Lemma homo_mono :
{homo f : x y / x < y} → {mono f : x y / x ≤ y}.
+
Lemma ler_mono :
{homo f : x y / x < y} → {mono f : x y / x ≤ y}.
-
Lemma nhomo_mono :
{homo f : x y /~ x < y} → {mono f : x y /~ x ≤ y}.
+
Lemma ler_nmono :
{homo f : x y /~ x < y} → {mono f : x y /~ x ≤ y}.
-
Lemma homo_mono_in :
-
{in D &, {homo f : x y / x < y}} → {in D &, {mono f : x y / x ≤ y}}.
+
Lemma ler_mono_in :
+
{in D &, {homo f : x y / x < y}} → {in D &, {mono f : x y / x ≤ y}}.
-
Lemma nhomo_mono_in :
-
{in D &, {homo f : x y /~ x < y}} → {in D &, {mono f : x y /~ x ≤ y}}.
+
Lemma ler_nmono_in :
+
{in D &, {homo f : x y /~ x < y}} → {in D &, {mono f : x y /~ x ≤ y}}.
+
+
+
Lemma lern_mono :
{homo f' : m n / m < n >-> (
m < n)%
N} →
+
{mono f' : m n / m ≤ n >-> (
m ≤ n)%
N}.
+
+
+
Lemma lern_nmono :
{homo f' : m n / n < m >-> (
m < n)%
N} →
+
{mono f' : m n / n ≤ m >-> (
m ≤ n)%
N}.
+
+
+
Lemma lern_mono_in :
{in D &, {homo f' : m n / m < n >-> (
m < n)%
N}} →
+
{in D &, {mono f' : m n / m ≤ n >-> (
m ≤ n)%
N}}.
+
+
+
Lemma lern_nmono_in :
{in D &, {homo f' : m n / n < m >-> (
m < n)%
N}} →
+
{in D &, {mono f' : m n / n ≤ m >-> (
m ≤ n)%
N}}.
End RealDomainMonotony.
+
+
Section RealDomainArgExtremum.
+
+
+
Context {
R :
realDomainType} {
I :
finType} (
i0 :
I).
+
Context (
P :
pred I) (
F :
I → R) (
Pi0 :
P i0).
+
+
+
Definition arg_minr :=
extremum <=%R i0 P F.
+
Definition arg_maxr :=
extremum >=%R i0 P F.
+
+
+
Lemma arg_minrP:
extremum_spec <=%R P F arg_minr.
+
+
+
Lemma arg_maxrP:
extremum_spec >=%R P F arg_maxr.
+
+
+
End RealDomainArgExtremum.
+
+
+
Notation "[ 'arg' 'minr_' ( i < i0 | P ) F ]" :=
+ (
arg_minr i0 (
fun i ⇒
P%
B) (
fun i ⇒
F))
+ (
at level 0,
i,
i0 at level 10,
+
format "[ 'arg' 'minr_' ( i < i0 | P ) F ]") :
form_scope.
+
+
+
Notation "[ 'arg' 'minr_' ( i < i0 'in' A ) F ]" :=
+
[arg minr_(i < i0 | i \in A) F]
+ (
at level 0,
i,
i0 at level 10,
+
format "[ 'arg' 'minr_' ( i < i0 'in' A ) F ]") :
form_scope.
+
+
+
Notation "[ 'arg' 'minr_' ( i < i0 ) F ]" :=
[arg minr_(i < i0 | true) F]
+ (
at level 0,
i,
i0 at level 10,
+
format "[ 'arg' 'minr_' ( i < i0 ) F ]") :
form_scope.
+
+
+
Notation "[ 'arg' 'maxr_' ( i > i0 | P ) F ]" :=
+ (
arg_maxr i0 (
fun i ⇒
P%
B) (
fun i ⇒
F))
+ (
at level 0,
i,
i0 at level 10,
+
format "[ 'arg' 'maxr_' ( i > i0 | P ) F ]") :
form_scope.
+
+
+
Notation "[ 'arg' 'maxr_' ( i > i0 'in' A ) F ]" :=
+
[arg maxr_(i > i0 | i \in A) F]
+ (
at level 0,
i,
i0 at level 10,
+
format "[ 'arg' 'maxr_' ( i > i0 'in' A ) F ]") :
form_scope.
+
+
+
Notation "[ 'arg' 'maxr_' ( i > i0 ) F ]" :=
[arg maxr_(i > i0 | true) F]
+ (
at level 0,
i,
i0 at level 10,
+
format "[ 'arg' 'maxr_' ( i > i0 ) F ]") :
form_scope.
+
Section RealDomainOperations.
@@ -3591,35 +3837,35 @@
Variable R :
realDomainType.
Implicit Types x y z t :
R.
-
Hint Resolve (@
num_real R).
+
Hint Resolve (@
num_real R) :
core.
Lemma sgr_cp0 x :
-
((sg x == 1
) = (0
< x)) ×
-
((sg x == -1
) = (x < 0
)) ×
-
((sg x == 0
) = (x == 0
)).
+
((sg x == 1
) = (0
< x)) ×
+
((sg x == -1
) = (x < 0
)) ×
+
((sg x == 0
) = (x == 0
)).
-
CoInductive sgr_val x :
R → bool → bool → bool → bool → bool → bool
-
→ bool → bool → bool → bool → bool → bool → R → Set :=
- |
SgrNull of x = 0 :
sgr_val x 0
true true true true false false
-
true false false true false false 0
- |
SgrPos of x > 0 :
sgr_val x x false false true false false true
-
false false true false false true 1
- |
SgrNeg of x < 0 :
sgr_val x (
- x)
false true false false true false
-
false true false false true false (-1).
+
Variant sgr_val x :
R → bool → bool → bool → bool → bool → bool
+
→ bool → bool → bool → bool → bool → bool → R → Set :=
+ |
SgrNull of x = 0 :
sgr_val x 0
true true true true false false
+
true false false true false false 0
+ |
SgrPos of x > 0 :
sgr_val x x false false true false false true
+
false false true false false true 1
+ |
SgrNeg of x < 0 :
sgr_val x (
- x)
false true false false true false
+
false true false false true false (-1).
Lemma sgrP x :
-
sgr_val x `|x| (0
== x) (
x ≤ 0) (0
≤ x) (
x == 0) (
x < 0) (0
< x)
- (0
== sg x) (-1
== sg x) (1
== sg x)
- (
sg x == 0) (
sg x == -1) (
sg x == 1) (
sg x).
+
sgr_val x `|x| (0
== x) (
x ≤ 0) (0
≤ x) (
x == 0) (
x < 0) (0
< x)
+ (0
== sg x) (-1
== sg x) (1
== sg x)
+ (
sg x == 0) (
sg x == -1) (
sg x == 1) (
sg x).
-
Lemma normrEsg x :
`|x| = sg x × x.
+
Lemma normrEsg x :
`|x| = sg x × x.
-
Lemma numEsg x :
x = sg x × `|x|.
+
Lemma numEsg x :
x = sg x × `|x|.
@@ -3628,25 +3874,25 @@
GG: duplicate!