Replace signed by itv

CHANGELOG_UNRELEASED.md

@@ -4,14 +4,63 @@
 
 ### Added
 
+- in `mathcomp_extra.v`
+  + lemmas `comparable_BSide_min`, `BSide_min`, `BSide_max`,
+    `real_BSide_min`, `real_BSide_max`, `natr_min`, `natr_max`,
+    `comparable_min_le_min`, `comparable_max`, `min_le_min`,
+    `max_le_max` and `real_sqrtC`
+
+- in `itv.v`
+  + lemmas `cmp0`, `neq0`, `eq0F`
+  + definitions `ItvReal` and `Itv01`
+  + lemmas `cmp0`, `neq0`, `eq0F`, `num_min`, `num_max`
+  + notation `%:num`
+  + notations `{posnum R}`, `{nonneg R}`, `%:pos`, `%:nng`,
+    `%:posnum`, `%:nngnum`, `[gt0 of _]`, `[lt0 of _]`, `[ge0 of _]`,
+    `[le0 of _]`, `[cmp0 of _]`, `[neq0 of _]`
+  + definitions `PosNum` and `NngNum`
+
+- in `constructive_ereal.v`
+  + lemmas `cmp0y`, `cmp0Ny`, `real_miney`, `real_minNye`,
+    `real_maxey`, `real_maxNye`, `oppe_cmp0`, `real_fine`,
+    `real_muleN`, `real_mulNe`, `real_muleNN`
+
 ### Changed
 
+- in `itv.v`
+  + definition `ItvNum`
+
 ### Renamed
 
+- in `itv.v`
+  + `itv_bottom` -> `bottom`
+  + `itv_gt0` -> `gt0`
+  + `itv_le0F` -> `le0F`
+  + `itv_lt0` -> `lt0`
+  + `itv_ge0F` -> `ge0F`
+  + `itv_ge0` -> `ge0`
+  + `itv_lt0F` -> `lt0F`
+  + `itv_le0` -> `le0`
+  + `itv_gt0F` -> `gt0F`
+  + `itv_top_typ` -> `top_typ`
+  + `inum_eq` -> `num_eq`
+  + `inum_le` -> `num_le`
+  + `inum_lt` -> `num_lt`
+
 ### Generalized
 
+- in `constructive_ereal.v`:
+  + generalized from `realDomainType` to `numDomainType`
+    * lemmas `EFin_min` and `EFin_max`
+    * lemmas `maxye`, `maxeNy`, `mineNy`, `minye`
+
 ### Deprecated
 
+- file `signed.v` (use `itv.v` instead)
+
+- in `itv.v`:
+  + notation `%:inum` (use `%:num` instead)
+
 ### Removed
 
 ### Infrastructure

analysis_stdlib/Rstruct_topology.v

@@ -12,7 +12,7 @@ From mathcomp Require Import archimedean.
 From HB Require Import structures.
 From mathcomp Require Import mathcomp_extra.
 From mathcomp Require Import boolp classical_sets.
-From mathcomp Require Import reals signed.
+From mathcomp Require Import reals itv.
 From mathcomp Require Import topology.
 From mathcomp Require Export Rstruct.
 

analysis_stdlib/showcase/uniform_bigO.v

@@ -3,7 +3,7 @@ From Coq Require Import Reals.
 From Coq Require Import ssreflect ssrfun ssrbool.
 From mathcomp Require Import ssrnat eqtype choice fintype bigop order ssralg ssrnum.
 From mathcomp Require Import boolp reals Rstruct_topology ereal.
-From mathcomp Require Import classical_sets signed topology normedtype landau.
+From mathcomp Require Import classical_sets itv topology normedtype landau.
 
 Set Implicit Arguments.
 Unset Strict Implicit.
@@ -98,7 +98,7 @@ Proof.
 move=> fOg; apply/Ouex_to_P; move: fOg => /eqOP [k [kreal hk]].
 have /hk [Q [->]] : k < maxr 1 (k + 1) by rewrite lt_max ltrDl orbC ltr01.
 move=> [R [[_/posnumP[e1] Re1] [_/posnumP[e2] Re2]] sRQ] fOg.
-exists (minr e1%:num e2%:num) => //.
+exists (minr e1%:num e2%:num); first by apply: gt0; exact: RbaseSymbolsImpl.R.
 exists (maxr 1 (k + 1)); first by rewrite lt_max ltr01.
 move=> x dx dxe Pdx; apply: (fOg (x, dx)); split=> //=.
 move: dxe; rewrite gt_max !lt_min => /andP[/andP [dxe11 _] /andP [_ dxe22]].

classical/mathcomp_extra.v

@@ -538,3 +538,82 @@ Qed.
 Definition sigT_fun {I : Type} {X : I -> Type} {T : Type}
   (f : forall i, X i -> T) (x : {i & X i}) : T :=
   (f (projT1 x) (projT2 x)).
