+ +

Library mathcomp.ssreflect.finset

+ +

+(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.
+ Distributed under the terms of CeCILL-B. *)
+Require Import mathcomp.ssreflect.ssreflect.
+ +
+

+ +

+ This file defines a type for sets over a finite Type, similar to the type + of functions over a finite Type defined in finfun.v (indeed, based in it): + {set T} where T must have a finType structure + We equip {set T} itself with a finType structure, hence Leibnitz 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 set corresponding to a predicate p. + [set x | P] == the set containing the x such that P is true (x may + appear in P). + [set x | P & Q] := [set x | P && Q]. + [set x in A] == the set containing the x in a collective predicate A. + [set x in A | P] == the set containing the x in A such that P is true. + [set x in A | P & Q] := [set x in A | P && Q]. + All these have typed variants [set x : T | P], [set x : T in A], etc. + 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 == A with the element x added (:= [set x] :| A). + A :&: B == the intersection of A and B. + ~: A == the complement of A. + A :\: B == the difference A minus B. + A :\ x == A with the element x removed (:= A :\: [set x]). + \bigcup<range> A == the union of all A, for i in <range> (i is bound in + A, see bigop.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. + pblock P x == a block of P containing x, or else set0. + equivalence_partition R D == the partition induced on D by the relation R + (provided R is an equivalence relation in D). + preim_partition f D == the partition induced on D by the equivalence + [rel x y | f x == f y]. + is_transversal X P D <=> X is a transversal of the partition P of D. + transversal P D == a transversal of P, provided P is a partition of D. + transversal_repr x0 X B == a representative of B \in P selected by the + tranversal X of P, or else x0. + powerset A == the set of all subset of the set A. + P ::&: A == those sets in P that are subsets of the set A. + f @^-1: A == the preimage of the collective predicate A under f. + f @: A == the image set of the collective predicate A by f. + f @2:(A, B) == the image set of A x B by the binary function f. + [set E | x in A] == the set of all the values of the expression E, for x + drawn from the collective predicate A. + [set E | x in A & P] == the set of values of E for x drawn from A, such + that P is true. + [set E | x in A, y in B] == the set of values of E for x drawn from A and + and y drawn from B; B may depend on x. + [set E | x <- A, y <- B & P] == the set of values of E for x drawn from A + y drawn from B, such that P is trye. + [set E | x : T] == the set of all values of E, with x in type T. + [set E | x : T & P] == the set of values of E for x : T s.t. P is true. + [set E | x : T, y : U in B], [set E | x : T, y : U in B & P], + [set E | x : T in A, y : U], [set E | x : T in A, y : U & P], + [set E | x : T, y : U], [set E | x : T, y : U & P] + == type-ranging versions of the binary comprehensions. + [set E | x : T in A], [set E | x in A, y], [set E | x, y & P], etc. + == typed and untyped variants of the comprehensions above. + The types may be required as type inference processes E + before considering A or B. Note that type casts in the + binary comprehension must either be both present or absent + and that there are no untyped variants for single-type + comprehension as Coq parsing confuses [x | P] and [E | x]. + 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. + In addition to the standard suffixes described in ssrbool.v, we associate + the following suffixes to set operations: + 0 -- the empty set, as in in_set0 : (x \in set0) = false. + T -- the full set, as in in_setT : x \in [set: T]. + 1 -- a singleton set, as in in_set1 : (x \in [set a]) = (x == a). + 2 -- an unordered pair, as in + in_set2 : (x \in [set a; b]) = (x == a) || (x == b). + C -- complement, as in setCK : ~: ~: A = A. + I -- intersection, as in setIid : A :&: A = A. + U -- union, as in setUid : A :|: A = A. + D -- difference, as in setDv : A :\: A = set0. + S -- a subset argument, as in + setIS: B \subset C -> A :&: B \subset A :&: C + These suffixes are sometimes preceded with an `s' to distinguish them from + their basic ssrbool interpretation, e.g., + card1 : #|pred1 x| = 1 and cards1 : #| [set x]| = 1 + We also use a trailling `r' to distinguish a right-hand complement from + commutativity, e.g., + setIC : A :&: B = B :&: A and setICr : A :&: ~: A = set0. +

+ +
+Set Implicit Arguments.
+Section SetType.
+ +
+Variable T : finType.
+ +
+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 set_subType := Eval hnf in [newType for finfun_of_set ].
+Definition set_eqMixin := Eval hnf in [eqMixin of set_type by <:].
+Canonical set_eqType := Eval hnf in EqType set_type set_eqMixin.
+Definition set_choiceMixin := [choiceMixin of set_type by <:].
+Canonical set_choiceType := Eval hnf in ChoiceType set_type set_choiceMixin.
+Definition set_countMixin := [countMixin of set_type by <:].
+Canonical set_countType := Eval hnf in CountType set_type set_countMixin.
+Canonical set_subCountType := Eval hnf in [subCountType of set_type ].
+Definition set_finMixin := [finMixin of set_type by <:].
+Canonical set_finType := Eval hnf in FinType set_type set_finMixin.
+Canonical 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.
+ +
+ +
+ +
+Module Type SetDefSig.
+Parameter finset : ∀ T : finType, pred T → {set T }.
+Parameter pred_of_set : ∀ T, set_type T → fin_pred_sort (predPredType T).
+

+ +

+ The weird type of pred_of_set is imposed by the syntactic restrictions on + coercion declarations; it is unfortunately not possible to use a functor + to retype the declaration, because this triggers an ugly bug in the Coq + coercion chaining code. +

+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 finset_unlock := Unlockable SetDef.finsetE.
+Canonical pred_of_set_unlock := Unlockable SetDef.pred_of_setE.
+ +
+Notation "[ 'set' x : T | P ]" := (finset (fun x : T ⇒ P%B))
+  (at level 0, x at level 99, only parsing) : set_scope.
+Notation "[ 'set' x | P ]" := [set x : _ | P]
+  (at level 0, x, P at level 99, format "[ 'set' x | P ]") : set_scope.
+Notation "[ 'set' x 'in' A ]" := [set x | x \in A]
+  (at level 0, x at level 99, format "[ 'set' x 'in' A ]") : set_scope.
+Notation "[ 'set' x : T 'in' A ]" := [set x : T | x \in A]
+  (at level 0, x at level 99, only parsing) : set_scope.
+Notation "[ 'set' x : T | P & Q ]" := [set x : T | P && Q]
+  (at level 0, x at level 99, only parsing) : set_scope.
+Notation "[ 'set' x | P & Q ]" := [set x | P && Q ]
+  (at level 0, x, P at level 99, format "[ 'set' x | P & Q ]") : set_scope.
+Notation "[ 'set' x : T 'in' A | P ]" := [set x : T | x \in A & P]
+  (at level 0, x at level 99, only parsing) : set_scope.
+Notation "[ 'set' x 'in' A | P ]" := [set x | x \in A & P]
+  (at level 0, x at level 99, format "[ 'set' x 'in' A | P ]") : set_scope.
+Notation "[ 'set' x 'in' A | P & Q ]" := [set x in A | P && Q]
+  (at level 0, x at level 99,
+   format "[ 'set' x 'in' A | P & Q ]") : set_scope.
+Notation "[ 'set' x : T 'in' A | P & Q ]" := [set x : T in A | P && Q]
+  (at level 0, x at level 99, only parsing) : set_scope.
+ +
+

+ +

+ This lets us use set and subtypes of set, like group or coset_of, both as + collective predicates and as arguments of the \pi(_) notation. +

+Coercion pred_of_set : set_type >-> fin_pred_sort.
+ +
+

+ +

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

+Canonical set_predType T :=
+  Eval hnf in @mkPredType _ (unkeyed (set_type T)) (@pred_of_set T).
+ +
+Section BasicSetTheory.
+ +
+Variable T : finType.
+Implicit Types (x : T) (A B : {set T }) (pA : pred T).
+ +
+Canonical set_of_subType := Eval hnf in [subType of {set T }].
+Canonical set_of_eqType := Eval hnf in [eqType of {set T }].
+Canonical set_of_choiceType := Eval hnf in [choiceType of {set T }].
+Canonical set_of_countType := Eval hnf in [countType of {set T }].
+Canonical set_of_subCountType := Eval hnf in [subCountType of {set T }].
+Canonical set_of_finType := Eval hnf in [finType of {set T }].
+Canonical set_of_subFinType := Eval hnf in [subFinType of {set T }].
+ +
+Lemma in_set pA x : x \in finset pA = pA x.
+ +
+Lemma setP A B : A =i B ↔ A = B.
+ +
+Definition set0 := [set x : T | false ].
+Definition setTfor (phT : phant T) := [set x : T | true ].
+ +
+Lemma in_setT x : x \in setTfor (Phant T).
+ +
+Lemma eqsVneq A B : {A = B } + {A != B }.
+ +
+End BasicSetTheory.
+ +
+Definition inE := (in_set , inE ).
+ +
+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) (A B D : {set T }) (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 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 ].
+Definition powerset D := [set A : {set T } | A \subset D ].
+ +
+End setOpsDefs.
+ +
+Notation "[ 'set' a ]" := (set1 a)
+  (at level 0, a at level 99, format "[ 'set' a ]") : set_scope.
+Notation "[ 'set' a : T ]" := [set (a : T)]
+  (at level 0, a at level 99, format "[ 'set' a : T ]") : set_scope.
+Notation "A :|: B" := (setU A B) : set_scope.
+Notation "a |: A" := ([set a] :|: A) : set_scope.
+

