addressing comments

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`

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.

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.

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).