Library mathcomp.ssreflect.finset

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.

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.

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.

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.

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

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

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

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

distribute /cancel

complement

difference

powerset

cardinal lemmas for sets

other inclusions