Library libs.fset

Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq finfun fintype choice.
Require Import finset fingraph tuple path bigop.

Require Import edone bcase base.

Finite Sets over choice types and countable types

This file defines a type {fset T} of finite sets over a type T with choice implemented as constructive quotient on duplicate free lists. If T is a countable type, then {fset T}, {fset {fset T}}, etc. also are countable types.

For X,Y : {fset T} and x,y : T we define.

x \in X == x is an element of X (i.e., {fset X} is a predType)

fset0 == the empty set

[fset x] == singleton x

[fset x in X | P] == separation (i.e, the elements of A satisfying P)

[fset f x | x <- X] == replacement (i.e., map)

[fset f x | x <- X,P] == replacement (i.e., map)

[fset x;..;y] == explicit set

[fset x;..;y & X] == x |` (.. (y |` X))

X `|` Y == the union of X and Y

x |` X == [fset x] `|` X

X `&` Y == the intersection of X and Y

\bigcup_(x in X) F == the union of all F x where x ranges over X

powerset X == the poweset of X (of type {fset {fset T}})

X `<=` Y == X is a subset of Y

X `<` Y == X is a proper subset of Y

size X == the cardinality of X (via coercion to seq T)

fsum w X == the sum of the weights of the elements in X (w : T -> nat)

If F : {fset T} -> {fset T} is a monotone function bounded by some set

lfp F == the least fipoint of F

gfp F == the greatest fixpoint of F

We port a large protion of the lemmas from finset.v. Lemmas corresponding to lemmas in finset.v have a 'f' prefixed to their name (or the string 'set') Otherwise we follow a similar naming convention:

0 -- the empty set

1 -- singleton set

I -- intersection

U -- union

D -- difference

S -- subset

Set Implicit Arguments.
Import Prenex Implicits.

We build finite sets over choice types and countable types by chosing a unique, duplicate free list as canonical representative of every set.

Section FinSets.
  Variable T : choiceType.

  Definition fset_axiom (el : seq T) := uniq el && (el == choose (perm_eq el) el ).
  Record fset_type := Fset { elements :> seq T ; _ : fset_axiom elements}.

  Definition fset_of of phant T := fset_type.
  Identity Coercion type_of_fset_of : fset_of >-> fset_type.

  Canonical Structure fset_subType := [subType for elements by fset_type_rect ].
  Canonical Structure fset_eqType := EqType _ [eqMixin of fset_type by <:].
  Canonical Structure fset_predType := mkPredType (fun (X : fset_type) x => nosimpl x \in elements X).
  Canonical Structure fset_choiceType := Eval hnf in ChoiceType _ [choiceMixin of fset_type by <:].
End FinSets.

Additional Canonical Structures in case T is a countType. This allows sets of sets of countTypes

Canonical Structure fset_countType (T : countType) :=
Eval hnf in CountType _ [countMixin of fset_type T by <:].
Canonical Structure fset_subCountType (T : countType) :=
Eval hnf in [subCountType of fset_type T ].

Notation for fsets using Phant to allow the type checker to infer the Caonical Structure for the element type

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

Section Extensionality.
  Variables T : choiceType.

  Lemma fset_eq X Y : X =i Y -> X == Y :> {fset T }.

  Lemma fset_ext X Y : X =i Y -> X = Y :> {fset T }.
End Extensionality.

In conntrast to finite sets over finite types, where sets are constructed from predicates, we contruct sets from seqences by chosing a ducplicate free equivalent.

Section SetOfSeq.
  Variable (T : choiceType).

  Definition fseq (xs : seq T) : seq T :=
    let e := undup xs in choose (perm_eq e) e.

  Lemma fseq_perm_eq xs : perm_eq (undup xs) (fseq xs).

  Lemma fseq_uniq xs : uniq (fseq xs).

  Lemma fseq_axiom (xs : seq T) : fset_axiom (fseq xs).

  Definition set_of xs : {fset T } := Fset (fseq_axiom xs).

  Lemma set_ofE x xs : (x \in set_of xs ) = (x \in xs ).

  Lemma funiq (X : {fset T }) : uniq X.

  Lemma set_of_uniq (s : seq T) : uniq s -> perm_eq (set_of s) s.
End SetOfSeq.
Global Opaque set_of.

Primitive operations

The primitive operations for the construction of sets are separation, union, singleton, emptyset and replacement (imset).

Local Notation sep_def := (fun T X p => @set_of T (filter p (elements X))).
Local Notation fsetU_def := (fun T X Y => @set_of T (elements X ++ elements Y)).
Local Notation fset1_def := (fun T x => @set_of T [:: x ]).
Local Notation fset0_def := (fun T => @set_of T [::]).
Local Notation fimset_def :=
  (fun (aT rT : choiceType) f X => @set_of rT (@map aT rT f (elements X))).
Local Notation fimset2_def := (fun (aT aT' rT : choiceType) f X Y =>
  @set_of rT (@allpairs aT aT' rT f (elements X) (elements Y))).

Module Type FsetType.
  Implicit Types (T aT rT : choiceType).
  Parameter sep : forall T, {fset T } -> pred T -> {fset T }.
  Axiom sepE : sep = sep_def.
  Parameter fsetU : forall T, {fset T } -> {fset T } -> {fset T }.
  Axiom fsetUE : fsetU = fsetU_def.
  Parameter fset0_ : forall T, {fset T }.
  Axiom fset0E : fset0_ = fset0_def.
  Parameter fset1 : forall T, T-> {fset T }.
  Axiom fset1E : fset1 = fset1_def.
  Parameter fimset : forall aT rT, (aT -> rT) -> {fset aT } -> {fset rT }.
  Axiom fimsetE : fimset = fimset_def.
  Parameter fimset2 : forall aT aT' rT, (aT -> aT' -> rT) -> {fset aT } -> {fset aT'} -> {fset rT }.
  Axiom fimset2E : fimset2 = fimset2_def.
End FsetType.

Module Fset : FsetType.
  Implicit Types (T aT rT : choiceType).
  Definition sep := sep_def.
  Lemma sepE : sep = sep_def.
  Definition fsetU := fsetU_def.
  Lemma fsetUE : fsetU = fsetU_def.
  Definition fset0_ := fset0_def.
  Lemma fset0E : @fset0_ = fset0_def.
  Definition fset1 := fset1_def.
  Lemma fset1E : fset1 = fset1_def.
  Definition fimset := fimset_def.
  Lemma fimsetE : fimset = fimset_def.
  Definition fimset2 := fimset2_def.
  Lemma fimset2E : fimset2 = fimset2_def.
End Fset.
Export Fset.

Notations

Notation "[ 'fset' x 'in' X | P ]" := (sep X (fun x => P))
(at level 0, x, X at level 99, format "[ 'fset' x 'in' X | P ]").

Definition fsetI (T : choiceType) (X Y : {fset T }) := [fset x in X | x \in Y ].
Definition fsetD (T : choiceType) (X Y : {fset T }) := [fset x in X | x \notin Y ].
Definition subset (T : choiceType) (X Y : {fset T }) := all (mem Y) X.
Definition proper (T : choiceType) (X Y : {fset T }) := subset X Y && ~~ subset Y X.
Definition fsetX (T T' : choiceType) (X : {fset T }) (Y : {fset T'}) := fimset2 pair X Y.

Notation "X `|` Y" := (fsetU X Y) (at level 52, left associativity).
Notation "X `&` Y" := (fsetI X Y) (at level 48, left associativity).
Notation "X `\` Y" := (fsetD X Y) (at level 48, left associativity).
Notation "X `<=` Y" := (subset X Y) (at level 70 ,no associativity).
Notation "X `<` Y" := (proper X Y) (at level 70, no associativity).
Notation "[ 'fset' x ]" := (fset1 x) (at level 0,x at level 99, format "[ 'fset' x ]" ).
Notation fset0 := (@fset0_ _).
Notation "f `@` X" := (fimset f X) (at level 45).
Notation "x |` X" := ([fset x] `|` X) (at level 52, left associativity).
Notation "X `x` Y" := (fsetX X Y) (at level 44, left associativity).

