Library finset

Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq div choice fintype.
Require Import finfun bigops.

This file defines a type for sets over a finite Type, similarly to (and,  
 indeed, using) finfun.v:                                                  
  {set T} where T must have a finType structure                            
 We equip {set T} itself with a finType structure, hence Leinitz and       
 extensional equalities coincide on {set T}, and we can form {set {set T}} 
   If A, B : {set T} and P : {set {set T}}, we define:                     
           x \in A == x belongs to A (i.e., {set T} implements predType,   
                      by coercion to pred_sort)                            
             mem A == the predicate corresponding to A                     
          finset p == the A corresponding to a predicate p                 
       [set x | C] == the A containing the x such that C holds (x is bound 
                      in C)                                                
     [set x \in D] == the A containing the x in the collective predicate D 
 [set x \in D | C] == the A containing the x in D such that C holds        
              set0 == the empty set                                        
  [set: T] or setT == the full set (the A containing all x : T)            
           A :|: B == the union of A and B                                 
            x |: A == add x to A                                           
           A :&: B == the intersection of A and B                          
              ~: A == the complement of A                                  
           A :\: B == the difference A minus B                             
            A :\ x == remove x from A                                      
 \bigcup_<range> A == the union of all A, for i in <range> (i is bound in  
                      A, see bigops.v)                                     
 \bigcap_<range> A == the intersection of all A, for i in <range>          
           cover P == the union of the set of sets P                       
        trivIset P == the elements of P are pairwise disjoint              
     partition P A == P is a partition of A                                
          P ::&: A == those sets in P that are subsets of A                
        minset p A == A is a minimal set satisfying p                      
        maxset p A == A is a maximal set satisfying p                      
 We also provide notations A :=: B, A :<>: B, A :==: B, A :!=: B, A :=P: B 
 that specialize A = B, A <> B, A == B, etc., to {set _}. This is useful   
 for subtypes of {set T}, such as {group T}, that coerce to {set T}.       
   We give many lemmas on these operations, on card, and on set inclusion. 

Import Prenex Implicits.
Section SetType.

Variable T : finType.

We should really use a Record to declare set_type, but that runs against  
 a Coq bug that zaps the Type universe in Record declarations.             

Inductive set_type : predArgType := FinSet of {ffun pred T}.
Definition finfun_of_set A := let: FinSet f := A in f.
Definition set_of of phant T := set_type.
Identity Coercion type_of_set_of : set_of >-> set_type.

Canonical Structure set_subType :=
  Eval hnf in [newType for finfun_of_set by set_type_rect].
Definition set_eqMixin := Eval hnf in [eqMixin of set_type by <:].
Canonical Structure set_eqType := Eval hnf in EqType set_type set_eqMixin.
Definition set_choiceMixin := [choiceMixin of set_type by <:].
Canonical Structure set_choiceType :=
  Eval hnf in ChoiceType set_type set_choiceMixin.
Definition set_countMixin := [countMixin of set_type by <:].
Canonical Structure set_countType :=
  Eval hnf in CountType set_type set_countMixin.
Canonical Structure set_subCountType := Eval hnf in [subCountType of set_type].
Definition set_finMixin := [finMixin of set_type by <:].
Canonical Structure set_finType := Eval hnf in FinType set_type set_finMixin.
Canonical Structure set_subFinType := Eval hnf in [subFinType of set_type].

End SetType.

Delimit Scope set_scope with SET.
Open Scope set_scope.

Notation "{ 'set' T }" := (set_of (Phant T))
  (at level 0, format "{ 'set' T }") : type_scope.

We later define several subtypes that coerce to set; for these it is 
 preferable to state equalities at the {set _} level, even when       
 comparing subtype values, because the primitive "injection" tactic   
 tends to diverge on complex types (e.g., quotient groups).           
 We provide some parse-only notation to make this technicality less   
 obstrusive.                                                          

Notation "A :=: B" := (A = B :> {set _})
  (at level 70, no associativity, only parsing) : set_scope.
Notation "A :<>: B" := (A <> B :> {set _})
  (at level 70, no associativity, only parsing) : set_scope.
Notation "A :==: B" := (A == B :> {set _})
  (at level 70, no associativity, only parsing) : set_scope.
Notation "A :!=: B" := (A != B :> {set _})
  (at level 70, no associativity, only parsing) : set_scope.
Notation "A :=P: B" := (A =P B :> {set _})
  (at level 70, no associativity, only parsing) : set_scope.

Notation Local finset_def := (fun T P => @FinSet T (finfun P)).

Notation Local pred_of_set_def := (fun T (A : set_type T) => val A : _ -> _).

Module Type SetDefSig.
Parameter finset : forall T : finType, pred T -> {set T}.
Parameter pred_of_set : forall T, set_type T -> pred_sort (predPredType T).

This lets us use subtypes of set, like group or coset_of, as predicates. 

Coercion pred_of_set : set_type >-> pred_class.
Axiom finsetE : finset = finset_def.
Axiom pred_of_setE : pred_of_set = pred_of_set_def.
End SetDefSig.

Module SetDef : SetDefSig.
Definition finset := finset_def.
Definition pred_of_set := pred_of_set_def.
Lemma finsetE : finset = finset_def.

Lemma pred_of_setE : pred_of_set = pred_of_set_def.

End SetDef.

Notation finset := SetDef.finset.
Notation pred_of_set := SetDef.pred_of_set.
Canonical Structure finset_unlock := Unlockable SetDef.finsetE.
Canonical Structure pred_of_set_unlock := Unlockable SetDef.pred_of_setE.

Notation "[ 'set' x : T | P ]" := (finset (fun x : T => P))
  (at level 0, x at level 69, only parsing) : set_scope.
Notation "[ 'set' x | P ]" := [set x : _ | P]
  (at level 0, x at level 69, format "[ 'set' x | P ]") : set_scope.
Notation "[ 'set' x \in A | P ]" := [set x | (x \in A) && P]
  (at level 0, x at level 69, format "[ 'set' x \in A | P ]") : set_scope.
Notation "[ 'set' x \in A ]" := [set x | x \in A]
  (at level 0, x at level 69, format "[ 'set' x \in A ]") : set_scope.

Begin outcomment
Notation "A :<=: B" := (pred_of_set A \subset pred_of_set B)
  (at level 70, B at next level, no associativity) : subset_scope.
Notation "A :<: B" := (pred_of_set A \proper pred_of_set B)
   (at level 70, B at next level, no associativity) : subset_scope.
Open Scope subset_scope.
Notation "A :<=: B :<=: C" := ((A :<=: B) && (B :<=: C))
  (at level 70, B at next level, no associativity) : subset_scope.
Notation "A :<: B :<=: C" := ((A :<: B) && (B :<=: C))
  (at level 70, B at next level, no associativity) : subset_scope.
Notation "A :<=: B :<: C" := ((A :<=: B) && (B :<: C))
  (at level 70, B at next level, no associativity) : subset_scope.
Notation "A :<: B :<: C" := ((A :<: B) && (B :<: C))
  (at level 70, B at next level, no associativity) : subset_scope.
