new factory for algebra of sets (#1251)

* new factory for algebra of sets -- Co-authored-by: @JeremyDubut Co-authored-by: @AkihisaYamada Co-authored-by: Takafumi Saikawa <[email protected]>
math-comp · Jul 31, 2024 · d5b959a · d5b959a
1 parent 0a9b2aa
commit d5b959a
Show file tree

Hide file tree

Showing 4 changed files with 157 additions and 2 deletions.
diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
@@ -6,6 +6,19 @@
 
 - in `topology.v`:
   + lemma `ball_subspace_ball`
+- in `classical_sets.v`:
+  + lemma `setCD`
+
+- in `measure.v`:
+  + factory `isAlgebraOfSets_setD`
+
+- in `classical_sets.v`:
+  + 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_setX`
 
 - in `classical_sets.v`:
   + lemma `setDU`

diff --git a/classical/classical_sets.v b/classical/classical_sets.v
@@ -42,6 +42,7 @@ From mathcomp Require Import mathcomp_extra boolp.
 (* |                   `` `\|` `` |==| $\cup$                                 *)
 (* |                    `` `&` `` |==| $\cap$                                 *)
 (* |                    `` `\` `` |==| set difference                         *)
+(* |                    `` `^` `` |==| symmetric difference                   *)
 (* |                     `` ~` `` |==| set complement                         *)
 (* |                   `` `<=` `` |==| $\subseteq$                            *)
 (* |                 `` f @` A `` |==| image by f of A                        *)
@@ -244,6 +245,7 @@ Reserved Notation "~` A" (at level 35, right associativity).
 Reserved Notation "[ 'set' ~ a ]" (at level 0, format "[ 'set' ~  a ]").
 Reserved Notation "A `\` B" (at level 50, left associativity).
 Reserved Notation "A `\ b" (at level 50, left associativity).
+Reserved Notation "A `^` B" (at level 52, left associativity).
 (*
 Reserved Notation "A `+` B"  (at level 54, left associativity).
 Reserved Notation "A +` B"  (at level 54, left associativity).
@@ -400,6 +402,10 @@ 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 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].
 
 Notation "\bigcup_ ( i 'in' P ) F" :=
@@ -995,6 +1001,9 @@ Qed.
 Lemma setCI A B : ~` (A `&` B) = ~` A `|` ~` B.
 Proof. by rewrite -[in LHS](setCK A) -[in LHS](setCK B) -setCU setCK. Qed.
 
+Lemma setCD A B : ~` (A `\` B) = ~` A `|` B.
+Proof. by rewrite setDE setCI setCK. Qed.
+
 Lemma setDUr A B C : A `\` (B `|` C) = (A `\` B) `&` (A `\` C).
 Proof. by rewrite !setDE setCU setIIr. Qed.
 
@@ -1114,6 +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 setX0 : right_id set0 (@setX T).
+Proof. by move=> A; rewrite /setX setD0 set0D setU0. Qed.
+
+Lemma set0X : left_id set0 (@setX T).
+Proof. by move=> A; rewrite /setX set0D setD0 set0U. Qed.
+
+Lemma setXK A : A `^` A = set0.
+Proof. by rewrite /setX setDv setU0. Qed.
+
+Lemma setXC : commutative (@setX T).
+Proof. by move=> A B; rewrite /setX setUC. Qed.
+
+Lemma setXTC A : A `^` [set: T] = ~` A.
+Proof. by rewrite /setX setDT set0U setTD. Qed.
+
+Lemma setTXC A : [set: T] `^` A = ~` A.
+Proof. by rewrite setXC setXTC. Qed.
+
+Lemma setXA : associative (@setX T).
+Proof.
+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 setIXl : left_distributive (@setI T) (@setX T).
+Proof.
+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 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 /setX; apply/seteqP; split => x/=;
+by have [|] := pselect (A x); have [|] := pselect (B x); tauto.
+Qed.
+
+Lemma setXU A B : (A `^` B) `^` (A `&` B) = A `|` B.
+Proof.
+rewrite /setX; apply/seteqP; split => x/=;
+by have [|] := pselect (A x); have [|] := pselect (B x); tauto.
+Qed.
+
+Lemma setXI A B : (A `|` B) `\` (A `^` B) = A `&` B.
+Proof.
+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.
@@ -1314,6 +1388,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
@@ -191,6 +191,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         *)
+(*      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     *)
@@ -356,6 +358,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 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,6 +1169,38 @@ HB.instance Definition _ := SemiRingOfSets_isRingOfSets.Build d T measurableU.
 
 HB.end.
 
+HB.factory Record isRingOfSets_setX (d : measure_display) T
+    of Pointed T := {
+  measurable : set (set T) ;
+  measurable_nonempty : measurable !=set0 ;
+  measurable_setX : setX_closed measurable ;
+  measurable_setI : setI_closed measurable }.
+
+HB.builders Context d T of isRingOfSets_setX d T.
+
+Let m0 : measurable set0.
+Proof.
+have [A mA] := measurable_nonempty.
+have := measurable_setX mA mA.
+by rewrite setXK.
+Qed.
+
+Let mU : setU_closed measurable.
+Proof.
+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 -setXD.
+by apply: measurable_setX => //; exact: measurable_setI.
+Qed.
+
+HB.instance Definition _ := isRingOfSets.Build d T m0 mU mD.
+
+HB.end.
+
 HB.factory Record isAlgebraOfSets (d : measure_display) T of Pointed T := {
   measurable : set (set T) ;
   measurable0 : measurable set0 ;
@@ -1191,6 +1226,30 @@ HB.instance Definition _ := RingOfSets_isAlgebraOfSets.Build d T measurableT.
 
 HB.end.
 
+HB.factory Record isAlgebraOfSets_setD (d : measure_display) T of Pointed T := {
+  measurable : set (set T) ;
+  measurableT : measurable [set: T] ;
+  measurableD : setDI_closed measurable
+}.
+
+HB.builders Context d T of isAlgebraOfSets_setD d T.
+
+Let m0 : measurable set0.
+Proof. by rewrite -(setDT setT); apply: measurableD; exact: measurableT. Qed.
+
+Let mU : setU_closed measurable.
+Proof.
+move=> A B mA mB.
+rewrite -(setCK A) -setCD -!setTD; apply: measurableD; first exact: measurableT.
+by do 2 apply: measurableD => //; exact: measurableT.
+Qed.
+
+HB.instance Definition _ := isRingOfSets.Build d T m0 mU measurableD.
+
+HB.instance Definition _ := RingOfSets_isAlgebraOfSets.Build d T measurableT.
+
+HB.end.
+
 HB.factory Record isMeasurable (d : measure_display) T of Pointed T := {
   measurable : set (set T) ;
   measurable0 : measurable set0 ;

diff --git a/theories/topology.v b/theories/topology.v
@@ -4772,7 +4772,8 @@ HB.instance Definition _ := Uniform_isPseudoMetric.Build R M
 
 HB.end.
 
-Lemma entourage_ballE {R : numDomainType} {M : pseudoMetricType R} : entourage_ (@ball R M) = entourage.
+Lemma entourage_ballE {R : numDomainType} {M : pseudoMetricType R} :
+  entourage_ (@ball R M) = entourage.
 Proof. by rewrite entourageE_subproof. Qed.
 
 Lemma entourage_from_ballE {R : numDomainType} {M : pseudoMetricType R} :
@@ -4791,7 +4792,8 @@ Definition nbhs_ball_ {R : numDomainType} {T T'} (ball : T -> R -> set T')
 Definition nbhs_ball {R : numDomainType} {M : pseudoMetricType R} :=
   nbhs_ball_ (@ball R M).
 
-Lemma nbhs_ballE {R : numDomainType} {M : pseudoMetricType R} : (@nbhs_ball R M) = nbhs.
+Lemma nbhs_ballE {R : numDomainType} {M : pseudoMetricType R} :
+  @nbhs_ball R M = nbhs.
 Proof.
 rewrite predeq2E => x P; rewrite -nbhs_entourageE; split.
   by move=> [_/posnumP[e] sbxeP]; exists [set xy | ball xy.1 e%:num xy.2].
@@ -5360,11 +5362,14 @@ Qed.
 
 Section pseudoMetric_of_normedDomain.
 Context {K : numDomainType} {R : normedZmodType K}.
+
 Lemma ball_norm_center (x : R) (e : K) : 0 < e -> ball_ Num.norm x e x.
 Proof. by move=> ? /=; rewrite subrr normr0. Qed.
+
 Lemma ball_norm_symmetric (x y : R) (e : K) :
   ball_ Num.norm x e y -> ball_ Num.norm y e x.
 Proof. by rewrite /= distrC. Qed.
+
 Lemma ball_norm_triangle (x y z : R) (e1 e2 : K) :
   ball_ Num.norm x e1 y -> ball_ Num.norm y e2 z -> ball_ Num.norm x (e1 + e2) z.
 Proof.
@@ -5380,6 +5385,7 @@ rewrite /nbhs_ entourage_E predeq2E => x A; split.
   by exists [set xy | ball_ Num.norm xy.1 e xy.2] => //; exists e.
 by move=> [E [e egt0 sbeE] sEA]; exists e => // ??; apply/sEA/sbeE.
 Qed.
+
 End pseudoMetric_of_normedDomain.
 
 HB.instance Definition _ (R : zmodType) := Pointed.on R^o.