Merge pull request #336 from math-comp/generalize_trivIset

generalize the defintion of trivIset

CHANGELOG_UNRELEASED.md

@@ -16,6 +16,13 @@
 - in `normedtype.v`, lemmas `nbhs0_lt`, `nbhs'0_lt`, `interior_closed_ballE`, open_nbhs_closed_ball`
 - in `classical_sets.v`, lemmas `subset_has_lbound`, `subset_has_ubound`
 
+- in `classical_sets.v`, lemma `mksetE`
+
+- in `classical_sets.v`:
+  + definitions `cover`, `partition`, `pblock_index`, `pblock`
+  + lemmas `trivIsetP`, `trivIset_sets`, `trivIset_restr`, `perm_eq_trivIset`
+  + lemma `fdisjoint_cset`
+
 - in `reals.v`, lemmas `sup_setU`, `inf_setU`
 - in `boolp.v`, lemmas `iff_notr`, `iff_not2`
 - in `reals.v`, lemmas `RtointN`, `floor_le0`
@@ -44,6 +51,9 @@
   + same change for `<`
   + change extended to notations `_ <= _ <= _`, `_ < _ <= _`, `_ <= _ < _`, `_ < _ < _`
 
+- in `classical_sets.v`:
+  + generalization and change of `trivIset` (and thus lemmas `trivIset_bigUI` and `trivIset_setI`)
+
 ### Renamed
 
 - in `normedtype.v`, `bounded_on` -> `bounded_near`

theories/classical_sets.v

@@ -230,6 +230,9 @@ Definition setM T1 T2 (A1 : set T1) (A2 : set T2) := [set z | A1 z.1 /\ A2 z.2].
 Definition fst_set T1 T2 (A : set (T1 * T2)) := [set x | exists y, A (x, y)].
 Definition snd_set T1 T2 (A : set (T1 * T2)) := [set y | exists x, A (x, y)].
 
+Lemma mksetE (P : T -> Prop) x : [set x | P x] x = P x.
+Proof. by []. Qed.
+
 Definition bigsetI T I (P : set I) (F : I -> set T) :=
   [set a | forall i, P i -> F i a].
 Definition bigsetU T I (P : set I) (F : I -> set T) :=
@@ -567,6 +570,15 @@ Proof. by rewrite 2!setDE setCI setCK setIUr setICr set0U. Qed.
 
 End basic_lemmas.
 
+(* TODO: other lemmas that relate fset and classical sets *)
+Lemma fdisjoint_cset (T : choiceType) (A B : {fset T}) :
+  [disjoint A & B]%fset = ([set x | x \in A] `&` [set x | x \in B] == set0).
+Proof.
+rewrite -fsetI_eq0; apply/idP/idP; apply: contraLR.
+by move=> /set0P[t [tA tB]]; apply/fset0Pn; exists t; rewrite inE; apply/andP.
+by move=> /fset0Pn[t]; rewrite inE => /andP[tA tB]; apply/set0P; exists t.
+Qed.
+
 Section SetMonoids.
 Variable (T : Type).
 
@@ -775,20 +787,6 @@ Lemma preimage_bigcap {aT rT I} (P : set I) (f : aT -> rT) F :
   f @^-1` (\bigcap_ (i in P) F i) = \bigcap_(i in P) (f @^-1` F i).
 Proof. exact/predeqP. Qed.
 
-Definition trivIset T (F : nat -> set T) :=
-  forall i j, i != j -> F i `&` F j = set0.
-
-Lemma trivIset_bigUI T (F : nat -> set T) : trivIset F ->
-  forall n m, n <= m -> \big[setU/set0]_(i < n) F i `&` F m = set0.
-Proof.
-move=> tF; elim => [|n ih m]; first by move=> m _; rewrite big_ord0 set0I.
-by rewrite ltn_neqAle => /andP[? ?]; rewrite big_ord_recr setIUl tF ?setU0 ?ih.
-Qed.
-
-Lemma trivIset_setI T (F : nat -> set T) : trivIset F ->
-  forall A, trivIset (fun n => A `&` F n).
-Proof. by move=> tF A j i /tF; apply: subsetI_eq0; apply subIset; right. Qed.
-
 Lemma setM0 T1 T2 (A1 : set T1) : A1 `*` set0 = set0 :> set (T1 * T2).
 Proof. by rewrite predeqE => -[t u]; split => // -[]. Qed.
 
@@ -944,6 +942,83 @@ Proof. exact: (xgetPN point). Qed.
 
 End PointedTheory.
 
+Section partitions.
+
+Definition trivIset T I (D : set I) (F : I -> set T) :=
+  forall i j : I, D i -> D j -> F i `&` F j !=set0 -> i = j.
+
+Lemma trivIsetP {T} {I : eqType} {D : set I} {F : I -> set T} :
+  trivIset D F <->
+  forall i j : I, D i -> D j -> i != j -> F i `&` F j = set0.
+Proof.
+split=> tDF i j Di Dj; first by apply: contraNeq => /set0P/tDF->.
+by move=> /set0P; apply: contraNeq => /tDF->.
+Qed.
+
+Lemma trivIset_bigUI T (D : {pred nat}) (F : nat -> set T) : trivIset D F ->
+  forall n m, D m -> n <= m -> \big[setU/set0]_(i < n | D i) F i `&` F m = set0.
+Proof.
+move=> /trivIsetP tA; elim => [|n IHn] m Dm.
+  by move=> _; rewrite big_ord0 set0I.
+move=> lt_nm; rewrite big_mkcond/= big_ord_recr -big_mkcond/=.
+rewrite setIUl IHn 1?ltnW// set0U.
+by case: ifPn => [Dn|NDn]; rewrite ?set0I// tA// ltn_eqF.
+Qed.
+
+Lemma trivIset_setI T I D (F : I -> set T) X :
+  trivIset D F -> trivIset D (fun i => X `&` F i).
+Proof.
+move=> tDF i j Di Dj; rewrite setIACA setIid => -[x [_ Fijx]].
+by apply: tDF => //; exists x.
+Qed.
+
+Definition cover T I D (F : I -> set T) := \bigcup_(i in D) F i.
+
+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].
+
+Definition pblock_index T (I : pointedType) D (F : I -> set T) (x : T) :=
+  get (fun i => D i /\ F i x).
+
+Definition pblock T (I : pointedType) D (F : I -> set T) (x : T) :=
+  F (pblock_index D F x).
+
+(* TODO: theory of trivIset, cover, partition, pblock_index and pblock *)
+
+Lemma trivIset_sets T I D (F : I -> set T) :
+  trivIset D F -> trivIset [set F i | i in D] id.
+Proof. by move=> DF A B [i Di <-{A}] [j Dj <-{B}] /DF ->. Qed.
+
+Lemma trivIset_restr T I D' D (F : I -> set T) :
+(*  D `<=` D' -> (forall i, D i -> ~ D' i -> F i !=set0) ->*)
+  D `<=` D' -> (forall i, D' i -> ~ D i -> F i = set0) ->
+  trivIset D F = trivIset D' F.
+Proof.
+move=> DD' DD'F.
+rewrite propeqE; split=> [DF i j D'i D'j FiFj0|D'F i j Di Dj FiFj0].
+  have [Di|Di] := pselect (D i); last first.
+    by move: FiFj0; rewrite (DD'F i) // set0I => /set0P; rewrite eqxx.
+  have [Dj|Dj] := pselect (D j).
+  - exact: DF.
+  - by move: FiFj0; rewrite (DD'F j) // setI0 => /set0P; rewrite eqxx.
+by apply D'F => //; apply DD'.
+Qed.
+
+Lemma perm_eq_trivIset {T : eqType} (s1 s2 : seq (set T)) : perm_eq s1 s2 ->
+  trivIset setT (fun i => nth set0 s1 i) ->
+  trivIset setT (fun i => nth set0 s2 i).
+Proof.
+rewrite perm_sym => /(perm_iotaP set0)[s ss1 s12] /trivIsetP /(_ _ _ I I) ts1.
+apply/trivIsetP => i j _ _ ij.
+rewrite {}s12 {s2}; have [si|si] := ltnP i (size s); last first.
+  by rewrite (nth_default set0) ?size_map// set0I.
+rewrite (nth_map O) //; have [sj|sj] := ltnP j (size s); last first.
+  by rewrite (nth_default set0) ?size_map// setI0.
+by rewrite  (nth_map O) // ts1 // nth_uniq // (perm_uniq ss1) iota_uniq.
+Qed.
+
+End partitions.
+
 Definition total_on T (A : set T) (R : T -> T -> Prop) :=
   forall s t, A s -> A t -> R s t \/ R t s.
 

theories/measure.v

@@ -235,31 +235,32 @@ Definition semi_additive2 := forall A B, measurable A -> measurable B ->
   A `&` B = set0 -> mu (A `|` B) = (mu A + mu B)%E.
 
 Definition semi_additive :=
-  forall A, (forall i, measurable (A i)) -> trivIset A ->
+  forall A, (forall i : nat, measurable (A i)) -> trivIset setT A ->
   (forall n, measurable (\big[setU/set0]_(i < n) A i)) ->
   forall n, mu (\big[setU/set0]_(i < n) A i) = (\sum_(i < n) mu (A i))%E.
 
 Definition semi_sigma_additive :=
-  forall A, (forall i, measurable (A i)) -> trivIset A ->
+  forall A, (forall i : nat, measurable (A i)) -> trivIset setT A ->
   measurable (\bigcup_n A n) ->
   (fun n => (\sum_(i < n) mu (A i))%E) --> mu (\bigcup_n A n).
 
 Definition additive2 := forall A B, measurable A -> measurable B ->
   A `&` B = set0 -> mu (A `|` B) = (mu A + mu B)%E.
 
 Definition additive :=
-  forall A, (forall i, measurable (A i)) -> trivIset A ->
+  forall A, (forall i : nat, measurable (A i)) -> trivIset setT A ->
   forall n, mu (\big[setU/set0]_(i < n) A i) = (\sum_(i < n) mu (A i))%E.
 
 Definition sigma_additive :=
-  forall A, (forall i, measurable (A i)) -> trivIset A ->
+  forall A, (forall i : nat, measurable (A i)) -> trivIset setT A ->
   (fun n => (\sum_(i < n) mu (A i))%E) --> mu (\bigcup_n A n).
 
 Lemma semi_additive2P : mu set0 = 0%:E -> semi_additive <-> semi_additive2.
 Proof.
-move=> mu0; split => [amx A B mA mB mAB AB|a2mx A mA ATI mbigA n].
+move=> mu0; split => [amx A B mA mB mAB AB|a2mx A mA /trivIsetP ATI mbigA n].
   set C := bigcup2 A B.
-  have tC : trivIset C by move=> [|[|i]] [|[|j]]; rewrite ?set0I ?setI0// setIC.
+  have tC : trivIset setT C.
+    by apply/trivIsetP => -[|[|i]] [|[|j]]; rewrite ?set0I ?setI0// setIC.
   have mC : forall i, measurable (C i).
     by move=> [|[]] //= i; exact: measurable0.
   have := amx _ mC tC _ 2%N; rewrite !big_ord_recl !big_ord0 adde0/= setU0.
@@ -272,12 +273,10 @@ move=> mu0; split => [amx A B mA mB mAB AB|a2mx A mA ATI mbigA n].
 elim: n => [|n IHn] in A mA ATI mbigA *.
   by rewrite !big_ord0.
 rewrite big_ord_recr /= a2mx //; last 3 first.
-   exact: mbigA.
-   have := mbigA n.+1.
-   by rewrite big_ord_recr.
-   rewrite big_distrl /= big1 // => i _; apply: ATI; rewrite lt_eqF //.
-   exact: ltn_ord.
-by rewrite IHn // [in RHS]big_ord_recr.
+- exact: mbigA.
+- by have := mbigA n.+1; rewrite big_ord_recr.
+- by rewrite big_distrl /= big1 // => i _; rewrite ATI// ltn_eqF.
+- by rewrite IHn // [in RHS]big_ord_recr.
 Qed.
 
 End semi_additivity.
@@ -309,7 +308,8 @@ Lemma semi_sigma_additive_is_additive
 Proof.
 move=> mu0 samu; apply/semi_additive2P => // A B mA mB mAB AB_eq0.
 pose C := bigcup2 A B.
-have tC : trivIset C by move=> [|[|i]] [|[|j]]; rewrite ?setI0 ?set0I// setIC.
+have tC : trivIset setT C.
+  by apply/trivIsetP=> -[|[|i]] [|[|j]]; rewrite ?setI0 ?set0I// setIC.
 have -> : A `|` B = \bigcup_i C i.
   rewrite predeqE => x; split.
     by case=> [Ax|Bx]; by [exists 0%N|exists 1%N].
@@ -516,12 +516,12 @@ Definition B_of (A : (set T) ^nat) :=
   fun n => if n isn't n'.+1 then A O else A n `\` A n'.
 
 Lemma trivIset_B_of (A : (set T) ^nat) :
-  {homo A : n m / (n <= m)%nat >-> n `<=` m} -> trivIset (B_of A).
+  {homo A : n m / (n <= m)%nat >-> n `<=` m} -> trivIset setT (B_of A).
 Proof.
-move=> ndA i j; wlog : i j / (i < j)%N.
-  move=> h; rewrite neq_ltn => /orP[|] ?; by
-    [rewrite h // ltn_eqF|rewrite setIC h // ltn_eqF].
-move=> ij _; move: j i ij; case => // j [_ /=|n].
+move=> ndA i j _ _; wlog ij : i j / (i < j)%N => [/(_ _ _ _) tB|].
+  by have [ij /tB->|ij|] := ltngtP i j; rewrite //setIC => /tB->.
+move=> /set0P; apply: contraNeq => _; apply/eqP.
+case: j i ij => // j [_ /=|n].
   rewrite funeqE => x; rewrite propeqE; split => // -[A0 [Aj1 Aj]].
   exact/Aj/(ndA O).
 rewrite ltnS => nj /=; rewrite funeqE => x; rewrite propeqE; split => //.
@@ -586,7 +586,7 @@ Lemma cvg_mu_inc (A : (set T) ^nat) :
   mu \o A --> mu (\bigcup_n A n).
 Proof.
 move=> mA mbigcupA ndA.
-have Binter : trivIset (B_of A) := trivIset_B_of ndA.
+have Binter : trivIset setT (B_of A) := trivIset_B_of ndA.
 have ABE : forall n, A n.+1 = A n `|` B_of A n.+1 := UB_of ndA.
 have AE n : A n = \big[setU/set0]_(i < n.+1) (B_of A) i := eq_bigsetUB_of n ndA.
 have -> : \bigcup_n A n = \bigcup_n (B_of A) n := eq_bigcupB_of ndA.