From d8fc1ad3d9dde84ddedde82b7b5bdfc6184d05f8 Mon Sep 17 00:00:00 2001
From: Reynald Affeldt <reynald.affeldt@aist.go.jp>
Date: Wed, 26 Jun 2024 12:18:38 +0900
Subject: [PATCH] new factory for algebra of sets

Co-authored-by: @JeremyDubut
Co-authored-by: @AkihisaYamada
---
 CHANGELOG_UNRELEASED.md    |  5 +++++
 classical/classical_sets.v |  3 +++
 theories/measure.v         | 22 ++++++++++++++++++++++
 theories/topology.v        | 10 ++++++++--
 4 files changed, 38 insertions(+), 2 deletions(-)

diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index 3bd10f2be8..a67c8558f9 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -6,6 +6,11 @@
 
 - in `topology.v`:
   + lemma `ball_subspace_ball`
+- in `classical_sets.v`:
+  + lemma `setCD`
+
+- in `measure.v`:
+  + factory `isAlgebraOfSetsD`
 
 ### Changed
 
diff --git a/classical/classical_sets.v b/classical/classical_sets.v
index 0360808c37..db6a0c05b9 100644
--- a/classical/classical_sets.v
+++ b/classical/classical_sets.v
@@ -985,6 +985,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.
 
diff --git a/theories/measure.v b/theories/measure.v
index 25ff40621a..e8832fdd1d 100644
--- a/theories/measure.v
+++ b/theories/measure.v
@@ -1183,6 +1183,28 @@ HB.instance Definition _ := RingOfSets_isAlgebraOfSets.Build d T measurableT.
 
 HB.end.
 
+HB.factory Record isAlgebraOfSetsD (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.
+
+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.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
index 82834994df..d0887d093d 100644
--- 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].
@@ -5354,11 +5356,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.
@@ -5374,6 +5379,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.