+ +

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

+Notation "[ 'set' a1 ; a2 ; .. ; an ]" := (setU .. (a1 |: [set a2]) .. [set an])
+  (at level 0, a1 at level 99,
+   format "[ 'set' a1 ; a2 ; .. ; an ]") : set_scope.
+Notation "A :&: B" := (setI A B) : set_scope.
+Notation "~: A" := (setC A) (at level 35, right associativity) : set_scope.
+Notation "[ 'set' ~ a ]" := (~: [set a])
+  (at level 0, format "[ 'set' ~ a ]") : set_scope.
+Notation "A :\: B" := (setD A B) : set_scope.
+Notation "A :\ a" := (A :\: [set a]) : set_scope.
+Notation "P ::&: D" := (ssetI P D) (at level 48) : set_scope.
+ +
+Section setOps.
+ +
+Variable T : finType.
+Implicit Types (a x : T) (A B C D : {set T }) (pA pB pC : pred T).
+ +
+Lemma eqEsubset A B : (A == B ) = (A \subset B ) && (B \subset A ).
+ +
+Lemma subEproper A B : A \subset B = (A == B ) || (A \proper B ).
+ +
+Lemma eqVproper A B : A \subset B → A = B ∨ A \proper B.
+ +
+Lemma properEneq A B : A \proper B = (A != B ) && (A \subset B ).
+ +
+Lemma proper_neq A B : A \proper B → A != B.
+ +
+Lemma eqEproper A B : (A == B ) = (A \subset B ) && ~~ (A \proper B ).
+ +
+Lemma eqEcard A B : (A == B ) = (A \subset B ) && (#|B | ≤ #|A |).
+ +
+Lemma properEcard A B : (A \proper B ) = (A \subset B ) && (#|A | < #|B |).
+ +
+Lemma subset_leqif_cards A B : A \subset B → (#|A | ≤ #|B | ?= iff (A == B )).
+ +
+Lemma in_set0 x : x \in set0 = false.
+ +
+Lemma sub0set A : set0 \subset A.
+ +
+Lemma subset0 A : (A \subset set0 ) = (A == set0 ).
+ +
+Lemma proper0 A : (set0 \proper A ) = (A != set0 ).
+ +
+Lemma subset_neq0 A B : A \subset B → A != set0 → B != set0.
+ +
+Lemma set_0Vmem A : (A = set0 ) + {x : T | x \in A }.
+ +
+Lemma enum_set0 : enum set0 = [::] :> seq T.
+ +
+Lemma subsetT A : A \subset setT.
+ +
+Lemma subsetT_hint mA : subset mA (mem [set : T ]).
+ Hint Resolve subsetT_hint.
+ +
+Lemma subTset A : (setT \subset A ) = (A == setT ).
+ +
+Lemma properT A : (A \proper setT ) = (A != setT ).
+ +
+Lemma set1P x a : reflect (x = a) (x \in [set a ]).
+ +
+Lemma enum_setT : enum [set : T ] = Finite.enum T.
+ +
+Lemma in_set1 x a : (x \in [set a ]) = (x == a ).
+ +
+Lemma set11 x : x \in [set x ].
+ +
+Lemma set1_inj : injective (@set1 T).
+ +
+Lemma enum_set1 a : enum [set a ] = [:: a ].
+ +
+Lemma setU1P x a B : reflect (x = a ∨ x \in B) (x \in a |: B).
+ +
+Lemma in_setU1 x a B : (x \in a |: B ) = (x == a ) || (x \in B ).
+ +
+Lemma set_cons a s : [set x in a :: s ] = a |: [set x in s ].
+ +
+Lemma setU11 x B : x \in x |: B.
+ +
+Lemma setU1r 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 x A b : x \in A → x \in A :|: [set b ].
+ +
+Lemma set1Ur A b : b \in A :|: [set b ].
+ +
+Lemma in_setC1 x a : (x \in [set ¬ a ]) = (x != a ).
+ +
+Lemma setC11 x : (x \in [set ¬ x ]) = false.
+ +
+Lemma setD1P x A b : reflect (x != b ∧ x \in A) (x \in A :\ b).
+ +
+Lemma in_setD1 x A b : (x \in A :\ b ) = (x != b ) && (x \in A ) .
+ +
+Lemma setD11 b A : (b \in A :\ b ) = false.
+ +
+Lemma setD1K a A : a \in A → a |: (A :\ a ) = A.
+ +
+Lemma setU1K a B : a \notin B → (a |: B ) :\ a = B.
+ +
+Lemma set2P x a b : reflect (x = a ∨ x = b) (x \in [set a ; b ]).
+ +
+Lemma in_set2 x a b : (x \in [set a ; b ]) = (x == a ) || (x == b ).
+ +
+Lemma set21 a b : a \in [set a ; b ].
+ +
+Lemma set22 a b : b \in [set a ; b ].
+ +
+Lemma setUP x A B : reflect (x \in A ∨ x \in B) (x \in A :|: B).
+ +
+Lemma in_setU x A B : (x \in A :|: B ) = (x \in A ) || (x \in B ).
+ +
+Lemma setUC A B : A :|: B = B :|: A.
+ +
+Lemma setUS A B C : A \subset B → C :|: A \subset C :|: B.
+ +
+Lemma setSU A B C : A \subset B → A :|: C \subset B :|: C.
+ +
+Lemma setUSS A B C D : A \subset C → B \subset D → A :|: B \subset C :|: D.
+ +
+Lemma set0U A : set0 :|: A = A.
+ +
+Lemma setU0 A : A :|: set0 = A.
+ +
+Lemma setUA A B C : A :|: (B :|: C ) = A :|: B :|: C.
+ +
+Lemma setUCA A B C : A :|: (B :|: C ) = B :|: (A :|: C ).
+ +
+Lemma setUAC A B C : A :|: B :|: C = A :|: C :|: B.
+ +
+Lemma setUACA A B C D : (A :|: B ) :|: (C :|: D ) = (A :|: C ) :|: (B :|: D ).
+ +
+Lemma setTU A : setT :|: A = setT.
+ +
+Lemma setUT A : A :|: setT = setT.
+ +
+Lemma setUid A : A :|: A = A.
+ +
+Lemma setUUl A B C : A :|: B :|: C = (A :|: C ) :|: (B :|: C ).
+ +
+Lemma setUUr A B C : A :|: (B :|: C ) = (A :|: B ) :|: (A :|: C ).
+ +
+

+ +

+ intersection +

+ + setIdP is a generalisation of setIP that applies to comprehensions. +

+Lemma setIdP x pA pB : reflect (pA x ∧ pB x) (x \in [set y | pA y & pB y ]).
+ +
+Lemma setId2P x pA pB pC :
+ reflect [/\ pA x , pB x & pC x ] (x \in [set y | pA y & pB y && pC y ]).
+ +
+Lemma setIdE A pB : [set x in A | pB x ] = A :&: [set x | pB x ].
+ +
+Lemma setIP x A B : reflect (x \in A ∧ x \in B) (x \in A :&: B).
+ +
+Lemma in_setI x A B : (x \in A :&: B ) = (x \in A ) && (x \in B ).
+ +
+Lemma setIC A B : A :&: B = B :&: A.
+ +
+Lemma setIS A B C : A \subset B → C :&: A \subset C :&: B.
+ +
+Lemma setSI A B C : A \subset B → A :&: C \subset B :&: C.
+ +
+Lemma setISS A B C D : A \subset C → B \subset D → A :&: B \subset C :&: D.
+ +
+Lemma setTI A : setT :&: A = A.
+ +
+Lemma setIT A : A :&: setT = A.
+ +
+Lemma set0I A : set0 :&: A = set0.
+ +
+Lemma setI0 A : A :&: set0 = set0.
+ +
+Lemma setIA A B C : A :&: (B :&: C ) = A :&: B :&: C.
+ +
+Lemma setICA A B C : A :&: (B :&: C ) = B :&: (A :&: C ).
+ +
+Lemma setIAC A B C : A :&: B :&: C = A :&: C :&: B.
+ +
+Lemma setIACA A B C D : (A :&: B ) :&: (C :&: D ) = (A :&: C ) :&: (B :&: D ).
+ +
+Lemma setIid A : A :&: A = A.
+ +
+Lemma setIIl A B C : A :&: B :&: C = (A :&: C ) :&: (B :&: C ).
+ +
+Lemma setIIr A B C : A :&: (B :&: C ) = (A :&: B ) :&: (A :&: C ).
+ +
+

+ +

+ distribute /cancel +

+ +

+ complement +

+ +
+Lemma setCP x A : reflect (¬ x \in A) (x \in ~: A).
+ +
+Lemma in_setC x A : (x \in ~: A ) = (x \notin A ).
+ +
+Lemma setCK : involutive (@setC T).
+ +
+Lemma setC_inj : injective (@setC T).
+ +
+Lemma subsets_disjoint A B : (A \subset B ) = [disjoint A & ~: B ].
+ +
+Lemma disjoints_subset A B : [disjoint A & B ] = (A \subset ~: B ).
+ +
+Lemma powersetCE A B : (A \in powerset (~: B)) = [disjoint A & B ].
+ +
+Lemma setCS A B : (~: A \subset ~: B ) = (B \subset A ).
+ +
+Lemma setCU A B : ~: (A :|: B ) = ~: A :&: ~: B.
+ +
+Lemma setCI A B : ~: (A :&: B ) = ~: A :|: ~: B.
+ +
+Lemma setUCr A : A :|: ~: A = setT.
+ +
+Lemma setICr A : A :&: ~: A = set0.
+ +
+Lemma setC0 : ~: set0 = [set : T ].
+ +
+Lemma setCT : ~: [set : T ] = set0.
+ +
+

+ +

+ difference +

+ +
+Lemma setDP A B x : reflect (x \in A ∧ x \notin B) (x \in A :\: B).
+ +
+Lemma in_setD A B x : (x \in A :\: B ) = (x \notin B ) && (x \in A ).
+ +
+Lemma setDE A B : A :\: B = A :&: ~: B.
+ +
+Lemma setSD A B C : A \subset B → A :\: C \subset B :\: C.
+ +
+Lemma setDS A B C : A \subset B → C :\: B \subset C :\: A.
+ +
+Lemma setDSS A B C D : A \subset C → D \subset B → A :\: B \subset C :\: D.
+ +
+Lemma setD0 A : A :\: set0 = A.
+ +
+Lemma set0D A : set0 :\: A = set0.
+ +
+Lemma setDT A : A :\: setT = set0.
+ +
+Lemma setTD A : setT :\: A = ~: A.
+ +
+Lemma setDv A : A :\: A = set0.
+ +
+Lemma setCD A B : ~: (A :\: B ) = ~: A :|: B.
+ +
+Lemma setID A B : A :&: B :|: A :\: B = A.
+ +
+Lemma setDUl A B C : (A :|: B ) :\: C = (A :\: C ) :|: (B :\: C ).
+ +
+Lemma setDUr A B C : A :\: (B :|: C ) = (A :\: B ) :&: (A :\: C ).
+ +
+Lemma setDIl A B C : (A :&: B ) :\: C = (A :\: C ) :&: (B :\: C ).
+ +
+Lemma setIDA A B C : A :&: (B :\: C ) = (A :&: B ) :\: C.
+ +
+Lemma setIDAC A B C : (A :\: B ) :&: C = (A :&: C ) :\: B.
+ +
+Lemma setDIr A B C : A :\: (B :&: C ) = (A :\: B ) :|: (A :\: C ).
+ +
+Lemma setDDl A B C : (A :\: B ) :\: C = A :\: (B :|: C ).
+ +
+Lemma setDDr A B C : A :\: (B :\: C ) = (A :\: B ) :|: (A :&: C ).
+ +
+

+ +

+ powerset +

+ +
+Lemma powersetE A B : (A \in powerset B ) = (A \subset B ).
+ +
+Lemma powersetS A B : (powerset A \subset powerset B ) = (A \subset B ).
+ +
+Lemma powerset0 : powerset set0 = [set set0 ] :> {set {set T }}.
+ +
+Lemma powersetT : powerset [set : T ] = [set : {set T }].
+ +
+Lemma setI_powerset P A : P :&: powerset A = P ::&: A.
+ +
+

+ +

+ cardinal lemmas for sets +

+ +
+Lemma cardsE pA : #|[set x in pA ]| = #|pA |.
+ +
+Lemma sum1dep_card pA : \sum_(x | pA x ) 1 = #|[set x | pA x ]|.
+ +
+Lemma sum_nat_dep_const pA n : \sum_(x | pA x ) n = #|[set x | pA x ]| × n.
+ +
+Lemma cards0 : #|@set0 T | = 0.
+ +
+Lemma cards_eq0 A : (#|A | == 0) = (A == set0 ).
+ +
+Lemma set0Pn A : reflect (∃ x, x \in A) (A != set0).
+ +
+Lemma card_gt0 A : (0 < #|A |) = (A != set0 ).
+ +
+Lemma cards0_eq A : #|A | = 0 → A = set0.
+ +
+Lemma cards1 x : #|[set x ]| = 1.
+ +
+Lemma cardsUI A B : #|A :|: B | + #|A :&: B | = #|A | + #|B |.
+ +
+Lemma cardsU A B : #|A :|: B | = (#|A | + #|B | - #|A :&: B |)%N.
+ +
+Lemma cardsI A B : #|A :&: B | = (#|A | + #|B | - #|A :|: B |)%N.
+ +
+Lemma cardsT : #|[set : T ]| = #|T |.
+ +
+Lemma cardsID B A : #|A :&: B | + #|A :\: B | = #|A |.
+ +
+Lemma cardsD A B : #|A :\: B | = (#|A | - #|A :&: B |)%N.
+ +
+Lemma cardsC A : #|A | + #|~: A | = #|T |.
+ +
+Lemma cardsCs A : #|A | = #|T | - #|~: A |.
+ +
+Lemma cardsU1 a A : #|a |: A | = (a \notin A ) + #|A |.
+ +
+Lemma cards2 a b : #|[set a ; b ]| = (a != b ).+1.
+ +
+Lemma cardsC1 a : #|[set ¬ a ]| = #|T |.-1.
+ +
+Lemma cardsD1 a A : #|A | = (a \in A ) + #|A :\ a |.
+ +
+

+ +

+ other inclusions +

+ +
+Lemma subsetIl A B : A :&: B \subset A.
+ +
+Lemma subsetIr A B : A :&: B \subset B.
+ +
+Lemma subsetUl A B : A \subset A :|: B.
+ +
+Lemma subsetUr A B : B \subset A :|: B.
+ +
+Lemma subsetU1 x A : A \subset x |: A.
+ +
+Lemma subsetDl A B : A :\: B \subset A.
+ +
+Lemma subD1set A x : A :\ x \subset A.
+ +
+Lemma subsetDr A B : A :\: B \subset ~: B.
+ +
+Lemma sub1set A x : ([set x ] \subset A ) = (x \in A ).
+ +
+Lemma cards1P A : reflect (∃ x, A = [set x ]) (#|A | == 1).
+ +
+Lemma subset1 A x : (A \subset [set x ]) = (A == [set x ]) || (A == set0 ).
+ +
+Lemma powerset1 x : powerset [set x ] = [set set0 ; [set x ]].
+ +
+Lemma setIidPl A B : reflect (A :&: B = A) (A \subset B).
+ +
+Lemma setIidPr A B : reflect (A :&: B = B) (B \subset A).
+ +
+Lemma cardsDS A B : B \subset A → #|A :\: B | = (#|A | - #|B |)%N.
+ +
+Lemma setUidPl A B : reflect (A :|: B = A) (B \subset A).
+ +
+Lemma setUidPr A B : reflect (A :|: B = B) (A \subset B).
+ +
+Lemma setDidPl A B : reflect (A :\: B = A) [disjoint A & B ].
+ +
+Lemma subIset A B C : (B \subset A ) || (C \subset A ) → (B :&: C \subset A ).
+ +
+Lemma subsetI A B C : (A \subset B :&: C ) = (A \subset B ) && (A \subset C ).
+ +
+Lemma subsetIP A B C : reflect (A \subset B ∧ A \subset C) (A \subset B :&: C).
+ +
+Lemma subsetIidl A B : (A \subset A :&: B ) = (A \subset B ).
+ +
+Lemma subsetIidr A B : (B \subset A :&: B ) = (B \subset A ).
+ +
+Lemma powersetI A B : powerset (A :&: B) = powerset A :&: powerset B.
+ +
+Lemma subUset A B C : (B :|: C \subset A ) = (B \subset A ) && (C \subset A ).
+ +
+Lemma subsetU A B C : (A \subset B ) || (A \subset C ) → A \subset B :|: C.
+ +
+Lemma subUsetP A B C : reflect (A \subset C ∧ B \subset C) (A :|: B \subset C).
+ +
+Lemma subsetC A B : (A \subset ~: B ) = (B \subset ~: A ).
+ +
+Lemma subCset A B : (~: A \subset B ) = (~: B \subset A ).
+ +
+Lemma subsetD A B C : (A \subset B :\: C ) = (A \subset B ) && [disjoint A & C ].
+ +
+Lemma subDset A B C : (A :\: B \subset C ) = (A \subset B :|: C ).
+ +
+Lemma subsetDP A B C :
+  reflect (A \subset B ∧ [disjoint A & C ]) (A \subset B :\: C).
+ +
+Lemma setU_eq0 A B : (A :|: B == set0 ) = (A == set0 ) && (B == set0 ).
+ +
+Lemma setD_eq0 A B : (A :\: B == set0 ) = (A \subset B ).
+ +
+Lemma setI_eq0 A B : (A :&: B == set0 ) = [disjoint A & B ].
+ +
+Lemma disjoint_setI0 A B : [disjoint A & B ] → A :&: B = set0.
+ +
+Lemma subsetD1 A B x : (A \subset B :\ x ) = (A \subset B ) && (x \notin A ).
+ +
+Lemma subsetD1P A B x : reflect (A \subset B ∧ x \notin A) (A \subset B :\ x).
+ +
+Lemma properD1 A x : x \in A → A :\ x \proper A.
+ +
+Lemma properIr A B : ~~ (B \subset A ) → A :&: B \proper B.
+ +
+Lemma properIl A B : ~~ (A \subset B ) → A :&: B \proper A.
+ +
+Lemma properUr A B : ~~ (A \subset B ) → B \proper A :|: B.
+ +
+Lemma properUl A B : ~~ (B \subset A ) → A \proper A :|: B.
+ +
+Lemma proper1set A x : ([set x ] \proper A ) → (x \in A ).
+ +
+Lemma properIset A B C : (B \proper A ) || (C \proper A ) → (B :&: C \proper A ).
+ +
+Lemma properI A B C : (A \proper B :&: C ) → (A \proper B ) && (A \proper C ).
+ +
+Lemma properU A B C : (B :|: C \proper A ) → (B \proper A ) && (C \proper A ).
+ +
+Lemma properD A B C : (A \proper B :\: C ) → (A \proper B ) && [disjoint A & C ].
+ +
+End setOps.
+ +
+Hint Resolve subsetT_hint.
+ +
+Section setOpsAlgebra.
+ +
+Import Monoid.
+ +
+Variable T : finType.
+ +
+Canonical setI_monoid := Law (@setIA T) (@setTI T) (@setIT T).
+ +
+Canonical setI_comoid := ComLaw (@setIC T).
+Canonical setI_muloid := MulLaw (@set0I T) (@setI0 T).
+ +
+Canonical setU_monoid := Law (@setUA T) (@set0U T) (@setU0 T).
+Canonical setU_comoid := ComLaw (@setUC T).
+Canonical setU_muloid := MulLaw (@setTU T) (@setUT T).
+ +
+Canonical setI_addoid := AddLaw (@setUIl T) (@setUIr T).
+Canonical 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 x1 x2 : ((x1 , x2 ) \in setX ) = (x1 \in A1 ) && (x2 \in A2 ).
+ +
+Lemma setXP x1 x2 : reflect (x1 \in A1 ∧ x2 \in A2) ((x1 , x2 ) \in setX).
+ +
+Lemma cardsX : #|setX | = #|A1 | × #|A2 |.
+ +
+End CartesianProd.
+ +
+ +
+ +
+Module Type ImsetSig.
+Parameter imset : ∀ aT rT : finType,
+ (aT → rT ) → mem_pred aT → {set rT }.
+Parameter imset2 : ∀ 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 imset_unlock := Unlockable Imset.imsetE.
+Canonical 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: A" := (preimset f (mem A)) (at level 24) : set_scope.
+Notation "f @: A" := (imset f (mem A)) (at level 24) : set_scope.
+Notation "f @2: ( A , B )" := (imset2 f (mem A) (fun _ ⇒ mem B))
+  (at level 24, format "f @2: ( A , B )") : set_scope.
+ +
+

+ +

+ Comprehensions +

+Notation "[ 'set' E | x 'in' A ]" := ((fun x ⇒ E) @: A)
+  (at level 0, E, x at level 99,
+   format "[ '[hv' 'set' E '/ ' | x 'in' A ] ']'") : set_scope.
+Notation "[ 'set' E | x 'in' A & P ]" := [set E | x in [set x in A | P]]
+ (at level 0, E, x at level 99,
+   format "[ '[hv' 'set' E '/ ' | x 'in' A '/ ' & P ] ']'") : set_scope.
+Notation "[ 'set' E | x 'in' A , y 'in' B ]" :=
+  (imset2 (fun x y ⇒ E) (mem A) (fun x ⇒ (mem B)))
+  (at level 0, E, x, y at level 99, format
+   "[ '[hv' 'set' E '/ ' | x 'in' A , '/ ' y 'in' B ] ']'"
+  ) : set_scope.
+Notation "[ 'set' E | x 'in' A , y 'in' B & P ]" :=
+  [set E | x in A, y in [set y in B | P]]
+ (at level 0, E, x, y at level 99, format
+   "[ '[hv' 'set' E '/ ' | x 'in' A , '/ ' y 'in' B '/ ' & P ] ']'"
+  ) : set_scope.
+ +
+

+ +

+ Typed variants. +

+Notation "[ 'set' E | x : T 'in' A ]" := ((fun x : T ⇒ E) @: A)
+  (at level 0, E, x at level 99, only parsing) : set_scope.
+Notation "[ 'set' E | x : T 'in' A & P ]" :=
+  [set E | x : T in [set x : T in A | P]]
+ (at level 0, E, x at level 99, only parsing) : set_scope.
+Notation "[ 'set' E | x : T 'in' A , y : U 'in' B ]" :=
+  (imset2 (fun (x : T) (y : U) ⇒ E) (mem A) (fun (x : T) ⇒ (mem B)))
+  (at level 0, E, x, y at level 99, only parsing) : set_scope.
+Notation "[ 'set' E | x : T 'in' A , y : U 'in' B & P ]" :=
+  [set E | x : T in A, y : U in [set y : U in B | P]]
+ (at level 0, E, x, y at level 99, only parsing) : set_scope.
+ +
+

+ +

+ Comprehensions over a type. +

+Notation "[ 'set' E | x : T ]" := [set E | x : T in predOfType T]
+  (at level 0, E, x at level 99,
+   format "[ '[hv' 'set' E '/ ' | x : T ] ']'") : set_scope.
+Notation "[ 'set' E | x : T & P ]" := [set E | x : T in [set x : T | P]]
+ (at level 0, E, x at level 99,
+   format "[ '[hv' 'set' E '/ ' | x : T '/ ' & P ] ']'") : set_scope.
+Notation "[ 'set' E | x : T , y : U 'in' B ]" :=
+  [set E | x : T in predOfType T, y : U in B]
+  (at level 0, E, x, y at level 99, format
+   "[ '[hv' 'set' E '/ ' | x : T , '/ ' y : U 'in' B ] ']'")
+   : set_scope.
+Notation "[ 'set' E | x : T , y : U 'in' B & P ]" :=
+  [set E | x : T, y : U in [set y in B | P]]
+ (at level 0, E, x, y at level 99, format
+ "[ '[hv ' 'set' E '/' | x : T , '/ ' y : U 'in' B '/' & P ] ']'"
+  ) : set_scope.
+Notation "[ 'set' E | x : T 'in' A , y : U ]" :=
+  [set E | x : T in A, y : U in predOfType U]
+  (at level 0, E, x, y at level 99, format
+   "[ '[hv' 'set' E '/ ' | x : T 'in' A , '/ ' y : U ] ']'")
+   : set_scope.
+Notation "[ 'set' E | x : T 'in' A , y : U & P ]" :=
+  [set E | x : T in A, y : U in [set y in P]]
+ (at level 0, E, x, y at level 99, format
+   "[ '[hv' 'set' E '/ ' | x : T 'in' A , '/ ' y : U & P ] ']'")
+   : set_scope.
+Notation "[ 'set' E | x : T , y : U ]" :=
+  [set E | x : T, y : U in predOfType U]
+  (at level 0, E, x, y at level 99, format
+   "[ '[hv' 'set' E '/ ' | x : T , '/ ' y : U ] ']'")
+   : set_scope.
+Notation "[ 'set' E | x : T , y : U & P ]" :=
+  [set E | x : T, y : U in [set y in P]]
+ (at level 0, E, x, y at level 99, format
+   "[ '[hv' 'set' E '/ ' | x : T , '/ ' y : U & P ] ']'")
+   : set_scope.
+ +
+

+ +

+ Untyped variants. +

+Notation "[ 'set' E | x , y 'in' B ]" := [set E | x : _, y : _ in B]
+  (at level 0, E, x, y at level 99, only parsing) : set_scope.
+Notation "[ 'set' E | x , y 'in' B & P ]" := [set E | x : _, y : _ in B & P]
+  (at level 0, E, x, y at level 99, only parsing) : set_scope.
+Notation "[ 'set' E | x 'in' A , y ]" := [set E | x : _ in A, y : _]
+  (at level 0, E, x, y at level 99, only parsing) : set_scope.
+Notation "[ 'set' E | x 'in' A , y & P ]" := [set E | x : _ in A, y : _ & P]
+  (at level 0, E, x, y at level 99, only parsing) : set_scope.
+Notation "[ 'set' E | x , y ]" := [set E | x : _, y : _]
+  (at level 0, E, x, y at level 99, only parsing) : set_scope.
+Notation "[ 'set' E | x , y & P ]" := [set E | x : _, y : _ & P ]
+  (at level 0, E, x, y at level 99, only parsing) : set_scope.
+ +
+

+ +

+ Print-only variants to work around the Coq pretty-printer K-term kink. +

+Notation "[ 'se' 't' E | x 'in' A , y 'in' B ]" :=
+  (imset2 (fun x y ⇒ E) (mem A) (fun _ ⇒ mem B))
+  (at level 0, E, x, y at level 99, format
+   "[ '[hv' 'se' 't' E '/ ' | x 'in' A , '/ ' y 'in' B ] ']'")
+   : set_scope.
+Notation "[ 'se' 't' E | x 'in' A , y 'in' B & P ]" :=
+  [se t E | x in A, y in [set y in B | P]]
+ (at level 0, E, x, y at level 99, format
+ "[ '[hv ' 'se' 't' E '/' | x 'in' A , '/ ' y 'in' B '/' & P ] ']'"
+  ) : set_scope.
+Notation "[ 'se' 't' E | x : T , y : U 'in' B ]" :=
+  (imset2 (fun x (y : U) ⇒ E) (mem (predOfType T)) (fun _ ⇒ mem B))
+  (at level 0, E, x, y at level 99, format
+   "[ '[hv ' 'se' 't' E '/' | x : T , '/ ' y : U 'in' B ] ']'")
+   : set_scope.
+Notation "[ 'se' 't' E | x : T , y : U 'in' B & P ]" :=
+  [se t E | x : T, y : U in [set y in B | P]]
+ (at level 0, E, x, y at level 99, format
+"[ '[hv ' 'se' 't' E '/' | x : T , '/ ' y : U 'in' B '/' & P ] ']'"
+  ) : set_scope.
+Notation "[ 'se' 't' E | x : T 'in' A , y : U ]" :=
+  (imset2 (fun x y ⇒ E) (mem A) (fun _ : T ⇒ mem (predOfType U)))
+  (at level 0, E, x, y at level 99, format
+   "[ '[hv' 'se' 't' E '/ ' | x : T 'in' A , '/ ' y : U ] ']'")
+   : set_scope.
+Notation "[ 'se' 't' E | x : T 'in' A , y : U & P ]" :=
+  (imset2 (fun x (y : U) ⇒ E) (mem A) (fun _ : T ⇒ mem [set y \in P]))
+  (at level 0, E, x, y at level 99, format
+"[ '[hv ' 'se' 't' E '/' | x : T 'in' A , '/ ' y : U '/' & P ] ']'"
+  ) : set_scope.
+Notation "[ 'se' 't' E | x : T , y : U ]" :=
+  [se t E | x : T, y : U in predOfType U]
+  (at level 0, E, x, y at level 99, format
+   "[ '[hv' 'se' 't' E '/ ' | x : T , '/ ' y : U ] ']'")
+   : set_scope.
+Notation "[ 'se' 't' E | x : T , y : U & P ]" :=
+  [se t E | x : T, y : U in [set y in P]]
+ (at level 0, E, x, y at level 99, format
+   "[ '[hv' 'se' 't' E '/' | x : T , '/ ' y : U '/' & 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 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 D1 D2 y : reflect (imset2_spec D1 D2 y) (y \in imset2 f2 D1 D2).
+ +
+Lemma mem_imset (D : pred aT) x : x \in D → f x \in f @: D.
+ +
+Lemma imset0 : f @: set0 = set0.
+ +
+Lemma imset_eq0 (A : {set aT }) : (f @: A == set0 ) = (A == set0 ).
+ +
+Lemma imset_set1 x : f @: [set x ] = [set f x ].
+ +
+Lemma mem_imset2 (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 sub_imset_pre (A : pred aT) (B : pred rT) :
+  (f @: A \subset B ) = (A \subset f @^-1: B ).
+ +
+Lemma preimsetS (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 (A B : {set rT }) :
+  f @^-1: (A :&: B ) = (f @^-1: A ) :&: (f @^-1: B ).
+ +
+Lemma preimsetU (A B : {set rT }) :
+  f @^-1: (A :|: B ) = (f @^-1: A ) :|: (f @^-1: B ).
+ +
+Lemma preimsetD (A B : {set rT }) :
+  f @^-1: (A :\: B ) = (f @^-1: A ) :\: (f @^-1: B ).
+ +
+Lemma preimsetC (A : {set rT }) : f @^-1: (~: A ) = ~: f @^-1: A.
+ +
+Lemma imsetS (A B : pred aT) : A \subset B → f @: A \subset f @: B.
+ +
+Lemma imset_proper (A B : {set aT }) :
+   {in B &, injective f } → A \proper B → f @: A \proper f @: B.
+ +
+Lemma preimset_proper (A B : {set rT }) :
+  B \subset codom f → A \proper B → (f @^-1: A ) \proper (f @^-1: B ).
+ +
+Lemma imsetU (A B : {set aT }) : f @: (A :|: B ) = (f @: A ) :|: (f @: B ).
+ +
+Lemma imsetU1 a (A : {set aT }) : f @: (a |: A ) = f a |: (f @: A ).
+ +
+Lemma imsetI (A B : {set aT }) :
+  {in A & B , injective f } → f @: (A :&: B ) = f @: A :&: f @: B.
+ +
+Lemma imset2Sl (A B : pred aT) (C : pred aT2) :
+  A \subset B → f2 @2: (A , C ) \subset f2 @2: (B , C ).
+ +
+Lemma imset2Sr (A B : pred aT2) (C : pred aT) :
+  A \subset B → f2 @2: (C , A ) \subset f2 @2: (C , B ).
+ +
+Lemma imset2S (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.
+ +
+Implicit Types (f g : aT → rT) (D : {set aT }) (R : pred rT).
+ +
+Lemma eq_preimset f g R : f =1 g → f @^-1: R = g @^-1: R.
+ +
+Lemma eq_imset f g D : f =1 g → f @: D = g @: D.
+ +
+Lemma eq_in_imset f g D : {in D , f =1 g } → f @: D = g @: D.
+ +
+Lemma eq_in_imset2 (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 (A : {set aT }) (B : {set aT2 }) :
+  [set (x , y ) | x in A , y in B ] = setX A B.
+ +
+Lemma setXS (A1 B1 : {set aT }) (A2 B2 : {set aT2 }) :
+  A1 \subset B1 → A2 \subset B2 → setX A1 A2 \subset setX B1 B2.
+ +
+End FunImage.
+ +
+ +
+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 F : \big [op /idx ]_(i in set0 ) F i = idx.
+ +
+Lemma big_set1 a F : \big [op /idx ]_(i in [set a ]) F i = F a.
+ +
+Lemma big_setIDdep 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_setID A B F :
+  \big [aop /idx ]_(i in A ) F i =
+     aop (\big [aop /idx ]_(i in A :&: B ) F i)
+         (\big [aop /idx ]_(i in A :\: B ) F i).
+ +
+Lemma big_setD1 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 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 h (A : pred I) 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 h (A : pred I) 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.
+ +
+ +
+Section Fun2Set1.
+ +
+Variables aT1 aT2 rT : finType.
+Variables (f : aT1 → aT2 → rT).
+ +
+Lemma imset2_set1l x1 (D2 : pred aT2) : f @2: ([set x1 ], D2 ) = f x1 @: D2.
+ +
+Lemma imset2_set1r 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 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 imset_injP : reflect {in D &, 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 (aT rT : finType) (f : aT → rT) (R : pred rT) :
+  {on R , bijective f } → #|f @^-1: R | = #|R |.
+ +
+Lemma can_imset_pre (T : finType) f g (A : {set T }) :
+  cancel f g → f @: A = g @^-1: A :> {set T }.
+ +
+Lemma imset_id (T : finType) (A : {set T }) : [set x | x in A ] = A.
+ +
+Lemma card_preimset (T : finType) (f : T → T) (A : {set T }) :
+  injective f → #|f @^-1: A | = #|A |.
+ +
+Lemma card_powerset (T : finType) (A : {set T }) : #|powerset A | = 2 ^ #|A |.
+ +
+Section FunImageComp.
+ +
+Variables T T' U : finType.
+ +
+Lemma imset_comp (f : T' → U) (g : T → T') (H : pred T) :
+  (f \o g ) @: H = f @: (g @: H ).
+ +
+End FunImageComp.
+ +
+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.
+ +
+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 Types (U : pred T) (P : pred I) (A B : {set I }) (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 j P F : P j → F j \subset \bigcup_(i | P i ) F i.
+ +
+Lemma bigcup_max j U P F :
+  P j → U \subset F j → U \subset \bigcup_(i | P i ) F i.
+ +
+Lemma bigcupP x P F :
+  reflect (exists2 i, P i & x \in F i) (x \in \bigcup_(i | P i ) F i).
+ +
+Lemma bigcupsP U P F :
+  reflect (∀ i, P i → F i \subset U) (\bigcup_(i | P i ) F i \subset U).
+ +
+Lemma bigcup_disjoint U P F :
+  (∀ i, P i → [disjoint U & F i ]) → [disjoint U & \bigcup_(i | P i ) F i ].
+ +
+Lemma bigcup_setU 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 r F : \bigcup_(i <- r ) F i = \bigcup_(i in r ) F i.
+ +
+

+ +

+ Unlike its setU counterpart, this lemma is useable. +

+ +

+ + 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 := [∀ (B : sT | B \subset A ), (B == A ) == P B ].
+ +
+Lemma minset_eq P1 P2 A : P1 =1 P2 → minset P1 A = minset P2 A.
+ +
+Lemma minsetP P A :
+ reflect ((P A ) ∧ (∀ B, P B → B \subset A → B = A )) (minset P A).
+ +
+Lemma minsetp P A : minset P A → P A.
+ +
+Lemma minsetinf P A B : minset P A → P B → B \subset A → B = A.
+ +
+Lemma ex_minset P : (∃ A, P A ) → {A | minset P A }.
+ +
+Lemma minset_exists P C : P C → {A | minset P A & A \subset C }.
+ +
+

+ +

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

+Fact maxset_key : unit.
+Definition maxset P A :=
+ minset (fun B ⇒ locked_with maxset_key P (~: B)) (~: A).
+ +
+Lemma maxset_eq P1 P2 A : P1 =1 P2 → maxset P1 A = maxset P2 A.
+ +
+Lemma maxminset P A : maxset P A = minset [pred B | P (~: B)] (~: A).
+ +
+Lemma minmaxset P A : minset P A = maxset [pred B | P (~: B)] (~: A).
+ +
+Lemma maxsetP P A :
+ reflect ((P A ) ∧ (∀ B, P B → A \subset B → B = A )) (maxset P A).
+ +
+Lemma maxsetp P A : maxset P A → P A.
+ +
+Lemma maxsetsup P A B : maxset P A → P B → A \subset B → B = A.
+ +
+Lemma ex_maxset P : (∃ A, P A ) → {A | maxset P A }.
+ +
+Lemma maxset_exists P C : P C → {A : sT | maxset P A & C \subset A }.
+ +
+End MaxSetMinSet.
+ +
+ +
+