From 8bcd64e0ce3533642c157010bf061c47d7217284 Mon Sep 17 00:00:00 2001 From: zstone Date: Wed, 31 Aug 2022 00:45:55 -0400 Subject: [PATCH 1/3] homotopies debugging canonical issue homotopy stuff more homotopy stuff path chains path connected is an equivalence relation trying to define parametrization doing subspace topology stuff fixing near continuous cleaned up realfun things build correctly changelog and linting fixing changelog getting there on paths reversing paths more stuff about continuous HB proving group properties no simple way around injectivity associative proof moving stuff itv changes awful split domain proofs path linking respects quotients definition of path --- CHANGELOG_UNRELEASED.md | 3 + theories/homotopy.v | 766 ++++++++++++++++++++++++++++++++++++++ theories/mathcomp_extra.v | 604 ++++++++++++++++++++++++++++++ theories/real_interval.v | 7 + theories/topology.v | 33 +- 5 files changed, 1403 insertions(+), 10 deletions(-) create mode 100644 theories/homotopy.v create mode 100644 theories/mathcomp_extra.v diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 6e4b434fb..8f404e04f 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -126,6 +126,7 @@ + generalize `lte_addl`, `lte_addr`, `gte_subl`, `gte_subr`, `lte_daddl`, `lte_daddr`, `gte_dsubl`, `gte_dsubr` - in `topology.v`: + + lemma `weak_subspace_open` + lemmas `continuous_subspace0`, `continuous_subspace1` - in `realfun.v`: @@ -183,6 +184,8 @@ + lemma `lte_spaddr`, renamed `lte_spaddre` ### Removed +- in `realFun.v`: + + removed `continuous_subspace_itv` - in file `classical_sets.v`: + lemmas `pred_oappE` and `pred_oapp_set` (moved to `mathcomp_extra.v`) diff --git a/theories/homotopy.v b/theories/homotopy.v new file mode 100644 index 000000000..b99fd7503 --- /dev/null +++ b/theories/homotopy.v @@ -0,0 +1,766 @@ +(* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C. *) +From mathcomp Require Import all_ssreflect ssralg ssrint ssrnum matrix. +From mathcomp Require Import interval rat generic_quotient. +Require Import mathcomp_extra boolp reals ereal set_interval classical_sets. +Require Import signed functions topology normedtype landau sequences derive. +Require Import realfun. +From HB Require Import structures. + +Add Search Blacklist "__canonical__". +Add Search Blacklist "__functions_". +Add Search Blacklist "_factory_". +Add Search Blacklist "_mixin_". + +(******************************************************************************) +(* Definitions and lemmas for homotopy theory *) +(* *) +(* *) +(******************************************************************************) + +Set Implicit Arguments. +Unset Strict Implicit. +Unset Printing Implicit Defensive. +Import Order.TTheory GRing.Theory Num.Def Num.Theory. +Import numFieldNormedType.Exports. + +Local Open Scope classical_set_scope. +Local Open Scope ring_scope. +Local Open Scope quotient_scope. + +HB.mixin Record IsContinuous {T U : topologicalType} (A : set T) (f : T -> U) := + { continuous_fun : {within A, continuous f }}. + +HB.structure Definition JustContinuous {T U : topologicalType} A + := {f of @IsContinuous T U A f}. + +HB.structure Definition ContinuousFun {T U : topologicalType} + (A : set T) (B : set U) := + {f of @IsContinuous T U A f & @Fun T U A B f}. + +Notation "{ 'continuous' A >-> B }" := + (@ContinuousFun.type _ _ A B) : form_scope. +Notation "[ 'continuous' 'of' f ]" := + ([the (@ContinuousFun.type _ _ _ _) of (f: _ -> _)]) : form_scope. + +Canonical continuous_eq {T U : topologicalType} (A : set T) (B : set U) := + EqType {continuous A >-> B} gen_eqMixin. +Canonical continuous_choice {T U : topologicalType} (A : set T) (B : set U) := + ChoiceType {continuous A >-> B} gen_choiceMixin . + +HB.mixin Record IsParametrization {R : realType} (f : R -> R) := + { + parametrize_init : f 0 = 0; + parametrize_final : f 1 = 1; + }. + +HB.structure Definition JustParametrization {R : realType} + := {f of @IsParametrization R f}. + +HB.structure Definition Parametrization {R : realType} + := {f of @IsParametrization R f & + @IsContinuous R R `[0,1]%classic f & + @Fun R R `[0,1]%classic `[0,1]%classic f }. + +HB.structure Definition InjParametrization {R : realType} + := {f of @Parametrization R f & + @SplitInj R R `[0,1]%classic f }. + +Notation "{ 'parametrization' R }" := (@Parametrization.type R) : form_scope. +Notation "[ 'parametrization' 'of' f ]" := + ([the (@Parametrization.type _) of (f: _ -> _)]) : form_scope. + +Notation "{ 'inj_parametrization' R }" := (@InjParametrization.type R) : form_scope. +Notation "[ 'inj_parametrization' 'of' f ]" := + ([the (@InjParametrization.type _) of (f: _ -> _)]) : form_scope. + +Section continuous_hb_basics. +Section composition. +Context {T U V : topologicalType} {A : set T} {B : set U} {C : set V}. + +Local Lemma comp_continuous (f : {continuous A >-> B}) (g : {continuous B >-> C}) : + IsContinuous _ _ A (g \o f). +Proof. split => x; apply: (@continuous_comp + (subspace_topologicalType A) (subspace_topologicalType B) _). + exact/subspaceT_continuous/continuous_fun. +exact: continuous_fun. +Qed. + +HB.instance Definition funcomp f g := comp_continuous f g. +End composition. + +Section identity. +Context {T : topologicalType} {A : set T}. +Local Lemma cts_identity : IsContinuous _ _ A (@idfun T). +Proof. by split => x; exact: continuous_subspaceT. Qed. +HB.instance Definition _ := cts_identity. +End identity. + +Section constants. +Context {T U : topologicalType} {A : set T}. +Local Lemma cts_const (y : U) : IsContinuous _ _ A (cst y). +Proof. by split => x; exact: cst_continuous. Qed. +HB.instance Definition _ (y : U) := cts_const y. +End constants. + +Section affine. +Context {R : realType}. +Definition affine (a b x: R) : R := a * x + b. + +Lemma affine_comp a b c d : affine a b \o affine c d = + affine (a * c) (a * d + b). +Proof. by apply: funext => r /=; rewrite /affine mulrDr mulrA addrA. Qed. + +Lemma affine_id a : a != 0 -> affine a 0 \o affine (1/a) 0 = id. +Proof. +move=> an0; apply: funext => r; rewrite affine_comp div1r divrr ?unitfE //. +by rewrite /affine mulr0 ?addr0 mul1r. +Qed. + +Lemma affine_ctsT (a b : R) : continuous (affine a b). +Proof. +rewrite /affine => r; apply: cvgD; last exact: cvg_cst; exact: mulrl_continuous. +Qed. + +Local Lemma cts_affine (a b : R) A : IsContinuous R R A (affine a b). +Proof. +split => x; apply: continuous_subspaceT; exact: affine_ctsT. +Qed. + +HB.instance Definition _ (a b : R) A := cts_affine a b A. + +Local Lemma affine_pitv_ccE a b x y r : + 0 < a -> + affine a b r \in `[x, y]%classic = (r \in `[(x - b)/a, (y-b)/a]%classic). +Proof. +rewrite ?in_itv /= ?ler_pdivl_mulr ?[2 * _]mulrC // ?mem_setE ?in_itv. +move: a => _/posnumP[a] /=; rewrite /affine/=. +apply: Bool.eq_true_iff_eq; split => /andP [] P Q; apply/andP; split. +- by rewrite ler_pdivr_mulr // ler_subl_addr mulrC. +- by rewrite ler_pdivl_mulr // -ler_subl_addr mulrC opprK. +- by rewrite -ler_subl_addr mulrC -ler_pdivr_mulr. +- by rewrite -[b]opprK - mulrC ler_subl_addr -ler_pdivl_mulr. +Qed. + +Local Lemma affine_pitv_ocE a b x y r : + 0 < a -> + affine a b r \in `]x, y]%classic = (r \in `](x - b)/a, (y-b)/a]%classic). +Proof. +rewrite ?in_itv /= ?ler_pdivl_mulr ?[2 * _]mulrC // ?mem_setE ?in_itv. +move: a => _/posnumP[a] /=; rewrite /affine/=. +apply: Bool.eq_true_iff_eq; split => /andP [] P Q; apply/andP; split. +- by rewrite ltr_pdivr_mulr // ltr_subl_addr mulrC. +- by rewrite ler_pdivl_mulr // -ler_subl_addr mulrC opprK. +- by rewrite -ltr_subl_addr mulrC -ltr_pdivr_mulr. +- by rewrite -[b]opprK - mulrC ler_subl_addr -ler_pdivl_mulr. +Qed. + +Local Lemma affine_pmono (a b : R) : + 0 < a -> {mono (affine a b) : x y / x <= y }. +Proof. +by move: a => _/posnumP[a] => x y; rewrite /affine ler_add2r ler_pmul2l. +Qed. + +Variables (a : {posnum R}) (b x y :R). +Local Lemma affine_fun_pitv : + @set_fun R R `[x,y]%classic `[a%:num*x + b, a%:num * y + b]%classic + (affine a%:num b). +Proof. +move=> r /itvP rxy; rewrite /= in_itv; apply/andP. +by split => /=; rewrite /affine ler_add2r ler_wpmul2l // rxy. +Qed. + +HB.instance Definition F := IsFun.Build _ _ _ _ _ affine_fun_pitv. + +Definition affine_fun : {continuous `[x,y] >-> `[a%:num*x + b, a%:num * y + b]} := + [continuous of (affine a%:num b)]. + +End affine. + +End continuous_hb_basics. + +Section SplitDomain. +Context {R : realType}. +Implicit Types T : topologicalType. +Let split_domain_aux {T} (f g: R -> T) := + (patch (g \o (affine 1 (-1))) (`[0,1]%classic) f). + +Lemma split_domain_auxP {T} f g x : x \in `[0,2] -> + [/\ (x \in `[0, 1]) & @split_domain_aux T f g x = f x] + \/ + [/\ x \in `]1, 2], x \in ~` `[0, 1] & @split_domain_aux T f g x = (g \o affine 1 (-1)) x]. +Proof. +move=> x01; rewrite /split_domain_aux /= /patch /=. +case: ifP => xI; [left | right]; split => //; first by rewrite set_itv_set. + rewrite in_itv /=; apply/andP; split; last by move/itvP:x01 => ->. + rewrite real_ltNge // ?num_real //; move/negP: xI; apply: contra_notT. + by rewrite negbK -set_itv_set in_itv /= => xh; rewrite xh (itvP x01). +by apply /mem_set => /=; rewrite set_itv_set xI. +Qed. + +Lemma split_domain_aux_fun {T} B (f g : R -> T) : + set_fun `[0,1] B f -> set_fun `[0,1] B g -> + set_fun `[0,2] B (split_domain_aux f g). +Proof. +move=> funF funG x /(@split_domain_auxP T f g) [][]. + by move=> xI ->; first exact: funF. +move=> ? ? ->; apply: funG; rewrite /= set_itv_set affine_pitv_ccE // ?subr0 . +by rewrite opprK add0r divrr ?unitfE // -set_itv_set divr1; apply: subset_itv_oc_cc. +Qed. + +HB.instance Definition _ {T} (B : set T) {f g : {fun `[0,1] >-> B}} := + IsFun.Build _ _ _ _ (split_domain_aux f g) (split_domain_aux_fun funS funS). + +Lemma split_cts1 {T} (f g : R -> T) : {within `[0,1], continuous f} -> + {within `[0,1], continuous (split_domain_aux f g)}. +Proof. +move=> ctsF; apply: (@subspace_eq_continuous _ _ _ f) => //. +by move=> q ?; rewrite /split_domain_aux patchT. +Qed. + +Lemma split_cts2 {T} (f g : R -> T) : (g 0 = f 1) -> + {within `[0,1], continuous g} -> + {within `[1,2], continuous (split_domain_aux f g)}. +Proof. +move=> fg_midpoint ctsg; rewrite /split_domain_aux within_continuousE. +apply: (@subspace_eq_continuous _ _ _ (g \o (@affine_fun R (PosNum ltr01) (-1) 1 2))). + move=> q /set_mem /=; case : (eqVneq q 1). + move=> -> _; rewrite /patch -set_itv_set bound_itvE ler01 /affine. + by rewrite mulr1 subrr fg_midpoint. + move=> qn1 q12; rewrite patchC //; apply/mem_set; rewrite /= in_itv /=. + apply/negP/nandP; right; rewrite le_eqVlt negb_or qn1 real_ltNge ?num_real //. + by move/itvP: q12 ->. +move=> z; apply (@continuous_comp (subspace_topologicalType `[1,2]) + (subspace_topologicalType `[0,1]) T); last exact: ctsg. +apply: subspaceT_continuous; last apply: continuous_fun. +move=> x /(affine_fun_pitv (PosNum ltr01) (-1)); rewrite /= ?mul1r subrr. +by rewrite (_ : 2-1 = 1) // -addrA subrr addr0. +Qed. + +Lemma split_domain_aux_cts {T} (f g : R -> T) : (g 0 = f 1) -> + {within `[0,1], continuous f} -> + {within `[0,1], continuous g} -> + {within `[0,2], continuous (split_domain_aux f g)}. +Proof. +move=> fg_midpoint ctsf ctsg. +have : (`[0,1]%classic `|` `[1,2]%classic = `[(0:R),2]%classic). + rewrite ?set_itvcc eqEsubset; (split => r /=; first case) => /andP [lb ub]. + - by apply/andP; split => //; apply: (ge_trans _ ub) => /=; rewrite ler_paddr. + - by apply/andP; split => //; apply: (ge_trans lb) => /=. + - case/orP: (@real_leVge R r (1) (num_real _) (num_real _)) => rh. + by left; apply/andP; split. + by right; apply/andP; split. +move=> <-; apply: withinU_continuous; (try exact: interval_closed). + exact: split_cts1. +exact: split_cts2. +Qed. + +Lemma split_domain_mono (f g : R -> R): + f 1 <= g 0 -> + {in `[0,1] &, {mono f : x y / x <= y}} -> + {in `[0,1] &, {mono g : x y / x <= y}} -> + {in `[0,2] &, {mono (split_domain_aux f g) : x y / x <= y}}. +Proof. +move=> f1g0 monof monog x y. +have fltg : forall p q, p \in `[0,1] -> q \in `]1,2] -> f p < g (affine 1 (-1) q). + move=> p q pI qI; apply: (@le_lt_trans _ _ (f 1)). + by rewrite monof // ?bound_itvE // (itvP pI). + apply: (@le_lt_trans _ _ (g 0)) => //. + rewrite (leW_mono_in (monog)) ?bound_itvE // ?in_itv /= /affine mul1r. + by rewrite ltr_subr_addr add0r (itvP qI). + by rewrite ?ler_subr_addr ?add0r ?ler_subl_addr ?(itvP qI). +move=> /(split_domain_auxP f g) [][] xI => [|?] ->; +move=> /(split_domain_auxP f g) [][] yI => [|?] ->. +- rewrite monof // ?affine_pmono //. +- have xley : x < y by apply (@le_lt_trans _ _ (1)); rewrite ?(itvP xI) ?(itvP yI). + by rewrite (ltW (fltg _ _ xI yI )) // (ltW xley). +- have xley : y < x by apply (@le_lt_trans _ _ (1)); rewrite ?(itvP xI) ?(itvP yI). + rewrite [x <= y]real_leNgt ?num_real // xley /=. + rewrite real_leNgt ?num_real //; apply: negbF. + rewrite fltg // (ltW xley). +- rewrite monog ?set_itv_set ?affine_pitv_ccE // ?opprK ?add0r ?divr1. + + rewrite real_mono // ?num_real // => p q. + by rewrite (leW_mono (affine_pmono _ _)). + + by rewrite -set_itv_set; apply: subset_itv_oc_cc. + + by rewrite -set_itv_set; apply: subset_itv_oc_cc. +Qed. + +Definition split_domain {T} (f g: R -> T) := split_domain_aux f g \o affine 2 0. + +End SplitDomain. + +Section Parametrizations. +Context {R : realType}. + +Lemma parametrize_monotone (f : {inj_parametrization R}) : + {in `[0,1] &, {mono f : x y / x <= y}}. +Proof. +apply: itv_continuous_inj_le. +- exists 0; exists 1; rewrite ?bound_itvE ?parametrize_init. + by rewrite ?parametrize_final; split. +- apply: continuous_fun. +- by move: (@inj _ _ _ f); rewrite mem_setE. +Qed. + +Section Identity. +HB.instance Definition _ := @IsParametrization.Build _ (@idfun R) erefl erefl. +Definition id_parametrization := [inj_parametrization of (@idfun R)]. +End Identity. + +Section Composition. +Variables (f g : {parametrization R}). +Let h := (f \o g) : R -> R. +HB.instance Definition _ := Fun.on h. +HB.instance Definition _ := JustContinuous.on h. + +Local Lemma h_init : h 0 = 0. +Proof. by rewrite /h /= ?parametrize_init. Qed. + +Local Lemma h_final : h 1 = 1. +Proof. by rewrite /h /= ?parametrize_final. Qed. + +HB.instance Definition _ := @IsParametrization.Build _ _ h_init h_final. + +Definition comp_parametrization := [parametrization of h]. + +End Composition. + +Section InjComposition. +Variables (f g : {inj_parametrization R}). +Let h := (f \o g) : R -> R. +HB.instance Definition _ := SplitInjFun.on h. +HB.instance Definition _ := Parametrization.on h. + +Definition comp_inj_parametrization := [inj_parametrization of h]. +End InjComposition. + +Section Inverses. +Local Open Scope fun_scope. +Variables (f : {inj_parametrization R}). + +Let g := (f^-1) : R -> R. + +Local Lemma g_continuous :IsContinuous _ _ `[0,1]%classic g. +Proof. +split; rewrite -(@parametrize_init _ f) -(@parametrize_final _ f). +apply: segment_can_le_continuous => //; first exact: continuous_fun. +by move=> ? ?; exact/funK/mem_set. +Qed. + +HB.instance Definition _ := g_continuous. + +Local Lemma g_init : g 0 = 0. +Proof. +rewrite -[x in g x](@parametrize_init _ f) [g (f _)]funK //. +by rewrite mem_setE /= bound_itvE. +Qed. + +Local Lemma g_final : g 1 = 1. +Proof. +rewrite -[x in g x](@parametrize_final _ f) [g (f _)]funK //. +by rewrite mem_setE /= bound_itvE. +Qed. + +Local Lemma g_cancel : {in `[0,1]%classic, cancel g f}. +Proof. +rewrite mem_setE /= -(@parametrize_init _ f) -(@parametrize_final _ f). +apply: segment_continuous_le_can_sym => //; first exact: continuous_fun. +by move=> ? ?; apply/funK/mem_set. +Qed. + +Local Lemma g_fun : set_fun `[0,1]%classic `[0,1]%classic g. +Proof. +have gle : {in `[0,1] &, {mono g : x y / x <= y}}. + apply: itv_continuous_inj_le. + - by exists 0; exists 1; rewrite ?bound_itvE ?g_init ?g_final; split. + - apply: continuous_fun. + - by apply: can_in_inj => p q; exact/g_cancel/mem_set. +move=> z; rewrite /= ?in_itv /= => /[dup] ? /andP [] ? ?. +by rewrite -g_init -g_final; apply/andP; split; rewrite gle // ?bound_itvE. +Qed. + +HB.instance Definition _ := Can.Build _ _ _ g g_cancel. +HB.instance Definition _ := IsFun.Build _ _ _ _ _ g_fun. + +HB.instance Definition _ := @IsParametrization.Build _ _ g_init g_final. + +Definition inv_parametrization := [inj_parametrization of g]. + +Lemma inv_parametrization_can_r : {in `[0,1], cancel f inv_parametrization}. +Proof. +move=> z zI /=; rewrite (@segment_continuous_can_sym _ 0 1) //. +- exact: continuous_fun. +- move=> w wI; move: (@funK _ _ _ inv_parametrization w). + by rewrite mem_setE invV => /(_ wI). +- by rewrite g_init g_final /minr /maxr ltr01. +Qed. + +Lemma inv_parametrization_can_l: {in `[0,1], cancel inv_parametrization f}. +Proof. by move=> z zI; apply: funK; rewrite mem_setE. Qed. + +End Inverses. + +Definition rev_param (x : R) : R := `1- x. + +Local Lemma rev_param_funS : set_fun `[0,1]%classic `[0,1]%classic rev_param. +Proof. +rewrite ?set_itvcc => x /= /andP [] xnng xle1; apply/andP. +split; [exact: onem_ge0| exact: onem_le1]. +Qed. + +HB.instance Definition _ := IsFun.Build R R _ _ _ rev_param_funS. + +Local Lemma rev_param_continuous : {within `[0,1], continuous rev_param}. +Proof. +move=> z; apply: continuous_subspaceT. +move=> ?; apply: (@continuousD R R R ); first exact: cvg_cst. +exact: opp_continuous. +Qed. + +HB.instance Definition _ := IsContinuous.Build _ _ _ _ rev_param_continuous. + +Lemma rev_param_cancel (A : set R) : {in A, cancel rev_param rev_param}. +Proof. by move=> x _; rewrite /rev_param onemK. Qed. + +Lemma split_inj_rev_param : SplitInjFun _ `[0,1] `[0,1] rev_param. +Proof. +have [f /=] := funPsplitinj (@rev_param_cancel `[0,1]%classic). +rewrite (_ : rev_param = homotopy_rev_param__canonical__functions_Fun) //. +move=> ->; case: f => ?; apply. +Qed. + +HB.instance Definition _ := split_inj_rev_param. + +Section Reversal. +Variables (f : {parametrization R}). + +Let g := rev_param \o f \o rev_param. +HB.instance Definition _ := JustContinuous.on g. +HB.instance Definition _ := Fun.on g. + +Local Lemma rev_rev_init : g 0 = 0. +Proof. by rewrite /g /= /rev_param /= onem0 parametrize_final onem1. Qed. + +Local Lemma rev_rev_final : g 1 = 1. +Proof. by rewrite /g /= /rev_param /= onem1 parametrize_init onem0. Qed. + +HB.instance Definition _ := @IsParametrization.Build + _ _ rev_rev_init rev_rev_final. + +Definition double_reverse := [parametrization of g]. + +End Reversal. + +Lemma ler12 : (1:R) <= 2. +Proof. by rewrite (_ : 1 = ((1%:R : R))) // (@ler_nat R). Qed. + +Lemma ltr12 : (1:R) < 2. +Proof. by rewrite (_ : 1 = ((1%:R : R))) // (@ltr_nat R). Qed. + +#[local] Hint Resolve ler12 : core. +#[local] Hint Resolve ltr12 : core. + +Section InjReversal. +Variables (f : {inj_parametrization R}). +HB.instance Definition _ := Parametrization.on (double_reverse f). +HB.instance Definition _ := SplitInjFun.on (double_reverse f). + +Definition double_reverse_inj := [inj_parametrization of (double_reverse f)]. + +End InjReversal. + +Section SplitParametrization. +Context (f g: {inj_parametrization R}). +Let hpos : (0:R) < 1/2. Proof. by []. Qed. +Let pos2 : (0:R) < 2. Proof. by []. Qed. +Let shift1 := [continuous of affine_fun (PosNum hpos) 0 0 1 \o f]. +Let shift2 := [continuous of affine_fun (PosNum hpos) (1/2) 0 1 \o g]. + +Lemma split_parametrize_fun : set_fun `[0,1] `[0,1] (split_domain shift1 shift2). +Proof. +rewrite /split_domain => x /[dup] x01 /(affine_fun_pitv (PosNum pos2) 0) /=. +rewrite mulr0 ?addr0 mulr1 => /(@split_domain_aux_fun R R `[0,1] _ _); apply. + move=> y /(@funS _ _ _ _ shift1) /=; move: (affine _ _ _). + rewrite mulr0 addr0; apply: subitvPr; rewrite /Order.le /= ?mulr1 addr0. + by rewrite ler_pdivr_mulr // mul1r. +move=> y /(@funS _ _ _ _ shift2) /=; move: (affine _ _ _). +by rewrite mulr1 -splitr; apply: subitvPl; rewrite /Order.le /= ?mulr0 add0r. +Qed. + +HB.instance Definition _ := @IsFun.Build _ _ _ _ _ split_parametrize_fun. + +Lemma split_parametrize_cts : {within `[0,1], continuous (split_domain shift1 shift2)}. +Proof. +move=> x. +apply: (@continuous_comp (subspace_topologicalType _) (subspace_topologicalType `[0,2]) _). + apply: subspaceT_continuous; last exact: continuous_fun. + by move=> q /(affine_fun_pitv (PosNum pos2) 0); rewrite /= mulr0 ?addr0 mulr1. +apply: split_domain_aux_cts; last exact: continuous_fun; first last. + exact: continuous_fun. +by rewrite /= /affine parametrize_init parametrize_final mulr0 add0r addr0 mulr1. +Qed. + +HB.instance Definition _ := @IsContinuous.Build _ _ _ _ split_parametrize_cts. + +Local Lemma split_parametrize_init : split_domain shift1 shift2 0 = 0. +Proof. +rewrite /split_domain /= /affine ?addr0. +by rewrite patchT mulr0 /= -?set_itv_set ?bound_itvE // addr0 parametrize_init mulr0. +Qed. + +Local Lemma split_parametrize_final : split_domain shift1 shift2 1 = 1. +Proof. +rewrite /split_domain /= /affine mulr1 addr0 ?mul1r patchC. + rewrite /= mul1r (_ : 2-1 = 1); last by apply/eqP; rewrite subr_eq. + by rewrite parametrize_final mulr1 -div1r -splitr. +rewrite in_setC; apply/negP; rewrite -set_itv_set inE=> /andP. +rewrite /Order.le /=; apply/not_andP; right; apply/negP; rewrite -real_ltNge //. +Qed. + +HB.instance Definition _ := @IsParametrization.Build _ _ + split_parametrize_init split_parametrize_final. + +Local Lemma split_parametrize_inj : + @SplitInj R R `[0,1] (split_domain shift1 shift2). +Proof. +have [] := @pPinj_ R R idfun `[0,1] (split_domain shift1 shift2); first last. + by move=> x ->; case: x. +apply: (mono_inj_in lexx le_anti) => x y /= /set_mem /= xI /set_mem /= yI. +rewrite split_domain_mono //; first by rewrite affine_pmono. +- by rewrite /= parametrize_init parametrize_final /affine mulr0 addr0 add0r mulr1. +- move=> p q pI qI; rewrite /= affine_pmono //. + rewrite (@segment_continuous_inj_le _ _ 0 1) // ?parametrize_init ?parametrize_final //. + exact: continuous_fun. + move=> m n; rewrite ?set_itv_set; move: m n; exact: inj. +- move=> p q pI qI; rewrite /= affine_pmono //. + rewrite (@segment_continuous_inj_le _ _ 0 1) // ?parametrize_init ?parametrize_final //. + exact: continuous_fun. + move=> m n; rewrite ?set_itv_set; move: m n; exact: inj. +- rewrite set_itv_set affine_pitv_ccE // ?subr0 ?mul0r divrr ?unitfE //. + by rewrite -set_itv_set. +- rewrite set_itv_set affine_pitv_ccE // ?subr0 ?mul0r divrr ?unitfE //. + by rewrite -set_itv_set. +Qed. + +HB.instance Definition _ := split_parametrize_inj. + +Definition split_parametrize := [inj_parametrization of (split_domain shift1 shift2)]. + +End SplitParametrization. + +End Parametrizations. + +Section Reparametrization. + +Context {R : realType} {T : topologicalType} (B : set T). + +Definition reparametrize (f g : R -> T) : bool := + `[]. + +Lemma reflexive_reparametrize : reflexive reparametrize. +Proof. by move=> f; apply/asboolP; exists id_parametrization. Qed. + +Lemma symmetric_reparametrize : symmetric reparametrize. +Proof. +by move=> f g; apply/asbool_equiv_eq; split=> [][] gamma fgamg; + exists (inv_parametrization gamma) => z zI; + rewrite /comp -fgamg /comp ?inv_parametrization_can_l //; + apply: (@funS _ _ _ _ (inv_parametrization gamma)). +Qed. + +Lemma transitive_reparametrize : transitive reparametrize. +Proof. +move=> f g h /asboolP [p pfg] /asboolP [q qgh]; apply/asboolP. +exists (comp_parametrization p q) => z zI /=. +by rewrite -qgh //= -pfg //; exact: (@funS _ _ _ _ q). +Qed. + +Definition equiv_rel_reparametrize := EquivRel reparametrize + reflexive_reparametrize symmetric_reparametrize transitive_reparametrize. + +Definition RPath := {eq_quot equiv_rel_reparametrize}. + +Definition path_init := lift_fun1 RPath (fun f => f 0). + +Lemma path_init_mono : {mono \pi_RPath : f / f 0 >-> path_init f}. +Proof. +move=> f; unlock path_init. +have : ((repr (\pi_(RPath) f)) = f %[mod RPath]) by rewrite reprK. +move=> /eqquotP /asboolP [] gamma /(_ 0). +by rewrite bound_itvE /= parametrize_init; exact. +Qed. + +Canonical pi_path_init_mono := PiMono1 path_init_mono. + +Definition path_final := lift_fun1 RPath (fun f => f 1). + +Lemma path_final_mono : {mono \pi_RPath : f / f 1 >-> path_final f}. +Proof. +move=> f; unlock path_final. +have : ((repr (\pi_(RPath) f)) = f %[mod RPath]) by rewrite reprK. +move=> /eqquotP /asboolP [] gamma /(_ 1). +by rewrite bound_itvE /= parametrize_final; exact. +Qed. + +Canonical pi_path_final_mono := PiMono1 path_final_mono. + +Definition path_image := lift_fun1 RPath (fun f => f @` `[0,1] ). + +Lemma path_image_mono : {mono \pi_RPath : f / f @` `[0,1] >-> path_image f}. +Proof. +move=> f; unlock path_image; rewrite eqEsubset; split => z /= [w wI] <-. + have /eqquotP/asboolP [gamma fg]: f = repr (\pi_(RPath) f) %[mod RPath]. + by rewrite reprK. + by (exists (gamma w); last exact: fg); exact: (@funS _ _ _ _ gamma). +have /eqquotP/asboolP [gamma fg]: repr (\pi_(RPath) f) = f %[mod RPath]. + by rewrite reprK. +(exists (gamma w); last exact: fg); exact: (@funS _ _ _ _ gamma). +Qed. + +Canonical pi_path_image_mono := PiMono1 path_image_mono. + +Let cts_fun_rev (f : R -> T) := f \o rev_param. + +Definition path_reverse := lift_op1 RPath cts_fun_rev. + +Lemma path_reverse_morph : {morph \pi : f / cts_fun_rev f >-> path_reverse f}. +Proof. +move=> f /=; unlock path_reverse; apply/eqquotP/asboolP. +have /eqquotP/asboolP [gamma fg]: repr (\pi_(RPath) f) = f %[mod RPath]. + by rewrite reprK. +exists (double_reverse_inj (inv_parametrization gamma)) => x x01 /=. +have gx01 : (gamma^-1)%function (rev_param x) \in `[0, 1]. + apply: (@funS _ _ _ _ [fun of inv_parametrization gamma]). + exact: funS. +rewrite /cts_fun_rev /= (@rev_param_cancel _ `[0,1]%classic) -?fg ?inE // /RPath. + have /= := (@funK _ _ _ (inv_parametrization gamma) (rev_param x)). +by rewrite invV => -> //=; apply/mem_set; exact: funS. +Qed. + +Canonical pi_path_reverse_morph := PiMorph1 path_reverse_morph. + +Lemma path_reverse_final_initE (f : RPath) : + path_final (path_reverse f) = path_init f. +Proof. +have := path_init_mono (repr f); rewrite reprK => ->. +have := path_reverse_morph (repr f); rewrite reprK /= => <-. +rewrite (path_final_mono (cts_fun_rev (repr f))). +by rewrite /cts_fun_rev /= /rev_param onem1. +Qed. + +Lemma path_reverse_init_finalE (f : RPath) : + path_init (path_reverse f) = path_final f. +Proof. +have := path_final_mono (repr f); rewrite reprK => ->. +have := path_reverse_morph (repr f); rewrite reprK /= => <-. +rewrite (path_init_mono (cts_fun_rev (repr f))). +by rewrite /cts_fun_rev /= /rev_param onem0. +Qed. + +Lemma path_cts : {mono \pi_RPath : f / {within `[0,1], continuous f} + >-> {within `[0,1], continuous (repr f)}}. +Proof. +move=> f; rewrite propeqE; split => ctsF. + have /eqquotP/asboolP [gamma fpp]: repr (\pi_RPath f) = f %[mod RPath]. + by rewrite reprK. + apply: subspace_eq_continuous. + move=> x /set_mem /=; move: x; exact: fpp. + move=> x; apply: (@continuous_comp (subspace_topologicalType _) (subspace_topologicalType `[0,1]) _). + by apply: subspaceT_continuous; [exact: funS | exact: continuous_fun]. + exact: ctsF. +have /eqquotP/asboolP [gamma fpp]: f = repr (\pi_RPath f) %[mod RPath]. + by rewrite reprK. +apply: subspace_eq_continuous. + move=> x /set_mem /=; move: x; exact: fpp. +move=> x; apply: (@continuous_comp (subspace_topologicalType _) (subspace_topologicalType _) _). + by apply: subspaceT_continuous; [exact: funS | exact: continuous_fun]. +exact: ctsF. +Qed. + +Canonical pi_path_cts_mono := PiMono1 path_cts. + +Definition path_link := lift_op2 RPath split_domain. + +Lemma path_link_morph : {morph \pi : f g / split_domain f g >-> path_link f g}. +Proof. +move=> f g /=; unlock path_link; apply/eqquotP/asboolP. +have /eqquotP/asboolP [r1 fpp]: (f = (repr (\pi_(RPath) f)) %[mod RPath]). + by rewrite reprK. +have /eqquotP/asboolP [r2 gpp]: (g = (repr (\pi_(RPath) g)) %[mod RPath]). + by rewrite reprK. +exists (split_parametrize r1 r2) => x x01. +have : affine 2 0 x \in `[0,2]. + by rewrite set_itv_set affine_pitv_ccE // ?subr0 mul0r divrr ?unitfE // -set_itv_set. +rewrite /split_parametrize /= /split_domain /=. +move: {x01 x} (affine 2 0 x) => x /(split_domain_auxP + (affine (1/2) 0 \o r1) (affine (1/2) (1/2) \o r2)) []. + case => x01 -> /=; rewrite -/((_ 2 0 \o _ (1/2) 0) _) affine_id //. + by rewrite ?patchT -?set_itv_set -?fpp //; last exact: (@funS _ _ _ _ r1). +case=> x12 xn01 -> /=. +rewrite -/((affine 2 0 \o affine (1/2) (1/2)) (r2 _)) affine_comp div1r divrr ?unitfE //. +rewrite addr0 {2}/affine mul1r ?patchC //=. + rewrite /affine ?mul1r -?addrA ?subrr ?addr0 -?gpp //= in_itv /=. + by rewrite ler_subr_addr add0r ler_subl_addr ?(itvP x12). +have afx : affine 1 (-1) x \in `]0,1]. + by rewrite in_itv /affine /= mul1r ltr_subr_addr add0r ler_subl_addr. +have r2I : r2 (affine 1 (-1) x) \in `]0,1]. + rewrite in_itv /= lt0r /= -andbA; apply/andP; split; first last. + by move/subset_itv_oc_cc/(@funS _ _ _ _ r2): afx; rewrite /= in_itv. + apply /eqP => M; suff E : x = 1. + by move/set_mem: xn01 => /=; rewrite E bound_itvE. + apply: subr0_eq; apply: (@inj _ _ _ r2) => //. + - rewrite -set_itv_set in_itv /=. + by rewrite ler_subr_addr add0r ler_subl_addr ?(itvP x12). + - by rewrite -set_itv_set bound_itvE. + - rewrite parametrize_init (_ : x - 1 = affine 1 (-1) x) //. + by rewrite /affine mul1r. +apply/mem_set; rewrite /= in_itv /=; apply/negP/nandP; right. +by rewrite -real_ltNge ?num_real // -ltr_subl_addr subrr (itvP r2I). +Qed. + +Canonical pi_path_chain_morph := PiMorph2 path_link_morph. + +End Reparametrization. + +HB.mixin Record IsRPathFrom {R} {T : topologicalType} + (x : T) (f : @RPath R T) := + { from_point : path_init f = x }. + +HB.structure Definition RPathFrom {R} {T : topologicalType} + (x : T) := {f of @IsRPathFrom R T x f}. + +HB.mixin Record IsRPathTo {R} {T : topologicalType} + (x : T) (f : @RPath R T) := + { to_point : path_final f = x }. + +HB.structure Definition RPathTo {R} {T : topologicalType} + (x : T) := {f of @IsRPathTo R T x f}. + +HB.structure Definition RPathBetween {R} {T : topologicalType} + (x y : T) := {f of (@RPathFrom R T x f) & (@RPathTo R T y f)}. + +HB.mixin Record IsPath {R} {T : topologicalType} (B : set T) (f : @RPath R T) := + { + continuous_path : {within `[0,1], continuous (repr f)}; + path_fun : set_fun `[0,1]%classic B (repr f); + }. + +HB.structure Definition Path {R} {T : topologicalType} (B : set T) := + { f of IsPath R T B f}. + +HB.structure Definition PathFrom {R} {T : topologicalType} (B : set T) (x : T) := + { f of IsPath R T B f & IsRPathFrom R T x f}. + +HB.structure Definition PathTo {R} {T : topologicalType} (B : set T) (y : T) := + { f of IsPath R T B f & IsRPathTo R T y f}. + +HB.structure Definition PathBetween {R} {T : topologicalType} (B : set T) (x y : T) := + { f of IsPath R T B f & IsRPathFrom R T x f & IsRPathTo R T y f}. + +Notation "{ 'path' R 'from' x 'to' y 'in` B }" := + (@PathBetween.type R _ B x y) : form_scope. + +Notation "{ 'Loop' R 'at' x 'in' B }" := + (@PathBetween.type R _ B x x) : form_scope. + +Notation "[ 'loop' of' f ]" := + ([the (@PathBetween.type _ _ _ _ _) of (f: @Path _ _ _)]) : form_scope. diff --git a/theories/mathcomp_extra.v b/theories/mathcomp_extra.v new file mode 100644 index 000000000..4d0611659 --- /dev/null +++ b/theories/mathcomp_extra.v @@ -0,0 +1,604 @@ +(* mathcomp analysis (c) 2022 Inria and AIST. License: CeCILL-C. *) +From mathcomp Require choice. +(* Missing coercion (done before Import to avoid redeclaration error, + thanks to KS for the trick) *) +(* MathComp 1.15 addition *) +Coercion choice.Choice.mixin : choice.Choice.class_of >-> choice.Choice.mixin_of. +From mathcomp Require Import all_ssreflect finmap ssralg ssrnum ssrint rat. +From mathcomp Require Import finset interval. +From mathcomp.classical Require Import boolp classical_sets. +From mathcomp.classical Require Export mathcomp_extra. + +(***************************) +(* MathComp 1.15 additions *) +(***************************) + +(******************************************************************************) +(* This files contains lemmas and definitions missing from MathComp. *) +(* *) +(* f \max g := fun x => Num.max (f x) (g x) *) +(* lteBSide, bnd_simp == multirule to simplify inequalities between *) +(* interval bounds *) +(* miditv i == middle point of interval i *) +(* *) +(******************************************************************************) + +Set Implicit Arguments. +Unset Strict Implicit. +Unset Printing Implicit Defensive. + +Reserved Notation "f \max g" (at level 50, left associativity). + +Lemma enum_ord0 : enum 'I_0 = [::]. +Proof. by apply/eqP; rewrite -size_eq0 size_enum_ord. Qed. + +Lemma enum_ordSr n : enum 'I_n.+1 = + rcons (map (widen_ord (leqnSn _)) (enum 'I_n)) ord_max. +Proof. +apply: (inj_map val_inj); rewrite val_enum_ord. +rewrite -[in iota _ _]addn1 iotaD/= cats1 map_rcons; congr (rcons _ _). +by rewrite -map_comp/= (@eq_map _ _ _ val) ?val_enum_ord. +Qed. + +Lemma obindEapp {aT rT} (f : aT -> option rT) : obind f = oapp f None. +Proof. by []. Qed. + +Lemma omapEbind {aT rT} (f : aT -> rT) : omap f = obind (olift f). +Proof. by []. Qed. + +Lemma omapEapp {aT rT} (f : aT -> rT) : omap f = oapp (olift f) None. +Proof. by []. Qed. + +Lemma oappEmap {aT rT} (f : aT -> rT) (y0 : rT) x : + oapp f y0 x = odflt y0 (omap f x). +Proof. by case: x. Qed. + +Lemma omap_comp aT rT sT (f : aT -> rT) (g : rT -> sT) : + omap (g \o f) =1 omap g \o omap f. +Proof. by case. Qed. + +Lemma oapp_comp_f {aT rT sT} (f : aT -> rT) (g : rT -> sT) (x : rT) : + oapp (g \o f) (g x) =1 g \o oapp f x. +Proof. by case. Qed. + +Lemma can_in_comp [A B C : Type] (D : {pred B}) (D' : {pred C}) + [f : B -> A] [h : C -> B] + [f' : A -> B] [h' : B -> C] : + {homo h : x / x \in D' >-> x \in D} -> + {in D, cancel f f'} -> {in D', cancel h h'} -> + {in D', cancel (f \o h) (h' \o f')}. +Proof. by move=> hD fK hK c cD /=; rewrite fK ?hK ?hD. Qed. + +Lemma in_inj_comp A B C (f : B -> A) (h : C -> B) (P : pred B) (Q : pred C) : + {in P &, injective f} -> {in Q &, injective h} -> {homo h : x / Q x >-> P x} -> + {in Q &, injective (f \o h)}. +Proof. +by move=> Pf Qh QP x y xQ yQ xy; apply Qh => //; apply Pf => //; apply QP. +Qed. + +Lemma pcan_in_comp [A B C : Type] (D : {pred B}) (D' : {pred C}) + [f : B -> A] [h : C -> B] + [f' : A -> option B] [h' : B -> option C] : + {homo h : x / x \in D' >-> x \in D} -> + {in D, pcancel f f'} -> {in D', pcancel h h'} -> + {in D', pcancel (f \o h) (obind h' \o f')}. +Proof. by move=> hD fK hK c cD /=; rewrite fK/= ?hK ?hD. Qed. + +Lemma ocan_comp [A B C : Type] [f : B -> option A] [h : C -> option B] + [f' : A -> B] [h' : B -> C] : + ocancel f f' -> ocancel h h' -> ocancel (obind f \o h) (h' \o f'). +Proof. +move=> fK hK c /=; rewrite -[RHS]hK/=; case hcE : (h c) => [b|]//=. +by rewrite -[b in RHS]fK; case: (f b) => //=; have := hK c; rewrite hcE. +Qed. + +Lemma eqbLR (b1 b2 : bool) : b1 = b2 -> b1 -> b2. +Proof. by move->. Qed. + +Import Order.TTheory GRing.Theory Num.Theory. + +Definition max_fun T (R : numDomainType) (f g : T -> R) x := Num.max (f x) (g x). +Notation "f \max g" := (max_fun f g) : ring_scope. +Arguments max_fun {T R} _ _ _ /. + +Lemma gtr_opp (R : numDomainType) (r : R) : (0 < r)%R -> (- r < r)%R. +Proof. by move=> n0; rewrite -subr_lt0 -opprD oppr_lt0 addr_gt0. Qed. + +Lemma le_le_trans {disp : unit} {T : porderType disp} (x y z t : T) : + (z <= x)%O -> (y <= t)%O -> (x <= y)%O -> (z <= t)%O. +Proof. by move=> + /(le_trans _)/[apply]; apply: le_trans. Qed. + +Notation eqLHS := (X in (X == _))%pattern. +Notation eqRHS := (X in (_ == X))%pattern. +Notation leLHS := (X in (X <= _)%O)%pattern. +Notation leRHS := (X in (_ <= X)%O)%pattern. +Notation ltLHS := (X in (X < _)%O)%pattern. +Notation ltRHS := (X in (_ < X)%O)%pattern. +Inductive boxed T := Box of T. + +Lemma eq_bigl_supp [R : eqType] [idx : R] [op : Monoid.law idx] [I : Type] + [r : seq I] [P1 : pred I] (P2 : pred I) (F : I -> R) : + {in [pred x | F x != idx], P1 =1 P2} -> + \big[op/idx]_(i <- r | P1 i) F i = \big[op/idx]_(i <- r | P2 i) F i. +Proof. +move=> P12; rewrite big_mkcond [RHS]big_mkcond; apply: eq_bigr => i _. +by case: (eqVneq (F i) idx) => [->|/P12->]; rewrite ?if_same. +Qed. + +Lemma perm_big_supp_cond [R : eqType] [idx : R] [op : Monoid.com_law idx] [I : eqType] + [r s : seq I] [P : pred I] (F : I -> R) : + perm_eq [seq i <- r | P i && (F i != idx)] [seq i <- s | P i && (F i != idx)] -> + \big[op/idx]_(i <- r | P i) F i = \big[op/idx]_(i <- s| P i) F i. +Proof. +move=> prs; rewrite !(bigID [pred i | F i == idx] P F)/=. +rewrite big1 ?Monoid.mul1m; last by move=> i /andP[_ /eqP->]. +rewrite [in RHS]big1 ?Monoid.mul1m; last by move=> i /andP[_ /eqP->]. +by rewrite -[in LHS]big_filter -[in RHS]big_filter; apply perm_big. +Qed. + +Lemma perm_big_supp [R : eqType] [idx : R] [op : Monoid.com_law idx] [I : eqType] + [r s : seq I] [P : pred I] (F : I -> R) : + perm_eq [seq i <- r | (F i != idx)] [seq i <- s | (F i != idx)] -> + \big[op/idx]_(i <- r | P i) F i = \big[op/idx]_(i <- s| P i) F i. +Proof. +by move=> ?; apply: perm_big_supp_cond; rewrite !filter_predI perm_filter. +Qed. + +Local Open Scope order_scope. +Local Open Scope ring_scope. +Import GRing.Theory Order.TTheory. + +Lemma mulr_ge0_gt0 (R : numDomainType) (x y : R) : 0 <= x -> 0 <= y -> + (0 < x * y) = (0 < x) && (0 < y). +Proof. +rewrite le_eqVlt => /predU1P[<-|x0]; first by rewrite mul0r ltxx. +rewrite le_eqVlt => /predU1P[<-|y0]; first by rewrite mulr0 ltxx andbC. +by apply/idP/andP=> [|_]; rewrite pmulr_rgt0. +Qed. + +Section lt_le_gt_ge. +Variable (R : numFieldType). +Implicit Types x y z a b : R. + +Lemma splitr x : x = x / 2%:R + x / 2%:R. +Proof. by rewrite -mulr2n -mulr_natr mulfVK //= pnatr_eq0. Qed. + +Lemma ler_addgt0Pr x y : reflect (forall e, e > 0 -> x <= y + e) (x <= y). +Proof. +apply/(iffP idP)=> [lexy e e_gt0 | lexye]; first by rewrite ler_paddr// ltW. +have [||ltyx]// := comparable_leP. + rewrite (@comparabler_trans _ (y + 1))// /Order.comparable ?lexye ?ltr01//. + by rewrite ler_addl ler01 orbT. +have /midf_lt [_] := ltyx; rewrite le_gtF//. +rewrite -(@addrK _ y y) addrAC -addrA 2!mulrDl -splitr lexye//. +by rewrite divr_gt0// ?ltr0n// subr_gt0. +Qed. + +Lemma ler_addgt0Pl x y : reflect (forall e, e > 0 -> x <= e + y) (x <= y). +Proof. +by apply/(equivP (ler_addgt0Pr x y)); split=> lexy e /lexy; rewrite addrC. +Qed. + +Lemma in_segment_addgt0Pr x y z : + reflect (forall e, e > 0 -> y \in `[x - e, z + e]) (y \in `[x, z]). +Proof. +apply/(iffP idP)=> [xyz e /[dup] e_gt0 /ltW e_ge0 | xyz_e]. + by rewrite in_itv /= ler_subl_addr !ler_paddr// (itvP xyz). +by rewrite in_itv /= ; apply/andP; split; apply/ler_addgt0Pr => ? /xyz_e; + rewrite in_itv /= ler_subl_addr => /andP []. +Qed. + +Lemma in_segment_addgt0Pl x y z : + reflect (forall e, e > 0 -> y \in `[(- e + x), (e + z)]) (y \in `[x, z]). +Proof. +apply/(equivP (in_segment_addgt0Pr x y z)). +by split=> zxy e /zxy; rewrite [z + _]addrC [_ + x]addrC. +Qed. + +Lemma lt_le a b : (forall x, x < a -> x < b) -> a <= b. +Proof. +move=> ab; apply/ler_addgt0Pr => e e_gt0; rewrite -ler_subl_addr ltW//. +by rewrite ab // ltr_subl_addr -ltr_subl_addl subrr. +Qed. + +Lemma gt_ge a b : (forall x, b < x -> a < x) -> a <= b. +Proof. +move=> ab; apply/ler_addgt0Pr => e e_gt0. +by rewrite ltW// ab// -ltr_subl_addl subrr. +Qed. + +End lt_le_gt_ge. + +(**********************************) +(* End of MathComp 1.15 additions *) +(**********************************) + +Lemma natr1 (R : ringType) (n : nat) : (n%:R + 1 = n.+1%:R :> R)%R. +Proof. by rewrite GRing.mulrSr. Qed. + +Lemma nat1r (R : ringType) (n : nat) : (1 + n%:R = n.+1%:R :> R)%R. +Proof. by rewrite GRing.mulrS. Qed. + +(* To be backported to finmap *) + +Lemma fset_nat_maximum (X : choiceType) (A : {fset X}) + (f : X -> nat) : A != fset0 -> + (exists i, i \in A /\ forall j, j \in A -> f j <= f i)%nat. +Proof. +move=> /fset0Pn[x Ax]. +have [/= y _ /(_ _ isT) mf] := @arg_maxnP _ [` Ax]%fset xpredT (f \o val) isT. +exists (val y); split; first exact: valP. +by move=> z Az; have := mf [` Az]%fset. +Qed. + +Lemma image_nat_maximum n (f : nat -> nat) : + (exists i, i <= n /\ forall j, j <= n -> f j <= f i)%N. +Proof. +have [i _ /(_ _ isT) mf] := @arg_maxnP _ (@ord0 n) xpredT f isT. +by exists i; split; rewrite ?leq_ord// => j jn; have := mf (@Ordinal n.+1 j jn). +Qed. + +Lemma card_fset_sum1 (T : choiceType) (A : {fset T}) : + #|` A| = (\sum_(i <- A) 1)%N. +Proof. by rewrite big_seq_fsetE/= sum1_card cardfE. Qed. + +Arguments big_rmcond {R idx op I r} P. +Arguments big_rmcond_in {R idx op I r} P. + +(*******************************) +(* MathComp > 1.15.0 additions *) +(*******************************) + +Section bigminr_maxr. +Import Num.Def. + +Lemma bigminr_maxr (R : realDomainType) I r (P : pred I) (F : I -> R) x : + \big[minr/x]_(i <- r | P i) F i = - \big[maxr/- x]_(i <- r | P i) - F i. +Proof. +by elim/big_rec2: _ => [|i y _ _ ->]; rewrite ?oppr_max opprK. +Qed. +End bigminr_maxr. + +Section SemiGroupProperties. +Variables (R : Type) (op : R -> R -> R). +Hypothesis opA : associative op. + +Section Id. +Variable x : R. +Hypothesis opxx : op x x = x. + +Lemma big_const_idem I (r : seq I) P : \big[op/x]_(i <- r | P i) x = x. +Proof. by elim/big_ind : _ => // _ _ -> ->. Qed. + +Lemma big_id_idem I (r : seq I) P F : + op (\big[op/x]_(i <- r | P i) F i) x = \big[op/x]_(i <- r | P i) F i. +Proof. by elim/big_rec : _ => // ? ? ?; rewrite -opA => ->. Qed. + +End Id. + +Section Abelian. +Hypothesis opC : commutative op. + +Let opCA : left_commutative op. Proof. by move=> x *; rewrite !opA (opC x). Qed. + +Variable x : R. + +Lemma big_rem_AC (I : eqType) (r : seq I) z (P : pred I) F : z \in r -> + \big[op/x]_(y <- r | P y) F y = + if P z then op (F z) (\big[op/x]_(y <- rem z r | P y) F y) + else \big[op/x]_(y <- rem z r | P y) F y. +Proof. +elim: r =>// i r ih; rewrite big_cons rem_cons inE =>/predU1P[-> /[!eqxx]//|zr]. +by case: eqP => [-> //|]; rewrite ih// big_cons; case: ifPn; case: ifPn. +Qed. + +Lemma bigD1_AC (I : finType) j (P : pred I) F : P j -> + \big[op/x]_(i | P i) F i = op (F j) (\big[op/x]_(i | P i && (i != j)) F i). +Proof. +rewrite (big_rem_AC _ _ (mem_index_enum j)) => ->. +by rewrite rem_filter ?index_enum_uniq// big_filter_cond big_andbC. +Qed. + +Section Id. +Hypothesis opxx : op x x = x. + +Lemma big_mkcond_idem I r (P : pred I) F : + \big[op/x]_(i <- r | P i) F i = \big[op/x]_(i <- r) (if P i then F i else x). +Proof. +elim: r => [|i r]; rewrite ?(big_nil, big_cons)//. +by case: ifPn => Pi ->//; rewrite -[in LHS]big_id_idem. +Qed. + +Lemma big_split_idem I r (P : pred I) F1 F2 : + \big[op/x]_(i <- r | P i) op (F1 i) (F2 i) = + op (\big[op/x]_(i <- r | P i) F1 i) (\big[op/x]_(i <- r | P i) F2 i). +Proof. by elim/big_rec3 : _ => [//|i ? ? _ _ ->]; rewrite // opCA -!opA opCA. Qed. + +Lemma big_id_idem_AC I (r : seq I) P F : + \big[op/x]_(i <- r | P i) op (F i) x = \big[op/x]_(i <- r | P i) F i. +Proof. by rewrite big_split_idem big_const_idem ?big_id_idem. Qed. + +Lemma bigID_idem I r (a P : pred I) F : + \big[op/x]_(i <- r | P i) F i = + op (\big[op/x]_(i <- r | P i && a i) F i) + (\big[op/x]_(i <- r | P i && ~~ a i) F i). +Proof. +rewrite -big_id_idem_AC big_mkcond_idem !(big_mkcond_idem _ _ F) -big_split_idem. +by apply: eq_bigr => i; case: ifPn => //=; case: ifPn. +Qed. + +End Id. + +End Abelian. + +End SemiGroupProperties. + +Section bigmaxmin. +Local Notation max := Order.max. +Local Notation min := Order.min. +Local Open Scope order_scope. +Variables (d : _) (T : porderType d). +Variables (I : finType) (f : I -> T) (x0 x : T) (P : pred I). + +Lemma bigmax_le : + x0 <= x -> (forall i, P i -> f i <= x) -> \big[max/x0]_(i | P i) f i <= x. +Proof. by move=> ? ?; elim/big_ind: _ => // *; rewrite maxEle; case: ifPn. Qed. + +Lemma bigmax_lt : + x0 < x -> (forall i, P i -> f i < x) -> \big[max/x0]_(i | P i) f i < x. +Proof. by move=> ? ?; elim/big_ind: _ => // *; rewrite maxElt; case: ifPn. Qed. + +Lemma lt_bigmin : + x < x0 -> (forall i, P i -> x < f i) -> x < \big[min/x0]_(i | P i) f i. +Proof. by move=> ? ?; elim/big_ind: _ => // *; rewrite minElt; case: ifPn. Qed. + +Lemma le_bigmin : + x <= x0 -> (forall i, P i -> x <= f i) -> x <= \big[min/x0]_(i | P i) f i. +Proof. by move=> ? ?; elim/big_ind: _ => // *; rewrite minEle; case: ifPn. Qed. + +End bigmaxmin. + +Section bigmax. +Local Notation max := Order.max. +Local Open Scope order_scope. +Variables (d : unit) (T : orderType d). + +Section bigmax_Type. +Variables (I : Type) (r : seq I) (x : T). +Implicit Types (P a : pred I) (F : I -> T). + +Lemma bigmax_mkcond P F : \big[max/x]_(i <- r | P i) F i = + \big[max/x]_(i <- r) (if P i then F i else x). +Proof. by rewrite big_mkcond_idem ?maxxx//; [exact: maxA|exact: maxC]. Qed. + +Lemma bigmax_split P F1 F2 : + \big[max/x]_(i <- r | P i) (max (F1 i) (F2 i)) = + max (\big[max/x]_(i <- r | P i) F1 i) (\big[max/x]_(i <- r | P i) F2 i). +Proof. by rewrite big_split_idem ?maxxx//; [exact: maxA|exact: maxC]. Qed. + +Lemma bigmax_idl P F : + \big[max/x]_(i <- r | P i) F i = max x (\big[max/x]_(i <- r | P i) F i). +Proof. by rewrite maxC big_id_idem ?maxxx//; exact: maxA. Qed. + +Lemma bigmax_idr P F : + \big[max/x]_(i <- r | P i) F i = max (\big[max/x]_(i <- r | P i) F i) x. +Proof. by rewrite [LHS]bigmax_idl maxC. Qed. + +Lemma bigmaxID a P F : \big[max/x]_(i <- r | P i) F i = + max (\big[max/x]_(i <- r | P i && a i) F i) + (\big[max/x]_(i <- r | P i && ~~ a i) F i). +Proof. by rewrite (bigID_idem maxA maxC _ _ a) ?maxxx. Qed. + +End bigmax_Type. + +Section bigmax_finType. +Variables (I : finType) (x : T). +Implicit Types (P : pred I) (F : I -> T). + +Lemma bigmaxD1 j P F : P j -> + \big[max/x]_(i | P i) F i = max (F j) (\big[max/x]_(i | P i && (i != j)) F i). +Proof. by move/(bigD1_AC maxA maxC) ->. Qed. + +Lemma le_bigmax_cond j P F : P j -> F j <= \big[max/x]_(i | P i) F i. +Proof. by move=> Pj; rewrite (bigmaxD1 _ Pj) le_maxr lexx. Qed. + +Lemma le_bigmax F j : F j <= \big[max/x]_i F i. +Proof. exact: le_bigmax_cond. Qed. + +(* NB: as of [2022-08-02], bigop.bigmax_sup already exists for nat *) +Lemma bigmax_sup j P m F : P j -> m <= F j -> m <= \big[max/x]_(i | P i) F i. +Proof. by move=> Pj ?; apply: le_trans (le_bigmax_cond _ Pj). Qed. + +Lemma bigmax_leP m P F : reflect (x <= m /\ forall i, P i -> F i <= m) + (\big[max/x]_(i | P i) F i <= m). +Proof. +apply: (iffP idP) => [|[? ?]]; last exact: bigmax_le. +rewrite bigmax_idl le_maxl => /andP[-> leFm]; split=> // i Pi. +by apply: le_trans leFm; exact: le_bigmax_cond. +Qed. + +Lemma bigmax_ltP m P F : + reflect (x < m /\ forall i, P i -> F i < m) (\big[max/x]_(i | P i) F i < m). +Proof. +apply: (iffP idP) => [|[? ?]]; last exact: bigmax_lt. +rewrite bigmax_idl lt_maxl => /andP[-> ltFm]; split=> // i Pi. +by apply: le_lt_trans ltFm; exact: le_bigmax_cond. +Qed. + +Lemma bigmax_eq_arg j P F : P j -> (forall i, P i -> x <= F i) -> + \big[max/x]_(i | P i) F i = F [arg max_(i > j | P i) F i]. +Proof. +move=> Pi0; case: arg_maxP => //= i Pi PF PxF. +apply/eqP; rewrite eq_le le_bigmax_cond // andbT. +by apply/bigmax_leP; split => //; exact: PxF. +Qed. + +Lemma eq_bigmax j P F : P j -> (forall i, P i -> x <= F i) -> + {i0 | i0 \in I & \big[max/x]_(i | P i) F i = F i0}. +Proof. by move=> Pi0 Hx; rewrite (bigmax_eq_arg Pi0) //; eexists. Qed. + +Lemma homo_le_bigmax P F1 F2 : (forall i, P i -> F1 i <= F2 i) -> + \big[max/x]_(i | P i) F1 i <= \big[max/x]_(i | P i) F2 i. +Proof. +move=> FG; elim/big_ind2 : _ => // a b e f ba fe. +rewrite le_maxr 2!le_maxl ba fe /= andbT; have [//|/= af] := leP f a. +by rewrite (le_trans ba) // (le_trans _ fe) // ltW. +Qed. + +End bigmax_finType. + +End bigmax. +Arguments bigmax_mkcond {d T I r}. +Arguments bigmaxID {d T I r}. +Arguments bigmaxD1 {d T I x} j. +Arguments bigmax_sup {d T I x} j. +Arguments bigmax_eq_arg {d T I} x j. +Arguments eq_bigmax {d T I x} j. + +Section bigmin. +Local Notation min := Order.min. +Local Open Scope order_scope. +Variables (d : _) (T : orderType d). + +Section bigmin_Type. +Variable (I : Type) (r : seq I) (x : T). +Implicit Types (P a : pred I) (F : I -> T). + +Lemma bigmin_mkcond P F : \big[min/x]_(i <- r | P i) F i = + \big[min/x]_(i <- r) (if P i then F i else x). +Proof. rewrite big_mkcond_idem ?minxx//; [exact: minA|exact: minC]. Qed. + +Lemma bigmin_split P F1 F2 : + \big[min/x]_(i <- r | P i) (min (F1 i) (F2 i)) = + min (\big[min/x]_(i <- r | P i) F1 i) (\big[min/x]_(i <- r | P i) F2 i). +Proof. rewrite big_split_idem ?minxx//; [exact: minA|exact: minC]. Qed. + +Lemma bigmin_idl P F : + \big[min/x]_(i <- r | P i) F i = min x (\big[min/x]_(i <- r | P i) F i). +Proof. rewrite minC big_id_idem ?minxx//; exact: minA. Qed. + +Lemma bigmin_idr P F : + \big[min/x]_(i <- r | P i) F i = min (\big[min/x]_(i <- r | P i) F i) x. +Proof. by rewrite [LHS]bigmin_idl minC. Qed. + +Lemma bigminID a P F : \big[min/x]_(i <- r | P i) F i = + min (\big[min/x]_(i <- r | P i && a i) F i) + (\big[min/x]_(i <- r | P i && ~~ a i) F i). +Proof. by rewrite (bigID_idem minA minC _ _ a) ?minxx. Qed. + +End bigmin_Type. + +Section bigmin_finType. +Variable (I : finType) (x : T). +Implicit Types (P : pred I) (F : I -> T). + +Lemma bigminD1 j P F : P j -> + \big[min/x]_(i | P i) F i = min (F j) (\big[min/x]_(i | P i && (i != j)) F i). +Proof. by move/(bigD1_AC minA minC _ _) ->. Qed. + +Lemma bigmin_le_cond j P F : P j -> \big[min/x]_(i | P i) F i <= F j. +Proof. +have := mem_index_enum j; rewrite unlock; elim: (index_enum I) => //= i l ih. +rewrite inE => /orP [/eqP-> ->|/ih leminlfi Pi]; first by rewrite le_minl lexx. +by case: ifPn => Pj; [rewrite le_minl leminlfi// orbC|exact: leminlfi]. +Qed. + +Lemma bigmin_le j F : \big[min/x]_i F i <= F j. +Proof. exact: bigmin_le_cond. Qed. + +Lemma bigmin_inf j P m F : P j -> F j <= m -> \big[min/x]_(i | P i) F i <= m. +Proof. by move=> Pj ?; apply: le_trans (bigmin_le_cond _ Pj) _. Qed. + +Lemma bigmin_geP m P F : reflect (m <= x /\ forall i, P i -> m <= F i) + (m <= \big[min/x]_(i | P i) F i). +Proof. +apply: (iffP idP) => [lemFi|[lemx lemPi]]; [split|exact: le_bigmin]. +- by rewrite (le_trans lemFi)// bigmin_idl le_minl lexx. +- by move=> i Pi; rewrite (le_trans lemFi)// (bigminD1 _ Pi)// le_minl lexx. +Qed. + +Lemma bigmin_gtP m P F : + reflect (m < x /\ forall i, P i -> m < F i) (m < \big[min/x]_(i | P i) F i). +Proof. +apply: (iffP idP) => [lemFi|[lemx lemPi]]; [split|exact: lt_bigmin]. +- by rewrite (lt_le_trans lemFi)// bigmin_idl le_minl lexx. +- by move=> i Pi; rewrite (lt_le_trans lemFi)// (bigminD1 _ Pi)// le_minl lexx. +Qed. + +Lemma bigmin_eq_arg j P F : P j -> (forall i, P i -> F i <= x) -> + \big[min/x]_(i | P i) F i = F [arg min_(i < j | P i) F i]. +Proof. +move=> Pi0; case: arg_minP => //= i Pi PF PFx. +apply/eqP; rewrite eq_le bigmin_le_cond //=. +by apply/bigmin_geP; split => //; exact: PFx. +Qed. + +Lemma eq_bigmin j P F : P j -> (forall i, P i -> F i <= x) -> + {i0 | i0 \in I & \big[min/x]_(i | P i) F i = F i0}. +Proof. by move=> Pi0 Hx; rewrite (bigmin_eq_arg Pi0) //; eexists. Qed. + +End bigmin_finType. + +End bigmin. +Arguments bigmin_mkcond {d T I r}. +Arguments bigminID {d T I r}. +Arguments bigminD1 {d T I x} j. +Arguments bigmin_inf {d T I x} j. +Arguments bigmin_eq_arg {d T I} x j. +Arguments eq_bigmin {d T I x} j. + +Reserved Notation "`1- r" (format "`1- r", at level 2). + +Section onem. +Variable R : numDomainType. +Implicit Types r : R. + +Definition onem r := 1 - r. +Local Notation "`1- r" := (onem r). + +Lemma onem0 : `1-0 = 1. Proof. by rewrite /onem subr0. Qed. + +Lemma onem1 : `1-1 = 0. Proof. by rewrite /onem subrr. Qed. + +Lemma onemK r : `1-(`1-r) = r. +Proof. by rewrite /onem opprB addrCA subrr addr0. Qed. + +Lemma onem_gt0 r : r < 1 -> 0 < `1-r. Proof. by rewrite subr_gt0. Qed. + +Lemma onem_ge0 r : r <= 1 -> 0 <= `1-r. +Proof. by rewrite le_eqVlt => /predU1P[->|/onem_gt0/ltW]; rewrite ?onem1. Qed. + +Lemma onem_le1 r : 0 <= r -> `1-r <= 1. +Proof. by rewrite ler_subl_addr ler_addl. Qed. + +Lemma onem_lt1 r : 0 < r -> `1-r < 1. +Proof. by rewrite ltr_subl_addr ltr_addl. Qed. + +Lemma onemX_ge0 r n : 0 <= r -> r <= 1 -> 0 <= `1-(r ^+ n). +Proof. by move=> ? ?; rewrite subr_ge0 exprn_ile1. Qed. + +Lemma onemX_lt1 r n : 0 < r -> `1-(r ^+ n) < 1. +Proof. by move=> ?; rewrite onem_lt1// exprn_gt0. Qed. + +Lemma onemD r s : `1-(r + s) = `1-r - s. +Proof. by rewrite /onem addrAC opprD addrA addrAC. Qed. + +Lemma onemMr r s : s * `1-r = s - s * r. +Proof. by rewrite /onem mulrBr mulr1. Qed. + +Lemma onemM r s : `1-(r * s) = `1-r + `1-s - `1-r * `1-s. +Proof. +rewrite /onem mulrBr mulr1 mulrBl mul1r opprB -addrA. +by rewrite (addrC (1 - r)) !addrA subrK opprB addrA subrK addrK. +Qed. + +Lemma onem_lt : {mono onem : x y /~ x <= y}. +Proof. +by move=> x y; rewrite ler_subl_addl addrA ler_subr_addr addrC ler_add2r. +Qed. + +End onem. +Notation "`1- r" := (onem r) : ring_scope. + +Lemma lez_abs2 (a b : int) : 0 <= a -> a <= b -> (`|a| <= `|b|)%N. +Proof. by case: a => //= n _; case: b. Qed. \ No newline at end of file diff --git a/theories/real_interval.v b/theories/real_interval.v index 11f90a366..332be63e8 100644 --- a/theories/real_interval.v +++ b/theories/real_interval.v @@ -199,6 +199,13 @@ have [i0 /(congr1 (@Rhull _))|] := boolP (neitv i). by rewrite negbK => /eqP ->; rewrite predeqE => /(_ 0)[_]/(_ Logic.I). Qed. +Lemma set_itv_set (a b r :R) : r \in `[a,b] = (r \in `[a,b]%classic). +Proof. +rewrite ?in_itv /= ?mem_setE ?in_itv /=. +by apply: Bool.eq_true_iff_eq; split => /andP [] P Q; apply/andP; split. +Qed. + + End set_itv_realType. Section Rhull_lemmas. diff --git a/theories/topology.v b/theories/topology.v index 401ce7aec..9b714cda8 100644 --- a/theories/topology.v +++ b/theories/topology.v @@ -6107,13 +6107,6 @@ case: (y in _ @[_ --> y]) / (nbhs_subspaceP x) => Ax. by move=> ? /nbhs_singleton //= ?; rewrite nbhs_simpl => ? ->. Qed. -Lemma subspace_eq_continuous {S : topologicalType} (f g : subspace A -> S) : - {in A, f =1 g} -> continuous f -> continuous g. -Proof. -rewrite ?subspace_continuousP=> feq L x Ax; rewrite -(feq x) ?inE //. -by apply: cvg_trans _ (L x Ax); apply: fmap_within_eq=> ? ?; rewrite feq. -Qed. - Lemma continuous_subspace_in {U : topologicalType} (f : subspace A -> U) : continuous f = {in A, continuous f}. Proof. @@ -6299,6 +6292,17 @@ Section SubspaceRelative. Context {T : topologicalType}. Implicit Types (U : topologicalType) (A B : set T). +Lemma subspace_eq_continuous {U} A (f g : T -> U) : + {in A, f =1 g} -> {within A, continuous f} -> {within A, continuous g}. +Proof. +rewrite ?subspace_continuousP=> feq L x Ax; rewrite -(feq x) ?inE //. +by apply: cvg_trans _ (L x Ax); apply: fmap_within_eq=> ? ?; rewrite feq. +Qed. + +Lemma within_continuousE {U} A (f : T -> U) : + {within A, continuous f} = continuous (f : subspace A -> U). +Proof. done. Qed. + Lemma nbhs_subspace_subset A B (x : T) : A `<=` B -> nbhs (x : subspace B) `<=` nbhs (x : subspace A). Proof. @@ -6346,6 +6350,13 @@ move=> ctsf; rewrite continuous_subspace_in => ? ?. exact: continuous_in_subspaceT. Qed. +Lemma continuous_subspaceTE {U} (f : T -> U) : + {within [set: T], continuous f} = continuous f. +Proof. +rewrite propeqE; split; last exact: continuous_subspaceT. +by move=> + x Q nQ /= => /(_ x Q nQ) /=; rewrite nbhs_simpl /= ?nbhs_subspaceT. +Qed. + Lemma continuous_open_subspace {U} A (f : T -> U) : open A -> {within A, continuous f} = {in A, continuous f}. Proof. @@ -6376,10 +6387,12 @@ rewrite [RHS]setIUr -V2W -V1W eqEsubset; split=> ?. by case=> [][] ? ?; split=> []; [left; split | left | right; split | right]. Qed. -Lemma subspaceT_continuous {U} A (B : set U) (f : {fun A >-> B}) : - {within A, continuous f} -> continuous (f : subspace A -> subspace B). +Lemma subspaceT_continuous {U} A (B : set U) (f : T -> U) : + set_fun A B f -> + {within A, continuous f} -> + continuous (f : subspace A -> subspace B). Proof. -move=> /continuousP ctsf; apply/continuousP => O /open_subspaceP [V [oV VBOB]]. +move=> funS /continuousP ctsf; apply/continuousP => O /open_subspaceP [V [oV VBOB]]. rewrite -open_subspaceIT; apply/open_subspaceP. case/open_subspaceP: (ctsf _ oV) => W [oW fVA]; exists W; split => //. rewrite fVA -setIA setIid eqEsubset; split => x [fVx Ax]; split => //. From e86b5d4d00cd15cd2dd0e6323ab57b2830f28246 Mon Sep 17 00:00:00 2001 From: zstone Date: Thu, 20 Oct 2022 15:54:01 -0400 Subject: [PATCH 2/3] cleaning up rebase --- CHANGELOG_UNRELEASED.md | 3 - theories/mathcomp_extra.v | 604 -------------------------------------- 2 files changed, 607 deletions(-) delete mode 100644 theories/mathcomp_extra.v diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 8f404e04f..6e4b434fb 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -126,7 +126,6 @@ + generalize `lte_addl`, `lte_addr`, `gte_subl`, `gte_subr`, `lte_daddl`, `lte_daddr`, `gte_dsubl`, `gte_dsubr` - in `topology.v`: - + lemma `weak_subspace_open` + lemmas `continuous_subspace0`, `continuous_subspace1` - in `realfun.v`: @@ -184,8 +183,6 @@ + lemma `lte_spaddr`, renamed `lte_spaddre` ### Removed -- in `realFun.v`: - + removed `continuous_subspace_itv` - in file `classical_sets.v`: + lemmas `pred_oappE` and `pred_oapp_set` (moved to `mathcomp_extra.v`) diff --git a/theories/mathcomp_extra.v b/theories/mathcomp_extra.v deleted file mode 100644 index 4d0611659..000000000 --- a/theories/mathcomp_extra.v +++ /dev/null @@ -1,604 +0,0 @@ -(* mathcomp analysis (c) 2022 Inria and AIST. License: CeCILL-C. *) -From mathcomp Require choice. -(* Missing coercion (done before Import to avoid redeclaration error, - thanks to KS for the trick) *) -(* MathComp 1.15 addition *) -Coercion choice.Choice.mixin : choice.Choice.class_of >-> choice.Choice.mixin_of. -From mathcomp Require Import all_ssreflect finmap ssralg ssrnum ssrint rat. -From mathcomp Require Import finset interval. -From mathcomp.classical Require Import boolp classical_sets. -From mathcomp.classical Require Export mathcomp_extra. - -(***************************) -(* MathComp 1.15 additions *) -(***************************) - -(******************************************************************************) -(* This files contains lemmas and definitions missing from MathComp. *) -(* *) -(* f \max g := fun x => Num.max (f x) (g x) *) -(* lteBSide, bnd_simp == multirule to simplify inequalities between *) -(* interval bounds *) -(* miditv i == middle point of interval i *) -(* *) -(******************************************************************************) - -Set Implicit Arguments. -Unset Strict Implicit. -Unset Printing Implicit Defensive. - -Reserved Notation "f \max g" (at level 50, left associativity). - -Lemma enum_ord0 : enum 'I_0 = [::]. -Proof. by apply/eqP; rewrite -size_eq0 size_enum_ord. Qed. - -Lemma enum_ordSr n : enum 'I_n.+1 = - rcons (map (widen_ord (leqnSn _)) (enum 'I_n)) ord_max. -Proof. -apply: (inj_map val_inj); rewrite val_enum_ord. -rewrite -[in iota _ _]addn1 iotaD/= cats1 map_rcons; congr (rcons _ _). -by rewrite -map_comp/= (@eq_map _ _ _ val) ?val_enum_ord. -Qed. - -Lemma obindEapp {aT rT} (f : aT -> option rT) : obind f = oapp f None. -Proof. by []. Qed. - -Lemma omapEbind {aT rT} (f : aT -> rT) : omap f = obind (olift f). -Proof. by []. Qed. - -Lemma omapEapp {aT rT} (f : aT -> rT) : omap f = oapp (olift f) None. -Proof. by []. Qed. - -Lemma oappEmap {aT rT} (f : aT -> rT) (y0 : rT) x : - oapp f y0 x = odflt y0 (omap f x). -Proof. by case: x. Qed. - -Lemma omap_comp aT rT sT (f : aT -> rT) (g : rT -> sT) : - omap (g \o f) =1 omap g \o omap f. -Proof. by case. Qed. - -Lemma oapp_comp_f {aT rT sT} (f : aT -> rT) (g : rT -> sT) (x : rT) : - oapp (g \o f) (g x) =1 g \o oapp f x. -Proof. by case. Qed. - -Lemma can_in_comp [A B C : Type] (D : {pred B}) (D' : {pred C}) - [f : B -> A] [h : C -> B] - [f' : A -> B] [h' : B -> C] : - {homo h : x / x \in D' >-> x \in D} -> - {in D, cancel f f'} -> {in D', cancel h h'} -> - {in D', cancel (f \o h) (h' \o f')}. -Proof. by move=> hD fK hK c cD /=; rewrite fK ?hK ?hD. Qed. - -Lemma in_inj_comp A B C (f : B -> A) (h : C -> B) (P : pred B) (Q : pred C) : - {in P &, injective f} -> {in Q &, injective h} -> {homo h : x / Q x >-> P x} -> - {in Q &, injective (f \o h)}. -Proof. -by move=> Pf Qh QP x y xQ yQ xy; apply Qh => //; apply Pf => //; apply QP. -Qed. - -Lemma pcan_in_comp [A B C : Type] (D : {pred B}) (D' : {pred C}) - [f : B -> A] [h : C -> B] - [f' : A -> option B] [h' : B -> option C] : - {homo h : x / x \in D' >-> x \in D} -> - {in D, pcancel f f'} -> {in D', pcancel h h'} -> - {in D', pcancel (f \o h) (obind h' \o f')}. -Proof. by move=> hD fK hK c cD /=; rewrite fK/= ?hK ?hD. Qed. - -Lemma ocan_comp [A B C : Type] [f : B -> option A] [h : C -> option B] - [f' : A -> B] [h' : B -> C] : - ocancel f f' -> ocancel h h' -> ocancel (obind f \o h) (h' \o f'). -Proof. -move=> fK hK c /=; rewrite -[RHS]hK/=; case hcE : (h c) => [b|]//=. -by rewrite -[b in RHS]fK; case: (f b) => //=; have := hK c; rewrite hcE. -Qed. - -Lemma eqbLR (b1 b2 : bool) : b1 = b2 -> b1 -> b2. -Proof. by move->. Qed. - -Import Order.TTheory GRing.Theory Num.Theory. - -Definition max_fun T (R : numDomainType) (f g : T -> R) x := Num.max (f x) (g x). -Notation "f \max g" := (max_fun f g) : ring_scope. -Arguments max_fun {T R} _ _ _ /. - -Lemma gtr_opp (R : numDomainType) (r : R) : (0 < r)%R -> (- r < r)%R. -Proof. by move=> n0; rewrite -subr_lt0 -opprD oppr_lt0 addr_gt0. Qed. - -Lemma le_le_trans {disp : unit} {T : porderType disp} (x y z t : T) : - (z <= x)%O -> (y <= t)%O -> (x <= y)%O -> (z <= t)%O. -Proof. by move=> + /(le_trans _)/[apply]; apply: le_trans. Qed. - -Notation eqLHS := (X in (X == _))%pattern. -Notation eqRHS := (X in (_ == X))%pattern. -Notation leLHS := (X in (X <= _)%O)%pattern. -Notation leRHS := (X in (_ <= X)%O)%pattern. -Notation ltLHS := (X in (X < _)%O)%pattern. -Notation ltRHS := (X in (_ < X)%O)%pattern. -Inductive boxed T := Box of T. - -Lemma eq_bigl_supp [R : eqType] [idx : R] [op : Monoid.law idx] [I : Type] - [r : seq I] [P1 : pred I] (P2 : pred I) (F : I -> R) : - {in [pred x | F x != idx], P1 =1 P2} -> - \big[op/idx]_(i <- r | P1 i) F i = \big[op/idx]_(i <- r | P2 i) F i. -Proof. -move=> P12; rewrite big_mkcond [RHS]big_mkcond; apply: eq_bigr => i _. -by case: (eqVneq (F i) idx) => [->|/P12->]; rewrite ?if_same. -Qed. - -Lemma perm_big_supp_cond [R : eqType] [idx : R] [op : Monoid.com_law idx] [I : eqType] - [r s : seq I] [P : pred I] (F : I -> R) : - perm_eq [seq i <- r | P i && (F i != idx)] [seq i <- s | P i && (F i != idx)] -> - \big[op/idx]_(i <- r | P i) F i = \big[op/idx]_(i <- s| P i) F i. -Proof. -move=> prs; rewrite !(bigID [pred i | F i == idx] P F)/=. -rewrite big1 ?Monoid.mul1m; last by move=> i /andP[_ /eqP->]. -rewrite [in RHS]big1 ?Monoid.mul1m; last by move=> i /andP[_ /eqP->]. -by rewrite -[in LHS]big_filter -[in RHS]big_filter; apply perm_big. -Qed. - -Lemma perm_big_supp [R : eqType] [idx : R] [op : Monoid.com_law idx] [I : eqType] - [r s : seq I] [P : pred I] (F : I -> R) : - perm_eq [seq i <- r | (F i != idx)] [seq i <- s | (F i != idx)] -> - \big[op/idx]_(i <- r | P i) F i = \big[op/idx]_(i <- s| P i) F i. -Proof. -by move=> ?; apply: perm_big_supp_cond; rewrite !filter_predI perm_filter. -Qed. - -Local Open Scope order_scope. -Local Open Scope ring_scope. -Import GRing.Theory Order.TTheory. - -Lemma mulr_ge0_gt0 (R : numDomainType) (x y : R) : 0 <= x -> 0 <= y -> - (0 < x * y) = (0 < x) && (0 < y). -Proof. -rewrite le_eqVlt => /predU1P[<-|x0]; first by rewrite mul0r ltxx. -rewrite le_eqVlt => /predU1P[<-|y0]; first by rewrite mulr0 ltxx andbC. -by apply/idP/andP=> [|_]; rewrite pmulr_rgt0. -Qed. - -Section lt_le_gt_ge. -Variable (R : numFieldType). -Implicit Types x y z a b : R. - -Lemma splitr x : x = x / 2%:R + x / 2%:R. -Proof. by rewrite -mulr2n -mulr_natr mulfVK //= pnatr_eq0. Qed. - -Lemma ler_addgt0Pr x y : reflect (forall e, e > 0 -> x <= y + e) (x <= y). -Proof. -apply/(iffP idP)=> [lexy e e_gt0 | lexye]; first by rewrite ler_paddr// ltW. -have [||ltyx]// := comparable_leP. - rewrite (@comparabler_trans _ (y + 1))// /Order.comparable ?lexye ?ltr01//. - by rewrite ler_addl ler01 orbT. -have /midf_lt [_] := ltyx; rewrite le_gtF//. -rewrite -(@addrK _ y y) addrAC -addrA 2!mulrDl -splitr lexye//. -by rewrite divr_gt0// ?ltr0n// subr_gt0. -Qed. - -Lemma ler_addgt0Pl x y : reflect (forall e, e > 0 -> x <= e + y) (x <= y). -Proof. -by apply/(equivP (ler_addgt0Pr x y)); split=> lexy e /lexy; rewrite addrC. -Qed. - -Lemma in_segment_addgt0Pr x y z : - reflect (forall e, e > 0 -> y \in `[x - e, z + e]) (y \in `[x, z]). -Proof. -apply/(iffP idP)=> [xyz e /[dup] e_gt0 /ltW e_ge0 | xyz_e]. - by rewrite in_itv /= ler_subl_addr !ler_paddr// (itvP xyz). -by rewrite in_itv /= ; apply/andP; split; apply/ler_addgt0Pr => ? /xyz_e; - rewrite in_itv /= ler_subl_addr => /andP []. -Qed. - -Lemma in_segment_addgt0Pl x y z : - reflect (forall e, e > 0 -> y \in `[(- e + x), (e + z)]) (y \in `[x, z]). -Proof. -apply/(equivP (in_segment_addgt0Pr x y z)). -by split=> zxy e /zxy; rewrite [z + _]addrC [_ + x]addrC. -Qed. - -Lemma lt_le a b : (forall x, x < a -> x < b) -> a <= b. -Proof. -move=> ab; apply/ler_addgt0Pr => e e_gt0; rewrite -ler_subl_addr ltW//. -by rewrite ab // ltr_subl_addr -ltr_subl_addl subrr. -Qed. - -Lemma gt_ge a b : (forall x, b < x -> a < x) -> a <= b. -Proof. -move=> ab; apply/ler_addgt0Pr => e e_gt0. -by rewrite ltW// ab// -ltr_subl_addl subrr. -Qed. - -End lt_le_gt_ge. - -(**********************************) -(* End of MathComp 1.15 additions *) -(**********************************) - -Lemma natr1 (R : ringType) (n : nat) : (n%:R + 1 = n.+1%:R :> R)%R. -Proof. by rewrite GRing.mulrSr. Qed. - -Lemma nat1r (R : ringType) (n : nat) : (1 + n%:R = n.+1%:R :> R)%R. -Proof. by rewrite GRing.mulrS. Qed. - -(* To be backported to finmap *) - -Lemma fset_nat_maximum (X : choiceType) (A : {fset X}) - (f : X -> nat) : A != fset0 -> - (exists i, i \in A /\ forall j, j \in A -> f j <= f i)%nat. -Proof. -move=> /fset0Pn[x Ax]. -have [/= y _ /(_ _ isT) mf] := @arg_maxnP _ [` Ax]%fset xpredT (f \o val) isT. -exists (val y); split; first exact: valP. -by move=> z Az; have := mf [` Az]%fset. -Qed. - -Lemma image_nat_maximum n (f : nat -> nat) : - (exists i, i <= n /\ forall j, j <= n -> f j <= f i)%N. -Proof. -have [i _ /(_ _ isT) mf] := @arg_maxnP _ (@ord0 n) xpredT f isT. -by exists i; split; rewrite ?leq_ord// => j jn; have := mf (@Ordinal n.+1 j jn). -Qed. - -Lemma card_fset_sum1 (T : choiceType) (A : {fset T}) : - #|` A| = (\sum_(i <- A) 1)%N. -Proof. by rewrite big_seq_fsetE/= sum1_card cardfE. Qed. - -Arguments big_rmcond {R idx op I r} P. -Arguments big_rmcond_in {R idx op I r} P. - -(*******************************) -(* MathComp > 1.15.0 additions *) -(*******************************) - -Section bigminr_maxr. -Import Num.Def. - -Lemma bigminr_maxr (R : realDomainType) I r (P : pred I) (F : I -> R) x : - \big[minr/x]_(i <- r | P i) F i = - \big[maxr/- x]_(i <- r | P i) - F i. -Proof. -by elim/big_rec2: _ => [|i y _ _ ->]; rewrite ?oppr_max opprK. -Qed. -End bigminr_maxr. - -Section SemiGroupProperties. -Variables (R : Type) (op : R -> R -> R). -Hypothesis opA : associative op. - -Section Id. -Variable x : R. -Hypothesis opxx : op x x = x. - -Lemma big_const_idem I (r : seq I) P : \big[op/x]_(i <- r | P i) x = x. -Proof. by elim/big_ind : _ => // _ _ -> ->. Qed. - -Lemma big_id_idem I (r : seq I) P F : - op (\big[op/x]_(i <- r | P i) F i) x = \big[op/x]_(i <- r | P i) F i. -Proof. by elim/big_rec : _ => // ? ? ?; rewrite -opA => ->. Qed. - -End Id. - -Section Abelian. -Hypothesis opC : commutative op. - -Let opCA : left_commutative op. Proof. by move=> x *; rewrite !opA (opC x). Qed. - -Variable x : R. - -Lemma big_rem_AC (I : eqType) (r : seq I) z (P : pred I) F : z \in r -> - \big[op/x]_(y <- r | P y) F y = - if P z then op (F z) (\big[op/x]_(y <- rem z r | P y) F y) - else \big[op/x]_(y <- rem z r | P y) F y. -Proof. -elim: r =>// i r ih; rewrite big_cons rem_cons inE =>/predU1P[-> /[!eqxx]//|zr]. -by case: eqP => [-> //|]; rewrite ih// big_cons; case: ifPn; case: ifPn. -Qed. - -Lemma bigD1_AC (I : finType) j (P : pred I) F : P j -> - \big[op/x]_(i | P i) F i = op (F j) (\big[op/x]_(i | P i && (i != j)) F i). -Proof. -rewrite (big_rem_AC _ _ (mem_index_enum j)) => ->. -by rewrite rem_filter ?index_enum_uniq// big_filter_cond big_andbC. -Qed. - -Section Id. -Hypothesis opxx : op x x = x. - -Lemma big_mkcond_idem I r (P : pred I) F : - \big[op/x]_(i <- r | P i) F i = \big[op/x]_(i <- r) (if P i then F i else x). -Proof. -elim: r => [|i r]; rewrite ?(big_nil, big_cons)//. -by case: ifPn => Pi ->//; rewrite -[in LHS]big_id_idem. -Qed. - -Lemma big_split_idem I r (P : pred I) F1 F2 : - \big[op/x]_(i <- r | P i) op (F1 i) (F2 i) = - op (\big[op/x]_(i <- r | P i) F1 i) (\big[op/x]_(i <- r | P i) F2 i). -Proof. by elim/big_rec3 : _ => [//|i ? ? _ _ ->]; rewrite // opCA -!opA opCA. Qed. - -Lemma big_id_idem_AC I (r : seq I) P F : - \big[op/x]_(i <- r | P i) op (F i) x = \big[op/x]_(i <- r | P i) F i. -Proof. by rewrite big_split_idem big_const_idem ?big_id_idem. Qed. - -Lemma bigID_idem I r (a P : pred I) F : - \big[op/x]_(i <- r | P i) F i = - op (\big[op/x]_(i <- r | P i && a i) F i) - (\big[op/x]_(i <- r | P i && ~~ a i) F i). -Proof. -rewrite -big_id_idem_AC big_mkcond_idem !(big_mkcond_idem _ _ F) -big_split_idem. -by apply: eq_bigr => i; case: ifPn => //=; case: ifPn. -Qed. - -End Id. - -End Abelian. - -End SemiGroupProperties. - -Section bigmaxmin. -Local Notation max := Order.max. -Local Notation min := Order.min. -Local Open Scope order_scope. -Variables (d : _) (T : porderType d). -Variables (I : finType) (f : I -> T) (x0 x : T) (P : pred I). - -Lemma bigmax_le : - x0 <= x -> (forall i, P i -> f i <= x) -> \big[max/x0]_(i | P i) f i <= x. -Proof. by move=> ? ?; elim/big_ind: _ => // *; rewrite maxEle; case: ifPn. Qed. - -Lemma bigmax_lt : - x0 < x -> (forall i, P i -> f i < x) -> \big[max/x0]_(i | P i) f i < x. -Proof. by move=> ? ?; elim/big_ind: _ => // *; rewrite maxElt; case: ifPn. Qed. - -Lemma lt_bigmin : - x < x0 -> (forall i, P i -> x < f i) -> x < \big[min/x0]_(i | P i) f i. -Proof. by move=> ? ?; elim/big_ind: _ => // *; rewrite minElt; case: ifPn. Qed. - -Lemma le_bigmin : - x <= x0 -> (forall i, P i -> x <= f i) -> x <= \big[min/x0]_(i | P i) f i. -Proof. by move=> ? ?; elim/big_ind: _ => // *; rewrite minEle; case: ifPn. Qed. - -End bigmaxmin. - -Section bigmax. -Local Notation max := Order.max. -Local Open Scope order_scope. -Variables (d : unit) (T : orderType d). - -Section bigmax_Type. -Variables (I : Type) (r : seq I) (x : T). -Implicit Types (P a : pred I) (F : I -> T). - -Lemma bigmax_mkcond P F : \big[max/x]_(i <- r | P i) F i = - \big[max/x]_(i <- r) (if P i then F i else x). -Proof. by rewrite big_mkcond_idem ?maxxx//; [exact: maxA|exact: maxC]. Qed. - -Lemma bigmax_split P F1 F2 : - \big[max/x]_(i <- r | P i) (max (F1 i) (F2 i)) = - max (\big[max/x]_(i <- r | P i) F1 i) (\big[max/x]_(i <- r | P i) F2 i). -Proof. by rewrite big_split_idem ?maxxx//; [exact: maxA|exact: maxC]. Qed. - -Lemma bigmax_idl P F : - \big[max/x]_(i <- r | P i) F i = max x (\big[max/x]_(i <- r | P i) F i). -Proof. by rewrite maxC big_id_idem ?maxxx//; exact: maxA. Qed. - -Lemma bigmax_idr P F : - \big[max/x]_(i <- r | P i) F i = max (\big[max/x]_(i <- r | P i) F i) x. -Proof. by rewrite [LHS]bigmax_idl maxC. Qed. - -Lemma bigmaxID a P F : \big[max/x]_(i <- r | P i) F i = - max (\big[max/x]_(i <- r | P i && a i) F i) - (\big[max/x]_(i <- r | P i && ~~ a i) F i). -Proof. by rewrite (bigID_idem maxA maxC _ _ a) ?maxxx. Qed. - -End bigmax_Type. - -Section bigmax_finType. -Variables (I : finType) (x : T). -Implicit Types (P : pred I) (F : I -> T). - -Lemma bigmaxD1 j P F : P j -> - \big[max/x]_(i | P i) F i = max (F j) (\big[max/x]_(i | P i && (i != j)) F i). -Proof. by move/(bigD1_AC maxA maxC) ->. Qed. - -Lemma le_bigmax_cond j P F : P j -> F j <= \big[max/x]_(i | P i) F i. -Proof. by move=> Pj; rewrite (bigmaxD1 _ Pj) le_maxr lexx. Qed. - -Lemma le_bigmax F j : F j <= \big[max/x]_i F i. -Proof. exact: le_bigmax_cond. Qed. - -(* NB: as of [2022-08-02], bigop.bigmax_sup already exists for nat *) -Lemma bigmax_sup j P m F : P j -> m <= F j -> m <= \big[max/x]_(i | P i) F i. -Proof. by move=> Pj ?; apply: le_trans (le_bigmax_cond _ Pj). Qed. - -Lemma bigmax_leP m P F : reflect (x <= m /\ forall i, P i -> F i <= m) - (\big[max/x]_(i | P i) F i <= m). -Proof. -apply: (iffP idP) => [|[? ?]]; last exact: bigmax_le. -rewrite bigmax_idl le_maxl => /andP[-> leFm]; split=> // i Pi. -by apply: le_trans leFm; exact: le_bigmax_cond. -Qed. - -Lemma bigmax_ltP m P F : - reflect (x < m /\ forall i, P i -> F i < m) (\big[max/x]_(i | P i) F i < m). -Proof. -apply: (iffP idP) => [|[? ?]]; last exact: bigmax_lt. -rewrite bigmax_idl lt_maxl => /andP[-> ltFm]; split=> // i Pi. -by apply: le_lt_trans ltFm; exact: le_bigmax_cond. -Qed. - -Lemma bigmax_eq_arg j P F : P j -> (forall i, P i -> x <= F i) -> - \big[max/x]_(i | P i) F i = F [arg max_(i > j | P i) F i]. -Proof. -move=> Pi0; case: arg_maxP => //= i Pi PF PxF. -apply/eqP; rewrite eq_le le_bigmax_cond // andbT. -by apply/bigmax_leP; split => //; exact: PxF. -Qed. - -Lemma eq_bigmax j P F : P j -> (forall i, P i -> x <= F i) -> - {i0 | i0 \in I & \big[max/x]_(i | P i) F i = F i0}. -Proof. by move=> Pi0 Hx; rewrite (bigmax_eq_arg Pi0) //; eexists. Qed. - -Lemma homo_le_bigmax P F1 F2 : (forall i, P i -> F1 i <= F2 i) -> - \big[max/x]_(i | P i) F1 i <= \big[max/x]_(i | P i) F2 i. -Proof. -move=> FG; elim/big_ind2 : _ => // a b e f ba fe. -rewrite le_maxr 2!le_maxl ba fe /= andbT; have [//|/= af] := leP f a. -by rewrite (le_trans ba) // (le_trans _ fe) // ltW. -Qed. - -End bigmax_finType. - -End bigmax. -Arguments bigmax_mkcond {d T I r}. -Arguments bigmaxID {d T I r}. -Arguments bigmaxD1 {d T I x} j. -Arguments bigmax_sup {d T I x} j. -Arguments bigmax_eq_arg {d T I} x j. -Arguments eq_bigmax {d T I x} j. - -Section bigmin. -Local Notation min := Order.min. -Local Open Scope order_scope. -Variables (d : _) (T : orderType d). - -Section bigmin_Type. -Variable (I : Type) (r : seq I) (x : T). -Implicit Types (P a : pred I) (F : I -> T). - -Lemma bigmin_mkcond P F : \big[min/x]_(i <- r | P i) F i = - \big[min/x]_(i <- r) (if P i then F i else x). -Proof. rewrite big_mkcond_idem ?minxx//; [exact: minA|exact: minC]. Qed. - -Lemma bigmin_split P F1 F2 : - \big[min/x]_(i <- r | P i) (min (F1 i) (F2 i)) = - min (\big[min/x]_(i <- r | P i) F1 i) (\big[min/x]_(i <- r | P i) F2 i). -Proof. rewrite big_split_idem ?minxx//; [exact: minA|exact: minC]. Qed. - -Lemma bigmin_idl P F : - \big[min/x]_(i <- r | P i) F i = min x (\big[min/x]_(i <- r | P i) F i). -Proof. rewrite minC big_id_idem ?minxx//; exact: minA. Qed. - -Lemma bigmin_idr P F : - \big[min/x]_(i <- r | P i) F i = min (\big[min/x]_(i <- r | P i) F i) x. -Proof. by rewrite [LHS]bigmin_idl minC. Qed. - -Lemma bigminID a P F : \big[min/x]_(i <- r | P i) F i = - min (\big[min/x]_(i <- r | P i && a i) F i) - (\big[min/x]_(i <- r | P i && ~~ a i) F i). -Proof. by rewrite (bigID_idem minA minC _ _ a) ?minxx. Qed. - -End bigmin_Type. - -Section bigmin_finType. -Variable (I : finType) (x : T). -Implicit Types (P : pred I) (F : I -> T). - -Lemma bigminD1 j P F : P j -> - \big[min/x]_(i | P i) F i = min (F j) (\big[min/x]_(i | P i && (i != j)) F i). -Proof. by move/(bigD1_AC minA minC _ _) ->. Qed. - -Lemma bigmin_le_cond j P F : P j -> \big[min/x]_(i | P i) F i <= F j. -Proof. -have := mem_index_enum j; rewrite unlock; elim: (index_enum I) => //= i l ih. -rewrite inE => /orP [/eqP-> ->|/ih leminlfi Pi]; first by rewrite le_minl lexx. -by case: ifPn => Pj; [rewrite le_minl leminlfi// orbC|exact: leminlfi]. -Qed. - -Lemma bigmin_le j F : \big[min/x]_i F i <= F j. -Proof. exact: bigmin_le_cond. Qed. - -Lemma bigmin_inf j P m F : P j -> F j <= m -> \big[min/x]_(i | P i) F i <= m. -Proof. by move=> Pj ?; apply: le_trans (bigmin_le_cond _ Pj) _. Qed. - -Lemma bigmin_geP m P F : reflect (m <= x /\ forall i, P i -> m <= F i) - (m <= \big[min/x]_(i | P i) F i). -Proof. -apply: (iffP idP) => [lemFi|[lemx lemPi]]; [split|exact: le_bigmin]. -- by rewrite (le_trans lemFi)// bigmin_idl le_minl lexx. -- by move=> i Pi; rewrite (le_trans lemFi)// (bigminD1 _ Pi)// le_minl lexx. -Qed. - -Lemma bigmin_gtP m P F : - reflect (m < x /\ forall i, P i -> m < F i) (m < \big[min/x]_(i | P i) F i). -Proof. -apply: (iffP idP) => [lemFi|[lemx lemPi]]; [split|exact: lt_bigmin]. -- by rewrite (lt_le_trans lemFi)// bigmin_idl le_minl lexx. -- by move=> i Pi; rewrite (lt_le_trans lemFi)// (bigminD1 _ Pi)// le_minl lexx. -Qed. - -Lemma bigmin_eq_arg j P F : P j -> (forall i, P i -> F i <= x) -> - \big[min/x]_(i | P i) F i = F [arg min_(i < j | P i) F i]. -Proof. -move=> Pi0; case: arg_minP => //= i Pi PF PFx. -apply/eqP; rewrite eq_le bigmin_le_cond //=. -by apply/bigmin_geP; split => //; exact: PFx. -Qed. - -Lemma eq_bigmin j P F : P j -> (forall i, P i -> F i <= x) -> - {i0 | i0 \in I & \big[min/x]_(i | P i) F i = F i0}. -Proof. by move=> Pi0 Hx; rewrite (bigmin_eq_arg Pi0) //; eexists. Qed. - -End bigmin_finType. - -End bigmin. -Arguments bigmin_mkcond {d T I r}. -Arguments bigminID {d T I r}. -Arguments bigminD1 {d T I x} j. -Arguments bigmin_inf {d T I x} j. -Arguments bigmin_eq_arg {d T I} x j. -Arguments eq_bigmin {d T I x} j. - -Reserved Notation "`1- r" (format "`1- r", at level 2). - -Section onem. -Variable R : numDomainType. -Implicit Types r : R. - -Definition onem r := 1 - r. -Local Notation "`1- r" := (onem r). - -Lemma onem0 : `1-0 = 1. Proof. by rewrite /onem subr0. Qed. - -Lemma onem1 : `1-1 = 0. Proof. by rewrite /onem subrr. Qed. - -Lemma onemK r : `1-(`1-r) = r. -Proof. by rewrite /onem opprB addrCA subrr addr0. Qed. - -Lemma onem_gt0 r : r < 1 -> 0 < `1-r. Proof. by rewrite subr_gt0. Qed. - -Lemma onem_ge0 r : r <= 1 -> 0 <= `1-r. -Proof. by rewrite le_eqVlt => /predU1P[->|/onem_gt0/ltW]; rewrite ?onem1. Qed. - -Lemma onem_le1 r : 0 <= r -> `1-r <= 1. -Proof. by rewrite ler_subl_addr ler_addl. Qed. - -Lemma onem_lt1 r : 0 < r -> `1-r < 1. -Proof. by rewrite ltr_subl_addr ltr_addl. Qed. - -Lemma onemX_ge0 r n : 0 <= r -> r <= 1 -> 0 <= `1-(r ^+ n). -Proof. by move=> ? ?; rewrite subr_ge0 exprn_ile1. Qed. - -Lemma onemX_lt1 r n : 0 < r -> `1-(r ^+ n) < 1. -Proof. by move=> ?; rewrite onem_lt1// exprn_gt0. Qed. - -Lemma onemD r s : `1-(r + s) = `1-r - s. -Proof. by rewrite /onem addrAC opprD addrA addrAC. Qed. - -Lemma onemMr r s : s * `1-r = s - s * r. -Proof. by rewrite /onem mulrBr mulr1. Qed. - -Lemma onemM r s : `1-(r * s) = `1-r + `1-s - `1-r * `1-s. -Proof. -rewrite /onem mulrBr mulr1 mulrBl mul1r opprB -addrA. -by rewrite (addrC (1 - r)) !addrA subrK opprB addrA subrK addrK. -Qed. - -Lemma onem_lt : {mono onem : x y /~ x <= y}. -Proof. -by move=> x y; rewrite ler_subl_addl addrA ler_subr_addr addrC ler_add2r. -Qed. - -End onem. -Notation "`1- r" := (onem r) : ring_scope. - -Lemma lez_abs2 (a b : int) : 0 <= a -> a <= b -> (`|a| <= `|b|)%N. -Proof. by case: a => //= n _; case: b. Qed. \ No newline at end of file From d3a4cc1a97f7c77ace3e7f6f90f2788a716f3f8f Mon Sep 17 00:00:00 2001 From: zstone Date: Thu, 20 Oct 2022 16:16:12 -0400 Subject: [PATCH 3/3] adding homotopy to coq project --- _CoqProject | 1 + 1 file changed, 1 insertion(+) diff --git a/_CoqProject b/_CoqProject index 1a9dd0cdc..c93621709 100644 --- a/_CoqProject +++ b/_CoqProject @@ -38,6 +38,7 @@ theories/numfun.v theories/lebesgue_integral.v theories/summability.v theories/signed.v +theories/homotopy.v theories/altreals/xfinmap.v theories/altreals/discrete.v theories/altreals/realseq.v