diff --git a/lib/bigop_ext.v b/lib/bigop_ext.v index 7a6af600..acc7dcfb 100644 --- a/lib/bigop_ext.v +++ b/lib/bigop_ext.v @@ -674,3 +674,30 @@ Qed. End classical. End order. + +Section big_union. + +Definition big_union_disj := big_union. + +(* TODO: this is more generic and should be called big_union *) +Lemma big_union_nondisj (R : Type) (idx : R) (M : Monoid.com_law idx) + (A : finType) (X1 X2 : {set A}) (f : A -> R) : + \big[M/idx]_(a in (X1 :&: X2)) f a = idx -> + \big[M/idx]_(a in (X1 :|: X2)) f a = + M (\big[M/idx]_(a in X1) f a) (\big[M/idx]_(a in X2) f a). +Proof. +move=> I0. +rewrite -setIUY big_union_disj 1?disjoint_sym ?setIYI_disj //. +rewrite I0 Monoid.opm1 big_union_disj; last first. + by rewrite -setI_eq0 setIDA setIC Order.SetSubsetOrder.setIDv // set0D. + (* Order.SetSubsetOrder.setIDv is B :&: (A :\: B) = set0 *) +set lhs := LHS. +rewrite -(setID X1 X2) big_union_disj; last first. + by rewrite -setI_eq0 setIC -setIA Order.SetSubsetOrder.setIDv // setI0. +rewrite I0 Monoid.op1m. +rewrite -[in X in M _ X](setID X2 X1) big_union_disj; last first. + by rewrite -setI_eq0 setIC -setIA Order.SetSubsetOrder.setIDv // setI0. +by rewrite setIC I0 Monoid.op1m. +Qed. + +End big_union. diff --git a/lib/ssr_ext.v b/lib/ssr_ext.v index 6ec8cad3..e2b710c3 100644 --- a/lib/ssr_ext.v +++ b/lib/ssr_ext.v @@ -12,6 +12,7 @@ Declare Scope vec_ext_scope. Notation "t '!_' i" := (tnth t i) (at level 9) : tuple_ext_scope. Reserved Notation "A `* B" (at level 46, left associativity). +Reserved Notation "A :+: B" (at level 52, left associativity). Set Implicit Arguments. Unset Strict Implicit. @@ -504,6 +505,21 @@ Qed. Lemma setDUKl A (E F : {set A}) : (E :|: F) :\: E = F :\: E. Proof. by rewrite setDUl setDv set0U. Qed. +Lemma setDIlW (T : finType) (A B C : {set T}) : + A :&: B :\: C = A :&: B :\: C :&: B. +Proof. +apply/setP=> x; rewrite !inE. +by case: (x \in A); case: (x \in B); case: (x \in C). +Qed. + +Lemma setIDACW (T : finType) (A B C : {set T}) : + (A :\: B) :&: C = A :&: C :\: B :&: C. +Proof. by rewrite setIDAC setDIlW. Qed. + +Lemma setDAC (T : finType) (A B C : {set T}) : + A :\: B :\: C = A :\: C :\: B. +Proof. by rewrite setDDl setUC -setDDl. Qed. + Lemma setU_setUD A (E F : {set A}) : E :|: F = F :|: E :\: F. Proof. apply/setP => a; rewrite !inE; apply/orP/orP => -[->|H] ; [ @@ -649,8 +665,45 @@ Lemma big_set2 (R : Type) (idx : R) (op : Monoid.com_law idx) (I : finType) a != b -> \big[op/idx]_(i in [set a; b]) F i = op (F a) (F b). Proof. by move=> ab; rewrite big_setU1 ?inE // big_set1. Qed. +Definition setY (T : finType) (A B : {set T}) := (A :\: B :|: B :\: A). +Notation "A :+: B" := (setY A B). + +Section setY_lemmas. +Variable (T : finType). +Local Notation "+%S" := (@setY T). +Local Notation "-%S" := idfun. +Local Notation "0" := (@set0 T). + +Lemma setYA : associative +%S. +Proof. +move=> x y z; apply/setP=> i; rewrite !inE. +by case: (i \in x); case: (i \in y); case: (i \in z). +Qed. +Lemma setYC : commutative +%S. +Proof. by move=> *; rewrite /setY setUC. Qed. +Lemma set0Y : left_id 0 +%S. +Proof. by move=> ?; rewrite /setY set0D setD0 set0U. Qed. +Lemma setNY : left_inverse 0 -%S +%S. +Proof. by move=> *; rewrite /setY /= setDv setU0. Qed. +Lemma setIYl : left_distributive (@setI T) +%S. +Proof. by move=> *; rewrite [in LHS]/setY setIUl !setIDACW. Qed. + +Lemma setIUY (A B : {set T}) : + (A :+: B) :|: (A :&: B) = A :|: B. +Proof. by apply/setP=> x; rewrite !inE; case: (x \in A); case: (x \in B). Qed. + +Lemma setIYI_disj (A B : {set T}) : + [disjoint (A :+: B) & (A :&: B)]. +Proof. +rewrite -setI_eq0; apply/eqP/setP=> x; rewrite !inE. +by case: (x \in A); case: (x \in B). +Qed. + +End setY_lemmas. + End finset_ext. Notation "A `* B" := (setX A B) : set_scope. +Notation "A :+: B" := (setY A B). Module Set2. Section set2. diff --git a/robust/robustmean.v b/robust/robustmean.v index 38b0dad8..b051e86a 100644 --- a/robust/robustmean.v +++ b/robust/robustmean.v @@ -1,4 +1,4 @@ -From mathcomp Require Import all_ssreflect ssralg ssrnum matrix. +From mathcomp Require Import all_ssreflect all_algebra. From mathcomp Require boolp. From mathcomp Require Import Rstruct reals mathcomp_extra. From mathcomp Require Import lra ring. @@ -28,84 +28,6 @@ Import Order.POrderTheory Order.Theory Num.Theory GRing.Theory. (* *) (******************************************************************************) -Reserved Notation "A :^: B" (at level 52, left associativity). - -Lemma setDIlW (T : finType) (A B C : {set T}) : - A :&: B :\: C = A :&: B :\: C :&: B. -Proof. -apply/setP=> x; rewrite !inE. -by case: (x \in A); case: (x \in B); case: (x \in C). -Qed. - -Lemma setIDACW (T : finType) (A B C : {set T}) : - (A :\: B) :&: C = A :&: C :\: B :&: C. -Proof. by rewrite setIDAC setDIlW. Qed. - -Lemma setDAC (T : finType) (A B C : {set T}) : - A :\: B :\: C = A :\: C :\: B. -Proof. by rewrite setDDl setUC -setDDl. Qed. - -(* symmetric difference *) -Definition adds (T : finType) (A B : {set T}) := (A :\: B :|: B :\: A). -Notation "A :^: B" := (adds A B). - -Section adds_lemmas. -Variable (T : finType). -Implicit Types (A B C : {set T}). -Local Notation "+%S" := (@adds T). -Local Notation "-%S" := idfun. -Local Notation "0" := (@set0 T). - -Lemma addsA : associative +%S. -Proof. -move=> x y z; apply/setP=> i; rewrite !inE. -by case: (i \in x); case: (i \in y); case: (i \in z). -Qed. -Lemma addsC : commutative +%S. -Proof. by move=> *; rewrite /adds setUC. Qed. -Lemma add0s : left_id 0 +%S. -Proof. by move=> ?; rewrite /adds set0D setD0 set0U. Qed. -Lemma addNs : left_inverse 0 -%S +%S. -Proof. by move=> *; rewrite /adds /= setDv setU0. Qed. -Lemma setI_addl : left_distributive (@setI T) +%S. -Proof. by move=> *; rewrite [in LHS]/adds setIUl !setIDACW. Qed. -End adds_lemmas. - -From mathcomp Require Import all_algebra. -Search subsetv. - -Lemma setIUAdd (T : finType) (A B : {set T}) : - (A :^: B) :|: (A :&: B) = A :|: B. -Proof. by apply/setP=> x; rewrite !inE; case: (x \in A); case: (x \in B). Qed. - -Lemma setIIAdd_disj (T : finType) (A B : {set T}) : - [disjoint (A :^: B) & (A :&: B)]. -Proof. -rewrite -setI_eq0; apply/eqP/setP=> x; rewrite !inE. -by case: (x \in A); case: (x \in B). -Qed. - -Definition big_union_disj := big_union. - -Lemma big_union (R : Type) (idx : R) (M : Monoid.com_law idx) - (A : finType) (X1 X2 : {set A}) (f : A -> R) : - \big[M/idx]_(a in (X1 :&: X2)) f a = idx -> - \big[M/idx]_(a in (X1 :|: X2)) f a = - M (\big[M/idx]_(a in X1) f a) (\big[M/idx]_(a in X2) f a). -Proof. -move=> I0. -rewrite -setIUAdd big_union_disj 1?disjoint_sym ?setIIAdd_disj //. -rewrite I0 Monoid.opm1 big_union_disj; last first. - by rewrite -setI_eq0 setIDA setIC Order.SetSubsetOrder.setIDv // set0D. -set lhs := LHS. -rewrite -(setID X1 X2) big_union_disj; last first. - by rewrite -setI_eq0 setIC -setIA Order.SetSubsetOrder.setIDv // setI0. -rewrite I0 Monoid.op1m. -rewrite -[in X in M _ X](setID X2 X1) big_union_disj; last first. - by rewrite -setI_eq0 setIC -setIA Order.SetSubsetOrder.setIDv // setI0. -by rewrite setIC I0 Monoid.op1m. -Qed. - (* TODO: define RV_ringType mimicking fct_ringType *) Section mul_RV. Context {R : realType}. @@ -654,7 +576,7 @@ have[FIH0|FIHneq0]:= eqVneq (Pr P (F :&: H)) 0. rewrite FIH0 mulr0 !addr0=> FIGF. by congr (_ * _)=> //; apply: cEx_sub_eq=> //; exact: subsetIl. move=> FGHF. -rewrite !cExE -!mulrA !mulVf // !mulr1 -big_union /=; last first. +rewrite !cExE -!mulrA !mulVf // !mulr1 -big_union_nondisj /=; last first. have/setIidPl/(congr1 (Pr P)):= FsubGUH. rewrite setIUr Pr_setU FGHF=> /eqP. rewrite -subr_eq0 addrAC subrr add0r oppr_eq0 => /eqP /psumr_eq0P P0. @@ -677,7 +599,7 @@ Lemma cExID (X : {RV P -> R}) (F G : {set U}) : `E_[ X | F ] * Pr P F. Proof. rewrite setDE cEx_union ?setUCr //. -rewrite -big_union /=; last by rewrite setICA -setIA setICr !setI0 big_set0. +rewrite -big_union_nondisj /=; last by rewrite setICA -setIA setICr !setI0 big_set0. by rewrite -setIUr setUCr setIT. Qed.