Library libs.fset

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

Require Import edone bcase base.

Set Implicit Arguments.
Import Prenex Implicits.

Finite Sets over choice types and countable types

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.

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

  Lemma funiq (X : {fset T }) : uniq X.
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 fset_ax_of_seq (xs : seq T) : fset_axiom (fseq xs).

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

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

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

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.

Set Operators and 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).

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

Lemma fset0F (T : choiceType) : @set_of T [::] = fset0.

Lemma fset1F (T : choiceType) a : @set_of T [:: a ] = [fset a ].

Theory

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

  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).
  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_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 X Y 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 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 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 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 = true.

  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.

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.

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

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

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

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

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

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

End Size.

Induction Principles

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

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

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.

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

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 fsubIl X Y : (X `&` Y ) `<=` X.

  Lemma fsubIr X Y : (X `&` Y ) `<=` 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 in_fsetT (T : finType) (x : T) : x \in fsetT.

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

Section Comprehension.
  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.
End Comprehension.

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.

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 iterFsub n : iter n F fset0 `<=` iter n .+1 F fset0.

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

  Lemma lfpE : lfp = F lfp.

End Fixpoints.

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.

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.

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.

Legacy/compatibility

Definition feqEsub := eqEsub.

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