Library mathcomp.ssreflect.finset

(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.                  
 Distributed under the terms of CeCILL-B.                                  *)
From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat div seq.
From mathcomp Require Import choice fintype finfun bigop.

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 transversal 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 true. [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. Provided a monotonous function F : {set T} -> {set T}, we get fixpoints fixset F := iter #|T| F set0 == the least fixpoint of F == the minimal set such that F X == X fix_order F x == the minimum number of iterations so that x is in iter (fix_order F x) F set0 funsetC F := fun X => ~: F (~: X) cofixset F == the greatest fixpoint of F == the maximal set such that F X == X := ~: fixset (funsetC F) 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 trailing `r' to distinguish a right-hand complement from commutativity, e.g., setIC : A :&: B = B :&: A and setICr : A :&: ~: A = set0.

Set Implicit Arguments.

Declare Scope set_scope.

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.
Bind Scope set_scope with set_type.
Bind Scope set_scope with set_of.
Open Scope set_scope.
Arguments finfun_of_set {T} A%SET.

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 obstructive.
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.

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

Local Notation pred_of_set_def := (fun T (A : set_type T) ⇒ val A : _ → _).

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.

Set spanned by a sequence.
Notation "[ 'set' :: s ]" := (finset [in pred_of_seq s])
  (at level 0, format "[ 'set' :: s ]") : 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 := @PredType _ (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 : eq_xor_neq A B (B == A) (A == B).

Lemma eq_finset (pA pB : pred T) : pA =1 pB → finset pA = finset pB.

End BasicSetTheory.

Arguments eqsVneq {T} A B, {T A B}.

Definition inE := (in_set, inE).

Arguments set0 {T}.
Arguments eq_finset {T} [pA] pB eq_pAB.
#[global] Hint Resolve in_setT : core.

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 set_enum A : [set:: enum A] = 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 : core.

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_nil : [set:: nil] = @set0 T.

Lemma set_seq1 a : [set:: [:: a]] = [set a].

Lemma set_cons a s : [set:: a :: s] = a |: [set:: 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

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

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

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

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

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

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

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

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

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.

Lemma properC A B : (~: B \proper ~: A) = (A \proper B).

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_cond_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).

Variant cards_eq_spec A : seq T → {set T} → nat → Type :=
| CardEq (s : seq T) & uniq s : cards_eq_spec A s [set x | x \in s] (size s).

Lemma cards_eqP A : cards_eq_spec A (enum A) A #|A|.

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

Lemma cards2P A : reflect (∃ x y : T, x != y ∧ A = [set x; y])
                          (#|A| == 2).

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).
Arguments setIidPl {A 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 disjoints1 A x : [disjoint [set x] & A] = (x \notin A).

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].

Lemma properCr A B : (A \proper ~: B) = (B \proper ~: A).

Lemma properCl A B : (~: A \proper B) = (~: B \proper A).

End setOps.

Arguments set1P {T x a}.
Arguments set1_inj {T} [x1 x2].
Arguments set2P {T x a b}.
Arguments setIdP {T x pA pB}.
Arguments setIP {T x A B}.
Arguments setU1P {T x a B}.
Arguments setD1P {T x A b}.
Arguments setUP {T x A B}.
Arguments setDP {T A B x}.
Arguments cards1P {T A}.
Arguments setCP {T x A}.
Arguments setIidPl {T A B}.
Arguments setIidPr {T A B}.
Arguments setUidPl {T A B}.
Arguments setUidPr {T A B}.
Arguments setDidPl {T A B}.
Arguments subsetIP {T A B C}.
Arguments subUsetP {T A B C}.
Arguments subsetDP {T A B C}.
Arguments subsetD1P {T A B x}.
#[global] Hint Resolve subsetT_hint : core.

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.

Arguments setXP {fT1 fT2 A1 A2 x1 x2}.

Local Notation imset_def :=
  (fun (aT rT : finType) f mD ⇒ [set y in @image_mem aT rT f mD]).
Local Notation imset2_def :=
  (fun (aT1 aT2 rT : finType) f (D1 : mem_pred aT1) (D2 : _ → mem_pred aT2) ⇒
     [set y : rT in [seq uncurry f u | u in [pred u | D1 u.1 & D2 u.1 u.2]]]).

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 pred_of_set [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 pred_of_set [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.
Local Notation predOfType T := (pred_of_simpl (@pred_of_argType T)).
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 pred_of_set [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 pred_of_set [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 pred_of_set [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 pred_of_set [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.

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).

Variant 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 imset_f (D : {pred aT}) x : x \in D → f x \in f @: D.

Lemma mem_imset (D : {pred aT}) x : injective f → f x \in f @: D = (x \in 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 imset_inj : injective f → injective (fun A : {set aT} ⇒ f @: A).

Lemma imset_disjoint (A B : {pred aT}) :
  injective f → [disjoint f @: A & f @: B] = [disjoint A & B].

Lemma imset2_f (D : {pred aT}) (D2 : aT → {pred aT2}) x x2 :
    x \in D → x2 \in D2 x →
  f2 x x2 \in [set f2 y y2 | y in D, y2 in D2 y].

Lemma mem_imset2 (D : {pred aT}) (D2 : aT → {pred aT2}) x x2 :
    injective2 f2 →
  (f2 x x2 \in [set f2 y y2 | y in D, y2 in D2 y])
    = (x \in D) && (x2 \in D2 x).

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 : {pred 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.

Arguments imsetP {aT rT f D y}.
Arguments imset2P {aT aT2 rT f2 D1 D2 y}.
Arguments imset_disjoint {aT rT f A B}.

Section BigOpsSemiGroup.

Variables (R : Type) (op : R → R → R).
Hypotheses (opA : associative op) (opC : commutative op).

Variable (le : rel R).
Hypotheses (le_refl : reflexive le) (le_incr : ∀ x y, le x (op x y)).

Context [x : R].

Lemma subset_le_big_cond (I : finType) (A A' P P' : {pred I}) (F : I → R) :
    [set i in A | P i] \subset [set i in A' | P' i] →
  le (\big[op/x]_(i in A | P i) F i) (\big[op/x]_(i in A' | P' i) F i).

End BigOpsSemiGroup.

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_set (A : pred I) F :
   \big[op/idx]_(i in [set i | A i]) (F i) = \big[op/idx]_(i in A) (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_setIDcond 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 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 big_imset_cond h (A : {pred I}) (P : pred J) G : {in A &, injective h} →
  \big[aop/idx]_(j in h @: A | P j) G j =
    \big[aop/idx]_(i in A | P (h i)) 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.

Lemma bigA_distr (R : Type) (zero one : R) (mul : Monoid.mul_law zero)
  (add : Monoid.add_law zero mul) (I : finType) (F G : I → R) :
  \big[mul/one]_i add (F i) (G i) =
  \big[add/zero]_(J in {set I}) \big[mul/one]_i (if i \in J then F i else G i).

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

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.

Arguments imset_injP {aT rT f D}.

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 bigcup0P P F :
  reflect (∀ i, P i → F i = set0) (\bigcup_(i | P i) F i == set0).

Lemma bigcup_disjointP U P F :
  reflect (∀ i : I, P i → [disjoint U & F i])
          [disjoint U & \bigcup_(i | P i) F i].

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.
Lemma bigcap_inf j P F : P j → \bigcap_(i | P i) F i \subset F j.

Lemma bigcap_min j U P F :
  P j → F j \subset U → \bigcap_(i | P i) F i \subset U.

Lemma bigcapsP U P F :
  reflect (∀ i, P i → U \subset F i) (U \subset \bigcap_(i | P i) F i).

Lemma bigcapP x P F :
  reflect (∀ i, P i → x \in F i) (x \in \bigcap_(i | P i) F i).

Lemma setC_bigcup J r (P : pred J) (F : J → {set T}) :
  ~: (\bigcup_(j <- r | P j) F j) = \bigcap_(j <- r | P j) ~: F j.

Lemma setC_bigcap J r (P : pred J) (F : J → {set T}) :
  ~: (\bigcap_(j <- r | P j) F j) = \bigcup_(j <- r | P j) ~: F j.

Lemma bigcap_setU 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 r F : \bigcap_(i <- r) F i = \bigcap_(i in r) F i.

End BigSetOps.

Arguments bigcup_sup [T I] j [P F].
Arguments bigcup_max [T I] j [U P F].
Arguments bigcupP {T I x P F}.
Arguments bigcupsP {T I U P F}.
Arguments bigcup_disjointP {T I U P F}.
Arguments bigcap_inf [T I] j [P F].
Arguments bigcap_min [T I] j [U P F].
Arguments bigcapP {T I x P F}.
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) = uncurry 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 (A B : {set aT1}) (C : {set aT2}) :
  f @2: (A :|: B, C) = f @2: (A, C) :|: f @2: (B, C).

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

End ImsetCurry.

Section Partitions.

Variables T I : finType.
Implicit Types (x y z : T) (A B D X : {set T}) (P Q : {set {set T}}).
Implicit Types (J : pred I) (F : I → {set T}).

Definition cover P := \bigcup_(B in P) B.
Definition pblock P x := odflt set0 (pick [pred B in P | x \in B]).
Definition trivIset P := \sum_(B in P) #|B| == #|cover P|.
Definition partition P D := [&& cover P == D, trivIset P & set0 \notin P].

Definition is_transversal X P D :=
  [&& partition P D, X \subset D & [∀ B in P, #|X :&: B| == 1]].
Definition transversal P D := [set odflt x [pick y in pblock P x] | x in D].
Definition transversal_repr x0 X B := odflt x0 [pick x in X :&: B].

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

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

Lemma imset_cover (T' : finType) P (f : T → T') :
  [set f x | x in cover P] = \bigcup_(i in P) [set f x | x in i].

Lemma cover1 A : cover [set A] = A.

Lemma trivIset1 A : trivIset [set A].

Lemma trivIsetP P :
  reflect {in P &, ∀ A B, A != B → [disjoint A & B]} (trivIset P).

Lemma trivIsetS P Q : P \subset Q → trivIset Q → trivIset P.

Lemma trivIsetD P Q : trivIset P → trivIset (P :\: Q).

Lemma trivIsetU P Q :
  trivIset Q → trivIset P → [disjoint cover Q & cover P] → trivIset (Q :|: P).

Lemma coverD1 P B : trivIset P → B \in P → cover (P :\ B) = cover P :\: B.

Lemma trivIsetI P D : trivIset P → trivIset (P ::&: D).

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

Lemma mem_pblock P x : (x \in pblock P x) = (x \in cover P).

Lemma pblock_mem P x : x \in cover P → pblock P x \in P.

Lemma def_pblock P B x : trivIset P → B \in P → x \in B → pblock P x = B.

Lemma same_pblock P x y :
  trivIset P → x \in pblock P y → pblock P x = pblock P y.

Lemma eq_pblock P x y :
    trivIset P → x \in cover P →
  (pblock P x == pblock P y) = (y \in pblock P x).

Lemma trivIsetU1 A P :
    {in P, ∀ B, [disjoint A & B]} → trivIset P → set0 \notin P →
  trivIset (A |: P) ∧ A \notin P.

Lemma cover_imset J F : cover (F @: J) = \bigcup_(i in J) F i.

Lemma trivIimset J F (P := F @: J) :
    {in J &, ∀ i j, j != i → [disjoint F i & F j]} → set0 \notin P →
  trivIset P ∧ {in J &, injective F}.

Lemma cover_partition P D : partition P D → cover P = D.

Lemma partition0 P D : partition P D → set0 \in P = false.

Lemma partition_neq0 P D B : partition P D → B \in P → B != set0.

Lemma partition_trivIset P D : partition P D → trivIset P.

Lemma partitionS P D B : partition P D → B \in P → B \subset D.

Lemma partitionD1 P D B :
  partition P D → B \in P → partition (P :\ B) (D :\: B).

Lemma partitionU1 P D B :
  partition P D → B != set0 → [disjoint B & D] → partition (B |: P) (B :|: D).

Lemma partition_set0 P : partition P set0 = (P == set0).

Lemma card_partition P D : partition P D → #|D| = \sum_(A in P) #|A|.

Lemma card_uniform_partition n P D :
  {in P, ∀ A, #|A| = n} → partition P D → #|D| = #|P| × n.

Lemma partition_pigeonhole P D A :
  partition P D → #|P| ≤ #|A| → A \subset D → {in P, ∀ B, #|A :&: B| ≤ 1} →
  {in P, ∀ B, A :&: B != set0}.

Section BigOps.

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

Lemma big_trivIset_cond P (K : pred T) (E : T → R) :
  trivIset P → \big[op/idx]_(x in cover P | K x) E x = rhs_cond P K E.

Lemma big_trivIset P (E : T → R) :
  trivIset P → \big[op/idx]_(x in cover P) E x = rhs P E.

Lemma set_partition_big_cond P D (K : pred T) (E : T → R) :
  partition P D → \big[op/idx]_(x in D | K x) E x = rhs_cond P K E.

Lemma set_partition_big P D (E : T → R) :
  partition P D → \big[op/idx]_(x in D) E x = rhs P E.

Lemma partition_disjoint_bigcup (F : I → {set T}) E :
    (∀ i j, i != j → [disjoint F i & F j]) →
  \big[op/idx]_(x in \bigcup_i F i) E x =
    \big[op/idx]_i \big[op/idx]_(x in F i) E x.

End BigOps.

Section Equivalence.

Variables (R : rel T) (D : {set T}).

Let Px x := [set y in D | R x y].
Definition equivalence_partition := [set Px x | x in D].
Local Notation P := equivalence_partition.
Hypothesis eqiR : {in D & &, equivalence_rel R}.

Let Pxx x : x \in D → x \in Px x.
Let PPx x : x \in D → Px x \in P := fun Dx ⇒ imset_f _ Dx.

Lemma equivalence_partitionP : partition P D.

Lemma pblock_equivalence_partition :
  {in D &, ∀ x y, (y \in pblock P x) = R x y}.

End Equivalence.

Lemma pblock_equivalence P D :
  partition P D → {in D & &, equivalence_rel (fun x y ⇒ y \in pblock P x)}.

Lemma equivalence_partition_pblock P D :
  partition P D → equivalence_partition (fun x y ⇒ y \in pblock P x) D = P.

Section Preim.

Variables (rT : eqType) (f : T → rT).

Definition preim_partition := equivalence_partition (fun x y ⇒ f x == f y).

Lemma preim_partitionP D : partition (preim_partition D) D.

End Preim.

Lemma preim_partition_pblock P D :
  partition P D → preim_partition (pblock P) D = P.

Lemma transversalP P D : partition P D → is_transversal (transversal P D) P D.

Section Transversals.

Variables (X : {set T}) (P : {set {set T}}) (D : {set T}).
Hypothesis trPX : is_transversal X P D.

Lemma transversal_sub : X \subset D.

Let tiP : trivIset P.

Let sXP : {subset X ≤ cover P}.

Let trX : {in P, ∀ B, #|X :&: B| == 1}.

Lemma setI_transversal_pblock x0 B :
  B \in P → X :&: B = [set transversal_repr x0 X B].

Lemma repr_mem_pblock x0 B : B \in P → transversal_repr x0 X B \in B.

Lemma repr_mem_transversal x0 B : B \in P → transversal_repr x0 X B \in X.

Lemma transversal_reprK x0 : {in P, cancel (transversal_repr x0 X) (pblock P)}.

Lemma pblockK x0 : {in X, cancel (pblock P) (transversal_repr x0 X)}.

Lemma pblock_inj : {in X &, injective (pblock P)}.

Lemma pblock_transversal : pblock P @: X = P.

Lemma card_transversal : #|X| = #|P|.

Lemma im_transversal_repr x0 : transversal_repr x0 X @: P = X.

End Transversals.

End Partitions.

Arguments trivIsetP {T P}.
Arguments big_trivIset_cond [T R idx op] P [K E].
Arguments set_partition_big_cond [T R idx op] P [D K E].
Arguments big_trivIset [T R idx op] P [E].
Arguments set_partition_big [T R idx op] P [D E].


Lemma partition_partition (T : finType) (D : {set T}) P Q :
    partition P D → partition Q P →
  partition (cover @: Q) D ∧ {in Q &, injective cover}.

Lemma indexed_partition (I T : finType) (J : {pred I}) (B : I → {set T}) :
  let P := [set B i | i in J] in
  {in J &, ∀ i j : I, j != i → [disjoint B i & B j]} →
  (∀ i : I, J i → B i != set0) → partition P (cover P) ∧ {in J &, injective B}.

Section PartitionImage.
Variables (T : finType) (P : {set {set T}}) (D : {set T}).
Variables (T' : finType) (f : T → T') (inj_f : injective f).
Let fP := [set f @: (B : {set T}) | B in P].

Lemma imset_trivIset : trivIset fP = trivIset P.

Lemma imset0mem : (set0 \in fP) = (set0 \in P).

Lemma imset_partition : partition fP (f @: D) = partition P D.
End PartitionImage.

Maximum and minimum (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).
Arguments minsetP {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.

Arguments setCK {T}.
Arguments minsetP {T P A}.
Arguments maxsetP {T P A}.

Section SetFixpoint.

Section Least.
Variables (T : finType) (F : {set T} → {set T}).
Hypothesis (F_mono : {homo F : X Y / X \subset Y}).

Let n := #|T|.
Let iterF i := iter i F set0.

Lemma subset_iterS i : iterF i \subset iterF i.+1.

Lemma subset_iter : {homo iterF : i j / i ≤ j >-> i \subset j}.

Definition fixset := iterF n.

Lemma fixsetK : F fixset = fixset.
Hint Resolve fixsetK : core.

Lemma minset_fix : minset [pred X | F X == X] fixset.

Lemma fixsetKn k : iter k F fixset = fixset.

Lemma iter_sub_fix k : iterF k \subset fixset.

Lemma fix_order_proof x : x \in fixset → ∃ n, x \in iterF n.

Definition fix_order (x : T) :=
 if (x \in fixset) =P true isn't ReflectT x_fix then 0
 else (ex_minn (fix_order_proof x_fix)).

Lemma fix_order_le_max (x : T) : fix_order x ≤ n.

Lemma in_iter_fix_orderE (x : T) :
  (x \in iterF (fix_order x)) = (x \in fixset).

Lemma fix_order_gt0 (x : T) : (fix_order x > 0) = (x \in fixset).

Lemma fix_order_eq0 (x : T) : (fix_order x == 0) = (x \notin fixset).

Lemma in_iter_fixE (x : T) k : (x \in iterF k) = (0 < fix_order x ≤ k).

Lemma in_iter (x : T) k : x \in fixset → fix_order x ≤ k → x \in iterF k.

Lemma notin_iter (x : T) k : k < fix_order x → x \notin iterF k.

Lemma fix_order_small x k : x \in iterF k → fix_order x ≤ k.

Lemma fix_order_big x k : x \in fixset → x \notin iterF k → fix_order x > k.

Lemma le_fix_order (x y : T) : y \in iterF (fix_order x) →
  fix_order y ≤ fix_order x.

End Least.

Section Greatest.
Variables (T : finType) (F : {set T} → {set T}).
Hypothesis (F_mono : {homo F : X Y / X \subset Y}).

Definition funsetC X := ~: (F (~: X)).
Lemma funsetC_mono : {homo funsetC : X Y / X \subset Y}.
Hint Resolve funsetC_mono : core.

Definition cofixset := ~: fixset funsetC.

Lemma cofixsetK : F cofixset = cofixset.

Lemma maxset_cofix : maxset [pred X | F X == X] cofixset.

End Greatest.

End SetFixpoint.