This is left recursive to avoid having an explicit fset0 at the end

Notation "[ 'fset' x1 ; x2 ; .. ; xn ]" := (fsetU .. (x1 |` [fset x2]) .. [fset xn])
  (at level 0, x1 at level 99, format "[ 'fset' x1 ; x2 ; .. ; xn ]").
Notation "[ 'fset' x1 , x2 , .. , xn & X ]" := (x1 |` (x2 |` .. (xn |` X) ..))
  (at level 0, x1 at level 99, format "[ 'fset' x1 , x2 , .. , xn & X ]").
Notation "[ 'all' x 'in' s , p ]" := (all (fun x => p) s)
  (at level 0, x at level 99, format "[ 'all' x 'in' s , p ]").
Notation "[ 'some' x 'in' s , p ]" := (has (fun x => p) s)
  (at level 0, x at level 99, format "[ 'some' x 'in' s , p ]").

Notation "[ 'fset' E | x <- X ]" := (fimset (fun x => E) X)
  (at level 0, E, x at level 99, format "[ '[hv' 'fset' E '/ ' | x <- X ] ']'").
Notation "[ 'fset' E | a <- A , b <- B ]" :=
  (fimset2 (fun a b => E) A B) (at level 0, E, a, b at level 99).

Definition fimset3 (aT1 aT2 aT3 rT : choiceType) (f : aT1 -> aT2 -> aT3 -> rT) X Y Z :=
  [fset f x y.1 y.2 | x <- X , y <- Y `x ` Z ].

