From 9ef13c280b4ac892dd1276a511efa9611ccb2efa Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Mon, 29 Jul 2024 17:01:06 +0900 Subject: [PATCH] addressing comments --- CHANGELOG_UNRELEASED.md | 11 +++--- classical/classical_sets.v | 79 +++++++++++++++++++++++--------------- theories/measure.v | 24 ++++++------ theories/normedtype.v | 2 +- 4 files changed, 65 insertions(+), 51 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index de68f052a..c28821c11 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -13,13 +13,12 @@ + factory `isAlgebraOfSets_setD` - in `classical_sets.v`: - + definition `sym_diff`, notation ``` `^` ``` - + lemmas `sym_diffxx`, `sym_diff_setU`, `sym_diff_set`, `sym_diff_setI`, - `sym_diffC`, `sym_diffA`, `sym_diff0`, `sym_diffE`, `sym_diffT`, `sym_diffv`, - `sym_diff_def` - + + definition `setX`, notation ``` `^` ``` + + lemmas `setX0`, `set0X`, `setXK`, `setXC`, `setXA`, `setIXl`, `mulrXr`, + `setX_def`, `setXE`, `setXU`, `setXI`, `setXD`, `setXCT`, `setCXT`, `setXTC`, `setTXC` + - in `measure.v`: - + factory `isRingOfSets_sym_diff` + + factory `isRingOfSets_setX` - in `classical_sets.v`: + lemma `setDU` diff --git a/classical/classical_sets.v b/classical/classical_sets.v index ea03a4f09..8a39953d5 100644 --- a/classical/classical_sets.v +++ b/classical/classical_sets.v @@ -402,9 +402,9 @@ Notation "A `\` B" := (setD A B) : classical_set_scope. Notation "A `\ a" := (A `\` [set a]) : classical_set_scope. Notation "[ 'disjoint' A & B ]" := (disj_set A B) : classical_set_scope. -Definition sym_diff {T : Type} (A B : set T) := (A `\` B) `|` (B `\` A). -Arguments sym_diff _ _ _ _ /. -Notation "A `^` B" := (sym_diff A B) : classical_set_scope. +Definition setX {T : Type} (A B : set T) := (A `\` B) `|` (B `\` A). +Arguments setX _ _ _ _ /. +Notation "A `^` B" := (setX A B) : classical_set_scope. Notation "'`I_' n" := [set k | is_true (k < n)%N]. @@ -1123,59 +1123,71 @@ Lemma bigcupM1r T1 T2 (A1 : T2 -> set T1) (A2 : set T2) : \bigcup_(i in A2) (A1 i `*` [set i]) = A1 ``*` A2. Proof. by apply/predeqP => -[i j]; split=> [[? ? [? /= -> //]]|[]]; exists j. Qed. -Lemma sym_diffxx A : A `^` A = set0. -Proof. by rewrite /sym_diff setDv setU0. Qed. +Lemma setX0 : right_id set0 (@setX T). +Proof. by move=> A; rewrite /setX setD0 set0D setU0. Qed. -Lemma sym_diff0 A : A `^` set0 = A. -Proof. by rewrite /sym_diff setD0 set0D setU0. Qed. +Lemma set0X : left_id set0 (@setX T). +Proof. by move=> A; rewrite /setX set0D setD0 set0U. Qed. -Lemma sym_diffT A : A `^` [set: T] = ~` A. -Proof. by rewrite /sym_diff setDT set0U setTD. Qed. +Lemma setXK A : A `^` A = set0. +Proof. by rewrite /setX setDv setU0. Qed. -Lemma sym_diffv A : A `^` ~` A = [set: T]. -Proof. by rewrite /sym_diff setDE setCK setIid setDE setIid setUv. Qed. +Lemma setXC : commutative (@setX T). +Proof. by move=> A B; rewrite /setX setUC. Qed. -Lemma sym_diffC A B : A `^` B = B `^` A. -Proof. by rewrite /sym_diff setUC. Qed. +Lemma setXTC A : A `^` [set: T] = ~` A. +Proof. by rewrite /setX setDT set0U setTD. Qed. -Lemma sym_diffA A B C : A `^` (B `^` C) = (A `^` B) `^` C. +Lemma setTXC A : [set: T] `^` A = ~` A. +Proof. by rewrite setXC setXTC. Qed. + +Lemma setXA : associative (@setX T). Proof. -rewrite /sym_diff; apply/seteqP; split => x/=; +move=> A B C; rewrite /setX; apply/seteqP; split => x/=; by have [|] := pselect (A x); have [|] := pselect (B x); have [|] := pselect (C x); tauto. Qed. -Lemma sym_diff_def A B : A `^` B = (A `&` ~` B) `|` (~` A `&` B). -Proof. by rewrite /sym_diff !setDE (setIC B). Qed. - -Lemma sym_diffE A B : A `^` B = (A `|` B) `\` (A `&` B). +Lemma setIXl : left_distributive (@setI T) (@setX T). Proof. -rewrite /sym_diff; apply/seteqP; split => x/=; -by have [|] := pselect (A x); have [|] := pselect (B x); tauto. +move=> A B C; rewrite /setX; apply/seteqP; split => x/=; +by have [|] := pselect (A x); have [|] := pselect (B x); + have [|] := pselect (C x); tauto. Qed. -Lemma sym_diff_setU A B : (A `^` B) `^` (A `&` B) = A `|` B. +Lemma setIXr : right_distributive (@setI T) (@setX T). +Proof. by move=> A B C; rewrite setIC setIXl -2!(setIC A). Qed. + +Lemma setX_def A B : A `^` B = (A `\` B) `|` (B `\` A). +Proof. by []. Qed. + +Lemma setXE A B : A `^` B = (A `|` B) `\` (A `&` B). Proof. -rewrite /sym_diff; apply/seteqP; split => x/=; +rewrite /setX; apply/seteqP; split => x/=; by have [|] := pselect (A x); have [|] := pselect (B x); tauto. Qed. -Lemma sym_diff_setD A B : A `^` (A `&` B) = A `\` B. -Proof. by rewrite /sym_diff; apply/seteqP; split => x/=; tauto. Qed. - -Lemma sym_diff_setI A B : (A `|` B) `\` (A `^` B) = A `&` B. +Lemma setXU A B : (A `^` B) `^` (A `&` B) = A `|` B. Proof. -rewrite /sym_diff; apply/seteqP; split => x/=; +rewrite /setX; apply/seteqP; split => x/=; by have [|] := pselect (A x); have [|] := pselect (B x); tauto. Qed. -Lemma setI_sym_diff A B C : A `&` (B `^` C) = (A `&` B) `^` (A `&` C). +Lemma setXI A B : (A `|` B) `\` (A `^` B) = A `&` B. Proof. -rewrite /sym_diff; apply/seteqP; split => x/=; -by have [|] := pselect (A x); have [|] := pselect (B x); - have [|] := pselect (C x); tauto. +rewrite /setX; apply/seteqP; split => x/=; +by have [|] := pselect (A x); have [|] := pselect (B x); tauto. Qed. +Lemma setXD A B : A `^` (A `&` B) = A `\` B. +Proof. by rewrite /setX; apply/seteqP; split => x/=; tauto. Qed. + +Lemma setXCT A : A `^` ~` A = [set: T]. +Proof. by rewrite /setX setDE setCK setIid setDE setIid setUv. Qed. + +Lemma setCXT A : ~` A `^` A = [set: T]. +Proof. by rewrite setXC setXCT. Qed. + End basic_lemmas. #[global] Hint Resolve subsetUl subsetUr subIsetl subIsetr subDsetl subDsetr : core. @@ -1371,6 +1383,9 @@ HB.instance Definition _ := isMulLaw.Build (set T) set0 setI set0I setI0. HB.instance Definition _ := isAddLaw.Build (set T) setU setI setUIl setUIr. HB.instance Definition _ := isAddLaw.Build (set T) setI setU setIUl setIUr. +HB.instance Definition _ := isComLaw.Build (set T) set0 setX setXA setXC set0X. +HB.instance Definition _ := isAddLaw.Build (set T) setI setX setIXl setIXr. + End SetMonoids. Section base_image_lemmas. diff --git a/theories/measure.v b/theories/measure.v index 3adaa2457..b558468c3 100644 --- a/theories/measure.v +++ b/theories/measure.v @@ -189,7 +189,8 @@ From HB Require Import structures. (* setSD_closed G == the set of sets G is closed under proper *) (* difference *) (* setDI_closed G == the set of sets G is closed under difference *) -(* sym_diff_closed G == the set of sets G is closed by symmetric difference *) +(* setX_closed G == the set of sets G is closed under symmetric *) +(* difference *) (* ndseq_closed G == the set of sets G is closed under non-decreasing *) (* countable union *) (* niseq_closed G == the set of sets G is closed under non-increasing *) @@ -355,7 +356,7 @@ Definition setI_closed := forall A B, G A -> G B -> G (A `&` B). Definition setU_closed := forall A B, G A -> G B -> G (A `|` B). Definition setSD_closed := forall A B, B `<=` A -> G A -> G B -> G (A `\` B). Definition setDI_closed := forall A B, G A -> G B -> G (A `\` B). -Definition sym_diff_closed := forall A B, G A -> G B -> G (A `^` B). +Definition setX_closed := forall A B, G A -> G B -> G (A `^` B). Definition fin_bigcap_closed := forall I (D : set I) A_, finite_set D -> (forall i, D i -> G (A_ i)) -> @@ -1166,33 +1167,32 @@ HB.instance Definition _ := SemiRingOfSets_isRingOfSets.Build d T measurableU. HB.end. -HB.factory Record isRingOfSets_sym_diff (d : measure_display) T +HB.factory Record isRingOfSets_setX (d : measure_display) T of Pointed T := { measurable : set (set T) ; measurable_nonempty : measurable !=set0 ; - measurable_sym_diff : sym_diff_closed measurable ; + measurable_setX : setX_closed measurable ; measurable_setI : setI_closed measurable }. -HB.builders Context d T of isRingOfSets_sym_diff d T. +HB.builders Context d T of isRingOfSets_setX d T. Let m0 : measurable set0. Proof. have [A mA] := measurable_nonempty. -have := measurable_sym_diff mA mA. -by rewrite sym_diffxx. +have := measurable_setX mA mA. +by rewrite setXK. Qed. Let mU : setU_closed measurable. Proof. -move=> A B mA mB; rewrite -sym_diff_setU. -apply: measurable_sym_diff; first exact: measurable_sym_diff. -exact: measurable_setI. +move=> A B mA mB; rewrite -setXU. +by apply: measurable_setX; [exact: measurable_setX|exact: measurable_setI]. Qed. Let mD : setDI_closed measurable. Proof. -move=> A B mA mB; rewrite -sym_diff_setD. -by apply: measurable_sym_diff => //; exact: measurable_setI. +move=> A B mA mB; rewrite -setXD. +by apply: measurable_setX => //; exact: measurable_setI. Qed. HB.instance Definition _ := isRingOfSets.Build d T m0 mU mD. diff --git a/theories/normedtype.v b/theories/normedtype.v index 721569595..41f16dd13 100644 --- a/theories/normedtype.v +++ b/theories/normedtype.v @@ -692,7 +692,7 @@ Proof. by rewrite cvgeNyPltr. Qed. Lemma cvgNey f : (\- f @ F --> +oo) <-> (f @ F --> -oo). Proof. rewrite cvgeNyPler cvgeyPger; split=> Foo A Areal; -by near do rewrite -lee_opp2 ?oppeK; apply: Foo; rewrite rpredN. +by near do rewrite -leeN2 ?oppeK; apply: Foo; rewrite rpredN. Unshelve. all: end_near. Qed. Lemma cvgNeNy f : (\- f @ F --> -oo) <-> (f @ F --> +oo).