- -

Library mathcomp.ssreflect.finset

- -

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

- -

- 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 := @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 : {A = B } + {A != B }.
- -
-Lemma eq_finset (pA pB : pred T) : pA =1 pB → finset pA = finset pB.
- -
-End BasicSetTheory.
- -
-Definition inE := (in_set , inE ).
- -
-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 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_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_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 ).
- -
-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 : 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.
- -
- -
- -
-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).
- -
-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 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_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.
- -
- -
-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.
- -
-