Notation "[ 'fset' E | a <- A , b <- B , c <- C ]" :=
  (fimset3 (fun a b c => E) A B C) (at level 0, E, a, b, c at level 99).

Basic Theory

Section OperationsTheory.
  Variable aT1 aT2 aT3 T T': choiceType.
  Implicit Types X Y Z : {fset T }.
  Implicit Types x y z : T.

  Lemma fset0F : set_of [::] = fset0 :> {fset T }.

  Lemma fset1F x : set_of [:: x ] = [fset x ] :> {fset T }.

For fset0 and fset1 we know the repesentative

  Lemma fset1Es x : [fset x ] = [:: x ] :> seq T.

  Lemma fset0Es : fset0 = [::] :> seq T.

  Lemma in_sep X p x : x \in [fset y in X | p y] = (x \in X ) && (p x ).

  Lemma in_fsetU x X Y : (x \in X `|` Y ) = (x \in X ) || (x \in Y ).

  Lemma in_fsetD x X Y : (x \in X `\` Y ) = (x \in X ) && (x \notin Y ).

  Lemma in_fsetI x X Y : (x \in X `&` Y ) = (x \in X ) && (x \in Y ).

  Lemma in_fset0 x : (x \in fset0 ) = false.

  Lemma in_fset1 x y : (x \in [fset y ]) = (x == y ).

  Lemma fset11 x : (x \in [fset x ]).

  Definition in_fset := (in_sep ,in_fsetU ,in_fset0 ,fset11 ,in_fset1 ).
  Definition inE := (in_fset ,inE ).

  Section Laws.
    Variables X Y Z : {fset T }.

    Lemma fsetUA : X `|` (Y `|` Z ) = X `|` Y `|` Z.

    Lemma fsetUC : X `|` Y = Y `|` X.

    Lemma fsetIA : X `&` (Y `&` Z ) = X `&` Y `&` Z.

    Lemma fsetIC : X `&` Y = Y `&` X.

    Lemma fsetIUr : X `&` (Y `|` Z ) = (X `&` Y ) `|` (X `&` Z ).

    Lemma fsetIUl : (Y `|` Z ) `&` X = (Y `&` X ) `|` (Z `&` X ).

    Lemma fsetUIr : X `|` (Y `&` Z ) = (X `|` Y ) `&` (X `|` Z ).

    Lemma fsetUIl : (Y `&` Z ) `|` X = (Y `|` X ) `&` (Z `|` X ).

    Lemma fset1U x : x \in X -> X = x |` X.

    Lemma fset1U1 x : x \in x |` X.

    Lemma fsetUP x : reflect (x \in X \/ x \in Y) (x \in X `|` Y).

    Lemma fsetU1P y x : reflect (y = x \/ y \in X) (y \in x |` X).
  End Laws.

Separation

  Lemma sepU X Y p :
    [fset x in X `|` Y | p x] = [fset x in X | p x] `|` [fset x in Y | p x].

  Lemma sep0 p : [fset x in fset0 | p x] = fset0 :> {fset T }.

  Lemma sep1 (a : T) (p : pred T) :
    [fset x in [fset a ] | p x] = if p a then [fset a ] else fset0.

