symmetric difference

Co-authored-by: Takafumi Saikawa <[email protected]>

CHANGELOG_UNRELEASED.md

@@ -10,7 +10,16 @@
   + lemma `setCD`
 
 - in `measure.v`:
-  + factory `isAlgebraOfSetsD`
+  + 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`
+
+- in `measure.v`:
+  + factory `isRingOfSets_sym_diff`
 
 - in `classical_sets.v`:
   + lemma `setDU`

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 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.
+
 Notation "'`I_' n" := [set k | is_true (k < n)%N].
 
 Notation "\bigcup_ ( i 'in' P ) F" :=
@@ -1117,6 +1123,59 @@ 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 sym_diff0 A : A `^` set0 = A.
+Proof. by rewrite /sym_diff setD0 set0D setU0. Qed.
+
+Lemma sym_diffT A : A `^` [set: T] = ~` A.
+Proof. by rewrite /sym_diff setDT set0U setTD. Qed.
+
+Lemma sym_diffv A : A `^` ~` A = [set: T].
+Proof. by rewrite /sym_diff setDE setCK setIid setDE setIid setUv. Qed.
+
+Lemma sym_diffC A B : A `^` B = B `^` A.
+Proof. by rewrite /sym_diff setUC. Qed.
+
+Lemma sym_diffA A B C : A `^` (B `^` C) = (A `^` B) `^` C.
+Proof.
+rewrite /sym_diff; 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).
+Proof.
+rewrite /sym_diff; apply/seteqP; split => x/=;
+by have [|] := pselect (A x); have [|] := pselect (B x); tauto.
+Qed.
+
+Lemma sym_diff_setU 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); 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.
+Proof.
+rewrite /sym_diff; 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).
+Proof.
+rewrite /sym_diff; apply/seteqP; split => x/=;
+by have [|] := pselect (A x); have [|] := pselect (B x);
+  have [|] := pselect (C x); tauto.
+Qed.
+
 End basic_lemmas.
 #[global]
 Hint Resolve subsetUl subsetUr subIsetl subIsetr subDsetl subDsetr : core.

theories/measure.v

@@ -187,6 +187,7 @@ From HB Require Import structures.
 (*      setU_closed G == the set of sets G is closed under finite union       *)
 (*      setC_closed G == the set of sets G is closed under complement         *)
 (*      setD_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  *)
 (*     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     *)
@@ -352,6 +353,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 setD_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 fin_bigcap_closed :=
     forall I (D : set I) A_, finite_set D -> (forall i, D i -> G (A_ i)) ->
@@ -1160,6 +1162,39 @@ HB.instance Definition _ := SemiRingOfSets_isRingOfSets.Build d T measurableU.
 
 HB.end.
 
+HB.factory Record isRingOfSets_sym_diff (d : measure_display) T
+    of Pointed T := {
+  measurable : set (set T) ;
+  measurable_nonempty : measurable !=set0 ;
+  measurable_sym_diff : sym_diff_closed measurable ;
+  measurable_setI : setI_closed measurable }.
+
+HB.builders Context d T of isRingOfSets_sym_diff d T.
+
+Let m0 : measurable set0.
+Proof.
+have [A mA] := measurable_nonempty.
+have := measurable_sym_diff mA mA.
+by rewrite sym_diffxx.
+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.
+Qed.
+
+Let mD : setDI_closed measurable.
+Proof.
+move=> A B mA mB; rewrite -sym_diff_setD.
+by apply: measurable_sym_diff => //; 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 ;
@@ -1185,13 +1220,13 @@ HB.instance Definition _ := RingOfSets_isAlgebraOfSets.Build d T measurableT.
 
 HB.end.
 
-HB.factory Record isAlgebraOfSetsD (d : measure_display) T of Pointed T := {
+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 isAlgebraOfSetsD d T.
+HB.builders Context d T of isAlgebraOfSets_setD d T.
 
 Let m0 : measurable set0.
 Proof. by rewrite -(setDT setT); apply: measurableD; exact: measurableT. Qed.
@@ -1205,6 +1240,8 @@ 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 := {