+
+(* To backport to interval (through mathcomp_extra) *)
+Lemma comparable_BSide_min d (T : porderType d) b (x y : T) : (x >=< y)%O ->
+  BSide b (Order.min x y) = Order.min (BSide b x) (BSide b y).
+Proof. by rewrite !minEle bnd_simp => /comparable_leP[]. Qed.
+
+(* To backport to interval (through mathcomp_extra) *)
+Lemma comparable_BSide_max d (T : porderType d) b (x y : T) : (x >=< y)%O ->
+  BSide b (Order.max x y) = Order.max (BSide b x) (BSide b y).
+Proof. by rewrite !maxEle bnd_simp => /comparable_leP[]. Qed.
+
+(* To backport to interval (through mathcomp_extra) *)
+Lemma BSide_min d (T : orderType d) b (x y : T) : (x >=< y)%O ->
+  BSide b (Order.min x y) = Order.min (BSide b x) (BSide b y).
+Proof. exact: comparable_BSide_min. Qed.
+
+(* To backport to interval (through mathcomp_extra) *)
+Lemma BSide_max d (T : orderType d) b (x y : T) : (x >=< y)%O ->
+  BSide b (Order.max x y) = Order.max (BSide b x) (BSide b y).
+Proof. exact: comparable_BSide_max. Qed.
+
+Section NumDomainType.
+
+Variable (R : numDomainType).
+
+(* To backport to interval (through mathcomp_extra) *)
+Lemma real_BSide_min b (x y : R) : x \in Num.real -> y \in Num.real ->
+  BSide b (Order.min x y) = Order.min (BSide b x) (BSide b y).
+Proof. by move=> xr yr; apply/comparable_BSide_min/real_comparable. Qed.
+
+(* To backport to interval (through mathcomp_extra) *)
+Lemma real_BSide_max b (x y : R) : x \in Num.real -> y \in Num.real ->
+  BSide b (Order.max x y) = Order.max (BSide b x) (BSide b y).
+Proof. by move=> xr yr; apply/comparable_BSide_max/real_comparable. Qed.
+
+(* To backport to ssralg.v *)
+Lemma natr_min (m n : nat) : (Order.min m n)%:R = Order.min m%:R n%:R :> R.
+Proof. by rewrite !minElt ltr_nat /Order.lt/= -fun_if. Qed.
+
+(* To backport to ssralg.v *)
+Lemma natr_max (m n : nat) : (Order.max m n)%:R = Order.max m%:R n%:R :> R.
+Proof. by rewrite !maxElt ltr_nat /Order.lt/= -fun_if. Qed.
+
+End NumDomainType.
+
+(* To backport to order.v (through mathcomp_extra) *)
+Lemma comparable_min_le_min d (T : porderType d) (x y z t : T) :
+    (x >=< y)%O -> (z >=< t)%O ->
+  (x <= z)%O -> (y <= t)%O -> (Order.min x y <= Order.min z t)%O.
+Proof.
+move=> + + xz yt => /comparable_leP[] xy /comparable_leP[] zt //.
+- exact: le_trans xy yt.
+- exact: le_trans (ltW xy) xz.
+Qed.
+
+(* To backport to order.v (through mathcomp_extra) *)
+Lemma comparable_max_le_max d (T : porderType d) (x y z t : T) :
+    (x >=< y)%O -> (z >=< t)%O ->
+  (x <= z)%O -> (y <= t)%O -> (Order.max x y <= Order.max z t)%O.
+Proof.
+move=> + + xz yt => /comparable_leP[] xy /comparable_leP[] zt //.
+- exact: le_trans yt (ltW zt).
+- exact: le_trans xz zt.
+Qed.
+
+(* To backport to order.v (through mathcomp_extra) *)
+Lemma min_le_min d (T : orderType d) (x y z t : T) :
+  (x <= z)%O -> (y <= t)%O -> (Order.min x y <= Order.min z t)%O.
+Proof. exact: comparable_min_le_min. Qed.
+
+(* To backport to order.v (through mathcomp_extra) *)
+Lemma max_le_max d (T : orderType d) (x y z t : T) :
+  (x <= z)%O -> (y <= t)%O -> (Order.max x y <= Order.max z t)%O.
+Proof. exact: comparable_max_le_max. Qed.
+
+(* To backport to ssrnum.v *)
+Lemma real_sqrtC {R : numClosedFieldType} (x : R) : 0 <= x ->
+  sqrtC x \in Num.real.
+Proof. by rewrite -sqrtC_ge0; apply: ger0_real. Qed.

reals/all_reals.v

@@ -1,4 +1,3 @@
-From mathcomp Require Export signed.
 From mathcomp Require Export itv.
 From mathcomp Require Export constructive_ereal.
 From mathcomp Require Export reals.