Empty Set

  Lemma fset0Vmem X : ( X = fset0 ) + { x | x \in X }.

  Lemma emptyPn X : reflect (exists x , x \in X) (X != fset0).

  Lemma fsetU0 X : X `|` fset0 = X.

  Lemma fset0U X : fset0 `|` X = X.

  Lemma fsetI0 X : fset0 `&` X = fset0.

  Lemma fset0I X : X `&` fset0 = fset0.

  Lemma fsetD0 X : X `\` fset0 = X.

Imset

  Lemma fimsetP X (f : T -> T') a :
    reflect (exists2 x, x \in X & a = f x) (a \in f `@` X).

  Lemma in_fimset x X (f : T -> T') : (x \in X) -> (f x \in f `@` X).

  Variables (A : {fset aT1 }) (B : {fset aT2 }) (C : {fset aT3 }).

  CoInductive fimset2_spec (rT : choiceType) f (y : rT) : Prop :=
    fImset_spec a b : y = f a b -> a \in A -> b \in B -> fimset2_spec f y.

  Lemma fimset2P (rT : choiceType) f (y : rT) :
    reflect (fimset2_spec f y) (y \in fimset2 f A B).

  Lemma mem_fimset2 (rT : choiceType) (f : aT1 -> aT2 -> rT) a b :
    a \in A -> b \in B -> f a b \in fimset2 f A B.

  Definition injective2 (f : aT1 -> aT2 -> T) :=
    forall a1 a2 b1 b2, f a1 b1 = f a2 b2 -> a1 = a2 /\ b1 = b2.

  Lemma in_fimset2 (f : aT1 -> aT2 -> T) a b :
    injective2 f -> (f a b \in fimset2 f A B ) = (a \in A ) && (b \in B ).

  Lemma in_fimset2F (f g : aT1 -> aT2 -> T) a b :
    (forall a b a' b', f a b <> g a' b') -> (f a b \in fimset2 g A B = false).

Cross Product

Lemma in_fsetX a b : ((a ,b ) \in A `x ` B ) = (a \in A ) && (b \in B ).

Lemma fsetXP a b : reflect (a \in A /\ b \in B) ((a ,b ) \in A `x ` B).

Subset

  Lemma subP (T1 : choiceType) (X Y : {fset T1 }) : reflect {subset X <= Y } (X `<=` Y).

  Lemma subPn X Y : reflect (exists2 x, x \in X & x \notin Y) (~~ (X `<=` Y )).

  Lemma subxx X : X `<=` X.
  Hint Resolve subxx.

  Lemma sub_trans Y X Z : X `<=` Y -> Y `<=` Z -> X `<=` Z.

  Lemma eqEsub X Y : (X == Y ) = (X `<=` Y ) && (Y `<=` X ).

  Lemma sub0x X : fset0 `<=` X.

  Lemma subx0 X : X `<=` fset0 = (X == fset0 ).

  Lemma fsubUr X Y : X `<=` Y `|` X.

  Lemma fsubUl X Y : X `<=` X `|` Y.

  Lemma fsubIl X Y : (X `&` Y ) `<=` X.

  Lemma fsubIr X Y : (X `&` Y ) `<=` Y.

  Lemma fsubDl X Y : X `\` Y `<=` X.

  Hint Resolve sub0x fset11 fsubUr fsubUl fsubDl.

  Lemma subsep X (P : pred T) : [fset x in X | P x] `<=` X.

  Lemma sep_sub X X' p q : X `<=` X' -> {in X , subpred p q } ->
    [fset x in X | p x] `<=` [fset x in X' | q x].

  Lemma sep_sep X p q : [fset x in sep X p | q x] = [fset x in X | p x && q x].

  Lemma sepS X Y p : X `<=` Y -> [fset x in X | p x] `<=` [fset x in Y | p x].

  Lemma fsubUset X Y Z : (X `|` Y `<=` Z ) = (X `<=` Z ) && (Y `<=` Z ).

  Lemma fsubUsetP X Y Z: reflect ((X `<=` Z ) /\ (Y `<=` Z )) (X `|` Y `<=` Z).

  Lemma fsetUSU X X' Y Y' : X `<=` X' -> Y `<=` Y' -> X `|` Y `<=` X' `|` Y'.

  Lemma fsetSU X Y Z : X `<=` Y -> X `|` Z `<=` Y `|` Z.

  Lemma fsetUS X Y Z : X `<=` Y -> Z `|` X `<=` Z `|` Y.

  Lemma fsub1 x X : ([fset x ] `<=` X ) = (x \in X ).

  Lemma fsetDSS X X' Y Y' : X `<=` X' -> Y' `<=` Y -> X `\` Y `<=` X' `\` Y'.

  Lemma fsetDS X Y Z : X `<=` Y -> Z `\` Y `<=` Z `\` X.

  Definition fsetCK Y X : X `<=` Y -> Y `\` (Y `\` X ) = X.

  Lemma fsetUD X Y : Y `<=` X -> Y `|` (X `\` Y ) = X.

  Lemma fsetUD1 x X : x \in X -> x |` (X `\` [fset x ]) = X.

  Lemma properE X Y : X `<` Y -> exists2 x, (x \in Y ) & (x \notin X ).

  Lemma properEneq X Y : (X `<` Y ) = (X != Y ) && (X `<=` Y ).

  Lemma properD1 X x : x \in X -> X `\` [fset x ] `<` X.

  Lemma fproperU X Y : (X `<` Y `|` X ) = ~~ (Y `<=` X ).

  Lemma fproper1 x X : (X `<` x |` X ) = (x \notin X ).

  Lemma fimsetS X Y (f : T -> T') : X `<=` Y -> f `@` X `<=` f `@` Y.

Powerset - Definition suggested by Georges Gonthier

  Definition powerset X : {fset {fset T }} :=
    let e := elements X in
    let mT := ((size e ).-tuple bool) in
      set_of (map (fun m : mT => set_of (mask m e)) (enum {: mT })).

  Lemma powersetE X Y : (X \in powerset Y ) = (X `<=` Y ).

  Lemma powersetP X Y : reflect {subset X <= Y } (X \in powerset Y).

  Lemma powersetU X1 X2 (X3 : {fset T }) :
    (X1 `|` X2 \in powerset X3 ) = (X1 \in powerset X3 ) && (X2 \in powerset X3 ).

  Lemma sub_power X Y Z : X `<=` Y -> Y \in powerset Z -> X \in powerset Z.

  Lemma power_sub X Z Z' : X \in powerset Z -> Z `<=` Z' -> X \in powerset Z'.

  Lemma power_mon X Y : X `<=` Y -> powerset X `<=` powerset Y.

  Lemma fsubsetU X Z Z' : (X `<=` Z ) || (X `<=` Z') -> (X `<=` Z `|` Z').

Quantification

  Lemma allU X Y p : all p (X `|` Y) = all p X && all p Y.

  Lemma all_fset1 x p : all p [fset x ] = p x.

  Lemma all_fset0 (p : pred T) : all p fset0.

  Lemma has_fset1 x p : has p [fset x ] = p x.

  Lemma has_fset0 (p : pred T) : has p fset0 = false.

  Lemma all_subP (U : {fset T }) (P : pred _) :
    reflect (forall X, X `<=` U -> P X) (all P (powerset U)).

End OperationsTheory.
Hint Resolve sub0x fset11 fsubUr fsubUl fsubDl subsep.

Section Fimset3.
  Variables (aT1 aT2 aT3 rT : choiceType) (f : aT1 -> aT2 -> aT3 -> rT).
  Variables (A : {fset aT1 }) (B : {fset aT2 }) (C : {fset aT3 }).

  CoInductive fimset3_spec x : Prop :=
    fImset3_spec a b c : x = f a b c -> a \in A -> b \in B -> c \in C -> fimset3_spec x.

  Lemma fimset3P x :
    reflect (fimset3_spec x) (x \in [fset f a b c | a <- A , b <- B , c <- C ]).

  Lemma mem_fimset3 a b c:
    a \in A -> b \in B -> c \in C -> f a b c \in fimset3 f A B C.
End Fimset3.

TODO: if T is a finite type, then {fset T} should also be a finite type. This means there is a universal set and one can form unrestricted comprehensions. Hence, for finite T, {fset T} behaves like {set T}.

Definition fsetT {T : finType} := set_of (enum T).

Lemma in_fsetT (T : finType) (x : T) : x \in fsetT.

Definition fset (T: finType) (q : pred T) := [fset x in fsetT | q x].

Lemma fsetE (T: finType) (q : pred T) x : x \in fset q = q x.

Big Unions

fsetU/fset0 forms a commutative monoid. For any such monoid indexing with a separation is equivalent to indexing on the base set and filtering.

Canonical Structure fsetU_law (T : choiceType) :=
  Monoid.Law (@fsetUA T) (@fset0U T) (@fsetU0 T).
Canonical Structure fsetU_comlaw (T : choiceType) :=
  Monoid.ComLaw (@fsetUC T).

Notation "\bigcup_( x 'in' X | P ) F" :=
  (\big [fsetU /fset0 ]_(x <- elements X | P) F) (at level 41).
Notation "\bigcup_( x 'in' X ) F" :=
  (\bigcup_( x in X | true ) F) (at level 41).

Lemma big_sep (T R : choiceType) (idx : R) (op : Monoid.com_law idx) (F : T -> R) (X : {fset T }) p:
  \big [op /idx ]_(i <- [fset x in X | p x]) F i = \big [op /idx ]_(i <- X | p i) F i.

Lemma cupP (T T' : choiceType) (X : {fset T }) (P : pred T) (F : T -> {fset T'}) y :
  reflect (exists x, [&& x \in X , P x & y \in F x ]) (y \in \bigcup_(x in X | P x) F x).

