From 171af4cc0f066a9ac129f6d7132f61799ce5380b Mon Sep 17 00:00:00 2001 From: Yosuke Tsuji Date: Wed, 23 Apr 2025 12:04:13 +0900 Subject: [PATCH 01/45] sorgenfreyline and properties --- theories/showcase/sorgenfreyline.v | 263 +++++++++++++++++++++++++++++ 1 file changed, 263 insertions(+) create mode 100644 theories/showcase/sorgenfreyline.v diff --git a/theories/showcase/sorgenfreyline.v b/theories/showcase/sorgenfreyline.v new file mode 100644 index 000000000..095e87da1 --- /dev/null +++ b/theories/showcase/sorgenfreyline.v @@ -0,0 +1,263 @@ +From HB Require Import structures. +From mathcomp Require Import all_ssreflect all_algebra all_fingroup. +From mathcomp Require Import wochoice contra. +From mathcomp Require Import boolp classical_sets set_interval. +From mathcomp Require Import topology_structure separation_axioms connected. +From mathcomp Require Import reals. + +Set Implicit Arguments. +Unset Strict Implicit. +Unset Printing Implicit Defensive. + +Import GRing.Theory Num.Theory Order.Theory. +Local Open Scope ring_scope. +Import boolp. + +Import classical_sets. +Local Open Scope classical_set_scope. + +Section general_topology. +Context {T : topologicalType}. + +Section extra. + +(* TODO: better name? *) +Lemma nbhs_cobind (x y : T) : + (forall A, nbhs x A -> A y) -> forall A, nbhs x A -> nbhs y A. +Proof. +move=> + A /[1!(nbhsE x)] -[] U oU UA => /(_ U (open_nbhs_nbhs oU)) Uy. +by rewrite nbhsE; exists U=> //; split; case: oU. +Qed. + +Lemma all_and2P (P Q : T -> Prop): + (forall A, P A /\ Q A) <-> ((forall A, P A) /\ (forall A, Q A)). +Proof. by firstorder. Qed. + +Lemma all_and2E (P Q : T -> Prop): + (forall A, P A /\ Q A) = ((forall A, P A) /\ (forall A, Q A)). +Proof. exact/propeqP/all_and2P. Qed. + +End extra. + +Lemma kolmogorov_inj_nbhsP : kolmogorov_space T <-> injective (@nbhs _ T). +Proof. +split => i x y. + apply: contraPP => /eqP /i [] X [] [] /[swap] h1 /[swap] xy; + by rewrite inE in h1; rewrite (xy, esym xy) inE => /nbhs_singleton /h1. +apply: contraNP => /asboolPn /forallp_asboolPn H. +apply/eqP/i/predeqP => A. +wlog: x y H / nbhs x A. + split => ?; first by rewrite -(H0 x). + by rewrite -(H0 y) => // B; rewrite boolp.orC. +split=> //. +rewrite nbhsE => -[] B /[dup] /open_nbhs_nbhs nbhsB [] opB Bx BA. +move: (H B); rewrite not_orE !inE !not_andE -!implyE !notK. +by case => /(_ nbhsB) By _; apply/(filterS BA) /open_nbhs_nbhs. +Qed. + +End general_topology. + +Section Sorgenfrey_line. +Variable R : realType. + +Let I := (R^o * R^o)%type. +Let D := [set : I]. +Let b (d : I) := `[ d.1, d.2 [%classic. +Let b_cover : \bigcup_(i in D) b i = setT. +Proof. +apply/seteqP; split => // x _ . +exists (x, x+1)%R => //=. +by rewrite /b /= in_itv /= lexx /= ltrDl. +Qed. +Let b_join i j t : D i -> D j -> b i t -> b j t -> + exists k, [/\ D k, b k t & b k `<=` b i `&` b j]. +Proof. +move=> Di Dj bit bjt. +exists (Order.max i.1 j.1, Order.min i.2 j.2)%R. +rewrite /D /=. +rewrite /b /= in_itv. +split; trivial. + rewrite /=. + rewrite comparable_ge_max; last first. + rewrite /Order.comparable. + apply:real_leVge; apply:num_real; apply:num_real. + rewrite comparable_lt_min; last first. + apply:real_leVge; apply:num_real; apply:num_real. + (*rewrite Bool.andb_assoc.*) + have:( t \in `[ i.1, i.2 [%R ). + by rewrite in_itv /=; apply bit. + have:( t \in `[ j.1, j.2 [%R ). + by rewrite in_itv /=; apply bjt. + Check(t \in `[j.1, j.2[%R). + rewrite !in_itv /=. + case/andP => -> ->. + by case/andP => -> ->. +rewrite /=. +move=> x. +rewrite /= !in_itv /=. +rewrite comparable_ge_max; last first. + apply:real_leVge; apply:num_real; apply:num_real. +case/andP => /andP [] -> ->. +rewrite comparable_lt_min; last first. + apply:real_leVge; apply:num_real; apply:num_real. +by case/andP => -> ->. +Qed. + + +Fail Check R:topologicalType. +Fail Check R^o : topologicalType. +HB.about GRing.regular. +(* prove I is pointed *) +#[export, non_forgetful_inheritance] +HB.instance Definition _ := @isPointed.Build R 0. +HB.instance Definition Sorgenfrey_mixin := @isBaseTopological.Build R I D b b_cover b_join. +Definition sorgenfrey := HB.pack_for topologicalType _ Sorgenfrey_mixin. +Check sorgenfrey : topologicalType. + +Lemma open_separated (T : topologicalType) (A B : set T) : + open A -> open B -> (A `&` B = set0 -> separated A B). +Proof. +move=> oA oB. +apply:contraPP. +rewrite /separated. +rewrite not_andP. +case. + contra. + rewrite disjoints_subset => AsubnB. + rewrite disjoints_subset. + move:(closure_subset AsubnB). + have:closed (~` B). + by apply:open_closedC. + move/closure_id => csB. + by rewrite -csB. +contra. +rewrite setIC. +rewrite disjoints_subset => BsubnA. +rewrite setIC disjoints_subset. +move:(closure_subset BsubnA). +have:closed (~` A). + by apply:open_closedC. +move/closure_id => csA. +by rewrite -csA. +Qed. + +Lemma separated_sub (T : topologicalType)(A B C : set T) : + separated A B -> C `<=` B -> separated A C. +Proof. +rewrite /separated. +case. +move=> cAB0 AcB0. +move=> CB. +split. + rewrite setIC disjoints_subset. + apply (subset_trans CB). + by rewrite -disjoints_subset setIC. +rewrite setIC disjoints_subset. +apply (subset_trans (closure_subset CB)). +by rewrite -disjoints_subset setIC. +Qed. + +Check sorgenfrey. + +Lemma sorgenfrey_line_totally_disconnected : totally_disconnected [set: sorgenfrey]. +Proof. +rewrite /totally_disconnected. +move=> x Rx. +(*rewrite /setT /set1.*) +rewrite /connected_component. +have:forall C : set sorgenfrey, C x -> connected C -> C = [set x]. + move=> C Cx. + apply:contraPP. + move=> Cneqsetx. + have[y [yx Cy]]:(exists y, y != x /\ C y). + apply/not_existsP. + move:Cneqsetx. + contra. + move=> H. + apply:funext. + move=> y. + move:(H y). + rewrite not_andE. + move=>Hy. + rewrite propeqP /=. + split. + case:Hy => //. + move/negP. + rewrite negbK. + by move/eqP. + by move->. + wlog xy : x y yx Cx Cy {Rx Cneqsetx} / x < y. + move:(yx). + rewrite neq_lt. + case/orP. + move=> ylx H. + apply:(H y x) => //. + by rewrite eq_sym. + move=> xly H. + by apply:(H x y) => //. + rewrite connectedPn. + exists (fun b => if b then C `&` `]-oo, y[ else C `&` `[ y, +oo[). + split. + - case. + exists x. + by split. + exists y. + split => //=. + by rewrite in_itv /= lexx. + - rewrite -setIUr. + move:(setCitv `[y, y[%R ). + rewrite /=. + rewrite setUC => <-. + by rewrite set_itvco0 setC0 setIT. + apply: (separated_sub (B := `]-oo, y[)); last by apply: subIsetr. + rewrite separatedC. + apply: (separated_sub (B := `[y, +oo[)); last by apply: subIsetr. + apply: open_separated. + - have -> : `]-oo, y[ = \bigcup_( z in `]-oo, y[ ) `[z, y[. + apply/seteqP. + split => w Hw /=. + exists w => //=. + move: Hw. + by rewrite /= !in_itv /= lexx => ->. + by case: Hw => t /= /[!in_itv] /= _ /andP []. + apply: bigcup_open => w ? /=. + rewrite /open /=. + exists [set (w, y)] => //. + by rewrite bigcup_set1. + - have -> : `[y, +oo[ = \bigcup_( z in `[y, +oo[ ) `[y, z[. + apply/seteqP. + split => w Hw /=. + exists (w+1) => //=. + move: Hw. + rewrite /= !in_itv /=. + rewrite andbC /= andbC /=. + by apply/(ler_wpDr ler01). + rewrite in_itv /=. + apply/andP. + split. + move:Hw. + by rewrite /= in_itv /= andbC. + apply:ltr_pwDr; last by []. + by apply: ltr01. + rewrite in_itv /= andbC /=. + by case: Hw => t /= /[!in_itv] /= _ /andP []. + apply: bigcup_open => w ? /=. + rewrite /open /=. + exists [set (y, w)] => //. + by rewrite bigcup_set1. + apply/seteqP. + split => w //=. + by rewrite !in_itv /= leNgt => -[] ->. +move=> H. +rewrite ( _ : [set C | _ ] = [set [set x]]). + by rewrite bigcup_set1. +apply/seteqP. +split => C //=. + case=>*. + exact: H. +move->. +split => //. +exact: connected1. +Qed. + +End Sorgenfrey_line. From fc5695528f6735881d46228296b655d2d0b4516c Mon Sep 17 00:00:00 2001 From: Yosuke Tsuji Date: Wed, 23 Apr 2025 12:50:43 +0900 Subject: [PATCH 02/45] make --- _CoqProject | 1 + theories/Make | 1 + 2 files changed, 2 insertions(+) diff --git a/_CoqProject b/_CoqProject index 47e426cfc..5dd4d0233 100644 --- a/_CoqProject +++ b/_CoqProject @@ -120,5 +120,6 @@ theories/kernel.v theories/pi_irrational.v theories/gauss_integral.v theories/showcase/summability.v +theories/showcase/sorgenfreyline.v analysis_stdlib/Rstruct_topology.v analysis_stdlib/showcase/uniform_bigO.v diff --git a/theories/Make b/theories/Make index 77ba62671..db9dea809 100644 --- a/theories/Make +++ b/theories/Make @@ -86,3 +86,4 @@ pi_irrational.v gauss_integral.v all_analysis.v showcase/summability.v +showcase/sorgenfreyline.v From 3825cc9da9f3be3593e29efc57b3b0db5c316bfa Mon Sep 17 00:00:00 2001 From: Yosuke Tsuji Date: Wed, 7 May 2025 09:37:35 +0900 Subject: [PATCH 03/45] add Definition perfectly_normal_space --- theories/topology_theory/separation_axioms.v | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/theories/topology_theory/separation_axioms.v b/theories/topology_theory/separation_axioms.v index 452143cdf..14c1172dd 100644 --- a/theories/topology_theory/separation_axioms.v +++ b/theories/topology_theory/separation_axioms.v @@ -1132,3 +1132,12 @@ by rewrite -(existT_inj2 lr). Qed. End sigT_separations. + +Section perfectlynormalspace. +Context (R : realType) (T : topologicalType). + +Definition perfectly_normal_space := + forall E F : set T, exists f : T -> R, + continuous f /\ E `<=` f @^-1` [set 0] /\ F `<=` f @^-1` [set 1]. + +End perfectlynormalspace. From cc5886fd3be3f01785aec5ba60f1a817732fae7e Mon Sep 17 00:00:00 2001 From: Yosuke Tsuji Date: Wed, 7 May 2025 12:09:18 +0900 Subject: [PATCH 04/45] add Definition sdist --- theories/showcase/sorgenfreyline.v | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/theories/showcase/sorgenfreyline.v b/theories/showcase/sorgenfreyline.v index 095e87da1..8be6ff24b 100644 --- a/theories/showcase/sorgenfreyline.v +++ b/theories/showcase/sorgenfreyline.v @@ -260,4 +260,11 @@ split => //. exact: connected1. Qed. + +Definition sdist (E : set sorgenfrey) (x : sorgenfrey) := + let xl := inf [set y | x - y \in E /\ 0 < y] in + let xr := inf [set y | x + y \in E /\ 0 <= y] in + if x - xl \in E then Order.min xl xr else Order.min 1 xr. + + End Sorgenfrey_line. From 0049b38ccdb606e716bb1437c09bdcb0f4735c02 Mon Sep 17 00:00:00 2001 From: Takafumi Saikawa Date: Sat, 10 May 2025 02:35:10 +0900 Subject: [PATCH 05/45] simplify b_join --- theories/showcase/sorgenfreyline.v | 46 +++++++----------------------- 1 file changed, 10 insertions(+), 36 deletions(-) diff --git a/theories/showcase/sorgenfreyline.v b/theories/showcase/sorgenfreyline.v index 8be6ff24b..644565f81 100644 --- a/theories/showcase/sorgenfreyline.v +++ b/theories/showcase/sorgenfreyline.v @@ -72,47 +72,21 @@ Qed. Let b_join i j t : D i -> D j -> b i t -> b j t -> exists k, [/\ D k, b k t & b k `<=` b i `&` b j]. Proof. -move=> Di Dj bit bjt. -exists (Order.max i.1 j.1, Order.min i.2 j.2)%R. -rewrite /D /=. -rewrite /b /= in_itv. -split; trivial. - rewrite /=. - rewrite comparable_ge_max; last first. - rewrite /Order.comparable. - apply:real_leVge; apply:num_real; apply:num_real. - rewrite comparable_lt_min; last first. - apply:real_leVge; apply:num_real; apply:num_real. - (*rewrite Bool.andb_assoc.*) - have:( t \in `[ i.1, i.2 [%R ). - by rewrite in_itv /=; apply bit. - have:( t \in `[ j.1, j.2 [%R ). - by rewrite in_itv /=; apply bjt. - Check(t \in `[j.1, j.2[%R). - rewrite !in_itv /=. - case/andP => -> ->. - by case/andP => -> ->. -rewrite /=. -move=> x. -rewrite /= !in_itv /=. -rewrite comparable_ge_max; last first. - apply:real_leVge; apply:num_real; apply:num_real. -case/andP => /andP [] -> ->. -rewrite comparable_lt_min; last first. - apply:real_leVge; apply:num_real; apply:num_real. -by case/andP => -> ->. +move=> _ _; case: i=> i1 i2; case: j=> j1 j2. +rewrite /b /= !in_itv /= => /andP [] i1t ti2 /andP [] j1t tj2. +exists (Order.max i1 j1, Order.min i2 j2). +rewrite /D /= in_itv /= subsetI. +case: (leP i1 j1) => ij1; case: (leP i2 j2) => ij2. +all: rewrite !(i1t, ti2, j1t, tj2)/=. +all: split=> //; split; apply: subset_itv. +all: by rewrite leBSide //= ltW. Qed. - -Fail Check R:topologicalType. -Fail Check R^o : topologicalType. -HB.about GRing.regular. -(* prove I is pointed *) -#[export, non_forgetful_inheritance] +#[non_forgetful_inheritance] HB.instance Definition _ := @isPointed.Build R 0. +#[non_forgetful_inheritance] HB.instance Definition Sorgenfrey_mixin := @isBaseTopological.Build R I D b b_cover b_join. Definition sorgenfrey := HB.pack_for topologicalType _ Sorgenfrey_mixin. -Check sorgenfrey : topologicalType. Lemma open_separated (T : topologicalType) (A B : set T) : open A -> open B -> (A `&` B = set0 -> separated A B). From 56ff7d6ecc5e23bcb37fb22f9a3317c49131af94 Mon Sep 17 00:00:00 2001 From: Takafumi Saikawa Date: Sat, 10 May 2025 19:35:57 +0900 Subject: [PATCH 06/45] simplify open_separatend and subset_separated --- theories/showcase/sorgenfreyline.v | 61 ++++++++++-------------------- 1 file changed, 21 insertions(+), 40 deletions(-) diff --git a/theories/showcase/sorgenfreyline.v b/theories/showcase/sorgenfreyline.v index 644565f81..748040c6a 100644 --- a/theories/showcase/sorgenfreyline.v +++ b/theories/showcase/sorgenfreyline.v @@ -88,52 +88,33 @@ HB.instance Definition _ := @isPointed.Build R 0. HB.instance Definition Sorgenfrey_mixin := @isBaseTopological.Build R I D b b_cover b_join. Definition sorgenfrey := HB.pack_for topologicalType _ Sorgenfrey_mixin. -Lemma open_separated (T : topologicalType) (A B : set T) : - open A -> open B -> (A `&` B = set0 -> separated A B). +Let open_half_separated (T : topologicalType) (A B : set T) : + open A -> open B -> A `&` B = set0 -> closure A `&` B = set0. Proof. move=> oA oB. -apply:contraPP. -rewrite /separated. -rewrite not_andP. -case. - contra. - rewrite disjoints_subset => AsubnB. - rewrite disjoints_subset. - move:(closure_subset AsubnB). - have:closed (~` B). - by apply:open_closedC. - move/closure_id => csB. - by rewrite -csB. -contra. -rewrite setIC. -rewrite disjoints_subset => BsubnA. -rewrite setIC disjoints_subset. -move:(closure_subset BsubnA). -have:closed (~` A). - by apply:open_closedC. -move/closure_id => csA. -by rewrite -csA. +rewrite disjoints_subset -subset0. +move=> /closure_subset; rewrite closure_setC. +move: oB=> /interior_id -> /(@setSI _ B). +by rewrite setICl. Qed. -Lemma separated_sub (T : topologicalType)(A B C : set T) : - separated A B -> C `<=` B -> separated A C. +Lemma open_separated (T : topologicalType) (A B : set T) : + open A -> open B -> A `&` B = set0 -> separated A B. Proof. -rewrite /separated. -case. -move=> cAB0 AcB0. -move=> CB. -split. - rewrite setIC disjoints_subset. - apply (subset_trans CB). - by rewrite -disjoints_subset setIC. -rewrite setIC disjoints_subset. -apply (subset_trans (closure_subset CB)). -by rewrite -disjoints_subset setIC. +move=> oA oB AB0; split; first exact: open_half_separated. +by rewrite setIC; apply: open_half_separated=> //; rewrite setIC. Qed. -Check sorgenfrey. +Lemma subset_separated (T : topologicalType) (A B C : set T) : + B `<=` C -> separated A C -> separated A B. +Proof. +move=> BC []; rewrite -!subset0. +have:= BC => /(@setIS _ (closure A)) /subset_trans /[apply] ?. +have:= closure_subset BC=> /(@setIS _ A) /subset_trans /[apply] ?. +by split; rewrite -!subset0. +Qed. -Lemma sorgenfrey_line_totally_disconnected : totally_disconnected [set: sorgenfrey]. +Lemma sorgenfrey_totally_disconnected : totally_disconnected [set: sorgenfrey]. Proof. rewrite /totally_disconnected. move=> x Rx. @@ -183,9 +164,9 @@ have:forall C : set sorgenfrey, C x -> connected C -> C = [set x]. rewrite /=. rewrite setUC => <-. by rewrite set_itvco0 setC0 setIT. - apply: (separated_sub (B := `]-oo, y[)); last by apply: subIsetr. + apply: (subset_separated (C := `]-oo, y[)); first exact: subIsetr. rewrite separatedC. - apply: (separated_sub (B := `[y, +oo[)); last by apply: subIsetr. + apply: (subset_separated (C := `[y, +oo[)); first exact: subIsetr. apply: open_separated. - have -> : `]-oo, y[ = \bigcup_( z in `]-oo, y[ ) `[z, y[. apply/seteqP. From 91fdb6df656c4a16bda9fa755a24740f73273fb6 Mon Sep 17 00:00:00 2001 From: Takafumi Saikawa Date: Sun, 11 May 2025 01:43:30 +0900 Subject: [PATCH 07/45] simplify sorgenfrey_totally_disconnected --- theories/showcase/sorgenfreyline.v | 199 +++++++++++------------------ 1 file changed, 76 insertions(+), 123 deletions(-) diff --git a/theories/showcase/sorgenfreyline.v b/theories/showcase/sorgenfreyline.v index 748040c6a..9ab2cb9ae 100644 --- a/theories/showcase/sorgenfreyline.v +++ b/theories/showcase/sorgenfreyline.v @@ -19,6 +19,54 @@ Local Open Scope classical_set_scope. Section general_topology. Context {T : topologicalType}. +Section connected_separated. +Let open_half_separated (A B : set T) : + open A -> open B -> A `&` B = set0 -> closure A `&` B = set0. +Proof. +move=> oA oB. +rewrite disjoints_subset -subset0. +move=> /closure_subset; rewrite closure_setC. +move: oB=> /interior_id -> /(@setSI _ B). +by rewrite setICl. +Qed. + +Lemma open_separated (A B : set T) : + open A -> open B -> A `&` B = set0 -> separated A B. +Proof. +move=> oA oB AB0; split; first exact: open_half_separated. +by rewrite setIC; apply: open_half_separated=> //; rewrite setIC. +Qed. + +Lemma subset_separated2l (A B C : set T) : + B `<=` C -> separated A C -> separated A B. +Proof. +move=> BC []; rewrite -!subset0. +have:= BC => /(@setIS _ (closure A)) /subset_trans /[apply] ?. +have:= closure_subset BC=> /(@setIS _ A) /subset_trans /[apply] ?. +by split; rewrite -!subset0. +Qed. + +Lemma subset_separated2r (A B C : set T) : + B `<=` C -> separated C A -> separated B A. +Proof. by rewrite !(separatedC _ A); exact: subset_separated2l. Qed. + +Lemma subset_separated (A B C D : set T) : + A `<=` B -> C `<=` D -> separated B D -> separated A C. +Proof. by move=> ? /subset_separated2l /[apply]; exact: subset_separated2r. Qed. + +Lemma connectedPn (A : set T) : + ~ connected A <-> + (exists E1 E2 : set T, + [/\ E1 !=set0, E2 !=set0, A = E1 `|` E2 & separated E1 E2]). +Proof. +split; first by move/connectedPn=> [] E [] *; exists (E false), (E true). +case=> E1 [] E2 [] *. +apply/connectedPn; exists (fun b=> if b then E2 else E1); split=> //. +by case. +Qed. + +End connected_separated. + Section extra. (* TODO: better name? *) @@ -88,131 +136,36 @@ HB.instance Definition _ := @isPointed.Build R 0. HB.instance Definition Sorgenfrey_mixin := @isBaseTopological.Build R I D b b_cover b_join. Definition sorgenfrey := HB.pack_for topologicalType _ Sorgenfrey_mixin. -Let open_half_separated (T : topologicalType) (A B : set T) : - open A -> open B -> A `&` B = set0 -> closure A `&` B = set0. -Proof. -move=> oA oB. -rewrite disjoints_subset -subset0. -move=> /closure_subset; rewrite closure_setC. -move: oB=> /interior_id -> /(@setSI _ B). -by rewrite setICl. -Qed. - -Lemma open_separated (T : topologicalType) (A B : set T) : - open A -> open B -> A `&` B = set0 -> separated A B. -Proof. -move=> oA oB AB0; split; first exact: open_half_separated. -by rewrite setIC; apply: open_half_separated=> //; rewrite setIC. -Qed. - -Lemma subset_separated (T : topologicalType) (A B C : set T) : - B `<=` C -> separated A C -> separated A B. -Proof. -move=> BC []; rewrite -!subset0. -have:= BC => /(@setIS _ (closure A)) /subset_trans /[apply] ?. -have:= closure_subset BC=> /(@setIS _ A) /subset_trans /[apply] ?. -by split; rewrite -!subset0. -Qed. - Lemma sorgenfrey_totally_disconnected : totally_disconnected [set: sorgenfrey]. Proof. -rewrite /totally_disconnected. -move=> x Rx. -(*rewrite /setT /set1.*) -rewrite /connected_component. -have:forall C : set sorgenfrey, C x -> connected C -> C = [set x]. - move=> C Cx. - apply:contraPP. - move=> Cneqsetx. - have[y [yx Cy]]:(exists y, y != x /\ C y). - apply/not_existsP. - move:Cneqsetx. - contra. - move=> H. - apply:funext. - move=> y. - move:(H y). - rewrite not_andE. - move=>Hy. - rewrite propeqP /=. - split. - case:Hy => //. - move/negP. - rewrite negbK. - by move/eqP. - by move->. - wlog xy : x y yx Cx Cy {Rx Cneqsetx} / x < y. - move:(yx). - rewrite neq_lt. - case/orP. - move=> ylx H. - apply:(H y x) => //. - by rewrite eq_sym. - move=> xly H. - by apply:(H x y) => //. - rewrite connectedPn. - exists (fun b => if b then C `&` `]-oo, y[ else C `&` `[ y, +oo[). - split. - - case. - exists x. - by split. - exists y. - split => //=. - by rewrite in_itv /= lexx. - - rewrite -setIUr. - move:(setCitv `[y, y[%R ). - rewrite /=. - rewrite setUC => <-. - by rewrite set_itvco0 setC0 setIT. - apply: (subset_separated (C := `]-oo, y[)); first exact: subIsetr. - rewrite separatedC. - apply: (subset_separated (C := `[y, +oo[)); first exact: subIsetr. - apply: open_separated. - - have -> : `]-oo, y[ = \bigcup_( z in `]-oo, y[ ) `[z, y[. - apply/seteqP. - split => w Hw /=. - exists w => //=. - move: Hw. - by rewrite /= !in_itv /= lexx => ->. - by case: Hw => t /= /[!in_itv] /= _ /andP []. - apply: bigcup_open => w ? /=. - rewrite /open /=. - exists [set (w, y)] => //. - by rewrite bigcup_set1. - - have -> : `[y, +oo[ = \bigcup_( z in `[y, +oo[ ) `[y, z[. - apply/seteqP. - split => w Hw /=. - exists (w+1) => //=. - move: Hw. - rewrite /= !in_itv /=. - rewrite andbC /= andbC /=. - by apply/(ler_wpDr ler01). - rewrite in_itv /=. - apply/andP. - split. - move:Hw. - by rewrite /= in_itv /= andbC. - apply:ltr_pwDr; last by []. - by apply: ltr01. - rewrite in_itv /= andbC /=. - by case: Hw => t /= /[!in_itv] /= _ /andP []. - apply: bigcup_open => w ? /=. - rewrite /open /=. - exists [set (y, w)] => //. - by rewrite bigcup_set1. - apply/seteqP. - split => w //=. - by rewrite !in_itv /= leNgt => -[] ->. -move=> H. -rewrite ( _ : [set C | _ ] = [set [set x]]). - by rewrite bigcup_set1. -apply/seteqP. -split => C //=. - case=>*. - exact: H. -move->. -split => //. -exact: connected1. +move=> x _. +apply/seteqP; split=> y //=; last by move->; apply: connected_component_refl. +case=> C [] Cx _ + Cy; apply: contraPP=> yx. +wlog xy : x y yx Cx Cy / x < y. + have/eqP:= yx; rewrite real_neqr_lt ?num_real// => /orP []. + by move/[swap]/[apply]/(_ (nesym yx)); exact. + by move/[swap]/[apply]; exact. +apply/connectedPn; exists (C `&` `]-oo, y[ ), (C `&` `[y, +oo[ ); split. +- by exists x. +- by exists y; split=> //=; rewrite in_itv /= lexx. +- by rewrite -setIUr -itv_bndbnd_setU// set_itvNyy setIT. +apply: subset_separated; [exact: subIsetr | exact: subIsetr |]. +apply: open_separated. +- have-> : `]-oo, y[ = \bigcup_(z in `]-oo, y[ ) `[z, y[. + apply/seteqP; split=> w /=; rewrite in_itv/=. + by move=> wy; exists w=> //=; rewrite in_itv/= lexx. + by case=> z /=; rewrite !in_itv/= => _ /andP []. + apply: bigcup_open=> w ?; exists [set (w, y)]=> //. + exact: bigcup_set1. +- have-> : `[y, +oo[ = \bigcup_(z in `[y, +oo[ ) `[y, z[. + apply/seteqP; split=> w /=; rewrite in_itv/= andbT. + move=> yw; exists (w+1) => /=; rewrite in_itv/= ?ler_wpDr//. + by rewrite yw/= ltrDl. + by case=> z /=; rewrite !in_itv/= => _ /andP []. + apply: bigcup_open=> w _; exists [set (y, w)]=> //. + exact: bigcup_set1. +rewrite -subset0=> w [] /=; rewrite !in_itv /= andbT. +by move/lt_le_trans/[apply]; rewrite ltxx. Qed. From fddffe861cc0958eca7d43cb1c375c145478c00c Mon Sep 17 00:00:00 2001 From: Jacques Garrigue Date: Tue, 13 May 2025 08:29:37 +0900 Subject: [PATCH 08/45] almost complete proof of continuous_sdist --- theories/showcase/sorgenfreyline.v | 220 ++++++++++++++++++++++++++++- 1 file changed, 216 insertions(+), 4 deletions(-) diff --git a/theories/showcase/sorgenfreyline.v b/theories/showcase/sorgenfreyline.v index 9ab2cb9ae..18b0442e9 100644 --- a/theories/showcase/sorgenfreyline.v +++ b/theories/showcase/sorgenfreyline.v @@ -169,10 +169,222 @@ by move/lt_le_trans/[apply]; rewrite ltxx. Qed. -Definition sdist (E : set sorgenfrey) (x : sorgenfrey) := - let xl := inf [set y | x - y \in E /\ 0 < y] in - let xr := inf [set y | x + y \in E /\ 0 <= y] in - if x - xl \in E then Order.min xl xr else Order.min 1 xr. +Definition sdist (E : set sorgenfrey) (x : sorgenfrey) : R := + let dl := [set y | x - y \in E /\ 0 <= y] in + let dr := [set y | x + y \in E /\ 0 < y] in + Order.min (if x - inf dl \in E then inf dl else 1) + (if dr == set0 then 1 else inf dr). + +From mathcomp Require Import topology normedtype. +Let Rtopo := num_topology.numFieldTopology.Real_sort__canonical__topology_structure_Topological R. + +From mathcomp Require Import ring. + +Lemma abs_subr_min (x y t u : R) : + `|Num.min x y - Num.min t u| <= Num.max `|x - t| `|y - u|. +Proof. +have cxy : x >=< y by rewrite comparablerE num_real. +have ctu : t >=< u by rewrite comparablerE num_real. +have cxtyu : `|x-t| >=< `|y-u| by rewrite comparablerE num_real. +case: (comparable_leP cxy) => xy; case: (comparable_leP ctu) => tu; + rewrite comparable_le_max //. +- by rewrite lexx. +- case: (lerP x u) => xu. + case: (lerP x t) => xt. by rewrite lerD2r ltW. + by rewrite leNgt (lt_trans tu xt) in xu. + case: (lerP u y) => uy. by rewrite lerD2r xy orbT. + by rewrite leNgt (lt_trans uy xu) in xy. +- case: (lerP y t) => yt. + case: (lerP y u) => uy. by rewrite lerD2r tu orbT. + by rewrite leNgt (lt_le_trans uy yt) in tu. + case: (lerP t x) => xt. by rewrite lerD2r (ltW xy). + by rewrite ltNge (ltW (lt_trans xt yt)) in xy. +- by rewrite lexx orbT. +Qed. + +Lemma le_inf_n0 (E : set R) (x : R) : x \in E -> inf E != 0 -> inf E <= x. +Proof. +move=> xE infE0. +rewrite -(inf1 x) le_inf //. +- rewrite image_set1 => z /= ->. + apply/downP; exists (-x) => //. + by exists x => //; rewrite -inE. +- by exists x. +- move: infE0. + by apply: contraNP => /inf_out ->. +Qed. + +Lemma inf_ge0 (E : set R) : {in E, forall x : R, x >= 0} -> inf E >= 0. +Proof. +move=> E_ge0. +case/boolP: (E == set0) => [/eqP -> | /set0P E0]. + by rewrite inf0. +apply: lb_le_inf => // x Ex. +by apply: E_ge0; rewrite inE. +Qed. + +Lemma continuous_sdist E : + closed E -> forall x, @continuous_at sorgenfrey Rtopo x (sdist E). +Proof. +move=> CE x N. +rewrite -(@filter_from_ballE R (GRing_regular__canonical__pseudometric_structure_PseudoMetric R)). +case => eps /= eps0 epsN. +pose xepsE := [set y | x + y \in E /\ 0 < y < eps]. +pose eps' := xget eps xepsE. +exists (`[x,x+eps'[); split => //=. +- exists [set (x,x+eps')]. + by move=> i /= ->. + by rewrite bigcup_set1. +- rewrite in_itv /= lexx ltrDl /eps' /=. + case: (xgetP eps xepsE) => //. + move=> y ->. + by rewrite /xepsE /= => -[] _ /andP[]. +rewrite -image_sub. +move=> y /= [] z. +rewrite in_itv /= => /andP[xz zx] <- {y}. +apply: epsN. +rewrite /ball /=. +rewrite /sdist. +have [<-|xz'] := eqVneq x z. + by rewrite subrr normr0. +have {xz xz'} xz: x < z by rewrite lt_neqAle xz'. +set dxl := [set y | x - y \in E /\ 0 <= y]. +set dxr := [set y | x + y \in E /\ 0 < y]. +set xr : R := if dxr == set0 then _ else _. +set dzl := [set y | z - y \in E /\ 0 <= y]. +set dzr := [set y | z + y \in E /\ 0 < y]. +set zr : R := if dzr == set0 then _ else _. +case/boolP: (xepsE == set0). + move/eqP => xepsE0. + have Heps' : eps' = eps. + rewrite /eps'. + case: (xgetP eps xepsE) => //. + move=> y ->. + by rewrite xepsE0. + rewrite {}Heps' {eps'} in zx. + have znE : z \notin E. + apply/negP => zE. + suff : xepsE (z-x) by rewrite xepsE0. + by rewrite /xepsE /= addrA (addrC x) addrK zE ltrBrDl addr0 ltrBlDl xz zx. + have Hr : `|Num.min 1 xr - Num.min 1 zr| < eps. + rewrite /xr /zr. + case/boolP: (dxr == set0) => dxr0. + suff -> : dzr == set0 by rewrite subrr normr0. + apply/notP => /negP/set0P [] y [] Hy y0. + suff : y + z - x \in dxr by rewrite (eqP dxr0) inE. + rewrite inE /dxr /= addrA (addrC x) addrK addrC Hy. + by rewrite subr_gt0 ltr_wpDr // ltW. + rewrite ifF. rewrite (le_lt_trans (abs_subr_min _ _ _ _)) //. admit. + apply/negbTE/set0P. + case/set0P: dxr0 => y [] Hy y0. + exists (y + x - z). + rewrite /dzr /= addrA (addrC z) addrK addrC Hy. + rewrite subr_gt0 ltNge. + split => //; apply/negP => xyz. + suff : xepsE y by rewrite xepsE0. + by rewrite /xepsE /= Hy y0 -(ltrD2l x) (le_lt_trans xyz). + have [dxl0|] := eqVneq dxl set0. + rewrite dxl0 inf0 subr0. + case: ifPn => xinE. + suff : 0 \in dxl by rewrite inE dxl0. + by rewrite inE /dxl /= subr0. + have dzl0 : dzl = set0. + apply/notP => /eqP/set0P [t] [] ztE t0. + case/boolP: (z - t > x) => ztx. + suff : z-t-x \in xepsE by rewrite xepsE0 inE. + rewrite inE /xepsE /= addrA (addrC x) addrK ztE. + rewrite ltrBrDl addr0 ztx ltrBlDl. + by rewrite -(subr0 (x+eps)) ltr_leB. + rewrite -leNgt in ztx. + suff : x - (z-t) \in dxl by rewrite dxl0 inE. + rewrite inE /dxl /=. + by rewrite opprD addrA addrC subrr addr0 opprK ztE lerBrDl addr0. + by rewrite dzl0 inf0 subr0 (negbTE znE). + case/set0P => w Hw. + have xzl : x - inf dxl = z - inf dzl. + rewrite /dzl. + rewrite -{1}(addrNK x z) (addrC (z-x)) -(opprB x) -(inf1 (x-z)). + rewrite -addrA -opprD -inf_sumE; first last. + - split; last by exists 0 => t []. + exists (w+z-x) => //=. + rewrite -addrA opprD !addrA (addrC z) addrKA opprK addrC. + case: Hw => -> w0. + by rewrite lerBrDl addr0 ler_wpDl // (ltW xz). + - exact: has_inf1. + congr (x - inf _); symmetry. + apply/seteqP; split => t /=. + case=> u -> [{}u] [wE w0] <-{t}. + rewrite /dxl /= !opprD opprK !addrA subrr add0r wE. + have : z - u <= x. + rewrite -subr_le0 leNgt. + apply/negP => zux. + suff : xepsE (z - u - x) by rewrite xepsE0. + rewrite /xepsE /= (addrC x) -addrA (addrC _ x) subrr addr0 wE. + by rewrite zux ltrBlDr (addrC _ x) (le_lt_trans _ zx) // gerBl. + by rewrite -addrA (addrC (-z)) -(opprB z) lerBrDl addr0. + case=> xtE t0. + exists (x-z) => //. + exists (t+z-x); last by ring. + rewrite (_ : z - _ = x - t); last by ring. + by rewrite xtE -addrA addr_ge0 // subr_ge0 ltW. + rewrite -xzl. + case: ifPn => xlE //. + rewrite (le_lt_trans (abs_subr_min _ _ _ _)) //. admit. +move/set0P/xgetPex => /(_ eps). +rewrite -/eps' => -[] eps'E Heps'. +have eps'l : forall t, x <= t < x + eps' -> + let dr := [set y | t + y \in E /\ 0 < y] in + 0 <= (if dr == set0 then 1 else inf dr) < eps. + move=> t Ht /=. + set dr := [set y | t + y \in E /\ 0 < y]. + rewrite ifF; last first. + apply/negbTE/set0P. + exists (x+eps'-t). + rewrite /dr /= (addrC _ (-t)) addrA subrr add0r eps'E. + rewrite addrC subr_gt0 //; by case/andP: Ht. + rewrite inf_ge0; last by move=> u; rewrite inE => -[] _ /ltW. + case/boolP: (dr == set0) => [/eqP ->|/set0P dr0]. + by rewrite inf0 eps0. + have [-> // | infdr0] := eqVneq (inf dr) 0. + apply (@le_lt_trans _ _ (eps'+x-t)). + apply: le_inf_n0 => //. + rewrite inE /dr /= (addrC _ (-t)) addrA subrr add0r addrC eps'E. + rewrite addrC subr_gt0 //; by case/andP: Ht. + apply: (@le_lt_trans _ _ eps'). + rewrite -addrA gerDl lerBlDl addr0; by case/andP: Ht. + by case/andP: Heps'. +set dr := Num.min _ _. +set dr' := Num.min _ _. +have Hdr : 0 <= dr < eps. + rewrite /dr. + rewrite comparable_le_min; last first. + apply:real_leVge; apply:num_real; apply:num_real. + rewrite comparable_gt_min; last first. + apply:real_leVge; apply:num_real; apply:num_real. + rewrite fun_if inf_ge0; last by move=> u; rewrite inE => -[]. + rewrite ler01 if_same /=. + have : x <= x < x + eps'. + by rewrite lexx ltrDl; case/andP: Heps'. + move/eps'l => /andP[] -> ->. + by rewrite orbT. +have Hdr' : 0 <= dr' < eps. + rewrite /dr'. + rewrite comparable_le_min; last first. + apply:real_leVge; apply:num_real; apply:num_real. + rewrite comparable_gt_min; last first. + apply:real_leVge; apply:num_real; apply:num_real. + rewrite fun_if inf_ge0; last by move=> u; rewrite inE => -[]. + rewrite ler01 if_same /=. + have : x <= z < x + eps'. + by rewrite zx ltW // xz. + move/eps'l => /andP[] -> ->. + by rewrite orbT. +rewrite -maxrN comparable_gt_max; last exact/real_leVge/num_real/num_real. +case/andP: Hdr => Hdr1 Hdr2. +case/andP: Hdr' => Hdr1' Hdr2'. +rewrite (le_lt_trans _ Hdr2) ?gerBl //. +by rewrite (le_lt_trans _ Hdr2') // opprD opprK addrC gerBl. +Abort. End Sorgenfrey_line. From 187db8b67ffcec30330fcb1429320660a9213094 Mon Sep 17 00:00:00 2001 From: Jacques Garrigue Date: Tue, 13 May 2025 09:52:32 +0900 Subject: [PATCH 09/45] simplify abs_subr_min --- theories/showcase/sorgenfreyline.v | 28 ++++++++++++---------------- 1 file changed, 12 insertions(+), 16 deletions(-) diff --git a/theories/showcase/sorgenfreyline.v b/theories/showcase/sorgenfreyline.v index 18b0442e9..97be31792 100644 --- a/theories/showcase/sorgenfreyline.v +++ b/theories/showcase/sorgenfreyline.v @@ -183,23 +183,19 @@ From mathcomp Require Import ring. Lemma abs_subr_min (x y t u : R) : `|Num.min x y - Num.min t u| <= Num.max `|x - t| `|y - u|. Proof. -have cxy : x >=< y by rewrite comparablerE num_real. -have ctu : t >=< u by rewrite comparablerE num_real. +wlog xy: x y t u / x <= y. + move=> H. + case/boolP: (x <= y) => [/H //| xy]. + by rewrite minC (minC t) maxC H // ltW // ltNge. +case: (lerP x y); [move=> _ | by rewrite ltNge xy]. have cxtyu : `|x-t| >=< `|y-u| by rewrite comparablerE num_real. -case: (comparable_leP cxy) => xy; case: (comparable_leP ctu) => tu; - rewrite comparable_le_max //. -- by rewrite lexx. -- case: (lerP x u) => xu. - case: (lerP x t) => xt. by rewrite lerD2r ltW. - by rewrite leNgt (lt_trans tu xt) in xu. - case: (lerP u y) => uy. by rewrite lerD2r xy orbT. - by rewrite leNgt (lt_trans uy xu) in xy. -- case: (lerP y t) => yt. - case: (lerP y u) => uy. by rewrite lerD2r tu orbT. - by rewrite leNgt (lt_le_trans uy yt) in tu. - case: (lerP t x) => xt. by rewrite lerD2r (ltW xy). - by rewrite ltNge (ltW (lt_trans xt yt)) in xy. -- by rewrite lexx orbT. +case: (lerP t u) => tu; rewrite comparable_le_max //. + by rewrite lexx. +case: (lerP x u) => xu. + case: (lerP x t) => xt. by rewrite lerD2r ltW. + by rewrite leNgt (lt_trans tu xt) in xu. +case: (lerP u y) => uy. by rewrite lerD2r xy orbT. +by rewrite leNgt (lt_trans uy xu) in xy. Qed. Lemma le_inf_n0 (E : set R) (x : R) : x \in E -> inf E != 0 -> inf E <= x. From c75057f78f66d361c702f41e3593cb053ae4e10c Mon Sep 17 00:00:00 2001 From: Yosuke Tsuji Date: Wed, 4 Jun 2025 11:21:27 +0900 Subject: [PATCH 10/45] fix Definition perfectly_normal_space --- theories/topology_theory/separation_axioms.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/theories/topology_theory/separation_axioms.v b/theories/topology_theory/separation_axioms.v index 14c1172dd..039a0f82d 100644 --- a/theories/topology_theory/separation_axioms.v +++ b/theories/topology_theory/separation_axioms.v @@ -1137,7 +1137,7 @@ Section perfectlynormalspace. Context (R : realType) (T : topologicalType). Definition perfectly_normal_space := - forall E F : set T, exists f : T -> R, - continuous f /\ E `<=` f @^-1` [set 0] /\ F `<=` f @^-1` [set 1]. + forall E : set T, closed E -> + exists f : T -> R, continuous f /\ E = f @^-1` [set 0]. End perfectlynormalspace. From 4e36b69bd115809c4421e12ead526b4d65320184 Mon Sep 17 00:00:00 2001 From: Jacques Garrigue Date: Wed, 14 May 2025 10:27:00 +0900 Subject: [PATCH 11/45] prove zeroset_sdist --- theories/showcase/sorgenfreyline.v | 248 ++++++++++++++++------------- 1 file changed, 133 insertions(+), 115 deletions(-) diff --git a/theories/showcase/sorgenfreyline.v b/theories/showcase/sorgenfreyline.v index 97be31792..c36b9d5ae 100644 --- a/theories/showcase/sorgenfreyline.v +++ b/theories/showcase/sorgenfreyline.v @@ -168,12 +168,15 @@ rewrite -subset0=> w [] /=; rewrite !in_itv /= andbT. by move/lt_le_trans/[apply]; rewrite ltxx. Qed. +(* Pseudo-distance function for perfectly normal space *) +Variable E : set sorgenfrey. +Hypothesis CE : closed E. -Definition sdist (E : set sorgenfrey) (x : sorgenfrey) : R := - let dl := [set y | x - y \in E /\ 0 <= y] in - let dr := [set y | x + y \in E /\ 0 < y] in - Order.min (if x - inf dl \in E then inf dl else 1) - (if dr == set0 then 1 else inf dr). +Let dl x := [set y | x - y \in E /\ 0 <= y]. +Let dr x := [set y | x + y \in E /\ 0 < y]. +Definition sdist (x : sorgenfrey) : R := + Order.min (if x - inf (dl x) \in E then inf (dl x) else 1) + (if dr x == set0 then 1 else inf (dr x)). From mathcomp Require Import topology normedtype. Let Rtopo := num_topology.numFieldTopology.Real_sort__canonical__topology_structure_Topological R. @@ -183,11 +186,11 @@ From mathcomp Require Import ring. Lemma abs_subr_min (x y t u : R) : `|Num.min x y - Num.min t u| <= Num.max `|x - t| `|y - u|. Proof. -wlog xy: x y t u / x <= y. +wlog: x y t u / x <= y. move=> H. case/boolP: (x <= y) => [/H //| xy]. by rewrite minC (minC t) maxC H // ltW // ltNge. -case: (lerP x y); [move=> _ | by rewrite ltNge xy]. +case: (lerP x y) => // xy _. have cxtyu : `|x-t| >=< `|y-u| by rewrite comparablerE num_real. case: (lerP t u) => tu; rewrite comparable_le_max //. by rewrite lexx. @@ -198,31 +201,37 @@ case: (lerP u y) => uy. by rewrite lerD2r xy orbT. by rewrite leNgt (lt_trans uy xu) in xy. Qed. -Lemma le_inf_n0 (E : set R) (x : R) : x \in E -> inf E != 0 -> inf E <= x. +Lemma le_inf_n0 (S : set R) (x : R) : x \in S -> inf S != 0 -> inf S <= x. Proof. -move=> xE infE0. +move=> xS infS0. rewrite -(inf1 x) le_inf //. - rewrite image_set1 => z /= ->. apply/downP; exists (-x) => //. by exists x => //; rewrite -inE. - by exists x. -- move: infE0. +- move: infS0. by apply: contraNP => /inf_out ->. Qed. -Lemma inf_ge0 (E : set R) : {in E, forall x : R, x >= 0} -> inf E >= 0. +Lemma inf_ge0 (S : set R) : {in S, forall x : R, x >= 0} -> inf S >= 0. Proof. -move=> E_ge0. -case/boolP: (E == set0) => [/eqP -> | /set0P E0]. +move=> S_ge0. +case/boolP: (S == set0) => [/eqP -> | /set0P S0]. by rewrite inf0. -apply: lb_le_inf => // x Ex. -by apply: E_ge0; rewrite inE. +apply: lb_le_inf => // x Sx. +by apply: S_ge0; rewrite inE. Qed. -Lemma continuous_sdist E : - closed E -> forall x, @continuous_at sorgenfrey Rtopo x (sdist E). +Let dl_ge0 x : {in dl x, forall y : R, y >= 0}. +Proof. by move=> y; rewrite inE => -[]. Qed. + +Let dr_ge0 x : {in dr x, forall y : R, y >= 0}. +Proof. by move=> y; rewrite inE => -[] _ /ltW. Qed. + +Lemma continuous_sdist : + forall x, @continuous_at sorgenfrey Rtopo x sdist. Proof. -move=> CE x N. +move=> x N. rewrite -(@filter_from_ballE R (GRing_regular__canonical__pseudometric_structure_PseudoMetric R)). case => eps /= eps0 epsN. pose xepsE := [set y | x + y \in E /\ 0 < y < eps]. @@ -244,12 +253,8 @@ rewrite /sdist. have [<-|xz'] := eqVneq x z. by rewrite subrr normr0. have {xz xz'} xz: x < z by rewrite lt_neqAle xz'. -set dxl := [set y | x - y \in E /\ 0 <= y]. -set dxr := [set y | x + y \in E /\ 0 < y]. -set xr : R := if dxr == set0 then _ else _. -set dzl := [set y | z - y \in E /\ 0 <= y]. -set dzr := [set y | z + y \in E /\ 0 < y]. -set zr : R := if dzr == set0 then _ else _. +set xr : R := if dr x == set0 then _ else _. +set zr : R := if dr z == set0 then _ else _. case/boolP: (xepsE == set0). move/eqP => xepsE0. have Heps' : eps' = eps. @@ -264,123 +269,136 @@ case/boolP: (xepsE == set0). by rewrite /xepsE /= addrA (addrC x) addrK zE ltrBrDl addr0 ltrBlDl xz zx. have Hr : `|Num.min 1 xr - Num.min 1 zr| < eps. rewrite /xr /zr. - case/boolP: (dxr == set0) => dxr0. - suff -> : dzr == set0 by rewrite subrr normr0. + case: ifPn => drx0. + suff -> : dr z == set0 by rewrite subrr normr0. apply/notP => /negP/set0P [] y [] Hy y0. - suff : y + z - x \in dxr by rewrite (eqP dxr0) inE. - rewrite inE /dxr /= addrA (addrC x) addrK addrC Hy. + suff : y + z - x \in dr x by rewrite (eqP drx0) inE. + rewrite inE /dr /= addrA (addrC x) addrK addrC Hy. by rewrite subr_gt0 ltr_wpDr // ltW. rewrite ifF. rewrite (le_lt_trans (abs_subr_min _ _ _ _)) //. admit. apply/negbTE/set0P. - case/set0P: dxr0 => y [] Hy y0. + case/set0P: drx0 => y [] Hy y0. exists (y + x - z). - rewrite /dzr /= addrA (addrC z) addrK addrC Hy. + rewrite /dr /= addrA (addrC z) addrK addrC Hy. rewrite subr_gt0 ltNge. split => //; apply/negP => xyz. suff : xepsE y by rewrite xepsE0. by rewrite /xepsE /= Hy y0 -(ltrD2l x) (le_lt_trans xyz). - have [dxl0|] := eqVneq dxl set0. - rewrite dxl0 inf0 subr0. - case: ifPn => xinE. - suff : 0 \in dxl by rewrite inE dxl0. - by rewrite inE /dxl /= subr0. - have dzl0 : dzl = set0. - apply/notP => /eqP/set0P [t] [] ztE t0. + have dlxz : dl z = [set t + (z - x) | t in dl x]. + apply/seteqP; rewrite /dl; split => t /= []. + move => ztE y0. case/boolP: (z - t > x) => ztx. suff : z-t-x \in xepsE by rewrite xepsE0 inE. rewrite inE /xepsE /= addrA (addrC x) addrK ztE. rewrite ltrBrDl addr0 ztx ltrBlDl. by rewrite -(subr0 (x+eps)) ltr_leB. rewrite -leNgt in ztx. - suff : x - (z-t) \in dxl by rewrite dxl0 inE. - rewrite inE /dxl /=. - by rewrite opprD addrA addrC subrr addr0 opprK ztE lerBrDl addr0. - by rewrite dzl0 inf0 subr0 (negbTE znE). + exists (x - (z-t)). + by rewrite opprD addrA subrr opprK add0r ztE subr_ge0. + by rewrite (addrC z) opprD opprK !addrA addrNK addrAC subrr add0r. + move=> w [] xwE w0 <-. + rewrite !opprD (addrCA z) !addrA addrK addrC opprK xwE. + by rewrite subr_ge0 ler_wpDl // ltW. + have [dlx0|] := eqVneq (dl x) set0. + rewrite dlx0 inf0 subr0. + case: ifPn => xinE. + suff : 0 \in dl x by rewrite inE dlx0. + by rewrite inE /dl /= subr0. + by rewrite dlxz dlx0 image_set0 inf0 subr0 (negbTE znE). case/set0P => w Hw. - have xzl : x - inf dxl = z - inf dzl. - rewrite /dzl. - rewrite -{1}(addrNK x z) (addrC (z-x)) -(opprB x) -(inf1 (x-z)). - rewrite -addrA -opprD -inf_sumE; first last. - - split; last by exists 0 => t []. - exists (w+z-x) => //=. - rewrite -addrA opprD !addrA (addrC z) addrKA opprK addrC. - case: Hw => -> w0. - by rewrite lerBrDl addr0 ler_wpDl // (ltW xz). - - exact: has_inf1. - congr (x - inf _); symmetry. - apply/seteqP; split => t /=. - case=> u -> [{}u] [wE w0] <-{t}. - rewrite /dxl /= !opprD opprK !addrA subrr add0r wE. - have : z - u <= x. - rewrite -subr_le0 leNgt. - apply/negP => zux. - suff : xepsE (z - u - x) by rewrite xepsE0. - rewrite /xepsE /= (addrC x) -addrA (addrC _ x) subrr addr0 wE. - by rewrite zux ltrBlDr (addrC _ x) (le_lt_trans _ zx) // gerBl. - by rewrite -addrA (addrC (-z)) -(opprB z) lerBrDl addr0. - case=> xtE t0. - exists (x-z) => //. - exists (t+z-x); last by ring. - rewrite (_ : z - _ = x - t); last by ring. - by rewrite xtE -addrA addr_ge0 // subr_ge0 ltW. + have xzl : x - inf (dl x) = z - inf (dl z). + rewrite dlxz. + rewrite (_ : [set _ | _ in _] = [set t + y | t in dl x & y in [set z - x]]). + rewrite inf_sumE. + - by rewrite inf1 !opprD !addrA (addrC z) addrK (opprK x) addrC. + - split. by exists w. + exists 0. move=> u. rewrite -inE. exact: dl_ge0. + - exact: has_inf1. + apply/seteqP; split => y /= [] u dlxu. + by move <-; exists u => //; exists (z-x). + by case=> v -> <-; exists u. rewrite -xzl. case: ifPn => xlE //. rewrite (le_lt_trans (abs_subr_min _ _ _ _)) //. admit. move/set0P/xgetPex => /(_ eps). rewrite -/eps' => -[] eps'E Heps'. -have eps'l : forall t, x <= t < x + eps' -> - let dr := [set y | t + y \in E /\ 0 < y] in - 0 <= (if dr == set0 then 1 else inf dr) < eps. +rewrite -/(sdist x) -/(sdist z). +have eps'l : forall t, x <= t < x + eps' -> 0 <= sdist t < eps. move=> t Ht /=. - set dr := [set y | t + y \in E /\ 0 < y]. - rewrite ifF; last first. - apply/negbTE/set0P. + rewrite /sdist. + set xl : R := if _ then _ else 1. + case: ifPn. + move/negP; elim; apply/negP/set0P. exists (x+eps'-t). rewrite /dr /= (addrC _ (-t)) addrA subrr add0r eps'E. rewrite addrC subr_gt0 //; by case/andP: Ht. - rewrite inf_ge0; last by move=> u; rewrite inE => -[] _ /ltW. - case/boolP: (dr == set0) => [/eqP ->|/set0P dr0]. - by rewrite inf0 eps0. - have [-> // | infdr0] := eqVneq (inf dr) 0. - apply (@le_lt_trans _ _ (eps'+x-t)). - apply: le_inf_n0 => //. - rewrite inE /dr /= (addrC _ (-t)) addrA subrr add0r addrC eps'E. - rewrite addrC subr_gt0 //; by case/andP: Ht. - apply: (@le_lt_trans _ _ eps'). - rewrite -addrA gerDl lerBlDl addr0; by case/andP: Ht. - by case/andP: Heps'. -set dr := Num.min _ _. -set dr' := Num.min _ _. -have Hdr : 0 <= dr < eps. - rewrite /dr. - rewrite comparable_le_min; last first. - apply:real_leVge; apply:num_real; apply:num_real. - rewrite comparable_gt_min; last first. - apply:real_leVge; apply:num_real; apply:num_real. - rewrite fun_if inf_ge0; last by move=> u; rewrite inE => -[]. - rewrite ler01 if_same /=. - have : x <= x < x + eps'. - by rewrite lexx ltrDl; case/andP: Heps'. - move/eps'l => /andP[] -> ->. - by rewrite orbT. -have Hdr' : 0 <= dr' < eps. - rewrite /dr'. - rewrite comparable_le_min; last first. - apply:real_leVge; apply:num_real; apply:num_real. - rewrite comparable_gt_min; last first. - apply:real_leVge; apply:num_real; apply:num_real. - rewrite fun_if inf_ge0; last by move=> u; rewrite inE => -[]. - rewrite ler01 if_same /=. - have : x <= z < x + eps'. - by rewrite zx ltW // xz. - move/eps'l => /andP[] -> ->. - by rewrite orbT. + move=> drt0. + rewrite comparable_le_min; last exact/real_leVge/num_real/num_real. + rewrite comparable_gt_min; last exact/real_leVge/num_real/num_real. + rewrite {1}/xl fun_if inf_ge0 // ler01 if_same /=. + rewrite inf_ge0 /=; last by move=> u; rewrite inE => -[] _ /ltW. + case/andP: Ht => xt tx. + rewrite orbC (@le_lt_trans _ _ (eps'+x-t)) //. + have [-> | infdr0] := eqVneq (inf (dr t)) 0. + by rewrite subr_ge0 addrC ltW. + rewrite le_inf_n0 // inE /dr /= (addrC _ (-t)) addrA subrr add0r addrC. + by rewrite eps'E addrC subr_gt0. + case/andP: Heps' => eps'0 Heps'. + by rewrite (le_lt_trans _ Heps') // -addrA gerDl lerBlDl addr0. +have Hx : 0 <= sdist x < eps. + by apply: eps'l; rewrite lexx ltrDl; case/andP: Heps'. +have Hz : 0 <= sdist z < eps. + by apply: eps'l; rewrite zx ltW // xz. rewrite -maxrN comparable_gt_max; last exact/real_leVge/num_real/num_real. -case/andP: Hdr => Hdr1 Hdr2. -case/andP: Hdr' => Hdr1' Hdr2'. -rewrite (le_lt_trans _ Hdr2) ?gerBl //. -by rewrite (le_lt_trans _ Hdr2') // opprD opprK addrC gerBl. -Abort. +case/andP: Hx => Hx1 Hx2. +case/andP: Hz => Hz1 Hz2. +by rewrite opprB !ltrBlDr !ltr_wpDr. +Admitted. +Lemma zeroset_sdist : E = sdist @^-1` [set 0]. +Proof. +rewrite /sdist. +apply/seteqP; split => x /= Hx. + suff -> : inf (dl x) = 0. + rewrite subr0 ifT; last by rewrite inE. + case: ifP => _; case: lerP => //. + by rewrite ltNge ler01. + by rewrite ltNge inf_ge0. + apply/eqP; rewrite eq_le inf_ge0 //. + rewrite -[X in _ <= X]inf1 le_inf /dl //=. + - move=> y []z /= -> <- /=. + exists (-0); split => //=. + exists 0 => //; by rewrite subr0 inE. + - by exists 0. + - split. exists 0 => /=; by rewrite subr0 inE. + by exists 0 => y []. +move/eqP: Hx; rewrite /sdist. +rewrite minEle; case: ifP => _. + case: ifP; last by rewrite (negbTE (@oner_neq0 _)). + rewrite inE => /[swap] /eqP ->. + by rewrite subr0. +case: ifPn; first by rewrite (negbTE (@oner_neq0 _)). +move=> n0 /eqP infeq. +case/boolP: (x \in E); first by rewrite inE. +rewrite -in_setC inE. +have : open (~` E) by rewrite openC. +rewrite openE /= => HE xE. +suff: False by []. +case: (HE x xE) => opx [] /= [] L HL <- [] /= [a a'] La. +rewrite /b /= in_itv /= => xa. +move/(subset_trans (bigcup_sup La)) => /= aE. +have := @inf_adherent _ (dr x) (a' -x). +case/andP: xa => ax xa'. +rewrite subr_gt0 xa'. +have hE : has_inf (dr x). + split. by apply/set0P. + exists 0. by move=> y [] _ /ltW. +case/(_ isT hE) => y yxr. +rewrite infeq add0r ltrBrDl => xya'. +case: yxr => xyE y0. +suff : x+y \notin E by rewrite xyE. +rewrite -in_setC inE. apply: aE => /=. +by rewrite in_itv /= xya' (le_trans ax) // ler_wpDr // ltW. +Qed. End Sorgenfrey_line. From 7159793e65938813189a76c33b2a51ac14c1131d Mon Sep 17 00:00:00 2001 From: Jacques Garrigue Date: Wed, 14 May 2025 11:35:18 +0900 Subject: [PATCH 12/45] clarify --- theories/showcase/sorgenfreyline.v | 59 ++++++++++++++++-------------- 1 file changed, 32 insertions(+), 27 deletions(-) diff --git a/theories/showcase/sorgenfreyline.v b/theories/showcase/sorgenfreyline.v index c36b9d5ae..ef9e363f7 100644 --- a/theories/showcase/sorgenfreyline.v +++ b/theories/showcase/sorgenfreyline.v @@ -228,6 +228,21 @@ Proof. by move=> y; rewrite inE => -[]. Qed. Let dr_ge0 x : {in dr x, forall y : R, y >= 0}. Proof. by move=> y; rewrite inE => -[] _ /ltW. Qed. +Lemma image2_set1 A B C (S : set A) (eb : B) (f : A -> B -> C) : + [set f x y | x in S & y in [set eb]] = [set f x eb | x in S]. +Proof. +apply/seteqP; split => y /= [] u dlxu. + by case=> v -> <-; exists u. +by move <-; exists u => //; exists eb. +Qed. + +Lemma image2X A B C (SA : set A) (SB : set B) (f : A -> B -> C) : + [set f x y | x in SA & y in SB] = [set f x y | y in SB & x in SA]. +Proof. +rewrite !image2E. +by apply/seteqP; split => c /= [] [x y] /= [] Hx Hy <-; exists (y,x). +Qed. + Lemma continuous_sdist : forall x, @continuous_at sorgenfrey Rtopo x sdist. Proof. @@ -257,16 +272,12 @@ set xr : R := if dr x == set0 then _ else _. set zr : R := if dr z == set0 then _ else _. case/boolP: (xepsE == set0). move/eqP => xepsE0. - have Heps' : eps' = eps. - rewrite /eps'. - case: (xgetP eps xepsE) => //. - move=> y ->. - by rewrite xepsE0. + have Heps' : eps' = eps by rewrite /eps' xgetPN // xepsE0 => t. rewrite {}Heps' {eps'} in zx. have znE : z \notin E. apply/negP => zE. suff : xepsE (z-x) by rewrite xepsE0. - by rewrite /xepsE /= addrA (addrC x) addrK zE ltrBrDl addr0 ltrBlDl xz zx. + by rewrite /xepsE /= addrA (addrC x) addrK subr_gt0 xz ltrBlDl. have Hr : `|Num.min 1 xr - Num.min 1 zr| < eps. rewrite /xr /zr. case: ifPn => drx0. @@ -275,29 +286,29 @@ case/boolP: (xepsE == set0). suff : y + z - x \in dr x by rewrite (eqP drx0) inE. rewrite inE /dr /= addrA (addrC x) addrK addrC Hy. by rewrite subr_gt0 ltr_wpDr // ltW. - rewrite ifF. rewrite (le_lt_trans (abs_subr_min _ _ _ _)) //. admit. + rewrite ifF. + rewrite (le_lt_trans (abs_subr_min _ _ _ _)) //. + rewrite subrr normr0 maxEle normr_ge0. + admit. apply/negbTE/set0P. case/set0P: drx0 => y [] Hy y0. exists (y + x - z). - rewrite /dr /= addrA (addrC z) addrK addrC Hy. - rewrite subr_gt0 ltNge. + rewrite /dr /= addrA (addrC z) addrK addrC Hy subr_gt0 ltNge. split => //; apply/negP => xyz. suff : xepsE y by rewrite xepsE0. by rewrite /xepsE /= Hy y0 -(ltrD2l x) (le_lt_trans xyz). have dlxz : dl z = [set t + (z - x) | t in dl x]. apply/seteqP; rewrite /dl; split => t /= []. move => ztE y0. - case/boolP: (z - t > x) => ztx. + case: (ltrP x (z-t)) => ztx. suff : z-t-x \in xepsE by rewrite xepsE0 inE. rewrite inE /xepsE /= addrA (addrC x) addrK ztE. - rewrite ltrBrDl addr0 ztx ltrBlDl. - by rewrite -(subr0 (x+eps)) ltr_leB. - rewrite -leNgt in ztx. + by rewrite subr_gt0 ztx ltrBlDl ltrBlDr ltr_wpDr. exists (x - (z-t)). by rewrite opprD addrA subrr opprK add0r ztE subr_ge0. - by rewrite (addrC z) opprD opprK !addrA addrNK addrAC subrr add0r. + by rewrite (addrC z) opprD opprK !addrA addrNK addrC addKr. move=> w [] xwE w0 <-. - rewrite !opprD (addrCA z) !addrA addrK addrC opprK xwE. + rewrite !opprD (addrCA z) !addrA addrK addrC opprK. by rewrite subr_ge0 ler_wpDl // ltW. have [dlx0|] := eqVneq (dl x) set0. rewrite dlx0 inf0 subr0. @@ -306,18 +317,12 @@ case/boolP: (xepsE == set0). by rewrite inE /dl /= subr0. by rewrite dlxz dlx0 image_set0 inf0 subr0 (negbTE znE). case/set0P => w Hw. - have xzl : x - inf (dl x) = z - inf (dl z). - rewrite dlxz. - rewrite (_ : [set _ | _ in _] = [set t + y | t in dl x & y in [set z - x]]). - rewrite inf_sumE. - - by rewrite inf1 !opprD !addrA (addrC z) addrK (opprK x) addrC. - - split. by exists w. - exists 0. move=> u. rewrite -inE. exact: dl_ge0. - - exact: has_inf1. - apply/seteqP; split => y /= [] u dlxu. - by move <-; exists u => //; exists (z-x). - by case=> v -> <-; exists u. - rewrite -xzl. + have <- : x - inf (dl x) = z - inf (dl z). + rewrite dlxz -image2_set1 inf_sumE. + - by rewrite inf1 !opprD !addrA (addrC z) addrK (opprK x) addrC. + - split. by exists w. + exists 0. move=> u. rewrite -inE. exact: dl_ge0. + - exact: has_inf1. case: ifPn => xlE //. rewrite (le_lt_trans (abs_subr_min _ _ _ _)) //. admit. move/set0P/xgetPex => /(_ eps). From 39100b73a043500a819cc80cb33b20c992aa8777 Mon Sep 17 00:00:00 2001 From: Jacques Garrigue Date: Wed, 14 May 2025 20:30:13 +0900 Subject: [PATCH 13/45] dl_shift --- theories/showcase/sorgenfreyline.v | 72 +++++++++++++++++++++--------- 1 file changed, 50 insertions(+), 22 deletions(-) diff --git a/theories/showcase/sorgenfreyline.v b/theories/showcase/sorgenfreyline.v index ef9e363f7..c8e314ad8 100644 --- a/theories/showcase/sorgenfreyline.v +++ b/theories/showcase/sorgenfreyline.v @@ -243,28 +243,62 @@ rewrite !image2E. by apply/seteqP; split => c /= [] [x y] /= [] Hx Hy <-; exists (y,x). Qed. +Let dl_shift x z : + x < z -> `]x, z] `<=` ~` E -> dl z = [set t + (z - x) | t in dl x]. +Proof. +move=> xz xzNE. +apply/seteqP; rewrite /dl; split => t /= []. + move => ztE y0. + case: (ltrP x (z-t)) => ztx. + suff : z - t \notin E by rewrite ztE. + rewrite -in_setC inE. + apply: xzNE. + by rewrite /= in_itv /= ztx lerBlDr lerDl. + exists (x - (z-t)). + by rewrite opprD addrA subrr opprK add0r ztE subr_ge0. + by rewrite (addrC z) opprD opprK !addrA addrNK addrC addKr. +move=> w [] xwE w0 <-. +rewrite !opprD (addrCA z) !addrA addrK addrC opprK. +by rewrite subr_ge0 ler_wpDl // ltW. +Qed. + +Let dr_shift x z : + x < z -> `]x, z] `<=` ~` E -> dr x = [set t + (z - x) | t in dr z]. +Proof. +move=> xz xzNE. +apply/seteqP; rewrite /dr; split => t /= []. + move => xtE y0. + case: (ltrP z (x+t)) => zxt; last first. + suff : x + t \notin E by rewrite xtE. + rewrite -in_setC inE. + apply: xzNE. + by rewrite /= in_itv /= zxt ltrDl y0. + exists (x + t - z). + by rewrite addrA (addrC z) addrK xtE subr_gt0. + by rewrite addrA (addrAC _ _ z) addrK (addrC x) addrK. +move=> w [] xwE w0 <-. +rewrite !addrA addrAC (addrC x) addrK addrC. +by rewrite subr_gt0 ltr_wpDr // ltW. +Qed. + Lemma continuous_sdist : forall x, @continuous_at sorgenfrey Rtopo x sdist. Proof. -move=> x N. +move=> x B. rewrite -(@filter_from_ballE R (GRing_regular__canonical__pseudometric_structure_PseudoMetric R)). -case => eps /= eps0 epsN. +case => eps /= eps0 epsB. pose xepsE := [set y | x + y \in E /\ 0 < y < eps]. pose eps' := xget eps xepsE. exists (`[x,x+eps'[); split => //=. -- exists [set (x,x+eps')]. - by move=> i /= ->. +- exists [set (x,x+eps')] => //. by rewrite bigcup_set1. - rewrite in_itv /= lexx ltrDl /eps' /=. - case: (xgetP eps xepsE) => //. - move=> y ->. - by rewrite /xepsE /= => -[] _ /andP[]. + by case: (xgetP eps xepsE) => // y -> [] _ /andP[]. rewrite -image_sub. move=> y /= [] z. rewrite in_itv /= => /andP[xz zx] <- {y}. -apply: epsN. -rewrite /ball /=. -rewrite /sdist. +apply: epsB. +rewrite /ball /sdist /=. have [<-|xz'] := eqVneq x z. by rewrite subrr normr0. have {xz xz'} xz: x < z by rewrite lt_neqAle xz'. @@ -298,18 +332,12 @@ case/boolP: (xepsE == set0). suff : xepsE y by rewrite xepsE0. by rewrite /xepsE /= Hy y0 -(ltrD2l x) (le_lt_trans xyz). have dlxz : dl z = [set t + (z - x) | t in dl x]. - apply/seteqP; rewrite /dl; split => t /= []. - move => ztE y0. - case: (ltrP x (z-t)) => ztx. - suff : z-t-x \in xepsE by rewrite xepsE0 inE. - rewrite inE /xepsE /= addrA (addrC x) addrK ztE. - by rewrite subr_gt0 ztx ltrBlDl ltrBlDr ltr_wpDr. - exists (x - (z-t)). - by rewrite opprD addrA subrr opprK add0r ztE subr_ge0. - by rewrite (addrC z) opprD opprK !addrA addrNK addrC addKr. - move=> w [] xwE w0 <-. - rewrite !opprD (addrCA z) !addrA addrK addrC opprK. - by rewrite subr_ge0 ler_wpDl // ltW. + apply: dl_shift => // t /=. + rewrite in_itv /= => /andP[] xt tz. + apply: contraPnot xepsE0. + rewrite -inE => Et; apply/eqP/set0P. + exists (t-x); rewrite /xepsE /= addrA (addrC x) addrK. + by rewrite subr_gt0 xt ltrBlDl (le_lt_trans tz). have [dlx0|] := eqVneq (dl x) set0. rewrite dlx0 inf0 subr0. case: ifPn => xinE. From 5f315654598e0bb8caec7d7e93e4a4add5f31252 Mon Sep 17 00:00:00 2001 From: Jacques Garrigue Date: Wed, 4 Jun 2025 11:25:21 +0900 Subject: [PATCH 14/45] add section --- theories/showcase/sorgenfreyline.v | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/theories/showcase/sorgenfreyline.v b/theories/showcase/sorgenfreyline.v index c8e314ad8..4eccada93 100644 --- a/theories/showcase/sorgenfreyline.v +++ b/theories/showcase/sorgenfreyline.v @@ -168,10 +168,11 @@ rewrite -subset0=> w [] /=; rewrite !in_itv /= andbT. by move/lt_le_trans/[apply]; rewrite ltxx. Qed. -(* Pseudo-distance function for perfectly normal space *) +Section distance. Variable E : set sorgenfrey. Hypothesis CE : closed E. +(* Pseudo-distance function for perfectly normal space *) Let dl x := [set y | x - y \in E /\ 0 <= y]. Let dr x := [set y | x + y \in E /\ 0 < y]. Definition sdist (x : sorgenfrey) : R := @@ -433,5 +434,6 @@ suff : x+y \notin E by rewrite xyE. rewrite -in_setC inE. apply: aE => /=. by rewrite in_itv /= xya' (le_trans ax) // ler_wpDr // ltW. Qed. +End distance. End Sorgenfrey_line. From 10b62e3f0bd534c7c97336eadfe54b5010be9bdf Mon Sep 17 00:00:00 2001 From: Yosuke Tsuji Date: Fri, 20 Jun 2025 16:00:02 +0900 Subject: [PATCH 15/45] remove Admitted --- _CoqProject | 1 - experimental_reals/discrete.v | 2 +- reals/all_reals.v | 1 - reals/interval_inference.v | 1642 ---------------------------- reals/reals.v | 2 +- theories/showcase/sorgenfreyline.v | 89 +- 6 files changed, 73 insertions(+), 1664 deletions(-) delete mode 100644 reals/interval_inference.v diff --git a/_CoqProject b/_CoqProject index 5dd4d0233..a324ce03e 100644 --- a/_CoqProject +++ b/_CoqProject @@ -30,7 +30,6 @@ reals/constructive_ereal.v reals/reals.v reals/real_interval.v reals/signed.v -reals/interval_inference.v reals/prodnormedzmodule.v reals/all_reals.v experimental_reals/xfinmap.v diff --git a/experimental_reals/discrete.v b/experimental_reals/discrete.v index 63ca0e73b..412877a07 100644 --- a/experimental_reals/discrete.v +++ b/experimental_reals/discrete.v @@ -4,7 +4,7 @@ (* Copyright (c) - 2016--2018 - Polytechnique *) (* -------------------------------------------------------------------- *) -From Corelib Require Setoid. +From Coq Require Setoid. From HB Require Import structures. From mathcomp Require Import all_ssreflect all_algebra. From mathcomp.classical Require Import boolp. diff --git a/reals/all_reals.v b/reals/all_reals.v index 38290e673..928723a8a 100644 --- a/reals/all_reals.v +++ b/reals/all_reals.v @@ -1,4 +1,3 @@ -From mathcomp Require Export interval_inference. From mathcomp Require Export constructive_ereal. From mathcomp Require Export reals. From mathcomp Require Export real_interval. diff --git a/reals/interval_inference.v b/reals/interval_inference.v deleted file mode 100644 index d3be1c30e..000000000 --- a/reals/interval_inference.v +++ /dev/null @@ -1,1642 +0,0 @@ -(* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C. *) -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. - -(* N.B.: This file has been backported in mathcomp-algebra 2.4.0, when -performing changes here, be careful to keep both files reasonnably in -sync during the transition period before we can remove the current -file (i.e. the day we'll require mathcomp >= 2.4.0). *) - -(**md**************************************************************************) -(* # Numbers within an interval *) -(* *) -(* This file develops tools to make the manipulation of numbers within *) -(* 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 *) -(* %: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 *) -(* *) -(* ``` *) -(* {itv R & i} == generic type of values in interval i : interval int *) -(* See interval.v for notations that can be used for i. *) -(* R must have a numDomainType structure. This type is shown *) -(* to be a porderType. *) -(* {i01 R} := {itv R & `[0, 1]} *) -(* Allows to solve automatically goals of the form x >= 0 *) -(* and x <= 1 when x is canonically a {i01 R}. *) -(* {i01 R} is canonically stable by common operations. *) -(* {posnum R} := {itv R & `]0, +oo[) *) -(* {nonneg R} := {itv R & `[0, +oo[) *) -(* ``` *) -(* *) -(* ## casts from/to values within known interval *) -(* *) -(* Explicit casts of x to some {itv R & i} according to existing canonical *) -(* instances: *) -(* ``` *) -(* x%:itv == cast to the most precisely known {itv R & i} *) -(* x%:i01 == cast to {i01 R}, or fail *) -(* x%:pos == cast to {posnum R}, or fail *) -(* x%:nng == cast to {nonneg R}, or fail *) -(* ``` *) -(* *) -(* Explicit casts of x from some {itv R & i} to R: *) -(* ``` *) -(* x%:num == cast from {itv R & i} *) -(* x%:posnum == cast from {posnum R} *) -(* x%:nngnum == cast from {nonneg R} *) -(* ``` *) -(* *) -(* ## sign proofs *) -(* *) -(* ``` *) -(* [itv of x] == proof that x is in the 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 *) -(* *) -(* ``` *) -(* ItvNum xr lx xu == builds a {itv R & i} from proofs xr : x \in Num.real, *) -(* lx : map_itv_bound (Itv.num_sem R) l <= BLeft x *) -(* xu : BRight x <= 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 : map_itv_bound (Itv.num_sem R) l <= BLeft x *) -(* xu : BRight x <= 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 *) -(* 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 *) -(* 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 top_typ *) -(* below for an example on how to add your favorite type. *) -(* *) -(******************************************************************************) - -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. -Unset Printing Implicit Defensive. -Import Order.TTheory Order.Syntax. -Import GRing.Theory Num.Theory. - -Local Open Scope ring_scope. -Local Open Scope order_scope. - -Definition map_itv_bound S T (f : S -> T) (b : itv_bound S) : itv_bound T := - match b with - | BSide b x => BSide b (f x) - | BInfty b => BInfty _ b - end. - -Lemma map_itv_bound_comp S T U (f : T -> S) (g : U -> T) (b : itv_bound U) : - map_itv_bound (f \o g) b = map_itv_bound f (map_itv_bound g b). -Proof. by case: b. Qed. - -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 map_itv_comp S T U (f : T -> S) (g : U -> T) (i : interval U) : - map_itv (f \o g) i = map_itv f (map_itv g i). -Proof. by case: i => l u /=; rewrite -!map_itv_bound_comp. Qed. - -(* First, the interval arithmetic operations we will later use *) -Module IntItv. -Implicit Types (b : itv_bound int) (i j : interval int). - -Definition opp_bound b := - match b with - | BSide b x => BSide (~~ b) (intZmod.oppz x) - | BInfty b => BInfty _ (~~ b) - end. - -Lemma opp_bound_ge0 b : (BLeft 0%R <= opp_bound b)%O = (b <= BRight 0%R)%O. -Proof. by case: b => [[] b | []//]; rewrite /= !bnd_simp oppr_ge0. Qed. - -Lemma opp_bound_gt0 b : (BRight 0%R <= opp_bound b)%O = (b <= BLeft 0%R)%O. -Proof. -by case: b => [[] b | []//]; rewrite /= !bnd_simp ?oppr_ge0 ?oppr_gt0. -Qed. - -Definition opp i := - let: Interval l u := i in Interval (opp_bound u) (opp_bound l). -Arguments opp /. - -Definition add_boundl b1 b2 := - match b1, b2 with - | BSide b1 x1, BSide b2 x2 => BSide (b1 && b2) (intZmod.addz x1 x2) - | _, _ => BInfty _ true - end. - -Definition add_boundr b1 b2 := - match b1, b2 with - | BSide b1 x1, BSide b2 x2 => BSide (b1 || b2) (intZmod.addz x1 x2) - | _, _ => BInfty _ false - end. - -Definition add i1 i2 := - let: Interval l1 u1 := i1 in let: Interval l2 u2 := i2 in - Interval (add_boundl l1 l2) (add_boundr u1 u2). -Arguments add /. - -Variant signb := EqZero | NonNeg | NonPos. - -Definition sign_boundl b := - let: b0 := BLeft 0%Z in - if b == b0 then EqZero else if (b <= b0)%O then NonPos else NonNeg. - -Definition sign_boundr b := - 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 sign i : signi := - let: Interval l u := i in - match sign_boundl l, sign_boundr 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. - -Definition mul_boundl b1 b2 := - match b1, b2 with - | BInfty _, _ - | _, BInfty _ - | BLeft 0%Z, _ - | _, BLeft 0%Z => BLeft 0%Z - | BSide b1 x1, BSide b2 x2 => BSide (b1 && b2) (intRing.mulz x1 x2) - end. - -Definition mul_boundr b1 b2 := - match b1, b2 with - | 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 _, _ => +oo%O - end. - -Lemma mul_boundrC b1 b2 : mul_boundr b1 b2 = mul_boundr b2 b1. -Proof. -by move: b1 b2 => [[] [[|?]|?] | []] [[] [[|?]|?] | []] //=; rewrite mulnC. -Qed. - -Lemma mul_boundr_gt0 b1 b2 : - (BRight 0%Z <= b1 -> BRight 0%Z <= b2 -> BRight 0%Z <= mul_boundr 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. - -Definition mul i1 i2 := - let: Interval l1 u1 := i1 in let: Interval l2 u2 := i2 in - let: opp := opp_bound in - let: mull := mul_boundl in let: mulr := mul_boundr in - match sign i1, sign i2 with - | 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 /. - -Definition min i j := - let: Interval li ui := i in let: Interval lj uj := j in - Interval (Order.min li lj) (Order.min ui uj). -Arguments min /. - -Definition max i j := - let: Interval li ui := i in let: Interval lj uj := j in - Interval (Order.max li lj) (Order.max ui uj). -Arguments max /. - -Definition keep_nonneg_bound b := - match b with - | BSide _ (Posz _) => BLeft 0%Z - | BSide _ (Negz _) => -oo%O - | BInfty _ => -oo%O - end. -Arguments keep_nonneg_bound /. - -Definition keep_pos_bound b := - match b with - | BSide b 0%Z => BSide b 0%Z - | BSide _ (Posz (S _)) => BRight 0%Z - | BSide _ (Negz _) => -oo - | BInfty _ => -oo - end. -Arguments keep_pos_bound /. - -Definition keep_nonpos_bound b := - match b with - | BSide _ (Negz _) | BSide _ (Posz 0) => BRight 0%Z - | BSide _ (Posz (S _)) => +oo%O - | BInfty _ => +oo%O - end. -Arguments keep_nonpos_bound /. - -Definition keep_neg_bound b := - match b with - | BSide b 0%Z => BSide b 0%Z - | BSide _ (Negz _) => BLeft 0%Z - | BSide _ (Posz _) => +oo - | BInfty _ => +oo - end. -Arguments keep_neg_bound /. - -Definition inv i := - let: Interval l u := i in - Interval (keep_pos_bound l) (keep_neg_bound u). -Arguments inv /. - -Definition exprn_le1_bound b1 b2 := - if b2 isn't BSide _ 1%Z then +oo - else if (BLeft (-1)%Z <= b1)%O then BRight 1%Z else +oo. -Arguments exprn_le1_bound /. - -Definition exprn i := - let: Interval l u := i in - Interval (keep_pos_bound l) (exprn_le1_bound l u). -Arguments exprn /. - -Definition exprz i1 i2 := - let: Interval l2 _ := i2 in - if l2 is BSide _ (Posz _) then exprn i1 else - let: Interval l u := i1 in - Interval (keep_pos_bound l) +oo. -Arguments exprz /. - -Definition keep_sign i := - let: Interval l u := i in - Interval (keep_nonneg_bound l) (keep_nonpos_bound u). - -(* used in ereal.v *) -Definition keep_nonpos i := - let 'Interval l u := i in - Interval -oo%O (keep_nonpos_bound u). -Arguments keep_nonpos /. - -(* used in ereal.v *) -Definition keep_nonneg i := - let 'Interval l u := i in - Interval (keep_nonneg_bound l) +oo%O. -Arguments keep_nonneg /. - -End IntItv. - -Module Itv. - -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. - -Section Itv. -Context T (sem : interval int -> T -> bool). - -Definition spec (i : t) (x : T) := if i is Real i then sem i x else true. - -Record def (i : t) := Def { - r : T; - #[canonical=no] - P : spec i r -}. - -End Itv. - -Record typ i := Typ { - sort : Type; - #[canonical=no] - sort_sem : interval int -> sort -> bool; - #[canonical=no] - allP : forall x : sort, spec sort_sem i x -}. - -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 num_sem (R : numDomainType) (i : interval int) (x : R) : bool := - (x \in Num.real) && (x \in map_itv intr i). - -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[). - -(* a few lifting helper functions *) -Definition real1 (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 real2 (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 spec_real1 T f (op1 : T -> T) (op1i : interval int -> interval int) : - forall (x : T), (forall xi, f xi x = true -> f (op1i xi) (op1 x) = true) -> - forall xi, spec f xi x -> spec f (real1 op1i xi) (op1 x). -Proof. by move=> x + [//| xi]; apply. Qed. - -Lemma spec_real2 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, spec f xi x -> spec f yi y -> - spec f (real2 op2i xi yi) (op2 x y). -Proof. by move=> + [//| xi] [//| yi]; apply. Qed. - -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 _ _ (Real `]0%Z, +oo[) x) : ring_scope. -Notation "x %:nngnum" := (@r _ _ (Real `[0%Z, +oo[) x) : ring_scope. -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 := (@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. -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. - -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. - -Module TypInstances. - -Lemma top_typ_spec T f (x : T) : Itv.spec f Itv.Top x. -Proof. by []. Qed. - -Canonical top_typ T f := Itv.Typ (@top_typ_spec T f). - -Lemma real_domain_typ_spec (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_spec R). - -Lemma real_field_typ_spec (R : realFieldType) (x : R) : - num_spec (Itv.Real `]-oo, +oo[) x. -Proof. exact: real_domain_typ_spec. Qed. - -Canonical real_field_typ (R : realFieldType) := - Itv.Typ (@real_field_typ_spec R). - -Lemma nat_typ_spec (x : nat) : nat_spec (Itv.Real `[0, +oo[) x. -Proof. by []. Qed. - -Canonical nat_typ := Itv.Typ nat_typ_spec. - -Lemma typ_inum_spec (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 ) - to canonical projections (c.f., Print Canonical Projections - 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 (i : Itv.t) (xt : Itv.typ i) (x : Itv.sort xt) := - Itv.mk (typ_inum_spec x). - -End TypInstances. -Export (canonicals) TypInstances. - -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. - -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. - -Section NumDomainTheory. -Context {R : numDomainType} {i : Itv.t}. -Implicit Type x : num_def R i. - -Lemma le_num_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. - -Lemma num_itv_bound_le_BLeft (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]/(map_itv_bound intr (BLeft y)). -by rewrite le_num_itv_bound. -Qed. - -Lemma BRight_le_num_itv_bound (x : int) (y : itv_bound int) : - (BRight (x%:~R : R) <= num_itv_bound R y)%O = (BRight x <= y)%O. -Proof. -rewrite -[BRight x%:~R]/(map_itv_bound intr (BRight x)). -by rewrite le_num_itv_bound. -Qed. - -Lemma num_spec_sub (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 le_num_itv_bound. -- by apply: le_trans zux _; rewrite le_num_itv_bound. -Qed. - -Definition empty_itv := Itv.Real `[1, 0]%Z. - -Lemma bottom x : ~ unify_itv i empty_itv. -Proof. -case: x => x /= /[swap] /num_spec_sub /[apply] /andP[_] /=. -by rewrite in_itv/= => /andP[] /le_trans /[apply]; rewrite ler10. -Qed. - -Lemma gt0 x : unify_itv i (Itv.Real `]0%Z, +oo[) -> 0 < x%:num :> R. -Proof. -case: x => x /= /[swap] /num_spec_sub /[apply] /andP[_]. -by rewrite /= in_itv/= andbT. -Qed. - -Lemma le0F x : unify_itv i (Itv.Real `]0%Z, +oo[) -> x%:num <= 0 :> R = false. -Proof. -case: x => x /= /[swap] /num_spec_sub /[apply] /andP[_] /=. -by rewrite in_itv/= andbT => /lt_geF. -Qed. - -Lemma lt0 x : unify_itv i (Itv.Real `]-oo, 0%Z[) -> x%:num < 0 :> R. -Proof. -by case: x => x /= /[swap] /num_spec_sub /[apply] /andP[_] /=; rewrite in_itv. -Qed. - -Lemma ge0F x : unify_itv i (Itv.Real `]-oo, 0%Z[) -> 0 <= x%:num :> R = false. -Proof. -case: x => x /= /[swap] /num_spec_sub /[apply] /andP[_] /=. -by rewrite in_itv/= => /lt_geF. -Qed. - -Lemma ge0 x : unify_itv i (Itv.Real `[0%Z, +oo[) -> 0 <= x%:num :> R. -Proof. -case: x => x /= /[swap] /num_spec_sub /[apply] /andP[_] /=. -by rewrite in_itv/= andbT. -Qed. - -Lemma lt0F x : unify_itv i (Itv.Real `[0%Z, +oo[) -> x%:num < 0 :> R = false. -Proof. -case: x => x /= /[swap] /num_spec_sub /[apply] /andP[_] /=. -by rewrite in_itv/= andbT => /le_gtF. -Qed. - -Lemma le0 x : unify_itv i (Itv.Real `]-oo, 0%Z]) -> x%:num <= 0 :> R. -Proof. -by case: x => x /= /[swap] /num_spec_sub /[apply] /andP[_] /=; rewrite in_itv. -Qed. - -Lemma gt0F x : unify_itv i (Itv.Real `]-oo, 0%Z]) -> 0 < x%:num :> R = false. -Proof. -case: x => x /= /[swap] /num_spec_sub /[apply] /andP[_] /=. -by rewrite in_itv/= => /le_gtF. -Qed. - -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 => ~~ Itv.sub ix iy) (Itv.Real `[0%Z, 0%Z]) i -> - 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. -- by case: l l0 => [[] l /= |//]; rewrite !bnd_simp ?lerz0 ?ltrz0. -- by case: u u0 => [[] u /= |//]; rewrite !bnd_simp ?ler0z ?ltr0z. -Qed. - -Lemma eq0F x : - unify (fun ix iy => ~~ Itv.sub ix iy) (Itv.Real `[0%Z, 0%Z]) i -> - x%:num == 0 :> R = false. -Proof. by move=> u; apply/negbTE/neq0. Qed. - -Lemma lt1 x : unify_itv i (Itv.Real `]-oo, 1%Z[) -> x%:num < 1 :> R. -Proof. -by case: x => x /= /[swap] /num_spec_sub /[apply] /andP[_] /=; rewrite in_itv. -Qed. - -Lemma ge1F x : unify_itv i (Itv.Real `]-oo, 1%Z[) -> 1 <= x%:num :> R = false. -Proof. -case: x => x /= /[swap] /num_spec_sub /[apply] /andP[_] /=. -by rewrite in_itv/= => /lt_geF. -Qed. - -Lemma le1 x : unify_itv i (Itv.Real `]-oo, 1%Z]) -> x%:num <= 1 :> R. -Proof. -by case: x => x /= /[swap] /num_spec_sub /[apply] /andP[_] /=; rewrite in_itv. -Qed. - -Lemma gt1F x : unify_itv i (Itv.Real `]-oo, 1%Z]) -> 1 < x%:num :> R = false. -Proof. -case: x => x /= /[swap] /num_spec_sub /[apply] /andP[_] /=. -by rewrite in_itv/= => /le_gtF. -Qed. - -Lemma widen_itv_subproof x i' : Itv.sub i i' -> num_spec i' x%:num. -Proof. by case: x => x /= /[swap] /num_spec_sub; 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. - -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} _ {_}. -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} _ {_}. -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. -#[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)) (Itv.Real `[0, 1]%Z) _) - (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 `]0%Z, +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 `[0%Z, +oo[) _) - (only printing) : ring_scope. - -Local Open Scope ring_scope. - -Module Instances. - -Import IntItv. - -Section NumDomainInstances. -Context {R : numDomainType}. - -Lemma num_spec_zero : 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 num_spec_zero. - -Lemma num_spec_one : 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 num_spec_one. - -Lemma opp_boundr (x : R) b : - (BRight (- x)%R <= num_itv_bound R (opp_bound b))%O - = (num_itv_bound R b <= BLeft x)%O. -Proof. -by case: b => [[] b | []//]; rewrite /= !bnd_simp mulrNz ?lerN2 // ltrN2. -Qed. - -Lemma opp_boundl (x : R) b : - (num_itv_bound R (opp_bound 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. - -Lemma num_spec_opp (i : Itv.t) (x : num_def R i) (r := Itv.real1 opp i) : - num_spec r (- x%:num). -Proof. -apply: Itv.spec_real1 (Itv.P x). -case: x => x /= _ [l u] /and3P[xr lx xu]. -rewrite /Itv.num_sem/= realN xr/=; apply/andP. -by rewrite opp_boundl opp_boundr. -Qed. - -Canonical opp_inum (i : Itv.t) (x : num_def R i) := Itv.mk (num_spec_opp x). - -Lemma num_itv_add_boundl (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_boundl 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. - -Lemma num_itv_add_boundr (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_boundr 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. - -Lemma num_spec_add (xi yi : Itv.t) (x : num_def R xi) (y : num_def R yi) - (r := Itv.real2 add xi yi) : - num_spec r (x%:num + y%:num). -Proof. -apply: Itv.spec_real2 (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 num_itv_add_boundl ?num_itv_add_boundr. -Qed. - -Canonical add_inum (xi yi : Itv.t) (x : num_def R xi) (y : num_def R yi) := - Itv.mk (num_spec_add x y). - -Variant sign_spec (l u : itv_bound int) (x : R) : signi -> Set := - | ISignEqZero : l = BLeft 0 -> u = BRight 0 -> x = 0 -> - sign_spec l u x (Known EqZero) - | ISignNonNeg : (BLeft 0%:Z <= l)%O -> (BRight 0%:Z < u)%O -> 0 <= x -> - sign_spec l u x (Known NonNeg) - | ISignNonPos : (l < BLeft 0%:Z)%O -> (u <= BRight 0%:Z)%O -> x <= 0 -> - sign_spec l u x (Known NonPos) - | ISignBoth : (l < BLeft 0%:Z)%O -> (BRight 0%:Z < u)%O -> x \in Num.real -> - sign_spec l u x Unknown. - -Lemma 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 -> - sign_spec l u x (sign (Interval l u)). -Proof. -move=> + + xr; rewrite /sign/sign_boundl/sign_boundr. -have [lneg|lpos|->] := ltgtP l; have [uneg|upos|->] := ltgtP u => lx xu. -- apply: ISignNonPos => //; first exact: ltW. - have:= le_trans xu (eqbRL (le_num_itv_bound _ _) (ltW uneg)). - by rewrite bnd_simp. -- exact: ISignBoth. -- exact: ISignNonPos. -- have:= @ltxx _ _ (num_itv_bound R l). - rewrite (le_lt_trans lx) -?leBRight_ltBLeft ?(le_trans xu)//. - by rewrite le_num_itv_bound (le_trans (ltW uneg)). -- apply: ISignNonNeg => //; first exact: ltW. - have:= le_trans (eqbRL (le_num_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 le_num_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 le_num_itv_bound -?ltBRight_leBLeft. -- exact: ISignNonNeg. -- apply: ISignEqZero => //. - by apply/le_anti/andP; move: lx xu; rewrite !bnd_simp. -Qed. - -Lemma num_itv_mul_boundl b1 b2 (x1 x2 : R) : - (BLeft 0%:Z <= b1 -> BLeft 0%:Z <= b2 -> - num_itv_bound R b1 <= BLeft x1 -> - num_itv_bound R b2 <= BLeft x2 -> - num_itv_bound R (mul_boundl 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. - 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 num_itv_mul_boundr b1 b2 (x1 x2 : R) : - (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_boundr 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 BRight_le_mul_boundr b1 b2 (x1 x2 : R) : - (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_boundr b1 b2))%O. -Proof. -move=> x1ge0 x2r b2ge0 lex1b1 lex2b2. -have /orP[x2ge0 | x2le0] := x2r; first exact: num_itv_mul_boundr. -have lem0 : (BRight (x1 * x2) <= BRight 0%R)%O. - by rewrite bnd_simp mulr_ge0_le0 // ltW. -apply: le_trans lem0 _. -rewrite -(mulr0z 1) BRight_le_num_itv_bound. -apply: mul_boundr_gt0 => //. -by rewrite -(@BRight_le_num_itv_bound R) (le_trans _ lex1b1). -Qed. - -Lemma comparable_num_itv_bound (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 num_itv_bound_min (x y : itv_bound int) : - 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; [by rewrite !minEle le_num_itv_bound lexy|]. -rewrite minElt -if_neg -comparable_leNgt ?le_num_itv_bound ?ltW//. -exact: comparable_num_itv_bound. -Qed. - -Lemma num_itv_bound_max (x y : itv_bound int) : - 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 le_num_itv_bound lexy|]. -rewrite maxElt -if_neg -comparable_leNgt ?le_num_itv_bound ?ltW//. -exact: comparable_num_itv_bound. -Qed. - -Lemma num_spec_mul (xi yi : Itv.t) (x : num_def R xi) (y : num_def R yi) - (r := Itv.real2 mul xi yi) : - 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]]. -rewrite -/(sign (Interval xl xu)) -/(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: (signP xlx xxu xr) => xlb xub xs. -- by rewrite xs mul0r; case: (signP yly yyu yr). -- case: (signP yly yyu yr) => ylb yub ys. - + by rewrite ys mulr0. - + apply/and3P; split=> //=. - * exact: num_itv_mul_boundl xlx yly. - * exact: num_itv_mul_boundr xxu yyu. - + apply/and3P; split=> //=; rewrite -[x * y]opprK -mulrN. - * by rewrite opp_boundl num_itv_mul_boundr ?oppr_ge0// opp_boundr. - * by rewrite opp_boundr num_itv_mul_boundl ?opp_boundl// opp_bound_ge0. - + apply/and3P; split=> //=. - * rewrite -[x * y]opprK -mulrN opp_boundl. - by rewrite BRight_le_mul_boundr ?realN ?opp_boundr// opp_bound_gt0 ltW. - * by rewrite BRight_le_mul_boundr// ltW. -- case: (signP yly yyu yr) => ylb yub ys. - + by rewrite ys mulr0. - + apply/and3P; split=> //=; rewrite -[x * y]opprK -mulNr. - * rewrite opp_boundl. - by rewrite num_itv_mul_boundr ?oppr_ge0 ?opp_boundr. - * by rewrite opp_boundr num_itv_mul_boundl ?opp_boundl// opp_bound_ge0. - + apply/and3P; split=> //=; rewrite -mulrNN. - * by rewrite num_itv_mul_boundl ?opp_bound_ge0 ?opp_boundl. - * by rewrite num_itv_mul_boundr ?oppr_ge0 ?opp_boundr. - + apply/and3P; split=> //=; rewrite -[x * y]opprK. - * rewrite -mulNr opp_boundl BRight_le_mul_boundr ?oppr_ge0 ?opp_boundr//. - exact: ltW. - * rewrite opprK -mulrNN. - by rewrite BRight_le_mul_boundr ?opp_boundr - ?oppr_ge0 ?realN ?opp_bound_gt0// ltW. -- case: (signP yly yyu yr) => ylb yub ys. - + by rewrite ys mulr0. - + apply/and3P; split=> //=; rewrite mulrC mul_boundrC. - * rewrite -[y * x]opprK -mulrN opp_boundl. - rewrite BRight_le_mul_boundr ?oppr_ge0 ?realN ?opp_boundr//. - by rewrite opp_bound_gt0 ltW. - * by rewrite BRight_le_mul_boundr// ltW. - + apply/and3P; split=> //=; rewrite mulrC mul_boundrC. - * rewrite -[y * x]opprK -mulNr opp_boundl. - by rewrite BRight_le_mul_boundr ?oppr_ge0 ?opp_boundr// ltW. - * rewrite -mulrNN BRight_le_mul_boundr ?oppr_ge0 ?realN ?opp_boundr//. - by rewrite opp_bound_gt0 ltW. -apply/and3P; rewrite xyr/= num_itv_bound_min num_itv_bound_max. -rewrite (comparable_ge_min _ (comparable_num_itv_bound _ _)). -rewrite (comparable_le_max _ (comparable_num_itv_bound _ _)). -case: (comparable_leP xr) => [x0 | /ltW x0]; split=> //. -- apply/orP; right; rewrite -[x * y]opprK -mulrN opp_boundl. - by rewrite BRight_le_mul_boundr ?realN ?opp_boundr// opp_bound_gt0 ltW. -- by apply/orP; right; rewrite BRight_le_mul_boundr// ltW. -- apply/orP; left; rewrite -[x * y]opprK -mulNr opp_boundl. - by rewrite BRight_le_mul_boundr ?oppr_ge0 ?opp_boundr// ltW. -- apply/orP; left; rewrite -mulrNN. - rewrite BRight_le_mul_boundr ?oppr_ge0 ?realN ?opp_boundr//. - by rewrite opp_bound_gt0 ltW. -Qed. - -Canonical mul_inum (xi yi : Itv.t) (x : num_def R xi) (y : num_def R yi) := - Itv.mk (num_spec_mul x y). - -Lemma num_spec_min (xi yi : Itv.t) (x : num_def R xi) (y : num_def R yi) - (r := Itv.real2 min xi yi) : - num_spec r (Order.min x%:num y%:num). -Proof. -apply: Itv.spec_real2 (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//= num_itv_bound_min real_BSide_min//. -- apply: (comparable_le_min2 (comparable_num_itv_bound _ _)) => //. - exact: real_comparable. -- apply: (comparable_le_min2 _ (comparable_num_itv_bound _ _)) => //. - exact: real_comparable. -Qed. - -Lemma num_spec_max (xi yi : Itv.t) (x : num_def R xi) (y : num_def R yi) - (r := Itv.real2 max xi yi) : - num_spec r (Order.max x%:num y%:num). -Proof. -apply: Itv.spec_real2 (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//= num_itv_bound_max real_BSide_max//. -- apply: (comparable_le_max2 (comparable_num_itv_bound _ _)) => //. - exact: real_comparable. -- apply: (comparable_le_max2 _ (comparable_num_itv_bound _ _)) => //. - 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 min 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 max 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 min 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 min xi yi) := - Itv.mk (min_max_maxP x y). - -(* Instance of the above structure for numDomainType *) -Canonical num_min_max_typ := MinMaxTyp num_spec_min num_spec_max. - -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. - -Definition natmul_itv (i1 i2 : Itv.t) : Itv.t := - match i1, i2 with - | Itv.Top, _ => Itv.Top - | _, Itv.Top => Itv.Real `]-oo, +oo[ - | Itv.Real i1, Itv.Real i2 => Itv.Real (mul i1 i2) - end. -Arguments natmul_itv /. - -Lemma num_spec_natmul (xi ni : Itv.t) (x : num_def R xi) (n : nat_def ni) - (r := natmul_itv xi ni) : - num_spec r (x%:num *+ n%:num). -Proof. -rewrite {}/r; case: xi x ni n => [//| xi] x [| ni] n. - by apply/and3P; case: n%:num => [|?]; rewrite ?mulr0n ?realrMn. -have Pn : num_spec (Itv.Real ni) (n%:num%:R : R). - by case: n => /= n; rewrite [Itv.nat_sem ni n](nat_num_spec (Itv.Real ni)). -rewrite -mulr_natr -[n%:num%:R]/((Itv.Def Pn)%:num). -by rewrite (@num_spec_mul (Itv.Real xi) (Itv.Real ni)). -Qed. - -Canonical natmul_inum (xi ni : Itv.t) (x : num_def R xi) (n : nat_def ni) := - Itv.mk (num_spec_natmul x n). - -Lemma num_spec_int (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 num_spec_intmul (xi ii : Itv.t) (x : num_def R xi) (i : num_def int ii) - (r := natmul_itv xi ii) : - num_spec r (x%:num *~ i%:num). -Proof. -rewrite {}/r; case: xi x ii i => [//| xi] x [| ii] i. - by apply/and3P; case: i%:inum => [[|n] | n]; rewrite ?mulr0z ?realN ?realrMn. -have Pi : num_spec (Itv.Real ii) (i%:num%:~R : R). - by case: i => /= i; rewrite [Itv.num_sem ii i](num_spec_int (Itv.Real ii)). -rewrite -mulrzr -[i%:num%:~R]/((Itv.Def Pi)%:num). -by rewrite (@num_spec_mul (Itv.Real xi) (Itv.Real ii)). -Qed. - -Canonical intmul_inum (xi ni : Itv.t) (x : num_def R xi) (n : num_def int ni) := - Itv.mk (num_spec_intmul x n). - -Lemma num_itv_bound_keep_pos (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_bound 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. - -Lemma num_itv_bound_keep_neg (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_bound 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. - -Lemma num_spec_inv (i : Itv.t) (x : num_def R i) (r := Itv.real1 inv i) : - num_spec r (x%:num^-1). -Proof. -apply: Itv.spec_real1 (Itv.P x). -case: x => x /= _ [l u] /and3P[xr /= lx xu]. -rewrite /Itv.num_sem/= realV xr/=; apply/andP; split. -- apply: num_itv_bound_keep_pos lx. - + by move=> ?; rewrite invr_ge0. - + by move=> ?; rewrite invr_gt0. -- apply: num_itv_bound_keep_neg 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 (num_spec_inv x). - -Lemma num_itv_bound_exprn_le1 (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_bound l u))%O. -Proof. -case: u => [bu [[//|[|//]] |//] | []//]. -rewrite /exprn_le1_bound; case: (leP _ l) => [lge1 /= |//] lx xu. -rewrite bnd_simp; case: n => [| n]; rewrite ?expr0//. -have xN1 : -1 <= x. - case: l lge1 lx => [[] l | []//]; rewrite !bnd_simp -(@ler_int R). - - exact: le_trans. - - by move=> + /ltW; apply: le_trans. -have x1 : x <= 1 by case: bu xu; rewrite bnd_simp// => /ltW. -have xr : x \is Num.real by exact: ler1_real. -case: (real_ge0P xr) => x0; first by rewrite expr_le1. -rewrite -[x]opprK exprNn; apply: le_trans (ler_piMl _ _) _. -- by rewrite exprn_ge0 ?oppr_ge0 1?ltW. -- suff: -1 <= (-1) ^+ n.+1 :> R /\ (-1) ^+ n.+1 <= 1 :> R => [[]//|]. - elim: n => [|n [IHn1 IHn2]]; rewrite ?expr1// ![_ ^+ n.+2]exprS !mulN1r. - by rewrite lerNl opprK lerNl. -- by rewrite expr_le1 ?oppr_ge0 1?lerNl// ltW. -Qed. - -Lemma num_spec_exprn (i : Itv.t) (x : num_def R i) n (r := Itv.real1 exprn i) : - num_spec r (x%:num ^+ n). -Proof. -apply: (@Itv.spec_real1 _ _ (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: (@num_itv_bound_keep_pos (fun x => x^+n)) lx. - + exact: exprn_ge0. - + exact: exprn_gt0. -- exact: num_itv_bound_exprn_le1 lx xu. -Qed. - -Canonical exprn_inum (i : Itv.t) (x : num_def R i) n := - Itv.mk (num_spec_exprn x n). - -Lemma num_spec_exprz (xi ki : Itv.t) (x : num_def R xi) (k : num_def int ki) - (r := Itv.real2 exprz xi ki) : - num_spec r (x%:num ^ k%:num). -Proof. -rewrite {}/r; case: ki k => [|[lk uk]] k; first by case: xi x. -case: xi x => [//|xi x]; rewrite /Itv.real2. -have P : Itv.num_sem - (let 'Interval l _ := xi in Interval (keep_pos_bound l) +oo) - (x%:num ^ k%:num). - case: xi x => lx ux x; apply/and3P; split=> [||//]. - have xr : x%:num \is Num.real by case: x => x /=/andP[]. - by case: k%:num => n; rewrite ?realV realX. - apply: (@num_itv_bound_keep_pos (fun x => x ^ k%:num)); - [exact: exprz_ge0 | exact: exprz_gt0 |]. - by case: x => x /=/and3P[]. -case: lk k P => [slk [lk | lk] | slk] k P; [|exact: P..]. -case: k P => -[k | k] /= => [_ _|]; rewrite -/(exprn xi); last first. - by move=> /and3P[_ /=]; case: slk; rewrite bnd_simp -pmulrn natz. -exact: (@num_spec_exprn (Itv.Real xi)). -Qed. - -Canonical exprz_inum (xi ki : Itv.t) (x : num_def R xi) (k : num_def int ki) := - Itv.mk (num_spec_exprz x k). - -Lemma num_spec_norm {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 (num_spec_norm x). - -End NumDomainInstances. - -Section RcfInstances. -Context {R : rcfType}. - -Definition sqrt_itv (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 0%Z => 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 /. - -Lemma num_spec_sqrt (i : Itv.t) (x : num_def R i) (r := sqrt_itv 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 (num_spec_sqrt x). - -End RcfInstances. - -Section NumClosedFieldInstances. -Context {R : numClosedFieldType}. - -Definition sqrtC_itv (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 /. - -Lemma num_spec_sqrtC (i : Itv.t) (x : num_def R i) (r := sqrtC_itv 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: sqrtC_real; 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 (num_spec_sqrtC x). - -End NumClosedFieldInstances. - -Section NatInstances. -Local Open Scope nat_scope. -Implicit Type (n : nat). - -Lemma nat_spec_zero : nat_spec (Itv.Real `[0, 0]%Z) 0. Proof. by []. Qed. - -Canonical zeron_inum := Itv.mk nat_spec_zero. - -Lemma nat_spec_add (xi yi : Itv.t) (x : nat_def xi) (y : nat_def yi) - (r := Itv.real2 add 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: num_spec_add. -Qed. - -Canonical addn_inum (xi yi : Itv.t) (x : nat_def xi) (y : nat_def yi) := - Itv.mk (nat_spec_add x y). - -Lemma nat_spec_succ (i : Itv.t) (n : nat_def i) - (r := Itv.real2 add i (Itv.Real `[1, 1]%Z)) : - nat_spec r (S n%:num). -Proof. -pose i1 := Itv.Real `[1, 1]%Z; have P1 : nat_spec i1 1 by []. -by rewrite -addn1 -[1%N]/((Itv.Def P1)%:num); apply: nat_spec_add. -Qed. - -Canonical succn_inum (i : Itv.t) (n : nat_def i) := Itv.mk (nat_spec_succ n). - -Lemma nat_spec_double (i : Itv.t) (n : nat_def i) (r := Itv.real2 add i i) : - nat_spec r (n%:num.*2). -Proof. by rewrite -addnn nat_spec_add. Qed. - -Canonical double_inum (i : Itv.t) (x : nat_def i) := Itv.mk (nat_spec_double x). - -Lemma nat_spec_mul (xi yi : Itv.t) (x : nat_def xi) (y : nat_def yi) - (r := Itv.real2 mul 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: num_spec_mul. -Qed. - -Canonical muln_inum (xi yi : Itv.t) (x : nat_def xi) (y : nat_def yi) := - Itv.mk (nat_spec_mul x y). - -Lemma nat_spec_exp (i : Itv.t) (x : nat_def i) n (r := Itv.real1 exprn 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: num_spec_exprn. -Qed. - -Canonical expn_inum (i : Itv.t) (x : nat_def i) n := Itv.mk (nat_spec_exp x n). - -Lemma nat_spec_min (xi yi : Itv.t) (x : nat_def xi) (y : nat_def yi) - (r := Itv.real2 min 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_spec_min. -Qed. - -Canonical minn_inum (xi yi : Itv.t) (x : nat_def xi) (y : nat_def yi) := - Itv.mk (nat_spec_min x y). - -Lemma nat_spec_max (xi yi : Itv.t) (x : nat_def xi) (y : nat_def yi) - (r := Itv.real2 max 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_spec_max. -Qed. - -Canonical maxn_inum (xi yi : Itv.t) (x : nat_def xi) (y : nat_def yi) := - Itv.mk (nat_spec_max x y). - -Canonical nat_min_max_typ := MinMaxTyp nat_spec_min nat_spec_max. - -Lemma nat_spec_factorial (n : nat) : nat_spec (Itv.Real `[1%Z, +oo[) n`!. -Proof. by apply/andP; rewrite bnd_simp lez_nat fact_gt0. Qed. - -Canonical factorial_inum n := Itv.mk (nat_spec_factorial n). - -End NatInstances. - -Section IntInstances. - -Lemma num_spec_Posz 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 (num_spec_Posz n). - -Lemma num_spec_Negz 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 (num_spec_Negz n). - -End IntInstances. - -End Instances. -Export (canonicals) Instances. - -Section Morph. -Context {R : numDomainType} {i : Itv.t}. -Local Notation nR := (num_def R i). -Implicit Types x y : nR. -Local Notation num := (@num R (@Itv.num_sem R) i). - -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. - -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)). -Implicit Type x y : nR. -Local Notation num := (@num R (@Itv.num_sem R) i). - -Lemma num_le_max a x y : - 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%: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%: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%: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%: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%: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%: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%:num y%:num < a = (x%:num < a) || (y%:num < a). -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). -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 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. -Variable x : {i01 R}. - -Goal 0%:i01 = 1%:i01 :> {i01 R}. -Proof. -Abort. - -Goal (- x%:num)%:itv = (- x%:num)%:itv :> {itv R & `[-1, 0]}. -Proof. -Abort. - -Goal (1 - x%:num)%:i01 = x. -Proof. -Abort. - -End Test1. - -Section Test2. - -Variable R : realDomainType. -Variable x y : {i01 R}. - -Goal (x%:num * y%:num)%:i01 = x%:num%:i01. -Proof. -Abort. - -End Test2. - -Module Test3. -Section Test3. -Variable R : realDomainType. - -Definition s_of_pq (p q : {i01 R}) : {i01 R} := - (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. - -End Test3. -End Test3. diff --git a/reals/reals.v b/reals/reals.v index a400ee645..3f0ccdaf5 100644 --- a/reals/reals.v +++ b/reals/reals.v @@ -43,7 +43,7 @@ (* *) (******************************************************************************) -From Corelib Require Import Setoid. +From Coq Require Import Setoid. From HB Require Import structures. From mathcomp Require Import all_ssreflect all_algebra archimedean. From mathcomp Require Import boolp classical_sets set_interval. diff --git a/theories/showcase/sorgenfreyline.v b/theories/showcase/sorgenfreyline.v index 4eccada93..5c73af2ac 100644 --- a/theories/showcase/sorgenfreyline.v +++ b/theories/showcase/sorgenfreyline.v @@ -182,8 +182,6 @@ Definition sdist (x : sorgenfrey) : R := From mathcomp Require Import topology normedtype. Let Rtopo := num_topology.numFieldTopology.Real_sort__canonical__topology_structure_Topological R. -From mathcomp Require Import ring. - Lemma abs_subr_min (x y t u : R) : `|Num.min x y - Num.min t u| <= Num.max `|x - t| `|y - u|. Proof. @@ -192,8 +190,7 @@ wlog: x y t u / x <= y. case/boolP: (x <= y) => [/H //| xy]. by rewrite minC (minC t) maxC H // ltW // ltNge. case: (lerP x y) => // xy _. -have cxtyu : `|x-t| >=< `|y-u| by rewrite comparablerE num_real. -case: (lerP t u) => tu; rewrite comparable_le_max //. +case: (lerP t u) => tu; rewrite le_max. by rewrite lexx. case: (lerP x u) => xu. case: (lerP x t) => xt. by rewrite lerD2r ltW. @@ -313,6 +310,13 @@ case/boolP: (xepsE == set0). apply/negP => zE. suff : xepsE (z-x) by rewrite xepsE0. by rewrite /xepsE /= addrA (addrC x) addrK subr_gt0 xz ltrBlDl. + have drzx : dr x = [set t + (z - x) | t in dr z]. + apply: dr_shift => // t /=. + rewrite in_itv /= => /andP[] xt tz. + apply: contraPnot xepsE0. + rewrite -inE => Et; apply/eqP/set0P. + exists (t-x); rewrite /xepsE /= addrA (addrC x) addrK. + by rewrite subr_gt0 xt ltrBlDl (le_lt_trans tz). have Hr : `|Num.min 1 xr - Num.min 1 zr| < eps. rewrite /xr /zr. case: ifPn => drx0. @@ -321,17 +325,29 @@ case/boolP: (xepsE == set0). suff : y + z - x \in dr x by rewrite (eqP drx0) inE. rewrite inE /dr /= addrA (addrC x) addrK addrC Hy. by rewrite subr_gt0 ltr_wpDr // ltW. + have drz0 : dr z !=set0. + case/set0P: drx0 => y [] Hy y0. + exists (y + x - z). + rewrite /dr /= addrA (addrC z) addrK addrC Hy subr_gt0 ltNge. + split => //; apply/negP => xyz. + suff : xepsE y by rewrite xepsE0. + by rewrite /xepsE /= Hy y0 -(ltrD2l x) (le_lt_trans xyz). rewrite ifF. rewrite (le_lt_trans (abs_subr_min _ _ _ _)) //. rewrite subrr normr0 maxEle normr_ge0. - admit. - apply/negbTE/set0P. - case/set0P: drx0 => y [] Hy y0. - exists (y + x - z). - rewrite /dr /= addrA (addrC z) addrK addrC Hy subr_gt0 ltNge. - split => //; apply/negP => xyz. - suff : xepsE y by rewrite xepsE0. - by rewrite /xepsE /= Hy y0 -(ltrD2l x) (le_lt_trans xyz). + rewrite drzx. + rewrite -image2_set1. + rewrite inf_sumE //. + rewrite inf1. + rewrite addrAC. + rewrite subrr add0r. + move/ltW: xz. + rewrite ler_def. + move/eqP ->. + by rewrite ltrBlDl. + split. by []. + exists 0. by move=> y [] _ /ltW. + exact/negbTE/set0P. have dlxz : dl z = [set t + (z - x) | t in dl x]. apply: dl_shift => // t /=. rewrite in_itv /= => /andP[] xt tz. @@ -346,14 +362,40 @@ case/boolP: (xepsE == set0). by rewrite inE /dl /= subr0. by rewrite dlxz dlx0 image_set0 inf0 subr0 (negbTE znE). case/set0P => w Hw. - have <- : x - inf (dl x) = z - inf (dl z). + have inf_dlxz : x - inf (dl x) = z - inf (dl z). rewrite dlxz -image2_set1 inf_sumE. - by rewrite inf1 !opprD !addrA (addrC z) addrK (opprK x) addrC. - split. by exists w. exists 0. move=> u. rewrite -inE. exact: dl_ge0. - exact: has_inf1. + rewrite -inf_dlxz. case: ifPn => xlE //. - rewrite (le_lt_trans (abs_subr_min _ _ _ _)) //. admit. + rewrite (le_lt_trans (abs_subr_min _ _ _ _)) //. + rewrite gt_max ltr_norml. + rewrite -[inf(dl x)]addr0. + rewrite -(subrr (-z)) opprK addrA -[_ - _]addrA -inf_dlxz. + rewrite -!addrA addrC !addrA subrK addrC. + rewrite (@le_lt_trans _ _ 0 (_ - _) ) //; first last. + by rewrite subr_le0 ltW. + rewrite ltrBrDl ltrBlDr zx /=. + rewrite /xr /zr. + rewrite drzx. + have[-> | drz0] := eqVneq (dr z) set0. + by rewrite image_set0 eqxx subrr normr0 eps0. + case:ifPn. + move/eqP /image_set0_set0 /eqP. + by rewrite (negPf drz0). + move=> drx0. + have inf_drxz : inf (dr x) = inf (dr z) + z - x. + rewrite drzx -image2_set1 inf_sumE. + - by rewrite inf1 addrA. + - split. by apply/set0P. + exists 0. move=> u. rewrite -inE. exact: dr_ge0. + - exact: has_inf1. + rewrite -drzx inf_drxz. + rewrite -!addrA addrC !addrA subrK ltr_norml. + rewrite (@lt_le_trans _ _ 0) ?ltrBlDl //= ?subr_ge0 ?ltW //. + by rewrite oppr_lt0. move/set0P/xgetPex => /(_ eps). rewrite -/eps' => -[] eps'E Heps'. rewrite -/(sdist x) -/(sdist z). @@ -367,8 +409,8 @@ have eps'l : forall t, x <= t < x + eps' -> 0 <= sdist t < eps. rewrite /dr /= (addrC _ (-t)) addrA subrr add0r eps'E. rewrite addrC subr_gt0 //; by case/andP: Ht. move=> drt0. - rewrite comparable_le_min; last exact/real_leVge/num_real/num_real. - rewrite comparable_gt_min; last exact/real_leVge/num_real/num_real. + rewrite le_min. + rewrite gt_min. rewrite {1}/xl fun_if inf_ge0 // ler01 if_same /=. rewrite inf_ge0 /=; last by move=> u; rewrite inE => -[] _ /ltW. case/andP: Ht => xt tx. @@ -383,11 +425,11 @@ have Hx : 0 <= sdist x < eps. by apply: eps'l; rewrite lexx ltrDl; case/andP: Heps'. have Hz : 0 <= sdist z < eps. by apply: eps'l; rewrite zx ltW // xz. -rewrite -maxrN comparable_gt_max; last exact/real_leVge/num_real/num_real. +rewrite -maxrN gt_max. case/andP: Hx => Hx1 Hx2. case/andP: Hz => Hz1 Hz2. by rewrite opprB !ltrBlDr !ltr_wpDr. -Admitted. +Qed. Lemma zeroset_sdist : E = sdist @^-1` [set 0]. Proof. @@ -436,4 +478,15 @@ by rewrite in_itv /= xya' (le_trans ax) // ler_wpDr // ltW. Qed. End distance. +Lemma sorgenfrey_line_perfectly_norml_space : + perfectly_normal_space R sorgenfrey. +Proof. +move=> E cE. +exists (sdist E). +split. + exact: continuous_sdist. +exact: zeroset_sdist. +Qed. + + End Sorgenfrey_line. From 4f05afcd47486d3df99c46acbef2cde0cf3cc3fc Mon Sep 17 00:00:00 2001 From: Yosuke Tsuji Date: Wed, 25 Jun 2025 12:12:55 +0900 Subject: [PATCH 16/45] add sorgenfrey epsilon delta --- theories/showcase/sorgenfreyline.v | 60 ++++++++++++++++++------------ 1 file changed, 36 insertions(+), 24 deletions(-) diff --git a/theories/showcase/sorgenfreyline.v b/theories/showcase/sorgenfreyline.v index 5c73af2ac..6e6380878 100644 --- a/theories/showcase/sorgenfreyline.v +++ b/theories/showcase/sorgenfreyline.v @@ -279,27 +279,43 @@ rewrite !addrA addrAC (addrC x) addrK addrC. by rewrite subr_gt0 ltr_wpDr // ltW. Qed. -Lemma continuous_sdist : - forall x, @continuous_at sorgenfrey Rtopo x sdist. +Definition continuous_at_sorgenfrey_to_Rtopo x (f : sorgenfrey -> R) := + forall eps : R, 0 < eps -> exists2 d : R, 0 < d & forall y : R, x <= y < x + d -> `|f x - f y| < eps. + +Lemma continuous_at_sorgenfrey_to_RtopoP f x : + continuous_at_sorgenfrey_to_Rtopo x f -> @continuous_at sorgenfrey Rtopo x f. Proof. -move=> x B. +move=> H B. rewrite -(@filter_from_ballE R (GRing_regular__canonical__pseudometric_structure_PseudoMetric R)). case => eps /= eps0 epsB. -pose xepsE := [set y | x + y \in E /\ 0 < y < eps]. -pose eps' := xget eps xepsE. -exists (`[x,x+eps'[); split => //=. -- exists [set (x,x+eps')] => //. +change (nbhs (f y @[y --> x]) B). +case: (H eps eps0) => /= d d0 H'. +exists (`[x,x+d[); split => //=. +- exists [set (x,x+d)] => //. by rewrite bigcup_set1. -- rewrite in_itv /= lexx ltrDl /eps' /=. - by case: (xgetP eps xepsE) => // y -> [] _ /andP[]. +- by rewrite in_itv /= lexx ltrDl d0. rewrite -image_sub. move=> y /= [] z. rewrite in_itv /= => /andP[xz zx] <- {y}. apply: epsB. -rewrite /ball /sdist /=. +apply: H'. +by rewrite xz zx. +Qed. + +Lemma continuous_sdist : + forall x, @continuous_at sorgenfrey Rtopo x sdist. +Proof. +move=> x. +apply: continuous_at_sorgenfrey_to_RtopoP => /= eps eps0. +pose xepsE := [set y | x + y \in E /\ 0 < y < eps]. +pose eps' := xget eps xepsE. +exists eps'. + by rewrite /eps'; case: (xgetP eps xepsE) => // y -> [] _ /andP[]. +move=> z /andP [] xz zx. have [<-|xz'] := eqVneq x z. by rewrite subrr normr0. have {xz xz'} xz: x < z by rewrite lt_neqAle xz'. +rewrite /sdist. set xr : R := if dr x == set0 then _ else _. set zr : R := if dr z == set0 then _ else _. case/boolP: (xepsE == set0). @@ -319,19 +335,15 @@ case/boolP: (xepsE == set0). by rewrite subr_gt0 xt ltrBlDl (le_lt_trans tz). have Hr : `|Num.min 1 xr - Num.min 1 zr| < eps. rewrite /xr /zr. - case: ifPn => drx0. - suff -> : dr z == set0 by rewrite subrr normr0. - apply/notP => /negP/set0P [] y [] Hy y0. - suff : y + z - x \in dr x by rewrite (eqP drx0) inE. - rewrite inE /dr /= addrA (addrC x) addrK addrC Hy. - by rewrite subr_gt0 ltr_wpDr // ltW. - have drz0 : dr z !=set0. - case/set0P: drx0 => y [] Hy y0. - exists (y + x - z). - rewrite /dr /= addrA (addrC z) addrK addrC Hy subr_gt0 ltNge. - split => //; apply/negP => xyz. - suff : xepsE y by rewrite xepsE0. - by rewrite /xepsE /= Hy y0 -(ltrD2l x) (le_lt_trans xyz). + case/boolP: (dr z == set0) => [/eqP |] drz0. + move: drzx. + rewrite drz0 image_set0 => /eqP ->. + by rewrite subrr normr0. + have drx0 : dr x !=set0. + case/set0P : drz0 => z0 drzz0. + rewrite drzx. + exists (z0 + (z - x)) => /=. + by exists z0. rewrite ifF. rewrite (le_lt_trans (abs_subr_min _ _ _ _)) //. rewrite subrr normr0 maxEle normr_ge0. @@ -345,7 +357,7 @@ case/boolP: (xepsE == set0). rewrite ler_def. move/eqP ->. by rewrite ltrBlDl. - split. by []. + split. exact/set0P. exists 0. by move=> y [] _ /ltW. exact/negbTE/set0P. have dlxz : dl z = [set t + (z - x) | t in dl x]. From 0e840fb8933b4ebec783e3ca20d717f7df49b8dc Mon Sep 17 00:00:00 2001 From: Yosuke Tsuji Date: Wed, 2 Jul 2025 12:19:56 +0900 Subject: [PATCH 17/45] refactor and add inf_dlxz --- theories/showcase/sorgenfreyline.v | 33 +++++++++++++++++++----------- 1 file changed, 21 insertions(+), 12 deletions(-) diff --git a/theories/showcase/sorgenfreyline.v b/theories/showcase/sorgenfreyline.v index 6e6380878..a1f8554d4 100644 --- a/theories/showcase/sorgenfreyline.v +++ b/theories/showcase/sorgenfreyline.v @@ -279,6 +279,19 @@ rewrite !addrA addrAC (addrC x) addrK addrC. by rewrite subr_gt0 ltr_wpDr // ltW. Qed. +Lemma inf_dlxz x z : + dl z = [set t + (z - x) | t in dl x] -> + dl x !=set0 -> + x - inf (dl x) = z - inf (dl z). +Proof. +move=> dlxz dlx0. +rewrite dlxz -image2_set1 inf_sumE. +- by rewrite inf1 !opprD !addrA (addrC z) addrK (opprK x) addrC. +- split => //. + exists 0. move=> u. rewrite -inE. exact: dl_ge0. +- exact: has_inf1. +Qed. + Definition continuous_at_sorgenfrey_to_Rtopo x (f : sorgenfrey -> R) := forall eps : R, 0 < eps -> exists2 d : R, 0 < d & forall y : R, x <= y < x + d -> `|f x - f y| < eps. @@ -311,6 +324,7 @@ pose xepsE := [set y | x + y \in E /\ 0 < y < eps]. pose eps' := xget eps xepsE. exists eps'. by rewrite /eps'; case: (xgetP eps xepsE) => // y -> [] _ /andP[]. +(* forall z : R, x <= z < x + eps' -> `|sdist x - sdist z| < eps *) move=> z /andP [] xz zx. have [<-|xz'] := eqVneq x z. by rewrite subrr normr0. @@ -325,13 +339,14 @@ case/boolP: (xepsE == set0). have znE : z \notin E. apply/negP => zE. suff : xepsE (z-x) by rewrite xepsE0. - by rewrite /xepsE /= addrA (addrC x) addrK subr_gt0 xz ltrBlDl. + by rewrite /xepsE /= addrC subrK subr_gt0 xz ltrBlDl. have drzx : dr x = [set t + (z - x) | t in dr z]. apply: dr_shift => // t /=. + (* t - x in xepsE -> False *) rewrite in_itv /= => /andP[] xt tz. apply: contraPnot xepsE0. rewrite -inE => Et; apply/eqP/set0P. - exists (t-x); rewrite /xepsE /= addrA (addrC x) addrK. + exists (t-x); rewrite /xepsE /= addrC subrK. by rewrite subr_gt0 xt ltrBlDl (le_lt_trans tz). have Hr : `|Num.min 1 xr - Num.min 1 zr| < eps. rewrite /xr /zr. @@ -365,7 +380,7 @@ case/boolP: (xepsE == set0). rewrite in_itv /= => /andP[] xt tz. apply: contraPnot xepsE0. rewrite -inE => Et; apply/eqP/set0P. - exists (t-x); rewrite /xepsE /= addrA (addrC x) addrK. + exists (t-x); rewrite /xepsE /= addrC subrK. by rewrite subr_gt0 xt ltrBlDl (le_lt_trans tz). have [dlx0|] := eqVneq (dl x) set0. rewrite dlx0 inf0 subr0. @@ -373,19 +388,13 @@ case/boolP: (xepsE == set0). suff : 0 \in dl x by rewrite inE dlx0. by rewrite inE /dl /= subr0. by rewrite dlxz dlx0 image_set0 inf0 subr0 (negbTE znE). - case/set0P => w Hw. - have inf_dlxz : x - inf (dl x) = z - inf (dl z). - rewrite dlxz -image2_set1 inf_sumE. - - by rewrite inf1 !opprD !addrA (addrC z) addrK (opprK x) addrC. - - split. by exists w. - exists 0. move=> u. rewrite -inE. exact: dl_ge0. - - exact: has_inf1. - rewrite -inf_dlxz. + move/set0P => dlx0. + rewrite -(inf_dlxz dlxz) //. case: ifPn => xlE //. rewrite (le_lt_trans (abs_subr_min _ _ _ _)) //. rewrite gt_max ltr_norml. rewrite -[inf(dl x)]addr0. - rewrite -(subrr (-z)) opprK addrA -[_ - _]addrA -inf_dlxz. + rewrite -(subrr (-z)) opprK addrA -[_ - _]addrA -(inf_dlxz dlxz) //. rewrite -!addrA addrC !addrA subrK addrC. rewrite (@le_lt_trans _ _ 0 (_ - _) ) //; first last. by rewrite subr_le0 ltW. From a6ac2b7e9b775b88ed74e4698075e279e4a80c98 Mon Sep 17 00:00:00 2001 From: Jacques Garrigue Date: Wed, 2 Jul 2025 13:23:31 +0900 Subject: [PATCH 18/45] better use of subrK/addKr --- theories/showcase/sorgenfreyline.v | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/theories/showcase/sorgenfreyline.v b/theories/showcase/sorgenfreyline.v index a1f8554d4..ee7dff145 100644 --- a/theories/showcase/sorgenfreyline.v +++ b/theories/showcase/sorgenfreyline.v @@ -254,7 +254,7 @@ apply/seteqP; rewrite /dl; split => t /= []. by rewrite /= in_itv /= ztx lerBlDr lerDl. exists (x - (z-t)). by rewrite opprD addrA subrr opprK add0r ztE subr_ge0. - by rewrite (addrC z) opprD opprK !addrA addrNK addrC addKr. + by rewrite (addrC z) opprD opprK !addrA subrK addrC addKr. move=> w [] xwE w0 <-. rewrite !opprD (addrCA z) !addrA addrK addrC opprK. by rewrite subr_ge0 ler_wpDl // ltW. @@ -272,10 +272,10 @@ apply/seteqP; rewrite /dr; split => t /= []. apply: xzNE. by rewrite /= in_itv /= zxt ltrDl y0. exists (x + t - z). - by rewrite addrA (addrC z) addrK xtE subr_gt0. - by rewrite addrA (addrAC _ _ z) addrK (addrC x) addrK. + by rewrite addrC subrK xtE subr_gt0. + by rewrite addrA subrK addrC addKr. move=> w [] xwE w0 <-. -rewrite !addrA addrAC (addrC x) addrK addrC. +rewrite !addrA addrC addrA addKr addrC. by rewrite subr_gt0 ltr_wpDr // ltW. Qed. @@ -395,7 +395,7 @@ case/boolP: (xepsE == set0). rewrite gt_max ltr_norml. rewrite -[inf(dl x)]addr0. rewrite -(subrr (-z)) opprK addrA -[_ - _]addrA -(inf_dlxz dlxz) //. - rewrite -!addrA addrC !addrA subrK addrC. + rewrite addrA addrC addrA addKr addrC. rewrite (@le_lt_trans _ _ 0 (_ - _) ) //; first last. by rewrite subr_le0 ltW. rewrite ltrBrDl ltrBlDr zx /=. @@ -414,7 +414,7 @@ case/boolP: (xepsE == set0). exists 0. move=> u. rewrite -inE. exact: dr_ge0. - exact: has_inf1. rewrite -drzx inf_drxz. - rewrite -!addrA addrC !addrA subrK ltr_norml. + rewrite addrC addrA addKr ltr_norml. rewrite (@lt_le_trans _ _ 0) ?ltrBlDl //= ?subr_ge0 ?ltW //. by rewrite oppr_lt0. move/set0P/xgetPex => /(_ eps). From 935b89b9b60f156c49c713c8727fe88d867d12d2 Mon Sep 17 00:00:00 2001 From: Yosuke Tsuji Date: Wed, 9 Jul 2025 12:23:07 +0900 Subject: [PATCH 19/45] refactor --- theories/showcase/sorgenfreyline.v | 87 ++++++++++++++---------------- 1 file changed, 41 insertions(+), 46 deletions(-) diff --git a/theories/showcase/sorgenfreyline.v b/theories/showcase/sorgenfreyline.v index ee7dff145..695a1bcfe 100644 --- a/theories/showcase/sorgenfreyline.v +++ b/theories/showcase/sorgenfreyline.v @@ -226,6 +226,9 @@ Proof. by move=> y; rewrite inE => -[]. Qed. Let dr_ge0 x : {in dr x, forall y : R, y >= 0}. Proof. by move=> y; rewrite inE => -[] _ /ltW. Qed. +Lemma sdist_ge0 x : 0 <= sdist x. +Proof. by rewrite /sdist le_min !fun_if ler01 !inf_ge0 // !if_same. Qed. + Lemma image2_set1 A B C (S : set A) (eb : B) (f : A -> B -> C) : [set f x y | x in S & y in [set eb]] = [set f x eb | x in S]. Proof. @@ -279,7 +282,7 @@ rewrite !addrA addrC addrA addKr addrC. by rewrite subr_gt0 ltr_wpDr // ltW. Qed. -Lemma inf_dlxz x z : +Lemma inf_dlxz x z : dl z = [set t + (z - x) | t in dl x] -> dl x !=set0 -> x - inf (dl x) = z - inf (dl z). @@ -292,6 +295,19 @@ rewrite dlxz -image2_set1 inf_sumE. - exact: has_inf1. Qed. +Lemma inf_drxz x z : + dr x = [set t + (z - x) | t in dr z] -> + dr z != set0 -> + inf (dr x) = inf (dr z) + z - x. +Proof. +move=> drzx drz0. +rewrite drzx -image2_set1 inf_sumE. +- by rewrite inf1 addrA. +- split. by apply/set0P. + exists 0. move=> u. rewrite -inE. exact: dr_ge0. +- exact: has_inf1. +Qed. + Definition continuous_at_sorgenfrey_to_Rtopo x (f : sorgenfrey -> R) := forall eps : R, 0 < eps -> exists2 d : R, 0 < d & forall y : R, x <= y < x + d -> `|f x - f y| < eps. @@ -350,31 +366,26 @@ case/boolP: (xepsE == set0). by rewrite subr_gt0 xt ltrBlDl (le_lt_trans tz). have Hr : `|Num.min 1 xr - Num.min 1 zr| < eps. rewrite /xr /zr. - case/boolP: (dr z == set0) => [/eqP |] drz0. + case/boolP: (dr z == set0) => [/eqP | /set0P] drz0. move: drzx. rewrite drz0 image_set0 => /eqP ->. by rewrite subrr normr0. have drx0 : dr x !=set0. - case/set0P : drz0 => z0 drzz0. + case : drz0 => z0 drzz0. rewrite drzx. exists (z0 + (z - x)) => /=. by exists z0. - rewrite ifF. - rewrite (le_lt_trans (abs_subr_min _ _ _ _)) //. - rewrite subrr normr0 maxEle normr_ge0. - rewrite drzx. - rewrite -image2_set1. - rewrite inf_sumE //. - rewrite inf1. - rewrite addrAC. - rewrite subrr add0r. - move/ltW: xz. - rewrite ler_def. - move/eqP ->. - by rewrite ltrBlDl. - split. exact/set0P. - exists 0. by move=> y [] _ /ltW. - exact/negbTE/set0P. + have inf_drlt : `|inf (dr x) - inf (dr z)| < eps. + rewrite drzx -image2_set1 inf_sumE //. + rewrite inf1 addrAC subrr add0r. + move/ltW: xz. + rewrite ler_def => /eqP ->. + by rewrite ltrBlDl. + split => //. + exists 0; by move=> y [] _ /ltW. + rewrite ifF; last exact/negbTE/set0P. + rewrite (le_lt_trans (abs_subr_min _ _ _ _)) //. + by rewrite subrr normr0 maxEle normr_ge0. have dlxz : dl z = [set t + (z - x) | t in dl x]. apply: dl_shift => // t /=. rewrite in_itv /= => /andP[] xt tz. @@ -407,49 +418,33 @@ case/boolP: (xepsE == set0). move/eqP /image_set0_set0 /eqP. by rewrite (negPf drz0). move=> drx0. - have inf_drxz : inf (dr x) = inf (dr z) + z - x. - rewrite drzx -image2_set1 inf_sumE. - - by rewrite inf1 addrA. - - split. by apply/set0P. - exists 0. move=> u. rewrite -inE. exact: dr_ge0. - - exact: has_inf1. - rewrite -drzx inf_drxz. + rewrite -drzx (inf_drxz drzx) //. rewrite addrC addrA addKr ltr_norml. rewrite (@lt_le_trans _ _ 0) ?ltrBlDl //= ?subr_ge0 ?ltW //. by rewrite oppr_lt0. move/set0P/xgetPex => /(_ eps). rewrite -/eps' => -[] eps'E Heps'. rewrite -/(sdist x) -/(sdist z). -have eps'l : forall t, x <= t < x + eps' -> 0 <= sdist t < eps. - move=> t Ht /=. +have eps'l : forall t, x <= t < x + eps' -> sdist t < eps. + move=> t /andP[xt tx] /=. rewrite /sdist. - set xl : R := if _ then _ else 1. - case: ifPn. - move/negP; elim; apply/negP/set0P. - exists (x+eps'-t). - rewrite /dr /= (addrC _ (-t)) addrA subrr add0r eps'E. - rewrite addrC subr_gt0 //; by case/andP: Ht. - move=> drt0. - rewrite le_min. - rewrite gt_min. - rewrite {1}/xl fun_if inf_ge0 // ler01 if_same /=. - rewrite inf_ge0 /=; last by move=> u; rewrite inE => -[] _ /ltW. - case/andP: Ht => xt tx. - rewrite orbC (@le_lt_trans _ _ (eps'+x-t)) //. + rewrite gt_min; apply/orP; right. + have /negbTE -> : dr t != set0. + apply/set0P; exists (x+eps'-t). + by rewrite /dr /= (addrC _ (-t)) addrA subrr add0r eps'E addrC subr_gt0. + rewrite (@le_lt_trans _ _ (eps'+x-t)) //. have [-> | infdr0] := eqVneq (inf (dr t)) 0. by rewrite subr_ge0 addrC ltW. rewrite le_inf_n0 // inE /dr /= (addrC _ (-t)) addrA subrr add0r addrC. by rewrite eps'E addrC subr_gt0. case/andP: Heps' => eps'0 Heps'. by rewrite (le_lt_trans _ Heps') // -addrA gerDl lerBlDl addr0. -have Hx : 0 <= sdist x < eps. +have Hx : sdist x < eps. by apply: eps'l; rewrite lexx ltrDl; case/andP: Heps'. -have Hz : 0 <= sdist z < eps. +have Hz : sdist z < eps. by apply: eps'l; rewrite zx ltW // xz. rewrite -maxrN gt_max. -case/andP: Hx => Hx1 Hx2. -case/andP: Hz => Hz1 Hz2. -by rewrite opprB !ltrBlDr !ltr_wpDr. +by rewrite opprB !ltrBlDr !ltr_wpDr // sdist_ge0. Qed. Lemma zeroset_sdist : E = sdist @^-1` [set 0]. From 940c0e968135dbd0a9bfd5014991e159fc7e65fa Mon Sep 17 00:00:00 2001 From: Jacques Garrigue Date: Wed, 9 Jul 2025 15:48:53 +0900 Subject: [PATCH 20/45] remore duplication and shorten --- theories/showcase/sorgenfreyline.v | 117 ++++++++++------------------- 1 file changed, 38 insertions(+), 79 deletions(-) diff --git a/theories/showcase/sorgenfreyline.v b/theories/showcase/sorgenfreyline.v index 695a1bcfe..aa6853c51 100644 --- a/theories/showcase/sorgenfreyline.v +++ b/theories/showcase/sorgenfreyline.v @@ -285,11 +285,11 @@ Qed. Lemma inf_dlxz x z : dl z = [set t + (z - x) | t in dl x] -> dl x !=set0 -> - x - inf (dl x) = z - inf (dl z). + inf (dl z) = inf (dl x) + z - x. Proof. move=> dlxz dlx0. rewrite dlxz -image2_set1 inf_sumE. -- by rewrite inf1 !opprD !addrA (addrC z) addrK (opprK x) addrC. +- by rewrite inf1 addrA. - split => //. exists 0. move=> u. rewrite -inE. exact: dl_ge0. - exact: has_inf1. @@ -348,103 +348,62 @@ have {xz xz'} xz: x < z by rewrite lt_neqAle xz'. rewrite /sdist. set xr : R := if dr x == set0 then _ else _. set zr : R := if dr z == set0 then _ else _. -case/boolP: (xepsE == set0). - move/eqP => xepsE0. +case/boolP: (xepsE == set0) => [/eqP xepsE0 | /set0P]. have Heps' : eps' = eps by rewrite /eps' xgetPN // xepsE0 => t. rewrite {}Heps' {eps'} in zx. - have znE : z \notin E. - apply/negP => zE. - suff : xepsE (z-x) by rewrite xepsE0. - by rewrite /xepsE /= addrC subrK subr_gt0 xz ltrBlDl. - have drzx : dr x = [set t + (z - x) | t in dr z]. - apply: dr_shift => // t /=. - (* t - x in xepsE -> False *) + have xznE : `]x,z] `<=` ~`E. + move=> t /=. rewrite in_itv /= => /andP[] xt tz. apply: contraPnot xepsE0. rewrite -inE => Et; apply/eqP/set0P. exists (t-x); rewrite /xepsE /= addrC subrK. by rewrite subr_gt0 xt ltrBlDl (le_lt_trans tz). + have znE : z \notin E. + rewrite -in_setC inE; apply: xznE. + by rewrite /= in_itv /= xz lexx. + have drzx : dr x = [set t + (z - x) | t in dr z] by apply: dr_shift. + have dlxz : dl z = [set t + (z - x) | t in dl x] by apply: dl_shift. + have xrzr_lt : `|xr - zr| < eps. + rewrite /xr /zr drzx. + have[-> | drz0] := eqVneq (dr z) set0. + by rewrite image_set0 eqxx subrr normr0 eps0. + case: ifPn => [/eqP /image_set0_set0 /eqP | drx0]. + by rewrite (negPf drz0). + rewrite -drzx (inf_drxz drzx) // addrC addrA addKr ltr_norml. + by rewrite (lt_le_trans (y:=0)) ?ltrBlDl //= ?subr_ge0 ?ltW // oppr_lt0. have Hr : `|Num.min 1 xr - Num.min 1 zr| < eps. - rewrite /xr /zr. - case/boolP: (dr z == set0) => [/eqP | /set0P] drz0. - move: drzx. - rewrite drz0 image_set0 => /eqP ->. - by rewrite subrr normr0. - have drx0 : dr x !=set0. - case : drz0 => z0 drzz0. - rewrite drzx. - exists (z0 + (z - x)) => /=. - by exists z0. - have inf_drlt : `|inf (dr x) - inf (dr z)| < eps. - rewrite drzx -image2_set1 inf_sumE //. - rewrite inf1 addrAC subrr add0r. - move/ltW: xz. - rewrite ler_def => /eqP ->. - by rewrite ltrBlDl. - split => //. - exists 0; by move=> y [] _ /ltW. - rewrite ifF; last exact/negbTE/set0P. - rewrite (le_lt_trans (abs_subr_min _ _ _ _)) //. - by rewrite subrr normr0 maxEle normr_ge0. - have dlxz : dl z = [set t + (z - x) | t in dl x]. - apply: dl_shift => // t /=. - rewrite in_itv /= => /andP[] xt tz. - apply: contraPnot xepsE0. - rewrite -inE => Et; apply/eqP/set0P. - exists (t-x); rewrite /xepsE /= addrC subrK. - by rewrite subr_gt0 xt ltrBlDl (le_lt_trans tz). - have [dlx0|] := eqVneq (dl x) set0. + apply: (le_lt_trans (abs_subr_min _ _ _ _)). + by rewrite subrr normr0 maxEle normr_ge0. + case/boolP: (dl x == set0) => [/eqP | /set0P] dlx0. rewrite dlx0 inf0 subr0. case: ifPn => xinE. suff : 0 \in dl x by rewrite inE dlx0. by rewrite inE /dl /= subr0. - by rewrite dlxz dlx0 image_set0 inf0 subr0 (negbTE znE). - move/set0P => dlx0. - rewrite -(inf_dlxz dlxz) //. - case: ifPn => xlE //. - rewrite (le_lt_trans (abs_subr_min _ _ _ _)) //. - rewrite gt_max ltr_norml. - rewrite -[inf(dl x)]addr0. - rewrite -(subrr (-z)) opprK addrA -[_ - _]addrA -(inf_dlxz dlxz) //. - rewrite addrA addrC addrA addKr addrC. - rewrite (@le_lt_trans _ _ 0 (_ - _) ) //; first last. - by rewrite subr_le0 ltW. - rewrite ltrBrDl ltrBlDr zx /=. - rewrite /xr /zr. - rewrite drzx. - have[-> | drz0] := eqVneq (dr z) set0. - by rewrite image_set0 eqxx subrr normr0 eps0. - case:ifPn. - move/eqP /image_set0_set0 /eqP. - by rewrite (negPf drz0). - move=> drx0. - rewrite -drzx (inf_drxz drzx) //. - rewrite addrC addrA addKr ltr_norml. - rewrite (@lt_le_trans _ _ 0) ?ltrBlDl //= ?subr_ge0 ?ltW //. - by rewrite oppr_lt0. -move/set0P/xgetPex => /(_ eps). -rewrite -/eps' => -[] eps'E Heps'. + by rewrite dlxz dlx0 image_set0 inf0 subr0 (negbTE znE) Hr. + rewrite (inf_dlxz dlxz) //. + rewrite {1}(addrC _ z) !opprD !addrA subrr add0r (addrC (- _)) (opprK x). + case: ifPn => xlE; last exact: Hr. + apply: (le_lt_trans (abs_subr_min _ _ _ _)). + rewrite !opprD !addrA subrr add0r (addrC (- _)) (opprK x). + rewrite gt_max ltr_norml xrzr_lt. + by rewrite ltrBrDl ltrBlDr zx ltrBlDl ltr_wpDr // ltW. +move/xgetPex => /= /(_ eps). +rewrite -/eps' => -[] eps'E /andP[eps'0 Heps']. rewrite -/(sdist x) -/(sdist z). have eps'l : forall t, x <= t < x + eps' -> sdist t < eps. move=> t /andP[xt tx] /=. rewrite /sdist. rewrite gt_min; apply/orP; right. - have /negbTE -> : dr t != set0. - apply/set0P; exists (x+eps'-t). - by rewrite /dr /= (addrC _ (-t)) addrA subrr add0r eps'E addrC subr_gt0. - rewrite (@le_lt_trans _ _ (eps'+x-t)) //. + have Ht : dr t (eps' + x - t) by rewrite /dr /= addrC subrK subr_gt0 addrC. + have /set0P /negbTE -> : dr t !=set0 by exists (eps'+x-t). + apply: (le_lt_trans _ _ (y:=eps'+x-t)). have [-> | infdr0] := eqVneq (inf (dr t)) 0. by rewrite subr_ge0 addrC ltW. - rewrite le_inf_n0 // inE /dr /= (addrC _ (-t)) addrA subrr add0r addrC. - by rewrite eps'E addrC subr_gt0. - case/andP: Heps' => eps'0 Heps'. + by rewrite le_inf_n0 // inE. by rewrite (le_lt_trans _ Heps') // -addrA gerDl lerBlDl addr0. -have Hx : sdist x < eps. - by apply: eps'l; rewrite lexx ltrDl; case/andP: Heps'. -have Hz : sdist z < eps. - by apply: eps'l; rewrite zx ltW // xz. -rewrite -maxrN gt_max. -by rewrite opprB !ltrBlDr !ltr_wpDr // sdist_ge0. +have Hx : sdist x < eps by apply: eps'l; rewrite lexx ltrDl. +have Hz : sdist z < eps by apply: eps'l; rewrite zx ltW // xz. +by rewrite -maxrN gt_max opprB !ltrBlDr !ltr_wpDr // sdist_ge0. Qed. Lemma zeroset_sdist : E = sdist @^-1` [set 0]. From ef027adb7faf72d272dde4c5d1a9f8b15da69090 Mon Sep 17 00:00:00 2001 From: Jacques Garrigue Date: Wed, 9 Jul 2025 17:38:18 +0900 Subject: [PATCH 21/45] extract sdist_in_lt and restructure --- theories/showcase/sorgenfreyline.v | 99 +++++++++++++++--------------- 1 file changed, 50 insertions(+), 49 deletions(-) diff --git a/theories/showcase/sorgenfreyline.v b/theories/showcase/sorgenfreyline.v index aa6853c51..77693bfc3 100644 --- a/theories/showcase/sorgenfreyline.v +++ b/theories/showcase/sorgenfreyline.v @@ -308,6 +308,22 @@ rewrite drzx -image2_set1 inf_sumE. - exact: has_inf1. Qed. +Lemma sdist_in_lt x t eps eps' : + x + eps' \in E -> eps' < eps -> + x <= t < x + eps' -> sdist t < eps. +Proof. +move=> eps'E Heps' /andP[xt tx] /=. +rewrite /sdist. +rewrite gt_min; apply/orP; right. +have Ht : dr t (eps' + x - t) by rewrite /dr /= addrC subrK subr_gt0 addrC. +have /set0P /negbTE -> : dr t !=set0 by exists (eps'+x-t). +apply: (le_lt_trans _ _ (y:=eps'+x-t)). + have [-> | infdr0] := eqVneq (inf (dr t)) 0. + by rewrite subr_ge0 addrC ltW. + by rewrite le_inf_n0 // inE. +by rewrite (le_lt_trans _ Heps') // -addrA gerDl lerBlDl addr0. +Qed. + Definition continuous_at_sorgenfrey_to_Rtopo x (f : sorgenfrey -> R) := forall eps : R, 0 < eps -> exists2 d : R, 0 < d & forall y : R, x <= y < x + d -> `|f x - f y| < eps. @@ -348,62 +364,47 @@ have {xz xz'} xz: x < z by rewrite lt_neqAle xz'. rewrite /sdist. set xr : R := if dr x == set0 then _ else _. set zr : R := if dr z == set0 then _ else _. -case/boolP: (xepsE == set0) => [/eqP xepsE0 | /set0P]. - have Heps' : eps' = eps by rewrite /eps' xgetPN // xepsE0 => t. - rewrite {}Heps' {eps'} in zx. - have xznE : `]x,z] `<=` ~`E. - move=> t /=. - rewrite in_itv /= => /andP[] xt tz. - apply: contraPnot xepsE0. - rewrite -inE => Et; apply/eqP/set0P. - exists (t-x); rewrite /xepsE /= addrC subrK. - by rewrite subr_gt0 xt ltrBlDl (le_lt_trans tz). - have znE : z \notin E. - rewrite -in_setC inE; apply: xznE. - by rewrite /= in_itv /= xz lexx. - have drzx : dr x = [set t + (z - x) | t in dr z] by apply: dr_shift. - have dlxz : dl z = [set t + (z - x) | t in dl x] by apply: dl_shift. - have xrzr_lt : `|xr - zr| < eps. - rewrite /xr /zr drzx. - have[-> | drz0] := eqVneq (dr z) set0. - by rewrite image_set0 eqxx subrr normr0 eps0. - case: ifPn => [/eqP /image_set0_set0 /eqP | drx0]. - by rewrite (negPf drz0). - rewrite -drzx (inf_drxz drzx) // addrC addrA addKr ltr_norml. - by rewrite (lt_le_trans (y:=0)) ?ltrBlDl //= ?subr_ge0 ?ltW // oppr_lt0. - have Hr : `|Num.min 1 xr - Num.min 1 zr| < eps. - apply: (le_lt_trans (abs_subr_min _ _ _ _)). - by rewrite subrr normr0 maxEle normr_ge0. +case/boolP: (xepsE == set0) => [xepsE0 | /set0P]; last first. + move/xgetPex => /= /(_ eps). + rewrite -/eps' => -[] x'E /andP[eps'0 Heps']. + rewrite -/(sdist x) -/(sdist z). + have Hx : sdist x < eps by apply: (sdist_in_lt x'E); rewrite // lexx ltrDl. + have Hz : sdist z < eps by apply: (sdist_in_lt x'E); rewrite // zx ltW // xz. + by rewrite -maxrN gt_max opprB !ltrBlDr !ltr_wpDr // sdist_ge0. +have Heps' : eps' = eps by rewrite /eps' xgetPN // (eqP xepsE0) => t. +rewrite {}Heps' {eps'} in zx. +have xznE : `]x,z] `<=` ~`E. + move=> t /=. + rewrite in_itv /= => /andP[] xt tz. + apply: contraTnot xepsE0. + rewrite -inE => Et; apply/set0P. + exists (t-x); rewrite /xepsE /= addrC subrK. + by rewrite subr_gt0 xt ltrBlDl (le_lt_trans tz). +have znE : z \notin E. + rewrite -in_setC inE; apply: xznE. + by rewrite /= in_itv /= xz lexx. +rewrite (le_lt_trans (abs_subr_min _ _ _ _)) // gt_max. +apply/andP; split; last first. +- have drzx : dr x = [set t + (z - x) | t in dr z] by apply: dr_shift. + rewrite /xr /zr drzx. + have[-> | drz0] := eqVneq (dr z) set0. + by rewrite image_set0 eqxx subrr normr0 eps0. + case: ifPn => [/eqP /image_set0_set0 /eqP | drx0]. + by rewrite (negPf drz0). + rewrite -drzx (inf_drxz drzx) // addrC addrA addKr ltr_norml. + by rewrite (lt_le_trans (y:=0)) ?ltrBlDl //= ?subr_ge0 ?ltW // oppr_lt0. +- have dlxz : dl z = [set t + (z - x) | t in dl x] by apply: dl_shift. case/boolP: (dl x == set0) => [/eqP | /set0P] dlx0. rewrite dlx0 inf0 subr0. case: ifPn => xinE. suff : 0 \in dl x by rewrite inE dlx0. by rewrite inE /dl /= subr0. - by rewrite dlxz dlx0 image_set0 inf0 subr0 (negbTE znE) Hr. + by rewrite dlxz dlx0 image_set0 inf0 subr0 (negbTE znE) subrr normr0. rewrite (inf_dlxz dlxz) //. - rewrite {1}(addrC _ z) !opprD !addrA subrr add0r (addrC (- _)) (opprK x). - case: ifPn => xlE; last exact: Hr. - apply: (le_lt_trans (abs_subr_min _ _ _ _)). + rewrite !opprD !addrA (addrC z) addrK (opprK x) (addrC (- _)). + case: ifPn => xlE; last by rewrite subrr normr0. rewrite !opprD !addrA subrr add0r (addrC (- _)) (opprK x). - rewrite gt_max ltr_norml xrzr_lt. - by rewrite ltrBrDl ltrBlDr zx ltrBlDl ltr_wpDr // ltW. -move/xgetPex => /= /(_ eps). -rewrite -/eps' => -[] eps'E /andP[eps'0 Heps']. -rewrite -/(sdist x) -/(sdist z). -have eps'l : forall t, x <= t < x + eps' -> sdist t < eps. - move=> t /andP[xt tx] /=. - rewrite /sdist. - rewrite gt_min; apply/orP; right. - have Ht : dr t (eps' + x - t) by rewrite /dr /= addrC subrK subr_gt0 addrC. - have /set0P /negbTE -> : dr t !=set0 by exists (eps'+x-t). - apply: (le_lt_trans _ _ (y:=eps'+x-t)). - have [-> | infdr0] := eqVneq (inf (dr t)) 0. - by rewrite subr_ge0 addrC ltW. - by rewrite le_inf_n0 // inE. - by rewrite (le_lt_trans _ Heps') // -addrA gerDl lerBlDl addr0. -have Hx : sdist x < eps by apply: eps'l; rewrite lexx ltrDl. -have Hz : sdist z < eps by apply: eps'l; rewrite zx ltW // xz. -by rewrite -maxrN gt_max opprB !ltrBlDr !ltr_wpDr // sdist_ge0. + by rewrite ltr_norml ltrBrDl ltrBlDr zx ltrBlDl ltr_wpDr // ltW. Qed. Lemma zeroset_sdist : E = sdist @^-1` [set 0]. From 61e6c3ab0760e7895db8f7b2ad2ad1ed92f3b3bb Mon Sep 17 00:00:00 2001 From: Jacques Garrigue Date: Wed, 9 Jul 2025 18:45:19 +0900 Subject: [PATCH 22/45] extract lerPnormB --- theories/showcase/sorgenfreyline.v | 36 ++++++++++++++++-------------- 1 file changed, 19 insertions(+), 17 deletions(-) diff --git a/theories/showcase/sorgenfreyline.v b/theories/showcase/sorgenfreyline.v index 77693bfc3..edfaa373f 100644 --- a/theories/showcase/sorgenfreyline.v +++ b/theories/showcase/sorgenfreyline.v @@ -308,22 +308,24 @@ rewrite drzx -image2_set1 inf_sumE. - exact: has_inf1. Qed. -Lemma sdist_in_lt x t eps eps' : - x + eps' \in E -> eps' < eps -> - x <= t < x + eps' -> sdist t < eps. +Lemma sdist_in_le x t eps : + x + eps \in E -> x <= t < x + eps -> sdist t <= eps. Proof. -move=> eps'E Heps' /andP[xt tx] /=. +move=> epsE /andP[xt tx] /=. rewrite /sdist. -rewrite gt_min; apply/orP; right. -have Ht : dr t (eps' + x - t) by rewrite /dr /= addrC subrK subr_gt0 addrC. -have /set0P /negbTE -> : dr t !=set0 by exists (eps'+x-t). -apply: (le_lt_trans _ _ (y:=eps'+x-t)). +rewrite ge_min; apply/orP; right. +have Ht : dr t (eps + x - t) by rewrite /dr /= addrC subrK subr_gt0 addrC. +have /set0P /negbTE -> : dr t !=set0 by exists (eps+x-t). +apply: (le_trans _ _ (y:=eps+x-t)). have [-> | infdr0] := eqVneq (inf (dr t)) 0. by rewrite subr_ge0 addrC ltW. by rewrite le_inf_n0 // inE. -by rewrite (le_lt_trans _ Heps') // -addrA gerDl lerBlDl addr0. +by rewrite lerBlDr lerD. Qed. +Lemma lerPnormB (x y m : R) : 0 <= x <= m -> 0 <= y <= m -> `|x - y| <= m. +Proof. by do!case/andP=>??; rewrite -maxrN ge_max opprB !lerBlDr !ler_wpDr. Qed. + Definition continuous_at_sorgenfrey_to_Rtopo x (f : sorgenfrey -> R) := forall eps : R, 0 < eps -> exists2 d : R, 0 < d & forall y : R, x <= y < x + d -> `|f x - f y| < eps. @@ -366,11 +368,11 @@ set xr : R := if dr x == set0 then _ else _. set zr : R := if dr z == set0 then _ else _. case/boolP: (xepsE == set0) => [xepsE0 | /set0P]; last first. move/xgetPex => /= /(_ eps). - rewrite -/eps' => -[] x'E /andP[eps'0 Heps']. - rewrite -/(sdist x) -/(sdist z). - have Hx : sdist x < eps by apply: (sdist_in_lt x'E); rewrite // lexx ltrDl. - have Hz : sdist z < eps by apply: (sdist_in_lt x'E); rewrite // zx ltW // xz. - by rewrite -maxrN gt_max opprB !ltrBlDr !ltr_wpDr // sdist_ge0. + rewrite -/eps' => -[] xE /andP[eps'0 Heps']. + rewrite -/(sdist x) -/(sdist z) (le_lt_trans _ Heps') //. + have Hx : sdist x <= eps' by apply: (sdist_in_le xE); rewrite // lexx ltrDl. + have Hz : sdist z <= eps' by apply: (sdist_in_le xE); rewrite // zx ltW // xz. + by rewrite lerPnormB // sdist_ge0. have Heps' : eps' = eps by rewrite /eps' xgetPN // (eqP xepsE0) => t. rewrite {}Heps' {eps'} in zx. have xznE : `]x,z] `<=` ~`E. @@ -391,8 +393,8 @@ apply/andP; split; last first. by rewrite image_set0 eqxx subrr normr0 eps0. case: ifPn => [/eqP /image_set0_set0 /eqP | drx0]. by rewrite (negPf drz0). - rewrite -drzx (inf_drxz drzx) // addrC addrA addKr ltr_norml. - by rewrite (lt_le_trans (y:=0)) ?ltrBlDl //= ?subr_ge0 ?ltW // oppr_lt0. + rewrite -drzx (inf_drxz drzx) // addrC addrA addKr. + by rewrite ltr_distl zx ltrBlDr ltr_wpDr // ltW. - have dlxz : dl z = [set t + (z - x) | t in dl x] by apply: dl_shift. case/boolP: (dl x == set0) => [/eqP | /set0P] dlx0. rewrite dlx0 inf0 subr0. @@ -404,7 +406,7 @@ apply/andP; split; last first. rewrite !opprD !addrA (addrC z) addrK (opprK x) (addrC (- _)). case: ifPn => xlE; last by rewrite subrr normr0. rewrite !opprD !addrA subrr add0r (addrC (- _)) (opprK x). - by rewrite ltr_norml ltrBrDl ltrBlDr zx ltrBlDl ltr_wpDr // ltW. + by rewrite ltr_distl ltrBlDr zx ltr_wpDr // ltW. Qed. Lemma zeroset_sdist : E = sdist @^-1` [set 0]. From a9941f0e41075eed1e14a33ac510c059f048ddfe Mon Sep 17 00:00:00 2001 From: Jacques Garrigue Date: Wed, 9 Jul 2025 19:07:46 +0900 Subject: [PATCH 23/45] renaming and style --- theories/showcase/sorgenfreyline.v | 33 +++++++++++++++--------------- 1 file changed, 16 insertions(+), 17 deletions(-) diff --git a/theories/showcase/sorgenfreyline.v b/theories/showcase/sorgenfreyline.v index edfaa373f..60524ed29 100644 --- a/theories/showcase/sorgenfreyline.v +++ b/theories/showcase/sorgenfreyline.v @@ -308,15 +308,15 @@ rewrite drzx -image2_set1 inf_sumE. - exact: has_inf1. Qed. -Lemma sdist_in_le x t eps : - x + eps \in E -> x <= t < x + eps -> sdist t <= eps. +Lemma sdist_in_le x t d : + x + d \in E -> x <= t < x + d -> sdist t <= d. Proof. -move=> epsE /andP[xt tx] /=. +move=> dE /andP[xt tx] /=. rewrite /sdist. rewrite ge_min; apply/orP; right. -have Ht : dr t (eps + x - t) by rewrite /dr /= addrC subrK subr_gt0 addrC. -have /set0P /negbTE -> : dr t !=set0 by exists (eps+x-t). -apply: (le_trans _ _ (y:=eps+x-t)). +have Ht : dr t (d + x - t) by rewrite /dr /= addrC subrK subr_gt0 addrC. +have /set0P /negbTE -> : dr t !=set0 by exists (d+x-t). +apply: (le_trans _ _ (y:=d+x-t)). have [-> | infdr0] := eqVneq (inf (dr t)) 0. by rewrite subr_ge0 addrC ltW. by rewrite le_inf_n0 // inE. @@ -355,11 +355,10 @@ Proof. move=> x. apply: continuous_at_sorgenfrey_to_RtopoP => /= eps eps0. pose xepsE := [set y | x + y \in E /\ 0 < y < eps]. -pose eps' := xget eps xepsE. -exists eps'. - by rewrite /eps'; case: (xgetP eps xepsE) => // y -> [] _ /andP[]. +exists (xget eps xepsE). + by case: (xgetP eps xepsE) => // y -> [] _ /andP[]. (* forall z : R, x <= z < x + eps' -> `|sdist x - sdist z| < eps *) -move=> z /andP [] xz zx. +move=> z /andP[xz zx]. have [<-|xz'] := eqVneq x z. by rewrite subrr normr0. have {xz xz'} xz: x < z by rewrite lt_neqAle xz'. @@ -368,16 +367,16 @@ set xr : R := if dr x == set0 then _ else _. set zr : R := if dr z == set0 then _ else _. case/boolP: (xepsE == set0) => [xepsE0 | /set0P]; last first. move/xgetPex => /= /(_ eps). - rewrite -/eps' => -[] xE /andP[eps'0 Heps']. - rewrite -/(sdist x) -/(sdist z) (le_lt_trans _ Heps') //. - have Hx : sdist x <= eps' by apply: (sdist_in_le xE); rewrite // lexx ltrDl. - have Hz : sdist z <= eps' by apply: (sdist_in_le xE); rewrite // zx ltW // xz. + set d := xget eps xepsE in zx *. + case=> xdE /andP[d0 deps]. + rewrite -/(sdist x) -/(sdist z) (le_lt_trans _ deps) //. + have Hx : sdist x <= d by apply: (sdist_in_le xdE); rewrite // lexx ltrDl. + have Hz : sdist z <= d by apply: (sdist_in_le xdE); rewrite // zx ltW // xz. by rewrite lerPnormB // sdist_ge0. -have Heps' : eps' = eps by rewrite /eps' xgetPN // (eqP xepsE0) => t. -rewrite {}Heps' {eps'} in zx. +rewrite xgetPN in zx; last by move=> t; rewrite (eqP xepsE0). have xznE : `]x,z] `<=` ~`E. move=> t /=. - rewrite in_itv /= => /andP[] xt tz. + rewrite in_itv /= => /andP[xt tz]. apply: contraTnot xepsE0. rewrite -inE => Et; apply/set0P. exists (t-x); rewrite /xepsE /= addrC subrK. From 455ba84e97a38965b5d8e97d24e0dd7b341944a2 Mon Sep 17 00:00:00 2001 From: Jacques Garrigue Date: Thu, 10 Jul 2025 15:53:36 +0900 Subject: [PATCH 24/45] simplify zeroset_sdist --- theories/showcase/sorgenfreyline.v | 80 ++++++++++-------------------- 1 file changed, 25 insertions(+), 55 deletions(-) diff --git a/theories/showcase/sorgenfreyline.v b/theories/showcase/sorgenfreyline.v index 60524ed29..b1e41e54a 100644 --- a/theories/showcase/sorgenfreyline.v +++ b/theories/showcase/sorgenfreyline.v @@ -199,32 +199,19 @@ case: (lerP u y) => uy. by rewrite lerD2r xy orbT. by rewrite leNgt (lt_trans uy xu) in xy. Qed. -Lemma le_inf_n0 (S : set R) (x : R) : x \in S -> inf S != 0 -> inf S <= x. -Proof. -move=> xS infS0. -rewrite -(inf1 x) le_inf //. -- rewrite image_set1 => z /= ->. - apply/downP; exists (-x) => //. - by exists x => //; rewrite -inE. -- by exists x. -- move: infS0. - by apply: contraNP => /inf_out ->. -Qed. - -Lemma inf_ge0 (S : set R) : {in S, forall x : R, x >= 0} -> inf S >= 0. +Lemma inf_ge0 (S : set R) : lbound S 0 -> inf S >= 0. Proof. move=> S_ge0. case/boolP: (S == set0) => [/eqP -> | /set0P S0]. by rewrite inf0. -apply: lb_le_inf => // x Sx. -by apply: S_ge0; rewrite inE. +by apply: lb_le_inf. Qed. -Let dl_ge0 x : {in dl x, forall y : R, y >= 0}. -Proof. by move=> y; rewrite inE => -[]. Qed. +Let dl_ge0 x : lbound (dl x) 0. +Proof. by move=> y []. Qed. -Let dr_ge0 x : {in dr x, forall y : R, y >= 0}. -Proof. by move=> y; rewrite inE => -[] _ /ltW. Qed. +Let dr_ge0 x : lbound (dr x) 0. +Proof. move=> y [] _; exact: ltW. Qed. Lemma sdist_ge0 x : 0 <= sdist x. Proof. by rewrite /sdist le_min !fun_if ler01 !inf_ge0 // !if_same. Qed. @@ -291,7 +278,7 @@ move=> dlxz dlx0. rewrite dlxz -image2_set1 inf_sumE. - by rewrite inf1 addrA. - split => //. - exists 0. move=> u. rewrite -inE. exact: dl_ge0. + exists 0. move=> u. exact: dl_ge0. - exact: has_inf1. Qed. @@ -304,7 +291,7 @@ move=> drzx drz0. rewrite drzx -image2_set1 inf_sumE. - by rewrite inf1 addrA. - split. by apply/set0P. - exists 0. move=> u. rewrite -inE. exact: dr_ge0. + exists 0. move=> u. exact: dr_ge0. - exact: has_inf1. Qed. @@ -317,9 +304,7 @@ rewrite ge_min; apply/orP; right. have Ht : dr t (d + x - t) by rewrite /dr /= addrC subrK subr_gt0 addrC. have /set0P /negbTE -> : dr t !=set0 by exists (d+x-t). apply: (le_trans _ _ (y:=d+x-t)). - have [-> | infdr0] := eqVneq (inf (dr t)) 0. - by rewrite subr_ge0 addrC ltW. - by rewrite le_inf_n0 // inE. + by apply: inf_lbound => //; exists 0. by rewrite lerBlDr lerD. Qed. @@ -410,45 +395,31 @@ Qed. Lemma zeroset_sdist : E = sdist @^-1` [set 0]. Proof. -rewrite /sdist. apply/seteqP; split => x /= Hx. - suff -> : inf (dl x) = 0. - rewrite subr0 ifT; last by rewrite inE. - case: ifP => _; case: lerP => //. - by rewrite ltNge ler01. - by rewrite ltNge inf_ge0. - apply/eqP; rewrite eq_le inf_ge0 //. - rewrite -[X in _ <= X]inf1 le_inf /dl //=. - - move=> y []z /= -> <- /=. - exists (-0); split => //=. - exists 0 => //; by rewrite subr0 inE. - - by exists 0. - - split. exists 0 => /=; by rewrite subr0 inE. - by exists 0 => y []. -move/eqP: Hx; rewrite /sdist. -rewrite minEle; case: ifP => _. + suff /eqP H : inf (dl x) == 0. + apply/esym/eqP; rewrite eq_le sdist_ge0 /sdist H /=. + by rewrite subr0 ifT ?inE // ge_min lexx. + rewrite eq_le inf_ge0 // andbT. + apply: inf_lbound. + exists 0. by move => t /dl_ge0. + by rewrite /dl /= subr0 inE. +move/eqP: Hx; rewrite /sdist minEle. +case: ifP => _. case: ifP; last by rewrite (negbTE (@oner_neq0 _)). rewrite inE => /[swap] /eqP ->. by rewrite subr0. case: ifPn; first by rewrite (negbTE (@oner_neq0 _)). move=> n0 /eqP infeq. -case/boolP: (x \in E); first by rewrite inE. -rewrite -in_setC inE. +apply/notP => xE. have : open (~` E) by rewrite openC. -rewrite openE /= => HE xE. -suff: False by []. -case: (HE x xE) => opx [] /= [] L HL <- [] /= [a a'] La. -rewrite /b /= in_itv /= => xa. +rewrite openE /= => /(_ x xE) [] opx [] /= [] L HL <- [] /= [a a'] La. +rewrite /b /= in_itv /= => /andP[ax xa']. move/(subset_trans (bigcup_sup La)) => /= aE. -have := @inf_adherent _ (dr x) (a' -x). -case/andP: xa => ax xa'. -rewrite subr_gt0 xa'. -have hE : has_inf (dr x). - split. by apply/set0P. - exists 0. by move=> y [] _ /ltW. -case/(_ isT hE) => y yxr. +have a'x_gt0 : a' - x > 0 by rewrite subr_gt0 xa'. +have hE : has_inf (dr x) by split; [apply/set0P | exists 0]. +case: (inf_adherent a'x_gt0 hE) => y drxy. rewrite infeq add0r ltrBrDl => xya'. -case: yxr => xyE y0. +case: drxy => xyE y0. suff : x+y \notin E by rewrite xyE. rewrite -in_setC inE. apply: aE => /=. by rewrite in_itv /= xya' (le_trans ax) // ler_wpDr // ltW. @@ -465,5 +436,4 @@ split. exact: zeroset_sdist. Qed. - End Sorgenfrey_line. From f4223b39a96769159e75305991b2c47ff1f4fa8b Mon Sep 17 00:00:00 2001 From: Jacques Garrigue Date: Thu, 10 Jul 2025 15:57:43 +0900 Subject: [PATCH 25/45] typo --- theories/showcase/sorgenfreyline.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/theories/showcase/sorgenfreyline.v b/theories/showcase/sorgenfreyline.v index b1e41e54a..ac1df261f 100644 --- a/theories/showcase/sorgenfreyline.v +++ b/theories/showcase/sorgenfreyline.v @@ -426,7 +426,7 @@ by rewrite in_itv /= xya' (le_trans ax) // ler_wpDr // ltW. Qed. End distance. -Lemma sorgenfrey_line_perfectly_norml_space : +Lemma sorgenfrey_line_perfectly_normal_space : perfectly_normal_space R sorgenfrey. Proof. move=> E cE. From 341f6fbdf89143253319a5a808811caae629df65 Mon Sep 17 00:00:00 2001 From: Jacques Garrigue Date: Thu, 10 Jul 2025 17:03:40 +0900 Subject: [PATCH 26/45] inf_shift --- theories/showcase/sorgenfreyline.v | 34 ++++++++++++------------------ 1 file changed, 13 insertions(+), 21 deletions(-) diff --git a/theories/showcase/sorgenfreyline.v b/theories/showcase/sorgenfreyline.v index ac1df261f..1be10e250 100644 --- a/theories/showcase/sorgenfreyline.v +++ b/theories/showcase/sorgenfreyline.v @@ -269,31 +269,23 @@ rewrite !addrA addrC addrA addKr addrC. by rewrite subr_gt0 ltr_wpDr // ltW. Qed. +Lemma inf_shift (s1 s2 : set R) (d : R) : + s2 = [set t + d | t in s1] -> + has_inf s1 -> + inf s2 = inf s1 + d. +Proof. by move=> -> lbs1; rewrite -image2_set1 inf_sumE // inf1. Qed. + Lemma inf_dlxz x z : - dl z = [set t + (z - x) | t in dl x] -> - dl x !=set0 -> + dl z = [set t + (z - x) | t in dl x] -> + dl x !=set0 -> inf (dl z) = inf (dl x) + z - x. -Proof. -move=> dlxz dlx0. -rewrite dlxz -image2_set1 inf_sumE. -- by rewrite inf1 addrA. -- split => //. - exists 0. move=> u. exact: dl_ge0. -- exact: has_inf1. -Qed. +Proof. by move=> H *; rewrite -addrA -(inf_shift H)//; split=>//; exists 0. Qed. Lemma inf_drxz x z : dr x = [set t + (z - x) | t in dr z] -> - dr z != set0 -> + dr z !=set0 -> inf (dr x) = inf (dr z) + z - x. -Proof. -move=> drzx drz0. -rewrite drzx -image2_set1 inf_sumE. -- by rewrite inf1 addrA. -- split. by apply/set0P. - exists 0. move=> u. exact: dr_ge0. -- exact: has_inf1. -Qed. +Proof. by move=> H *; rewrite -addrA -(inf_shift H)//; split=>//; exists 0. Qed. Lemma sdist_in_le x t d : x + d \in E -> x <= t < x + d -> sdist t <= d. @@ -377,8 +369,8 @@ apply/andP; split; last first. by rewrite image_set0 eqxx subrr normr0 eps0. case: ifPn => [/eqP /image_set0_set0 /eqP | drx0]. by rewrite (negPf drz0). - rewrite -drzx (inf_drxz drzx) // addrC addrA addKr. - by rewrite ltr_distl zx ltrBlDr ltr_wpDr // ltW. + rewrite -drzx (inf_drxz drzx); last exact/set0P. + by rewrite addrC addrA addKr ltr_distl zx ltrBlDr ltr_wpDr // ltW. - have dlxz : dl z = [set t + (z - x) | t in dl x] by apply: dl_shift. case/boolP: (dl x == set0) => [/eqP | /set0P] dlx0. rewrite dlx0 inf0 subr0. From 86618167c2ab7742d4f0550f88fa4dd36460aae7 Mon Sep 17 00:00:00 2001 From: Takafumi Saikawa Date: Thu, 10 Jul 2025 17:47:06 +0900 Subject: [PATCH 27/45] dlE drE --- theories/showcase/sorgenfreyline.v | 19 +++++++++++++++++++ 1 file changed, 19 insertions(+) diff --git a/theories/showcase/sorgenfreyline.v b/theories/showcase/sorgenfreyline.v index 1be10e250..51390a992 100644 --- a/theories/showcase/sorgenfreyline.v +++ b/theories/showcase/sorgenfreyline.v @@ -182,6 +182,25 @@ Definition sdist (x : sorgenfrey) : R := From mathcomp Require Import topology normedtype. Let Rtopo := num_topology.numFieldTopology.Real_sort__canonical__topology_structure_Topological R. +Local Lemma dlE x : dl x = (shift x) @` (-%R @` E) `&` `[0, +oo[. +Proof. +rewrite /dl; apply/seteqP; split=> y /=; rewrite in_itv inE /=. + case=> Exy ->; split => //. + exists (y - x); last by rewrite subrK. + by exists (x - y) => //; rewrite opprB. +case=> -[] v [] w Ew <- <- /[!andbT] ->; split => //. +by rewrite opprD opprK mathcomp_extra.subrKC. +Qed. + +Local Lemma drE x : dr x = (center x) @` E `&` `]0, +oo[. +Proof. +rewrite /dr; apply/seteqP; split=> y /=; rewrite in_itv inE /=. + case=> Exy ->; split => //. + by exists (x + y) => //; rewrite addrAC subrr add0r. +case=> -[] v Ev <- /[!andbT] ->; split => //. +by rewrite mathcomp_extra.subrKC. +Qed. + Lemma abs_subr_min (x y t u : R) : `|Num.min x y - Num.min t u| <= Num.max `|x - t| `|y - u|. Proof. From 517fbb8cccd0ea369cc509837a00df5fa257edaf Mon Sep 17 00:00:00 2001 From: Takafumi Saikawa Date: Thu, 10 Jul 2025 18:10:50 +0900 Subject: [PATCH 28/45] shiftN, centerN --- .../pseudometric_normed_Zmodule.v | 16 ++++++++++++++++ 1 file changed, 16 insertions(+) diff --git a/theories/normedtype_theory/pseudometric_normed_Zmodule.v b/theories/normedtype_theory/pseudometric_normed_Zmodule.v index 30e6d7511..7b9294eec 100644 --- a/theories/normedtype_theory/pseudometric_normed_Zmodule.v +++ b/theories/normedtype_theory/pseudometric_normed_Zmodule.v @@ -95,6 +95,22 @@ Proof. by rewrite funeqE => x /=; rewrite addr0. Qed. Lemma center0 : center 0 = id. Proof. by rewrite oppr0 shift0. Qed. +Lemma centerN (x y : R) : center x (- y) = - shift x y. +Proof. by rewrite /shift opprD. Qed. + +Lemma shiftN (x y : R) : shift x (- y) = - center x y. +Proof. by rewrite /shift opprD opprK. Qed. + +Lemma image_centerN (E : set R) (x : R) : + [set center x (- y) | y in E] =[set - (shift x y) | y in E]. +Proof. +by apply/seteqP; split => y [] u Eu <- /=; exists u => //; rewrite opprD. +Qed. + +Lemma image_shiftN (E : set R) (x : R) : + [set shift x (- y) | y in E] = [set - (center x y) | y in E]. +Proof. by rewrite -(opprK x) image_centerN opprK. Qed. + End Shift. Arguments shift {R} x / y. Notation center c := (shift (- c)). From a6f5ee79d82d1081b041b5e18dea4f2d5014861c Mon Sep 17 00:00:00 2001 From: Takafumi Saikawa Date: Thu, 10 Jul 2025 18:11:22 +0900 Subject: [PATCH 29/45] simplify dlE drE --- theories/showcase/sorgenfreyline.v | 11 +++++------ 1 file changed, 5 insertions(+), 6 deletions(-) diff --git a/theories/showcase/sorgenfreyline.v b/theories/showcase/sorgenfreyline.v index 51390a992..2003adfab 100644 --- a/theories/showcase/sorgenfreyline.v +++ b/theories/showcase/sorgenfreyline.v @@ -1,6 +1,6 @@ From HB Require Import structures. From mathcomp Require Import all_ssreflect all_algebra all_fingroup. -From mathcomp Require Import wochoice contra. +From mathcomp Require Import wochoice contra mathcomp_extra. From mathcomp Require Import boolp classical_sets set_interval. From mathcomp Require Import topology_structure separation_axioms connected. From mathcomp Require Import reals. @@ -182,14 +182,13 @@ Definition sdist (x : sorgenfrey) : R := From mathcomp Require Import topology normedtype. Let Rtopo := num_topology.numFieldTopology.Real_sort__canonical__topology_structure_Topological R. -Local Lemma dlE x : dl x = (shift x) @` (-%R @` E) `&` `[0, +oo[. +Local Lemma dlE x : dl x = [set shift x (- y) | y in E] `&` `[0, +oo[. Proof. rewrite /dl; apply/seteqP; split=> y /=; rewrite in_itv inE /=. case=> Exy ->; split => //. - exists (y - x); last by rewrite subrK. - by exists (x - y) => //; rewrite opprB. -case=> -[] v [] w Ew <- <- /[!andbT] ->; split => //. -by rewrite opprD opprK mathcomp_extra.subrKC. + by exists (x - y) => //; rewrite opprB addrAC addrK. +case=> -[] u Eu <- /[!andbT] ->; split => //. +by rewrite opprD opprK subrKC. Qed. Local Lemma drE x : dr x = (center x) @` E `&` `]0, +oo[. From dcbfa705fe9b3175ab83a8d4cc37affda86f6659 Mon Sep 17 00:00:00 2001 From: Takafumi Saikawa Date: Fri, 11 Jul 2025 01:39:34 +0900 Subject: [PATCH 30/45] lt_(dl,dr)_set0 --- theories/showcase/sorgenfreyline.v | 21 +++++++++++++++++++++ 1 file changed, 21 insertions(+) diff --git a/theories/showcase/sorgenfreyline.v b/theories/showcase/sorgenfreyline.v index 2003adfab..ae011bb9e 100644 --- a/theories/showcase/sorgenfreyline.v +++ b/theories/showcase/sorgenfreyline.v @@ -200,6 +200,27 @@ case=> -[] v Ev <- /[!andbT] ->; split => //. by rewrite mathcomp_extra.subrKC. Qed. +Local Lemma lt_dr_set0 x y : x < y -> dr x = set0 -> dr y = set0. +Proof. +move=> xy. +rewrite !drE !(rwP eqP); apply: contraLR. +case/set0P=> u /= [] [] v Ev <-. +rewrite in_itv /= andbT subr_gt0 => yv. +apply/set0P; exists (v - x) => /=. +rewrite in_itv /= subr_gt0 (lt_trans xy yv); split => //. +by exists v. +Qed. + +Local Lemma lt_dl_set0 x y : x < y -> dl y = set0 -> dl x = set0. +move=> xy. +rewrite !dlE !(rwP eqP); apply: contraLR. +case/set0P=> u /= [] [] v Ev <-. +rewrite in_itv /= andbT addrC subr_ge0 => vx. +apply/set0P; exists (y - v) => /=. +rewrite in_itv /= subr_ge0 (le_trans vx (ltW xy)); split => //. +by exists v => //; rewrite addrC. +Qed. + Lemma abs_subr_min (x y t u : R) : `|Num.min x y - Num.min t u| <= Num.max `|x - t| `|y - u|. Proof. From e66798b5292ab2cf528207f56b52b471c9a8c3aa Mon Sep 17 00:00:00 2001 From: Jacques Garrigue Date: Fri, 11 Jul 2025 12:11:44 +0900 Subject: [PATCH 31/45] dr_shift/dl_shift --- theories/showcase/sorgenfreyline.v | 23 +++++++++-------------- 1 file changed, 9 insertions(+), 14 deletions(-) diff --git a/theories/showcase/sorgenfreyline.v b/theories/showcase/sorgenfreyline.v index ae011bb9e..be170a0cc 100644 --- a/theories/showcase/sorgenfreyline.v +++ b/theories/showcase/sorgenfreyline.v @@ -275,18 +275,15 @@ Let dl_shift x z : Proof. move=> xz xzNE. apply/seteqP; rewrite /dl; split => t /= []. - move => ztE y0. + move=> ztE t0. case: (ltrP x (z-t)) => ztx. - suff : z - t \notin E by rewrite ztE. - rewrite -in_setC inE. - apply: xzNE. - by rewrite /= in_itv /= ztx lerBlDr lerDl. + elim: (xzNE (z-t)); last by rewrite -inE. + by rewrite /= in_itv /= ztx gerBl. exists (x - (z-t)). - by rewrite opprD addrA subrr opprK add0r ztE subr_ge0. + by rewrite subr_ge0 opprD addrA subrr add0r opprK. by rewrite (addrC z) opprD opprK !addrA subrK addrC addKr. move=> w [] xwE w0 <-. -rewrite !opprD (addrCA z) !addrA addrK addrC opprK. -by rewrite subr_ge0 ler_wpDl // ltW. +by rewrite !opprD (addrCA z) !addrA addrK addrC opprK subr_ge0 ler_wpDl // ltW. Qed. Let dr_shift x z : @@ -294,12 +291,10 @@ Let dr_shift x z : Proof. move=> xz xzNE. apply/seteqP; rewrite /dr; split => t /= []. - move => xtE y0. - case: (ltrP z (x+t)) => zxt; last first. - suff : x + t \notin E by rewrite xtE. - rewrite -in_setC inE. - apply: xzNE. - by rewrite /= in_itv /= zxt ltrDl y0. + move=> xtE t0. + case: (lerP (x+t) z) => zxt. + elim: (xzNE (x+t)); last by rewrite -inE. + by rewrite /= in_itv /= zxt ltrDl t0. exists (x + t - z). by rewrite addrC subrK xtE subr_gt0. by rewrite addrA subrK addrC addKr. From e00e50e804850e101ff866da5591affcb8ed60b8 Mon Sep 17 00:00:00 2001 From: Jacques Garrigue Date: Fri, 11 Jul 2025 12:36:04 +0900 Subject: [PATCH 32/45] elim --- theories/showcase/sorgenfreyline.v | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/theories/showcase/sorgenfreyline.v b/theories/showcase/sorgenfreyline.v index be170a0cc..ba3413538 100644 --- a/theories/showcase/sorgenfreyline.v +++ b/theories/showcase/sorgenfreyline.v @@ -446,9 +446,8 @@ have hE : has_inf (dr x) by split; [apply/set0P | exists 0]. case: (inf_adherent a'x_gt0 hE) => y drxy. rewrite infeq add0r ltrBrDl => xya'. case: drxy => xyE y0. -suff : x+y \notin E by rewrite xyE. -rewrite -in_setC inE. apply: aE => /=. -by rewrite in_itv /= xya' (le_trans ax) // ler_wpDr // ltW. +elim: (aE (x + y)); last by rewrite -inE. +by rewrite /= in_itv /= xya' (le_trans ax) // ler_wpDr // ltW. Qed. End distance. From 90899ab778f23ef1f001c4fc418d29a2da49db8b Mon Sep 17 00:00:00 2001 From: Jacques Garrigue Date: Tue, 22 Jul 2025 10:43:24 +0900 Subject: [PATCH 33/45] small clean up --- theories/showcase/sorgenfreyline.v | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) diff --git a/theories/showcase/sorgenfreyline.v b/theories/showcase/sorgenfreyline.v index ba3413538..88a349cd8 100644 --- a/theories/showcase/sorgenfreyline.v +++ b/theories/showcase/sorgenfreyline.v @@ -180,7 +180,8 @@ Definition sdist (x : sorgenfrey) : R := (if dr x == set0 then 1 else inf (dr x)). From mathcomp Require Import topology normedtype. -Let Rtopo := num_topology.numFieldTopology.Real_sort__canonical__topology_structure_Topological R. +Let Rtopo := num_topology.numFieldTopology + .Real_sort__canonical__topology_structure_Topological R. Local Lemma dlE x : dl x = [set shift x (- y) | y in E] `&` `[0, +oo[. Proof. @@ -280,10 +281,10 @@ apply/seteqP; rewrite /dl; split => t /= []. elim: (xzNE (z-t)); last by rewrite -inE. by rewrite /= in_itv /= ztx gerBl. exists (x - (z-t)). - by rewrite subr_ge0 opprD addrA subrr add0r opprK. - by rewrite (addrC z) opprD opprK !addrA subrK addrC addKr. + by rewrite subKr subr_ge0. + by rewrite addrAC (addrC x) subrK subKr. move=> w [] xwE w0 <-. -by rewrite !opprD (addrCA z) !addrA addrK addrC opprK subr_ge0 ler_wpDl // ltW. +by rewrite opprD opprB addrC !addrA subrK addrC subr_ge0 ler_wpDl // ltW. Qed. Let dr_shift x z : @@ -296,11 +297,10 @@ apply/seteqP; rewrite /dr; split => t /= []. elim: (xzNE (x+t)); last by rewrite -inE. by rewrite /= in_itv /= zxt ltrDl t0. exists (x + t - z). - by rewrite addrC subrK xtE subr_gt0. + by rewrite addrC subrK subr_gt0. by rewrite addrA subrK addrC addKr. move=> w [] xwE w0 <-. -rewrite !addrA addrC addrA addKr addrC. -by rewrite subr_gt0 ltr_wpDr // ltW. +by rewrite addrC addrA subrK addrC subr_gt0 ltr_wpDr // ltW. Qed. Lemma inf_shift (s1 s2 : set R) (d : R) : From fa36e57c3006b8cdde1becd493f54df96caf896d Mon Sep 17 00:00:00 2001 From: Yosuke Tsuji Date: Wed, 30 Jul 2025 12:35:58 +0900 Subject: [PATCH 34/45] move Section perfectlynormalspace separation_axioms.v to borel_hierarchy.v --- theories/borel_hierarchy.v | 45 ++++++++++++++++++++ theories/topology_theory/separation_axioms.v | 9 ---- 2 files changed, 45 insertions(+), 9 deletions(-) diff --git a/theories/borel_hierarchy.v b/theories/borel_hierarchy.v index 6bd0622ea..a6df8b6b7 100644 --- a/theories/borel_hierarchy.v +++ b/theories/borel_hierarchy.v @@ -21,8 +21,10 @@ Unset Printing Implicit Defensive. Import Order.TTheory GRing.Theory Num.Theory. Import numFieldNormedType.Exports. +Import numFieldTopology.Exports. Local Open Scope classical_set_scope. +Local Open Scope ring_scope. Section Gdelta_Fsigma. Context {T : topologicalType}. @@ -94,3 +96,46 @@ have /Baire : forall n, open (C n) /\ dense (C n). - by apply: denseI => //; apply oB. by rewrite -C0; exact: dense0. Qed. + +Section perfectlynormalspace. +Context (R : realType) (T : topologicalType). + +Definition perfectly_normal_space (x : R) := + forall E : set T, closed E -> + exists f : T -> R, continuous f /\ E = f @^-1` [set x]. + +Lemma perfectly_normal_spaceP x y : perfectly_normal_space x -> perfectly_normal_space y. +Proof. +move=>px E cE. +case:(px E cE) => f [] cf ->. +pose f' := f + cst (y - x). +exists f'. +split. +rewrite /f'. +move=> z. +apply: continuousD. +exact:cf. +exact:cst_continuous. +apply/seteqP. +rewrite /f' /cst /=. +split => z /=. +rewrite addrfctE => ->. +by rewrite subrKC. +rewrite addrfctE. +move/eqP. +by rewrite eq_sym -subr_eq opprB subrKC eq_sym => /eqP. +Qed. + +Definition perfectly_normal_space01 := + forall E F : set T, closed E -> closed F -> [disjoint E & F] -> + exists f : T -> R, continuous f /\ E = f @^-1` [set 0] /\ F = f @^-1` [set 1] + /\ f @` [set: T] = `[0, 1]%classic. + +Definition perfectly_normal_space_G_delta := + normal_space T /\ forall E : set T, closed E -> Gdelta E. + +Lemma perfectly_normal_space01P : perfectly_normal_space <-> perfectly_normal_space01. +Proof. +Admitted. + +End perfectlynormalspace. diff --git a/theories/topology_theory/separation_axioms.v b/theories/topology_theory/separation_axioms.v index 039a0f82d..452143cdf 100644 --- a/theories/topology_theory/separation_axioms.v +++ b/theories/topology_theory/separation_axioms.v @@ -1132,12 +1132,3 @@ by rewrite -(existT_inj2 lr). Qed. End sigT_separations. - -Section perfectlynormalspace. -Context (R : realType) (T : topologicalType). - -Definition perfectly_normal_space := - forall E : set T, closed E -> - exists f : T -> R, continuous f /\ E = f @^-1` [set 0]. - -End perfectlynormalspace. From 5c964153432de8687dbe4c09ffb2f0a3920ae56b Mon Sep 17 00:00:00 2001 From: Yosuke Tsuji Date: Wed, 30 Jul 2025 12:39:47 +0900 Subject: [PATCH 35/45] fix indent --- theories/borel_hierarchy.v | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) diff --git a/theories/borel_hierarchy.v b/theories/borel_hierarchy.v index a6df8b6b7..7c9867e5c 100644 --- a/theories/borel_hierarchy.v +++ b/theories/borel_hierarchy.v @@ -111,16 +111,16 @@ case:(px E cE) => f [] cf ->. pose f' := f + cst (y - x). exists f'. split. -rewrite /f'. -move=> z. -apply: continuousD. -exact:cf. -exact:cst_continuous. + rewrite /f'. + move=> z. + apply: continuousD. + exact:cf. + exact:cst_continuous. apply/seteqP. rewrite /f' /cst /=. split => z /=. -rewrite addrfctE => ->. -by rewrite subrKC. + rewrite addrfctE => ->. + by rewrite subrKC. rewrite addrfctE. move/eqP. by rewrite eq_sym -subr_eq opprB subrKC eq_sym => /eqP. From a1bd73e0ea33751e1001ee8f0e276ebbd4d24ca4 Mon Sep 17 00:00:00 2001 From: Yosuke Tsuji Date: Wed, 3 Sep 2025 17:27:09 +0900 Subject: [PATCH 36/45] WIP : add Vedenissoff theorem --- theories/borel_hierarchy.v | 35 +++++++++++++++++++++++++++++++++-- 1 file changed, 33 insertions(+), 2 deletions(-) diff --git a/theories/borel_hierarchy.v b/theories/borel_hierarchy.v index 7c9867e5c..fd90a3f81 100644 --- a/theories/borel_hierarchy.v +++ b/theories/borel_hierarchy.v @@ -126,16 +126,47 @@ move/eqP. by rewrite eq_sym -subr_eq opprB subrKC eq_sym => /eqP. Qed. +Definition perfectly_normal_space' (x : R) := + forall E : set T, open E -> + exists f : T -> R, continuous f /\ E = f @^-1` ~`[set x]. + Definition perfectly_normal_space01 := forall E F : set T, closed E -> closed F -> [disjoint E & F] -> exists f : T -> R, continuous f /\ E = f @^-1` [set 0] /\ F = f @^-1` [set 1] /\ f @` [set: T] = `[0, 1]%classic. -Definition perfectly_normal_space_G_delta := +Definition perfectly_normal_space_Gdelta := normal_space T /\ forall E : set T, closed E -> Gdelta E. -Lemma perfectly_normal_space01P : perfectly_normal_space <-> perfectly_normal_space01. +Let perfectly_normal_space_12 : perfectly_normal_space_Gdelta -> perfectly_normal_space' 0. +Proof. +Admitted. +Let perfectly_normal_space_23 : perfectly_normal_space' 0 -> perfectly_normal_space 0. +Proof. +Admitted. +Let perfectly_normal_space_34 : perfectly_normal_space 0 -> perfectly_normal_space01. +Proof. +Admitted. +Let perfectly_normal_space_41 : perfectly_normal_space01 -> perfectly_normal_space_Gdelta. Proof. Admitted. +Theorem Vedenissoff_closed : perfectly_normal_space_Gdelta <-> perfectly_normal_space 0. +Proof. +move: perfectly_normal_space_12 perfectly_normal_space_23 perfectly_normal_space_34 perfectly_normal_space_41. +tauto. +Qed. + +Theorem Vedenissoff_open : perfectly_normal_space_Gdelta <-> perfectly_normal_space' 0. +Proof. +move: perfectly_normal_space_12 perfectly_normal_space_23 perfectly_normal_space_34 perfectly_normal_space_41. +tauto. +Qed. + +Theorem Vedenissoff01 : perfectly_normal_space_Gdelta <-> perfectly_normal_space01. +Proof. +move: perfectly_normal_space_12 perfectly_normal_space_23 perfectly_normal_space_34 perfectly_normal_space_41. +tauto. +Qed. + End perfectlynormalspace. From 8edfc7ebc305a572cad2648f82a1fd6d5fa9c54c Mon Sep 17 00:00:00 2001 From: Yosuke Tsuji Date: Mon, 8 Sep 2025 11:01:01 +0900 Subject: [PATCH 37/45] rebase --- theories/showcase/sorgenfreyline.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/theories/showcase/sorgenfreyline.v b/theories/showcase/sorgenfreyline.v index 88a349cd8..3fea58237 100644 --- a/theories/showcase/sorgenfreyline.v +++ b/theories/showcase/sorgenfreyline.v @@ -3,7 +3,7 @@ From mathcomp Require Import all_ssreflect all_algebra all_fingroup. From mathcomp Require Import wochoice contra mathcomp_extra. From mathcomp Require Import boolp classical_sets set_interval. From mathcomp Require Import topology_structure separation_axioms connected. -From mathcomp Require Import reals. +From mathcomp Require Import reals borel_hierarchy. Set Implicit Arguments. Unset Strict Implicit. @@ -452,7 +452,7 @@ Qed. End distance. Lemma sorgenfrey_line_perfectly_normal_space : - perfectly_normal_space R sorgenfrey. + perfectly_normal_space sorgenfrey (0 : R). Proof. move=> E cE. exists (sdist E). From cf3b823308c69593bc7944308e91f99a9e27b34a Mon Sep 17 00:00:00 2001 From: Yosuke Tsuji Date: Mon, 8 Sep 2025 12:14:52 +0900 Subject: [PATCH 38/45] add proof of Vedenissoff --- theories/borel_hierarchy.v | 17 ++++++++++++++++- 1 file changed, 16 insertions(+), 1 deletion(-) diff --git a/theories/borel_hierarchy.v b/theories/borel_hierarchy.v index fd90a3f81..478c14981 100644 --- a/theories/borel_hierarchy.v +++ b/theories/borel_hierarchy.v @@ -141,14 +141,29 @@ Definition perfectly_normal_space_Gdelta := Let perfectly_normal_space_12 : perfectly_normal_space_Gdelta -> perfectly_normal_space' 0. Proof. Admitted. + Let perfectly_normal_space_23 : perfectly_normal_space' 0 -> perfectly_normal_space 0. Proof. -Admitted. +move=> pns' E cE. +case: (pns' (~`E)). + by rewrite openC. +move=> f [cf f0]. +exists f. +split. + by []. +by rewrite -[RHS]setCK preimage_setC -f0 setCK. +Qed. + Let perfectly_normal_space_34 : perfectly_normal_space 0 -> perfectly_normal_space01. Proof. Admitted. Let perfectly_normal_space_41 : perfectly_normal_space01 -> perfectly_normal_space_Gdelta. Proof. +move=> pns01. +split. + move=> A cA B AB. + rewrite /set_nbhs. + (*exists (~`B).*) Admitted. Theorem Vedenissoff_closed : perfectly_normal_space_Gdelta <-> perfectly_normal_space 0. From db97ab490e7460073703569a353036853c619045 Mon Sep 17 00:00:00 2001 From: Yosuke Tsuji Date: Sun, 14 Sep 2025 07:32:09 +0900 Subject: [PATCH 39/45] add proof of perfectly_normal_space_41 --- theories/borel_hierarchy.v | 15 ++++++++------- 1 file changed, 8 insertions(+), 7 deletions(-) diff --git a/theories/borel_hierarchy.v b/theories/borel_hierarchy.v index 478c14981..249c41a5c 100644 --- a/theories/borel_hierarchy.v +++ b/theories/borel_hierarchy.v @@ -144,11 +144,9 @@ Admitted. Let perfectly_normal_space_23 : perfectly_normal_space' 0 -> perfectly_normal_space 0. Proof. -move=> pns' E cE. -case: (pns' (~`E)). +move=> pns' E cE; case: (pns' (~`E)). by rewrite openC. -move=> f [cf f0]. -exists f. +move=> f [cf f0]; exists f. split. by []. by rewrite -[RHS]setCK preimage_setC -f0 setCK. @@ -161,9 +159,12 @@ Let perfectly_normal_space_41 : perfectly_normal_space01 -> perfectly_normal_spa Proof. move=> pns01. split. - move=> A cA B AB. - rewrite /set_nbhs. - (*exists (~`B).*) + move=> A cA B /set_nbhsP [C] [oC] AC. + have:= pns01 A (~`C) cA. + case. by apply: open_closedC. by apply/disj_setPCl. + move=> f [cf [f0 [f1 f01]]]. + exists (f @^-1` `[0, 1/2 [). + move=> a Aa. Admitted. Theorem Vedenissoff_closed : perfectly_normal_space_Gdelta <-> perfectly_normal_space 0. From 256f266c44278dbe708ae89e5712865c2c6642f3 Mon Sep 17 00:00:00 2001 From: Yosuke Tsuji Date: Wed, 17 Sep 2025 15:51:52 +0900 Subject: [PATCH 40/45] proof Lemmas perfectly_normal_space01_normal and perfectly_normal_space_41 --- theories/borel_hierarchy.v | 62 +++++++++++++++++++++++++++++++++----- 1 file changed, 54 insertions(+), 8 deletions(-) diff --git a/theories/borel_hierarchy.v b/theories/borel_hierarchy.v index 249c41a5c..3cef0c56b 100644 --- a/theories/borel_hierarchy.v +++ b/theories/borel_hierarchy.v @@ -19,7 +19,7 @@ Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. -Import Order.TTheory GRing.Theory Num.Theory. +Import Order.TTheory GRing.Theory Num.Theory Num.Def. Import numFieldNormedType.Exports. Import numFieldTopology.Exports. @@ -138,6 +138,33 @@ Definition perfectly_normal_space01 := Definition perfectly_normal_space_Gdelta := normal_space T /\ forall E : set T, closed E -> Gdelta E. +Lemma perfectly_normal_space01_normal : + perfectly_normal_space01 -> normal_space T. +Proof. +move=> pns01 A cA B /set_nbhsP[C] [oC AC CB]. +case: (pns01 A (~` C) cA). +- by rewrite closedC. +- exact/disj_setPCl. +move=> f [/continuousP /= cf] [f0] [f1] f01. +exists (f @^-1` `]-oo, 1/2]). + apply/set_nbhsP. + exists (f @^-1` `]-oo, 1/2[). + split => //. + - exact: cf. + - by rewrite f0 => x /= ->; rewrite in_itv /=. + - by apply: preimage_subset => x /=; rewrite !in_itv /=; apply: ltW. +apply: subset_trans CB. +have<-:= proj1 (closure_id _). + have<-:= (setCK C). + rewrite f1 preimage_setC. + apply: preimage_subset => x /=; rewrite in_itv /=. + apply: contraTnot => ->. + by rewrite -ltNge ltr_pdivrMr // mul1r ltr1n. +have/continuousP /continuous_closedP:= cf. +apply. +exact: lray_closed. +Qed. + Let perfectly_normal_space_12 : perfectly_normal_space_Gdelta -> perfectly_normal_space' 0. Proof. Admitted. @@ -155,17 +182,36 @@ Qed. Let perfectly_normal_space_34 : perfectly_normal_space 0 -> perfectly_normal_space01. Proof. Admitted. + Let perfectly_normal_space_41 : perfectly_normal_space01 -> perfectly_normal_space_Gdelta. Proof. move=> pns01. split. - move=> A cA B /set_nbhsP [C] [oC] AC. - have:= pns01 A (~`C) cA. - case. by apply: open_closedC. by apply/disj_setPCl. - move=> f [cf [f0 [f1 f01]]]. - exists (f @^-1` `[0, 1/2 [). - move=> a Aa. -Admitted. + exact: perfectly_normal_space01_normal. +move=> E cE. +have [] := pns01 _ _ cE closed0. + by apply/disj_setPLR; rewrite setC0. +move=> f [cf] [f0] [f1] f01. +exists (fun n => f @^-1` `]-oo, 1/n.+1%:R[). + move=> n; move/continuousP: cf; exact. +rewrite f0. +apply/seteqP; split => x /= Hx. + by move=> i _ /=; rewrite Hx in_itv /= divr_gt0. +case: (ltrgtP (f x) 0) => // fx. + have : f x \notin range f. + by rewrite f01 mem_setE in_itv /= negb_and -ltNge fx. + move/negP; elim. + by rewrite inE /=; exists x. +suff : False by []. +have /= := Hx (truncn (1 / f x)) I. +rewrite in_itv /=. +have /real_truncnS_gt := num_real (1 / f x). +rewrite -ltf_pV2; last first. +- by rewrite posrE divr_gt0. +- by rewrite posrE. +rewrite !div1r invrK => /lt_trans/[apply]. +by rewrite ltxx. +Qed. Theorem Vedenissoff_closed : perfectly_normal_space_Gdelta <-> perfectly_normal_space 0. Proof. From d8f163255aabc19bc120e50f41e4f65bfcf22576 Mon Sep 17 00:00:00 2001 From: Yosuke Tsuji Date: Wed, 1 Oct 2025 10:03:53 +0900 Subject: [PATCH 41/45] rename and add Vedenissof proof --- theories/borel_hierarchy.v | 94 ++++++++++++++++++++++++++------------ 1 file changed, 64 insertions(+), 30 deletions(-) diff --git a/theories/borel_hierarchy.v b/theories/borel_hierarchy.v index 3cef0c56b..4c663fe1b 100644 --- a/theories/borel_hierarchy.v +++ b/theories/borel_hierarchy.v @@ -165,11 +165,46 @@ apply. exact: lray_closed. Qed. -Let perfectly_normal_space_12 : perfectly_normal_space_Gdelta -> perfectly_normal_space' 0. +Let perfectly_normal_space_12 : perfectly_normal_space_Gdelta -> perfectly_normal_space 0. Proof. +move=> pnsGd E cE. +case: (pnsGd) => nT cEGdE. +have[U oU hE]:= cEGdE E cE. +have/boolp.choice[f_n Hn]: forall n, exists f : T -> R, + [/\ continuous f, range f `<=` `[0, 1], f @` E `<=` [set 0] & f @` (~` U n) `<=` [set 1]]. + move=> n. + apply/uniform_separatorP. + apply: normal_uniform_separator => //. + - by rewrite closedC. + - rewrite hE. + rewrite -subsets_disjoint. + exact: bigcap_inf. +pose f := fun x => (\sum_(n perfectly_normal_space 0. +Let perfectly_normal_space_13 : perfectly_normal_space_Gdelta -> perfectly_normal_space' 0. +move=> pnsGd E oE. +case: (pnsGd) => nT cEGdE. +have clcpE: closed (~`E). + by rewrite closedC. +have[U oU hE]:= cEGdE (~` E) clcpE. +have/boolp.choice[f_n Hn]: forall n, exists f : T -> R, + [/\ continuous f, range f `<=` `[0, 1], f @` (~` E) `<=` [set 0] & f @` (~` U n) `<=` [set 1]]. + move=> n. + apply/uniform_separatorP. + apply: normal_uniform_separator => //. + - by rewrite closedC. + - rewrite hE. + rewrite -subsets_disjoint. + exact: bigcap_inf. +Admitted. + +Let perfectly_normal_space_23 : perfectly_normal_space 0 -> perfectly_normal_space' 0. +Proof. +Admitted. + +Let perfectly_normal_space_32 : perfectly_normal_space' 0 -> perfectly_normal_space 0. Proof. move=> pns' E cE; case: (pns' (~`E)). by rewrite openC. @@ -179,38 +214,37 @@ split. by rewrite -[RHS]setCK preimage_setC -f0 setCK. Qed. -Let perfectly_normal_space_34 : perfectly_normal_space 0 -> perfectly_normal_space01. +Let perfectly_normal_space_24 : perfectly_normal_space 0 -> perfectly_normal_space01. Proof. Admitted. -Let perfectly_normal_space_41 : perfectly_normal_space01 -> perfectly_normal_space_Gdelta. +Let perfectly_normal_space_34 : perfectly_normal_space' 0 -> perfectly_normal_space01. Proof. -move=> pns01. -split. - exact: perfectly_normal_space01_normal. -move=> E cE. -have [] := pns01 _ _ cE closed0. - by apply/disj_setPLR; rewrite setC0. -move=> f [cf] [f0] [f1] f01. -exists (fun n => f @^-1` `]-oo, 1/n.+1%:R[). - move=> n; move/continuousP: cf; exact. -rewrite f0. -apply/seteqP; split => x /= Hx. - by move=> i _ /=; rewrite Hx in_itv /= divr_gt0. -case: (ltrgtP (f x) 0) => // fx. - have : f x \notin range f. - by rewrite f01 mem_setE in_itv /= negb_and -ltNge fx. - move/negP; elim. - by rewrite inE /=; exists x. -suff : False by []. -have /= := Hx (truncn (1 / f x)) I. -rewrite in_itv /=. -have /real_truncnS_gt := num_real (1 / f x). -rewrite -ltf_pV2; last first. -- by rewrite posrE divr_gt0. -- by rewrite posrE. -rewrite !div1r invrK => /lt_trans/[apply]. -by rewrite ltxx. +Admitted. + +Local Lemma perfectly_normal_space_42 : +perfectly_normal_space01 -> perfectly_normal_space 0. +Proof. +move=> + E cE => /(_ E set0 cE closed0). +rewrite disj_set2E setI0 eqxx => /(_ erefl). +case=> f [] cf [] Ef [] _ _. +by exists f; split. +Qed. + +Let perfectly_normal_space_41 : + perfectly_normal_space01 -> perfectly_normal_space_Gdelta. +Proof. +move=> pns01; split; first exact: perfectly_normal_space01_normal. +move=> E cE; case:(perfectly_normal_space_42 pns01 cE) => // f [] cf Ef. +exists (fun n => f @^-1` `]-n.+1%:R^-1,n.+1%:R^-1[%classic). + by move=> n; move/continuousP: cf; apply; exact: itv_open. +rewrite -preimage_bigcap (_ : bigcap _ _ = [set 0])//. +rewrite eqEsubset; split; last first. + by move=> x -> n _ /=; rewrite in_itv//= oppr_lt0 andbb invr_gt0. +apply: subsetC2; rewrite setC_bigcap => x /= /eqP x0. +exists (trunc `|x^-1|) => //=; rewrite in_itv/= -ltr_norml ltNge. +apply/negP; rewrite negbK. +by rewrite invf_ple ?posrE// ?normr_gt0// -normfV ltW// truncnS_gt. Qed. Theorem Vedenissoff_closed : perfectly_normal_space_Gdelta <-> perfectly_normal_space 0. From 6a8942c9f407465dd4769ef2c7ad209a80dd67d1 Mon Sep 17 00:00:00 2001 From: Yosuke Tsuji Date: Wed, 1 Oct 2025 22:07:45 +0900 Subject: [PATCH 42/45] add proof of perfectly_normal_space_12 --- theories/borel_hierarchy.v | 37 +++++++++++++++++++++++++++++++++++-- 1 file changed, 35 insertions(+), 2 deletions(-) diff --git a/theories/borel_hierarchy.v b/theories/borel_hierarchy.v index 4c663fe1b..ad2872912 100644 --- a/theories/borel_hierarchy.v +++ b/theories/borel_hierarchy.v @@ -22,6 +22,7 @@ Unset Printing Implicit Defensive. Import Order.TTheory GRing.Theory Num.Theory Num.Def. Import numFieldNormedType.Exports. Import numFieldTopology.Exports. +Import exp. Local Open Scope classical_set_scope. Local Open Scope ring_scope. @@ -179,8 +180,40 @@ have/boolp.choice[f_n Hn]: forall n, exists f : T -> R, - rewrite hE. rewrite -subsets_disjoint. exact: bigcap_inf. -pose f := fun x => (\sum_(n \sum_(k < n) (f_n k \* cst (2^-k.+1)). +rewrite /= in f_sum. +have cf_sum n : continuous (f_sum n). + move=> x. + elim: n => [| n IH]. + - rewrite /f_sum big_ord0. + exact: cst_continuous. + - rewrite /f_sum big_ord_recr /=. + apply: continuousD. + exact IH. + apply: continuousM. + by case: (Hn n) => /(_ x). + exact: cst_continuous. +pose f := fun x => limn (f_sum^~ x). +rewrite /= in f. +exists f. +split. + move=> x nfx. + rewrite -filter_from_ballE. + case. + move=> eps /= eps0 epsB. + pose n := (2 + truncn (- ln eps / ln 2))%N. + move: (cf_sum n). + have eps0' : eps / 2 > 0 by exact: divr_gt0. + move/continuousP/(_ _ (ball_open (f_sum n x) eps0')) : (cf_sum n) => /= ofs. + rewrite nbhs_filterE. + rewrite fmapE. + rewrite nbhsE /=. + set B := _ @^-1` _ in ofs. + exists B. + split => //. + exact: ballxx. + apply: subset_trans (preimage_subset (f:=f) epsB). + rewrite /B /preimage /ball => t /=. Admitted. Let perfectly_normal_space_13 : perfectly_normal_space_Gdelta -> perfectly_normal_space' 0. From cfcadcb235c4c3a58ae11b5ebaba000a1f91e10f Mon Sep 17 00:00:00 2001 From: Jacques Garrigue Date: Thu, 2 Oct 2025 11:52:26 +0900 Subject: [PATCH 43/45] wip --- theories/borel_hierarchy.v | 83 ++++++++++++++++++++++++++++++-------- 1 file changed, 66 insertions(+), 17 deletions(-) diff --git a/theories/borel_hierarchy.v b/theories/borel_hierarchy.v index ad2872912..84de51d70 100644 --- a/theories/borel_hierarchy.v +++ b/theories/borel_hierarchy.v @@ -180,29 +180,25 @@ have/boolp.choice[f_n Hn]: forall n, exists f : T -> R, - rewrite hE. rewrite -subsets_disjoint. exact: bigcap_inf. -pose f_sum := fun n => \sum_(k < n) (f_n k \* cst (2^-k.+1)). -rewrite /= in f_sum. +pose f_sum := fun n => \sum_(0 <= k < n) (f_n k \* cst (2^-k.+1)). have cf_sum n : continuous (f_sum n). - move=> x. - elim: n => [| n IH]. - - rewrite /f_sum big_ord0. - exact: cst_continuous. - - rewrite /f_sum big_ord_recr /=. - apply: continuousD. - exact IH. - apply: continuousM. - by case: (Hn n) => /(_ x). - exact: cst_continuous. + rewrite /f_sum => x; elim: n => [|n IH]. + rewrite big_geq //; exact: cst_continuous. + rewrite big_nat_recr //=; apply: continuousD => //. + apply/continuousM/cst_continuous. + by case: (Hn n) => /(_ x). +have f_sumE x n : f_sum n x = \sum_(0 <= k < n) (f_n k x * 2^-k.+1). + rewrite /f_sum. + elim: n => [|n IH]; first by rewrite !big_geq. + by rewrite !big_nat_recr //= [X in X _ _ x]/GRing.add /= IH. pose f := fun x => limn (f_sum^~ x). rewrite /= in f. exists f. split. - move=> x nfx. + move=> x Nfx. rewrite -filter_from_ballE. - case. - move=> eps /= eps0 epsB. + case => eps /= eps0 HB. pose n := (2 + truncn (- ln eps / ln 2))%N. - move: (cf_sum n). have eps0' : eps / 2 > 0 by exact: divr_gt0. move/continuousP/(_ _ (ball_open (f_sum n x) eps0')) : (cf_sum n) => /= ofs. rewrite nbhs_filterE. @@ -212,8 +208,61 @@ split. exists B. split => //. exact: ballxx. - apply: subset_trans (preimage_subset (f:=f) epsB). + apply: subset_trans (preimage_subset (f:=f) HB). rewrite /B /preimage /ball => t /=. + have ndf_sum y : {homo f_sum^~ y : a b / (a <= b)%N >-> a <= b}. + move=> a b ab. + rewrite /f_sum. + rewrite (big_cat_nat _ ab) //= lerDl. + elim/big_rec: _ => //= i f0 _. + rewrite /GRing.add /= => /le_trans; apply. + rewrite lerDr mulr_ge0 //. + case: (Hn i) => _ Hr _ _. + have /Hr /= := imageT (f_n i) y. + by rewrite in_itv /= => /andP[]. + by rewrite invr_ge0 exprn_ge0. + have Hcvg y : cvgn (f_sum^~ y). + apply: nondecreasing_is_cvgn => //. + exists 1 => z /= [m] _ <-. + rewrite /f_sum. + apply: (@le_trans _ _ (1 - 2^-m)); last first. + by rewrite gerBl invr_ge0 exprn_ge0. + elim: m => [|m IH]. + by rewrite big_geq // expr0 invr1 subrr. + rewrite big_nat_recr //=. + have Hm : f_n m y * 2 ^- m.+1 <= 2 ^- m.+1. + case: (Hn m) => _ Hr _ _. + have /Hr /= := imageT (f_n m) y. + rewrite in_itv /= => /andP[f0 f1]. + by rewrite -[leRHS]mul1r ler_pM. + apply: (le_trans (lerD IH Hm)). + rewrite -addrA. + have -> : 2^- m = 2 * 2^-m.+1 :> R. + by rewrite exprS invfM mulrA mulfV // mul1r. + rewrite -{1}add1n {1}mulrnDr mulrDl !mul1r opprD !addrA -addrA. + by rewrite [_ + 2^- _]addrC subrr addr0. + have Hf y : + f y = f_sum n y + limn (fun n' => \sum_(n <= k < n') f_n k y * 2^- k.+1). + have /= := nondecreasing_telescope_sumey n _ (ndf_sum y). + rewrite EFin_lim // fin_numE /= => /(_ isT). + rewrite (eq_eseriesr (g:=fun i => ((f_n i \* cst (2 ^- i.+1)) y)%:E)); + last first. + move => i _. + rewrite /f_sum -EFinD big_nat_recr //=. + by rewrite [X in X _ _ y]/GRing.add /= addrAC subrr add0r. + move/(f_equal (fun x => (f_sum n y)%:E + x)). + rewrite addrA addrAC -EFinB subrr add0r => H. + apply: EFin_inj. + rewrite -H EFinD; congr (_ + _). + rewrite -EFin_lim. + apply/congr_lim/boolp.funext => k /=. + elim: k => [|k IH]; first by rewrite !big_geq. + case: (leP n k) => nk. + by rewrite !big_nat_recr //= IH EFinD. + by rewrite !big_geq. + rewrite is_cvg_series_restrict /series /mk_sequence. + under [X in cvgn X]boolp.funext do rewrite -f_sumE. + exact: Hcvg. Admitted. Let perfectly_normal_space_13 : perfectly_normal_space_Gdelta -> perfectly_normal_space' 0. From 5702fc15c8dda9e83b958208f3b871069c5474b8 Mon Sep 17 00:00:00 2001 From: Jacques Garrigue Date: Thu, 2 Oct 2025 17:29:23 +0900 Subject: [PATCH 44/45] 1 -> 2 almost done --- theories/borel_hierarchy.v | 112 ++++++++++++++++++++++++------------- 1 file changed, 73 insertions(+), 39 deletions(-) diff --git a/theories/borel_hierarchy.v b/theories/borel_hierarchy.v index 84de51d70..d4df88b9f 100644 --- a/theories/borel_hierarchy.v +++ b/theories/borel_hierarchy.v @@ -166,19 +166,26 @@ apply. exact: lray_closed. Qed. +Lemma EFin_series (f : R^nat) : EFin \o series f = eseries (EFin \o f). +Proof. +apply/boolp.funext => n. +rewrite /series /eseries /=. +elim: n => [|n IH]; first by rewrite !big_geq. +by rewrite !big_nat_recr //= EFinD IH. +Qed. + Let perfectly_normal_space_12 : perfectly_normal_space_Gdelta -> perfectly_normal_space 0. Proof. move=> pnsGd E cE. case: (pnsGd) => nT cEGdE. -have[U oU hE]:= cEGdE E cE. +have[U oU HE]:= cEGdE E cE. have/boolp.choice[f_n Hn]: forall n, exists f : T -> R, [/\ continuous f, range f `<=` `[0, 1], f @` E `<=` [set 0] & f @` (~` U n) `<=` [set 1]]. move=> n. apply/uniform_separatorP. apply: normal_uniform_separator => //. - by rewrite closedC. - - rewrite hE. - rewrite -subsets_disjoint. + - rewrite HE -subsets_disjoint. exact: bigcap_inf. pose f_sum := fun n => \sum_(0 <= k < n) (f_n k \* cst (2^-k.+1)). have cf_sum n : continuous (f_sum n). @@ -187,13 +194,46 @@ have cf_sum n : continuous (f_sum n). rewrite big_nat_recr //=; apply: continuousD => //. apply/continuousM/cst_continuous. by case: (Hn n) => /(_ x). -have f_sumE x n : f_sum n x = \sum_(0 <= k < n) (f_n k x * 2^-k.+1). - rewrite /f_sum. +have f_sumE x : f_sum ^~ x = [series f_n k x * 2^-k.+1]_k. + apply/boolp.funext => n. + rewrite /f_sum /series /mk_sequence. elim: n => [|n IH]; first by rewrite !big_geq. by rewrite !big_nat_recr //= [X in X _ _ x]/GRing.add /= IH. pose f := fun x => limn (f_sum^~ x). rewrite /= in f. exists f. +have ndf_sum y : {homo f_sum^~ y : a b / (a <= b)%N >-> a <= b}. + move=> a b ab. + rewrite /f_sum. + rewrite (big_cat_nat _ ab) //= lerDl. + elim/big_rec: _ => //= i f0 _. + rewrite /GRing.add /= => /le_trans; apply. + rewrite lerDr mulr_ge0 //. + case: (Hn i) => _ Hr _ _. + have /Hr /= := imageT (f_n i) y. + by rewrite in_itv /= => /andP[]. + by rewrite invr_ge0 exprn_ge0. +(*have Hub y m k : (\sum_(m <= i < k) f_n i \* cst (2 ^- i.+1)) y <= 2^-m. + apply: (@le_trans _ _ (2^-m - 2^-k)); last first. + by rewrite gerBl invr_ge0 exprn_ge0.*) +have Hcvg y : cvgn (f_sum^~ y). + apply: nondecreasing_is_cvgn => //. + exists 1 => z /= [m] _ <-. + rewrite /f_sum. + apply: (@le_trans _ _ (1 - 2^-m)); last by rewrite gerBl invr_ge0 exprn_ge0. + elim: m => [|m IH]; first by rewrite big_geq // expr0 invr1 subrr. + rewrite big_nat_recr //=. + have Hm : f_n m y * 2 ^- m.+1 <= 2 ^- m.+1. + case: (Hn m) => _ Hr _ _. + have /Hr /= := imageT (f_n m) y. + rewrite in_itv /= => /andP[f0 f1]. + by rewrite -[leRHS]mul1r ler_pM. + apply: (le_trans (lerD IH Hm)). + rewrite -addrA. + have -> : 2^- m = 2 * 2^-m.+1 :> R. + by rewrite exprS invfM mulrA mulfV // mul1r. + rewrite -{1}add1n {1}mulrnDr mulrDl !mul1r opprD !addrA -addrA. + by rewrite [_ + 2^- _]addrC subrr addr0. split. move=> x Nfx. rewrite -filter_from_ballE. @@ -210,37 +250,6 @@ split. exact: ballxx. apply: subset_trans (preimage_subset (f:=f) HB). rewrite /B /preimage /ball => t /=. - have ndf_sum y : {homo f_sum^~ y : a b / (a <= b)%N >-> a <= b}. - move=> a b ab. - rewrite /f_sum. - rewrite (big_cat_nat _ ab) //= lerDl. - elim/big_rec: _ => //= i f0 _. - rewrite /GRing.add /= => /le_trans; apply. - rewrite lerDr mulr_ge0 //. - case: (Hn i) => _ Hr _ _. - have /Hr /= := imageT (f_n i) y. - by rewrite in_itv /= => /andP[]. - by rewrite invr_ge0 exprn_ge0. - have Hcvg y : cvgn (f_sum^~ y). - apply: nondecreasing_is_cvgn => //. - exists 1 => z /= [m] _ <-. - rewrite /f_sum. - apply: (@le_trans _ _ (1 - 2^-m)); last first. - by rewrite gerBl invr_ge0 exprn_ge0. - elim: m => [|m IH]. - by rewrite big_geq // expr0 invr1 subrr. - rewrite big_nat_recr //=. - have Hm : f_n m y * 2 ^- m.+1 <= 2 ^- m.+1. - case: (Hn m) => _ Hr _ _. - have /Hr /= := imageT (f_n m) y. - rewrite in_itv /= => /andP[f0 f1]. - by rewrite -[leRHS]mul1r ler_pM. - apply: (le_trans (lerD IH Hm)). - rewrite -addrA. - have -> : 2^- m = 2 * 2^-m.+1 :> R. - by rewrite exprS invfM mulrA mulfV // mul1r. - rewrite -{1}add1n {1}mulrnDr mulrDl !mul1r opprD !addrA -addrA. - by rewrite [_ + 2^- _]addrC subrr addr0. have Hf y : f y = f_sum n y + limn (fun n' => \sum_(n <= k < n') f_n k y * 2^- k.+1). have /= := nondecreasing_telescope_sumey n _ (ndf_sum y). @@ -260,9 +269,34 @@ split. case: (leP n k) => nk. by rewrite !big_nat_recr //= IH EFinD. by rewrite !big_geq. - rewrite is_cvg_series_restrict /series /mk_sequence. - under [X in cvgn X]boolp.funext do rewrite -f_sumE. - exact: Hcvg. + move: (Hcvg y). + by rewrite is_cvg_series_restrict f_sumE. + move=> feps. + rewrite !Hf opprD addrA (addrAC (f_sum n x)) -(addrA (_ - _)). + apply: (le_lt_trans (ler_normD _ _)). + rewrite (splitr eps). + apply: ltr_leD => //. + admit. +apply/seteqP; split => x /= Hx. + apply: EFin_inj. + rewrite -EFin_lim // f_sumE EFin_series /= eseries0 // => i _ _ /=. + case: (Hn i) => _ _ /(_ (f_n i x)) /= => ->. + by rewrite mul0r. + by exists x. +apply: contraPP Hx. +rewrite (_ : (~ E x) = setC E x) // HE setC_bigcap /= => -[] i _ HU. +case: (Hn i) => _ _ _ /(_ (f_n i x)) /= => Hfix. +rewrite /f => Hf. +have := (nondecreasing_cvgn_le (ndf_sum x) (Hcvg x) i.+1). +have := ndf_sum x _ _ (leq0n i.+1). +rewrite Hf {1}/f_sum big_geq // => /[swap] fi_le0. +rewrite le0r ltNge fi_le0 orbF. +rewrite /f_sum big_nat_recr //= [X in X _ _ x]/GRing.add /= -/(f_sum i). +rewrite Hfix; last by exists x. +rewrite mul1r /cst => /eqP fi0. +have := ndf_sum x _ _ (leq0n i). +rewrite {1}/f_sum big_geq // -[0 x]fi0 gerDl. +by rewrite leNgt invr_gt0 exprn_gt0. Admitted. Let perfectly_normal_space_13 : perfectly_normal_space_Gdelta -> perfectly_normal_space' 0. From b9fb7a78bae72e4871e4524e448fca0c5e0b1f66 Mon Sep 17 00:00:00 2001 From: Jacques Garrigue Date: Mon, 6 Oct 2025 19:13:10 +0900 Subject: [PATCH 45/45] use big_morph --- theories/borel_hierarchy.v | 8 ++------ 1 file changed, 2 insertions(+), 6 deletions(-) diff --git a/theories/borel_hierarchy.v b/theories/borel_hierarchy.v index d4df88b9f..5df9953c4 100644 --- a/theories/borel_hierarchy.v +++ b/theories/borel_hierarchy.v @@ -197,8 +197,7 @@ have cf_sum n : continuous (f_sum n). have f_sumE x : f_sum ^~ x = [series f_n k x * 2^-k.+1]_k. apply/boolp.funext => n. rewrite /f_sum /series /mk_sequence. - elim: n => [|n IH]; first by rewrite !big_geq. - by rewrite !big_nat_recr //= [X in X _ _ x]/GRing.add /= IH. + exact: (big_morph (fun f => f x)). pose f := fun x => limn (f_sum^~ x). rewrite /= in f. exists f. @@ -265,10 +264,7 @@ split. rewrite -H EFinD; congr (_ + _). rewrite -EFin_lim. apply/congr_lim/boolp.funext => k /=. - elim: k => [|k IH]; first by rewrite !big_geq. - case: (leP n k) => nk. - by rewrite !big_nat_recr //= IH EFinD. - by rewrite !big_geq. + exact/esym/big_morph. move: (Hcvg y). by rewrite is_cvg_series_restrict f_sumE. move=> feps.