From 94f29bd187b52bf0994c266c2bcf655c5eabfe82 Mon Sep 17 00:00:00 2001
From: Reynald Affeldt <reynald.affeldt@aist.go.jp>
Date: Fri, 12 Nov 2021 20:14:14 +0900
Subject: [PATCH] lemmas about cover

- from PR #371

Co-authored-by: Cyril Cohen <cyril.cohen@inria.fr>
---
 CHANGELOG_UNRELEASED.md   |  3 +++
 theories/classical_sets.v | 21 +++++++++++++++++++++
 2 files changed, 24 insertions(+)

diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index c1ee5bdc82..9e9db95fd8 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -4,6 +4,9 @@
 
 ### Added
 
+- in `classical_sets.v`:
+  + lemmas `cover_restr`, `eqcover_r`
+
 ### Changed
 
 ### Renamed
diff --git a/theories/classical_sets.v b/theories/classical_sets.v
index c5142df09f..d1dbeb83ab 100644
--- a/theories/classical_sets.v
+++ b/theories/classical_sets.v
@@ -1505,6 +1505,27 @@ Qed.
 
 Definition cover T I D (F : I -> set T) := \bigcup_(i in D) F i.
 
+Lemma cover_restr T I D' D (F : I -> set T) :
+  D `<=` D' -> (forall i, D' i -> ~ D i -> F i = set0) ->
+  cover D F = cover D' F.
+Proof.
+move=> DD' D'DF; rewrite /cover eqEsubset; split=> [r [i Di Fit]|r [i D'i Fit]].
+- by have [D'i|] := pselect (D' i); [exists i | have := DD' _ Di].
+- by have [Di|Di] := pselect (D i); [exists i | move: Fit; rewrite (D'DF i)].
+Qed.
+
+Lemma eqcover_r T I D (F G : I -> set T) :
+  [set F i | i in D] = [set G i | i in D] ->
+  cover D F = cover D G.
+Proof.
+move=> FG.
+rewrite eqEsubset; split => [t [i Di Fit]|t [i Di Git]].
+  have [j Dj GF] : [set G i | i in D] (F i) by rewrite -FG /mkset; exists i.
+  by exists j => //; rewrite GF.
+have [j Dj GF] : [set F i | i in D] (G i) by rewrite FG /mkset; exists i.
+by exists j => //; rewrite GF.
+Qed.
+
 Definition partition T I D (F : I -> set T) (A : set T) :=
   [/\ cover D F = A, trivIset D F & forall i, D i -> F i !=set0].