diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 5c7f246c14..d4475de911 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -24,6 +24,29 @@ + `ErealGenCInfty.measurable_set1_ninfty` -> `ErealGenCInfty.measurable_set1Ny` + `ErealGenCInfty.measurable_set1_pinfty` -> `ErealGenCInfty.measurable_set1y` +- in `set_interval.v`: + + `conv` -> `line_path` + + `conv_id` -> `line_path_id` + + `ndconv` -> `ndline_path` + + `convEl` -> `line_pathEl` + + `convEr` -> `line_pathEr` + + `conv10` -> `line_path10` + + `conv0` -> `line_path0` + + `conv1` -> `line_path1` + + `conv_sym` -> `line_path_sym` + + `conv_flat` -> `line_path_flat` + + `leW_conv` -> `leW_line_path` + + `ndconvE` -> `ndline_pathE` + + `convK` -> `line_pathK` + + `conv_inj` -> `line_path_inj` + + `conv_bij` -> `line_path_bij` + + `le_conv` -> `le_line_path` + + `lt_conv` -> `lt_line_path` + + `conv_itv_bij` -> `line_path_itv_bij` + + `mem_conv_itv` -> `mem_line_path_itv` + + `mem_conv_itvcc` -> `mem_line_path_itvcc` + + `range_conv` -> `range_line_path` + ### Generalized ### Deprecated diff --git a/classical/set_interval.v b/classical/set_interval.v index bf7c11c0b9..d24f79d70c 100644 --- a/classical/set_interval.v +++ b/classical/set_interval.v @@ -10,7 +10,9 @@ From HB Require Import structures. (* when the support type is a numFieldType, this *) (* is equivalent to (i.1 < i.2)%O (lemma neitvE) *) (* set_itv_infty_set0 == multirule to simplify empty intervals *) -(* conv, ndconv == convexity operator *) +(* line_path a b t := (1 - t) * a + t * b, convexity operator over a *) +(* numDomainType *) +(* ndline_path == line_path a b with the constraint that a < b *) (* factor a b x := (x - a) / (b - a) *) (* set_itvE == multirule to turn intervals into inequalities *) (* disjoint_itv i j == intervals i and j are disjoint *) @@ -330,44 +332,46 @@ Proof. by rewrite set_itv_splitI/= setDE setCitvr. Qed. End set_itv_porderType. -Section conv_factor_numDomainType. +Section line_path_factor_numDomainType. Variable R : numDomainType. Implicit Types (a b t r : R) (A : set R). Lemma mem_1B_itvcc t : (1 - t \in `[0, 1]) = (t \in `[0, 1]). Proof. by rewrite !in_itv/= subr_ge0 ger_addl oppr_le0 andbC. Qed. -Definition conv a b t : R := (1 - t) * a + t * b. +Definition line_path a b t : R := (1 - t) * a + t * b. -Lemma conv_id : conv 0 1 = id. -Proof. by apply/funext => t; rewrite /conv mulr0 add0r mulr1. Qed. +Lemma line_path_id : line_path 0 1 = id. +Proof. by apply/funext => t; rewrite /line_path mulr0 add0r mulr1. Qed. -Lemma convEl a b t : conv a b t = t * (b - a) + a. -Proof. by rewrite /conv mulrBl mul1r mulrBr addrAC [RHS]addrC addrA. Qed. +Lemma line_pathEl a b t : line_path a b t = t * (b - a) + a. +Proof. by rewrite /line_path mulrBl mul1r mulrBr addrAC [RHS]addrC addrA. Qed. -Lemma convEr a b t : conv a b t = (1 - t) * (a - b) + b. +Lemma line_pathEr a b t : line_path a b t = (1 - t) * (a - b) + b. Proof. -rewrite /conv mulrBr -addrA; congr (_ + _). +rewrite /line_path mulrBr -addrA; congr (_ + _). by rewrite mulrBl opprB mul1r addrNK. Qed. -Lemma conv10 t : conv 1 0 t = 1 - t. -Proof. by rewrite /conv mulr0 addr0 mulr1. Qed. +Lemma line_path10 t : line_path 1 0 t = 1 - t. +Proof. by rewrite /line_path mulr0 addr0 mulr1. Qed. -Lemma conv0 a b : conv a b 0 = a. -Proof. by rewrite /conv subr0 mul1r mul0r addr0. Qed. +Lemma line_path0 a b : line_path a b 0 = a. +Proof. by rewrite /line_path subr0 mul1r mul0r addr0. Qed. -Lemma conv1 a b : conv a b 1 = b. -Proof. by rewrite /conv subrr mul0r add0r mul1r. Qed. +Lemma line_path1 a b : line_path a b 1 = b. +Proof. by rewrite /line_path subrr mul0r add0r mul1r. Qed. -Lemma conv_sym a b t : conv a b t = conv b a (1 - t). -Proof. by rewrite /conv opprB addrCA subrr addr0 addrC. Qed. +Lemma line_path_sym a b t : line_path a b t = line_path b a (1 - t). +Proof. by rewrite /line_path opprB addrCA subrr addr0 addrC. Qed. -Lemma conv_flat a : conv a a = cst a. -Proof. by apply/funext => t; rewrite convEl subrr mulr0 add0r. Qed. +Lemma line_path_flat a : line_path a a = cst a. +Proof. by apply/funext => t; rewrite line_pathEl subrr mulr0 add0r. Qed. -Lemma leW_conv a b : a <= b -> {homo conv a b : x y / x <= y}. -Proof. by move=> ? ? ? ?; rewrite !convEl ler_add ?ler_wpmul2r// subr_ge0. Qed. +Lemma leW_line_path a b : a <= b -> {homo line_path a b : x y / x <= y}. +Proof. +by move=> ? ? ? ?; rewrite !line_pathEl ler_add ?ler_wpmul2r// subr_ge0. +Qed. Definition factor a b x := (x - a) / (b - a). @@ -382,51 +386,56 @@ Proof. by apply/funext => x; rewrite /factor subrr invr0 mulr0. Qed. Lemma factorl a b : factor a b a = 0. Proof. by rewrite /factor subrr mul0r. Qed. -Definition ndconv a b of a < b := conv a b. +Definition ndline_path a b of a < b := line_path a b. -Lemma ndconvE a b (ab : a < b) : ndconv ab = conv a b. Proof. by []. Qed. +Lemma ndline_pathE a b (ab : a < b) : ndline_path ab = line_path a b. +Proof. by []. Qed. -End conv_factor_numDomainType. +End line_path_factor_numDomainType. -Section conv_factor_numFieldType. +Section line_path_factor_numFieldType. Variable R : numFieldType. Implicit Types (a b t r : R) (A : set R). Lemma factorr a b : a != b -> factor a b b = 1. Proof. by move=> Nab; rewrite /factor divff// subr_eq0 eq_sym. Qed. -Lemma factorK a b : a != b -> cancel (factor a b) (conv a b). -Proof. by move=> ? x; rewrite convEl mulfVK ?addrNK// subr_eq0 eq_sym. Qed. +Lemma factorK a b : a != b -> cancel (factor a b) (line_path a b). +Proof. by move=> ? x; rewrite line_pathEl mulfVK ?addrNK// subr_eq0 eq_sym. Qed. -Lemma convK a b : a != b -> cancel (conv a b) (factor a b). -Proof. by move=> ? x; rewrite /factor convEl addrK mulfK// subr_eq0 eq_sym. Qed. +Lemma line_pathK a b : a != b -> cancel (line_path a b) (factor a b). +Proof. +by move=> ? x; rewrite /factor line_pathEl addrK mulfK// subr_eq0 eq_sym. +Qed. -Lemma conv_inj a b : a != b -> injective (conv a b). -Proof. by move/convK/can_inj. Qed. +Lemma line_path_inj a b : a != b -> injective (line_path a b). +Proof. by move/line_pathK/can_inj. Qed. Lemma factor_inj a b : a != b -> injective (factor a b). Proof. by move/factorK/can_inj. Qed. -Lemma conv_bij a b : a != b -> bijective (conv a b). -Proof. by move=> ab; apply: Bijective (convK ab) (factorK ab). Qed. +Lemma line_path_bij a b : a != b -> bijective (line_path a b). +Proof. by move=> ab; apply: Bijective (line_pathK ab) (factorK ab). Qed. Lemma factor_bij a b : a != b -> bijective (factor a b). -Proof. by move=> ab; apply: Bijective (factorK ab) (convK ab). Qed. +Proof. by move=> ab; apply: Bijective (factorK ab) (line_pathK ab). Qed. -Lemma le_conv a b : a < b -> {mono conv a b : x y / x <= y}. +Lemma le_line_path a b : a < b -> {mono line_path a b : x y / x <= y}. Proof. move=> ltab; have leab := ltW ltab. -by apply: homo_mono (convK _) (leW_factor _) (leW_conv _); rewrite // lt_eqF. +apply: homo_mono (line_pathK _) (leW_factor _) (leW_line_path _) => //. +by rewrite lt_eqF. Qed. Lemma le_factor a b : a < b -> {mono factor a b : x y / x <= y}. Proof. move=> ltab; have leab := ltW ltab. -by apply: homo_mono (factorK _) (leW_conv _) (leW_factor _); rewrite // lt_eqF. +apply: homo_mono (factorK _) (leW_line_path _) (leW_factor _) => //. +by rewrite lt_eqF. Qed. -Lemma lt_conv a b : a < b -> {mono conv a b : x y / x < y}. -Proof. by move/le_conv/leW_mono. Qed. +Lemma lt_line_path a b : a < b -> {mono line_path a b : x y / x < y}. +Proof. by move/le_line_path/leW_mono. Qed. Lemma lt_factor a b : a < b -> {mono factor a b : x y / x < y}. Proof. by move/le_factor/leW_mono. Qed. @@ -434,16 +443,17 @@ Proof. by move/le_factor/leW_mono. Qed. Let ltNeq a b : a < b -> a != b. Proof. by move=> /lt_eqF->. Qed. HB.instance Definition _ a b (ab : a < b) := - @Can2.Build _ _ setT setT (ndconv ab) (factor a b) + @Can2.Build _ _ setT setT (ndline_path ab) (factor a b) (fun _ _ => I) (fun _ _ => I) - (in1W (convK (ltNeq ab))) (in1W (factorK (ltNeq ab))). + (in1W (line_pathK (ltNeq ab))) (in1W (factorK (ltNeq ab))). -Lemma conv_itv_bij ba bb a b : a < b -> +Lemma line_path_itv_bij ba bb a b : a < b -> set_bij [set` Interval (BSide ba 0) (BSide bb 1)] - [set` Interval (BSide ba a) (BSide bb b)] (conv a b). + [set` Interval (BSide ba a) (BSide bb b)] (line_path a b). Proof. -move=> ltab; rewrite -ndconvE; apply: bij_subr => //=; rewrite setTI ?ndconvE. -apply/predeqP => t /=; rewrite !in_itv/= {1}convEl convEr. +move=> ltab; rewrite -ndline_pathE. +apply: bij_subr => //=; rewrite setTI ?ndline_pathE. +apply/predeqP => t /=; rewrite !in_itv/= {1}line_pathEl line_pathEr. rewrite -lteif_subl_addr subrr -lteif_pdivr_mulr ?subr_gt0// mul0r. rewrite -lteif_subr_addr subrr -lteif_ndivr_mulr ?subr_lt0// mul0r. by rewrite lteif_subr_addl addr0. @@ -453,32 +463,32 @@ Lemma factor_itv_bij ba bb a b : a < b -> set_bij [set` Interval (BSide ba a) (BSide bb b)] [set` Interval (BSide ba 0) (BSide bb 1)] (factor a b). Proof. -move=> ltab; have -> : factor a b = (ndconv ltab)^-1%FUN by []. -by apply/splitbij_sub_sym => //; apply: conv_itv_bij. +move=> ltab; have -> : factor a b = (ndline_path ltab)^-1%FUN by []. +by apply/splitbij_sub_sym => //; apply: line_path_itv_bij. Qed. -Lemma mem_conv_itv ba bb a b : a < b -> +Lemma mem_line_path_itv ba bb a b : a < b -> set_fun [set` Interval (BSide ba 0) (BSide bb 1)] - [set` Interval (BSide ba a) (BSide bb b)] (conv a b). -Proof. by case/(conv_itv_bij ba bb). Qed. + [set` Interval (BSide ba a) (BSide bb b)] (line_path a b). +Proof. by case/(line_path_itv_bij ba bb). Qed. -Lemma mem_conv_itvcc a b : a <= b -> set_fun `[0, 1] `[a, b] (conv a b). +Lemma mem_line_path_itvcc a b : a <= b -> set_fun `[0, 1] `[a, b] (line_path a b). Proof. -rewrite le_eqVlt => /predU1P[<-|]; first by rewrite set_itv1 conv_flat. -by move=> lt_ab; case: (conv_itv_bij true false lt_ab). +rewrite le_eqVlt => /predU1P[<-|]; first by rewrite set_itv1 line_path_flat. +by move=> lt_ab; case: (line_path_itv_bij true false lt_ab). Qed. -Lemma range_conv ba bb a b : a < b -> - conv a b @` [set` Interval (BSide ba 0) (BSide bb 1)] = +Lemma range_line_path ba bb a b : a < b -> + line_path a b @` [set` Interval (BSide ba 0) (BSide bb 1)] = [set` Interval (BSide ba a) (BSide bb b)]. -Proof. by move=> /(conv_itv_bij ba bb)/Pbij[f ->]; rewrite image_eq. Qed. +Proof. by move=> /(line_path_itv_bij ba bb)/Pbij[f ->]; rewrite image_eq. Qed. Lemma range_factor ba bb a b : a < b -> factor a b @` [set` Interval (BSide ba a) (BSide bb b)] = [set` Interval (BSide ba 0) (BSide bb 1)]. Proof. by move=> /(factor_itv_bij ba bb)/Pbij[f ->]; rewrite image_eq. Qed. -End conv_factor_numFieldType. +End line_path_factor_numFieldType. Lemma mem_factor_itv (R : realFieldType) ba bb (a b : R) : set_fun [set` Interval (BSide ba a) (BSide bb b)]