Lemma bigU1 (T T' : choiceType) (X : {fset T }) (F : T -> {fset T'}) x :
  x \in X -> F x `<=` \bigcup_(x in X ) F x.

Cardinality / Size

Section Size.
  Variable T : choiceType.
  Implicit Types X Y : {fset T }.

  Lemma sizes0 : @size T fset0 = 0.

  Lemma subset_size X Y : X `<=` Y -> size X <= size Y.

  Lemma subsize_eq X Y : X `<=` Y -> size Y <= size X -> X = Y.

  Lemma sizes_eq0 X : (size X == 0) = (X == fset0 ).

  Lemma size_gt0P X : reflect (exists x, x \in X) (0 < size X).

  Lemma size_sep X (p : pred T) : size [fset x in X | p x] <= size X.

  Lemma properW X Y : X `<` Y -> X `<=` Y.

  Lemma proper_size X Y : X `<` Y -> size X < size Y.

  Lemma size_of_uniq (T0 : choiceType) (s : seq T0) : uniq s -> size (set_of s) = size s.

  Lemma powerset_size X : size (powerset X) = 2 ^ (size X ).
End Size.

Weight function for sets

Definition const aT rT (c:rT) (f : aT -> rT) := forall x, f x = c.

Section FSum.
  Variables (T : choiceType) (w : T -> nat).
  Implicit Types X Y : {fset T }.

  Definition fdisj X Y := X `&` Y == fset0.

  Definition fsum X := \sum_(x <- X ) w x.

  Lemma fsumID p X : fsum X = fsum [fset x in X | p x ] + fsum [fset x in X | ~~ p x].

  Lemma fsum1 x : fsum [fset x ] = w x.

  Lemma fsum0 : fsum fset0 = 0.

  Lemma fsumS X p : fsum [fset x in X | p x] = fsum X - fsum [fset x in X | ~~ p x].

  Lemma fsumI X Y : fsum (X `&` Y) = fsum X - fsum (X `\` Y).

  Lemma fsumD X Y : fsum (X `\` Y) = fsum X - fsum (X `&` Y).

  Lemma fsumU X Y : fsum (X `|` Y) = fsum X + fsum Y - fsum (X `&` Y).

  Lemma fsumDsub X Y : Y `<=` X -> fsum (X `\` Y) = fsum X - fsum Y.

  Lemma fsum_const X n : {in X , const n w } -> fsum X = n * size X.

  Lemma fsum_eq0 X : fsum X = 0 -> {in X , const 0 w }.

  Lemma fsum_sub X Y : X `<=` Y -> fsum X <= fsum Y.

  Lemma fsum_replace X Y Z : fsum Z < fsum Y -> Y `<=` X -> fsum (Z `|` X `\` Y) < fsum X.
End FSum.

Lemma fsum_const1 (T : choiceType) (X : {fset T }) : fsum (fun _ => 1) X = size X.

Lemma fsizeU (T : choiceType) (X Y : {fset T }) : size (X `|` Y) <= size X + size Y.

Lemma fsizeU1 (T : choiceType) x (X : {fset T }) : size (x |` X) <= (size X ).+1.