End outcomment

Declare pred_of_set as a canonical instance of to_pred, but use the 
 coercion to resolve mem A to @mem (predPredType T) (pred_of_set A). 

Canonical Structure set_predType T :=
  Eval hnf in @mkPredType _ (let s := set_type T in s) (@pred_of_set T).

Begin outcomment Alternative:
Canonical Structure set_predType := Eval hnf in mkPredType pred_of_set.
Canonical Structure set_of_predType := Eval hnf in [predType of sT].
  Not selected because having two different ways of coercing to
  pred causes apply to fail, e.g., the group1 lemma does not apply
  to a 1 \in G with G : group gT when this goal results from
  rewriting A = G in 1 \in A, with A : set gT.
End outcomment

Section BasicSetTheory.

Variable T : finType.
Implicit Type x : T.

Canonical Structure set_of_subType := Eval hnf in [subType of {set T}].
Canonical Structure set_of_eqType := Eval hnf in [eqType of {set T}].
Canonical Structure set_of_choiceType := Eval hnf in [choiceType of {set T}].
Canonical Structure set_of_countType := Eval hnf in [countType of {set T}].
Canonical Structure set_of_subCountType :=
  Eval hnf in [subCountType of {set T}].
Canonical Structure set_of_finType := Eval hnf in [finType of {set T}].
Canonical Structure set_of_subFinType := Eval hnf in [subFinType of {set T}].

Lemma in_set : forall P x, x \in finset P = P x.

Lemma setP : forall A B : {set T}, A =i B <-> A = B.

Definition set0 := [set x : T | false].
Definition setTfor (phT : phant T) := [set x : T | true].

Lemma in_setT : forall x, x \in setTfor (Phant T).

Lemma eqsVneq : forall A B : {set T}, {A = B} + {A != B}.

End BasicSetTheory.

Definition inE := (in_set, inE).

Implicit Arguments set0 [T].
Hint Resolve in_setT.

Notation "[ 'set' : T ]" := (setTfor (Phant T))
  (at level 0, format "[ 'set' : T ]") : set_scope.

Notation setT := [set: _] (only parsing).

Section setOpsDefs.

Variable T : finType.
Implicit Types a x : T.
Implicit Types A B D : {set T}.
Implicit Types P : {set {set T}}.

Definition set1 a := [set x | x == a].
Definition setU A B := [set x | (x \in A) || (x \in B)].
Definition setI A B := [set x | (x \in A) && (x \in B)].
Definition setC A := [set x | x \notin A].
Definition setD A B := [set x | (x \notin B) && (x \in A)].
Definition ssetI P D := [set A \in P | A \subset D].

End setOpsDefs.

Notation "[ 'set' a ]" := (set1 a)
  (at level 0, a at level 69, format "[ 'set' a ]") : set_scope.
Notation "A :|: B" := (setU A B) (at level 52, left associativity) : set_scope.
Notation "a |: A" := ([set a] :|: A)
  (at level 52, left associativity) : set_scope.

This is left-associative due to limitations of the .. Notation 

