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