From a3e23bb545e9a1a1af86c1976e13e22007dc7489 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Sun, 10 Nov 2024 18:14:26 +0100 Subject: [PATCH 01/18] Remove unused imports of signed.v --- theories/cantor.v | 2 +- theories/exp.v | 2 +- theories/homotopy_theory/path.v | 2 +- theories/homotopy_theory/wedge_sigT.v | 2 +- theories/showcase/summability.v | 2 +- theories/topology_theory/bool_topology.v | 2 +- theories/topology_theory/nat_topology.v | 2 +- theories/topology_theory/one_point_compactification.v | 2 +- 8 files changed, 8 insertions(+), 8 deletions(-) diff --git a/theories/cantor.v b/theories/cantor.v index 8006e1ced..4abb09e12 100644 --- a/theories/cantor.v +++ b/theories/cantor.v @@ -3,7 +3,7 @@ From HB Require Import structures. From mathcomp Require Import all_ssreflect ssralg ssrint ssrnum interval rat. From mathcomp Require Import finmap. From mathcomp Require Import mathcomp_extra boolp classical_sets functions. -From mathcomp Require Import cardinality reals signed. +From mathcomp Require Import cardinality reals. From mathcomp Require Import topology function_spaces separation_axioms. (**md**************************************************************************) diff --git a/theories/exp.v b/theories/exp.v index cb7d2b8b7..3b8e397da 100644 --- a/theories/exp.v +++ b/theories/exp.v @@ -62,7 +62,7 @@ Fact is_cvg_pseries_inside_norm f (x z : R) : cvgn (pseries (fun i => `|f i|) z). Proof. move=> Cx zLx; have [K [Kreal Kf]] := cvg_series_bounded Cx. -have Kzxn n : 0 <= `|K + 1| * `|z ^+ n| / `|x ^+ n| by rewrite !mulr_ge0. +have Kzxn n : 0 <= `|K + 1| * `|z ^+ n| / `|x ^+ n| by rewrite !mulr_ge0. apply: normed_cvg. apply: series_le_cvg Kzxn _ _ => [//=| /= n|]. rewrite (_ : `|_ * _| = `|f n * x ^+ n| * `|z ^+ n| / `|x ^+ n|); last first. diff --git a/theories/homotopy_theory/path.v b/theories/homotopy_theory/path.v index e11e80938..e66a3a4d9 100644 --- a/theories/homotopy_theory/path.v +++ b/theories/homotopy_theory/path.v @@ -2,7 +2,7 @@ From HB Require Import structures. From mathcomp Require Import all_ssreflect all_algebra finmap generic_quotient. From mathcomp Require Import mathcomp_extra boolp classical_sets functions. -From mathcomp Require Import cardinality fsbigop reals signed topology. +From mathcomp Require Import cardinality fsbigop reals topology. From mathcomp Require Import function_spaces wedge_sigT. (**md**************************************************************************) diff --git a/theories/homotopy_theory/wedge_sigT.v b/theories/homotopy_theory/wedge_sigT.v index 86822e545..21b9dd659 100644 --- a/theories/homotopy_theory/wedge_sigT.v +++ b/theories/homotopy_theory/wedge_sigT.v @@ -2,7 +2,7 @@ From HB Require Import structures. From mathcomp Require Import all_ssreflect all_algebra finmap generic_quotient. From mathcomp Require Import mathcomp_extra boolp classical_sets functions. -From mathcomp Require Import cardinality fsbigop reals signed topology. +From mathcomp Require Import cardinality fsbigop reals topology. From mathcomp Require Import separation_axioms function_spaces. (**md**************************************************************************) diff --git a/theories/showcase/summability.v b/theories/showcase/summability.v index dae60a5b9..801b6b9b9 100644 --- a/theories/showcase/summability.v +++ b/theories/showcase/summability.v @@ -3,7 +3,7 @@ From HB Require Import structures. From mathcomp Require Import all_ssreflect ssralg ssrint ssrnum finmap matrix. From mathcomp Require Import interval zmodp. From mathcomp Require Import boolp classical_sets. -From mathcomp Require Import ereal reals signed topology normedtype. +From mathcomp Require Import ereal reals topology normedtype. (**md**************************************************************************) (* This file proposes a replacement for the definition `summable` (file *) diff --git a/theories/topology_theory/bool_topology.v b/theories/topology_theory/bool_topology.v index 29b8dc62f..2d4112091 100644 --- a/theories/topology_theory/bool_topology.v +++ b/theories/topology_theory/bool_topology.v @@ -1,7 +1,7 @@ (* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C. *) From HB Require Import structures. From mathcomp Require Import all_ssreflect all_algebra all_classical. -From mathcomp Require Import signed reals topology_structure uniform_structure. +From mathcomp Require Import reals topology_structure uniform_structure. From mathcomp Require Import pseudometric_structure order_topology compact. (**md**************************************************************************) diff --git a/theories/topology_theory/nat_topology.v b/theories/topology_theory/nat_topology.v index 4325ac634..30cb658ba 100644 --- a/theories/topology_theory/nat_topology.v +++ b/theories/topology_theory/nat_topology.v @@ -2,7 +2,7 @@ From HB Require Import structures. From mathcomp Require Import all_ssreflect all_algebra archimedean. From mathcomp Require Import all_classical. -From mathcomp Require Import signed reals topology_structure uniform_structure. +From mathcomp Require Import reals topology_structure uniform_structure. From mathcomp Require Import pseudometric_structure order_topology. (**md**************************************************************************) diff --git a/theories/topology_theory/one_point_compactification.v b/theories/topology_theory/one_point_compactification.v index 7c970d03f..737e524b3 100644 --- a/theories/topology_theory/one_point_compactification.v +++ b/theories/topology_theory/one_point_compactification.v @@ -1,6 +1,6 @@ From HB Require Import structures. From mathcomp Require Import all_ssreflect all_algebra all_classical. -From mathcomp Require Import signed topology_structure uniform_structure. +From mathcomp Require Import topology_structure uniform_structure. From mathcomp Require Import pseudometric_structure compact weak_topology. (**md**************************************************************************) From d94d0864a1edd6f976d2ec246693bfbe195b0718 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Sat, 16 Nov 2024 20:28:35 +0100 Subject: [PATCH 02/18] Generalize EFin_min and EFin_max Generalized from realDomainType to numDomainType --- CHANGELOG_UNRELEASED.md | 4 ++++ reals/constructive_ereal.v | 12 ++++++------ 2 files changed, 10 insertions(+), 6 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 971b02c98..6cc2cd47a 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -10,6 +10,10 @@ ### Generalized +- in `constructive_ereal.v`: + + generalized from `realDomainType` to `numDomainType` + * lemmas `EFin_min` and `EFin_max` + ### Deprecated ### Removed diff --git a/reals/constructive_ereal.v b/reals/constructive_ereal.v index a2155ef0e..6209188bc 100644 --- a/reals/constructive_ereal.v +++ b/reals/constructive_ereal.v @@ -702,6 +702,12 @@ Lemma sumEFin I s P (F : I -> R) : \sum_(i <- s | P i) (F i)%:E = (\sum_(i <- s | P i) F i)%:E. Proof. by rewrite (big_morph _ EFinD erefl). Qed. +Lemma EFin_min : {morph (@EFin R) : r s / Num.min r s >-> Order.min r s}. +Proof. by move=> x y; rewrite !minElt lte_fin -fun_if. Qed. + +Lemma EFin_max : {morph (@EFin R) : r s / Num.max r s >-> Order.max r s}. +Proof. by move=> x y; rewrite !maxElt lte_fin -fun_if. Qed. + Definition adde_def x y := ~~ ((x == +oo) && (y == -oo)) && ~~ ((x == -oo) && (y == +oo)). @@ -2366,9 +2372,6 @@ by move=> [x| |] [y| |]//= _ _; apply/esym; have [ab|ba] := leP x y; [apply/max_idPr; rewrite lee_fin|apply/max_idPl; rewrite lee_fin ltW]. Qed. -Lemma EFin_max : {morph (@EFin R) : r s / Num.max r s >-> maxe r s}. -Proof. by move=> a b /=; rewrite -fine_max. Qed. - Lemma fine_min : {in fin_num &, {mono @fine R : x y / mine x y >-> (Num.min x y)%:E}}. Proof. @@ -2376,9 +2379,6 @@ by move=> [x| |] [y| |]//= _ _; apply/esym; have [ab|ba] := leP x y; [apply/min_idPl; rewrite lee_fin|apply/min_idPr; rewrite lee_fin ltW]. Qed. -Lemma EFin_min : {morph (@EFin R) : r s / Num.min r s >-> mine r s}. -Proof. by move=> a b /=; rewrite -fine_min. Qed. - Lemma adde_maxl : left_distributive (@GRing.add (\bar R)) maxe. Proof. move=> x y z; have [xy|yx] := leP x y. From 2ac888ff61bce4fdb989ad1a70a4a4f53b91a5c4 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Sun, 24 Nov 2024 17:09:29 +0100 Subject: [PATCH 03/18] A few lemmas to backport about min and max --- CHANGELOG_UNRELEASED.md | 6 ++++ classical/mathcomp_extra.v | 74 ++++++++++++++++++++++++++++++++++++++ 2 files changed, 80 insertions(+) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 6cc2cd47a..1652c9240 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -4,6 +4,12 @@ ### 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` + and `max_le_max` + ### Changed ### Renamed diff --git a/classical/mathcomp_extra.v b/classical/mathcomp_extra.v index f2c287308..c0ce76885 100644 --- a/classical/mathcomp_extra.v +++ b/classical/mathcomp_extra.v @@ -538,3 +538,77 @@ 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. From bc15db387b32de701bc1789be40360b1614c7627 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Sun, 24 Nov 2024 17:10:05 +0100 Subject: [PATCH 04/18] Lemma real_sqrtC to backport --- CHANGELOG_UNRELEASED.md | 4 ++-- classical/mathcomp_extra.v | 5 +++++ 2 files changed, 7 insertions(+), 2 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 1652c9240..1753c3958 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -7,8 +7,8 @@ - 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` - and `max_le_max` + `comparable_min_le_min`, `comparable_max`, `min_le_min`, + `max_le_max` and `real_sqrtC` ### Changed diff --git a/classical/mathcomp_extra.v b/classical/mathcomp_extra.v index c0ce76885..380b284b5 100644 --- a/classical/mathcomp_extra.v +++ b/classical/mathcomp_extra.v @@ -612,3 +612,8 @@ Proof. exact: comparable_min_le_min. Qed. 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. From a6a1cd417d5197d758a653e0c8ae3b174bd60fe2 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Sun, 24 Nov 2024 17:15:53 +0100 Subject: [PATCH 05/18] Add lemmas about extended reals --- CHANGELOG_UNRELEASED.md | 6 +++ reals/constructive_ereal.v | 92 +++++++++++++++++++++++++++++--------- 2 files changed, 76 insertions(+), 22 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 1753c3958..231da5efa 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -10,6 +10,11 @@ `comparable_min_le_min`, `comparable_max`, `min_le_min`, `max_le_max` and `real_sqrtC` +- 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 ### Renamed @@ -19,6 +24,7 @@ - in `constructive_ereal.v`: + generalized from `realDomainType` to `numDomainType` * lemmas `EFin_min` and `EFin_max` + * lemmas `maxye`, `maxeNy`, `mineNy`, `minye` ### Deprecated diff --git a/reals/constructive_ereal.v b/reals/constructive_ereal.v index 6209188bc..6caabc258 100644 --- a/reals/constructive_ereal.v +++ b/reals/constructive_ereal.v @@ -366,6 +366,12 @@ Lemma le0y : (0 : \bar R) <= +oo. Proof. exact: real0. Qed. Lemma leNy0 : -oo <= (0 : \bar R). Proof. exact: real0. Qed. +Lemma cmp0y : ((0 : \bar R) >=< +oo%E)%O. +Proof. by rewrite /Order.comparable le0y. Qed. + +Lemma cmp0Ny : ((0 : \bar R) >=< -oo%E)%O. +Proof. by rewrite /Order.comparable leNy0 orbT. Qed. + Lemma lt0e x : (0 < x) = (x != 0) && (0 <= x). Proof. by case: x => [r| |]//; rewrite lte_fin lee_fin lt0r. Qed. @@ -386,6 +392,38 @@ Proof. by case: x => //=; rewrite real0. Qed. Lemma real_leNye x : (-oo <= x) = (fine x \is Num.real). Proof. by case: x => //=; rewrite real0. Qed. +Lemma minye : left_id (+oo : \bar R) Order.min. +Proof. by case. Qed. + +Lemma real_miney (x : \bar R) : (0 >=< x)%O -> Order.min x +oo = x. +Proof. +by case: x => [x |//|//] rx; rewrite minEle real_leey [_ \in Num.real]rx. +Qed. + +Lemma real_minNye (x : \bar R) : (0 >=< x)%O -> Order.min -oo%E x = -oo%E. +Proof. +by case: x => [x |//|//] rx; rewrite minEle real_leNye [_ \in Num.real]rx. +Qed. + +Lemma mineNy : right_zero (-oo : \bar R) Order.min. +Proof. by case=> [x |//|//]; rewrite minElt. Qed. + +Lemma maxye : left_zero (+oo : \bar R) Order.max. +Proof. by case. Qed. + +Lemma real_maxey (x : \bar R) : (0 >=< x)%O -> Order.max x +oo = +oo. +Proof. +by case: x => [x |//|//] rx; rewrite maxEle real_leey [_ \in Num.real]rx. +Qed. + +Lemma real_maxNye (x : \bar R) : (0 >=< x)%O -> Order.max -oo%E x = x. +Proof. +by case: x => [x |//|//] rx; rewrite maxEle real_leNye [_ \in Num.real]rx. +Qed. + +Lemma maxeNy : right_id (-oo : \bar R) Order.max. +Proof. by case=> [x |//|//]; rewrite maxElt. Qed. + Lemma gee0P x : 0 <= x <-> x = +oo \/ exists2 r, (r >= 0)%R & x = r%:E. Proof. split=> [|[->|[r r0 ->//]]]; last by rewrite real_leey/=. @@ -1099,6 +1137,9 @@ Proof. move: x => [x||] //; exact: oppr_ge0. Qed. Lemma oppe_le0 x : (- x <= 0) = (0 <= x). Proof. move: x => [x||] //; exact: oppr_le0. Qed. +Lemma oppe_cmp0 x : (0 >=< - x)%O = (0 >=< x)%O. +Proof. by rewrite /Order.comparable oppe_ge0 oppe_le0 orbC. Qed. + Lemma sume_ge0 T (f : T -> \bar R) (P : pred T) : (forall t, P t -> 0 <= f t) -> forall l, 0 <= \sum_(i <- l | P i) f i. Proof. by move=> f0 l; elim/big_rec : _ => // t x Pt; apply/adde_ge0/f0. Qed. @@ -1224,6 +1265,34 @@ case: x y => [x||] [y||]// rx ry; |by rewrite mulNyNy /Order.comparable le0y]. Qed. +Lemma real_fine (x : \bar R) : (0 >=< x)%O = (fine x \in Num.real). +Proof. by case: x => [x //||//]; rewrite /= real0 /Order.comparable le0y. Qed. + +Lemma real_muleN (x y : \bar R) : (0 >=< x)%O -> (0 >=< y)%O -> + x * - y = - (x * y). +Proof. +rewrite !real_fine; case: x y => [x||] [y||] /= xr yr; rewrite /mule/=. +- by rewrite mulrN. +- by case: ifP; rewrite ?oppe0//; case: ifP. +- by case: ifP; rewrite ?oppe0//; case: ifP. +- rewrite EFinN oppe_eq0; case: ifP; rewrite ?oppe0// oppe_gt0 !lte_fin. + by case: (real_ltgtP xr yr) => // <-; rewrite eqxx. +- by case: ifP. +- by case: ifP. +- rewrite EFinN oppe_eq0; case: ifP; rewrite ?oppe0// oppe_gt0 !lte_fin. + by case: (real_ltgtP xr yr) => // <-; rewrite eqxx. +- by rewrite lt0y. +- by rewrite lt0y. +Qed. + +Lemma real_mulNe (x y : \bar R) : (0 >=< x)%O -> (0 >=< y)%O -> + - x * y = - (x * y). +Proof. by move=> rx ry; rewrite muleC real_muleN 1?muleC. Qed. + +Lemma real_muleNN (x y : \bar R) : (0 >=< x)%O -> (0 >=< y)%O -> + - x * - y = x * y. +Proof. by move=> rx ry; rewrite real_muleN ?real_mulNe ?oppeK ?oppe_cmp0. Qed. + Lemma sqreD x y : x + y \is a fin_num -> (x + y) ^+ 2 = x ^+ 2 + x * y *+ 2 + y ^+ 2. Proof. @@ -1617,16 +1686,7 @@ by move: x y => [r0| |] [r1| |] //=; rewrite ?(leey, leNye)// !lee_fin lerNl. Qed. Lemma muleN x y : x * - y = - (x * y). -Proof. -move: x y => [x| |] [y| |] //=; rewrite /mule/=; try by rewrite ltry. -- by rewrite mulrN. -- by rewrite !eqe !lte_fin; case: ltrgtP => //; rewrite oppe0. -- by rewrite !eqe !lte_fin; case: ltrgtP => //; rewrite oppe0. -- rewrite !eqe oppr_eq0 eq_sym; case: ifP; rewrite ?oppe0// => y0. - by rewrite [RHS]fun_if ltNge if_neg EFinN leeNl oppe0 le_eqVlt eqe y0. -- rewrite !eqe oppr_eq0 eq_sym; case: ifP; rewrite ?oppe0// => y0. - by rewrite [RHS]fun_if ltNge if_neg EFinN leeNl oppe0 le_eqVlt eqe y0. -Qed. +Proof. by rewrite real_muleN ?real_fine ?num_real. Qed. Lemma mulNe x y : - x * y = - (x * y). Proof. by rewrite muleC muleN muleC. Qed. @@ -2393,30 +2453,18 @@ move=> x y z; have [yz|zy] := leP y z. by apply/esym/max_idPl; rewrite leeD2l// ltW. Qed. -Lemma maxye : left_zero (+oo : \bar R) maxe. -Proof. by move=> x; have [|//] := leP +oo x; rewrite leye_eq => /eqP. Qed. - Lemma maxey : right_zero (+oo : \bar R) maxe. Proof. by move=> x; rewrite maxC maxye. Qed. Lemma maxNye : left_id (-oo : \bar R) maxe. Proof. by move=> x; have [//|] := leP -oo x; rewrite ltNge leNye. Qed. -Lemma maxeNy : right_id (-oo : \bar R) maxe. -Proof. by move=> x; rewrite maxC maxNye. Qed. - HB.instance Definition _ := Monoid.isLaw.Build (\bar R) -oo maxe maxA maxNye maxeNy. Lemma minNye : left_zero (-oo : \bar R) mine. Proof. by move=> x; have [|//] := leP x -oo; rewrite leeNy_eq => /eqP. Qed. -Lemma mineNy : right_zero (-oo : \bar R) mine. -Proof. by move=> x; rewrite minC minNye. Qed. - -Lemma minye : left_id (+oo : \bar R) mine. -Proof. by move=> x; have [//|] := leP x +oo; rewrite ltNge leey. Qed. - Lemma miney : right_id (+oo : \bar R) mine. Proof. by move=> x; rewrite minC minye. Qed. From ef966d9e60ec7890cebf628eb1860fc025477829 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Mon, 11 Nov 2024 15:27:47 +0100 Subject: [PATCH 06/18] Generalize itv.v From intervals on numDomainType to any porderType by making the semantics (from intervals of int to intervals of the considered type) parametric. Currently only instantiated for numDomainType though. --- CHANGELOG_UNRELEASED.md | 19 + reals/itv.v | 1219 ++++++++++++++++++++++----------------- theories/convex.v | 2 +- theories/exp.v | 5 +- theories/hoelder.v | 4 +- 5 files changed, 702 insertions(+), 547 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 231da5efa..c35f7744c 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -10,6 +10,10 @@ `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` + - in `constructive_ereal.v` + lemmas `cmp0y`, `cmp0Ny`, `real_miney`, `real_minNye`, `real_maxey`, `real_maxNye`, `oppe_cmp0`, `real_fine`, @@ -17,8 +21,23 @@ ### 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` + ### Generalized - in `constructive_ereal.v`: diff --git a/reals/itv.v b/reals/itv.v index 7ac9e597b..706855742 100644 --- a/reals/itv.v +++ b/reals/itv.v @@ -3,7 +3,7 @@ From HB Require Import structures. From mathcomp Require Import ssreflect ssrfun ssrbool. From mathcomp Require Import ssrnat eqtype choice order ssralg ssrnum ssrint. From mathcomp Require Import interval. -From mathcomp Require Import mathcomp_extra boolp signed. +From mathcomp Require Import mathcomp_extra boolp. (**md**************************************************************************) (* # Numbers within an interval *) @@ -13,7 +13,7 @@ From mathcomp Require Import mathcomp_extra boolp signed. (* like {itv R & `[a, b]}, a notation e%:itv that infers an enclosing *) (* interval for expression e according to existing canonical instances and *) (* %:inum to cast back from type {itv R & i} to R. *) -(* For instance, x : {i01 R}, we have (1 - x%:inum)%:itv : {i01 R} *) +(* For instance, for x : {i01 R}, we have (1 - x%:inum)%:itv : {i01 R} *) (* automatically inferred. *) (* *) (* ## types for values within known interval *) @@ -24,6 +24,7 @@ From mathcomp Require Import mathcomp_extra boolp signed. (* and x <= 1 if x is canonically a {i01 R}. {i01 R} is *) (* canonically stable by common operations. *) (* {itv R & i} == more generic type of values in interval i : interval int *) +(* (see interval.v for notations that can be sused for i). *) (* R must have a numDomainType structure. This type is shown *) (* to be a porderType. *) (* ``` *) @@ -40,26 +41,32 @@ From mathcomp Require Import mathcomp_extra boolp signed. (* ## sign proofs *) (* ``` *) (* [itv of x] == proof that x is in interval inferred by x%:itv *) -(* [lb of x] == proof that lb < x or lb <= x with lb the lower bound *) -(* inferred by x%:itv *) -(* [ub of x] == proof that x < ub or x <= ub with ub the upper bound *) -(* inferred by x%:itv *) -(* [lbe of x] == proof that lb <= x *) -(* [ube of x] == proof that x <= ub *) (* ``` *) (* *) (* ## constructors *) (* ``` *) -(* ItvNum xin == builds a {itv R & i} from a proof xin : x \in i *) -(* where x : R *) +(* ItvNum xr lx xu == builds a {itv R & i} from proofs xr : x \in Num.real, *) +(* lx : Itv.map_itv_bound (Itv.num_sem R) l <= BLeft x *) +(* xu : BRight x <= Itv.map_itv_bound (Itv.num_sem R) u *) +(* where x : R with R : numDomainType *) +(* and l u : itv_bound int *) +(* ItvReal lx xu == builds a {itv R & i} from proofs *) +(* lx : Itv.map_itv_bound (Itv.num_sem R) l <= BLeft x *) +(* xu : BRight x <= Itv.map_itv_bound (Itv.num_sem R) u *) +(* where x : R with R : realDomainType *) +(* and l u : itv_bound int *) +(* Itv01 x0 x1 == builds a {i01 R} from proofs x0 : 0 <= x and x1 : x <= 1*) +(* where x : R with R : numDomainType *) (* ``` *) (* *) (* A number of canonical instances are provided for common operations, if *) (* your favorite operator is missing, look below for examples on how to add *) (* the appropriate Canonical. *) +(* Also note that all provided instances aren't necessarily optimal, *) +(* improvements welcome! *) (* Canonical instances are also provided according to types, as a *) -(* fallback when no known operator appears in the expression. Look to *) -(* itv_top_typ below for an example on how to add your favorite type. *) +(* fallback when no known operator appears in the expression. Look to top_typ *) +(* below for an example on how to add your favorite type. *) (******************************************************************************) Reserved Notation "{ 'itv' R & i }" @@ -70,11 +77,8 @@ Reserved Notation "{ 'i01' R }" Reserved Notation "x %:itv" (at level 2, format "x %:itv"). Reserved Notation "x %:i01" (at level 2, format "x %:i01"). Reserved Notation "x %:inum" (at level 2, format "x %:inum"). + Reserved Notation "[ 'itv' 'of' x ]" (format "[ 'itv' 'of' x ]"). -Reserved Notation "[ 'lb' 'of' x ]" (format "[ 'lb' 'of' x ]"). -Reserved Notation "[ 'ub' 'of' x ]" (format "[ 'ub' 'of' x ]"). -Reserved Notation "[ 'lbe' 'of' x ]" (format "[ 'lbe' 'of' x ]"). -Reserved Notation "[ 'ube' 'of' x ]" (format "[ 'ube' 'of' x ]"). Set Implicit Arguments. Unset Strict Implicit. @@ -85,11 +89,16 @@ Import GRing.Theory Num.Theory. Local Open Scope ring_scope. Local Open Scope order_scope. -Definition wider_itv (x y : interval int) := subitv y x. - Module Itv. -Section Itv. -Context (R : numDomainType). + +Variant t := Top | Real of interval int. + +Definition sub (x y : t) := + match x, y with + | _, Top => true + | Top, Real _ => false + | Real xi, Real yi => subitv xi yi + end. Definition map_itv_bound S T (f : S -> T) (b : itv_bound S) : itv_bound T := match b with @@ -97,86 +106,108 @@ Definition map_itv_bound S T (f : S -> T) (b : itv_bound S) : itv_bound T := | BInfty b => BInfty _ b end. -Definition map_itv S T (f : S -> T) (i : interval S) : interval T := - let 'Interval l u := i in Interval (map_itv_bound f l) (map_itv_bound f u). - -Lemma le_map_itv_bound (x y : itv_bound int) : - x <= y -> - map_itv_bound (fun x => x%:~R : R) x <= map_itv_bound (fun x => x%:~R : R) y. -Proof. -move: x y => [xb x | []xb //=]; last by case: xb. -case=> [yb y /=|//]. -by rewrite /Order.le/=; case: (_ ==> _) => /=; rewrite ?ler_int// ltr_int. -Qed. - -Lemma subitv_map_itv (x y : interval int) : - x <= y -> - map_itv (fun x => x%:~R : R) x <= map_itv (fun x => x%:~R : R) y. -Proof. -move: x y => [lx ux] [ly uy] /andP[lel leu]. -apply/andP; split; exact: le_map_itv_bound. -Qed. +Section Itv. +Context T (sem : interval int -> T -> bool). -Definition itv_cond (i : interval int) (x : R) := - x \in map_itv (fun x => x%:~R : R) i. +Definition spec (i : t) (x : T) := if i is Real i then sem i x else true. -Record def (i : interval int) := Def { - r :> R; +Record def (i : t) := Def { + r : T; #[canonical=no] - P : itv_cond i r + P : spec i r }. End Itv. -Notation spec i x := (itv_cond i%Z%R x). - -Record typ := Typ { - sort : numDomainType; +Record typ i := Typ { + sort : Type; #[canonical=no] - sort_itv : interval int; + sort_sem : interval int -> sort -> bool; #[canonical=no] - allP : forall x : sort, spec sort_itv x + allP : forall x : sort, spec sort_sem i x }. -Definition mk {R} i r P : @def R i := - @Def R i r P. +Definition mk {T f} i x P : @def T f i := @Def T f i x P. + +Definition from {T f i} {x : @def T f i} (phx : phantom T (r x)) := x. + +Definition fromP {T f i} {x : @def T f i} (phx : phantom T (r x)) := P x. -Definition from {R i} - {x : @def R i} (phx : phantom R x) := x. +Definition num_sem (R : numDomainType) (i : interval int) (x : R) : bool := + (x \in Num.real) + && let: Interval l u := i in + x \in Interval (map_itv_bound intr l) (map_itv_bound intr u). -Definition fromP {R i} - {x : @def R i} (phx : phantom R x) := P x. +Definition nat_sem (i : interval int) (x : nat) : bool := Posz x \in i. Module Exports. -Notation "{ 'itv' R & i }" := (def R i%Z) : type_scope. -Notation "{ 'i01' R }" := (def R `[Posz 0, Posz 1]) : type_scope. +Arguments r {T sem i}. +Notation "{ 'itv' R & i }" := (def (@num_sem R) (Itv.Real i%Z)) : type_scope. +Notation "{ 'i01' R }" := {itv R & `[0, 1]} : type_scope. Notation "x %:itv" := (from (Phantom _ x)) : ring_scope. Notation "[ 'itv' 'of' x ]" := (fromP (Phantom _ x)) : ring_scope. Notation inum := r. Notation "x %:inum" := (r x) : ring_scope. -Arguments r {R i}. End Exports. End Itv. Export Itv.Exports. +Local Notation num_spec := (Itv.spec (@Itv.num_sem _)). +Local Notation num_def R := (Itv.def (@Itv.num_sem R)). +Local Notation num_itv_bound R := (@Itv.map_itv_bound _ R intr). + +Local Notation nat_spec := (Itv.spec Itv.nat_sem). +Local Notation nat_def := (Itv.def Itv.nat_sem). + Section POrder. -Variables (R : numDomainType) (i : interval int). -Local Notation nR := {itv R & i}. -HB.instance Definition _ := [isSub for @Itv.r R i]. -HB.instance Definition _ := [Choice of nR by <:]. -HB.instance Definition _ := [SubChoice_isSubPOrder of nR by <: - with ring_display]. +Context d (T : porderType d) (f : interval int -> T -> bool) (i : Itv.t). +Local Notation itv := (Itv.def f i). +HB.instance Definition _ := [isSub for @Itv.r T f i]. +HB.instance Definition _ : Order.POrder d itv := [POrder of itv by <:]. End POrder. -(* TODO: numDomainType on sT ? *) -Lemma itv_top_typ_subproof (R : numDomainType) (x : R) : - Itv.spec `]-oo, +oo[ x. +Section Order. +Variables (R : numDomainType) (i : interval int). +Local Notation nR := (num_def R (Itv.Real i)). + +Lemma itv_le_total_subproof : total (<=%O : rel nR). +Proof. +move=> x y; apply: real_comparable. +- by case: x => [x /=/andP[]]. +- by case: y => [y /=/andP[]]. +Qed. + +HB.instance Definition _ := Order.POrder_isTotal.Build ring_display nR + itv_le_total_subproof. + +End Order. + +Lemma top_typ_subproof T f (x : T) : Itv.spec f Itv.Top x. Proof. by []. Qed. -Canonical itv_top_typ (R : numDomainType) := Itv.Typ (@itv_top_typ_subproof R). +Canonical top_typ T f := Itv.Typ (@top_typ_subproof T f). + +Lemma real_domain_typ_subproof (R : realDomainType) (x : R) : + num_spec (Itv.Real `]-oo, +oo[) x. +Proof. by rewrite /Itv.num_sem/= num_real. Qed. + +Canonical real_domain_typ (R : realDomainType) := + Itv.Typ (@real_domain_typ_subproof R). + +Lemma real_field_typ_subproof (R : realFieldType) (x : R) : + num_spec (Itv.Real `]-oo, +oo[) x. +Proof. exact: real_domain_typ_subproof. Qed. + +Canonical real_field_typ (R : realFieldType) := + Itv.Typ (@real_field_typ_subproof R). + +Lemma nat_typ_subproof (x : nat) : nat_spec (Itv.Real `[0, +oo[) x. +Proof. by []. Qed. -Lemma typ_inum_subproof (xt : Itv.typ) (x : Itv.sort xt) : - Itv.spec (Itv.sort_itv xt) x. +Canonical nat_typ := Itv.Typ nat_typ_subproof. + +Lemma typ_inum_subproof (i : Itv.t) (xt : Itv.typ i) (x : Itv.sort xt) : + Itv.spec (@Itv.sort_sem _ xt) i x. Proof. by move: xt x => []. Qed. (* This adds _ <- Itv.r ( typ_inum ) @@ -184,121 +215,212 @@ Proof. by move: xt x => []. Qed. Itv.r) meaning that if no other canonical instance (with a registered head symbol) is found, a canonical instance of Itv.typ, like the ones above, will be looked for. *) -Canonical typ_inum (xt : Itv.typ) (x : Itv.sort xt) := +Canonical typ_inum (i : Itv.t) (xt : Itv.typ i) (x : Itv.sort xt) := Itv.mk (typ_inum_subproof x). -Notation unify_itv ix iy := (unify wider_itv ix iy). +Class unify {T} f (x y : T) := Unify : f x y = true. +#[export] Hint Mode unify - - - + : typeclass_instances. +Class unify' {T} f (x y : T) := Unify' : f x y = true. +#[export] Instance unify'P {T} f (x y : T) : unify' f x y -> unify f x y := id. +#[export] +Hint Extern 0 (unify' _ _ _) => vm_compute; reflexivity : typeclass_instances. -Section Theory. -Context {R : numDomainType} {i : interval int}. -Local Notation sT := {itv R & i}. -Implicit Type x : sT. +Notation unify_itv ix iy := (unify Itv.sub ix iy). + +#[export] Instance top_wider_anything i : unify_itv i Itv.Top. +Proof. by case: i. Qed. + +#[export] Instance real_wider_anyreal i : + unify_itv (Itv.Real i) (Itv.Real `]-oo, +oo[). +Proof. by case: i => [l u]; apply/andP; rewrite !bnd_simp. Qed. + +Definition itv_real1_subdef (op1 : interval int -> interval int) + (x : Itv.t) : Itv.t := + match x with Itv.Top => Itv.Top | Itv.Real x => Itv.Real (op1 x) end. + +Definition itv_real2_subdef (op2 : interval int -> interval int -> interval int) + (x y : Itv.t) : Itv.t := + match x, y with + | Itv.Top, _ | _, Itv.Top => Itv.Top + | Itv.Real x, Itv.Real y => Itv.Real (op2 x y) + end. -Lemma itv_intro {x} : x%:inum = x%:inum :> R. Proof. by []. Qed. +Lemma itv_real1_subproof T f (op1 : T -> T) + (op1i : interval int -> interval int) (x : T) : + (forall xi, f xi x = true -> f (op1i xi) (op1 x) = true) -> + forall xi, Itv.spec f xi x -> + Itv.spec f (itv_real1_subdef op1i xi) (op1 x). +Proof. by move=> + [//| xi]; apply. Qed. + +Lemma itv_real2_subproof T f (op2 : T -> T -> T) + (op2i : interval int -> interval int -> interval int) (x y : T) : + (forall xi yi, f xi x = true -> f yi y = true -> + f (op2i xi yi) (op2 x y) = true) -> + forall xi yi, Itv.spec f xi x -> Itv.spec f yi y -> + Itv.spec f (itv_real2_subdef op2i xi yi) (op2 x y). +Proof. by move=> + [//| xi] [//| yi]; apply. Qed. + +Lemma map_itv_bound_comp S T U (f : T -> S) (g : U -> T) (b : itv_bound U) : + Itv.map_itv_bound (f \o g) b = Itv.map_itv_bound f (Itv.map_itv_bound g b). +Proof. by case: b. Qed. + +Section NumDomainTheory. +Context {R : numDomainType} {i : Itv.t}. +Implicit Type x : num_def R i. + +Lemma intr_le_map_itv_bound (x y : itv_bound int) : + (num_itv_bound R x <= num_itv_bound R y)%O = (x <= y)%O. +Proof. +by case: x y => [[] x | x] [[] y | y]//=; rewrite !bnd_simp ?ler_int ?ltr_int. +Qed. -Definition empty_itv := `[Posz 1, Posz 0]. +Lemma intr_BLeft_le_map_itv_bound (x : itv_bound int) (y : int) : + (num_itv_bound R x <= BLeft (y%:~R : R))%O = (x <= BLeft y)%O. +Proof. +rewrite -[BLeft y%:~R]/(Itv.map_itv_bound intr (BLeft y)). +by rewrite intr_le_map_itv_bound. +Qed. -Lemma itv_bottom x : unify_itv empty_itv i -> False. +Lemma BRight_intr_le_map_itv_bound (x : int) (y : itv_bound int) : + (BRight (x%:~R : R) <= num_itv_bound R y)%O = (BRight x <= y)%O. Proof. -move: x => [x /subitvP /(_ x)]; rewrite in_itv/= lexx => /(_ erefl) xi. -move=> /(@Itv.subitv_map_itv R) /subitvP /(_ _ xi). +rewrite -[BRight x%:~R]/(Itv.map_itv_bound intr (BRight x)). +by rewrite intr_le_map_itv_bound. +Qed. + +Lemma subitv_map_itv (x y : Itv.t) : Itv.sub x y -> + forall z : R, num_spec x z -> num_spec y z. +Proof. +case: x y => [| x] [| y] //= x_sub_y z /andP[rz]; rewrite /Itv.num_sem rz/=. +move: x y x_sub_y => [lx ux] [ly uy] /andP[lel leu] /=. +move=> /andP[lxz zux]; apply/andP; split. +- by apply: le_trans lxz; rewrite intr_le_map_itv_bound ?map_itv_bound_num. +- by apply: le_trans zux _; rewrite intr_le_map_itv_bound ?map_itv_bound_num. +Qed. + +Definition empty_itv := Itv.Real `[Posz 1, Posz 0]. + +Lemma bottom x : unify_itv i empty_itv -> False. +Proof. +case: x => x /= /[swap] /subitv_map_itv /[apply] /andP[_] /=. by rewrite in_itv/= => /andP[] /le_trans /[apply]; rewrite ler10. Qed. -Lemma itv_gt0 x : unify_itv `]Posz 0, +oo[ i -> 0%R < x%:inum :> R. +Lemma gt0 x : unify_itv i (Itv.Real `]Posz 0, +oo[) -> 0%R < x%:inum :> R. Proof. -move: x => [x /= xi] /(@Itv.subitv_map_itv R) /subitvP /(_ _ xi). -by rewrite in_itv/= andbT. +case: x => x /= /[swap] /subitv_map_itv /[apply] /andP[_]. +by rewrite /= in_itv/= andbT. Qed. -Lemma itv_le0F x : unify_itv `]Posz 0, +oo[ i -> x%:inum <= 0%R :> R = false. +Lemma le0F x : unify_itv i (Itv.Real `]Posz 0, +oo[) -> + x%:inum <= 0%R :> R = false. Proof. -move: x => [x /= xi] /(@Itv.subitv_map_itv R) /subitvP /(_ _ xi). +case: x => x /= /[swap] /subitv_map_itv /[apply] /andP[_] /=. by rewrite in_itv/= andbT => /lt_geF. Qed. -Lemma itv_lt0 x : unify_itv `]-oo, Posz 0[ i -> x%:inum < 0%R :> R. +Lemma lt0 x : unify_itv i (Itv.Real `]-oo, Posz 0[) -> x%:inum < 0%R :> R. Proof. -move: x => [x /= xi] /(@Itv.subitv_map_itv R) /subitvP /(_ _ xi). -by rewrite in_itv. +by case: x => x /= /[swap] /subitv_map_itv /[apply] /andP[_] /=; rewrite in_itv. Qed. -Lemma itv_ge0F x : unify_itv `]-oo, Posz 0[ i -> 0%R <= x%:inum :> R = false. +Lemma ge0F x : unify_itv i (Itv.Real `]-oo, Posz 0[) -> + 0%R <= x%:inum :> R = false. Proof. -move: x => [x /= xi] /(@Itv.subitv_map_itv R) /subitvP /(_ _ xi). +case: x => x /= /[swap] /subitv_map_itv /[apply] /andP[_] /=. by rewrite in_itv/= => /lt_geF. Qed. -Lemma itv_ge0 x : unify_itv `[Posz 0, +oo[ i -> 0%R <= x%:inum :> R. +Lemma ge0 x : unify_itv i (Itv.Real `[Posz 0, +oo[) -> 0%R <= x%:inum :> R. Proof. -move: x => [x /= xi] /(@Itv.subitv_map_itv R) /subitvP /(_ _ xi). +case: x => x /= /[swap] /subitv_map_itv /[apply] /andP[_] /=. by rewrite in_itv/= andbT. Qed. -Lemma itv_lt0F x : unify_itv `[Posz 0, +oo[ i -> x%:inum < 0%R :> R = false. +Lemma lt0F x : unify_itv i (Itv.Real `[Posz 0, +oo[) -> + x%:inum < 0%R :> R = false. Proof. -move: x => [x /= xi] /(@Itv.subitv_map_itv R) /subitvP /(_ _ xi). +case: x => x /= /[swap] /subitv_map_itv /[apply] /andP[_] /=. by rewrite in_itv/= andbT => /le_gtF. Qed. -Lemma itv_le0 x : unify_itv `]-oo, Posz 0] i -> x%:inum <= 0%R :> R. +Lemma le0 x : unify_itv i (Itv.Real `]-oo, Posz 0]) -> x%:inum <= 0%R :> R. Proof. -move: x => [x /= xi] /(@Itv.subitv_map_itv R) /subitvP /(_ _ xi). -by rewrite in_itv/=. +by case: x => x /= /[swap] /subitv_map_itv /[apply] /andP[_] /=; rewrite in_itv. Qed. -Lemma itv_gt0F x : unify_itv `]-oo, Posz 0] i -> 0%R < x%:inum :> R = false. +Lemma gt0F x : unify_itv i (Itv.Real `]-oo, Posz 0]) -> + 0%R < x%:inum :> R = false. Proof. -move: x => [x /= xi] /(@Itv.subitv_map_itv R) /subitvP /(_ _ xi). +case: x => x /= /[swap] /subitv_map_itv /[apply] /andP[_] /=. by rewrite in_itv/= => /le_gtF. Qed. -Lemma lt1 x : unify_itv `]-oo, Posz 1[ i -> x%:inum < 1%R :> R. +Lemma cmp0 x : unify_itv i (Itv.Real `]-oo, +oo[) -> (0 >=< x%:inum). +Proof. by case: i x => [//| i' [x /=/andP[]]]. Qed. + +Lemma neq0 x : + unify (fun ix iy => negb (Itv.sub ix iy)) (Itv.Real `[0%Z, 0%Z]) i -> + x%:inum != 0 :> R. Proof. -move: x => [x /= xi] /(@Itv.subitv_map_itv R) /subitvP /(_ _ xi). -by rewrite in_itv. +case: i x => [//| [l u] [x /= Px]]; apply: contra => /eqP x0 /=. +move: Px; rewrite x0 => /and3P[_ /= l0 u0]; apply/andP; split. +- by case: l l0 => [[] l /= |//]; rewrite !bnd_simp ?lerz0 ?ltrz0. +- by case: u u0 => [[] u /= |//]; rewrite !bnd_simp ?ler0z ?ltr0z. Qed. -Lemma ge1F x : unify_itv `]-oo, Posz 1[ i -> 1%R <= x%:inum :> R = false. +Lemma eq0F x : + unify (fun ix iy => negb (Itv.sub ix iy)) (Itv.Real `[0%Z, 0%Z]) i -> + x%:inum == 0 :> R = false. +Proof. by move=> u; apply/negbTE/neq0. Qed. + +Lemma lt1 x : unify_itv i (Itv.Real `]-oo, Posz 1[) -> x%:inum < 1%R :> R. Proof. -move: x => [x /= xi] /(@Itv.subitv_map_itv R) /subitvP /(_ _ xi). -by rewrite in_itv/= => /lt_geF. +by case: x => x /= /[swap] /subitv_map_itv /[apply] /andP[_] /=; rewrite in_itv. Qed. -Lemma le1 x : unify_itv `]-oo, Posz 1] i -> x%:inum <= 1%R :> R. +Lemma ge1F x : unify_itv i (Itv.Real `]-oo, Posz 1[) -> + 1%R <= x%:inum :> R = false. Proof. -move: x => [x /= xi] /(@Itv.subitv_map_itv R) /subitvP /(_ _ xi). -by rewrite in_itv/=. +case: x => x /= /[swap] /subitv_map_itv /[apply] /andP[_] /=. +by rewrite in_itv/= => /lt_geF. Qed. -Lemma gt1F x : unify_itv `]-oo, Posz 1] i -> 1%R < x%:inum :> R = false. +Lemma le1 x : unify_itv i (Itv.Real `]-oo, Posz 1]) -> x%:inum <= 1%R :> R. Proof. -move: x => [x /= xi] /(@Itv.subitv_map_itv R) /subitvP /(_ _ xi). -by rewrite in_itv/= => /le_gtF. +by case: x => x /= /[swap] /subitv_map_itv /[apply] /andP[_] /=; rewrite in_itv. Qed. -Lemma widen_itv_subproof x i' : unify_itv i' i -> Itv.spec i' x%:inum. +Lemma gt1F x : unify_itv i (Itv.Real `]-oo, Posz 1]) -> + 1%R < x%:inum :> R = false. Proof. -by move: x => [x /= xi] /(@Itv.subitv_map_itv R) /subitvP /(_ _ xi). +case: x => x /= /[swap] /subitv_map_itv /[apply] /andP[_] /=. +by rewrite in_itv/= => /le_gtF. Qed. -Definition widen_itv x i' (uni : unify_itv i' i) := +Lemma widen_itv_subproof x i' : Itv.sub i i' -> num_spec i' x%:inum. +Proof. by case: x => x /= /[swap] /subitv_map_itv; apply. Qed. + +Definition widen_itv x i' (uni : unify_itv i i') := Itv.mk (widen_itv_subproof x uni). Lemma widen_itvE x (uni : unify_itv i i) : @widen_itv x i uni = x. Proof. exact/val_inj. Qed. -End Theory. - -Arguments itv_bottom {R i} _ {_}. -Arguments itv_gt0 {R i} _ {_}. -Arguments itv_le0F {R i} _ {_}. -Arguments itv_lt0 {R i} _ {_}. -Arguments itv_ge0F {R i} _ {_}. -Arguments itv_ge0 {R i} _ {_}. -Arguments itv_lt0F {R i} _ {_}. -Arguments itv_le0 {R i} _ {_}. -Arguments itv_gt0F {R i} _ {_}. +End NumDomainTheory. + +Arguments bottom {R i} _ {_}. +Arguments gt0 {R i} _ {_}. +Arguments le0F {R i} _ {_}. +Arguments lt0 {R i} _ {_}. +Arguments ge0F {R i} _ {_}. +Arguments ge0 {R i} _ {_}. +Arguments lt0F {R i} _ {_}. +Arguments le0 {R i} _ {_}. +Arguments gt0F {R i} _ {_}. +Arguments cmp0 {R i} _ {_}. +Arguments neq0 {R i} _ {_}. +Arguments eq0F {R i} _ {_}. Arguments lt1 {R i} _ {_}. Arguments ge1F {R i} _ {_}. Arguments le1 {R i} _ {_}. @@ -306,30 +428,34 @@ Arguments gt1F {R i} _ {_}. Arguments widen_itv {R i} _ {_ _}. Arguments widen_itvE {R i} _ {_}. -#[global] Hint Extern 0 (is_true (0%R < _)%O) => solve [apply: itv_gt0] : core. -#[global] Hint Extern 0 (is_true (_ < 0%R)%O) => solve [apply: itv_lt0] : core. -#[global] Hint Extern 0 (is_true (0%R <= _)%O) => solve [apply: itv_ge0] : core. -#[global] Hint Extern 0 (is_true (_ <= 0%R)%O) => solve [apply: itv_le0] : core. -#[global] Hint Extern 0 (is_true (_ < 1%R)%O) => solve [apply: lt1] : core. -#[global] Hint Extern 0 (is_true (_ <= 1%R)%O) => solve [apply: le1] : core. +#[export] Hint Extern 0 (is_true (0%R < _)%R) => solve [apply: gt0] : core. +#[export] Hint Extern 0 (is_true (_ < 0%R)%R) => solve [apply: lt0] : core. +#[export] Hint Extern 0 (is_true (0%R <= _)%R) => solve [apply: ge0] : core. +#[export] Hint Extern 0 (is_true (_ <= 0%R)%R) => solve [apply: le0] : core. +#[export] Hint Extern 0 (is_true (_ \is Num.real)) => solve [apply: cmp0] + : core. +#[export] Hint Extern 0 (is_true (0%R >=< _)%R) => solve [apply: cmp0] : core. +#[export] Hint Extern 0 (is_true (_ != 0%R)) => solve [apply: neq0] : core. +#[export] Hint Extern 0 (is_true (_ < 1%R)%R) => solve [apply: lt1] : core. +#[export] Hint Extern 0 (is_true (_ <= 1%R)%R) => solve [apply: le1] : core. Notation "x %:i01" := (widen_itv x%:itv : {i01 _}) (only parsing) : ring_scope. Notation "x %:i01" := (@widen_itv _ _ - (@Itv.from _ _ _ (Phantom _ x)) `[Posz 0, Posz 1] _) + (@Itv.from _ _ _ (Phantom _ x)) (Itv.Real `[Posz 0, Posz 1]) _) (only printing) : ring_scope. Local Open Scope ring_scope. -Section NumDomainStability. +Section NumDomainInstances. Context {R : numDomainType}. -Lemma zero_inum_subproof : Itv.spec `[0, 0] (0 : R). -Proof. by rewrite /Itv.itv_cond/= inE. Qed. +Lemma zero_inum_subproof : num_spec (Itv.Real `[0, 0]) (0 : R). +Proof. by apply/andP; split; [exact: real0 | rewrite /= in_itv/= lexx]. Qed. Canonical zero_inum := Itv.mk zero_inum_subproof. -Lemma one_inum_subproof : Itv.spec `[1, 1] (1 : R). -Proof. by rewrite /Itv.itv_cond/= inE. Qed. +Lemma one_inum_subproof : num_spec (Itv.Real `[1, 1]) (1 : R). +Proof. by apply/andP; split; [exact: real1 | rewrite /= in_itv/= lexx]. Qed. Canonical one_inum := Itv.mk one_inum_subproof. @@ -338,59 +464,47 @@ Definition opp_itv_bound_subdef (b : itv_bound int) : itv_bound int := | BSide b x => BSide (~~ b) (intZmod.oppz x) | BInfty b => BInfty _ (~~ b) end. -Arguments opp_itv_bound_subdef /. Lemma opp_itv_ge0_subproof b : (BLeft 0%R <= opp_itv_bound_subdef b)%O = (b <= BRight 0%R)%O. Proof. by case: b => [[] b | []//]; rewrite /= !bnd_simp oppr_ge0. Qed. Lemma opp_itv_gt0_subproof b : - (BLeft 0%R < opp_itv_bound_subdef b)%O = (b < BRight 0%R)%O. + (BRight 0%R <= opp_itv_bound_subdef b)%O = (b <= BLeft 0%R)%O. Proof. -by case: b => [[] b | []//]; rewrite /= !bnd_simp ?oppr_ge0 // oppr_gt0. +by case: b => [[] b | []//]; rewrite /= !bnd_simp ?oppr_ge0 ?oppr_gt0. Qed. Lemma opp_itv_boundr_subproof (x : R) b : - (BRight (- x)%R <= Itv.map_itv_bound intr (opp_itv_bound_subdef b))%O - = (Itv.map_itv_bound intr b <= BLeft x)%O. + (BRight (- x)%R <= num_itv_bound R (opp_itv_bound_subdef b))%O + = (num_itv_bound R b <= BLeft x)%O. Proof. by case: b => [[] b | []//]; rewrite /= !bnd_simp mulrNz ?lerN2 // ltrN2. Qed. -Lemma opp_itv_le0_subproof b : - (opp_itv_bound_subdef b <= BRight 0%R)%O = (BLeft 0%R <= b)%O. -Proof. by case: b => [[] b | []//]; rewrite /= !bnd_simp oppr_le0. Qed. - -Lemma opp_itv_lt0_subproof b : - (opp_itv_bound_subdef b < BRight 0%R)%O = (BLeft 0%R < b)%O. -Proof. -by case: b => [[] b | []//]; rewrite /= !bnd_simp ?oppr_le0 // oppr_lt0. -Qed. - Lemma opp_itv_boundl_subproof (x : R) b : - (Itv.map_itv_bound intr (opp_itv_bound_subdef b) <= BLeft (- x)%R)%O - = (BRight x <= Itv.map_itv_bound intr b)%O. + (num_itv_bound R (opp_itv_bound_subdef b) <= BLeft (- x)%R)%O + = (BRight x <= num_itv_bound R b)%O. Proof. by case: b => [[] b | []//]; rewrite /= !bnd_simp mulrNz ?lerN2 // ltrN2. Qed. Definition opp_itv_subdef (i : interval int) : interval int := - let 'Interval l u := i in + let: Interval l u := i in Interval (opp_itv_bound_subdef u) (opp_itv_bound_subdef l). Arguments opp_itv_subdef /. -Lemma opp_inum_subproof (i : interval int) - (x : {itv R & i}) (r := opp_itv_subdef i) : - Itv.spec r (- x%:inum). +Lemma opp_inum_subproof (i : Itv.t) (x : num_def R i) + (r := itv_real1_subdef opp_itv_subdef i) : + num_spec r (- x%:inum). Proof. -rewrite {}/r; move: i x => [l u] [x /= /andP[xl xu]]; apply/andP; split. -- by case: u xu => [[] b i | [] //] /=; rewrite /Order.le/= mulrNz; - do ?[by rewrite lerNl opprK|by rewrite ltrNl opprK]. -- by case: l xl => [[] b i | [] //] /=; rewrite /Order.le/= mulrNz; - do ?[by rewrite ltrNl opprK|by rewrite lerNl opprK]. +apply: itv_real1_subproof (Itv.P x). +case: x => x /= _ [l u] /and3P[xr lx xu]. +rewrite /Itv.num_sem/= realN xr/=; apply/andP. +by rewrite opp_itv_boundl_subproof opp_itv_boundr_subproof. Qed. -Canonical opp_inum (i : interval int) (x : {itv R & i}) := +Canonical opp_inum (i : Itv.t) (x : num_def R i) := Itv.mk (opp_inum_subproof x). Definition add_itv_boundl_subdef (b1 b2 : itv_bound int) : itv_bound int := @@ -398,141 +512,163 @@ Definition add_itv_boundl_subdef (b1 b2 : itv_bound int) : itv_bound int := | BSide b1 x1, BSide b2 x2 => BSide (b1 && b2) (intZmod.addz x1 x2) | _, _ => BInfty _ true end. -Arguments add_itv_boundl_subdef /. + +Lemma add_itv_boundl_subproof (x1 x2 : R) b1 b2 : + (num_itv_bound R b1 <= BLeft x1)%O -> (num_itv_bound R b2 <= BLeft x2)%O -> + (num_itv_bound R (add_itv_boundl_subdef b1 b2) <= BLeft (x1 + x2)%R)%O. +Proof. +case: b1 b2 => [bb1 b1 |//] [bb2 b2 |//]. +case: bb1; case: bb2; rewrite /= !bnd_simp mulrzDr_tmp. +- exact: lerD. +- exact: ler_ltD. +- exact: ltr_leD. +- exact: ltrD. +Qed. Definition add_itv_boundr_subdef (b1 b2 : itv_bound int) : itv_bound int := match b1, b2 with | BSide b1 x1, BSide b2 x2 => BSide (b1 || b2) (intZmod.addz x1 x2) | _, _ => BInfty _ false end. -Arguments add_itv_boundr_subdef /. + +Lemma add_itv_boundr_subproof (x1 x2 : R) b1 b2 : + (BRight x1 <= num_itv_bound R b1)%O -> (BRight x2 <= num_itv_bound R b2)%O -> + (BRight (x1 + x2)%R <= num_itv_bound R (add_itv_boundr_subdef b1 b2))%O. +Proof. +case: b1 b2 => [bb1 b1 |//] [bb2 b2 |//]. +case: bb1; case: bb2; rewrite /= !bnd_simp mulrzDr_tmp. +- exact: ltrD. +- exact: ltr_leD. +- exact: ler_ltD. +- exact: lerD. +Qed. Definition add_itv_subdef (i1 i2 : interval int) : interval int := - let 'Interval l1 u1 := i1 in - let 'Interval l2 u2 := i2 in + let: Interval l1 u1 := i1 in + let: Interval l2 u2 := i2 in Interval (add_itv_boundl_subdef l1 l2) (add_itv_boundr_subdef u1 u2). Arguments add_itv_subdef /. -Lemma add_inum_subproof (xi yi : interval int) - (x : {itv R & xi}) (y : {itv R & yi}) - (r := add_itv_subdef xi yi) : - Itv.spec r (x%:inum + y%:inum). +Lemma add_inum_subproof (xi yi : Itv.t) (x : num_def R xi) (y : num_def R yi) + (r := itv_real2_subdef add_itv_subdef xi yi) : + num_spec r (x%:inum + y%:inum). Proof. -rewrite {}/r. -move: xi x yi y => [lx ux] [x /= /andP[xl xu]] [ly uy] [y /= /andP[yl yu]]. -rewrite /Itv.itv_cond in_itv; apply/andP; split. -- move: lx ly xl yl => [xb lx | //] [yb ly | //]. - by move: xb yb => [] []; rewrite /Order.le/= rmorphD/=; - do ?[exact: lerD|exact: ler_ltD|exact: ltr_leD|exact: ltrD]. -- move: ux uy xu yu => [xb ux | //] [yb uy | //]. - by move: xb yb => [] []; rewrite /Order.le/= rmorphD/=; - do ?[exact: lerD|exact: ler_ltD|exact: ltr_leD|exact: ltrD]. +apply: itv_real2_subproof (Itv.P x) (Itv.P y). +case: x y => [x /= _] [y /= _] => {xi yi r} -[lx ux] [ly uy]/=. +move=> /andP[xr /=/andP[lxx xux]] /andP[yr /=/andP[lyy yuy]]. +rewrite /Itv.num_sem realD//=; apply/andP. +by rewrite add_itv_boundl_subproof ?add_itv_boundr_subproof. Qed. -Canonical add_inum (xi yi : interval int) - (x : {itv R & xi}) (y : {itv R & yi}) := +Canonical add_inum (xi yi : Itv.t) (x : num_def R xi) (y : num_def R yi) := Itv.mk (add_inum_subproof x y). -End NumDomainStability. - -Section RealDomainStability. -Context {R : realDomainType}. - -Definition itv_bound_signl (b : itv_bound int) : KnownSign.sign := - let b0 := BLeft 0%Z in - (if b == b0 then =0 else if (b <= b0)%O then <=0 else >=0)%snum_sign. - -Definition itv_bound_signr (b : itv_bound int) : KnownSign.sign := - let b0 := BRight 0%Z in - (if b == b0 then =0 else if (b <= b0)%O then <=0 else >=0)%snum_sign. - -Definition interval_sign (i : interval int) : option KnownSign.real := - let 'Interval l u := i in - (match itv_bound_signl l, itv_bound_signr u with - | =0, <=0 - | >=0, =0 - | >=0, <=0 => None - | =0, =0 => Some (KnownSign.Sign =0) - | <=0, =0 - | <=0, <=0 => Some (KnownSign.Sign <=0) - | =0, >=0 - | >=0, >=0 => Some (KnownSign.Sign >=0) - | <=0, >=0 => Some >=<0 - end)%snum_sign. - -Variant interval_sign_spec (l u : itv_bound int) : option KnownSign.real -> Set := - | ISignNone : (u <= l)%O -> interval_sign_spec l u None - | ISignEqZero : l = BLeft 0 -> u = BRight 0 -> - interval_sign_spec l u (Some (KnownSign.Sign =0)) - | ISignNeg : (l < BLeft 0%:Z)%O -> (u <= BRight 0%:Z)%O -> - interval_sign_spec l u (Some (KnownSign.Sign <=0)) - | ISignPos : (BLeft 0%:Z <= l)%O -> (BRight 0%:Z < u)%O -> - interval_sign_spec l u (Some (KnownSign.Sign >=0)) - | ISignBoth : (l < BLeft 0%:Z)%O -> (BRight 0%:Z < u)%O -> - interval_sign_spec l u (Some >=<0%snum_sign). - -Lemma interval_signP l u : - interval_sign_spec l u (interval_sign (Interval l u)). -Proof. -rewrite /interval_sign/itv_bound_signl/itv_bound_signr. -have [lneg|lpos|->] := ltgtP l; have [uneg|upos|->] := ltgtP u. -- apply: ISignNeg => //; exact: ltW. +Variant signb := EqZero | NonNeg | NonPos. + +Definition itv_bound_signl (b : itv_bound int) : signb := + let: b0 := BLeft 0%Z in + if b == b0 then EqZero else if (b <= b0)%O then NonPos else NonNeg. + +Definition itv_bound_signr (b : itv_bound int) : signb := + let: b0 := BRight 0%Z in + if b == b0 then EqZero else if (b <= b0)%O then NonPos else NonNeg. + +Variant signi := Known of signb | Unknown | Empty. + +Definition interval_sign (i : interval int) : signi := + let: Interval l u := i in + match itv_bound_signl l, itv_bound_signr u with + | EqZero, NonPos + | NonNeg, EqZero + | NonNeg, NonPos => Empty + | EqZero, EqZero => Known EqZero + | NonPos, EqZero + | NonPos, NonPos => Known NonPos + | EqZero, NonNeg + | NonNeg, NonNeg => Known NonNeg + | NonPos, NonNeg => Unknown + end. + +Variant interval_sign_spec (l u : itv_bound int) (x : R) : signi -> Set := + | ISignEqZero : l = BLeft 0 -> u = BRight 0 -> x = 0 -> + interval_sign_spec l u x (Known EqZero) + | ISignNonNeg : (BLeft 0%:Z <= l)%O -> (BRight 0%:Z < u)%O -> 0 <= x -> + interval_sign_spec l u x (Known NonNeg) + | ISignNonPos : (l < BLeft 0%:Z)%O -> (u <= BRight 0%:Z)%O -> x <= 0 -> + interval_sign_spec l u x (Known NonPos) + | ISignBoth : (l < BLeft 0%:Z)%O -> (BRight 0%:Z < u)%O -> x \in Num.real -> + interval_sign_spec l u x Unknown. + +Lemma interval_signP (l u : itv_bound int) (x : R) : + (num_itv_bound R l <= BLeft x)%O -> (BRight x <= num_itv_bound R u)%O -> + x \in Num.real -> + interval_sign_spec l u x (interval_sign (Interval l u)). +Proof. +move=> + + xr; rewrite /interval_sign/itv_bound_signl/itv_bound_signr. +have [lneg|lpos|->] := ltgtP l; have [uneg|upos|->] := ltgtP u => lx xu. +- apply: ISignNonPos => //; first exact: ltW. + have:= le_trans xu (eqbRL (intr_le_map_itv_bound _ _) (ltW uneg)). + by rewrite bnd_simp. - exact: ISignBoth. -- exact: ISignNeg. -- by apply/ISignNone/ltW/(lt_le_trans uneg); rewrite leBRight_ltBLeft. -- by apply: ISignPos => //; exact: ltW. -- by apply: ISignNone; rewrite leBRight_ltBLeft. -- by apply: ISignNone; rewrite -ltBRight_leBLeft. -- exact: ISignPos. -- exact: ISignEqZero. +- exact: ISignNonPos. +- have:= (@ltxx _ _ (num_itv_bound R l)). + rewrite (le_lt_trans lx) -?leBRight_ltBLeft ?(le_trans xu)//. + by rewrite intr_le_map_itv_bound (le_trans (ltW uneg)). +- apply: ISignNonNeg => //; first exact: ltW. + have:= (le_trans (eqbRL (intr_le_map_itv_bound _ _) (ltW lpos)) lx). + by rewrite bnd_simp. +- have:= (@ltxx _ _ (num_itv_bound R l)). + rewrite (le_lt_trans lx) -?leBRight_ltBLeft ?(le_trans xu)//. + by rewrite intr_le_map_itv_bound ?leBRight_ltBLeft. +- have:= (@ltxx _ _ (num_itv_bound R (BLeft 0%Z))). + rewrite (le_lt_trans lx) -?leBRight_ltBLeft ?(le_trans xu)//. + by rewrite intr_le_map_itv_bound -?ltBRight_leBLeft. +- exact: ISignNonNeg. +- apply: ISignEqZero => //. + by apply/le_anti/andP; move: lx xu; rewrite !bnd_simp. Qed. Definition mul_itv_boundl_subdef (b1 b2 : itv_bound int) : itv_bound int := match b1, b2 with - | BSide true 0%Z, BSide _ _ - | BSide _ _, BSide true 0%Z => BSide true 0%Z - | BSide b1 x1, BSide b2 x2 => BSide (b1 && b2) (intRing.mulz x1 x2) + | BInfty _, _ | _, BInfty _ - | BInfty _, _ => BInfty _ false + | BLeft 0%Z, _ + | _, BLeft 0%Z => BLeft 0%Z + | BSide b1 x1, BSide b2 x2 => BSide (b1 && b2) (intRing.mulz x1 x2) end. -Arguments mul_itv_boundl_subdef /. Definition mul_itv_boundr_subdef (b1 b2 : itv_bound int) : itv_bound int := match b1, b2 with - | BSide true 0%Z, _ - | _, BSide true 0%Z => BSide true 0%Z - | BSide false 0%Z, _ - | _, BSide false 0%Z => BSide false 0%Z + | BLeft 0%Z, _ + | _, BLeft 0%Z => BLeft 0%Z + | BRight 0%Z, _ + | _, BRight 0%Z => BRight 0%Z | BSide b1 x1, BSide b2 x2 => BSide (b1 || b2) (intRing.mulz x1 x2) | _, BInfty _ - | BInfty _, _ => BInfty _ false + | BInfty _, _ => +oo%O end. -Arguments mul_itv_boundr_subdef /. Lemma mul_itv_boundl_subproof b1 b2 (x1 x2 : R) : (BLeft 0%:Z <= b1 -> BLeft 0%:Z <= b2 -> - Itv.map_itv_bound intr b1 <= BLeft x1 -> - Itv.map_itv_bound intr b2 <= BLeft x2 -> - Itv.map_itv_bound intr (mul_itv_boundl_subdef b1 b2) <= BLeft (x1 * x2))%O. + num_itv_bound R b1 <= BLeft x1 -> + num_itv_bound R b2 <= BLeft x2 -> + num_itv_bound R (mul_itv_boundl_subdef b1 b2) <= BLeft (x1 * x2))%O. Proof. move: b1 b2 => [[] b1 | []//] [[] b2 | []//] /=; rewrite 4!bnd_simp. - set bl := match b1 with 0%Z => _ | _ => _ end. have -> : bl = BLeft (b1 * b2). rewrite {}/bl; move: b1 b2 => [[|p1]|p1] [[|p2]|p2]; congr BLeft. by rewrite mulr0. - rewrite -2!(ler0z R) bnd_simp intrM; exact: ler_pM. -- case: b1 => [[|p1]|//]; rewrite -2!(ler0z R) !bnd_simp ?intrM. - by move=> _ geb2 ? ?; apply: mulr_ge0 => //; apply/(le_trans geb2)/ltW. - move=> p1gt0 b2ge0 lep1x1 ltb2x2. - have: (Posz p1.+1)%:~R * x2 <= x1 * x2. - by rewrite ler_pM2r //; apply: le_lt_trans ltb2x2. - by apply: lt_le_trans; rewrite ltr_pM2l // ltr0z. -- case: b2 => [[|p2]|//]; rewrite -2!(ler0z R) !bnd_simp ?intrM. - by move=> geb1 _ ? ?; apply: mulr_ge0 => //; apply/(le_trans geb1)/ltW. - move=> b1ge0 p2gt0 ltb1x1 lep2x2. - have: b1%:~R * x2 < x1 * x2; last exact/le_lt_trans/ler_pM. - by rewrite ltr_pM2r //; apply: lt_le_trans lep2x2; rewrite ltr0z. -- rewrite -2!(ler0z R) bnd_simp intrM; exact: ltr_pM. + by rewrite bnd_simp intrM -2!(ler0z R); apply: ler_pM. +- case: b1 => [[|b1] | b1]; rewrite !bnd_simp// => b1p b2p sx1 sx2. + + by rewrite mulr_ge0 ?(le_trans _ (ltW sx2)) ?ler0z. + + rewrite intrM (@lt_le_trans _ _ (b1.+1%:~R * x2)) ?ltr_pM2l//. + by rewrite ler_pM2r// (le_lt_trans _ sx2) ?ler0z. +- case: b2 => [[|b2] | b2]; rewrite !bnd_simp// => b1p b2p sx1 sx2. + + by rewrite mulr_ge0 ?(le_trans _ (ltW sx1)) ?ler0z. + + rewrite intrM (@le_lt_trans _ _ (b1%:~R * x2)) ?ler_wpM2l ?ler0z//. + by rewrite ltr_pM2r ?(lt_le_trans _ sx2). +- by rewrite -2!(ler0z R) bnd_simp intrM; apply: ltr_pM. Qed. Lemma mul_itv_boundrC_subproof b1 b2 : @@ -542,314 +678,315 @@ by move: b1 b2 => [[] [[|?]|?] | []] [[] [[|?]|?] | []] //=; rewrite mulnC. Qed. Lemma mul_itv_boundr_subproof b1 b2 (x1 x2 : R) : - (BLeft 0%R <= BLeft x1 -> BLeft 0%R <= BLeft x2 -> - BRight x1 <= Itv.map_itv_bound intr b1 -> - BRight x2 <= Itv.map_itv_bound intr b2 -> - BRight (x1 * x2) <= Itv.map_itv_bound intr (mul_itv_boundr_subdef b1 b2))%O. -Proof. -move: b1 b2 => [b1b b1 | []] [b2b b2 | []] //=; last first. -- move: b2 b2b => [[|p2]|p2] [] // _ + _ +; rewrite !bnd_simp => le1 le2. - + by move: (le_lt_trans le1 le2); rewrite ltxx. - + by move: (conj le1 le2) => /andP/le_anti <-; rewrite mulr0. -- move: b1 b1b => [[|p1]|p1] [] // + _ + _; rewrite !bnd_simp => le1 le2. - + by move: (le_lt_trans le1 le2); rewrite ltxx. - + by move: (conj le1 le2) => /andP/le_anti <-; rewrite mul0r. -case: b1 => [[|p1]|p1]. -- case: b1b. - by rewrite !bnd_simp => l _ l' _; move: (le_lt_trans l l'); rewrite ltxx. - by move: b2b b2 => [] [[|p2]|p2]; rewrite !bnd_simp; - first (by move=> _ l _ l'; move: (le_lt_trans l l'); rewrite ltxx); - move=> l _ l' _; move: (conj l l') => /andP/le_anti <-; rewrite mul0r. -- rewrite if_same. - case: b2 => [[|p2]|p2]. - + case: b2b => _ + _ +; rewrite !bnd_simp => l l'. - by move: (le_lt_trans l l'); rewrite ltxx. - by move: (conj l l') => /andP/le_anti <-; rewrite mulr0. - + move: b1b b2b => [] []; rewrite !bnd_simp; - rewrite -[intRing.mulz ?[a] ?[b]]/((Posz ?[a]) * ?[b])%R intrM. - * exact: ltr_pM. - * move=> x1ge0 x2ge0 ltx1p1 lex2p2. - have: x1 * p2.+1%:~R < p1.+1%:~R * p2.+1%:~R. - by rewrite ltr_pM2r // ltr0z. - exact/le_lt_trans/ler_pM. - * move=> x1ge0 x2ge0 lex1p1 ltx2p2. - have: p1.+1%:~R * x2 < p1.+1%:~R * p2.+1%:~R. - by rewrite ltr_pM2l // ltr0z. - exact/le_lt_trans/ler_pM. - * exact: ler_pM. - + case: b2b => _ + _; rewrite 2!bnd_simp => l l'. - by move: (le_lt_trans l l'); rewrite ltr0z. - by move: (le_trans l l'); rewrite ler0z. -- case: b1b => + _ + _; rewrite 2!bnd_simp => l l'. - by move: (le_lt_trans l l'); rewrite ltr0z. - by move: (le_trans l l'); rewrite ler0z. + (0 <= x1 -> 0 <= x2 -> + BRight x1 <= num_itv_bound R b1 -> + BRight x2 <= num_itv_bound R b2 -> + BRight (x1 * x2) <= num_itv_bound R (mul_itv_boundr_subdef b1 b2))%O. +Proof. +case: b1 b2 => [b1b b1 | []] [b2b b2 | []] //= x1p x2p; last first. +- case: b2b b2 => -[[|//] | //] _ x20. + + have:= (@ltxx _ (itv_bound R) (BLeft 0%:~R)). + by rewrite (lt_le_trans _ x20). + + have -> : x2 = 0 by apply/le_anti/andP. + by rewrite mulr0. +- case: b1b b1 => -[[|//] |//] x10 _. + + have:= (@ltxx _ (itv_bound R) (BLeft 0%Z%:~R)). + by rewrite (lt_le_trans _ x10). + + by have -> : x1 = 0; [apply/le_anti/andP | rewrite mul0r]. +case: b1b b2b => -[]; rewrite -[intRing.mulz]/GRing.mul. +- case: b1 => [[|b1] | b1]; rewrite !bnd_simp => x1b x2b. + + by have:= (@ltxx _ R 0); rewrite (le_lt_trans x1p x1b). + + case: b2 x2b => [[| b2] | b2] => x2b; rewrite bnd_simp. + * by have:= (@ltxx _ R 0); rewrite (le_lt_trans x2p x2b). + * by rewrite intrM ltr_pM. + * have:= (@ltxx _ R 0); rewrite (le_lt_trans x2p)//. + by rewrite (lt_le_trans x2b) ?lerz0. + + have:= (@ltxx _ R 0); rewrite (le_lt_trans x1p)//. + by rewrite (lt_le_trans x1b) ?lerz0. +- case: b1 => [[|b1] | b1]; rewrite !bnd_simp => x1b x2b. + + by have:= (@ltxx _ R 0); rewrite (le_lt_trans x1p x1b). + + case: b2 x2b => [[| b2] | b2] x2b; rewrite bnd_simp. + * exact: mulr_ge0_le0. + * by rewrite intrM (le_lt_trans (ler_wpM2l x1p x2b)) ?ltr_pM2r. + * have:= (@ltxx _ _ x2). + by rewrite (le_lt_trans x2b) ?(lt_le_trans _ x2p) ?ltrz0. + + have:= (@ltxx _ _ x1). + by rewrite (lt_le_trans x1b) ?(le_trans _ x1p) ?lerz0. +- case: b1 => [[|b1] | b1]; rewrite !bnd_simp => x1b x2b. + + case: b2 x2b => [[|b2] | b2] x2b; rewrite bnd_simp. + * by have:= (@ltxx _ _ x2); rewrite (lt_le_trans x2b). + * by have -> : x1 = 0; [apply/le_anti/andP | rewrite mul0r]. + * have:= (@ltxx _ _ x2). + by rewrite (lt_le_trans x2b) ?(le_trans _ x2p) ?lerz0. + + case: b2 x2b => [[|b2] | b2] x2b; rewrite bnd_simp. + * by have:= (@ltxx _ _ x2); rewrite (lt_le_trans x2b). + * by rewrite intrM (le_lt_trans (ler_wpM2r x2p x1b)) ?ltr_pM2l. + * have:= (@ltxx _ _ x2). + by rewrite (lt_le_trans x2b) ?(le_trans _ x2p) ?lerz0. + + have:= (@ltxx _ _ x1). + by rewrite (le_lt_trans x1b) ?(lt_le_trans _ x1p) ?ltrz0. +- case: b1 => [[|b1] | b1]; rewrite !bnd_simp => x1b x2b. + + by have -> : x1 = 0; [apply/le_anti/andP | rewrite mul0r]. + + case: b2 x2b => [[| b2] | b2] x2b; rewrite bnd_simp. + * by have -> : x2 = 0; [apply/le_anti/andP | rewrite mulr0]. + * by rewrite intrM ler_pM. + * have:= (@ltxx _ _ x2). + by rewrite (le_lt_trans x2b) ?(lt_le_trans _ x2p) ?ltrz0. + + have:= (@ltxx _ _ x1). + by rewrite (le_lt_trans x1b) ?(lt_le_trans _ x1p) ?ltrz0. +Qed. + +Lemma mul_itv_boundr_BRight_subproof b1 b2 : + (BRight 0%Z <= b1 -> BRight 0%Z <= b2 -> + BRight 0%Z <= mul_itv_boundr_subdef b1 b2)%O. +Proof. +case: b1 b2 => [b1b b1 | []] [b2b b2 | []]//=. +- by case: b1b b2b => -[]; case: b1 b2 => [[|b1] | b1] [[|b2] | b2]. +- by case: b1b b1 => -[[] |]. +- by case: b2b b2 => -[[] |]. Qed. Lemma mul_itv_boundr'_subproof b1 b2 (x1 x2 : R) : - (BLeft 0%:R <= BLeft x1 -> BRight 0%:Z <= b2 -> - BRight x1 <= Itv.map_itv_bound intr b1 -> - BRight x2 <= Itv.map_itv_bound intr b2 -> - BRight (x1 * x2) <= Itv.map_itv_bound intr (mul_itv_boundr_subdef b1 b2))%O. + (0 <= x1 -> x2 \in Num.real -> BRight 0%Z <= b2 -> + BRight x1 <= num_itv_bound R b1 -> + BRight x2 <= num_itv_bound R b2 -> + BRight (x1 * x2) <= num_itv_bound R (mul_itv_boundr_subdef b1 b2))%O. Proof. -move=> x1ge0 b2ge0 lex1b1 lex2b2. -have [x2ge0 | x2lt0] := leP 0 x2; first exact: mul_itv_boundr_subproof. +move=> x1ge0 x2r b2ge0 lex1b1 lex2b2. +have /orP[x2ge0 | x2le0] := x2r; first exact: mul_itv_boundr_subproof. have lem0 : (BRight (x1 * x2) <= BRight 0%R)%O. by rewrite bnd_simp mulr_ge0_le0 // ltW. apply: le_trans lem0 _. -move: b1 b2 lex1b1 lex2b2 b2ge0 => [b1b b1 | []] [b2b b2 | []] //=; last first. -- by move: b2 b2b => [[|?]|?] []. -- move: b1 b1b => [[|p1]|p1] [] //. - by rewrite leBRight_ltBLeft => /(le_lt_trans x1ge0); rewrite ltxx. -case: b1 => [[|p1]|p1]. -- case: b1b; last by move: b2b b2 => [] [[|]|]. - by rewrite leBRight_ltBLeft => /(le_lt_trans x1ge0); rewrite ltxx. -- rewrite if_same. - case: b2 => [[|p2]|p2]; first (by case: b2b); last by case: b2b. - by rewrite if_same => _ _ _ /=; rewrite leBSide ltrW_lteif // ltr0z. -- rewrite leBRight_ltBLeft => /(le_lt_trans x1ge0). - by case: b1b; rewrite bnd_simp ?ltr0z // ler0z. +rewrite -(mulr0z 1) BRight_intr_le_map_itv_bound. +apply: mul_itv_boundr_BRight_subproof => //. +by rewrite -(@BRight_intr_le_map_itv_bound R) (le_trans _ lex1b1). Qed. Definition mul_itv_subdef (i1 i2 : interval int) : interval int := - let 'Interval l1 u1 := i1 in - let 'Interval l2 u2 := i2 in - let opp := opp_itv_bound_subdef in - let mull := mul_itv_boundl_subdef in - let mulr := mul_itv_boundr_subdef in + let: Interval l1 u1 := i1 in + let: Interval l2 u2 := i2 in + let: opp := opp_itv_bound_subdef in + let: mull := mul_itv_boundl_subdef in + let: mulr := mul_itv_boundr_subdef in match interval_sign i1, interval_sign i2 with - | None, _ | _, None => `[1, 0] - | some s1, Some s2 => - (match s1, s2 with - | =0, _ => `[0, 0] - | _, =0 => `[0, 0] - | >=0, >=0 => Interval (mull l1 l2) (mulr u1 u2) - | <=0, <=0 => Interval (mull (opp u1) (opp u2)) (mulr (opp l1) (opp l2)) - | >=0, <=0 => Interval (opp (mulr u1 (opp l2))) (opp (mull l1 (opp u2))) - | <=0, >=0 => Interval (opp (mulr (opp l1) u2)) (opp (mull (opp u1) l2)) - | >=0, >=<0 => Interval (opp (mulr u1 (opp l2))) (mulr u1 u2) - | <=0, >=<0 => Interval (opp (mulr (opp l1) u2)) (mulr (opp l1) (opp l2)) - | >=<0, >=0 => Interval (opp (mulr (opp l1) u2)) (mulr u1 u2) - | >=<0, <=0 => Interval (opp (mulr u1 (opp l2))) (mulr (opp l1) (opp l2)) - | >=<0, >=<0 => Interval - (Order.min (opp (mulr (opp l1) u2)) - (opp (mulr u1 (opp l2)))) - (Order.max (mulr (opp l1) (opp l2)) - (mulr u1 u2)) - end)%snum_sign + | Empty, _ | _, Empty => `[1, 0] + | Known EqZero, _ | _, Known EqZero => `[0, 0] + | Known NonNeg, Known NonNeg => + Interval (mull l1 l2) (mulr u1 u2) + | Known NonPos, Known NonPos => + Interval (mull (opp u1) (opp u2)) (mulr (opp l1) (opp l2)) + | Known NonNeg, Known NonPos => + Interval (opp (mulr u1 (opp l2))) (opp (mull l1 (opp u2))) + | Known NonPos, Known NonNeg => + Interval (opp (mulr (opp l1) u2)) (opp (mull (opp u1) l2)) + | Known NonNeg, Unknown => + Interval (opp (mulr u1 (opp l2))) (mulr u1 u2) + | Known NonPos, Unknown => + Interval (opp (mulr (opp l1) u2)) (mulr (opp l1) (opp l2)) + | Unknown, Known NonNeg => + Interval (opp (mulr (opp l1) u2)) (mulr u1 u2) + | Unknown, Known NonPos => + Interval (opp (mulr u1 (opp l2))) (mulr (opp l1) (opp l2)) + | Unknown, Unknown => + Interval + (Order.min (opp (mulr (opp l1) u2)) (opp (mulr u1 (opp l2)))) + (Order.max (mulr (opp l1) (opp l2)) (mulr u1 u2)) end. Arguments mul_itv_subdef /. +Lemma comparable_num_itv_bound_subproof (x y : itv_bound int) : + (num_itv_bound R x >=< num_itv_bound R y)%O. +Proof. +by case: x y => [[] x | []] [[] y | []]//; apply/orP; + rewrite !bnd_simp ?ler_int ?ltr_int; + case: leP => xy; apply/orP => //; rewrite ltW ?orbT. +Qed. + Lemma map_itv_bound_min (x y : itv_bound int) : - Itv.map_itv_bound (fun x => x%:~R : R) (Order.min x y) - = Order.min (Itv.map_itv_bound intr x) (Itv.map_itv_bound intr y). + num_itv_bound R (Order.min x y) + = Order.min (num_itv_bound R x) (num_itv_bound R y). Proof. -have [lexy|ltyx] := leP x y; first by rewrite !minEle Itv.le_map_itv_bound. -by rewrite minElt -if_neg -leNgt Itv.le_map_itv_bound // ltW. +have [lexy | ltyx] := leP x y; [by rewrite !minEle intr_le_map_itv_bound lexy|]. +rewrite minElt -if_neg -comparable_leNgt ?intr_le_map_itv_bound ?ltW//. +exact: comparable_num_itv_bound_subproof. Qed. Lemma map_itv_bound_max (x y : itv_bound int) : - Itv.map_itv_bound (fun x => x%:~R : R) (Order.max x y) - = Order.max (Itv.map_itv_bound intr x) (Itv.map_itv_bound intr y). -Proof. -have [lexy|ltyx] := leP x y; first by rewrite !maxEle Itv.le_map_itv_bound. -by rewrite maxElt -if_neg -leNgt Itv.le_map_itv_bound // ltW. -Qed. - -Lemma mul_inum_subproof (xi yi : interval int) - (x : {itv R & xi}) (y : {itv R & yi}) - (r := mul_itv_subdef xi yi) : - Itv.spec r (x%:inum * y%:inum). -Proof. -rewrite {}/r. -move: xi x yi y => [lx ux] [x /= /andP[+ +]] [ly uy] [y /= /andP[+ +]]. -rewrite -/(interval_sign (Interval lx ux)). -rewrite -/(interval_sign (Interval ly uy)). -have empty10 (z : R) l u : (u <= l)%O -> - (Itv.map_itv_bound [eta intr] l <= BLeft z)%O -> - (BRight z <= Itv.map_itv_bound [eta intr] u)%O -> False. - move=> leul; rewrite leBRight_ltBLeft => /le_lt_trans /[apply]. - rewrite lt_def => /andP[/[swap]] => + /ltac:(apply/negP). - rewrite negbK; move: leul => /(Itv.le_map_itv_bound R) le1 le2. - by apply/eqP/le_anti; rewrite le1. -pose opp := opp_itv_bound_subdef. -pose mull := mul_itv_boundl_subdef. -pose mulr := mul_itv_boundr_subdef. -have [leuxlx|-> ->|lxneg uxneg|lxpos uxpos|lxneg uxpos] := interval_signP. -- move=> + + /ltac:(exfalso); exact: empty10. -- rewrite 2!bnd_simp => lex1 lex2 ley1 ley2. - have -> : x = 0 by apply: le_anti; rewrite lex1 lex2. - rewrite mul0r. - case: interval_signP; [|by move=> _ _; rewrite /Itv.itv_cond in_itv/= lexx..]. - by move=> leul; exfalso; move: ley1 ley2; apply: empty10. -- move=> lelxx lexux. - have xneg : x <= 0. - move: (le_trans lexux (Itv.le_map_itv_bound R uxneg)). - by rewrite /= bnd_simp. - have [leuyly|-> ->|lyneg uyneg|lypos uypos|lyneg uypos] := interval_signP. - + move=> + + /ltac:(exfalso); exact: empty10. - + rewrite 2!bnd_simp => ley1 ley2. - have -> : y = 0 by apply: le_anti; rewrite ley1 ley2. - by rewrite mulr0 /Itv.itv_cond in_itv/= lexx. - + move=> lelyy leyuy. - have yneg : y <= 0. - move: (le_trans leyuy (Itv.le_map_itv_bound R uyneg)). - by rewrite /= bnd_simp. - rewrite -[Interval _ _]/(Interval (mull (opp ux) (opp uy)) - (mulr (opp lx) (opp ly))). - rewrite -mulrNN /Itv.itv_cond itv_boundlr. - rewrite mul_itv_boundl_subproof ?mul_itv_boundr_subproof //. - * by rewrite bnd_simp oppr_ge0. - * by rewrite bnd_simp oppr_ge0. - * by rewrite opp_itv_boundr_subproof. - * by rewrite opp_itv_boundr_subproof. - * by rewrite opp_itv_ge0_subproof. - * by rewrite opp_itv_ge0_subproof. - * by rewrite opp_itv_boundl_subproof. - * by rewrite opp_itv_boundl_subproof. - + move=> lelyy leyuy. - have ypos : 0 <= y. - move: (le_trans (Itv.le_map_itv_bound R lypos) lelyy). - by rewrite /= bnd_simp. - rewrite -[Interval _ _]/(Interval (opp (mulr (opp lx) uy)) - (opp (mull (opp ux) ly))). - rewrite -[x * y]opprK -mulNr /Itv.itv_cond itv_boundlr. - rewrite opp_itv_boundl_subproof opp_itv_boundr_subproof. - rewrite mul_itv_boundl_subproof ?mul_itv_boundr_subproof //. - * by rewrite bnd_simp oppr_ge0. - * by rewrite opp_itv_boundr_subproof. - * by rewrite opp_itv_ge0_subproof. - * by rewrite opp_itv_boundl_subproof. - + move=> lelyy leyuy. - rewrite -[Interval _ _]/(Interval (opp (mulr (opp lx) uy)) - (mulr (opp lx) (opp ly))). - rewrite -[x * y]opprK -mulNr /Itv.itv_cond itv_boundlr. - rewrite opp_itv_boundl_subproof -mulrN. - rewrite 2?mul_itv_boundr'_subproof //. - * by rewrite bnd_simp oppr_ge0. - * by rewrite leBRight_ltBLeft opp_itv_gt0_subproof ltBRight_leBLeft ltW. - * by rewrite opp_itv_boundr_subproof. - * by rewrite opp_itv_boundr_subproof. - * by rewrite bnd_simp oppr_ge0. - * by rewrite ltW. - * by rewrite opp_itv_boundr_subproof. -- move=> lelxx lexux. - have xpos : 0 <= x. - move: (le_trans (Itv.le_map_itv_bound R lxpos) lelxx). - by rewrite /= bnd_simp. - have [leuyly|-> ->|lyneg uyneg|lypos uypos|lyneg uypos] := interval_signP. - + move=> + + /ltac:(exfalso); exact: empty10. - + rewrite 2!bnd_simp => ley1 ley2. - have -> : y = 0 by apply: le_anti; rewrite ley1 ley2. - by rewrite mulr0 /Itv.itv_cond in_itv/= lexx. - + move=> lelyy leyuy. - have yneg : y <= 0. - move: (le_trans leyuy (Itv.le_map_itv_bound R uyneg)). - by rewrite /= bnd_simp. - rewrite -[Interval _ _]/(Interval (opp (mulr ux (opp ly))) - (opp (mull lx (opp uy)))). - rewrite -[x * y]opprK -mulrN /Itv.itv_cond itv_boundlr. - rewrite opp_itv_boundl_subproof opp_itv_boundr_subproof. - rewrite mul_itv_boundr_subproof ?mul_itv_boundl_subproof //. - * by rewrite opp_itv_ge0_subproof. - * by rewrite opp_itv_boundl_subproof. - * by rewrite bnd_simp oppr_ge0. - * by rewrite opp_itv_boundr_subproof. - + move=> lelyy leyuy. - have ypos : 0 <= y. - move: (le_trans (Itv.le_map_itv_bound R lypos) lelyy). - by rewrite /= bnd_simp. - rewrite -[Interval _ _]/(Interval (mull lx ly) (mulr ux uy)). - rewrite /Itv.itv_cond itv_boundlr. - by rewrite mul_itv_boundr_subproof ?mul_itv_boundl_subproof. - + move=> lelyy leyuy. - rewrite -[Interval _ _]/(Interval (opp (mulr ux (opp ly))) (mulr ux uy)). - rewrite -[x * y]opprK -mulrN /Itv.itv_cond itv_boundlr. - rewrite opp_itv_boundl_subproof -mulrN opprK. - rewrite 2?mul_itv_boundr'_subproof //. - * by rewrite ltW. - * by rewrite leBRight_ltBLeft opp_itv_gt0_subproof ltBRight_leBLeft ltW. - * by rewrite opp_itv_boundr_subproof. -- move=> lelxx lexux. - have [leuyly|-> ->|lyneg uyneg|lypos uypos|lyneg uypos] := interval_signP. - + move=> + + /ltac:(exfalso); exact: empty10. - + rewrite 2!bnd_simp => ley1 ley2. - have -> : y = 0 by apply: le_anti; rewrite ley1 ley2. - by rewrite mulr0 /Itv.itv_cond in_itv/= lexx. - + move=> lelyy leyuy. - have yneg : y <= 0. - move: (le_trans leyuy (Itv.le_map_itv_bound R uyneg)). - by rewrite /= bnd_simp. - rewrite -[Interval _ _]/(Interval (opp (mulr ux (opp ly))) - (mulr (opp lx) (opp ly))). - rewrite -[x * y]opprK -mulrN /Itv.itv_cond itv_boundlr. - rewrite /mulr mul_itv_boundrC_subproof mulrC opp_itv_boundl_subproof. - rewrite [in X in _ && X]mul_itv_boundrC_subproof -mulrN. - rewrite mul_itv_boundr'_subproof ?mul_itv_boundr'_subproof //. - * by rewrite bnd_simp oppr_ge0. - * by rewrite leBRight_ltBLeft opp_itv_gt0_subproof ltBRight_leBLeft ltW. - * by rewrite opp_itv_boundr_subproof. - * by rewrite opp_itv_boundr_subproof. - * by rewrite bnd_simp oppr_ge0. - * by rewrite ltW. - * by rewrite opp_itv_boundr_subproof. - + move=> lelyy leyuy. - have ypos : 0 <= y. - move: (le_trans (Itv.le_map_itv_bound R lypos) lelyy). - by rewrite /= bnd_simp. - rewrite -[Interval _ _]/(Interval (opp (mulr (opp lx) uy)) (mulr ux uy)). - rewrite -[x * y]opprK -mulNr /Itv.itv_cond itv_boundlr. - rewrite /mulr mul_itv_boundrC_subproof mulrC opp_itv_boundl_subproof. - rewrite [in X in _ && X]mul_itv_boundrC_subproof -mulrN opprK. - rewrite mul_itv_boundr'_subproof ?mul_itv_boundr'_subproof //. - * by rewrite ltW. - * by rewrite leBRight_ltBLeft opp_itv_gt0_subproof ltBRight_leBLeft ltW. - * by rewrite opp_itv_boundr_subproof. - + move=> lelyy leyuy. - rewrite -[Interval _ _]/(Interval - (Order.min (opp (mulr (opp lx) uy)) - (opp (mulr ux (opp ly)))) - (Order.max (mulr (opp lx) (opp ly)) - (mulr ux uy))). - rewrite /Itv.itv_cond itv_boundlr. - rewrite map_itv_bound_min map_itv_bound_max ge_min le_max. - rewrite -[x * y]opprK !opp_itv_boundl_subproof. - rewrite -[in X in ((X || _) && _)]mulNr -[in X in ((_ || X) && _)]mulrN. - rewrite -[in X in (_ && (X || _))]mulrNN !opprK. - have [xpos|xneg] := leP 0 x. - * rewrite [in X in ((_ || X) && _)]mul_itv_boundr'_subproof ?orbT //=; - rewrite ?[in X in (_ || X)]mul_itv_boundr'_subproof ?orbT //. - - by rewrite ltW. - - by rewrite leBRight_ltBLeft opp_itv_gt0_subproof ltBRight_leBLeft ltW. - - by rewrite opp_itv_boundr_subproof. - * rewrite [in X in ((X || _) && _)]mul_itv_boundr'_subproof //=; - rewrite ?[in X in (X || _)]mul_itv_boundr'_subproof //. - - by rewrite bnd_simp oppr_ge0 ltW. - - by rewrite leBRight_ltBLeft opp_itv_gt0_subproof ltBRight_leBLeft ltW. - - by rewrite opp_itv_boundr_subproof. - - by rewrite opp_itv_boundr_subproof. - - by rewrite bnd_simp oppr_ge0 ltW. - - by rewrite ltW. - - by rewrite opp_itv_boundr_subproof. -Qed. - -Canonical mul_inum (xi yi : interval int) - (x : {itv R & xi}) (y : {itv R & yi}) := + num_itv_bound R (Order.max x y) + = Order.max (num_itv_bound R x) (num_itv_bound R y). +Proof. +have [lexy | ltyx] := leP x y; [by rewrite !maxEle intr_le_map_itv_bound lexy|]. +rewrite maxElt -if_neg -comparable_leNgt ?intr_le_map_itv_bound ?ltW//. +exact: comparable_num_itv_bound_subproof. +Qed. + +Lemma mul_inum_subproof (xi yi : Itv.t) (x : num_def R xi) (y : num_def R yi) + (r := itv_real2_subdef mul_itv_subdef xi yi) : + num_spec r (x%:inum * y%:inum). +Proof. +rewrite {}/r; case: xi yi x y => [//| [xl xu]] [//| [yl yu]]. +case=> [x /=/and3P[xr /= xlx xxu]] [y /=/and3P[yr /= yly yyu]]. +rewrite -/(interval_sign (Interval xl xu)) -/(interval_sign (Interval yl yu)). +have ns000 : @Itv.num_sem R `[0, 0] 0 by apply/and3P. +have xyr : x * y \in Num.real by exact: realM. +case: (interval_signP xlx xxu xr) => xlb xub xs. +- by rewrite xs mul0r; case: (interval_signP yly yyu yr). +- case: (interval_signP yly yyu yr) => ylb yub ys. + + by rewrite ys mulr0. + + apply/and3P; split=> //=. + * exact: mul_itv_boundl_subproof xlx yly. + * exact: mul_itv_boundr_subproof xxu yyu. + + apply/and3P; split=> //=; rewrite -[x * y]opprK -mulrN. + * rewrite opp_itv_boundl_subproof. + by rewrite mul_itv_boundr_subproof ?oppr_ge0// opp_itv_boundr_subproof. + * rewrite opp_itv_boundr_subproof. + rewrite mul_itv_boundl_subproof ?opp_itv_boundl_subproof//. + by rewrite opp_itv_ge0_subproof. + + apply/and3P; split=> //=. + * rewrite -[x * y]opprK -mulrN opp_itv_boundl_subproof. + rewrite mul_itv_boundr'_subproof ?realN ?opp_itv_boundr_subproof//. + by rewrite opp_itv_gt0_subproof ltW. + * by rewrite mul_itv_boundr'_subproof// ltW. +- case: (interval_signP yly yyu yr) => ylb yub ys. + + by rewrite ys mulr0. + + apply/and3P; split=> //=; rewrite -[x * y]opprK -mulNr. + * rewrite opp_itv_boundl_subproof. + by rewrite mul_itv_boundr_subproof ?oppr_ge0 ?opp_itv_boundr_subproof. + * rewrite opp_itv_boundr_subproof. + rewrite mul_itv_boundl_subproof ?opp_itv_boundl_subproof//. + by rewrite opp_itv_ge0_subproof. + + apply/and3P; split=> //=; rewrite -mulrNN. + * by rewrite mul_itv_boundl_subproof + ?opp_itv_ge0_subproof ?opp_itv_boundl_subproof. + * by rewrite mul_itv_boundr_subproof ?oppr_ge0 ?opp_itv_boundr_subproof. + + apply/and3P; split=> //=; rewrite -[x * y]opprK. + * rewrite -mulNr opp_itv_boundl_subproof. + rewrite mul_itv_boundr'_subproof ?oppr_ge0 ?opp_itv_boundr_subproof//. + exact: ltW. + * rewrite opprK -mulrNN. + by rewrite mul_itv_boundr'_subproof ?opp_itv_boundr_subproof + ?oppr_ge0 ?realN ?opp_itv_gt0_subproof// ltW. +- case: (interval_signP yly yyu yr) => ylb yub ys. + + by rewrite ys mulr0. + + apply/and3P; split=> //=; rewrite mulrC mul_itv_boundrC_subproof. + * rewrite -[y * x]opprK -mulrN opp_itv_boundl_subproof. + rewrite mul_itv_boundr'_subproof ?oppr_ge0 ?realN + ?opp_itv_boundr_subproof//. + by rewrite opp_itv_gt0_subproof ltW. + * by rewrite mul_itv_boundr'_subproof// ltW. + + apply/and3P; split=> //=; rewrite mulrC mul_itv_boundrC_subproof. + * rewrite -[y * x]opprK -mulNr opp_itv_boundl_subproof. + rewrite mul_itv_boundr'_subproof ?oppr_ge0 ?opp_itv_boundr_subproof//. + exact: ltW. + * rewrite -mulrNN mul_itv_boundr'_subproof ?oppr_ge0 ?realN + ?opp_itv_boundr_subproof//. + by rewrite opp_itv_gt0_subproof ltW. +apply/and3P; rewrite xyr/= map_itv_bound_min map_itv_bound_max. +rewrite (comparable_ge_min _ (comparable_num_itv_bound_subproof _ _)). +rewrite (comparable_le_max _ (comparable_num_itv_bound_subproof _ _)). +case: (comparable_leP xr) => [x0 | /ltW x0]; split=> //. +- apply/orP; right; rewrite -[x * y]opprK -mulrN opp_itv_boundl_subproof. + rewrite mul_itv_boundr'_subproof ?realN ?opp_itv_boundr_subproof//. + by rewrite opp_itv_gt0_subproof ltW. +- by apply/orP; right; rewrite mul_itv_boundr'_subproof// ltW. +- apply/orP; left; rewrite -[x * y]opprK -mulNr opp_itv_boundl_subproof. + by rewrite mul_itv_boundr'_subproof ?oppr_ge0 ?opp_itv_boundr_subproof// ltW. +- apply/orP; left; rewrite -mulrNN. + rewrite mul_itv_boundr'_subproof ?oppr_ge0 ?realN ?opp_itv_boundr_subproof//. + by rewrite opp_itv_gt0_subproof ltW. +Qed. + +Canonical mul_inum (xi yi : Itv.t) (x : num_def R xi) (y : num_def R yi) := Itv.mk (mul_inum_subproof x y). -End RealDomainStability. +End NumDomainInstances. Section Morph. -Context {R : numDomainType} {i : interval int}. -Local Notation nR := {itv R & i}. +Context {R : numDomainType} {i : Itv.t}. +Local Notation nR := (num_def R i). Implicit Types x y : nR. -Local Notation inum := (@inum R i). +Local Notation inum := (@inum R (@Itv.num_sem R) i). Lemma inum_eq : {mono inum : x y / x == y}. Proof. by []. Qed. Lemma inum_le : {mono inum : x y / (x <= y)%O}. Proof. by []. Qed. Lemma inum_lt : {mono inum : x y / (x < y)%O}. Proof. by []. Qed. +Lemma inum_min : {morph inum : x y / Order.min x y}. +Proof. by move=> x y; rewrite !minEle inum_le -fun_if. Qed. +Lemma inum_max : {morph inum : x y / Order.max x y}. +Proof. by move=> x y; rewrite !maxEle inum_le -fun_if. Qed. End Morph. +Section MorphReal. +Context {R : numDomainType} {i : interval int}. +Local Notation nR := (num_def R (Itv.Real i)). +Implicit Type x y : nR. +Local Notation num := (@inum R (@Itv.num_sem R) i). + +Lemma num_le_max a x y : + a <= Num.max x%:inum y%:inum = (a <= x%:inum) || (a <= y%:inum). +Proof. by rewrite -comparable_le_max// real_comparable. Qed. + +Lemma num_ge_max a x y : + Num.max x%:inum y%:inum <= a = (x%:inum <= a) && (y%:inum <= a). +Proof. by rewrite -comparable_ge_max// real_comparable. Qed. + +Lemma num_le_min a x y : + a <= Num.min x%:inum y%:inum = (a <= x%:inum) && (a <= y%:inum). +Proof. by rewrite -comparable_le_min// real_comparable. Qed. + +Lemma num_ge_min a x y : + Num.min x%:inum y%:inum <= a = (x%:inum <= a) || (y%:inum <= a). +Proof. by rewrite -comparable_ge_min// real_comparable. Qed. + +Lemma num_lt_max a x y : + a < Num.max x%:inum y%:inum = (a < x%:inum) || (a < y%:inum). +Proof. by rewrite -comparable_lt_max// real_comparable. Qed. + +Lemma num_gt_max a x y : + Num.max x%:inum y%:inum < a = (x%:inum < a) && (y%:inum < a). +Proof. by rewrite -comparable_gt_max// real_comparable. Qed. + +Lemma num_lt_min a x y : + a < Num.min x%:inum y%:inum = (a < x%:inum) && (a < y%:inum). +Proof. by rewrite -comparable_lt_min// real_comparable. Qed. + +Lemma num_gt_min a x y : + Num.min x%:inum y%:inum < a = (x%:inum < a) || (y%:inum < a). +Proof. by rewrite -comparable_gt_min// real_comparable. Qed. + +End MorphReal. + +Section ItvNum. +Context (R : numDomainType). +Context (x : R) (l u : itv_bound int). +Context (x_real : x \in Num.real). +Context (l_le_x : (num_itv_bound R l <= BLeft x)%O). +Context (x_le_u : (BRight x <= num_itv_bound R u)%O). +Lemma itvnum_subdef : num_spec (Itv.Real (Interval l u)) x. +Proof. by apply/and3P. Qed. +Definition ItvNum : num_def R (Itv.Real (Interval l u)) := Itv.mk itvnum_subdef. +End ItvNum. + +Section ItvReal. +Context (R : realDomainType). +Context (x : R) (l u : itv_bound int). +Context (l_le_x : (num_itv_bound R l <= BLeft x)%O). +Context (x_le_u : (BRight x <= num_itv_bound R u)%O). +Lemma itvreal_subdef : num_spec (Itv.Real (Interval l u)) x. +Proof. by apply/and3P; split; first exact: num_real. Qed. +Definition ItvReal : num_def R (Itv.Real (Interval l u)) := + Itv.mk itvreal_subdef. +End ItvReal. + +Section Itv01. +Context (R : numDomainType). +Context (x : R) (x_ge0 : 0 <= x) (x_le1 : x <= 1). +Lemma itv01_subdef : num_spec (Itv.Real `[0%Z, 1%Z]) x. +Proof. by apply/and3P; split; rewrite ?bnd_simp// ger0_real. Qed. +Definition Itv01 : num_def R (Itv.Real `[0%Z, 1%Z]) := Itv.mk itv01_subdef. +End Itv01. + Section Test1. Variable R : numDomainType. @@ -891,7 +1028,7 @@ Lemma s_of_p0 (p : {i01 R}) : s_of_pq p 0%:i01 = p. Proof. by apply/val_inj; rewrite /= subr0 mulr1 subKr. Qed. Canonical onem_itv01 (p : {i01 R}) : {i01 R} := - @Itv.mk _ _ (onem p%:inum) [itv of 1 - p%:inum]. + @Itv.mk _ _ _ (onem p%:inum) [itv of 1 - p%:inum]. Definition s_of_pq' (p q : {i01 R}) : {i01 R} := (`1- (`1-(p%:inum) * `1-(q%:inum)))%:i01. diff --git a/theories/convex.v b/theories/convex.v index dde76d9a1..591d0aa19 100644 --- a/theories/convex.v +++ b/theories/convex.v @@ -185,7 +185,7 @@ Let convexf_ptP : a < b -> (forall x, a <= x <= b -> 0 <= L x - f x) -> forall t, f (a <| t |> b) <= f a <| t |> f b. Proof. move=> ab h t; set x := a <| t |> b; have /h : a <= x <= b. - by rewrite -(conv1 a b) -{1}(conv0 a b) /x !le_line_path//= itv_ge0/=. + by rewrite -(conv1 a b) -{1}(conv0 a b) /x !le_line_path//= ge0/=. rewrite subr_ge0 => /le_trans; apply. by rewrite LE// /x line_pathK ?lt_eqF// convC line_pathK ?gt_eqF. Qed. diff --git a/theories/exp.v b/theories/exp.v index 3b8e397da..8f709ed49 100644 --- a/theories/exp.v +++ b/theories/exp.v @@ -968,11 +968,10 @@ rewrite le_eqVlt => /predU1P[<- b0 p0 q0 _|a0]. by rewrite mul0r powR0 ?gt_eqF// mul0r add0r divr_ge0 ?powR_ge0 ?ltW. rewrite le_eqVlt => /predU1P[<-|b0] p0 q0 pq. by rewrite mulr0 powR0 ?gt_eqF// mul0r addr0 divr_ge0 ?powR_ge0 ?ltW. -have q01 : (q^-1 \in `[0, 1])%R. - by rewrite in_itv/= invr_ge0 (ltW q0)/= -pq ler_wpDl// invr_ge0 ltW. +have iq1 : q^-1 <= 1 by rewrite -pq ler_wpDl// invr_ge0 ltW. have ap0 : (0 < a `^ p)%R by rewrite powR_gt0. have bq0 : (0 < b `^ q)%R by rewrite powR_gt0. -have := @concave_ln _ (@Itv.mk _ `[0, 1] _ q01)%R _ _ ap0 bq0. +have := @concave_ln _ (Itv01 (eqbRL (invr_ge0 _) (ltW q0)) iq1) _ _ ap0 bq0. have pq' : (p^-1 = 1 - q^-1)%R by rewrite -pq addrK. rewrite !convRE/= /onem -pq' -[_ <= ln _]ler_expR expRD (mulrC p^-1). rewrite ln_powR mulrAC divff ?mul1r ?gt_eqF// (mulrC q^-1). diff --git a/theories/hoelder.v b/theories/hoelder.v index 346c0cb48..b7476215d 100644 --- a/theories/hoelder.v +++ b/theories/hoelder.v @@ -347,8 +347,8 @@ move=> p1; rewrite (@le_trans _ _ ((2^-1 * `| f x | + 2^-1 * `| g x |) `^ p))//. rewrite ge0_ler_powR ?nnegrE ?(le_trans _ p1)//. by rewrite (le_trans (ler_normD _ _))// 2!normrM ger0_norm. rewrite {1 3}(_ : 2^-1 = 1 - 2^-1); last by rewrite {2}(splitr 1) div1r addrK. -rewrite (@convex_powR _ _ p1 (@Itv.mk _ _ _ _)) ?inE/= ?in_itv/= ?normr_ge0//. -by rewrite /Itv.itv_cond/= in_itv/= invr_ge0 ler0n invf_le1 ?ler1n. +rewrite (@convex_powR _ _ p1 (Itv01 _ _))// ?inE/= ?in_itv/= ?normr_ge0 ?invr_ge0//. +by rewrite invf_le1 ?ler1n. Qed. Let measurableT_comp_powR f p : From 8de0e98ad0871073325a30c3aca46ca763d491ff Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Sun, 24 Nov 2024 21:19:49 +0100 Subject: [PATCH 07/18] Replace notation %:inum with %:num --- CHANGELOG_UNRELEASED.md | 8 ++++ reals/itv.v | 96 +++++++++++++++++++++-------------------- 2 files changed, 57 insertions(+), 47 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index c35f7744c..5a4293185 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -13,6 +13,8 @@ - in `itv.v` + lemmas `cmp0`, `neq0`, `eq0F` + definitions `ItvReal` and `Itv01` + + lemmas `cmp0`, `neq0`, `eq0F`, `num_min`, `num_max` + + notation `%:num` - in `constructive_ereal.v` + lemmas `cmp0y`, `cmp0Ny`, `real_miney`, `real_minNye`, @@ -37,6 +39,9 @@ + `itv_le0` -> `le0` + `itv_gt0F` -> `gt0F` + `itv_top_typ` -> `top_typ` + + `inum_eq` -> `num_eq` + + `inum_le` -> `num_le` + + `inum_lt` -> `num_lt` ### Generalized @@ -47,6 +52,9 @@ ### Deprecated +- in `itv.v`: + + notation `%:inum` (use `%:num` instead) + ### Removed ### Infrastructure diff --git a/reals/itv.v b/reals/itv.v index 706855742..d54bd82b8 100644 --- a/reals/itv.v +++ b/reals/itv.v @@ -12,8 +12,8 @@ From mathcomp Require Import mathcomp_extra boolp. (* a known interval easier, thanks to canonical structures. This adds types *) (* like {itv R & `[a, b]}, a notation e%:itv that infers an enclosing *) (* interval for expression e according to existing canonical instances and *) -(* %:inum to cast back from type {itv R & i} to R. *) -(* For instance, for x : {i01 R}, we have (1 - x%:inum)%:itv : {i01 R} *) +(* %:num to cast back from type {itv R & i} to R. *) +(* For instance, for x : {i01 R}, we have (1 - x%:num)%:itv : {i01 R} *) (* automatically inferred. *) (* *) (* ## types for values within known interval *) @@ -35,7 +35,7 @@ From mathcomp Require Import mathcomp_extra boolp. (* according to existing canonical instances. *) (* x%:i01 == explicitly casts x to {i01 R} according to existing *) (* canonical instances. *) -(* x%:inum == explicit cast from {itv R & i} to R. *) +(* x%:num == explicit cast from {itv R & i} to R. *) (* ``` *) (* *) (* ## sign proofs *) @@ -77,6 +77,7 @@ Reserved Notation "{ 'i01' R }" Reserved Notation "x %:itv" (at level 2, format "x %:itv"). Reserved Notation "x %:i01" (at level 2, format "x %:i01"). Reserved Notation "x %:inum" (at level 2, format "x %:inum"). +Reserved Notation "x %:num" (at level 2, format "x %:num"). Reserved Notation "[ 'itv' 'of' x ]" (format "[ 'itv' 'of' x ]"). @@ -146,8 +147,9 @@ Notation "{ 'itv' R & i }" := (def (@num_sem R) (Itv.Real i%Z)) : type_scope. Notation "{ 'i01' R }" := {itv R & `[0, 1]} : type_scope. Notation "x %:itv" := (from (Phantom _ x)) : ring_scope. Notation "[ 'itv' 'of' x ]" := (fromP (Phantom _ x)) : ring_scope. -Notation inum := r. -Notation "x %:inum" := (r x) : ring_scope. +Notation num := r. +Notation "x %:inum" := (r x) (only parsing) : ring_scope. +Notation "x %:num" := (r x) : ring_scope. End Exports. End Itv. Export Itv.Exports. @@ -306,62 +308,62 @@ case: x => x /= /[swap] /subitv_map_itv /[apply] /andP[_] /=. by rewrite in_itv/= => /andP[] /le_trans /[apply]; rewrite ler10. Qed. -Lemma gt0 x : unify_itv i (Itv.Real `]Posz 0, +oo[) -> 0%R < x%:inum :> R. +Lemma gt0 x : unify_itv i (Itv.Real `]Posz 0, +oo[) -> 0%R < x%:num :> R. Proof. case: x => x /= /[swap] /subitv_map_itv /[apply] /andP[_]. by rewrite /= in_itv/= andbT. Qed. Lemma le0F x : unify_itv i (Itv.Real `]Posz 0, +oo[) -> - x%:inum <= 0%R :> R = false. + x%:num <= 0%R :> R = false. Proof. case: x => x /= /[swap] /subitv_map_itv /[apply] /andP[_] /=. by rewrite in_itv/= andbT => /lt_geF. Qed. -Lemma lt0 x : unify_itv i (Itv.Real `]-oo, Posz 0[) -> x%:inum < 0%R :> R. +Lemma lt0 x : unify_itv i (Itv.Real `]-oo, Posz 0[) -> x%:num < 0%R :> R. Proof. by case: x => x /= /[swap] /subitv_map_itv /[apply] /andP[_] /=; rewrite in_itv. Qed. Lemma ge0F x : unify_itv i (Itv.Real `]-oo, Posz 0[) -> - 0%R <= x%:inum :> R = false. + 0%R <= x%:num :> R = false. Proof. case: x => x /= /[swap] /subitv_map_itv /[apply] /andP[_] /=. by rewrite in_itv/= => /lt_geF. Qed. -Lemma ge0 x : unify_itv i (Itv.Real `[Posz 0, +oo[) -> 0%R <= x%:inum :> R. +Lemma ge0 x : unify_itv i (Itv.Real `[Posz 0, +oo[) -> 0%R <= x%:num :> R. Proof. case: x => x /= /[swap] /subitv_map_itv /[apply] /andP[_] /=. by rewrite in_itv/= andbT. Qed. Lemma lt0F x : unify_itv i (Itv.Real `[Posz 0, +oo[) -> - x%:inum < 0%R :> R = false. + x%:num < 0%R :> R = false. Proof. case: x => x /= /[swap] /subitv_map_itv /[apply] /andP[_] /=. by rewrite in_itv/= andbT => /le_gtF. Qed. -Lemma le0 x : unify_itv i (Itv.Real `]-oo, Posz 0]) -> x%:inum <= 0%R :> R. +Lemma le0 x : unify_itv i (Itv.Real `]-oo, Posz 0]) -> x%:num <= 0%R :> R. Proof. by case: x => x /= /[swap] /subitv_map_itv /[apply] /andP[_] /=; rewrite in_itv. Qed. Lemma gt0F x : unify_itv i (Itv.Real `]-oo, Posz 0]) -> - 0%R < x%:inum :> R = false. + 0%R < x%:num :> R = false. Proof. case: x => x /= /[swap] /subitv_map_itv /[apply] /andP[_] /=. by rewrite in_itv/= => /le_gtF. Qed. -Lemma cmp0 x : unify_itv i (Itv.Real `]-oo, +oo[) -> (0 >=< x%:inum). +Lemma cmp0 x : unify_itv i (Itv.Real `]-oo, +oo[) -> (0 >=< x%:num). Proof. by case: i x => [//| i' [x /=/andP[]]]. Qed. Lemma neq0 x : unify (fun ix iy => negb (Itv.sub ix iy)) (Itv.Real `[0%Z, 0%Z]) i -> - x%:inum != 0 :> R. + x%:num != 0 :> R. Proof. case: i x => [//| [l u] [x /= Px]]; apply: contra => /eqP x0 /=. move: Px; rewrite x0 => /and3P[_ /= l0 u0]; apply/andP; split. @@ -371,34 +373,34 @@ Qed. Lemma eq0F x : unify (fun ix iy => negb (Itv.sub ix iy)) (Itv.Real `[0%Z, 0%Z]) i -> - x%:inum == 0 :> R = false. + x%:num == 0 :> R = false. Proof. by move=> u; apply/negbTE/neq0. Qed. -Lemma lt1 x : unify_itv i (Itv.Real `]-oo, Posz 1[) -> x%:inum < 1%R :> R. +Lemma lt1 x : unify_itv i (Itv.Real `]-oo, Posz 1[) -> x%:num < 1%R :> R. Proof. by case: x => x /= /[swap] /subitv_map_itv /[apply] /andP[_] /=; rewrite in_itv. Qed. Lemma ge1F x : unify_itv i (Itv.Real `]-oo, Posz 1[) -> - 1%R <= x%:inum :> R = false. + 1%R <= x%:num :> R = false. Proof. case: x => x /= /[swap] /subitv_map_itv /[apply] /andP[_] /=. by rewrite in_itv/= => /lt_geF. Qed. -Lemma le1 x : unify_itv i (Itv.Real `]-oo, Posz 1]) -> x%:inum <= 1%R :> R. +Lemma le1 x : unify_itv i (Itv.Real `]-oo, Posz 1]) -> x%:num <= 1%R :> R. Proof. by case: x => x /= /[swap] /subitv_map_itv /[apply] /andP[_] /=; rewrite in_itv. Qed. Lemma gt1F x : unify_itv i (Itv.Real `]-oo, Posz 1]) -> - 1%R < x%:inum :> R = false. + 1%R < x%:num :> R = false. Proof. case: x => x /= /[swap] /subitv_map_itv /[apply] /andP[_] /=. by rewrite in_itv/= => /le_gtF. Qed. -Lemma widen_itv_subproof x i' : Itv.sub i i' -> num_spec i' x%:inum. +Lemma widen_itv_subproof x i' : Itv.sub i i' -> num_spec i' x%:num. Proof. by case: x => x /= /[swap] /subitv_map_itv; apply. Qed. Definition widen_itv x i' (uni : unify_itv i i') := @@ -496,7 +498,7 @@ Arguments opp_itv_subdef /. Lemma opp_inum_subproof (i : Itv.t) (x : num_def R i) (r := itv_real1_subdef opp_itv_subdef i) : - num_spec r (- x%:inum). + num_spec r (- x%:num). Proof. apply: itv_real1_subproof (Itv.P x). case: x => x /= _ [l u] /and3P[xr lx xu]. @@ -551,7 +553,7 @@ Arguments add_itv_subdef /. Lemma add_inum_subproof (xi yi : Itv.t) (x : num_def R xi) (y : num_def R yi) (r := itv_real2_subdef add_itv_subdef xi yi) : - num_spec r (x%:inum + y%:inum). + num_spec r (x%:num + y%:num). Proof. apply: itv_real2_subproof (Itv.P x) (Itv.P y). case: x y => [x /= _] [y /= _] => {xi yi r} -[lx ux] [ly uy]/=. @@ -822,7 +824,7 @@ Qed. Lemma mul_inum_subproof (xi yi : Itv.t) (x : num_def R xi) (y : num_def R yi) (r := itv_real2_subdef mul_itv_subdef xi yi) : - num_spec r (x%:inum * y%:inum). + num_spec r (x%:num * y%:num). Proof. rewrite {}/r; case: xi yi x y => [//| [xl xu]] [//| [yl yu]]. case=> [x /=/and3P[xr /= xlx xxu]] [y /=/and3P[yr /= yly yyu]]. @@ -905,15 +907,15 @@ Section Morph. Context {R : numDomainType} {i : Itv.t}. Local Notation nR := (num_def R i). Implicit Types x y : nR. -Local Notation inum := (@inum R (@Itv.num_sem R) i). +Local Notation num := (@num R (@Itv.num_sem R) i). -Lemma inum_eq : {mono inum : x y / x == y}. Proof. by []. Qed. -Lemma inum_le : {mono inum : x y / (x <= y)%O}. Proof. by []. Qed. -Lemma inum_lt : {mono inum : x y / (x < y)%O}. Proof. by []. Qed. -Lemma inum_min : {morph inum : x y / Order.min x y}. -Proof. by move=> x y; rewrite !minEle inum_le -fun_if. Qed. -Lemma inum_max : {morph inum : x y / Order.max x y}. -Proof. by move=> x y; rewrite !maxEle inum_le -fun_if. Qed. +Lemma num_eq : {mono num : x y / x == y}. Proof. by []. Qed. +Lemma num_le : {mono num : x y / (x <= y)%O}. Proof. by []. Qed. +Lemma num_lt : {mono num : x y / (x < y)%O}. Proof. by []. Qed. +Lemma num_min : {morph num : x y / Order.min x y}. +Proof. by move=> x y; rewrite !minEle num_le -fun_if. Qed. +Lemma num_max : {morph num : x y / Order.max x y}. +Proof. by move=> x y; rewrite !maxEle num_le -fun_if. Qed. End Morph. @@ -921,38 +923,38 @@ Section MorphReal. Context {R : numDomainType} {i : interval int}. Local Notation nR := (num_def R (Itv.Real i)). Implicit Type x y : nR. -Local Notation num := (@inum R (@Itv.num_sem R) i). +Local Notation num := (@num R (@Itv.num_sem R) i). Lemma num_le_max a x y : - a <= Num.max x%:inum y%:inum = (a <= x%:inum) || (a <= y%:inum). + a <= Num.max x%:num y%:num = (a <= x%:num) || (a <= y%:num). Proof. by rewrite -comparable_le_max// real_comparable. Qed. Lemma num_ge_max a x y : - Num.max x%:inum y%:inum <= a = (x%:inum <= a) && (y%:inum <= a). + Num.max x%:num y%:num <= a = (x%:num <= a) && (y%:num <= a). Proof. by rewrite -comparable_ge_max// real_comparable. Qed. Lemma num_le_min a x y : - a <= Num.min x%:inum y%:inum = (a <= x%:inum) && (a <= y%:inum). + a <= Num.min x%:num y%:num = (a <= x%:num) && (a <= y%:num). Proof. by rewrite -comparable_le_min// real_comparable. Qed. Lemma num_ge_min a x y : - Num.min x%:inum y%:inum <= a = (x%:inum <= a) || (y%:inum <= a). + Num.min x%:num y%:num <= a = (x%:num <= a) || (y%:num <= a). Proof. by rewrite -comparable_ge_min// real_comparable. Qed. Lemma num_lt_max a x y : - a < Num.max x%:inum y%:inum = (a < x%:inum) || (a < y%:inum). + a < Num.max x%:num y%:num = (a < x%:num) || (a < y%:num). Proof. by rewrite -comparable_lt_max// real_comparable. Qed. Lemma num_gt_max a x y : - Num.max x%:inum y%:inum < a = (x%:inum < a) && (y%:inum < a). + Num.max x%:num y%:num < a = (x%:num < a) && (y%:num < a). Proof. by rewrite -comparable_gt_max// real_comparable. Qed. Lemma num_lt_min a x y : - a < Num.min x%:inum y%:inum = (a < x%:inum) && (a < y%:inum). + a < Num.min x%:num y%:num = (a < x%:num) && (a < y%:num). Proof. by rewrite -comparable_lt_min// real_comparable. Qed. Lemma num_gt_min a x y : - Num.min x%:inum y%:inum < a = (x%:inum < a) || (y%:inum < a). + Num.min x%:num y%:num < a = (x%:num < a) || (y%:num < a). Proof. by rewrite -comparable_gt_min// real_comparable. Qed. End MorphReal. @@ -996,11 +998,11 @@ Goal 0%:i01 = 1%:i01 :> {i01 R}. Proof. Abort. -Goal (- x%:inum)%:itv = (- x%:inum)%:itv :> {itv R & `[-1, 0]}. +Goal (- x%:num)%:itv = (- x%:num)%:itv :> {itv R & `[-1, 0]}. Proof. Abort. -Goal (1 - x%:inum)%:i01 = x. +Goal (1 - x%:num)%:i01 = x. Proof. Abort. @@ -1011,7 +1013,7 @@ Section Test2. Variable R : realDomainType. Variable x y : {i01 R}. -Goal (x%:inum * y%:inum)%:i01 = x%:inum%:i01. +Goal (x%:num * y%:num)%:i01 = x%:num%:i01. Proof. Abort. @@ -1022,16 +1024,16 @@ Section Test3. Variable R : realDomainType. Definition s_of_pq (p q : {i01 R}) : {i01 R} := - (1 - ((1 - p%:inum)%:i01%:inum * (1 - q%:inum)%:i01%:inum))%:i01. + (1 - ((1 - p%:num)%:i01%:num * (1 - q%:num)%:i01%:num))%:i01. Lemma s_of_p0 (p : {i01 R}) : s_of_pq p 0%:i01 = p. Proof. by apply/val_inj; rewrite /= subr0 mulr1 subKr. Qed. Canonical onem_itv01 (p : {i01 R}) : {i01 R} := - @Itv.mk _ _ _ (onem p%:inum) [itv of 1 - p%:inum]. + @Itv.mk _ _ _ (onem p%:num) [itv of 1 - p%:num]. Definition s_of_pq' (p q : {i01 R}) : {i01 R} := - (`1- (`1-(p%:inum) * `1-(q%:inum)))%:i01. + (`1- (`1-(p%:num) * `1-(q%:num)))%:i01. End Test3. End Test3. From 7e45cebd03cd204d92b79f0a7415101e2cadf701 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Sun, 24 Nov 2024 21:11:08 +0100 Subject: [PATCH 08/18] Retrieve posnum and nonneg interfaces from signed into itv --- CHANGELOG_UNRELEASED.md | 4 ++ reals/itv.v | 96 +++++++++++++++++++++++++++++++++++++++++ 2 files changed, 100 insertions(+) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 5a4293185..70a6cb529 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -15,6 +15,10 @@ + 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`, diff --git a/reals/itv.v b/reals/itv.v index d54bd82b8..e43723cec 100644 --- a/reals/itv.v +++ b/reals/itv.v @@ -27,6 +27,8 @@ From mathcomp Require Import mathcomp_extra boolp. (* (see interval.v for notations that can be sused for i). *) (* R must have a numDomainType structure. This type is shown *) (* to be a porderType. *) +(* {posnum R} := {itv R & `]0, +oo[) *) +(* {nonneg R} := {itv R & `[0, +oo[) *) (* ``` *) (* *) (* ## casts from/to values within known interval *) @@ -35,12 +37,24 @@ From mathcomp Require Import mathcomp_extra boolp. (* according to existing canonical instances. *) (* x%:i01 == explicitly casts x to {i01 R} according to existing *) (* canonical instances. *) +(* x%:pos == explicitly casts x to {posnum R} according to existing *) +(* canonical instances. *) +(* x%:nng == explicitly casts x to {nonneg R} according to existing *) +(* canonical instances. *) (* x%:num == explicit cast from {itv R & i} to R. *) +(* x%:posnum == explicit cast from {posnum R} to R. *) +(* x%:nngnum == explicit cast from {nonneg R} to R. *) (* ``` *) (* *) (* ## sign proofs *) (* ``` *) (* [itv of x] == proof that x is in interval inferred by x%:itv *) +(* [gt0 of x] == proof that x > 0 *) +(* [lt0 of x] == proof that x < 0 *) +(* [ge0 of x] == proof that x >= 0 *) +(* [le0 of x] == proof that x <= 0 *) +(* [cmp0 of x] == proof that 0 >=< x *) +(* [neq0 of x] == proof that x != 0 *) (* ``` *) (* *) (* ## constructors *) @@ -57,6 +71,8 @@ From mathcomp Require Import mathcomp_extra boolp. (* and l u : itv_bound int *) (* Itv01 x0 x1 == builds a {i01 R} from proofs x0 : 0 <= x and x1 : x <= 1*) (* where x : R with R : numDomainType *) +(* PosNum x0 == builds a {posnum R} from a proof x0 : x > 0 where x : R *) +(* NngNum x0 == builds a {posnum R} from a proof x0 : x >= 0 where x : R*) (* ``` *) (* *) (* A number of canonical instances are provided for common operations, if *) @@ -73,13 +89,25 @@ Reserved Notation "{ 'itv' R & i }" (at level 0, R at level 200, i at level 200, format "{ 'itv' R & i }"). Reserved Notation "{ 'i01' R }" (at level 0, R at level 200, format "{ 'i01' R }"). +Reserved Notation "{ 'posnum' R }" (at level 0, format "{ 'posnum' R }"). +Reserved Notation "{ 'nonneg' R }" (at level 0, format "{ 'nonneg' R }"). Reserved Notation "x %:itv" (at level 2, format "x %:itv"). Reserved Notation "x %:i01" (at level 2, format "x %:i01"). +Reserved Notation "x %:pos" (at level 2, format "x %:pos"). +Reserved Notation "x %:nng" (at level 2, format "x %:nng"). Reserved Notation "x %:inum" (at level 2, format "x %:inum"). Reserved Notation "x %:num" (at level 2, format "x %:num"). +Reserved Notation "x %:posnum" (at level 2, format "x %:posnum"). +Reserved Notation "x %:nngnum" (at level 2, format "x %:nngnum"). Reserved Notation "[ 'itv' 'of' x ]" (format "[ 'itv' 'of' x ]"). +Reserved Notation "[ 'gt0' 'of' x ]" (format "[ 'gt0' 'of' x ]"). +Reserved Notation "[ 'lt0' 'of' x ]" (format "[ 'lt0' 'of' x ]"). +Reserved Notation "[ 'ge0' 'of' x ]" (format "[ 'ge0' 'of' x ]"). +Reserved Notation "[ 'le0' 'of' x ]" (format "[ 'le0' 'of' x ]"). +Reserved Notation "[ 'cmp0' 'of' x ]" (format "[ 'cmp0' 'of' x ]"). +Reserved Notation "[ 'neq0' 'of' x ]" (format "[ 'neq0' 'of' x ]"). Set Implicit Arguments. Unset Strict Implicit. @@ -141,15 +169,25 @@ Definition num_sem (R : numDomainType) (i : interval int) (x : R) : bool := Definition nat_sem (i : interval int) (x : nat) : bool := Posz x \in i. +Definition posnum (R : numDomainType) of phant R := + def (@num_sem R) (Real `]0, +oo[). + +Definition nonneg (R : numDomainType) of phant R := + def (@num_sem R) (Real `[0, +oo[). + Module Exports. Arguments r {T sem i}. Notation "{ 'itv' R & i }" := (def (@num_sem R) (Itv.Real i%Z)) : type_scope. Notation "{ 'i01' R }" := {itv R & `[0, 1]} : type_scope. +Notation "{ 'posnum' R }" := (@posnum _ (Phant R)) : ring_scope. +Notation "{ 'nonneg' R }" := (@nonneg _ (Phant R)) : ring_scope. Notation "x %:itv" := (from (Phantom _ x)) : ring_scope. Notation "[ 'itv' 'of' x ]" := (fromP (Phantom _ x)) : ring_scope. Notation num := r. Notation "x %:inum" := (r x) (only parsing) : ring_scope. Notation "x %:num" := (r x) : ring_scope. +Notation "x %:posnum" := (@r _ _ (Itv.Real `]0%Z, +oo[) x) : ring_scope. +Notation "x %:nngnum" := (@r _ _ (Itv.Real `[0%Z, +oo[) x) : ring_scope. End Exports. End Itv. Export Itv.Exports. @@ -409,6 +447,14 @@ Definition widen_itv x i' (uni : unify_itv i i') := Lemma widen_itvE x (uni : unify_itv i i) : @widen_itv x i uni = x. Proof. exact/val_inj. Qed. +Lemma posE x (uni : unify_itv i (Itv.Real `]0%Z, +oo[)) : + (widen_itv x%:num%:itv uni)%:num = x%:num. +Proof. by []. Qed. + +Lemma nngE x (uni : unify_itv i (Itv.Real `[0%Z, +oo[)) : + (widen_itv x%:num%:itv uni)%:num = x%:num. +Proof. by []. Qed. + End NumDomainTheory. Arguments bottom {R i} _ {_}. @@ -429,6 +475,15 @@ Arguments le1 {R i} _ {_}. Arguments gt1F {R i} _ {_}. Arguments widen_itv {R i} _ {_ _}. Arguments widen_itvE {R i} _ {_}. +Arguments posE {R i} _ {_}. +Arguments nngE {R i} _ {_}. + +Notation "[ 'gt0' 'of' x ]" := (ltac:(refine (gt0 x%:itv))). +Notation "[ 'lt0' 'of' x ]" := (ltac:(refine (lt0 x%:itv))). +Notation "[ 'ge0' 'of' x ]" := (ltac:(refine (ge0 x%:itv))). +Notation "[ 'le0' 'of' x ]" := (ltac:(refine (le0 x%:itv))). +Notation "[ 'cmp0' 'of' x ]" := (ltac:(refine (cmp0 x%:itv))). +Notation "[ 'neq0' 'of' x ]" := (ltac:(refine (neq0 x%:itv))). #[export] Hint Extern 0 (is_true (0%R < _)%R) => solve [apply: gt0] : core. #[export] Hint Extern 0 (is_true (_ < 0%R)%R) => solve [apply: lt0] : core. @@ -445,6 +500,16 @@ Notation "x %:i01" := (widen_itv x%:itv : {i01 _}) (only parsing) : ring_scope. Notation "x %:i01" := (@widen_itv _ _ (@Itv.from _ _ _ (Phantom _ x)) (Itv.Real `[Posz 0, Posz 1]) _) (only printing) : ring_scope. +Notation "x %:pos" := (widen_itv x%:itv : {posnum _}) (only parsing) + : ring_scope. +Notation "x %:pos" := (@widen_itv _ _ + (@Itv.from _ _ _ (Phantom _ x)) (Itv.Real `]Posz 0, +oo[) _) + (only printing) : ring_scope. +Notation "x %:nng" := (widen_itv x%:itv : {nonneg _}) (only parsing) + : ring_scope. +Notation "x %:nng" := (@widen_itv _ _ + (@Itv.from _ _ _ (Phantom _ x)) (Itv.Real `[Posz 0, +oo[) _) + (only printing) : ring_scope. Local Open Scope ring_scope. @@ -989,6 +1054,37 @@ Proof. by apply/and3P; split; rewrite ?bnd_simp// ger0_real. Qed. Definition Itv01 : num_def R (Itv.Real `[0%Z, 1%Z]) := Itv.mk itv01_subdef. End Itv01. +Section Posnum. +Context (R : numDomainType) (x : R) (x_gt0 : 0 < x). +Lemma posnum_subdef : num_spec (Itv.Real `]0, +oo[) x. +Proof. by apply/and3P; rewrite /= gtr0_real. Qed. +Definition PosNum : {posnum R} := Itv.mk posnum_subdef. +End Posnum. + +Section Nngnum. +Context (R : numDomainType) (x : R) (x_ge0 : 0 <= x). +Lemma nngnum_subdef : num_spec (Itv.Real `[0, +oo[) x. +Proof. by apply/and3P; rewrite /= ger0_real. Qed. +Definition NngNum : {nonneg R} := Itv.mk nngnum_subdef. +End Nngnum. + +Variant posnum_spec (R : numDomainType) (x : R) : + R -> bool -> bool -> bool -> Type := +| IsPosnum (p : {posnum R}) : posnum_spec x (p%:num) false true true. + +Lemma posnumP (R : numDomainType) (x : R) : 0 < x -> + posnum_spec x x (x == 0) (0 <= x) (0 < x). +Proof. +move=> x_gt0; case: real_ltgt0P (x_gt0) => []; rewrite ?gtr0_real // => _ _. +by rewrite -[x]/(PosNum x_gt0)%:num; constructor. +Qed. + +Variant nonneg_spec (R : numDomainType) (x : R) : R -> bool -> Type := +| IsNonneg (p : {nonneg R}) : nonneg_spec x (p%:num) true. + +Lemma nonnegP (R : numDomainType) (x : R) : 0 <= x -> nonneg_spec x x (0 <= x). +Proof. by move=> xge0; rewrite xge0 -[x]/(NngNum xge0)%:num; constructor. Qed. + Section Test1. Variable R : numDomainType. From 974e61f00a8459e3cece47ba808124b11064c439 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Sun, 24 Nov 2024 21:39:08 +0100 Subject: [PATCH 09/18] Retrieve notation !! from signed --- reals/itv.v | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/reals/itv.v b/reals/itv.v index e43723cec..cc31434c0 100644 --- a/reals/itv.v +++ b/reals/itv.v @@ -109,6 +109,8 @@ Reserved Notation "[ 'le0' 'of' x ]" (format "[ 'le0' 'of' x ]"). Reserved Notation "[ 'cmp0' 'of' x ]" (format "[ 'cmp0' 'of' x ]"). Reserved Notation "[ 'neq0' 'of' x ]" (format "[ 'neq0' 'of' x ]"). +Reserved Notation "!! x" (at level 100, only parsing). + Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. @@ -118,6 +120,13 @@ Import GRing.Theory Num.Theory. Local Open Scope ring_scope. Local Open Scope order_scope. +Notation "!! x" := (ltac:(refine x)) (only parsing). +(* infer class to help typeclass inference on the fly *) +Class infer (P : Prop) := Infer : P. +#[export] Hint Mode infer ! : typeclass_instances. +#[export] Hint Extern 0 (infer _) => (exact) : typeclass_instances. +Lemma inferP (P : Prop) : P -> infer P. Proof. by []. Qed. + Module Itv. Variant t := Top | Real of interval int. From 2d2b7d57bb149adb8fc614c7496e6df22772c03a Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Sun, 24 Nov 2024 17:40:20 +0100 Subject: [PATCH 10/18] Add itv instances for min and max --- reals/itv.v | 76 +++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 76 insertions(+) diff --git a/reals/itv.v b/reals/itv.v index cc31434c0..27c65df43 100644 --- a/reals/itv.v +++ b/reals/itv.v @@ -975,6 +975,82 @@ Qed. Canonical mul_inum (xi yi : Itv.t) (x : num_def R xi) (y : num_def R yi) := Itv.mk (mul_inum_subproof x y). +Definition min_itv_subdef (x y : interval int) : interval int := + let: Interval lx ux := x in + let: Interval ly uy := y in + Interval (Order.min lx ly) (Order.min ux uy). +Arguments min_itv_subdef /. + +Lemma num_min_inum_subproof (xi yi : Itv.t) (x : num_def R xi) (y : num_def R yi) + (r := itv_real2_subdef min_itv_subdef xi yi) : + num_spec r (Order.min x%:num y%:num). +Proof. +apply: itv_real2_subproof (Itv.P x) (Itv.P y). +case: x y => [x /= _] [y /= _] => {xi yi r} -[lx ux] [ly uy]/=. +move=> /andP[xr /=/andP[lxx xux]] /andP[yr /=/andP[lyy yuy]]. +apply/and3P; split; rewrite ?min_real//= map_itv_bound_min real_BSide_min//. +- apply: (comparable_min_le_min (comparable_num_itv_bound_subproof _ _)) => //. + exact: real_comparable. +- apply: (comparable_min_le_min _ (comparable_num_itv_bound_subproof _ _)) => //. + exact: real_comparable. +Qed. + +Definition max_itv_subdef (x y : interval int) : interval int := + let: Interval lx ux := x in + let: Interval ly uy := y in + Interval (Order.max lx ly) (Order.max ux uy). +Arguments max_itv_subdef /. + +Lemma num_max_inum_subproof (xi yi : Itv.t) (x : num_def R xi) (y : num_def R yi) + (r := itv_real2_subdef max_itv_subdef xi yi) : + num_spec r (Order.max x%:num y%:num). +Proof. +apply: itv_real2_subproof (Itv.P x) (Itv.P y). +case: x y => [x /= _] [y /= _] => {xi yi r} -[lx ux] [ly uy]/=. +move=> /andP[xr /=/andP[lxx xux]] /andP[yr /=/andP[lyy yuy]]. +apply/and3P; split; rewrite ?max_real//= map_itv_bound_max real_BSide_max//. +- apply: (comparable_max_le_max (comparable_num_itv_bound_subproof _ _)) => //. + exact: real_comparable. +- apply: (comparable_max_le_max _ (comparable_num_itv_bound_subproof _ _)) => //. + exact: real_comparable. +Qed. + +(* We can't directly put an instance on Order.min for R : numDomainType + since we may want instances for other porderType + (typically \bar R or even nat). So we resort on this additional + canonical structure. *) +Record min_max_typ d := MinMaxTyp { + min_max_sort : porderType d; + #[canonical=no] + min_max_sem : interval int -> min_max_sort -> bool; + #[canonical=no] + min_max_minP : forall (xi yi : Itv.t) (x : Itv.def min_max_sem xi) + (y : Itv.def min_max_sem yi), + let: r := itv_real2_subdef min_itv_subdef xi yi in + Itv.spec min_max_sem r (Order.min x%:num y%:num); + #[canonical=no] + min_max_maxP : forall (xi yi : Itv.t) (x : Itv.def min_max_sem xi) + (y : Itv.def min_max_sem yi), + let: r := itv_real2_subdef max_itv_subdef xi yi in + Itv.spec min_max_sem r (Order.max x%:num y%:num); +}. + +(* The default instances on porderType, for min... *) +Canonical min_typ_inum d (t : min_max_typ d) (xi yi : Itv.t) + (x : Itv.def (@min_max_sem d t) xi) (y : Itv.def (@min_max_sem d t) yi) + (r := itv_real2_subdef min_itv_subdef xi yi) := + Itv.mk (min_max_minP x y). + +(* ...and for max *) +Canonical max_typ_inum d (t : min_max_typ d) (xi yi : Itv.t) + (x : Itv.def (@min_max_sem d t) xi) (y : Itv.def (@min_max_sem d t) yi) + (r := itv_real2_subdef min_itv_subdef xi yi) := + Itv.mk (min_max_maxP x y). + +(* Instance of the above structure for numDomainType *) +Canonical num_min_max_typ (R : numDomainType) := + MinMaxTyp num_min_inum_subproof num_max_inum_subproof. + End NumDomainInstances. Section Morph. From 9201ebfb10da010004ce54fcc8e60a4a90ea5fe9 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Wed, 13 Nov 2024 13:06:47 +0100 Subject: [PATCH 11/18] Add instances for natmul and intmul --- reals/itv.v | 39 +++++++++++++++++++++++++++++++++++++++ 1 file changed, 39 insertions(+) diff --git a/reals/itv.v b/reals/itv.v index 27c65df43..7c99ba179 100644 --- a/reals/itv.v +++ b/reals/itv.v @@ -1051,6 +1051,45 @@ Canonical max_typ_inum d (t : min_max_typ d) (xi yi : Itv.t) Canonical num_min_max_typ (R : numDomainType) := MinMaxTyp num_min_inum_subproof num_max_inum_subproof. +Lemma nat_num_spec (i : Itv.t) (n : nat) : nat_spec i n = num_spec i (n%:R : R). +Proof. +case: i => [//| [l u]]; rewrite /= /Itv.num_sem realn/=; congr (_ && _). +- by case: l => [[] l |//]; rewrite !bnd_simp ?pmulrn ?ler_int ?ltr_int. +- by case: u => [[] u |//]; rewrite !bnd_simp ?pmulrn ?ler_int ?ltr_int. +Qed. + +Lemma natmul_inum_subproof (xi ni : Itv.t) (x : num_def R xi) (n : nat_def ni) + (r := itv_real2_subdef mul_itv_subdef xi ni) : + num_spec r (x%:num *+ n%:num). +Proof. +have Pn : num_spec ni (n%:num%:R : R) by case: n => /= n; rewrite nat_num_spec. +by rewrite -mulr_natr -[n%:num%:R]/((Itv.Def Pn)%:num) mul_inum_subproof. +Qed. + +Canonical natmul_inum (xi ni : Itv.t) (x : num_def R xi) (n : nat_def ni) := + Itv.mk (natmul_inum_subproof x n). + +Lemma int_num_spec (i : Itv.t) (n : int) : + num_spec i n = num_spec i (n%:~R : R). +Proof. +case: i => [//| [l u]]; rewrite /= /Itv.num_sem num_real realz/=. +congr (andb _ _). +- by case: l => [[] l |//]; rewrite !bnd_simp intz ?ler_int ?ltr_int. +- by case: u => [[] u |//]; rewrite !bnd_simp intz ?ler_int ?ltr_int. +Qed. + +Lemma intmul_inum_subproof (xi ii : Itv.t) + (x : num_def R xi) (i : num_def int ii) + (r := itv_real2_subdef mul_itv_subdef xi ii) : + num_spec r (x%:num *~ i%:num). +Proof. +have Pi : num_spec ii (i%:num%:~R : R) by case: i => /= i; rewrite int_num_spec. +by rewrite -mulrzr -[i%:num%:~R]/((Itv.Def Pi)%:num) mul_inum_subproof. +Qed. + +Canonical intmul_inum (xi ni : Itv.t) (x : num_def R xi) (n : num_def int ni) := + Itv.mk (intmul_inum_subproof x n). + End NumDomainInstances. Section Morph. From 26cc489102f937ab3a2efea0267a4967a24376e0 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Wed, 13 Nov 2024 16:04:52 +0100 Subject: [PATCH 12/18] Add instance for inv --- reals/itv.v | 65 +++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 65 insertions(+) diff --git a/reals/itv.v b/reals/itv.v index 7c99ba179..35fc1f327 100644 --- a/reals/itv.v +++ b/reals/itv.v @@ -1090,6 +1090,71 @@ Qed. Canonical intmul_inum (xi ni : Itv.t) (x : num_def R xi) (n : num_def int ni) := Itv.mk (intmul_inum_subproof x n). +Definition keep_pos_itv_bound_subdef (b : itv_bound int) : itv_bound int := + match b with + | BSide b (Posz 0) => BSide b 0 + | BSide _ (Posz (S _)) => BRight 0 + | BSide _ (Negz _) => -oo + | BInfty _ => -oo + end. +Arguments keep_pos_itv_bound_subdef /. + +Lemma keep_pos_itv_bound_subproof (op : R -> R) (x : R) b : + {homo op : x / 0 <= x} -> {homo op : x / 0 < x} -> + (num_itv_bound R b <= BLeft x)%O -> + (num_itv_bound R (keep_pos_itv_bound_subdef b) <= BLeft (op x))%O. +Proof. +case: b => [[] [] [| b] // | []//] hle hlt; rewrite !bnd_simp. +- exact: hle. +- by move=> blex; apply: le_lt_trans (hlt _ _) => //; apply: lt_le_trans blex. +- exact: hlt. +- by move=> bltx; apply: le_lt_trans (hlt _ _) => //; apply: le_lt_trans bltx. +Qed. + +Definition keep_neg_itv_bound_subdef (b : itv_bound int) : itv_bound int := + match b with + | BSide b (Posz 0) => BSide b 0 + | BSide _ (Negz _) => BLeft 0 + | BSide _ (Posz _) => +oo + | BInfty _ => +oo + end. +Arguments keep_neg_itv_bound_subdef /. + +Lemma keep_neg_itv_bound_subproof (op : R -> R) (x : R) b : + {homo op : x / x <= 0} -> {homo op : x / x < 0} -> + (BRight x <= num_itv_bound R b)%O -> + (BRight (op x) <= num_itv_bound R (keep_neg_itv_bound_subdef b))%O. +Proof. +case: b => [[] [[|//] | b] | []//] hge hgt; rewrite !bnd_simp. +- exact: hgt. +- by move=> xltb; apply: hgt; apply: lt_le_trans xltb _; rewrite lerz0. +- exact: hge. +- by move=> xleb; apply: hgt; apply: le_lt_trans xleb _; rewrite ltrz0. +Qed. + +Definition inv_itv_subdef (i : interval int) : interval int := + let: Interval l u := i in + Interval (keep_pos_itv_bound_subdef l) (keep_neg_itv_bound_subdef u). +Arguments inv_itv_subdef /. + +Lemma inv_inum_subproof (i : Itv.t) (x : num_def R i) + (r := itv_real1_subdef inv_itv_subdef i) : + num_spec r (x%:num^-1). +Proof. +apply: itv_real1_subproof (Itv.P x). +case: x => x /= _ [l u] /and3P[xr /= lx xu]. +rewrite /Itv.num_sem/= realV xr/=; apply/andP; split. +- apply: keep_pos_itv_bound_subproof lx. + + by move=> ?; rewrite invr_ge0. + + by move=> ?; rewrite invr_gt0. +- apply: keep_neg_itv_bound_subproof xu. + + by move=> ?; rewrite invr_le0. + + by move=> ?; rewrite invr_lt0. +Qed. + +Canonical inv_inum (i : Itv.t) (x : num_def R i) := + Itv.mk (inv_inum_subproof x). + End NumDomainInstances. Section Morph. From f21a6ab2ffa4732752eb2a260121cd77f082025f Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Wed, 13 Nov 2024 16:35:00 +0100 Subject: [PATCH 13/18] Add instance for exprn --- reals/itv.v | 40 ++++++++++++++++++++++++++++++++++++++++ 1 file changed, 40 insertions(+) diff --git a/reals/itv.v b/reals/itv.v index 35fc1f327..b7845d5da 100644 --- a/reals/itv.v +++ b/reals/itv.v @@ -1155,6 +1155,46 @@ Qed. Canonical inv_inum (i : Itv.t) (x : num_def R i) := Itv.mk (inv_inum_subproof x). +Definition exprn_le1_itv_bound_subdef (l u : itv_bound int) : itv_bound int := + if u isn't BSide _ (Posz 1) then +oo + else if (BLeft 0%Z <= l)%O then BRight 1%Z else +oo. +Arguments exprn_le1_itv_bound_subdef /. + +Lemma exprn_le1_itv_bound_subproof (x : R) n l u : + (num_itv_bound R l <= BLeft x)%O -> + (BRight x <= num_itv_bound R u)%O -> + (BRight (x ^+ n) <= num_itv_bound R (exprn_le1_itv_bound_subdef l u))%O. +Proof. +case: u => [bu [[//|[|//]] |//] | []//]. +rewrite /exprn_le1_itv_bound_subdef; case: (leP _ l) => [lge1 /= |//] lx xu. +rewrite bnd_simp; case: n => [| n]; rewrite ?expr0// expr_le1//. + by case: bu xu; rewrite bnd_simp//; apply: ltW. +case: l lge1 lx => [[] l | []//]; rewrite !bnd_simp -(@ler_int R). +- exact: le_trans. +- by move=> + /ltW; apply: le_trans. +Qed. + +Definition exprn_itv_subdef (i : interval int) : interval int := + let: Interval l u := i in + Interval (keep_pos_itv_bound_subdef l) (exprn_le1_itv_bound_subdef l u). +Arguments exprn_itv_subdef /. + +Lemma exprn_inum_subproof (i : Itv.t) (x : num_def R i) n + (r := itv_real1_subdef exprn_itv_subdef i) : + num_spec r (x%:num ^+ n). +Proof. +apply: (@itv_real1_subproof _ _ (fun x => x^+n) _ _ _ _ (Itv.P x)). +case: x => x /= _ [l u] /and3P[xr /= lx xu]. +rewrite /Itv.num_sem realX//=; apply/andP; split. +- apply: (@keep_pos_itv_bound_subproof (fun x => x^+n)) lx. + + exact: exprn_ge0. + + exact: exprn_gt0. +- exact: exprn_le1_itv_bound_subproof lx xu. +Qed. + +Canonical exprn_inum (i : Itv.t) (x : num_def R i) n := + Itv.mk (exprn_inum_subproof x n). + End NumDomainInstances. Section Morph. From e90f38326815935ad52a3bddb6d1c2d8b6ccfedd Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Wed, 13 Nov 2024 16:45:02 +0100 Subject: [PATCH 14/18] Add instance for norm --- reals/itv.v | 28 ++++++++++++++++++++++++++++ 1 file changed, 28 insertions(+) diff --git a/reals/itv.v b/reals/itv.v index b7845d5da..7455f3684 100644 --- a/reals/itv.v +++ b/reals/itv.v @@ -1195,6 +1195,13 @@ Qed. Canonical exprn_inum (i : Itv.t) (x : num_def R i) n := Itv.mk (exprn_inum_subproof x n). +Lemma norm_inum_subproof {V : normedZmodType R} (x : V) : + num_spec (Itv.Real `[0, +oo[) `|x|. +Proof. by apply/and3P; split; rewrite //= ?normr_real ?bnd_simp ?normr_ge0. Qed. + +Canonical norm_inum {V : normedZmodType R} (x : V) := + Itv.mk (norm_inum_subproof x). + End NumDomainInstances. Section Morph. @@ -1213,6 +1220,14 @@ Proof. by move=> x y; rewrite !maxEle num_le -fun_if. Qed. End Morph. +Section MorphNum. +Context {R : numDomainType}. + +Lemma num_abs_eq0 (a : R) : (`|a|%:nng == 0%:nng) = (a == 0). +Proof. by rewrite -normr_eq0. Qed. + +End MorphNum. + Section MorphReal. Context {R : numDomainType} {i : interval int}. Local Notation nR := (num_def R (Itv.Real i)). @@ -1253,6 +1268,19 @@ Proof. by rewrite -comparable_gt_min// real_comparable. Qed. End MorphReal. +Section MorphGe0. +Context {R : numDomainType}. +Local Notation nR := (num_def R (Itv.Real `[0%Z, +oo[)). +Implicit Type x y : nR. +Local Notation num := (@num R (@Itv.num_sem R) (Itv.Real `[0%Z, +oo[)). + +Lemma num_abs_le a x : 0 <= a -> (`|a|%:nng <= x) = (a <= x%:num). +Proof. by move=> a0; rewrite -num_le//= ger0_norm. Qed. + +Lemma num_abs_lt a x : 0 <= a -> (`|a|%:nng < x) = (a < x%:num). +Proof. by move=> a0; rewrite -num_lt/= ger0_norm. Qed. +End MorphGe0. + Section ItvNum. Context (R : numDomainType). Context (x : R) (l u : itv_bound int). From 24baad02de8386a6a2f50b4a624d69ddf6b77368 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Wed, 13 Nov 2024 16:58:34 +0100 Subject: [PATCH 15/18] Add instance for sqrt --- reals/itv.v | 63 +++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 63 insertions(+) diff --git a/reals/itv.v b/reals/itv.v index 7455f3684..d42c8f18e 100644 --- a/reals/itv.v +++ b/reals/itv.v @@ -1204,6 +1204,69 @@ Canonical norm_inum {V : normedZmodType R} (x : V) := End NumDomainInstances. +Section RcfInstances. +Context {R : rcfType}. + +Definition sqrt_itv_subdef (i : Itv.t) : Itv.t := + match i with + | Itv.Top => Itv.Real `[0%Z, +oo[ + | Itv.Real (Interval l u) => + match l with + | BSide b (Posz 0) => Itv.Real (Interval (BSide b 0%Z) +oo) + | BSide b (Posz (S _)) => Itv.Real `]0%Z, +oo[ + | _ => Itv.Real `[0, +oo[ + end + end. +Arguments sqrt_itv_subdef /. + +Lemma sqrt_inum_subproof (i : Itv.t) (x : num_def R i) + (r := sqrt_itv_subdef i) : + num_spec r (Num.sqrt x%:num). +Proof. +have: Itv.num_sem `[0%Z, +oo[ (Num.sqrt x%:num). + by apply/and3P; rewrite /= num_real !bnd_simp sqrtr_ge0. +rewrite {}/r; case: i x => [//| [[bl [l |//] |//] u]] [x /= +] _. +case: bl l => -[| l] /and3P[xr /= bx _]; apply/and3P; split=> //=; + move: bx; rewrite !bnd_simp ?sqrtr_ge0// sqrtr_gt0; + [exact: lt_le_trans | exact: le_lt_trans..]. +Qed. + +Canonical sqrt_inum (i : Itv.t) (x : num_def R i) := + Itv.mk (sqrt_inum_subproof x). + +End RcfInstances. + +Section NumClosedFieldInstances. +Context {R : numClosedFieldType}. + +Definition sqrtC_itv_subdef (i : Itv.t) : Itv.t := + match i with + | Itv.Top => Itv.Top + | Itv.Real (Interval l u) => + match l with + | BSide b (Posz _) => Itv.Real (Interval (BSide b 0%Z) +oo) + | _ => Itv.Top + end + end. +Arguments sqrtC_itv_subdef /. + +Lemma sqrtC_inum_subproof (i : Itv.t) (x : num_def R i) + (r := sqrtC_itv_subdef i) : + num_spec r (sqrtC x%:num). +Proof. +rewrite {}/r; case: i x => [//| [l u] [x /=/and3P[xr /= lx xu]]]. +case: l lx => [bl [l |//] |[]//] lx; apply/and3P; split=> //=. + by apply: real_sqrtC; case: bl lx => /[!bnd_simp] [|/ltW]; apply: le_trans. +case: bl lx => /[!bnd_simp] lx. +- by rewrite sqrtC_ge0; apply: le_trans lx. +- by rewrite sqrtC_gt0; apply: le_lt_trans lx. +Qed. + +Canonical sqrtC_inum (i : Itv.t) (x : num_def R i) := + Itv.mk (sqrtC_inum_subproof x). + +End NumClosedFieldInstances. + Section Morph. Context {R : numDomainType} {i : Itv.t}. Local Notation nR := (num_def R i). From 6723e9bcda34dbe824400925becf1480c26adb51 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Thu, 14 Nov 2024 23:56:36 +0100 Subject: [PATCH 16/18] Add instances on nat --- reals/itv.v | 104 ++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 104 insertions(+) diff --git a/reals/itv.v b/reals/itv.v index d42c8f18e..0321ffb77 100644 --- a/reals/itv.v +++ b/reals/itv.v @@ -1267,6 +1267,110 @@ Canonical sqrtC_inum (i : Itv.t) (x : num_def R i) := End NumClosedFieldInstances. +Section NatInstances. +Local Open Scope nat_scope. +Implicit Type (n : nat). + +Lemma zeron_inum_subproof : nat_spec (Itv.Real `[0, 0]%Z) 0. +Proof. by []. Qed. + +Canonical zeron_inum := Itv.mk zeron_inum_subproof. + +Lemma succn_inum_subproof n : nat_spec (Itv.Real `[1, +oo[%Z) n.+1. +Proof. by []. Qed. + +Canonical succn_inum n := Itv.mk (succn_inum_subproof n). + +Lemma addn_inum_subproof (xi yi : Itv.t) (x : nat_def xi) (y : nat_def yi) + (r := itv_real2_subdef add_itv_subdef xi yi) : + nat_spec r (x%:num + y%:num). +Proof. +have Px : num_spec xi (x%:num%:R : int). + by case: x => /= x; rewrite (@nat_num_spec int). +have Py : num_spec yi (y%:num%:R : int). + by case: y => /= y; rewrite (@nat_num_spec int). +rewrite (@nat_num_spec int) natrD. +rewrite -[x%:num%:R]/((Itv.Def Px)%:num) -[y%:num%:R]/((Itv.Def Py)%:num). +exact: add_inum_subproof. +Qed. + +Canonical addn_inum (xi yi : Itv.t) (x : nat_def xi) (y : nat_def yi) := + Itv.mk (addn_inum_subproof x y). + +Lemma double_inum_subproof (i : Itv.t) (n : nat_def i) + (r := itv_real2_subdef add_itv_subdef i i) : + nat_spec r (n%:num.*2). +Proof. by rewrite -addnn addn_inum_subproof. Qed. + +Canonical double_inum (i : Itv.t) (x : nat_def i) := + Itv.mk (double_inum_subproof x). + +Lemma muln_inum_subproof (xi yi : Itv.t) (x : nat_def xi) (y : nat_def yi) + (r := itv_real2_subdef mul_itv_subdef xi yi) : + nat_spec r (x%:num * y%:num). +Proof. +have Px : num_spec xi (x%:num%:R : int). + by case: x => /= x; rewrite (@nat_num_spec int). +have Py : num_spec yi (y%:num%:R : int). + by case: y => /= y; rewrite (@nat_num_spec int). +rewrite (@nat_num_spec int) natrM. +rewrite -[x%:num%:R]/((Itv.Def Px)%:num) -[y%:num%:R]/((Itv.Def Py)%:num). +exact: mul_inum_subproof. +Qed. + +Canonical muln_inum (xi yi : Itv.t) (x : nat_def xi) (y : nat_def yi) := + Itv.mk (muln_inum_subproof x y). + +Lemma expn_inum_subproof (i : Itv.t) (x : nat_def i) n + (r := itv_real1_subdef exprn_itv_subdef i) : + nat_spec r (x%:num ^ n). +Proof. +have Px : num_spec i (x%:num%:R : int). + by case: x => /= x; rewrite (@nat_num_spec int). +rewrite (@nat_num_spec int) natrX -[x%:num%:R]/((Itv.Def Px)%:num). +exact: exprn_inum_subproof. +Qed. + +Canonical expn_inum (i : Itv.t) (x : nat_def i) n := + Itv.mk (expn_inum_subproof x n). + +Lemma minn_inum_subproof (xi yi : Itv.t) (x : nat_def xi) (y : nat_def yi) + (r := itv_real2_subdef min_itv_subdef xi yi) : + nat_spec r (minn x%:num y%:num). +Proof. +have Px : num_spec xi (x%:num%:R : int). + by case: x => /= x; rewrite (@nat_num_spec int). +have Py : num_spec yi (y%:num%:R : int). + by case: y => /= y; rewrite (@nat_num_spec int). +rewrite (@nat_num_spec int) -minEnat natr_min. +rewrite -[x%:num%:R]/((Itv.Def Px)%:num) -[y%:num%:R]/((Itv.Def Py)%:num). +exact: num_min_inum_subproof. +Qed. + +Canonical minn_inum (xi yi : Itv.t) (x : nat_def xi) (y : nat_def yi) := + Itv.mk (minn_inum_subproof x y). + +Lemma maxn_inum_subproof (xi yi : Itv.t) (x : nat_def xi) (y : nat_def yi) + (r := itv_real2_subdef max_itv_subdef xi yi) : + nat_spec r (maxn x%:num y%:num). +Proof. +have Px : num_spec xi (x%:num%:R : int). + by case: x => /= x; rewrite (@nat_num_spec int). +have Py : num_spec yi (y%:num%:R : int). + by case: y => /= y; rewrite (@nat_num_spec int). +rewrite (@nat_num_spec int) -maxEnat natr_max. +rewrite -[x%:num%:R]/((Itv.Def Px)%:num) -[y%:num%:R]/((Itv.Def Py)%:num). +exact: num_max_inum_subproof. +Qed. + +Canonical maxn_inum (xi yi : Itv.t) (x : nat_def xi) (y : nat_def yi) := + Itv.mk (maxn_inum_subproof x y). + +Canonical nat_min_max_typ := + MinMaxTyp minn_inum_subproof maxn_inum_subproof. + +End NatInstances. + Section Morph. Context {R : numDomainType} {i : Itv.t}. Local Notation nR := (num_def R i). From ce41c556f5543b3d52ec4ec32a25e8afe67f8328 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Sat, 16 Nov 2024 17:28:21 +0100 Subject: [PATCH 17/18] Add instances on int --- reals/itv.v | 14 ++++++++++++++ 1 file changed, 14 insertions(+) diff --git a/reals/itv.v b/reals/itv.v index 0321ffb77..84abf730a 100644 --- a/reals/itv.v +++ b/reals/itv.v @@ -1371,6 +1371,20 @@ Canonical nat_min_max_typ := End NatInstances. +Section IntInstances. + +Lemma Posz_inum_subproof n : num_spec (Itv.Real `[0, +oo[) (Posz n). +Proof. by apply/and3P; rewrite /= num_real !bnd_simp. Qed. + +Canonical Posz_inum n := Itv.mk (Posz_inum_subproof n). + +Lemma Negz_inum_subproof n : num_spec (Itv.Real `]-oo, -1]) (Negz n). +Proof. by apply/and3P; rewrite /= num_real !bnd_simp. Qed. + +Canonical Negz_inum n := Itv.mk (Negz_inum_subproof n). + +End IntInstances. + Section Morph. Context {R : numDomainType} {i : Itv.t}. Local Notation nR := (num_def R i). From 89faa962ab890ac4c6cb008689ba4580252d10cc Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Sun, 24 Nov 2024 17:40:37 +0100 Subject: [PATCH 18/18] Port from signed to itv And deprecate signed. --- CHANGELOG_UNRELEASED.md | 2 + analysis_stdlib/Rstruct_topology.v | 2 +- analysis_stdlib/showcase/uniform_bigO.v | 4 +- reals/all_reals.v | 1 - reals/constructive_ereal.v | 861 ++++++++++++++---- reals/prodnormedzmodule.v | 4 +- reals/real_interval.v | 2 +- reals/signed.v | 3 + theories/charge.v | 26 +- theories/convex.v | 2 +- theories/derive.v | 2 +- theories/ereal.v | 91 +- theories/esum.v | 4 +- theories/exp.v | 2 +- theories/ftc.v | 2 +- theories/function_spaces.v | 2 +- theories/hoelder.v | 4 +- theories/kernel.v | 2 +- theories/landau.v | 4 +- theories/lebesgue_integral.v | 37 +- theories/lebesgue_measure.v | 7 +- theories/lebesgue_stieltjes_measure.v | 2 +- theories/measure.v | 28 +- theories/normedtype.v | 10 +- theories/numfun.v | 2 +- theories/probability.v | 4 +- theories/realfun.v | 2 +- theories/separation_axioms.v | 2 +- theories/sequences.v | 11 +- theories/topology_theory/compact.v | 2 +- theories/topology_theory/matrix_topology.v | 2 +- theories/topology_theory/num_topology.v | 2 +- theories/topology_theory/product_topology.v | 2 +- .../topology_theory/pseudometric_structure.v | 2 +- theories/topology_theory/weak_topology.v | 2 +- theories/trigo.v | 2 +- theories/tvs.v | 2 +- 37 files changed, 812 insertions(+), 329 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 70a6cb529..0b8d15761 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -56,6 +56,8 @@ ### Deprecated +- file `signed.v` (use `itv.v` instead) + - in `itv.v`: + notation `%:inum` (use `%:num` instead) diff --git a/analysis_stdlib/Rstruct_topology.v b/analysis_stdlib/Rstruct_topology.v index 1d8e3f65a..ce19bb01e 100644 --- a/analysis_stdlib/Rstruct_topology.v +++ b/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. diff --git a/analysis_stdlib/showcase/uniform_bigO.v b/analysis_stdlib/showcase/uniform_bigO.v index 58e6e9c5b..80306f9dd 100644 --- a/analysis_stdlib/showcase/uniform_bigO.v +++ b/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]]. diff --git a/reals/all_reals.v b/reals/all_reals.v index 1f7707f6c..00cdd1bfb 100644 --- a/reals/all_reals.v +++ b/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. diff --git a/reals/constructive_ereal.v b/reals/constructive_ereal.v index 6caabc258..68141caa2 100644 --- a/reals/constructive_ereal.v +++ b/reals/constructive_ereal.v @@ -11,7 +11,7 @@ bounds of intervals*) From HB Require Import structures. From mathcomp Require Import all_ssreflect all_algebra finmap. -From mathcomp Require Import mathcomp_extra signed. +From mathcomp Require Import mathcomp_extra itv. (**md**************************************************************************) (* # Extended real numbers $\overline{R}$ *) @@ -3462,201 +3462,689 @@ Module ConstructiveDualAddTheory. Export DualAddTheory. End ConstructiveDualAddTheory. -Definition posnume (R : numDomainType) of phant R := {> 0 : \bar R}. -Notation "{ 'posnum' '\bar' R }" := (@posnume _ (Phant R)) : type_scope. -Definition nonnege (R : numDomainType) of phant R := {>= 0 : \bar R}. -Notation "{ 'nonneg' '\bar' R }" := (@nonnege _ (Phant R)) : type_scope. +Section Itv. +Context {R : numDomainType}. -Notation "x %:pos" := (widen_signed x%:sgn : {posnum \bar _}) (only parsing) - : ereal_dual_scope. -Notation "x %:pos" := (widen_signed x%:sgn : {posnum \bar _}) (only parsing) - : ereal_scope. -Notation "x %:nng" := (widen_signed x%:sgn : {nonneg \bar _}) (only parsing) - : ereal_dual_scope. -Notation "x %:nng" := (widen_signed x%:sgn : {nonneg \bar _}) (only parsing) - : ereal_scope. -Notation "x %:pos" := (@widen_signed ereal_display _ _ _ _ - (@Signed.from _ _ _ _ _ _ (Phantom _ x)) - !=0 (KnownSign.Real (KnownSign.Sign >=0)) _ _) - (only printing) : ereal_dual_scope. -Notation "x %:pos" := (@widen_signed ereal_display _ _ _ _ - (@Signed.from _ _ _ _ _ _ (Phantom _ x)) - !=0 (KnownSign.Real (KnownSign.Sign >=0)) _ _) - (only printing) : ereal_scope. -Notation "x %:nng" := (@widen_signed ereal_display _ _ _ _ - (@Signed.from _ _ _ _ _ _ (Phantom _ x)) - ?=0 (KnownSign.Real (KnownSign.Sign >=0)) _ _) - (only printing) : ereal_dual_scope. -Notation "x %:nng" := (@widen_signed ereal_display _ _ _ _ - (@Signed.from _ _ _ _ _ _ (Phantom _ x)) - ?=0 (KnownSign.Real (KnownSign.Sign >=0)) _ _) - (only printing) : ereal_scope. +Definition ext_num_sem (i : interval int) (x : \bar R) := + (0 >=< x)%O + && let: Interval l u := i in + x \in Interval (Itv.map_itv_bound (EFin \o intr) l) + (Itv.map_itv_bound (EFin \o intr) u). -#[global] Hint Extern 0 (is_true (0%E < _)%O) => solve [apply: gt0] : core. -#[global] Hint Extern 0 (is_true (_ < 0%E)%O) => solve [apply: lt0] : core. -#[global] Hint Extern 0 (is_true (0%E <= _)%O) => solve [apply: ge0] : core. -#[global] Hint Extern 0 (is_true (_ <= 0%E)%O) => solve [apply: le0] : core. -#[global] Hint Extern 0 (is_true (0%E >=< _)%O) => solve [apply: cmp0] : core. -#[global] Hint Extern 0 (is_true (_ != 0%E)%O) => solve [apply: neq0] : core. +Local Notation num_spec := (Itv.spec (@Itv.num_sem _)). +Local Notation num_def R := (Itv.def (@Itv.num_sem R)). +Local Notation num_itv_bound R := (@Itv.map_itv_bound _ R intr). -Section SignedNumDomainStability. -Context {R : numDomainType}. +Local Notation ext_num_spec := (Itv.spec ext_num_sem). +Local Notation ext_num_def := (Itv.def ext_num_sem). +Local Notation ext_num_itv_bound := + (@Itv.map_itv_bound _ (\bar R) (EFin \o intr)). + +Lemma ext_num_num_sem_subproof i (x : R) : + Itv.ext_num_sem i x%:E = Itv.num_sem i x. +Proof. by case: i => [l u]; do 2![congr (_ && _)]; [case: l | case: u]. Qed. + +Lemma ext_num_num_spec_subproof i (x : R) : + ext_num_spec i x%:E = num_spec i x. +Proof. by case: i => [//| i]; apply: ext_num_num_sem_subproof. Qed. + +Lemma EFin_le_map_itv_bound (x y : itv_bound R) : + (Itv.map_itv_bound EFin x <= Itv.map_itv_bound EFin y)%O = (x <= y)%O. +Proof. by case: x y => [xb x | x] [yb y | y]. Qed. + +Lemma EFin_BLeft_le_map_itv_bound (x : itv_bound R) (y : R) : + (Itv.map_itv_bound EFin x <= BLeft y%:E)%O = (x <= BLeft y)%O. +Proof. +rewrite -[BLeft y%:E]/(Itv.map_itv_bound EFin (BLeft y)). +by rewrite EFin_le_map_itv_bound. +Qed. + +Lemma BRight_EFin_le_map_itv_bound (x : R) (y : itv_bound R) : + (BRight x%:E <= Itv.map_itv_bound EFin y)%O = (BRight x <= y)%O. +Proof. +rewrite -[BRight x%:E]/(Itv.map_itv_bound EFin (BRight x)). +by rewrite EFin_le_map_itv_bound. +Qed. + +Lemma ext_le_map_itv_bound (x y : itv_bound int) : + (ext_num_itv_bound x <= ext_num_itv_bound y)%O = (x <= y)%O. +Proof. +rewrite !(map_itv_bound_comp EFin intr)/=. +by rewrite EFin_le_map_itv_bound intr_le_map_itv_bound. +Qed. + +Lemma subitv_map_itv (x y : Itv.t) : Itv.sub x y -> + forall z : \bar R, ext_num_spec x z -> ext_num_spec y z. +Proof. +case: x y => [| x] [| y] //= x_sub_y z /andP[rz]; rewrite /Itv.ext_num_sem rz/=. +move: x y x_sub_y => [lx ux] [ly uy] /andP[lel leu] /=. +move=> /andP[lxz zux]; apply/andP; split. +- by apply: le_trans lxz; rewrite ext_le_map_itv_bound. +- by apply: le_trans zux _; rewrite ext_le_map_itv_bound. +Qed. + +Section ItvTheory. +Context {i : Itv.t}. +Implicit Type x : ext_num_def i. + +Lemma ext_widen_itv_subproof x i' : Itv.sub i i' -> + ext_num_spec i' x%:inum. +Proof. by case: x => x /= /[swap] /subitv_map_itv; apply. Qed. + +Definition ext_widen_itv x i' (uni : unify_itv i i') := + Itv.mk (ext_widen_itv_subproof x uni). + +Lemma gt0e x : unify_itv i (Itv.Real `]Posz 0, +oo[) -> 0%E < x%:inum :> \bar R. +Proof. +case: x => x /= /[swap] /subitv_map_itv /[apply] /andP[_]. +by rewrite /= in_itv/= andbT. +Qed. + +Lemma lte0 x : unify_itv i (Itv.Real `]-oo, Posz 0[) -> x%:inum < 0%E :> \bar R. +Proof. +by case: x => x /= /[swap] /subitv_map_itv /[apply] /andP[_] /=; rewrite in_itv. +Qed. + +Lemma ge0e x : unify_itv i (Itv.Real `[Posz 0, +oo[) -> 0%E <= x%:inum :> \bar R. +Proof. +case: x => x /= /[swap] /subitv_map_itv /[apply] /andP[_] /=. +by rewrite in_itv/= andbT. +Qed. + +Lemma lee0 x : unify_itv i (Itv.Real `]-oo, Posz 0]) -> x%:inum <= 0%E :> \bar R. +Proof. +by case: x => x /= /[swap] /subitv_map_itv /[apply] /andP[_] /=; rewrite in_itv. +Qed. + +Lemma cmp0e x : unify_itv i (Itv.Real `]-oo, +oo[) -> (0%E >=< x%:inum)%O. +Proof. by case: i x => [//| [l u] [[x||//] /=/andP[/= xr _]]]. Qed. + +Lemma neqe0 x : + unify (fun ix iy => negb (Itv.sub ix iy)) (Itv.Real `[0%Z, 0%Z]) i -> + x%:inum != 0 :> \bar R. +Proof. +case: i x => [//| [l u] [x /= Px]]; apply: contra => /eqP x0 /=. +move: Px; rewrite x0 => /and3P[_ /= l0 u0]; apply/andP; split. +- by case: l l0 => [[] l |]; rewrite ?bnd_simp ?lee_fin ?lte_fin ?lerz0 ?ltrz0. +- by case: u u0 => [[] u |]; rewrite ?bnd_simp ?lee_fin ?lte_fin ?ler0z ?ltr0z. +Qed. + +End ItvTheory. + +Lemma pinfty_inum_subproof : ext_num_spec (Itv.Real `]1%Z, +oo[) (+oo : \bar R). +Proof. by apply/and3P; rewrite /= cmp0y !bnd_simp real_ltry. Qed. + +Canonical pinfty_inum := Itv.mk (pinfty_inum_subproof). + +Lemma ninfty_inum_subproof : + ext_num_spec (Itv.Real `]-oo, (-1)%Z[) (-oo : \bar R). +Proof. by apply/and3P; rewrite /= cmp0Ny !bnd_simp real_ltNyr. Qed. + +Canonical ninfty_snum := Itv.mk (ninfty_inum_subproof). + +Lemma EFin_inum_subproof i (x : num_def R i) : ext_num_spec i x%:num%:E. +Proof. +case: i x => [//| [l u] [x /=/and3P[xr /= lx xu]]]. +by apply/and3P; split=> [//||]; [case: l lx | case: u xu]. +Qed. + +Canonical EFin_inum i (x : num_def R i) := Itv.mk (EFin_inum_subproof x). + +Definition keep_nonneg_itv_bound_subdef b := + match b with + | BSide _ (Posz _) => BLeft 0%Z + | BSide _ (Negz _) => -oo%O + | BInfty _ => -oo%O + end. +Arguments keep_nonneg_itv_bound_subdef /. -Lemma pinfty_snum_subproof : Signed.spec 0 !=0 >=0 (+oo : \bar R). -Proof. by rewrite /= le0y. Qed. +Definition keep_nonpos_itv_bound_subdef b := + match b with + | BSide _ (Negz _) | BSide _ (Posz 0) => BRight 0%Z + | BSide _ (Posz (S _)) => +oo%O + | BInfty _ => +oo%O + end. +Arguments keep_nonpos_itv_bound_subdef /. -Canonical pinfty_snum := Signed.mk (pinfty_snum_subproof). +Definition fine_itv_subdef i := + let: Interval l u := i in + Interval (keep_nonneg_itv_bound_subdef l) (keep_nonpos_itv_bound_subdef u). -Lemma ninfty_snum_subproof : Signed.spec 0 !=0 <=0 (-oo : \bar R). -Proof. by rewrite /= leNy0. Qed. +Lemma fine_inum_subproof i (x : ext_num_def i) + (r := itv_real1_subdef fine_itv_subdef i) : + num_spec r (fine x%:num). +Proof. +rewrite {}/r; case: i x => [//| [l u] [x /=/and3P[xr /= lx xu]]]. +apply/and3P; split; rewrite -?real_fine//. +- case: x lx {xu xr} => [x||]/=; [|by case: l => [? []|]..]. + by case: l => [[] [l |//] |//] /[!bnd_simp] => [|/ltW]/=; rewrite lee_fin; + apply: le_trans. +- case: x xu {lx xr} => [x||]/=; [|by case: u => [? [[]|] |]..]. + by case: u => [bu [[|//] | u] |//]; case: bu => /[!bnd_simp] [/ltW|]/=; + rewrite lee_fin// => xu; apply: le_trans xu _; rewrite lerz0. +Qed. -Canonical ninfty_snum := Signed.mk (ninfty_snum_subproof). +Canonical fine_inum i (x : ext_num_def i) := Itv.mk (fine_inum_subproof x). -Lemma EFin_snum_subproof nz cond (x : {num R & nz & cond}) : - Signed.spec 0 nz cond x%:num%:E. +Lemma ext_num_sem_y l u : + ext_num_sem (Interval l u) +oo = ((l != +oo%O) && (u == +oo%O)). Proof. -apply/andP; split. - case: cond nz x => [[[]|]|] [] x //=; - do ?[by case: (bottom x)|by rewrite eqe eq0F]. -case: cond nz x => [[[]|]|] [] x //=; - do ?[by case: (bottom x)|by rewrite ?lee_fin ?(eq0, ge0, le0) ?[_ || _]cmp0]. +apply/and3P/andP => [[_ ly uy] | [ly uy]]; split. +- by case: l ly => -[]. +- by case: u uy => -[]. +- exact: cmp0y. +- case: l ly => [|[]//]. + by case=> l _ /=; rewrite bnd_simp ?real_leey ?real_ltry /= realz. +- by case: u uy => -[]. Qed. -Canonical EFin_snum nz cond (x : {num R & nz & cond}) := - Signed.mk (EFin_snum_subproof x). +Lemma ext_num_sem_Ny l u : + ext_num_sem (Interval l u) -oo = ((l == -oo%O) && (u != -oo%O)). +Proof. +apply/and3P/andP => [[_ ly uy] | [ly uy]]; split. +- by case: l ly => -[]. +- by case: u uy => -[]. +- exact: real0. +- by case: l ly => -[]. +- case: u uy => [|[]//]. + by case=> u _ /=; rewrite bnd_simp ?real_leNye ?real_ltNyr /= realz. +Qed. -Lemma fine_snum_subproof (xnz : KnownSign.nullity) (xr : KnownSign.reality) - (x : {compare (0 : \bar R) & xnz & xr}) : - Signed.spec 0%R ?=0 xr (fine x%:num). +Lemma oppe_itv_boundr_subproof (x : \bar R) b : + (BRight (- x) <= ext_num_itv_bound (opp_itv_bound_subdef b))%O + = (ext_num_itv_bound b <= BLeft x)%O. Proof. -case: xr x => [[[]|]|]//= [x /andP[_]]/=. -- by move=> /eqP ->. -- by case: x. -- by case: x. -- by move=> /orP[]; case: x => [x||]//=; rewrite lee_fin => ->; rewrite ?orbT. +by case: b => [[] b | []//]; rewrite /= !bnd_simp mulrNz EFinN ?leeN2 // lteN2. Qed. -Canonical fine_snum (xnz : KnownSign.nullity) (xr : KnownSign.reality) - (x : {compare (0 : \bar R) & xnz & xr}) := - Signed.mk (fine_snum_subproof x). +Lemma oppe_itv_boundl_subproof (x : \bar R) b : + (ext_num_itv_bound (opp_itv_bound_subdef b) <= BLeft (- x))%O + = (BRight x <= ext_num_itv_bound b)%O. +Proof. +by case: b => [[] b | []//]; rewrite /= !bnd_simp mulrNz EFinN ?leeN2 // lteN2. +Qed. -Lemma oppe_snum_subproof (xnz : KnownSign.nullity) (xr : KnownSign.reality) - (x : {compare (0 : \bar R) & xnz & xr}) (r := opp_reality_subdef xnz xr) : - Signed.spec 0 xnz r (- x%:num). +Lemma oppe_inum_subproof i (x : ext_num_def i) + (r := itv_real1_subdef opp_itv_subdef i) : + ext_num_spec r (- x%:inum). Proof. -rewrite {}/r; case: xr xnz x => [[[]|]|] [] x //=; - do ?[by case: (bottom x) - |by rewrite ?eqe_oppLR ?oppe0 1?eq0//; - rewrite ?oppe_le0 ?oppe_ge0 ?(eq0, eq0F, ge0, le0)//; - rewrite orbC [_ || _]cmp0]. +rewrite {}/r; case: x => -[x||]/=; + [|by case: i => [//| [l u]]; rewrite /= ext_num_sem_y ext_num_sem_Ny; + case: l u => [[] ?|[]] [[] ?|[]]..]. +rewrite !ext_num_num_spec_subproof => Px. +by rewrite -[x]/(Itv.mk Px)%:inum opp_inum_subproof. Qed. -Canonical oppe_snum (xnz : KnownSign.nullity) (xr : KnownSign.reality) - (x : {compare (0 : \bar R) & xnz & xr}) := - Signed.mk (oppe_snum_subproof x). +Canonical oppe_inum i (x : ext_num_def i) := Itv.mk (oppe_inum_subproof x). -Lemma adde_snum_subproof (xnz ynz : KnownSign.nullity) - (xr yr : KnownSign.reality) - (x : {compare (0 : \bar R) & xnz & xr}) - (y : {compare (0 : \bar R) & ynz & yr}) - (rnz := add_nonzero_subdef xnz ynz xr yr) - (rrl := add_reality_subdef xnz ynz xr yr) : - Signed.spec 0 rnz rrl (adde x%:num y%:num). +Lemma adde_inum_subproof xi yi (x : ext_num_def xi) (y : ext_num_def yi) + (r := itv_real2_subdef add_itv_subdef xi yi) : + ext_num_spec r (adde x%:inum y%:inum). Proof. -rewrite {}/rnz {}/rrl; apply/andP; split. - move: xr yr xnz ynz x y => [[[]|]|] [[[]|]|] [] []//= x y; - by rewrite 1?adde_ss_eq0 ?(eq0F, ge0, le0, andbF, orbT). -move: xr yr xnz ynz x y => [[[]|]|] [[[]|]|] [] []//= x y; - do ?[by case: (bottom x)|by case: (bottom y) - |by rewrite adde_ge0|by rewrite adde_le0 - |exact: realDe|by rewrite 2!eq0 /adde/= addr0]. +rewrite {}/r; case: x y => -[x||] + [[y||]]/=; + [|by case: xi yi => [//| [xl xu]] [//| [yl yu]]; + rewrite /adde/= ?ext_num_sem_y ?ext_num_sem_Ny; + case: xl xu yl yu => [[] ?|[]] [[] ?|[]] [[] ?|[]] [[] ?|[]]..]. +rewrite !ext_num_num_spec_subproof => Px Py. +by rewrite -[x]/(Itv.mk Px)%:inum -[y]/(Itv.mk Py)%:inum add_inum_subproof. Qed. -Canonical adde_snum (xnz ynz : KnownSign.nullity) - (xr yr : KnownSign.reality) - (x : {compare (0 : \bar R) & xnz & xr}) - (y : {compare (0 : \bar R) & ynz & yr}) := - Signed.mk (adde_snum_subproof x y). +Canonical adde_inum xi yi (x : ext_num_def xi) (y : ext_num_def yi) := + Itv.mk (adde_inum_subproof x y). Import DualAddTheory. -Lemma dEFin_snum_subproof nz cond (x : {num R & nz & cond}) : - Signed.spec 0 nz cond (dEFin x%:num). -Proof. exact: EFin_snum_subproof. Qed. - -Canonical dEFin_snum nz cond (x : {num R & nz & cond}) := - Signed.mk (dEFin_snum_subproof x). - -Lemma dadde_snum_subproof (xnz ynz : KnownSign.nullity) - (xr yr : KnownSign.reality) - (x : {compare (0 : \bar R) & xnz & xr}) - (y : {compare (0 : \bar R) & ynz & yr}) - (rnz := add_nonzero_subdef xnz ynz xr yr) - (rrl := add_reality_subdef xnz ynz xr yr) : - Signed.spec 0 rnz rrl (dual_adde x%:num y%:num)%dE. -Proof. -rewrite {}/rnz {}/rrl; apply/andP; split. - move: xr yr xnz ynz x y => [[[]|]|] [[[]|]|] [] []//= x y; - by rewrite 1?dadde_ss_eq0 ?(eq0F, ge0, le0, andbF, orbT). -move: xr yr xnz ynz x y => [[[]|]|] [[[]|]|] [] []//= x y; - do ?[by case: (bottom x)|by case: (bottom y) - |by rewrite dadde_ge0|by rewrite dadde_le0 - |exact: realDed|by rewrite 2!eq0 /dual_adde/= addr0]. -Qed. - -Canonical dadde_snum (xnz ynz : KnownSign.nullity) - (xr yr : KnownSign.reality) - (x : {compare (0 : \bar R) & xnz & xr}) - (y : {compare (0 : \bar R) & ynz & yr}) := - Signed.mk (dadde_snum_subproof x y). - -Lemma mule_snum_subproof (xnz ynz : KnownSign.nullity) - (xr yr : KnownSign.reality) - (x : {compare (0 : \bar R) & xnz & xr}) - (y : {compare (0 : \bar R) & ynz & yr}) - (rnz := mul_nonzero_subdef xnz ynz xr yr) - (rrl := mul_reality_subdef xnz ynz xr yr) : - Signed.spec 0 rnz rrl (x%:num * y%:num). -Proof. -rewrite {}/rnz {}/rrl; apply/andP; split. - by move: xr yr xnz ynz x y => [[[]|]|] [[[]|]|] [] []// x y; - rewrite mule_neq0. -by move: xr yr xnz ynz x y => [[[]|]|] [[[]|]|] [] []/= x y //; - do ?[by case: (bottom x)|by case: (bottom y) - |by rewrite mule_ge0|by rewrite mule_le0_ge0 - |by rewrite mule_ge0_le0|by rewrite mule_le0|exact: realMe - |by rewrite eq0 ?mule0// mul0e]. -Qed. - -Canonical mule_snum (xnz ynz : KnownSign.nullity) (xr yr : KnownSign.reality) - (x : {compare (0 : \bar R) & xnz & xr}) - (y : {compare (0 : \bar R) & ynz & yr}) := - Signed.mk (mule_snum_subproof x y). - -Definition abse_reality_subdef (xnz : KnownSign.nullity) - (xr : KnownSign.reality) := (if xr is =0 then =0 else >=0)%snum_sign. -Arguments abse_reality_subdef /. - -Lemma abse_snum_subproof (xnz : KnownSign.nullity) (xr : KnownSign.reality) - (x : {compare (0 : \bar R) & xnz & xr}) (r := abse_reality_subdef xnz xr) : - Signed.spec 0 xnz r `|x%:num|. -Proof. -rewrite {}/r; case: xr xnz x => [[[]|]|] [] x //=; - do ?[by case: (bottom x)|by rewrite eq0 abse0 - |by rewrite abse_ge0// andbT gee0_abs - |by rewrite abse_ge0// andbT lee0_abs - |by rewrite abse_ge0// andbT abse_eq0]. -Qed. - -Canonical abse_snum (xnz : KnownSign.nullity) (xr : KnownSign.reality) - (x : {compare (0 : \bar R) & xnz & xr}) := - Signed.mk (abse_snum_subproof x). - -End SignedNumDomainStability. +Lemma dEFin_inum_subproof i (x : num_def R i) : ext_num_spec i (dEFin x%:num). +Proof. +case: i x => [//| [l u] [x /=/and3P[xr /= lx xu]]]. +by apply/and3P; split=> [//||]; [case: l lx | case: u xu]. +Qed. + +Canonical dEFin_inum i (x : num_def R i) := Itv.mk (dEFin_inum_subproof x). + +Lemma dadde_inum_subproof xi yi (x : ext_num_def xi) (y : ext_num_def yi) + (r := itv_real2_subdef add_itv_subdef xi yi) : + ext_num_spec r (dual_adde x%:inum y%:inum). +Proof. +rewrite {}/r; case: x y => -[x||] + [[y||]]/=; + [|by case: xi yi => [//| [xl xu]] [//| [yl yu]]; + rewrite /dual_adde/= ?ext_num_sem_y ?ext_num_sem_Ny; + case: xl xu yl yu => [[] ?|[]] [[] ?|[]] [[] ?|[]] [[] ?|[]]..]. +rewrite !ext_num_num_spec_subproof => Px Py. +by rewrite -[x]/(Itv.mk Px)%:inum -[y]/(Itv.mk Py)%:inum add_inum_subproof. +Qed. + +Canonical dadde_inum xi yi (x : ext_num_def xi) (y : ext_num_def yi) := + Itv.mk (dadde_inum_subproof x y). + +Variant ext_interval_sign_spec (l u : itv_bound int) (x : \bar R) : + signi -> Set := + | ISignEqZero : l = BLeft 0%Z -> u = BRight 0%Z -> x = 0 -> + ext_interval_sign_spec l u x (Known EqZero) + | ISignNonNeg : (BLeft 0%:Z <= l)%O -> (BRight 0%:Z < u)%O -> 0 <= x -> + ext_interval_sign_spec l u x (Known NonNeg) + | ISignNonPos : (l < BLeft 0%:Z)%O -> (u <= BRight 0%:Z)%O -> x <= 0 -> + ext_interval_sign_spec l u x (Known NonPos) + | ISignBoth : (l < BLeft 0%:Z)%O -> (BRight 0%:Z < u)%O -> + (0 >=< x)%O -> ext_interval_sign_spec l u x Unknown. + +Lemma ext_interval_signP (l u : itv_bound int) (x : \bar R) : + (ext_num_itv_bound l <= BLeft x)%O -> (BRight x <= ext_num_itv_bound u)%O -> + (0 >=< x)%O -> + ext_interval_sign_spec l u x (interval_sign (Interval l u)). +Proof. +case: x => [x||] xl xu xs. +- case: (@interval_signP R l u x _ _ xs). + + by case: l xl => -[]. + + by case: u xu => -[]. + + by move=> l0 u0 x0; apply: ISignEqZero => //; rewrite x0. + + by move=> l0 u0 x0; apply: ISignNonNeg. + + by move=> l0 u0 x0; apply: ISignNonPos. + + by move=> l0 u0 x0; apply: ISignBoth. +- have uy : u = +oo%O by case: u xu => -[]. + have u0 : (BRight 0%:Z < u)%O by rewrite uy. + case: (leP (BLeft 0%Z) l) => l0. + + suff -> : interval_sign (Interval l u) = Known NonNeg. + by apply: ISignNonNeg => //; apply: le0y. + rewrite /=/itv_bound_signl /itv_bound_signr uy/=. + by case: eqP => [//| /eqP lneq0]; case: ltgtP l0 lneq0. + + suff -> : interval_sign (Interval l u) = Unknown by exact: ISignBoth. + rewrite /=/itv_bound_signl /itv_bound_signr uy/=. + by case: eqP l0 => [->//| /eqP leq0] /ltW->. +- have ly : l = -oo%O by case: l xl => -[]. + have l0 : (l < BLeft 0%:Z)%O by rewrite ly. + case: (leP u (BRight 0%Z)) => u0. + + suff -> : interval_sign (Interval l u) = Known NonPos by exact: ISignNonPos. + rewrite /=/itv_bound_signl /itv_bound_signr ly/=. + by case: eqP => [//| /eqP uneq0]; case: ltgtP u0 uneq0. + + suff -> : interval_sign (Interval l u) = Unknown by exact: ISignBoth. + rewrite /=/itv_bound_signl /itv_bound_signr ly/=. + by case: eqP u0 => [->//| /eqP ueq0]; rewrite ltNge => /negbTE->. +Qed. + +Lemma ext_mul_itv_boundl_subproof b1 b2 (x1 x2 : \bar R) : + (BLeft 0%:Z <= b1 -> BLeft 0%:Z <= b2 -> + ext_num_itv_bound b1 <= BLeft x1 -> + ext_num_itv_bound b2 <= BLeft x2 -> + ext_num_itv_bound (mul_itv_boundl_subdef b1 b2) <= BLeft (x1 * x2))%O. +Proof. +move=> b10 b20 b1x1 b2x2. +have x10 : 0 <= x1. + by case: x1 b1x1 (le_trans (eqbRL (ext_le_map_itv_bound _ _) b10) b1x1). +have x20 : 0 <= x2. + by case: x2 b2x2 (le_trans (eqbRL (ext_le_map_itv_bound _ _) b20) b2x2). +have x1r : (0 >=< x1)%O by rewrite real_fine; exact/ger0_real/fine_ge0. +have x2r : (0 >=< x2)%O by rewrite real_fine; exact/ger0_real/fine_ge0. +have ley b1' b2' : + (Itv.map_itv_bound EFin (num_itv_bound R (mul_itv_boundl_subdef b1' b2')) + <= BLeft +oo%E)%O. + by case: b1' b2' => [[] [[| ?] | ?] | []] [[] [[| ?] | ?] | []]//=; + rewrite bnd_simp ?real_leey ?real_ltry/= ?realz. +case: x1 x2 x10 x20 x1r x2r b1x1 b2x2 => [x1||] [x2||] //= x10 x20 x1r x2r. +- rewrite !(map_itv_bound_comp, EFin_BLeft_le_map_itv_bound)/=. + exact: mul_itv_boundl_subproof. +- rewrite !(map_itv_bound_comp EFin intr) real_mulry//= => b1x1 _. + case: (comparable_ltgtP x1r) x10 => [x10 |//| [x10]] _. + by rewrite gtr0_sg ?mul1e ?bnd_simp. + rewrite -x10 sgr0 mul0e/= EFin_BLeft_le_map_itv_bound. + suff -> : b1 = BLeft 0%Z by case: b2 {b20}. + apply/le_anti; rewrite b10 andbT. + move: b1x1; rewrite EFin_BLeft_le_map_itv_bound. + by rewrite -x10 -(mulr0z 1) intr_BLeft_le_map_itv_bound. +- rewrite !(map_itv_bound_comp EFin intr) real_mulyr//= => _ b2x2. + case: (comparable_ltgtP x2r) x20 => [x20 |//| [x20]] _. + by rewrite gtr0_sg ?mul1e ?bnd_simp. + rewrite -x20 sgr0 mul0e/= EFin_BLeft_le_map_itv_bound. + suff -> : b2 = BLeft 0%Z by case: b1 {b10} => [[] [] []|]. + apply/le_anti; rewrite b20 andbT. + move: b2x2; rewrite EFin_BLeft_le_map_itv_bound. + by rewrite -x20 -(mulr0z 1) intr_BLeft_le_map_itv_bound. +- by rewrite mulyy/= 3!map_itv_bound_comp. +Qed. + +Lemma ext_mul_itv_boundr_subproof b1 b2 (x1 x2 : \bar R) : + (0 <= x1 -> 0 <= x2 -> + BRight x1 <= ext_num_itv_bound b1 -> + BRight x2 <= ext_num_itv_bound b2 -> + BRight (x1 * x2) <= ext_num_itv_bound (mul_itv_boundr_subdef b1 b2))%O. +Proof. +move=> x10 x20 b1x1 b2x2. +have x1r : (0 >=< x1)%O by rewrite real_fine; exact/ger0_real/fine_ge0. +have x2r : (0 >=< x2)%O by rewrite real_fine; exact/ger0_real/fine_ge0. +case: x1 x2 x10 x20 x1r x2r b1x1 b2x2 => [x1||] [x2||] //= x10 x20 x1r x2r. +- rewrite !(map_itv_bound_comp, BRight_EFin_le_map_itv_bound)/=. + exact: mul_itv_boundr_subproof. +- rewrite real_mulry// => b1x1 b2x2. + have -> : b2 = +oo%O by case: b2 b2x2 => -[]. + rewrite mul_itv_boundrC_subproof/= map_itv_bound_comp. + case: (comparable_ltgtP x1r) x10 => [x10 |//| [x10]] _. + + rewrite gtr0_sg ?mul1e ?bnd_simp//. + suff: (BRight 0%Z < b1)%O by case: b1 b1x1 => [[] [] [] |]. + move: b1x1; rewrite map_itv_bound_comp BRight_EFin_le_map_itv_bound. + case: b1 => [[] b1 |//]; rewrite !bnd_simp -(@ltr0z R). + * exact/le_lt_trans/ltW. + * exact/lt_le_trans. + + rewrite -x10 sgr0 mul0e/= BRight_EFin_le_map_itv_bound. + suff: (BRight 0%Z <= b1)%O by case: b1 b1x1 => [[] [] [] |]. + move: b1x1; rewrite map_itv_bound_comp BRight_EFin_le_map_itv_bound. + by rewrite -x10 -(@mulr0z R 1) BRight_intr_le_map_itv_bound. +- rewrite real_mulyr// => b1x1 b2x2. + have -> : b1 = +oo%O by case: b1 b1x1 => -[]. + rewrite /= map_itv_bound_comp. + case: (comparable_ltgtP x2r) x20 => [x20 |//| [x20]] _. + + rewrite gtr0_sg ?mul1e ?bnd_simp//. + suff: (BRight 0%Z < b2)%O by case: b2 b2x2 => [[] [] [] |]. + move: b2x2; rewrite map_itv_bound_comp BRight_EFin_le_map_itv_bound. + case: b2 => [[] b2 |//]; rewrite !bnd_simp -(@ltr0z R). + * exact/le_lt_trans/ltW. + * exact/lt_le_trans. + + rewrite -x20 sgr0 mul0e/= BRight_EFin_le_map_itv_bound. + suff: (BRight 0%Z <= b2)%O by case: b2 b2x2 => [[] [] [] |]. + move: b2x2; rewrite map_itv_bound_comp BRight_EFin_le_map_itv_bound. + by rewrite -x20 -(@mulr0z R 1) BRight_intr_le_map_itv_bound. +- rewrite mulyy/= => b1x1 b2x2. + have -> : b1 = +oo%O by case: b1 b1x1 => -[]. + by have -> : b2 = +oo%O by case: b2 b2x2 => -[]. +Qed. + +Lemma ext_mul_itv_boundr'_subproof b1 b2 (x1 x2 : \bar R) : + (0 <= x1 -> (0 >=< x2)%O -> BRight 0%Z <= b2 -> + BRight x1 <= ext_num_itv_bound b1 -> + BRight x2 <= ext_num_itv_bound b2 -> + BRight (x1 * x2) <= ext_num_itv_bound (mul_itv_boundr_subdef b1 b2))%O. +Proof. +move=> x1ge0 x2r b2ge0 lex1b1 lex2b2. +have /orP[x2ge0 | x2le0] : (0 <= x2) || (x2 <= 0). +- by case: x2 x2r {lex2b2} => [x2 /=|_|_]; rewrite ?lee_fin ?le0y ?leNy0. +- exact: ext_mul_itv_boundr_subproof. +have lem0 : (BRight (x1 * x2) <= BRight 0%R)%O. + by have:= mule_ge0_le0 x1ge0 x2le0; case: mule. +apply: le_trans lem0 _. +rewrite map_itv_bound_comp BRight_EFin_le_map_itv_bound/=. +rewrite -(@mulr0z R 1) BRight_intr_le_map_itv_bound. +apply: mul_itv_boundr_BRight_subproof => //. +case: x1 x1ge0 lex1b1 => [x1||//]/= x1ge0; last by case: b1 => -[]. +rewrite map_itv_bound_comp BRight_EFin_le_map_itv_bound. +rewrite -(@BRight_intr_le_map_itv_bound R)/=. +by apply: le_trans; rewrite bnd_simp -lee_fin. +Qed. + +Lemma comparable_ext_num_itv_bound_subproof (x y : itv_bound int) : + (ext_num_itv_bound x >=< ext_num_itv_bound y)%O. +Proof. +apply/orP; rewrite !(map_itv_bound_comp EFin intr)/= !EFin_le_map_itv_bound. +exact/orP/comparable_num_itv_bound_subproof. +Qed. + +Lemma ext_map_itv_bound_min (x y : itv_bound int) : + ext_num_itv_bound (Order.min x y) + = Order.min (ext_num_itv_bound x) (ext_num_itv_bound y). +Proof. +have [lexy | ltyx] := leP x y; [by rewrite !minEle ext_le_map_itv_bound lexy|]. +rewrite minElt -if_neg -comparable_leNgt ?ext_le_map_itv_bound ?ltW//. +exact: comparable_ext_num_itv_bound_subproof. +Qed. + +Lemma ext_map_itv_bound_max (x y : itv_bound int) : + ext_num_itv_bound (Order.max x y) + = Order.max (ext_num_itv_bound x) (ext_num_itv_bound y). +Proof. +have [lexy | ltyx] := leP x y; [by rewrite !maxEle ext_le_map_itv_bound lexy|]. +rewrite maxElt -if_neg -comparable_leNgt ?ext_le_map_itv_bound ?ltW//. +exact: comparable_ext_num_itv_bound_subproof. +Qed. + +Lemma mule_inum_subproof xi yi (x : ext_num_def xi) (y : ext_num_def yi) + (r := itv_real2_subdef mul_itv_subdef xi yi) : + ext_num_spec r (x%:inum * y%:inum). +Proof. +rewrite {}/r; case: xi yi x y => [//| [xl xu]] [//| [yl yu]]. +case=> [x /=/and3P[xr /= xlx xxu]] [y /=/and3P[yr /= yly yyu]]. +rewrite -/(interval_sign (Interval xl xu)) -/(interval_sign (Interval yl yu)). +have ns000 : ext_num_sem `[0%Z, 0%Z] 0 by apply/and3P; rewrite ?comparablexx. +have xyr : (0 >=< (x * y)%E)%O by exact: realMe. +case: (ext_interval_signP xlx xxu xr) => xlb xub xs. +- by rewrite xs mul0e; case: (ext_interval_signP yly yyu yr). +- case: (ext_interval_signP yly yyu yr) => ylb yub ys. + + by rewrite ys mule0. + + apply/and3P; split=> //=. + * exact: ext_mul_itv_boundl_subproof. + * exact: ext_mul_itv_boundr_subproof. + + apply/and3P; split=> //=; rewrite -[x * y]oppeK -real_muleN//. + * rewrite oppe_itv_boundl_subproof. + by rewrite ext_mul_itv_boundr_subproof ?oppe_ge0 ?oppe_itv_boundr_subproof. + * rewrite oppe_itv_boundr_subproof. + rewrite ext_mul_itv_boundl_subproof ?oppe_itv_boundl_subproof//. + by rewrite opp_itv_ge0_subproof. + + apply/and3P; split=> //=. + * rewrite -[x * y]oppeK -real_muleN// oppe_itv_boundl_subproof. + rewrite ext_mul_itv_boundr'_subproof -?real_fine ?oppe_cmp0 + ?oppe_itv_boundr_subproof//. + by rewrite opp_itv_gt0_subproof ltW. + * by rewrite ext_mul_itv_boundr'_subproof// ltW. +- case: (ext_interval_signP yly yyu yr) => ylb yub ys. + + by rewrite ys mule0. + + apply/and3P; split=> //=; rewrite -[x * y]oppeK -real_mulNe//. + * rewrite oppe_itv_boundl_subproof. + by rewrite ext_mul_itv_boundr_subproof ?oppe_ge0 ?oppe_itv_boundr_subproof. + * rewrite oppe_itv_boundr_subproof. + rewrite ext_mul_itv_boundl_subproof ?oppe_itv_boundl_subproof//. + by rewrite opp_itv_ge0_subproof. + + apply/and3P; split=> //=; rewrite -real_muleNN//. + * by rewrite ext_mul_itv_boundl_subproof + ?opp_itv_ge0_subproof ?oppe_itv_boundl_subproof. + * by rewrite ext_mul_itv_boundr_subproof ?oppe_ge0 ?oppe_itv_boundr_subproof. + + apply/and3P; split=> //=; rewrite -[x * y]oppeK. + * rewrite -real_mulNe// oppe_itv_boundl_subproof. + rewrite ext_mul_itv_boundr'_subproof ?oppe_ge0 ?oppe_itv_boundr_subproof//. + exact: ltW. + * rewrite oppeK -real_muleNN//. + by rewrite ext_mul_itv_boundr'_subproof ?oppe_itv_boundr_subproof + ?oppe_ge0 ?oppe_cmp0 ?opp_itv_gt0_subproof// ltW. +- case: (ext_interval_signP yly yyu yr) => ylb yub ys. + + by rewrite ys mule0. + + apply/and3P; split=> //=; rewrite muleC mul_itv_boundrC_subproof. + * rewrite -[y * x]oppeK -real_muleN// oppe_itv_boundl_subproof. + rewrite ext_mul_itv_boundr'_subproof ?oppe_ge0 ?oppe_cmp0 + ?oppe_itv_boundr_subproof//. + by rewrite opp_itv_gt0_subproof ltW. + * by rewrite ext_mul_itv_boundr'_subproof// ltW. + + apply/and3P; split=> //=; rewrite muleC mul_itv_boundrC_subproof. + * rewrite -[y * x]oppeK -real_mulNe// oppe_itv_boundl_subproof. + rewrite ext_mul_itv_boundr'_subproof ?oppe_ge0 ?oppe_itv_boundr_subproof//. + exact: ltW. + * rewrite -real_muleNN// ext_mul_itv_boundr'_subproof ?oppe_ge0 + ?oppe_cmp0 ?oppe_itv_boundr_subproof//. + by rewrite opp_itv_gt0_subproof ltW. +apply/and3P; rewrite xyr/= ext_map_itv_bound_min ext_map_itv_bound_max. +rewrite (comparable_ge_min _ (comparable_ext_num_itv_bound_subproof _ _)). +rewrite (comparable_le_max _ (comparable_ext_num_itv_bound_subproof _ _)). +have [x0 | /ltW x0] : 0 <= x \/ x < 0; [|split=> //..]. + case: x xr {xlx xxu xyr xs} => [x||] /= xr. + - by case: (comparable_leP xr) => x0; [left | right]. + - by left; rewrite le0y. + - by right; rewrite ltNy0. +- apply/orP; right; rewrite -[x * y]oppeK -real_muleN// oppe_itv_boundl_subproof. + rewrite ext_mul_itv_boundr'_subproof ?oppe_cmp0 ?oppe_itv_boundr_subproof//. + by rewrite opp_itv_gt0_subproof ltW. +- by apply/orP; right; rewrite ext_mul_itv_boundr'_subproof// ltW. +- apply/orP; left; rewrite -[x * y]oppeK -real_mulNe// oppe_itv_boundl_subproof. + rewrite ext_mul_itv_boundr'_subproof ?oppe_ge0 ?oppe_itv_boundr_subproof//. + exact: ltW. +- apply/orP; left; rewrite -real_muleNN//. + rewrite ext_mul_itv_boundr'_subproof ?oppe_ge0 ?oppe_cmp0 + ?oppe_itv_boundr_subproof//. + by rewrite opp_itv_gt0_subproof ltW. +Qed. + +Canonical mule_inum xi yi (x : ext_num_def xi) (y : ext_num_def yi) := + Itv.mk (mule_inum_subproof x y). + +Definition abse_itv_subdef (i : Itv.t) : Itv.t := + match i with + | Itv.Top => Itv.Real `[0%Z, +oo[ + | Itv.Real (Interval l u) => + match l with + | BRight (Posz _) | BLeft (Posz (S _)) => Itv.Real `]0%Z, +oo[ + | _ => Itv.Real `[0%Z, +oo[ + end + end. +Arguments abse_itv_subdef /. + +Lemma abse_inum_subproof i (x : ext_num_def i) + (r := abse_itv_subdef i) : + ext_num_spec r `|x%:inum|. +Proof. +have: ext_num_sem `[0%Z, +oo[ `|x%:inum|. + apply/and3P; split; rewrite ?bnd_simp ?abse_ge0//. + by case: x%:inum => [x'||]; rewrite ?cmp0y// le_comparable ?abse_ge0. +have: 0 < x%:inum -> ext_num_sem `]0%Z, +oo[ `|x%:inum|. + move=> xgt0; apply/and3P; split; rewrite ?bnd_simp//. + - by case: x%:num => [x'||]; rewrite ?cmp0y// le_comparable ?abse_ge0. + - case: x%:inum xgt0 => [x'|//|//]/=. + by rewrite !lte_fin normr_gt0; apply: lt0r_neq0. +rewrite {}/r; case: i x => [//| [[[] [[//| l] | //] | //] u]] [x /=] + + _; + move/and3P => [xr /= /[!bnd_simp]lx _]; apply. +- by apply: lt_le_trans lx; rewrite lte_fin ltr0z. +- by apply: le_lt_trans lx; rewrite lee_fin ler0z. +- by apply: lt_trans lx; rewrite lte_fin ltr0z. +Qed. + +Canonical abse_inum i (x : ext_num_def i) := Itv.mk (abse_inum_subproof x). + +Lemma ext_min_itv_boundl_subproof x1 x2 b1 b2 : + (ext_num_itv_bound b1 <= BLeft x1)%O -> + (ext_num_itv_bound b2 <= BLeft x2)%O -> + (ext_num_itv_bound (Order.min b1 b2) <= BLeft (Order.min x1 x2))%O. +Proof. +case: (leP b1 b2) => [b1_le_b2 | /ltW b2_le_b1]. +- have sb1_le_sb2 := eqbRL (ext_le_map_itv_bound _ _) b1_le_b2. + by rewrite minElt; case: (x1 < x2)%O => [//|_]; apply: le_trans. +- have sb2_le_sb1 := eqbRL (ext_le_map_itv_bound _ _) b2_le_b1. + by rewrite minElt; case: (x1 < x2)%O => [+ _|//]; apply: le_trans. +Qed. + +Lemma ext_min_itv_boundr_subproof x1 x2 b1 b2 : (x1 >=< x2)%O -> + (BRight x1 <= ext_num_itv_bound b1)%O -> + (BRight x2 <= ext_num_itv_bound b2)%O -> + (BRight (Order.min x1 x2) <= ext_num_itv_bound (Order.min b1 b2))%O. +Proof. +move=> x1_cmp_x2; case: (leP b1 b2) => [b1_le_b2 | /ltW b2_le_b1]. +- have sb1_le_sb2 := eqbRL (ext_le_map_itv_bound _ _) b1_le_b2. + by case: (comparable_leP x1_cmp_x2) => [//| /ltW ? + _]; apply: le_trans. +- have sb2_le_sb1 := eqbRL (ext_le_map_itv_bound _ _) b2_le_b1. + by case: (comparable_leP x1_cmp_x2) => [? _ |//]; apply: le_trans. +Qed. + +Lemma ext_min_inum_subproof (xi yi : Itv.t) + (x : ext_num_def xi) (y : ext_num_def yi) + (r := itv_real2_subdef min_itv_subdef xi yi) : + ext_num_spec r (Order.min x%:inum y%:inum). +Proof. +apply: itv_real2_subproof (Itv.P x) (Itv.P y). +case: x y => [x /= _] [y /= _] => {xi yi r} -[lx ux] [ly uy]/=. +move=> /andP[xr /=/andP[lxx xux]] /andP[yr /=/andP[lyy yuy]]. +apply/and3P; split. +- case: x y xr yr {lxx xux lyy yuy} => [x||] [y||]//=. + + by move=> ? ?; apply: comparable_minr. + + by move=> ? ?; rewrite real_miney. + + by move=> ? ?; rewrite real_minNye. +- exact: ext_min_itv_boundl_subproof. +- by apply: ext_min_itv_boundr_subproof => //; apply: ereal_comparable. +Qed. + +Lemma ext_max_itv_boundl_subproof x1 x2 b1 b2 : (x1 >=< x2)%O -> + (ext_num_itv_bound b1 <= BLeft x1)%O -> + (ext_num_itv_bound b2 <= BLeft x2)%O -> + (ext_num_itv_bound (Order.max b1 b2) <= BLeft (Order.max x1 x2))%O. +Proof. +move=> x1_cmp_x2. +case: (leP b1 b2) => [b1_le_b2 | /ltW b2_le_b1]. +- case: (comparable_leP x1_cmp_x2) => [//| /ltW ? _ sb2_x2]. + exact: le_trans sb2_x2 _. +- case: (comparable_leP x1_cmp_x2) => [? sb1_x1 _ |//]. + exact: le_trans sb1_x1 _. +Qed. + +Lemma ext_max_itv_boundr_subproof x1 x2 b1 b2 : + (BRight x1 <= ext_num_itv_bound b1)%O -> + (BRight x2 <= ext_num_itv_bound b2)%O -> + (BRight (Order.max x1 x2) <= ext_num_itv_bound (Order.max b1 b2))%O. +Proof. +case: (leP b1 b2) => [b1_le_b2 | /ltW b2_le_b1]. +- have sb1_le_sb2 := eqbRL (ext_le_map_itv_bound _ _) b1_le_b2. + by rewrite maxElt; case: ifP => [//|_ ? _]; apply: le_trans sb1_le_sb2. +- have sb2_le_sb1 := eqbRL (ext_le_map_itv_bound _ _) b2_le_b1. + by rewrite maxElt; case: ifP => [_ _ ?|//]; apply: le_trans sb2_le_sb1. +Qed. + +Lemma ext_max_inum_subproof (xi yi : Itv.t) + (x : ext_num_def xi) (y : ext_num_def yi) + (r := itv_real2_subdef max_itv_subdef xi yi) : + ext_num_spec r (Order.max x%:inum y%:inum). +Proof. +apply: itv_real2_subproof (Itv.P x) (Itv.P y). +case: x y => [x /= _] [y /= _] => {xi yi r} -[lx ux] [ly uy]/=. +move=> /andP[xr /=/andP[lxx xux]] /andP[yr /=/andP[lyy yuy]]. +apply/and3P; split. +- case: x y xr yr {lxx xux lyy yuy} => [x||] [y||]//=. + + by move=> ? ?; apply: comparable_maxr. + + by move=> ? ?; rewrite real_maxey. + + by move=> ? ?; rewrite real_maxNye. +- by apply: ext_max_itv_boundl_subproof => //; apply: ereal_comparable. +- exact: ext_max_itv_boundr_subproof. +Qed. + +Canonical ext_min_max_typ (R : numDomainType) := + MinMaxTyp ext_min_inum_subproof ext_max_inum_subproof. + +End Itv. + +Arguments gt0e {R i} _ {_}. +Arguments lte0 {R i} _ {_}. +Arguments ge0e {R i} _ {_}. +Arguments lee0 {R i} _ {_}. +Arguments cmp0e {R i} _ {_}. +Arguments neqe0 {R i} _ {_}. +Arguments ext_widen_itv {R i} _ {_ _}. + +Definition posnume (R : numDomainType) of phant R := + Itv.def (@ext_num_sem R) (Itv.Real `]0%Z, +oo[). +Notation "{ 'posnum' '\bar' R }" := (@posnume _ (Phant R)) : type_scope. +Definition nonnege (R : numDomainType) of phant R := + Itv.def (@ext_num_sem R) (Itv.Real `[0%Z, +oo[). +Notation "{ 'nonneg' '\bar' R }" := (@nonnege _ (Phant R)) : type_scope. +Notation "x %:pos" := (ext_widen_itv x%:itv : {posnum \bar _}) (only parsing) + : ereal_dual_scope. +Notation "x %:pos" := (ext_widen_itv x%:itv : {posnum \bar _}) (only parsing) + : ereal_scope. +Notation "x %:pos" := (@ext_widen_itv _ _ + (@Itv.from _ _ _ (Phantom _ x)) (Itv.Real `]Posz 0, +oo[) _) + (only printing) : ereal_dual_scope. +Notation "x %:pos" := (@ext_widen_itv _ _ + (@Itv.from _ _ _ (Phantom _ x)) (Itv.Real `]Posz 0, +oo[) _) + (only printing) : ereal_scope. +Notation "x %:nng" := (ext_widen_itv x%:itv : {nonneg \bar _}) (only parsing) + : ereal_dual_scope. +Notation "x %:nng" := (ext_widen_itv x%:itv : {nonneg \bar _}) (only parsing) + : ereal_scope. +Notation "x %:nng" := (@ext_widen_itv _ _ + (@Itv.from _ _ _ (Phantom _ x)) (Itv.Real `[Posz 0, +oo[) _) + (only printing) : ereal_dual_scope. +Notation "x %:nng" := (@ext_widen_itv _ _ + (@Itv.from _ _ _ (Phantom _ x)) (Itv.Real `[Posz 0, +oo[) _) + (only printing) : ereal_scope. + +#[export] Hint Extern 0 (is_true (0%R < _)%E) => solve [apply: gt0e] : core. +#[export] Hint Extern 0 (is_true (_ < 0%R)%E) => solve [apply: lte0] : core. +#[export] Hint Extern 0 (is_true (0%R <= _)%E) => solve [apply: ge0e] : core. +#[export] Hint Extern 0 (is_true (_ <= 0%R)%E) => solve [apply: lee0] : core. +#[export] Hint Extern 0 (is_true (0%R >=< _)%O) => solve [apply: cmp0e] : core. +#[export] Hint Extern 0 (is_true (_ != 0%R)%O) => solve [apply: neqe0] : core. Section MorphNum. -Context {R : numDomainType} {nz : KnownSign.nullity} {cond : KnownSign.reality}. -Local Notation nR := {compare (0 : \bar R) & nz & cond}. +Context {R : numDomainType} {i : Itv.t}. +Local Notation nR := (Itv.def (@ext_num_sem R) i). Implicit Types (a : \bar R). Lemma num_abse_eq0 a : (`|a|%:nng == 0%:E%:nng) = (a == 0). @@ -3665,10 +4153,9 @@ Proof. by rewrite -abse_eq0. Qed. End MorphNum. Section MorphReal. -Context {R : numDomainType} {nz : KnownSign.nullity} {r : KnownSign.real}. -Local Notation nR := {compare (0 : \bar R) & nz & r}. -Implicit Type x y : nR. -Local Notation num := (@num _ _ (0 : R) nz r). +Context {R : numDomainType} {xi yi : interval int}. +Implicit Type x : (Itv.def (@ext_num_sem R) (Itv.Real xi)). +Implicit Type y : (Itv.def (@ext_num_sem R) (Itv.Real yi)). Lemma num_lee_max a x y : a <= maxe x%:num y%:num = (a <= x%:num) || (a <= y%:num). @@ -3703,35 +4190,6 @@ Lemma num_gte_min a x y : Proof. by rewrite -comparable_gt_min// ereal_comparable. Qed. End MorphReal. -#[deprecated(since="mathcomp-analysis 1.2.0", note="renamed `num_lee_max`")] -Notation num_lee_maxr := num_lee_max (only parsing). -#[deprecated(since="mathcomp-analysis 1.2.0", note="renamed `num_gee_max`")] -Notation num_lee_maxl := num_gee_max (only parsing). -#[deprecated(since="mathcomp-analysis 1.2.0", note="renamed `num_lee_min`")] -Notation num_lee_minr := num_lee_min (only parsing). -#[deprecated(since="mathcomp-analysis 1.2.0", note="renamed `num_gee_min`")] -Notation num_lee_minl := num_gee_min (only parsing). -#[deprecated(since="mathcomp-analysis 1.2.0", note="renamed `num_lte_max`")] -Notation num_lte_maxr := num_lte_max (only parsing). -#[deprecated(since="mathcomp-analysis 1.2.0", note="renamed `num_gte_max`")] -Notation num_lte_maxl := num_gte_max (only parsing). -#[deprecated(since="mathcomp-analysis 1.2.0", note="renamed `num_lte_min`")] -Notation num_lte_minr := num_lte_min (only parsing). -#[deprecated(since="mathcomp-analysis 1.2.0", note="renamed `num_gte_min`")] -Notation num_lte_minl := num_gte_min (only parsing). - -Section MorphGe0. -Context {R : numDomainType} {nz : KnownSign.nullity}. -Local Notation nR := {compare (0 : \bar R) & ?=0 & >=0}. -Implicit Type x y : nR. -Local Notation num := (@num _ _ (0 : \bar R) ?=0 >=0). - -Lemma num_abse_le a x : 0 <= a -> (`|a|%:nng <= x)%O = (a <= x%:num). -Proof. by move=> a0; rewrite -num_le//= gee0_abs. Qed. - -Lemma num_abse_lt a x : 0 <= a -> (`|a|%:nng < x)%O = (a < x%:num). -Proof. by move=> a0; rewrite -num_lt/= gee0_abs. Qed. -End MorphGe0. Variant posnume_spec (R : numDomainType) (x : \bar R) : \bar R -> bool -> bool -> bool -> Type := @@ -3856,7 +4314,6 @@ apply: le_mono; move=> -[r0 | | ] [r1 | _ | _] //=. - by rewrite ltr_pdivrMr ?ltr_wpDr// mul1r ltr_pwDl // ler_norm. - rewrite ltr_pdivlMr ?mulN1r ?ltr_wpDr// => _. by rewrite ltrNl ltr_pwDl // ler_normr lexx orbT. -- by rewrite -subr_gt0 opprK. Qed. Definition lt_contract := leW_mono le_contract. diff --git a/reals/prodnormedzmodule.v b/reals/prodnormedzmodule.v index 38bfe229c..06f7ac181 100644 --- a/reals/prodnormedzmodule.v +++ b/reals/prodnormedzmodule.v @@ -1,8 +1,8 @@ (* mathcomp analysis (c) 2020 Inria and AIST. License: CeCILL-C. *) From HB Require Import structures. -From mathcomp Require Import all_ssreflect fingroup ssralg poly ssrnum. +From mathcomp Require Import all_ssreflect fingroup ssralg poly ssrnum. From mathcomp Require Import all_classical. -From mathcomp Require Import signed. +From mathcomp Require Import itv. (**md**************************************************************************) (* This file equips the product of two normedZmodTypes with a canonical *) diff --git a/reals/real_interval.v b/reals/real_interval.v index 15db5ad76..1c42bc9e9 100644 --- a/reals/real_interval.v +++ b/reals/real_interval.v @@ -4,7 +4,7 @@ From mathcomp Require Import fingroup perm rat archimedean finmap. From mathcomp Require Import boolp classical_sets functions. From mathcomp Require Export set_interval. From HB Require Import structures. -From mathcomp Require Import reals constructive_ereal signed. +From mathcomp Require Import reals itv constructive_ereal. (**md**************************************************************************) (* # Sets and intervals on $\overline{\mathbb{R}}$ *) diff --git a/reals/signed.v b/reals/signed.v index 84fc0d8db..93eb07f55 100644 --- a/reals/signed.v +++ b/reals/signed.v @@ -4,6 +4,9 @@ From Coq Require Import ssreflect ssrfun ssrbool. From mathcomp Require Import ssrnat eqtype choice order ssralg ssrnum ssrint. From mathcomp Require Import mathcomp_extra. +Attributes deprecated(since="mathcomp-analysis 1.8.0", + note="Use itv.v instead."). + (**md**************************************************************************) (* # Positive, non-negative numbers, etc. *) (* *) diff --git a/theories/charge.v b/theories/charge.v index d3329dce9..241ede655 100644 --- a/theories/charge.v +++ b/theories/charge.v @@ -4,7 +4,7 @@ From mathcomp Require Import finmap fingroup perm rat. From mathcomp Require Import mathcomp_extra boolp classical_sets cardinality. From mathcomp Require Import functions fsbigop set_interval. From HB Require Import structures. -From mathcomp Require Import reals ereal signed topology numfun normedtype. +From mathcomp Require Import reals itv ereal topology numfun normedtype. From mathcomp Require Import sequences esum measure realfun lebesgue_measure. From mathcomp Require Import lebesgue_integral. @@ -1286,7 +1286,7 @@ Qed. Lemma sup_int_approxRN_fin_num : M \is a fin_num. Proof. -rewrite ge0_fin_numE//; first exact: sup_int_approxRN_lty. +rewrite ge0_fin_numE; first exact: sup_int_approxRN_lty. exact: sup_int_approxRN_ge0. Qed. @@ -1337,7 +1337,7 @@ Qed. Lemma max_approxRN_seq_ge0 n x : 0 <= F_ n x. Proof. -by apply/bigmax_geP; right => /=; exists ord0 => //; exact: approxRN_seq_ge0. +by apply/bigmax_geP; right => /=; exists ord0; [|exact: approxRN_seq_ge0]. Qed. Lemma max_approxRN_seq_ge n x : F_ n x >= g_ n x. @@ -1496,7 +1496,7 @@ Qed. Let F_G m : F m \in G. Proof. -rewrite inE /G/=; split => //. +rewrite inE /G/=; split. - by move=> ?; exact: max_approxRN_seq_ge0. - apply/integrableP; split; first exact: measurable_max_approxRN_seq. under eq_integral. @@ -1569,7 +1569,7 @@ have [muA0|] := eqVneq (mu A) 0. exists (PosNum ltr01). under eq_integral. move=> x _; rewrite -(@gee0_abs _ (_ + _)); last first. - by rewrite adde_ge0// fRN_ge0. + by rewrite adde_ge0 ?fRN_ge0. over. rewrite (@integral_abs_eq0 _ _ _ _ setT)//. by rewrite (le_lt_trans _ h)// integral_ge0// => x Ax; exact: fRN_ge0. @@ -1614,7 +1614,7 @@ move=> mB; rewrite ge0_integralD//; last 2 first. by move=> x Bx; exact: fRN_ge0. exact: measurable_funS measurable_fun_fRN. rewrite fin_numD integral_cst// fin_numM ?fin_num_measure// andbT. -rewrite ge0_fin_numE ?measure_ge0//; last first. +rewrite ge0_fin_numE ?measure_ge0; last first. by apply: integral_ge0 => x Bx; exact: fRN_ge0. rewrite (le_lt_trans _ int_fRN_lty)//. under [in leRHS]eq_integral. @@ -1645,11 +1645,11 @@ apply: cvgeB. + have /cvg_ex[/= l hl] : cvg ((fun n => \sum_(0 <= i < n) \int[mu]_(y in H i) (fRN y + epsRN%:num%:E)) @ \oo). apply: is_cvg_ereal_nneg_natsum => n _. - by apply: integral_ge0 => x _; rewrite adde_ge0//; exact: fRN_ge0. + by apply: integral_ge0 => x _; rewrite adde_ge0 ?fRN_ge0. by rewrite (@cvg_lim _ _ _ _ _ _ l). + apply: emeasurable_funD => //=; apply: measurable_funTS. exact: measurable_fun_fRN. - + by move=> x _; rewrite adde_ge0//; exact: fRN_ge0. + + by move=> x _; rewrite adde_ge0 ?fRN_ge0. Qed. HB.instance Definition _ := @isCharge.Build _ _ _ sigmaRN @@ -1706,7 +1706,7 @@ have mh : measurable_fun setT h. - by apply: measurable_funTS; apply: emeasurable_funD => //; exact: mf. - by apply: measurable_funTS; exact: mf. have hge0 x : 0 <= h x. - by rewrite /h; case: ifPn => [_|?]; [rewrite adde_ge0// f_ge0|exact: f_ge0]. + by rewrite /h; case: ifPn => [_|?]; rewrite ?adde_ge0 ?f_ge0. have hnuP S : measurable S -> S `<=` AP -> \int[mu]_(x in S) h x <= nu S. move=> mS SAP. have : 0 <= sigma S. @@ -1746,7 +1746,7 @@ have int_h_M : \int[mu]_x h x > M. by rewrite setUv//; exact: mf. by move=> x _; exact: f_ge0. rewrite setUv int_fRNE -lte_subel_addl; last first. - rewrite ge0_fin_numE// ?sup_int_approxRN_lty//. + rewrite ge0_fin_numE ?sup_int_approxRN_lty. exact: approxRN_seq.sup_int_approxRN_lty. exact: sup_int_approxRN_ge0. by rewrite /M subee ?mule_gt0// approxRN_seq.sup_int_approxRN_fin_num. @@ -1942,8 +1942,8 @@ have -> : \int[mu]_(x in E) (f \* g) x = - move=> n; apply/emeasurable_funM; apply/measurable_funTS. exact/measurable_EFinP. exact: measurable_int (f_integrable _). - - by move=> n x Ex //=; rewrite mule_ge0 ?lee_fin//=; exact: f_ge0. - - by move=> x Ex a b /ndh /= /lefP hahb; rewrite lee_wpmul2r ?lee_fin// f_ge0. + - by move=> n x Ex /=; rewrite mule_ge0 ?lee_fin ?f_ge0. + - by move=> x Ex a b /ndh /= /lefP hahb; rewrite lee_wpmul2r ?lee_fin ?f_ge0. suff suf n : \int[mu]_(x in E) ((EFin \o h n) x * g x) = \int[nu]_(x in E) (EFin \o h n) x. by under eq_fun do rewrite suf. @@ -1974,7 +1974,7 @@ rewrite ge0_integralZl//. by rewrite -integral_mkcondr -f_integral// integral_indic// setIC. - apply: emeasurable_funM; first exact/measurable_EFinP. exact/measurable_funTS/(measurable_int _ (f_integrable _)). -- by move=> t Et; rewrite mule_ge0// ?lee_fin//; exact: f_ge0. +- by move=> t Et; rewrite mule_ge0 ?lee_fin ?f_ge0. - by move: rhn; rewrite inE => -[t _ <-]; rewrite lee_fin. Qed. diff --git a/theories/convex.v b/theories/convex.v index 591d0aa19..e09b544b6 100644 --- a/theories/convex.v +++ b/theories/convex.v @@ -2,7 +2,7 @@ From mathcomp Require Import all_ssreflect ssralg ssrint ssrnum finmap. From mathcomp Require Import matrix interval zmodp vector fieldext falgebra. From mathcomp Require Import mathcomp_extra boolp classical_sets set_interval. -From mathcomp Require Import functions cardinality ereal reals signed. +From mathcomp Require Import functions cardinality ereal reals. From mathcomp Require Import topology prodnormedzmodule normedtype derive. From mathcomp Require Import realfun itv. From HB Require Import structures. diff --git a/theories/derive.v b/theories/derive.v index fc68330d6..cdbd54a61 100644 --- a/theories/derive.v +++ b/theories/derive.v @@ -2,7 +2,7 @@ From HB Require Import structures. From mathcomp Require Import all_ssreflect ssralg ssrnum matrix interval. From mathcomp Require Import mathcomp_extra boolp classical_sets functions. -From mathcomp Require Import reals signed topology prodnormedzmodule tvs. +From mathcomp Require Import reals itv topology prodnormedzmodule tvs. From mathcomp Require Import normedtype landau forms. (**md**************************************************************************) diff --git a/theories/ereal.v b/theories/ereal.v index 015c0e020..2b3585f68 100644 --- a/theories/ereal.v +++ b/theories/ereal.v @@ -8,7 +8,7 @@ From HB Require Import structures. From mathcomp Require Import all_ssreflect all_algebra archimedean finmap. From mathcomp Require Import boolp classical_sets functions. From mathcomp Require Import fsbigop cardinality set_interval. -From mathcomp Require Import reals signed topology. +From mathcomp Require Import reals itv topology. From mathcomp Require Export constructive_ereal. (**md**************************************************************************) @@ -610,47 +610,54 @@ Proof. by apply/funext => x; rewrite /= !patchE; case: ifPn. Qed. Section SignedRealFieldStability. Context {R : realFieldType}. -Definition ereal_sup_reality_subdef (xnz : KnownSign.nullity) - (xr : KnownSign.reality) := - (if KnownSign.wider_reality <=0 xr then KnownSign.Real <=0 - else >=<0)%snum_sign. -Arguments ereal_sup_reality_subdef /. - -Lemma ereal_sup_snum_subproof (xnz : KnownSign.nullity) (xr : KnownSign.reality) - (S : {compare (0 : \bar R) & xnz & xr} -> Prop) - (r := ereal_sup_reality_subdef xnz xr) : - Signed.spec 0 ?=0 r (ereal_sup [set x%:num | x in S]%classic). -Proof. -rewrite {}/r; move: xr S => [[[]|]|] S /=; - do ?[by apply: ub_ereal_sup => _ [? _ <-] - |by case: ereal_sup => [s||]; - rewrite ?leey ?leNye// !lee_fin -realE num_real]. -Qed. - -Canonical ereal_sup_snum (xnz : KnownSign.nullity) (xr : KnownSign.reality) - (S : {compare (0 : \bar R) & xnz & xr} -> Prop) := - Signed.mk (ereal_sup_snum_subproof S). - -Definition ereal_inf_reality_subdef (xnz : KnownSign.nullity) - (xr : KnownSign.reality) := - (if KnownSign.wider_reality >=0 xr then KnownSign.Real >=0 - else >=<0)%snum_sign. -Arguments ereal_inf_reality_subdef /. - -Lemma ereal_inf_snum_subproof (xnz : KnownSign.nullity) (xr : KnownSign.reality) - (S : {compare (0 : \bar R) & xnz & xr} -> Prop) - (r := ereal_inf_reality_subdef xnz xr) : - Signed.spec 0 ?=0 r (ereal_inf [set x%:num | x in S]%classic). -Proof. -rewrite {}/r; move: xr S => [[[]|]|] S /=; - do ?[by apply: lb_ereal_inf => _ [? _ <-] - |by case: ereal_inf => [s||]; - rewrite ?leey ?leNye// !lee_fin -realE num_real]. -Qed. - -Canonical ereal_inf_snum (xnz : KnownSign.nullity) (xr : KnownSign.reality) - (S : {compare (0 : \bar R) & xnz & xr} -> Prop) := - Signed.mk (ereal_inf_snum_subproof S). +Definition ereal_sup_itv_subdef (i : interval int) : interval int := + let 'Interval l u := i in + Interval -oo%O (keep_nonpos_itv_bound_subdef u). +Arguments ereal_sup_itv_subdef /. + +Lemma ereal_sup_inum_subproof i + (S : Itv.def (@ext_num_sem R) i -> Prop) + (r := itv_real1_subdef ereal_sup_itv_subdef i) : + Itv.spec (@ext_num_sem R) r (ereal_sup [set x%:num | x in S]%classic). +Proof. +rewrite {}/r; case: i S => [//| [l u]] S /=. +apply/and3P; split. +- rewrite real_fine -real_leey. + by rewrite ub_ereal_sup// => _ [[[x||] /=/and3P[? ? ?]] _ <-]. +- by case: ereal_sup. +- case: u S => [[] [[| u] | u] S |//]; rewrite /= bnd_simp//; + apply: ub_ereal_sup => _ [[x /=/and3P[_ _ /= +]] _ <-]; rewrite bnd_simp//. + + by move/ltW. + + by move=> /ltW xu; apply: le_trans xu _; rewrite lee_fin lerz0. + + by move=> xu; apply: le_trans xu _; rewrite lee_fin lerz0. +Qed. + +Canonical ereal_sup_inum i (S : Itv.def (@ext_num_sem R) i -> Prop) := + Itv.mk (ereal_sup_inum_subproof S). + +Definition ereal_inf_itv_subdef (i : interval int) : interval int := + let 'Interval l u := i in + Interval (keep_nonneg_itv_bound_subdef l) +oo%O. +Arguments ereal_inf_itv_subdef /. + +Lemma ereal_inf_inum_subproof i + (S : Itv.def (@ext_num_sem R) i -> Prop) + (r := itv_real1_subdef ereal_inf_itv_subdef i) : + Itv.spec (@ext_num_sem R) r (ereal_inf [set x%:num | x in S]%classic). +Proof. +rewrite {}/r; case: i S => [//| [l u]] S /=. +apply/and3P; split. +- rewrite real_fine -real_leNye. + by rewrite lb_ereal_inf// => _ [[[x||] /=/and3P[? ? ?]] _ <-]. +- case: l S => [[] [l | l] S |//]; rewrite /= bnd_simp//; + apply: lb_ereal_inf => _ [[x /=/and3P[_ /= + _]] _ <-]; rewrite bnd_simp. + + by apply: le_trans; rewrite lee_fin ler0z. + + by move=> /ltW; apply: le_trans; rewrite lee_fin ler0z. +- by case: ereal_inf. +Qed. + +Canonical ereal_inf_inum i (S : Itv.def (@ext_num_sem R) i -> Prop) := + Itv.mk (ereal_inf_inum_subproof S). End SignedRealFieldStability. diff --git a/theories/esum.v b/theories/esum.v index 57959228b..3b289711b 100644 --- a/theories/esum.v +++ b/theories/esum.v @@ -1,7 +1,7 @@ (* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C. *) From mathcomp Require Import all_ssreflect ssralg ssrnum finmap. From mathcomp Require Import mathcomp_extra boolp classical_sets functions. -From mathcomp Require Import cardinality fsbigop reals ereal signed. +From mathcomp Require Import cardinality fsbigop reals ereal itv. From mathcomp Require Import topology sequences normedtype numfun. (**md**************************************************************************) @@ -256,7 +256,7 @@ apply: (@le_trans _ _ rewrite (fsetIidPr _). rewrite fsbig_finite// leeDl// big_seq sume_ge0//=. move=> [x y] /imfsetP[[x1 y1]] /[!inE] /andP[] /imfset2P[x2]/= /[!inE]. - rewrite andbT in_fset_set//; last exact: finite_set_fst. + rewrite andbT in_fset_set; last exact: finite_set_fst. move=> /[!inE] x2X [y2] /[!inE] /andP[] /[!in_fset_set]; last first. exact: finite_set_snd. move=> /[!inE] y2X y2J [-> ->] _ [-> ->]; rewrite a_ge0//. diff --git a/theories/exp.v b/theories/exp.v index 8f709ed49..c9811ce46 100644 --- a/theories/exp.v +++ b/theories/exp.v @@ -2,7 +2,7 @@ From mathcomp Require Import all_ssreflect ssralg ssrint ssrnum matrix. From mathcomp Require Import interval rat. From mathcomp Require Import boolp classical_sets functions. -From mathcomp Require Import mathcomp_extra reals ereal signed. +From mathcomp Require Import mathcomp_extra reals ereal itv. From mathcomp Require Import topology tvs normedtype landau sequences derive. From mathcomp Require Import realfun itv convex. diff --git a/theories/ftc.v b/theories/ftc.v index bbc908701..27106ecba 100644 --- a/theories/ftc.v +++ b/theories/ftc.v @@ -2,7 +2,7 @@ From HB Require Import structures. From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint interval finmap. From mathcomp Require Import mathcomp_extra boolp classical_sets functions. -From mathcomp Require Import cardinality fsbigop signed reals ereal. +From mathcomp Require Import cardinality fsbigop reals itv ereal. From mathcomp Require Import topology tvs normedtype sequences real_interval. From mathcomp Require Import esum measure lebesgue_measure numfun realfun. From mathcomp Require Import lebesgue_integral derive charge. diff --git a/theories/function_spaces.v b/theories/function_spaces.v index cc56990f6..f0d714e12 100644 --- a/theories/function_spaces.v +++ b/theories/function_spaces.v @@ -3,7 +3,7 @@ From HB Require Import structures. From mathcomp Require Import all_ssreflect all_algebra finmap generic_quotient. From mathcomp Require Import boolp classical_sets functions. From mathcomp Require Import cardinality mathcomp_extra fsbigop. -From mathcomp Require Import reals signed topology separation_axioms. +From mathcomp Require Import reals itv topology separation_axioms. (**md**************************************************************************) (* # The topology of functions spaces *) diff --git a/theories/hoelder.v b/theories/hoelder.v index b7476215d..e0f299a19 100644 --- a/theories/hoelder.v +++ b/theories/hoelder.v @@ -2,7 +2,7 @@ From HB Require Import structures. From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint interval finmap. From mathcomp Require Import mathcomp_extra boolp classical_sets functions. -From mathcomp Require Import cardinality fsbigop signed reals ereal. +From mathcomp Require Import cardinality fsbigop reals ereal. From mathcomp Require Import topology normedtype sequences real_interval. From mathcomp Require Import esum measure lebesgue_measure lebesgue_integral. From mathcomp Require Import numfun exp convex itv. @@ -365,7 +365,7 @@ move=> mf mg. rewrite !Lnorm1 -ge0_integralD//; [|by do 2 apply: measurableT_comp..]. rewrite ge0_le_integral//. - by do 2 apply: measurableT_comp => //; exact: measurable_funD. -- by move=> x _; rewrite lee_fin. +- by move=> x _; rewrite adde_ge0. - by apply/measurableT_comp/measurable_funD; exact/measurableT_comp. - by move=> x _; rewrite lee_fin ler_normD. Qed. diff --git a/theories/kernel.v b/theories/kernel.v index 4d154d267..0d0c0ec4d 100644 --- a/theories/kernel.v +++ b/theories/kernel.v @@ -2,7 +2,7 @@ From HB Require Import structures. From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint interval finmap. From mathcomp Require Import mathcomp_extra boolp classical_sets functions. -From mathcomp Require Import cardinality fsbigop reals ereal signed. +From mathcomp Require Import cardinality fsbigop reals itv ereal. From mathcomp Require Import topology normedtype sequences esum measure. From mathcomp Require Import numfun lebesgue_measure lebesgue_integral. diff --git a/theories/landau.v b/theories/landau.v index bee296e96..07118461b 100644 --- a/theories/landau.v +++ b/theories/landau.v @@ -2,7 +2,7 @@ From HB Require Import structures. From mathcomp Require Import all_ssreflect ssralg ssrnum. From mathcomp Require Import mathcomp_extra boolp classical_sets functions. -From mathcomp Require Import ereal reals signed topology normedtype. +From mathcomp Require Import ereal reals itv topology normedtype. From mathcomp Require Import prodnormedzmodule. (**md**************************************************************************) @@ -480,7 +480,7 @@ Proof. split=> [[k k0 fOg] | [k [kreal fOg]]]. exists k; rewrite realE (ltW k0) /=; split=> // l ltkl; move: fOg. by apply: filter_app; near=> x => /le_trans; apply; rewrite ler_wpM2r // ltW. -exists (Num.max 1 `|k + 1|) => //. +exists (Num.max 1 `|k + 1|); first exact/gt0/K. apply: fOg; rewrite (@lt_le_trans _ _ `|k + 1|) //. by rewrite (@lt_le_trans _ _ (k + 1)) ?ltrDl // real_ler_norm ?realD. by rewrite comparable_le_max ?real_comparable// lexx orbT. diff --git a/theories/lebesgue_integral.v b/theories/lebesgue_integral.v index c9b2bbfaf..38cde5ed0 100644 --- a/theories/lebesgue_integral.v +++ b/theories/lebesgue_integral.v @@ -3,7 +3,7 @@ From HB Require Import structures. From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint interval finmap. From mathcomp Require Import archimedean. From mathcomp Require Import boolp classical_sets functions. -From mathcomp Require Import cardinality fsbigop signed reals ereal topology. +From mathcomp Require Import cardinality fsbigop reals itv ereal topology. From mathcomp Require Import tvs normedtype sequences real_interval esum measure. From mathcomp Require Import lebesgue_measure numfun realfun function_spaces. @@ -1680,7 +1680,7 @@ have mh2 : measurable_fun setT h2 by exact/(measurable_restrictT _ _).1. have [g1 [nd_g1 gh1]] := approximation measurableT mh1 (fun x _ => h10 x). have [g2 [nd_g2 gh2]] := approximation measurableT mh2 (fun x _ => h20 x). pose g12 := fun n => add_nnsfun (g1 n) (g2 n). -rewrite (@nd_ge0_integral_lim _ _ _ mu _ g12) //; last 3 first. +rewrite (@nd_ge0_integral_lim _ _ _ mu _ g12); last 3 first. - by move=> x; rewrite adde_ge0. - by apply: nondecreasing_seqD => // x; [exact/(lef_at x nd_g1)|exact/(lef_at x nd_g2)]. @@ -1785,7 +1785,7 @@ pose Af x : set R := A `&` f @^-1` [set x]. have mAf x : measurable (Af x) by exact: measurableI. have finAf x : mu (Af x) < +oo. by rewrite (le_lt_trans _ finA)// le_measure// ?inE//; exact: subIsetl. -have eNpos : (0 < eps%:num/N.+1%:R)%R by []. +have eNpos : (0 < eps%:num / N.+1%:R)%R by []. have dK' x := lebesgue_regularity_inner (mAf x) (finAf x) eNpos. pose dK x : set R := projT1 (cid (dK' x)); pose J i : set R := Af i `\` dK i. have dkP x := projT2 (cid (dK' x)). @@ -3792,7 +3792,8 @@ have if_0 n : \int[mu]_(x in D) `|f_ n x| = 0. by apply: measurable_mine => //; exact: measurableT_comp. exact: f_bounded. rewrite (_ : (fun _ => _) = cst 0) // ?lim_cst// funeqE => n. -by rewrite -(if_0 n); apply: eq_integral => x _; rewrite gee0_abs// /f_. +rewrite -(if_0 n); apply: eq_integral => x _; rewrite gee0_abs// /f_. +exact/ge0e/R. Unshelve. all: by end_near. Qed. Lemma integral_abs_eq0 D (N : set T) (f : T -> \bar R) : @@ -5122,7 +5123,7 @@ have [] // := @dominated_convergence _ _ _ mu _ mE (fun n => EFin \o g_ n) f f. move=> _ /= fg0 gfcvg; exists g_; split. - move=> n; apply: (le_integrable mE _ _ intf). exact/measurable_EFinP/measurable_funTS. - move=> ? ?; rewrite /g_ !gee0_abs ?lee_fin//; last exact: fpos. + move=> ? ?; rewrite /g_ !gee0_abs ?lee_fin ?fpos//. by rewrite /= nnsfun_approxE le_approx. - exact: cvg_nnsfun_approx. - by apply: cvg_trans fg0; under eq_fun => ? do under eq_fun => t do @@ -5451,11 +5452,11 @@ transitivity (\sum_(k \in range f) rewrite indic_fubini_tonelli1// -ge0_integralZl//; last by rewrite lee_fin. - exact: indic_measurable_fun_fubini_tonelli_F. - by move=> /= x _; exact: indic_fubini_tonelli_F_ge0. -rewrite -ge0_integral_fsum //; last 2 first. +rewrite -ge0_integral_fsum => [|//|||//]; last 2 first. - by move=> r; apply/measurable_funeM/indic_measurable_fun_fubini_tonelli_F. - move=> r x _; rewrite /fubini_F. have [r0|r0] := leP 0%R r. - by rewrite mule_ge0//; exact: indic_fubini_tonelli_F_ge0. + by rewrite mule_ge0 ?indic_fubini_tonelli_F_ge0. rewrite integral0_eq ?mule0// => y _. by rewrite preimage_nnfun0//= indicE in_set0. apply: eq_integral => x _; rewrite sfun_fubini_tonelli_FE. @@ -5478,11 +5479,11 @@ transitivity (\sum_(k \in range f) rewrite indic_fubini_tonelli2// -ge0_integralZl//; last by rewrite lee_fin. - exact: indic_measurable_fun_fubini_tonelli_G. - by move=> /= x _; exact: indic_fubini_tonelli_G_ge0. -rewrite -ge0_integral_fsum //; last 2 first. +rewrite -ge0_integral_fsum => [|//|||//]; last 2 first. - by move=> r; apply/measurable_funeM/indic_measurable_fun_fubini_tonelli_G. - move=> r y _; rewrite /fubini_G. have [r0|r0] := leP 0%R r. - by rewrite mule_ge0//; exact: indic_fubini_tonelli_G_ge0. + by rewrite mule_ge0 ?indic_fubini_tonelli_G_ge0. rewrite integral0_eq ?mule0// => x _. by rewrite preimage_nnfun0//= indicE in_set0. apply: eq_integral => x _; rewrite sfun_fubini_tonelli_GE. @@ -5562,7 +5563,7 @@ rewrite [LHS](_ : _ = set r := fun _ => _; set l := fun _ => _; have -> // : l = r. by apply/funext => n; rewrite /l /r sfun_fubini_tonelli1. rewrite [RHS](_ : _ = limn (fun n => \int[m1]_x F_ g n x))//. -rewrite -monotone_convergence //; first exact: eq_integral. +rewrite -monotone_convergence => [|//|||]; first exact: eq_integral. - by move=> n; exact: sfun_measurable_fun_fubini_tonelli_F. - move=> n x _; apply: integral_ge0 => // y _ /=; rewrite lee_fin. exact: fun_ge0. @@ -5596,7 +5597,7 @@ rewrite [LHS](_ : _ = limn set r := fun _ => _; set l := fun _ => _; have -> // : l = r. by apply/funext => n; rewrite /l /r sfun_fubini_tonelli sfun_fubini_tonelli2. rewrite [RHS](_ : _ = limn (fun n => \int[m2]_y G_ g n y))//. -rewrite -monotone_convergence //; first exact: eq_integral. +rewrite -monotone_convergence => [|//|||]; first exact: eq_integral. - by move=> n; exact: sfun_measurable_fun_fubini_tonelli_G. - by move=> n y _; apply: integral_ge0 => // x _ /=; rewrite lee_fin fun_ge0. - move=> y /= _ a b ab; apply: ge0_le_integral => //. @@ -5730,7 +5731,7 @@ Qed. Let integrable_Fminus : m1.-integrable setT Fminus. Proof. apply/integrableP; split=> //. -apply: le_lt_trans (fubini1a.1 imf); apply: ge0_le_integral => //. +apply: le_lt_trans (fubini1a.1 imf); apply: ge0_le_integral => [//|//|||//|]. - exact: measurableT_comp. - by move=> *; exact: integral_ge0. - move=> x _; apply: le_trans. @@ -5848,18 +5849,18 @@ transitivity (\sum_(n n _; apply: eq_integral => x _. by rewrite ge0_integral_measure_series//; exact/measurableT_comp. transitivity (\sum_(n n _; rewrite integral_nneseries//. + apply: eq_eseriesr => n _; rewrite integral_nneseries => [//|//||]. by move=> m; exact: measurable_fun_fubini_tonelli_F. by move=> m x _; exact: integral_ge0. transitivity (\sum_(n n _; apply: eq_eseriesr => m _. by rewrite fubini_tonelli//; exact: finite_measure_sigma_finite. transitivity (\sum_(n n _; rewrite ge0_integral_measure_series//. + apply: eq_eseriesr => n _; rewrite ge0_integral_measure_series => [//|//||]. by move=> y _; exact: integral_ge0. exact: measurable_fun_fubini_tonelli_G. transitivity (\int[mseries s2 0]_y \sum_(n [//|//||]. by move=> n; apply: measurable_fun_fubini_tonelli_G. by move=> n y _; exact: integral_ge0. transitivity (\int[mseries s2 0]_y \int[mseries s1 0]_x f (x, y)). @@ -6125,7 +6126,7 @@ Proof. move=> Df x; apply: ereal_sup_le => //=. pose k := \int[mu]_(x in D `&` ball x 1) `|f x|%:E. exists ((fine (mu (ball x 1)))^-1%:E * k); last first. - rewrite mule_ge0//; last exact: integral_ge0. + rewrite mule_ge0 ?integral_ge0//. by rewrite lee_fin// invr_ge0// fine_ge0. exists 1%R; first by rewrite in_itv/= ltr01. rewrite iavg_restrict//; last exact: measurable_ball. @@ -6190,7 +6191,7 @@ move: a0; rewrite le_eqVlt => /predU1P[a0|a0]. have ka_pos : fine k / a \is Num.pos. by rewrite posrE divr_gt0// fine_gt0 // k_gt0/= locally_integrable_ltbally. have k_fin_num : k \is a fin_num. - by rewrite ge0_fin_numE ?locally_integrable_ltbally// integral_ge0. + by rewrite ge0_fin_numE ?locally_integrable_ltbally ?integral_ge0. have kar : (0 < 2^-1 * (fine k / a) - r)%R. move: afxr; rewrite -{1}(fineK k_fin_num) -lte_pdivrMr; last first. by rewrite fine_gt0// k_gt0/= ltey_eq k_fin_num. @@ -6292,7 +6293,7 @@ apply: (@le_trans _ _ (\sum_(i <- E) c^-1%:E * \int[mu]_(y in B i) `|(f y)|%:E)). rewrite [in leLHS]big_seq [in leRHS]big_seq; apply: lee_sum => r /ED /Dsub /[!inE] rD. by rewrite -lee_pdivrMl ?invr_gt0// invrK /B/=; exact/ltW/cMfx_int. -rewrite -ge0_sume_distrr//; last by move=> x _; rewrite integral_ge0. +rewrite -ge0_sume_distrr; last by move=> x _; rewrite integral_ge0. rewrite lee_wpmul2l//; first by rewrite lee_fin invr_ge0 ltW. rewrite -ge0_integral_bigsetU//=. - apply: ge0_subset_integral => //. diff --git a/theories/lebesgue_measure.v b/theories/lebesgue_measure.v index 5fbc202ca..56cc49a89 100644 --- a/theories/lebesgue_measure.v +++ b/theories/lebesgue_measure.v @@ -2,7 +2,7 @@ From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint interval. From mathcomp Require Import finmap fingroup perm rat archimedean. From mathcomp Require Import mathcomp_extra boolp classical_sets functions. -From mathcomp Require Import cardinality fsbigop reals ereal signed. +From mathcomp Require Import cardinality fsbigop reals itv ereal. From mathcomp Require Import topology numfun tvs normedtype function_spaces. From HB Require Import structures. From mathcomp Require Import sequences esum measure real_interval realfun exp. @@ -1693,7 +1693,8 @@ apply/uniform_restrict_cvg => /= U /=; rewrite !uniform_nbhsT. case/nbhs_ex => del /= ballU; apply: filterS; first by move=> ?; exact: ballU. have [N _ /(_ N)/(_ (leqnn _)) Ndel] := near_infty_natSinv_lt del. exists (badn N) => // r badNr x. -rewrite /patch; case: ifPn => // /set_mem xAB; apply: (lt_trans _ Ndel). +rewrite /patch; case: ifPn; last by move=> ?; apply: ballxx. +move=> /[!inE] xAB; apply: (lt_trans _ Ndel). move: xAB; rewrite setDE => -[Ax]; rewrite setC_bigcup => /(_ N I). rewrite /E setC_bigcup => /(_ r) /=; rewrite /h => /(_ badNr) /not_andP[]//. by move/negP; rewrite ltNge // distrC. @@ -2493,7 +2494,7 @@ have [|Aoo e0] := leP +oo (l^* A)%mu. by exists [set: R]; split => //; [exact: openT|rewrite Aoo leey]. have [F AF Fe] : exists2 I_, open_itv_cover A I_ & \sum_(0 <= k /lb_ereal_inf_adherent-/(_ _ e0)[_/= [F]] AF <- Fe. by exists F => //; exact/ltW. diff --git a/theories/lebesgue_stieltjes_measure.v b/theories/lebesgue_stieltjes_measure.v index 9e05ac8e7..f3fb9106d 100644 --- a/theories/lebesgue_stieltjes_measure.v +++ b/theories/lebesgue_stieltjes_measure.v @@ -4,7 +4,7 @@ From mathcomp Require Import finmap fingroup perm rat archimedean. From HB Require Import structures. From mathcomp.classical Require Import mathcomp_extra boolp classical_sets. From mathcomp.classical Require Import functions fsbigop cardinality. -From mathcomp Require Import reals ereal signed topology numfun normedtype. +From mathcomp Require Import reals ereal itv topology numfun normedtype. From mathcomp Require Import sequences esum real_interval measure realfun. (**md**************************************************************************) diff --git a/theories/measure.v b/theories/measure.v index 6cfd34f05..fd92ca66b 100644 --- a/theories/measure.v +++ b/theories/measure.v @@ -1,7 +1,7 @@ (* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C. *) From mathcomp Require Import all_ssreflect all_algebra archimedean finmap. From mathcomp Require Import mathcomp_extra boolp classical_sets functions. -From mathcomp Require Import cardinality fsbigop reals ereal signed. +From mathcomp Require Import cardinality fsbigop reals itv ereal. From mathcomp Require Import topology normedtype sequences esum numfun. From HB Require Import structures. @@ -1967,10 +1967,16 @@ Context d (T : semiRingOfSetsType d) (R : numFieldType). Variable mu : {content set T -> \bar R}. -Lemma content_snum_subproof S : Signed.spec 0 ?=0 >=0 (mu S). -Proof. exact: measure_ge0. Qed. +Lemma content_inum_subproof S : + Itv.spec (@ext_num_sem R) (Itv.Real `[0%Z, +oo[) (mu S). +Proof. +apply/and3P; split. +- by rewrite real_fine -real_leNye; apply: le_trans (measure_ge0 _ _). +- by rewrite /= bnd_simp measure_ge0. +- by rewrite bnd_simp. +Qed. -Canonical content_snum S := Signed.mk (content_snum_subproof S). +Canonical content_inum S := Itv.mk (content_inum_subproof S). End content_signed. @@ -2121,10 +2127,16 @@ Context d (R : numFieldType) (T : semiRingOfSetsType d). Variable mu : {measure set T -> \bar R}. -Lemma measure_snum_subproof S : Signed.spec 0 ?=0 >=0 (mu S). -Proof. exact: measure_ge0. Qed. +Lemma measure_inum_subproof S : + Itv.spec (@ext_num_sem R) (Itv.Real `[0%Z, +oo[) (mu S). +Proof. +apply/and3P; split. +- by rewrite real_fine -real_leNye; apply: le_trans (measure_ge0 _ _). +- by rewrite /= bnd_simp measure_ge0. +- by rewrite bnd_simp. +Qed. -Canonical measure_snum S := Signed.mk (measure_snum_subproof S). +Canonical measure_inum S := Itv.mk (measure_inum_subproof S). End measure_signed. @@ -3563,7 +3575,7 @@ by rewrite /mnormalize; case: ifPn => // _; rewrite measure0 mul0e. Qed. Let mnormalize_ge0 U : 0 <= mnormalize U. -Proof. by rewrite /mnormalize; case: ifPn => //; case: ifPn. Qed. +Proof. by rewrite /mnormalize; case: ifPn. Qed. Let mnormalize_sigma_additive : semi_sigma_additive mnormalize. Proof. diff --git a/theories/normedtype.v b/theories/normedtype.v index bf18d7bcd..b47d8d0f7 100644 --- a/theories/normedtype.v +++ b/theories/normedtype.v @@ -5,10 +5,9 @@ From mathcomp Require Import rat interval zmodp vector fieldext falgebra. From mathcomp Require Import boolp classical_sets functions. From mathcomp Require Import archimedean. From mathcomp Require Import cardinality set_interval ereal reals. -From mathcomp Require Import signed topology prodnormedzmodule function_spaces. +From mathcomp Require Import itv topology prodnormedzmodule function_spaces. From mathcomp Require Export real_interval separation_axioms tvs. - (**md**************************************************************************) (* # Norm-related Notions *) (* *) @@ -2341,7 +2340,7 @@ rewrite /normr /ball_ predeq3E => x e y /=; rewrite mx_normE; split => xey. by rewrite -num_lt /=; split => // -[? ?] _; rewrite !mxE; exact: xey. - have e_gt0 : 0 < e by rewrite (le_lt_trans _ xey). move: e_gt0 (e_gt0) xey => /ltW/nonnegP[{}e] e_gt0. - move=> /(bigmax_ltP _ _ _ (fun _ => _%:sgn)) /= [e0 xey] i j. + move=> /(bigmax_ltP _ _ _ (fun _ => _%:itv)) /= [e0 xey] i j. by move: (xey (i, j)); rewrite !mxE; exact. Qed. @@ -3311,7 +3310,8 @@ rewrite ball_close; split=> [bxy|edist0 eps]; first last. by apply: (@edist_lt_ball _ (x, y)); rewrite edist0. case: ltgtP (edist_ge0 (x, y)) => // dpos _. have xxfin : edist (x, y) \is a fin_num. - by rewrite ge0_fin_numE// (@le_lt_trans _ _ 1%:E) ?ltey// edist_fin. + rewrite ge0_fin_numE// (@le_lt_trans _ _ 1%:E) ?ltey// edist_fin//. + exact: bxy (widen_itv 1%:itv). have dpose : fine (edist (x, y)) > 0 by rewrite -lte_fin fineK. pose eps := PosNum dpose. have : (edist (x, y) <= (eps%:num / 2)%:E)%E. @@ -5330,7 +5330,7 @@ Proof. split=> [/nbhs_ballP[_/posnumP[r] xrB]|[e xeB]]; last first. apply/nbhs_ballP; exists e%:num => //=. exact: (subset_trans (@subset_closure _ _) xeB). -exists (r%:num / 2)%:sgn. +exists (r%:num / 2)%:itv. apply: (subset_trans (closed_ball_subset _ _) xrB) => //=. by rewrite lter_pdivrMr // ltr_pMr // ltr1n. Qed. diff --git a/theories/numfun.v b/theories/numfun.v index f3361cce0..4be9731cc 100644 --- a/theories/numfun.v +++ b/theories/numfun.v @@ -2,7 +2,7 @@ From HB Require Import structures. From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint interval finmap. From mathcomp Require Import mathcomp_extra boolp classical_sets fsbigop. -From mathcomp Require Import functions cardinality set_interval signed reals. +From mathcomp Require Import functions cardinality set_interval itv reals. From mathcomp Require Import ereal topology normedtype sequences. From mathcomp Require Import function_spaces. diff --git a/theories/probability.v b/theories/probability.v index c57cac324..3805178f0 100644 --- a/theories/probability.v +++ b/theories/probability.v @@ -5,7 +5,7 @@ From mathcomp Require Import mathcomp_extra boolp classical_sets functions. From mathcomp Require Import cardinality fsbigop. From HB Require Import structures. From mathcomp Require Import exp numfun lebesgue_measure lebesgue_integral. -From mathcomp Require Import reals ereal signed topology normedtype sequences. +From mathcomp Require Import reals itv ereal topology normedtype sequences. From mathcomp Require Import esum measure exp numfun lebesgue_measure. From mathcomp Require Import lebesgue_integral kernel. @@ -924,7 +924,7 @@ Context {R : realType}. Variables (p : R) (p0 : (0 <= p)%R) (p1 : ((NngNum p0)%:num <= 1)%R). Lemma bernoulli_dirac : bernoulli p = measure_add - (mscale (NngNum p0) \d_true) (mscale (onem_nonneg p1) \d_false). + (mscale (NngNum p0) \d_true) (mscale (1 - (Itv01 p0 p1)%:num)%:nng \d_false). Proof. apply/funext => U; rewrite /bernoulli; case: ifPn => [p01|]; last first. by rewrite p0/= p1. diff --git a/theories/realfun.v b/theories/realfun.v index b11415d1c..de0b66aff 100644 --- a/theories/realfun.v +++ b/theories/realfun.v @@ -4,7 +4,7 @@ From mathcomp Require Import all_ssreflect ssralg ssrint ssrnum archimedean. From mathcomp Require Import matrix interval zmodp vector fieldext falgebra. From mathcomp Require Import finmap. From mathcomp Require Import mathcomp_extra boolp classical_sets functions. -From mathcomp Require Import cardinality ereal reals signed. +From mathcomp Require Import cardinality ereal reals itv. From mathcomp Require Import topology prodnormedzmodule tvs normedtype derive. From mathcomp Require Import sequences real_interval. diff --git a/theories/separation_axioms.v b/theories/separation_axioms.v index 89a01e9d6..b2084deea 100644 --- a/theories/separation_axioms.v +++ b/theories/separation_axioms.v @@ -4,7 +4,7 @@ From mathcomp Require Import all_ssreflect all_algebra finmap generic_quotient. From mathcomp Require Import archimedean. From mathcomp Require Import boolp classical_sets functions wochoice. From mathcomp Require Import cardinality mathcomp_extra fsbigop set_interval. -From mathcomp Require Import filter reals signed topology. +From mathcomp Require Import filter reals itv topology. (**md**************************************************************************) (* # Separation Axioms *) diff --git a/theories/sequences.v b/theories/sequences.v index a3017a06d..2085b1e55 100644 --- a/theories/sequences.v +++ b/theories/sequences.v @@ -3,7 +3,7 @@ From HB Require Import structures. From mathcomp Require Import all_ssreflect ssralg ssrint ssrnum matrix. From mathcomp Require Import interval rat archimedean. From mathcomp Require Import mathcomp_extra boolp classical_sets functions. -From mathcomp Require Import set_interval reals ereal signed topology. +From mathcomp Require Import set_interval reals itv ereal topology. From mathcomp Require Import tvs normedtype landau. (**md**************************************************************************) @@ -892,7 +892,7 @@ suff abel : forall n, rewrite a_o. set h := 'o_\oo (@harmonic R). apply/eqoP => _/posnumP[e] /=. - near=> n; rewrite normr1 mulr1 normrM -ler_pdivlMl// ?normr_gt0//. + near=> n; rewrite normr1 mulr1 normrM -ler_pdivlMl ?normr_gt0//. rewrite mulrC -normrV ?unitfE //. near: n. by case: (eqoP eventually_filterType (@harmonic R) h) => Hh _; apply Hh. @@ -2855,8 +2855,9 @@ have /le_trans -> // : `| y n - y (n + m)| <= rewrite (le_trans (ler_distD (y (n + m)%N) _ _))//. apply: (le_trans (lerD ih _)); first by rewrite distrC addnS; exact: f1. rewrite [_ * `|_|]mulrC exprD mulrA geometric_seriesE ?lt_eqF//=. - rewrite -!/(`1-_) (onem_PosNum ctrf.1) (onemX_NngNum (ltW ctrf.1)). - rewrite -!mulrA -mulrDr ler_pM// -mulrDr exprSr onemM -addrA. + pose q' := Itv01 (!! ge0 q) (ltW q1). + rewrite -[q%:num]/(q'%:num) -!mulrA -mulrDr ler_pM// {}/q'/=. + rewrite -!/(`1-_) -mulrDr exprSr onemM -addrA. rewrite -[in leRHS](mulrC _ `1-(_ ^+ m)) -onemMr onemK. by rewrite [in leRHS]mulrDl mulrAC mulrV ?mul1r// unitf_gt0// onem_gt0. rewrite geometric_seriesE ?lt_eqF//= -[leRHS]mulr1 (ACl (1*4*2*3))/= -/C. @@ -2951,7 +2952,7 @@ have Ar : forall na : nat * (U * {posnum K}), exists b : U * {posnum K}, have /open_nbhs_nbhs/nbhs_closedballP[rn01 Ball_an1] : open_nbhs an1 ((closed_ball an rn%:num)^° `&` F n.+1) by []. have n31_gt0 : n.+3%:R^-1 > 0 :> K by []. - have majr : minr (PosNum n31_gt0)%:num rn01%:num > 0 by []. + have majr : minr (PosNum n31_gt0)%:num rn01%:num > 0 by exact/gt0/K. exists (an1, PosNum majr); split. apply/(subset_trans _ Ball_an1)/le_closed_ball => /=. by rewrite ge_min lexx orbT. diff --git a/theories/topology_theory/compact.v b/theories/topology_theory/compact.v index f0187e8a1..321dd2a07 100644 --- a/theories/topology_theory/compact.v +++ b/theories/topology_theory/compact.v @@ -1,7 +1,7 @@ (* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C. *) From HB Require Import structures. From mathcomp Require Import all_ssreflect all_algebra finmap all_classical. -From mathcomp Require Import signed reals topology_structure uniform_structure. +From mathcomp Require Import itv reals topology_structure uniform_structure. From mathcomp Require Import pseudometric_structure. (**md**************************************************************************) diff --git a/theories/topology_theory/matrix_topology.v b/theories/topology_theory/matrix_topology.v index 7610383a1..09e67f1b2 100644 --- a/theories/topology_theory/matrix_topology.v +++ b/theories/topology_theory/matrix_topology.v @@ -1,7 +1,7 @@ (* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C. *) From HB Require Import structures. From mathcomp Require Import all_ssreflect all_algebra finmap all_classical. -From mathcomp Require Import signed topology_structure uniform_structure. +From mathcomp Require Import itv topology_structure uniform_structure. From mathcomp Require Import pseudometric_structure. (**md**************************************************************************) (* # Matrix topology *) diff --git a/theories/topology_theory/num_topology.v b/theories/topology_theory/num_topology.v index ea87ef618..5685a0dc0 100644 --- a/theories/topology_theory/num_topology.v +++ b/theories/topology_theory/num_topology.v @@ -2,7 +2,7 @@ From HB Require Import structures. From mathcomp Require Import all_ssreflect all_algebra archimedean. From mathcomp Require Import all_classical. -From mathcomp Require Import signed reals topology_structure uniform_structure. +From mathcomp Require Import itv reals topology_structure uniform_structure. From mathcomp Require Import pseudometric_structure order_topology. (**md**************************************************************************) diff --git a/theories/topology_theory/product_topology.v b/theories/topology_theory/product_topology.v index 4755458fc..08e77020b 100644 --- a/theories/topology_theory/product_topology.v +++ b/theories/topology_theory/product_topology.v @@ -1,7 +1,7 @@ (* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C. *) From HB Require Import structures. From mathcomp Require Import all_ssreflect all_algebra all_classical. -From mathcomp Require Import signed topology_structure uniform_structure. +From mathcomp Require Import itv topology_structure uniform_structure. From mathcomp Require Import pseudometric_structure compact. (**md**************************************************************************) diff --git a/theories/topology_theory/pseudometric_structure.v b/theories/topology_theory/pseudometric_structure.v index ec133325f..fd98cbf4a 100644 --- a/theories/topology_theory/pseudometric_structure.v +++ b/theories/topology_theory/pseudometric_structure.v @@ -2,7 +2,7 @@ From HB Require Import structures. From mathcomp Require Import all_ssreflect all_algebra archimedean. From mathcomp Require Import all_classical. -From mathcomp Require Import signed reals topology_structure uniform_structure. +From mathcomp Require Import itv reals topology_structure uniform_structure. (**md**************************************************************************) (* # PseudoMetric Spaces *) diff --git a/theories/topology_theory/weak_topology.v b/theories/topology_theory/weak_topology.v index 0b13ca98d..290970716 100644 --- a/theories/topology_theory/weak_topology.v +++ b/theories/topology_theory/weak_topology.v @@ -1,7 +1,7 @@ (* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C. *) From HB Require Import structures. From mathcomp Require Import all_ssreflect all_algebra all_classical. -From mathcomp Require Import signed reals topology_structure uniform_structure. +From mathcomp Require Import itv reals topology_structure uniform_structure. From mathcomp Require Import order_topology pseudometric_structure. (**md**************************************************************************) diff --git a/theories/trigo.v b/theories/trigo.v index 90a2d0435..7474e66b9 100644 --- a/theories/trigo.v +++ b/theories/trigo.v @@ -3,7 +3,7 @@ From HB Require Import structures. From mathcomp Require Import all_ssreflect ssralg ssrint ssrnum matrix. From mathcomp Require Import interval rat. From mathcomp Require Import mathcomp_extra boolp classical_sets functions. -From mathcomp Require Import reals ereal nsatz_realtype signed topology. +From mathcomp Require Import reals ereal nsatz_realtype itv topology. From mathcomp Require Import normedtype landau sequences derive realfun exp. (**md**************************************************************************) diff --git a/theories/tvs.v b/theories/tvs.v index cb5c93eaf..98bc52663 100644 --- a/theories/tvs.v +++ b/theories/tvs.v @@ -4,7 +4,7 @@ From mathcomp Require Import all_ssreflect ssralg ssrint ssrnum finmap matrix. From mathcomp Require Import rat interval zmodp vector fieldext falgebra. From mathcomp Require Import archimedean. From mathcomp Require Import boolp classical_sets functions cardinality. -From mathcomp Require Import set_interval ereal reals signed topology. +From mathcomp Require Import set_interval ereal reals itv topology. From mathcomp Require Import prodnormedzmodule function_spaces. From mathcomp Require Import separation_axioms.