Notation "[ 'set' a1 ; a2 ; .. ; an ]" :=
  (setU .. Notation "A :&: B" := (setI A B) (at level 48, left associativity) : set_scope.
Notation "~: A" := (setC A) (at level 35, right associativity) : set_scope.
Notation "[ 'set' ~ a ]" := (~: [set a])
  (at level 0, a at level 69, format "[ 'set' ~ a ]") : set_scope.
Notation "A :\: B" := (setD A B) (at level 50) : set_scope.
Notation "A :\ a" := (A :\: [set a]) (at level 50) : set_scope.
Notation "P ::&: D" := (ssetI P D) (at level 48) : set_scope.

Section setOps.

Variable T : finType.
Implicit Types a x : T.
Implicit Types A B C D : {set T}.

Lemma eqEsubset : forall A B, (A == B) = (A \subset B) && (B \subset A).

Lemma subEproper : forall A B, A \subset B = (A == B) || (A \proper B).

Lemma properEneq : forall A B, A \proper B = (A != B) && (A \subset B).

Lemma eqEproper : forall A B, (A == B) = (A \subset B) && ~~ (A \proper B).

Lemma eqEcard : forall A B, (A == B) = (A \subset B) && (#|B| <= #|A|).

Lemma properEcard : forall A B, (A \proper B) = (A \subset B) && (#|A| < #|B|).

Lemma proper_neq : forall A B, A \proper B -> A != B.

Lemma in_set0 : forall x, x \in set0 = false.

Lemma sub0set : forall A, set0 \subset A.

Lemma subset0 : forall A, (A \subset set0) = (A == set0).

Lemma proper0 : forall A, (set0 \proper A) = (A != set0).

Lemma set_0Vmem : forall A, (A = set0) + {x : T | x \in A}.

Lemma subsetT : forall A, A \subset setT.

Lemma subTset : forall A, (setT \subset A) = (A == setT).

Lemma properT : forall A, (A \proper setT) = (A != setT).

Lemma set1P : forall x a, reflect (x = a) (x \in [set a]).

Lemma in_set1 : forall x a, (x \in [set a]) = (x == a).

Lemma set11 : forall x, x \in [set x].

Lemma set1_inj : injective (@set1 T).

Lemma setU1P : forall x a B, reflect (x = a \/ x \in B) (x \in a |: B).

Lemma in_setU1 : forall x a B, (x \in a |: B) = (x == a) || (x \in B).

Lemma set_cons : forall a s, [set x \in a :: s] = a |: [set x \in s].

Lemma setU11 : forall x B, x \in x |: B.

Lemma setU1r : forall x a B, x \in B -> x \in a |: B.

We need separate lemmas for the explicit enumerations since they 
 associate on the left.                                           

Lemma set1Ul : forall x A b, x \in A -> x \in A :|: [set b].

Lemma set1Ur : forall A b, b \in A :|: [set b].

Lemma in_setC1 : forall x a, (x \in [set~ a]) = (x != a).

Lemma setC11 : forall x, (x \in [set~ x]) = false.

Lemma setD1P : forall x A b, reflect (x != b /\ x \in A) (x \in A :\ b).

Lemma in_setD1 : forall x A b, (x \in A :\ b) = (x != b) && (x \in A) .

Lemma setD11 : forall b A, (b \in A :\ b) = false.

Lemma setD1K : forall a A, a \in A -> a |: (A :\ a) = A.

Lemma setU1K : forall a B, a \notin B -> (a |: B) :\ a = B.

Lemma set2P : forall x a b, reflect (x = a \/ x = b) (x \in [set a; b]).

Lemma in_set2 : forall x a b, (x \in [set a; b]) = (x == a) || (x == b).

Lemma set21 : forall a b, a \in [set a; b].

Lemma set22 : forall a b, b \in [set a; b].

Lemma setUP : forall x A B, reflect (x \in A \/ x \in B) (x \in A :|: B).

Lemma in_setU : forall x A B, (x \in A :|: B) = (x \in A) || (x \in B).

Lemma setUC : forall A B, A :|: B = B :|: A.

Lemma setUS : forall A B C, A \subset B -> C :|: A \subset C :|: B.

Lemma setSU : forall A B C, A \subset B -> A :|: C \subset B :|: C.

Lemma setUSS : forall A B C D,
  A \subset C -> B \subset D -> A :|: B \subset C :|: D.

Lemma set0U : forall A, set0 :|: A = A.

Lemma setU0 : forall A, A :|: set0 = A.

Lemma setUA : forall A B C, A :|: (B :|: C) = A :|: B :|: C.

Lemma setUCA : forall A B C, A :|: (B :|: C) = B :|: (A :|: C).

Lemma setUAC : forall A B C, A :|: B :|: C = A :|: C :|: B.

Lemma setTU : forall A, setT :|: A = setT.

Lemma setUT : forall A, A :|: setT = setT.

Lemma setUid : forall A, A :|: A = A.

Lemma setUUl : forall A B C, A :|: B :|: C = (A :|: C) :|: (B :|: C).

Lemma setUUr : forall A B C, A :|: (B :|: C) = (A :|: B) :|: (A :|: C).

intersect 

setIdP is a generalisation of setIP that applies to comprehensions. 

Lemma setIdP : forall x (pA pB : pred T),
  reflect (pA x /\ pB x) (x \in [set y | pA y && pB y]).

Lemma setIdE: forall A (p : pred T), [set x \in A | p x] = A :&: [set x | p x].

Lemma setIP : forall x A B,
  reflect (x \in A /\ x \in B) (x \in A :&: B).

Lemma in_setI : forall x A B, (x \in A :&: B) = (x \in A) && (x \in B).

Lemma setIC : forall A B, A :&: B = B :&: A.

Lemma setIS : forall A B C, A \subset B -> C :&: A \subset C :&: B.

Lemma setSI : forall A B C, A \subset B -> A :&: C \subset B :&: C.

Lemma setISS : forall A B C D,
  A \subset C -> B \subset D -> A :&: B \subset C :&: D.

Lemma setTI : forall A, setT :&: A = A.

Lemma setIT : forall A, A :&: setT = A.

Lemma set0I : forall A, set0 :&: A = set0.

Lemma setI0 : forall A, A :&: set0 = set0.

Lemma setIA : forall A B C, A :&: (B :&: C) = A :&: B :&: C.

Lemma setICA : forall A B C, A :&: (B :&: C) = B :&: (A :&: C).

Lemma setIAC : forall A B C, A :&: B :&: C = A :&: C :&: B.

Lemma setIid : forall A, A :&: A = A.

Lemma setIIl : forall A B C, A :&: B :&: C = (A :&: C) :&: (B :&: C).

Lemma setIIr : forall A B C, A :&: (B :&: C) = (A :&: B) :&: (A :&: C).

distribute /cancel 

Lemma setIUr : forall A B C, A :&: (B :|: C) = (A :&: B) :|: (A :&: C).

Lemma setIUl : forall A B C, (A :|: B) :&: C = (A :&: C) :|: (B :&: C).

Lemma setUIr : forall A B C, A :|: (B :&: C) = (A :|: B) :&: (A :|: C).

Lemma setUIl : forall A B C, (A :&: B) :|: C = (A :|: C) :&: (B :|: C).

Lemma setUK : forall A B, (A :|: B) :&: A = A.

Lemma setKU : forall A B, A :&: (B :|: A) = A.

Lemma setIK : forall A B, (A :&: B) :|: A = A.

Lemma setKI : forall A B, A :|: (B :&: A) = A.

complement 

Lemma setCP : forall x A, reflect (~ x \in A) (x \in ~: A).

Lemma in_setC : forall x A, (x \in ~: A) = (x \notin A).

Lemma setCK : involutive (@setC T).

Lemma setC_inj : injective (@setC T).

Lemma subsets_disjoint : forall A B, (A \subset B) = [disjoint A & ~: B].

Lemma disjoints_subset : forall A B, [disjoint A & B] = (A \subset ~: B).

Lemma setCS : forall A B, (~: A \subset ~: B) = (B \subset A).

Lemma setCU : forall A B, ~: (A :|: B) = ~: A :&: ~: B.

Lemma setCI : forall A B, ~: (A :&: B) = ~: A :|: ~: B.

Lemma setUCr : forall A, A :|: (~: A) = setT.

Lemma setICr : forall A, A :&: (~: A) = set0.

Lemma setC0 : ~: set0 = setT :> {set T}.

Lemma setCT : ~: setT = set0 :> {set T}.

difference 

Lemma setDP : forall A B x, reflect (x \in A /\ x \notin B) (x \in A :\: B).

Lemma in_setD : forall A B x, (x \in A :\: B) = (x \notin B) && (x \in A).

Lemma setDE : forall A B, A :\: B = A :&: ~: B.

Lemma setSD : forall A B C, A \subset B -> A :\: C \subset B :\: C.

Lemma setDS : forall A B C, A \subset B -> C :\: B \subset C :\: A.

Lemma setDSS : forall A B C D,
  A \subset C -> D \subset B -> A :\: B \subset C :\: D.

Lemma setD0 : forall A, A :\: set0 = A.

Lemma set0D : forall A, set0 :\: A = set0.

Lemma setDT : forall A, A :\: setT = set0.

Lemma setTD : forall A, setT :\: A = ~: A.

Lemma setDv : forall A, A :\: A = set0.

Lemma setCD : forall A B, ~: (A :\: B) = ~: A :|: B.

Lemma setDUl : forall A B C, (A :|: B) :\: C = (A :\: C) :|: (B :\: C).

Lemma setDUr : forall A B C, A :\: (B :|: C) = (A :\: B) :&: (A :\: C).

Lemma setDIl : forall A B C, (A :&: B) :\: C = (A :\: C) :&: (B :\: C).

Lemma setDIr : forall A B C, A :\: (B :&: C) = (A :\: B) :|: (A :\: C).

Lemma setDDl : forall A B C, (A :\: B) :\: C = A :\: (B :|: C).

Lemma setDDr : forall A B C, A :\: (B :\: C) = (A :\: B) :|: (A :&: C).

cardinal lemmas for sets 

Lemma cardsE : forall P : pred T, #|[set x \in P]| = #|P|.

Lemma sum1dep_card : forall P : pred T, \sum_(x | P x) 1 = #|[set x | P x]|.

Lemma sum_nat_dep_const : forall (P : pred T) n,
  \sum_(x | P x) n = #|[set x | P x]| * n.

Lemma cards0 : #|@set0 T| = 0.

Lemma cards_eq0 : forall A, (#|A| == 0) = (A == set0).

Lemma set0Pn : forall A, reflect (exists x, x \in A) (A != set0).

Lemma card_gt0 : forall A, (0 < #|A|) = (A != set0).

Lemma cards0_eq : forall A, #|A| = 0 -> A = set0.

Lemma cards1 : forall x, #|[set x]| = 1.

Lemma cardsUI : forall A B, #|A :|: B| + #|A :&: B| = #|A| + #|B|.

Lemma cardsT : #|[set: T]| = #|T|.

Lemma cardsID : forall B A, #|A :&: B| + #|A :\: B| = #|A|.

Lemma cardsC : forall A, #|A| + #|~: A| = #|T|.

Lemma cardsCs : forall A, #|A| = #|T| - #|~: A|.

Lemma cardsU1 : forall a A, #|a |: A| = (a \notin A) + #|A|.

Lemma cards2 : forall a b, #|[set a; b]| = (a != b).+1.

Lemma cardsC1 : forall a, #|[set~ a]| = #|T|.-1.

Lemma cardsD1 : forall a A, #|A| = (a \in A) + #|A :\ a|.

other inclusions 

Lemma subsetIl : forall A B, A :&: B \subset A.

Lemma subsetIr : forall A B, A :&: B \subset B.

Lemma subsetUl : forall A B, A \subset A :|: B.

Lemma subsetUr : forall A B, B \subset A :|: B.

Lemma subsetDl : forall A B, A :\: B \subset A.

Lemma subsetDr : forall A B, A :\: B \subset ~: B.

Lemma sub1set : forall A x, ([set x] \subset A) = (x \in A).

Lemma cards1P : forall A, reflect (exists x, A = [set x]) (#|A| == 1).

Lemma subset1 : forall A x, (A \subset [set x]) = (A == [set x]) || (A == set0).

Lemma subsetD1 : forall A x, A :\ x \subset A.

Lemma setIidPl : forall A B, reflect (A :&: B = A) (A \subset B).
Implicit Arguments setIidPl [A B].

Lemma setIidPr : forall A B, reflect (A :&: B = B) (B \subset A).

Lemma setUidPl : forall A B, reflect (A :|: B = A) (B \subset A).

Lemma setUidPr : forall A B, reflect (A :|: B = B) (A \subset B).

Lemma setDidPl : forall A B, reflect (A :\: B = A) [disjoint A & B].

Lemma subIset : forall A B C,
  (B \subset A) || (C \subset A) -> (B :&: C \subset A).

Lemma subsetI : forall A B C,
  (A \subset B :&: C) = (A \subset B) && (A \subset C).

Lemma subUset : forall A B C,
  (B :|: C \subset A) = (B \subset A) && (C \subset A).

Lemma subsetU : forall A B C,
  (A \subset B) || (A \subset C) -> A \subset B :|: C.

Lemma subsetD : forall A B C,
  (A \subset B :\: C) = (A \subset B) && [disjoint A & C].

Lemma subDset : forall A B C, (A :\: B \subset C) = (A \subset B :|: C).

Lemma setDeq0 : forall A B, (A :\: B == set0) = (A \subset B).

Lemma properD1 : forall A x, x \in A -> A :\ x \proper A.

Lemma properIr : forall A B, ~~ (B \subset A) -> A :&: B \proper B.

Lemma properIl : forall A B, ~~ (A \subset B) -> A :&: B \proper A.

Lemma properUr : forall A B, ~~ (A \subset B) -> B \proper A :|: B.

Lemma properUl : forall A B, ~~ (B \subset A) -> A \proper A :|: B.

Lemma proper1set : forall A x, ([set x] \proper A) -> (x \in A).

Lemma properIset : forall A B C,
  (B \proper A) || (C \proper A) -> (B :&: C \proper A).

Lemma properI : forall A B C,
  (A \proper B :&: C) -> (A \proper B) && (A \proper C).

Lemma properU : forall A B C,
  (B :|: C \proper A) -> (B \proper A) && (C \proper A).

Lemma properD : forall A B C,
  (A \proper B :\: C) -> (A \proper B) && [disjoint A & C].

End setOps.

Implicit Arguments set1P [T x a].
Implicit Arguments set1_inj [T].
Implicit Arguments set2P [T x a b].
Implicit Arguments setIdP [T x pA pB].
Implicit Arguments setIP [T x A B].
Implicit Arguments setU1P [T x a B].
Implicit Arguments setD1P [T x A b].
Implicit Arguments setUP [T x A B].
Implicit Arguments setDP [T x A B].
Implicit Arguments cards1P [T A].
Implicit Arguments setCP [T x A].
Implicit Arguments setIidPl [T A B].
Implicit Arguments setIidPr [T A B].
Implicit Arguments setUidPl [T A B].
Implicit Arguments setUidPr [T A B].
Implicit Arguments setDidPl [T A B].

Section setOpsAlgebra.

Import Monoid.

Variable T : finType.

Canonical Structure setI_monoid := Law (@setIA T) (@setTI T) (@setIT T).

Canonical Structure setI_comoid := ComLaw (@setIC T).
Canonical Structure setI_muloid := MulLaw (@set0I T) (@setI0 T).

Canonical Structure setU_monoid := Law (@setUA T) (@set0U T) (@setU0 T).
Canonical Structure setU_comoid := ComLaw (@setUC T).
Canonical Structure setU_muloid := MulLaw (@setTU T) (@setUT T).

Canonical Structure setI_addoid := AddLaw (@setUIl T) (@setUIr T).
Canonical Structure setU_addoid := AddLaw (@setIUl T) (@setIUr T).

End setOpsAlgebra.

Section CartesianProd.

Variables fT1 fT2 : finType.
Variables (A1 : {set fT1}) (A2 : {set fT2}).

Definition setX := [set u | (u.1 \in A1) && (u.2 \in A2)].

Lemma in_setX : forall x1 x2,
  ((x1, x2) \in setX) = (x1 \in A1) && (x2 \in A2).

Lemma setXP : forall x1 x2,
  reflect (x1 \in A1 /\ x2 \in A2) ((x1, x2) \in setX).

Lemma cardsX : #|setX| = #|A1| * #|A2|.

End CartesianProd.

Implicit Arguments setXP [x1 x2 fT1 fT2 A1 A2].

Notation Local imset_def :=
  (fun (aT rT : finType) f (D : mem_pred aT) => [set y \in @image aT rT f D]).
Notation Local imset2_def :=
  (fun (aT1 aT2 rT : finType) f (D1 : mem_pred aT1) (D2 : _ -> mem_pred aT2) =>
     [set y \in @image _ rT (prod_curry f) [pred u | D1 u.1 && D2 u.1 u.2]]).

Module Type ImsetSig.
Parameter imset : forall aT rT : finType,
 (aT -> rT) -> mem_pred aT -> {set rT}.
Parameter imset2 : forall aT1 aT2 rT : finType,
 (aT1 -> aT2 -> rT) -> mem_pred aT1 -> (aT1 -> mem_pred aT2) -> {set rT}.
Axiom imsetE : imset = imset_def.
Axiom imset2E : imset2 = imset2_def.
End ImsetSig.

Module Imset : ImsetSig.
Definition imset := imset_def.
Definition imset2 := imset2_def.
Lemma imsetE : imset = imset_def.

Lemma imset2E : imset2 = imset2_def.

End Imset.

Notation imset := Imset.imset.
Notation imset2 := Imset.imset2.
Canonical Structure imset_unlock := Unlockable Imset.imsetE.
Canonical Structure imset2_unlock := Unlockable Imset.imset2E.
Definition preimset (aT : finType) rT f (R : mem_pred rT) :=
  [set x : aT | in_mem (f x) R].

Notation "f @^-1: R" := (preimset f (mem R)) (at level 24) : set_scope.
Notation "f @: D" := (imset f (mem D)) (at level 24) : set_scope.
Notation "f @2: ( D1 , D2 )" := (imset2 f (mem D1) (fun _ => (mem D2)))
  (at level 24, format "f @2: ( D1 , D2 )") : set_scope.
Notation "[ 'set' E | x <- A ]" := ((fun x => E) @: A)
  (at level 0, E at level 69,
   format "[ 'set' E | x <- A ]") : set_scope.
Notation "[ 'set' E | x <- A , P ]" := ((fun x => E) @: [set x \in A | P])
  (at level 0, E at level 69,
   format "[ 'set' E | x <- A , P ]") : set_scope.
Notation "[ 'set' E | x <- A , y <- B ]" :=
  (imset2 (fun x y => E) (mem A) (fun x => (mem B)))
  (at level 0, E at level 69,
   format "[ 'set' E | x <- A , y <- B ]") : set_scope.
Notation "[ 'set' E | x <- A , y <- B , P ]" :=
  [set E | x <- A, y <- [set y \in B | P]] (at level 0, E at level 69,
   format "[ 'set' E | x <- A , y <- B , P ]") : set_scope.
Notation "[ 'set' E | x <- A , y < - B ]" :=
  (imset2 (fun x y => E) (mem A) (fun _ => mem B))
  (at level 0, E at level 69,
   format "[ 'set' E | x <- A , y < - B ]") : set_scope.
Notation "[ 'set' E | x <- A , y < - B , P ]" :=
  (imset2 (fun x y => E) (mem A) (fun _ => mem [set y \in B | P]))
  (at level 0, E at level 69,
   format "[ 'set' E | x <- A , y < - B , P ]") : set_scope.

Section FunImage.

Variables aT aT2 : finType.

Section ImsetTheory.

Variable rT : finType.

Section ImsetProp.

Variables (f : aT -> rT) (f2 : aT -> aT2 -> rT).

Lemma imsetP : forall D y,
  reflect (exists2 x, in_mem x D & y = f x) (y \in imset f D).

CoInductive imset2_spec D1 D2 y : Prop :=
  Imset2spec x1 x2 of in_mem x1 D1 & in_mem x2 (D2 x1) & y = f2 x1 x2.

Lemma imset2P : forall D1 D2 y,
  reflect (imset2_spec D1 D2 y) (y \in imset2 f2 D1 D2).

Lemma mem_imset : forall (D : pred aT) x, x \in D -> f x \in f @: D.

Lemma imset0 : f @: set0 = set0.

Lemma imset_set1 : forall x, f @: [set x] = [set f x].

Lemma mem_imset2 : forall (D : pred aT) (D2 : aT -> pred aT2) x x2,
  x \in D -> x2 \in D2 x ->
   f2 x x2 \in imset2 f2 (mem D) (fun x1 => mem (D2 x1)).

Lemma preimsetS : forall A B : pred rT,
  A \subset B -> (f @^-1: A) \subset (f @^-1: B).

Lemma preimset0 : f @^-1: set0 = set0.

Lemma preimsetT : f @^-1: setT = setT.

Lemma preimsetI : forall A B : {set rT},
  f @^-1: (A :&: B) = (f @^-1: A) :&: (f @^-1: B).

Lemma preimsetU : forall A B : {set rT},
  f @^-1: (A :|: B) = (f @^-1: A) :|: (f @^-1: B).

Lemma preimsetD : forall A B : {set rT},
  f @^-1: (A :\: B) = (f @^-1: A) :\: (f @^-1: B).

Lemma preimsetC : forall A : {set rT},
  f @^-1: (~: A) = ~: f @^-1: A.

Lemma imsetS : forall A B : pred aT,
  A \subset B -> f @: A \subset f @: B.

Lemma imset_proper : forall (A B : {set aT})(injf : {in B, injective f}),
   A \proper B -> f @: A \proper f @: B.

Lemma preimset_proper : forall (A B : {set rT}),
  B \subset codom f -> A \proper B -> (f @^-1: A) \proper (f @^-1: B).

Lemma imsetU : forall A B : {set aT},
  f @: (A :|: B) = (f @: A) :|: (f @: B).

Lemma imsetU1 : forall a (A : {set aT}), f @: (a |: A) = f a |: (f @: A).

Lemma imsetI : forall A B : {set aT},
  {in A & B, injective f} -> f @: (A :&: B) = f @: A :&: f @: B.

Lemma imset2Sl : forall (A B : pred aT) (C : pred aT2),
  A \subset B -> f2 @2: (A, C) \subset f2 @2: (B, C).

Lemma imset2Sr : forall (A B : pred aT2) (C : pred aT),
  A \subset B -> f2 @2: (C, A) \subset f2 @2: (C, B).

Lemma imset2S : forall (A B : pred aT) (A2 B2 : pred aT2),
  A \subset B -> A2 \subset B2 -> f2 @2: (A, A2) \subset f2 @2: (B, B2).

End ImsetProp.

Lemma eq_preimset : forall (f g : aT -> rT) (R : pred rT),
  f =1 g -> f @^-1: R = g @^-1: R.

Lemma eq_imset : forall (f g : aT -> rT) (D : {set aT}),
       f =1 g -> f @: D = g @: D.

Lemma eq_in_imset : forall (f g : aT -> rT) (D : {set aT}),
  {in D, f =1 g} -> f @: D = g @: D.

Lemma eq_in_imset2 :
  forall (f g : aT -> aT2 -> rT) (D : pred aT) (D2 : pred aT2),
  {in D & D2, f =2 g} -> f @2: (D, D2) = g @2: (D, D2).

End ImsetTheory.

Lemma imset2_pair : forall (A : {set aT}) (B : {set aT2}),
  [set (x, y) | x <- A, y <- B] = setX A B.

Lemma setXS : forall (A1 B1 : {set aT}) (A2 B2 : {set aT2}),
  A1 \subset B1 -> A2 \subset B2 -> setX A1 A2 \subset setX B1 B2.

End FunImage.

Implicit Arguments imsetP [aT rT f D y].
Implicit Arguments imset2P [aT aT2 rT f2 D1 D2 y].

Section BigOps.

Variables (R : Type) (idx : R).
Variables (op : Monoid.law idx) (aop : Monoid.com_law idx).
Variables I J : finType.
Implicit Type A B : {set I}.
Implicit Type h : I -> J.
Implicit Type P : pred I.
Implicit Type F : I -> R.

Lemma big_set0 : forall F, \big[op/idx]_(i \in set0) F i = idx.

Lemma big_set1 : forall a F, \big[op/idx]_(i \in [set a]) F i = F a.

Lemma big_setID : forall A B P F,
  \big[aop/idx]_(i \in A | P i) F i =
     aop (\big[aop/idx]_(i \in A :&: B | P i) F i)
         (\big[aop/idx]_(i \in A :\: B | P i) F i).

Lemma big_setD1 : forall a A F, a \in A ->
  \big[aop/idx]_(i \in A) F i = aop (F a) (\big[aop/idx]_(i \in A :\ a) F i).

Lemma big_setU1 : forall a A F, a \notin A ->
  \big[aop/idx]_(i \in a |: A) F i = aop (F a) (\big[aop/idx]_(i \in A) F i).

Lemma big_imset : forall h A G, {in A &, injective h} ->
  \big[aop/idx]_(j \in h @: A) G j = \big[aop/idx]_(i \in A) G (h i).

Lemma partition_big_imset : forall h A F,
  \big[aop/idx]_(i \in A) F i =
     \big[aop/idx]_(j \in h @: A) \big[aop/idx]_(i \in A | h i == j) F i.

End BigOps.

Implicit Arguments big_setID [R idx aop I A].
Implicit Arguments big_setD1 [R idx aop I A F].
Implicit Arguments big_setU1 [R idx aop I A F].
Implicit Arguments big_imset [R idx aop h I J A].
Implicit Arguments partition_big_imset [R idx aop I J].

Section Fun2Set1.

Variables aT1 aT2 rT : finType.
Variables (f : aT1 -> aT2 -> rT).

Lemma imset2_set1l : forall x1 (D2 : pred aT2),
  f @2: ([set x1], D2) = f x1 @: D2.

Lemma imset2_set1r : forall x2 (D1 : pred aT1),
  f @2: (D1, [set x2]) = f^~ x2 @: D1.

End Fun2Set1.

Section CardFunImage.

Variables aT aT2 rT : finType.
Variables (f : aT -> rT) (g : rT -> aT) (f2 : aT -> aT2 -> rT).
Variables (D : pred aT) (D2 : pred aT).

Lemma imset_card : #|f @: D| = #|[image f of D]|.

Lemma leq_imset_card : #|f @: D| <= #|D|.

Lemma card_in_imset : {in D &, injective f} -> #|f @: D| = #|D|.

Lemma card_imset : injective f -> #|f @: D| = #|D|.

Lemma can2_in_imset_pre :
  {in D, cancel f g} -> {on D, cancel g & f} -> f @: D = g @^-1: D.

Lemma can2_imset_pre : cancel f g -> cancel g f -> f @: D = g @^-1: D.

End CardFunImage.

Lemma on_card_preimset : forall (aT rT : finType) (f : aT -> rT) (R : pred rT),
  {on R, bijective f} -> #|f @^-1: R| = #|R|.

Lemma can_imset_pre : forall (T : finType) f g (A : {set T}),
  cancel f g -> f @: A = g @^-1: A :> {set T}.

Lemma card_preimset : forall (T : finType) (f : T -> T) (A : {set T}),
  injective f -> #|f @^-1: A| = #|A|.

Section FunImageComp.

Variables T T' U : finType.

Lemma imset_comp : forall (f : T' -> U) (g : T -> T') (H : pred T),
  (f \o g) @: H = f @: (g @: H).

End FunImageComp.

Reserved Notation "\bigcup_ i F"
  (at level 41, F at level 41, i at level 0,
           format "'[' \bigcup_ i '/ ' F ']'").
Reserved Notation "\bigcup_ ( <- r | P ) F"
  (at level 41, F at level 41, r at level 50,
           format "'[' \bigcup_ ( <- r | P ) '/ ' F ']'").
Reserved Notation "\bigcup_ ( i <- r | P ) F"
  (at level 41, F at level 41, i, r at level 50,
           format "'[' \bigcup_ ( i <- r | P ) '/ ' F ']'").
Reserved Notation "\bigcup_ ( i <- r ) F"
  (at level 41, F at level 41, i, r at level 50,
           format "'[' \bigcup_ ( i <- r ) '/ ' F ']'").
Reserved Notation "\bigcup_ ( m <= i < n | P ) F"
  (at level 41, F at level 41, m, i, n at level 50,
           format "'[' \bigcup_ ( m <= i < n | P ) '/ ' F ']'").
Reserved Notation "\bigcup_ ( m <= i < n ) F"
  (at level 41, F at level 41, i, m, n at level 50,
           format "'[' \bigcup_ ( m <= i < n ) '/ ' F ']'").
Reserved Notation "\bigcup_ ( i | P ) F"
  (at level 41, F at level 41, i at level 50,
           format "'[' \bigcup_ ( i | P ) '/ ' F ']'").
Reserved Notation "\bigcup_ ( i : t | P ) F"
  (at level 41, F at level 41, i at level 50,
           format "'[' \bigcup_ ( i : t | P ) '/ ' F ']'").
Reserved Notation "\bigcup_ ( i : t ) F"
  (at level 41, F at level 41, i at level 50,
           format "'[' \bigcup_ ( i : t ) '/ ' F ']'").
Reserved Notation "\bigcup_ ( i < n | P ) F"
  (at level 41, F at level 41, i, n at level 50,
           format "'[' \bigcup_ ( i < n | P ) '/ ' F ']'").
Reserved Notation "\bigcup_ ( i < n ) F"
  (at level 41, F at level 41, i, n at level 50,
           format "'[' \bigcup_ ( i < n ) '/ ' F ']'").
Reserved Notation "\bigcup_ ( i \in A | P ) F"
  (at level 41, F at level 41, i, A at level 50,
           format "'[' \bigcup_ ( i \in A | P ) '/ ' F ']'").
Reserved Notation "\bigcup_ ( i \in A ) F"
  (at level 41, F at level 41, i, A at level 50,
           format "'[' \bigcup_ ( i \in A ) '/ ' F ']'").

Notation "\bigcup_ ( <- r | P ) F" :=
  (\big[@setU _/set0]_(<- r | P%B) F%SET) : set_scope.
Notation "\bigcup_ ( i <- r | P ) F" :=
  (\big[@setU _/set0]_(i <- r | P) F%SET) : set_scope.
Notation "\bigcup_ ( i <- r ) F" :=
  (\big[@setU _/set0]_(i <- r) F%SET) : set_scope.
Notation "\bigcup_ ( m <= i < n | P ) F" :=
  (\big[@setU _/set0]_(m <= i < n | P%B) F%SET) : set_scope.
Notation "\bigcup_ ( m <= i < n ) F" :=
  (\big[@setU _/set0]_(m <= i < n) F%SET) : set_scope.
Notation "\bigcup_ ( i | P ) F" :=
  (\big[@setU _/set0]_(i | P%B) F%SET) : set_scope.
Notation "\bigcup_ i F" :=
  (\big[@setU _/set0]_i F%SET) : set_scope.
Notation "\bigcup_ ( i : t | P ) F" :=
  (\big[@setU _/set0]_(i : t | P%B) F%SET) (only parsing): set_scope.
Notation "\bigcup_ ( i : t ) F" :=
  (\big[@setU _/set0]_(i : t) F%SET) (only parsing) : set_scope.
Notation "\bigcup_ ( i < n | P ) F" :=
  (\big[@setU _/set0]_(i < n | P%B) F%SET) : set_scope.
Notation "\bigcup_ ( i < n ) F" :=
  (\big[@setU _/set0]_ (i < n) F%SET) : set_scope.
Notation "\bigcup_ ( i \in A | P ) F" :=
  (\big[@setU _/set0]_(i \in A | P%B) F%SET) : set_scope.
Notation "\bigcup_ ( i \in A ) F" :=
  (\big[@setU _/set0]_(i \in A) F%SET) : set_scope.

Reserved Notation "\bigcap_ i F"
  (at level 41, F at level 41, i at level 0,
           format "'[' \bigcap_ i '/ ' F ']'").
Reserved Notation "\bigcap_ ( <- r | P ) F"
  (at level 41, F at level 41, r at level 50,
           format "'[' \bigcap_ ( <- r | P ) '/ ' F ']'").
Reserved Notation "\bigcap_ ( i <- r | P ) F"
  (at level 41, F at level 41, i, r at level 50,
           format "'[' \bigcap_ ( i <- r | P ) F ']'").
Reserved Notation "\bigcap_ ( i <- r ) F"
  (at level 41, F at level 41, i, r at level 50,
           format "'[' \bigcap_ ( i <- r ) '/ ' F ']'").
Reserved Notation "\bigcap_ ( m <= i < n | P ) F"
  (at level 41, F at level 41, m, i, n at level 50,
           format "'[' \bigcap_ ( m <= i < n | P ) '/ ' F ']'").
Reserved Notation "\bigcap_ ( m <= i < n ) F"
  (at level 41, F at level 41, i, m, n at level 50,
           format "'[' \bigcap_ ( m <= i < n ) '/ ' F ']'").
Reserved Notation "\bigcap_ ( i | P ) F"
  (at level 41, F at level 41, i at level 50,
           format "'[' \bigcap_ ( i | P ) '/ ' F ']'").
Reserved Notation "\bigcap_ ( i : t | P ) F"
  (at level 41, F at level 41, i at level 50,
           format "'[' \bigcap_ ( i : t | P ) '/ ' F ']'").
Reserved Notation "\bigcap_ ( i : t ) F"
  (at level 41, F at level 41, i at level 50,
           format "'[' \bigcap_ ( i : t ) '/ ' F ']'").
Reserved Notation "\bigcap_ ( i < n | P ) F"
  (at level 41, F at level 41, i, n at level 50,
           format "'[' \bigcap_ ( i < n | P ) '/ ' F ']'").
Reserved Notation "\bigcap_ ( i < n ) F"
  (at level 41, F at level 41, i, n at level 50,
           format "'[' \bigcap_ ( i < n ) '/ ' F ']'").
Reserved Notation "\bigcap_ ( i \in A | P ) F"
  (at level 41, F at level 41, i, A at level 50,
           format "'[' \bigcap_ ( i \in A | P ) '/ ' F ']'").
Reserved Notation "\bigcap_ ( i \in A ) F"
  (at level 41, F at level 41, i, A at level 50,
           format "'[' \bigcap_ ( i \in A ) '/ ' F ']'").

Notation "\bigcap_ ( <- r | P ) F" :=
  (\big[@setI _/setT]_(<- r | P%B) F%SET) : set_scope.
Notation "\bigcap_ ( i <- r | P ) F" :=
  (\big[@setI _/setT]_(i <- r | P%B) F%SET) : set_scope.
Notation "\bigcap_ ( i <- r ) F" :=
  (\big[@setI _/setT]_(i <- r) F%SET) : set_scope.
Notation "\bigcap_ ( m <= i < n | P ) F" :=
  (\big[@setI _/setT]_(m <= i < n | P%B) F%SET) : set_scope.
Notation "\bigcap_ ( m <= i < n ) F" :=
  (\big[@setI _/setT]_(m <= i < n) F%SET) : set_scope.
Notation "\bigcap_ ( i | P ) F" :=
  (\big[@setI _/setT]_(i | P%B) F%SET) : set_scope.
Notation "\bigcap_ i F" :=
  (\big[@setI _/setT]_i F%SET) : set_scope.
Notation "\bigcap_ ( i : t | P ) F" :=
  (\big[@setI _/setT]_(i : t | P%B) F%SET) (only parsing): set_scope.
Notation "\bigcap_ ( i : t ) F" :=
  (\big[@setI _/setT]_(i : t) F%SET) (only parsing) : set_scope.
Notation "\bigcap_ ( i < n | P ) F" :=
  (\big[@setI _/setT]_(i < n | P%B) F%SET) : set_scope.
Notation "\bigcap_ ( i < n ) F" :=
  (\big[@setI _/setT]_(i < n) F%SET) : set_scope.
Notation "\bigcap_ ( i \in A | P ) F" :=
  (\big[@setI _/setT]_(i \in A | P%B) F%SET) : set_scope.
Notation "\bigcap_ ( i \in A ) F" :=
  (\big[@setI _/setT]_(i \in A) F%SET) : set_scope.

Section BigSetOps.

Variables T I : finType.
Implicit Type U : pred T.
Implicit Type P : pred I.
Implicit Types A B : {set I}.
Implicit Type F : I -> {set T}.

It is very hard to use this lemma, because the unification fails to 
 defer the F j pattern (even though it's a Miller pattern!).         

Lemma bigcup_sup : forall j P F, P j -> F j \subset \bigcup_(i | P i) F i.

Lemma bigcup_max : forall j U P F, P j ->
  U \subset F j -> U \subset \bigcup_(i | P i) F i.

Lemma bigcupP : forall x P F,
  reflect (exists2 i, P i & x \in F i) (x \in \bigcup_(i | P i) F i).

Lemma bigcupsP : forall U P F,
  reflect (forall i, P i -> F i \subset U) (\bigcup_(i | P i) F i \subset U).

Lemma bigcup_disjoint : forall U P F,
    (forall i, P i -> [disjoint U & F i]) ->
  [disjoint U & \bigcup_(i | P i) F i].

Lemma bigcup_setU : forall A B F,
  \bigcup_(i \in A :|: B) F i =
     (\bigcup_(i \in A) F i) :|: (\bigcup_ (i \in B) F i).

Lemma bigcup_seq : forall r F, \bigcup_(i <- r) F i = \bigcup_(i \in r) F i.

Unlike its setU counterpart, this lemma is useable. 

Lemma bigcap_inf : forall j P F, P j -> \bigcap_(i | P i) F i \subset F j.

Lemma bigcap_min : forall j U P F,
   P j -> F j \subset U -> \bigcap_(i | P i) F i \subset U.

Lemma bigcapsP : forall U P F,
  reflect (forall i, P i -> U \subset F i) (U \subset \bigcap_(i | P i) F i).

Lemma bigcapP : forall x P F,
  reflect (forall i, P i -> x \in F i) (x \in \bigcap_(i | P i) F i).

Lemma setC_bigcup : forall r P F,
  ~: (\bigcup_(i <- r | P i) F i) = \bigcap_(i <- r | P i) ~: F i.

Lemma setC_bigcap : forall r P F,
  ~: (\bigcap_(i <- r | P i) F i) = \bigcup_(i <- r | P i) ~: F i.

Lemma bigcap_setU : forall A B F,
  (\bigcap_(i \in A :|: B) F i) =
    (\bigcap_(i \in A) F i) :&: (\bigcap_(i \in B) F i).

Lemma bigcap_seq : forall r F, \bigcap_(i <- r) F i = \bigcap_(i \in r) F i.

End BigSetOps.

Implicit Arguments bigcup_sup [T I P F].
Implicit Arguments bigcup_max [T I U P F].
Implicit Arguments bigcupP [T I x P F].
Implicit Arguments bigcupsP [T I U P F].
Implicit Arguments bigcap_inf [T I P F].
Implicit Arguments bigcap_min [T I U P F].
Implicit Arguments bigcapP [T I x P F].
Implicit Arguments bigcapsP [T I U P F].

Section ImsetCurry.

Variables (aT1 aT2 rT : finType) (f : aT1 -> aT2 -> rT).

Section Curry.

Variables (A1 : {set aT1}) (A2 : {set aT2}).
Variables (D1 : pred aT1) (D2 : pred aT2).

Lemma curry_imset2X : f @2: (A1, A2) = prod_curry f @: (setX A1 A2).

Lemma curry_imset2l : f @2: (D1, D2) = \bigcup_(x1 \in D1) f x1 @: D2.

Lemma curry_imset2r : f @2: (D1, D2) = \bigcup_(x2 \in D2) f^~ x2 @: D1.

End Curry.

Lemma imset2Ul : forall (A B : {set aT1}) (C : {set aT2}),
  f @2: (A :|: B, C) = f @2: (A, C) :|: f @2: (B, C).

Lemma imset2Ur : forall (A : {set aT1}) (B C : {set aT2}),
  f @2: (A, B :|: C) = f @2: (A, B) :|: f @2: (A, C).

End ImsetCurry.

Section Partitions.

Variable T : finType.
Implicit Type A B D : {set T}.
Implicit Types P Q : {set {set T}}.

Definition cover P := \bigcup_(A \in P) A.
Definition trivIset P := \sum_(A \in P) #|A| == #|cover P|.
Definition partition P D := [&& cover P == D, trivIset P & set0 \notin P].

Lemma disjointEsetI : forall A B, [disjoint A & B] = (A :&: B == set0).

Lemma disjoint_setI0 : forall A B, [disjoint A & B] -> A :&: B = set0.

Lemma leq_card_setU : forall A B,
  #|A :|: B| <= #|A| + #|B| ?= iff [disjoint A & B].

Lemma leq_card_cover : forall P,
  #|cover P| <= \sum_(A \in P) #|A| ?= iff trivIset P.

Lemma trivIsetP : forall P,
  reflect {in P &, forall A B, A = B \/ [disjoint A & B]} (trivIset P).

Lemma trivIsetI : forall P D, trivIset P -> trivIset (P ::&: D).

Lemma cover_setI : forall P D, cover (P ::&: D) \subset cover P :&: D.

Definition cover_at x P := odflt set0 (pick [pred A \in P | x \in A]).

Lemma mem_cover_at : forall P x, (x \in cover_at x P) = (x \in cover P).

Lemma cover_at_mem : forall P x, x \in cover P -> cover_at x P \in P.

Lemma cover_at_eq : forall P A x,
  trivIset P -> A \in P -> (x \in cover P) && (cover_at x P == A) = (x \in A).

Lemma same_cover_at : forall P x y,
  trivIset P -> x \in cover_at y P -> cover_at x P = cover_at y P.

Section BigOps.

Variables (R : Type) (idx : R) (op : Monoid.com_law idx).
Let rhs P K F := \big[op/idx]_(A \in P) \big[op/idx]_(x \in A | K x) F x.

Lemma big_trivIset : forall P (K : pred T) (F : T -> R),
  trivIset P -> \big[op/idx]_(x \in cover P | K x) F x = rhs P K F.

Lemma set_partition_big : forall P D (K : pred T) (F : T -> R),
  partition P D -> \big[op/idx]_(x \in D | K x) F x = rhs P K F.

End BigOps.

Section Preim.

Variables (rT : eqType) (f : T -> rT).

Definition preim_at x := f @^-1: pred1 (f x).
Definition preim_partition D := [set D :&: preim_at x | x <- D].

Lemma preim_partitionP : forall D, partition (preim_partition D) D.

End Preim.

Lemma card_partition : forall D P, partition P D -> #|D| = \sum_(A \in P) #|A|.

Lemma card_uniform_partition : forall D P n,
  {in P, forall A, #|A| = n} -> partition P D -> #|D| = #|P| * n.

End Partitions.

Implicit Arguments trivIsetP [T P].
Implicit Arguments big_trivIset [T R idx op K F].
Implicit Arguments set_partition_big [T R idx op D K F].

 

  Maximum and minimun (sub)set with respect to a given pred         
                                                                    

Section MaxSetMinSet.

Variable T : finType.
Notation sT := {set T}.
Implicit Types A B C : sT.
Implicit Type P : pred sT.

Definition minset P A := forallb B : sT, (B \subset A) ==> ((B == A) == P B).

Lemma minset_eq : forall P1 P2 A, P1 =1 P2 -> minset P1 A = minset P2 A.

Lemma minsetP : forall P A,
  reflect ((P A) /\ (forall B, P B -> B \subset A -> B = A)) (minset P A).
Implicit Arguments minsetP [P A].

Lemma minsetp : forall P A, minset P A -> P A.

Lemma minsetinf : forall P A B, minset P A -> P B -> B \subset A -> B = A.

Lemma ex_minset : forall P, (exists A, P A) -> {A | minset P A}.

Lemma minset_exists : forall P C, P C -> {A | minset P A & A \subset C}.

The 'locked' allows Coq to find the value of P by unification. 

Definition maxset P A := minset (fun B => locked P (~: B)) (~: A).

Lemma maxset_eq : forall P1 P2 A, P1 =1 P2 -> maxset P1 A = maxset P2 A.

Lemma maxminset : forall P A, maxset P A = minset [pred B | P (~: B)] (~: A).

Lemma minmaxset : forall P A, minset P A = maxset [pred B | P (~: B)] (~: A).

Lemma maxsetP : forall P A,
  reflect ((P A) /\ (forall B, P B -> A \subset B -> B = A)) (maxset P A).

Lemma maxsetp : forall P A, maxset P A -> P A.

Lemma maxsetsup : forall P A B, maxset P A -> P B -> A \subset B -> B = A.

Lemma ex_maxset : forall P, (exists A, P A) -> {A | maxset P A}.

Lemma maxset_exists : forall P C, P C -> {A : sT | maxset P A & C \subset A}.

End MaxSetMinSet.

Implicit Arguments minsetP [T P A].
Implicit Arguments maxsetP [T P A].