Lemma fimsetU (aT rT : choiceType) (f : aT -> rT) (A B : {fset aT }) :
[fset f x | x <- A `|` B ] = [fset f x | x <- A ] `|` [fset f x | x <- B ].

Lemma fimset1 (aT rT : choiceType) (f : aT -> rT) a : [fset f x | x <- [fset a ]] = [fset f a ].

Lemma fimset0 (aT rT : choiceType) (f : aT -> rT) : [fset f x | x <- fset0 ] = fset0.

Lemma fimsetU1 (aT rT : choiceType) (f : aT -> rT) (B : {fset aT }) a :
[fset f x | x <- a |` B ] = f a |` [fset f x | x <- B ].

Lemma fsetUCA (T : choiceType) (A B C : {fset T }) : A `|` (B `|` C ) = B `|` (A `|` C ).

Lemma iter_fix T (F : T -> T) x k n :
  iter k F x = iter k .+1 F x -> k <= n -> iter n F x = iter n .+1 F x.

Fixpoints

Lemma wf_leq X (f : X -> nat) : well_founded (fun x y => f x < f y).

Lemma nat_size_ind (X:Type) (P : X -> Type) (f : X -> nat) :
   (forall x, (forall y, (f y < f x) -> P y) -> P x) -> forall x, P x.

Lemma slack_ind (T : choiceType) (P : {fset T } -> Type) (U : {fset T }):
  (forall X, (forall Y, Y `<=` U -> X `<` Y -> P Y) -> X `<=` U -> P X)-> forall X, X `<=` U -> P X.

Section Fixpoints.
  Variables (T : choiceType) (U : {fset T }) (F : {fset T } -> {fset T }).
  Definition monotone := forall X Y, X `<=` Y -> F X `<=` F Y.
  Definition bounded := forall X, X `<=` U -> F X `<=` U.
  Hypothesis (F_mono : monotone) (F_bound : bounded).

  Definition lfp := iter (size U) F fset0.

  Lemma lfp_ind_aux (P : {fset T } -> Type) : P fset0 -> (forall s , P s -> P (F s)) -> P lfp.

  Lemma lfp_ind (P : T -> Type) :
    (forall x X, (forall y, y \in X -> P y) -> x \in F X -> P x) -> forall x, x \in lfp -> P x.

  Lemma iterFsub1 n : iter n F fset0 `<=` iter n .+1 F fset0.

  Lemma iterFsub n m : n <= m -> iter n F fset0 `<=` iter m F fset0.

  Lemma iterFbound n : iter n F fset0 `<=` U.

  Lemma lfpE : lfp = F lfp.

  Lemma lfp_level_aux x : x \in lfp -> exists n, x \in iter n .+1 F fset0.

Should be level but this is not picked up by coqdoc

  Definition levl (x : T) (lx : x \in lfp) := ex_minn (lfp_level_aux lx).

  Lemma level_max (x : T) (lx : x \in lfp) : levl lx < size U.

  Lemma level1 (x : T) (lx : x \in lfp) : x \in iter (levl lx ).+1 F fset0.

  Lemma level2 (x y : T) (lx : x \in lfp) :
    y \in iter (levl lx) F fset0 -> exists ly, @levl y ly < levl lx.

End Fixpoints.

Section GreatestFixpoint.
  Variables (T : choiceType) (U : {fset T }) (F : {fset T } -> {fset T }).
  Hypothesis (F_mono : monotone F) (F_bound : bounded U F).

  Local Notation "~` A" := (U `\` A) (at level 0).

  Let F' A := ~` (F ~` A ).

  Let mono_F' : monotone F'.

  Let bounded_F' : bounded U F'.

  Definition gfp := ~` (lfp U F').

  Lemma gfpE : gfp = F gfp.

  Lemma gfp_ind_aux (P : {fset T } -> Type) : P U -> (forall s , P s -> P (F s)) -> P gfp.

  Lemma gfp_ind (P : T -> Type) :
    (forall x X, (forall y, y \in U -> P y -> y \in X) -> P x -> x \in F X) ->
    forall x, x \in U -> P x -> x \in gfp.
End GreatestFixpoint.

Section Pick.
  Variables (T:choiceType) (p : pred T) (X : {fset T }).

  Definition fpick :=
    if fset0Vmem [fset x in X | p x] is inr (exist x _) then Some x else None.

  CoInductive fpick_spec : option T -> Type :=
    | fPick x : p x -> x \in X -> fpick_spec (Some x)
    | fNopick : (forall x, x \in X -> ~~ p x) -> fpick_spec None.

  Lemma fpickP : fpick_spec (fpick).
End Pick.

Connectivity withing a set

Section FsetConnect.
  Variables (T : choiceType) (S : {fset T }) (e : rel T).

  Definition restrict := [rel a b : seq_sub S | e (val a) (val b)].

  Definition connect_in (x y : T) :=
    [exists a, exists b, [&& val a == x , val b == y & connect restrict a b]].

  Lemma connect_in0 (x : T) : x \in S -> connect_in x x.

  Lemma connect_in1 (x y : T) : x \in S -> y \in S -> e x y -> connect_in x y.

  Lemma connect_in_trans (z x y : T) : connect_in x z -> connect_in z y -> connect_in x y.

  Lemma connect_inP x y :
    reflect (exists p : seq T , [/\ all (mem S) (x ::p), path e x p & y = last x p ])
            (connect_in x y).
End FsetConnect.

Maximal extensions and Pruning

Section Maximal.
  Variable (T : choiceType) (U : {fset T }) (P : pred {fset T }).

  Definition maximalb (M : {fset T }) := P M && [all Y in powerset U , (M `<` Y) ==> ~~ P Y].
  Definition maximal (M : {fset T }) := P M /\ forall Y, Y `<=` U -> M `<` Y -> ~~ P Y.

  Lemma maximalP M : reflect (maximal M) (maximalb M).

  Lemma ex_max X : X `<=` U -> P X -> exists M, [/\ X `<=` M , M `<=` U & maximal M ].
End Maximal.

Section Pruning.
  Variables (T:choiceType) (p : T -> {fset T } -> bool).
  Implicit Types (S : {fset T }).

  Require Import Recdef.

  Function prune S {measure size} :=
    if fpick (p ^~ S) S is Some x then prune (S `\` [fset x]) else S.

  Lemma prune_ind (P : {fset T } -> Type) S :
    P S ->
    (forall x S0, p x S0 -> x \in S0 -> P S0 -> S0 `<=` S -> P (S0 `\` [fset x ])) ->
    P (prune S).

  Lemma prune_sub S : prune S `<=` S.

  Lemma pruneE x S : x \in prune S -> ~~ p x (prune S).
End Pruning.

Legacy/compatibility

Definition feqEsub := eqEsub.

Lemma set_of_nilp (T : choiceType) (s : seq T) : (set_of s == fset0 ) = (nilp s ).

Rudimentary Automation

Section AutoLemmas.
  Variables (T T':choiceType).
  Implicit Types (X Y Z : {fset T }).

  Lemma fsubU_auto X Y Z : (X `<=` Z) -> (Y `<=` Z) -> (X `|` Y `<=` Z).

  Lemma fsub1_auto x X : x \in X -> ([fset x ] `<=` X).

  Lemma fsetU_auto1 x X Y : x \in X -> x \in X `|` Y.

  Lemma fsetU_auto2 x X Y : x \in Y -> x \in X `|` Y.

  Lemma fsetU_auto3 X Y Z : X `<=` Y -> X `<=` Y `|` Z.

  Lemma fsetU_auto4 X Y Z : X `<=` Y -> X `<=` Z `|` Y.
End AutoLemmas.

Hint Resolve subxx fsetUSU fsubUl fsubUr fsubU_auto fsub1_auto
     fsetU_auto1 fsetU_auto2 fsetU_auto3 fsetU_auto4 fset11 fset1U1 : fset.

Hint Extern 4 (is_true _) => (match goal with [ H : is_true (_ `|` _ `<=` _) |- _ ] => case/fsubUsetP : H end) : fset .
Hint Extern 4 (is_true _) => (match goal with [ H : is_true ((_ \in _) && (_ \in _))|- _ ] => case/andP : H end) : fset .
Hint Extern 4 (is_true _) =>
  match goal with
    | [ H : is_true ((_ \in _) && (_ \in _)) |- _] => case/andP : H
  end : fset.