Library finsets


Require Import Relations.
Require Import List.
Require Import Setoid.
Require Import Arith.

Require Import basics.
Require Import preord.
Require Import categories.
Require Import sets.

The theory of finite sets.

Here we define the theory of finite sets. Concretely, finite sets are represetned by the standard list type, with list membership. Singleton sets are given by one-element lists, union is defined by list concatination and image is the stadard list map function.

Definition concat (A:Type) (l:list (list A)) : list A :=
  List.fold_right (@app A) (@nil A) l.

Module finset.
Section finset.
  Definition fset (A:preord) := list A.
  Definition fsingle (A:preord) (a:A) := a::nil.
  Definition fmember (A:preord) (a:A) (P:fset A) := exists a', In a' P /\ a a'.
  Definition fimage (A B:preord) (f:A B) (P:fset A) : fset B :=
    List.map (Preord.map A B f) P.
  Definition funion (A:preord) (XS:fset (set.set_preord fset fmember A)) : fset A :=
    fold_right (@app A) (@nil A) XS.

  Program Definition mixin : set.mixin_of fset fmember fsingle fimage funion :=
    set.Mixin fset fmember fsingle fimage funion _ _ _ _ _ _.
End finset.
End finset.

Canonical Structure finset_theory : set.theory :=
  set.Theory
    finset.fset
    finset.fmember
    finset.fsingle
    finset.fimage
    finset.funion
    finset.mixin.

Notation finset := (set_preord finset_theory).

Definition cl_finset_theory (CL:color) : set.theory
  := cset_theory finset_theory CL.
Notation cl_finset CL := (set_preord (cl_finset_theory CL)).

Program Definition finset_dec (A:preord) (Adec : ord_dec A) : set_dec finset_theory A
  := Setdec finset_theory A _.

Canonical Structure finset_dec.

Some useful lemmas relating list formation operations to finite set membership.
Lemma nil_elem : forall (A:preord) (x:A),
  x (nil : finset A) -> False.

Lemma cons_elem : forall (A:preord) (a:A) (P:finset A) (x:A),
  x (a::P : finset A) <-> x a \/ x P.

Lemma app_elem : forall (A:preord) (P Q:finset A) (x:A),
  x (P++Q : finset A) <-> x P \/ x Q.

Lemma nil_subset X (Q:finset X) :
  (nil : finset X) Q.

Lemma ub_nil : forall (X:preord) (a:X),
  upper_bound a (nil : finset X).

Lemma ub_cons (X:preord) (x:X) (xs:finset X) (a:X) :
  x a ->
  upper_bound a xs ->
  upper_bound a (x::xs : finset X).

Lemma cons_subset (X:preord) (x:X) (xs ys:finset X) :
  x ys -> xs ys -> (x::xs : finset X) ys.

Lemma cons_morphism (X:preord) (x x':X) (xs xs':finset X) :
  x x' -> xs xs' -> (x :: xs:finset X) x' :: xs'.

Lemma dec_conj (P Q : Prop) :
  {P}+{~P} -> {Q}+{~Q} -> {P/\Q}+{~(P/\Q)}.

The cartesian product of finite sets.
Fixpoint finprod {A B:preord} (P:finset A) (Q:finset B) : finset (A×B) :=
  match P with
  | nil => nil
  | x::P' => map (fun y => (x,y)) Q ++ finprod P' Q
  end.

Lemma finprod_elem : forall A B (P:finset A) (Q:finset B) a b,
  (a,b) finprod P Q <-> (a P /\ b Q).

Disjoint union of finite sets.

Fixpoint left_finset (A B:preord) (X:finset (sum_preord A B)) : finset A :=
  match X with
  | nil => nil
  | inl l :: X' => l :: left_finset A B X'
  | inr _ :: X' => left_finset A B X'
  end.

Fixpoint right_finset (A B:preord) (X:finset (sum_preord A B)) : finset B :=
  match X with
  | nil => nil
  | inl _ :: X' => right_finset A B X'
  | inr r :: X' => r :: right_finset A B X'
  end.

Lemma left_finset_elem A B X a :
  a left_finset A B X <-> inl a X.

Lemma right_finset_elem A B X b :
  b right_finset A B X <-> inr b X.

Definition finsum {A B:preord} (P:finset A) (Q:finset B) : finset (sum_preord A B) :=
  map inl P ++ map inr Q.

Lemma finsum_left_elem : forall A B (P:finset A) (Q:finset B) a,
  inl a finsum P Q <-> a P.

Lemma finsum_right_elem : forall A B (P:finset A) (Q:finset B) b,
  inr b finsum P Q <-> b Q.

Lemma left_right_finset_finsum A B X :
  X finsum (left_finset A B X) (right_finset A B X).

We can take the subset of a finite set if the predicate we wish to use to take the subset is decidable.
Section finsubset.
  Variable A:preord.
  Variable P : A -> Prop.
  Variable HP : forall x y, x y -> P x -> P y.
  Variable Hdec : forall x, { P x } + { ~P x }.

  Fixpoint finsubset (l:finset A) : finset A :=
    match l with
    | nil => nil
    | x::xs => if Hdec x then x :: finsubset xs else finsubset xs
    end.

  Lemma finsubset_elem : forall X x,
    x finsubset X <-> (x X /\ P x).
End finsubset.

We can take the intersection of finite sets if the elements have decidable equality.
Definition fin_intersect (A:preord) (Hdec:ord_dec A) (X Y:finset A) : finset A
 := finsubset A (fun x => x X) (fun x => finset_dec A Hdec x X) Y.

Lemma fin_intersect_elem : forall A Hdec X Y x,
  x fin_intersect A Hdec X Y <-> (x X /\ x Y).

Definition fin_list_intersect
  A Hdec (l:finset (finset A)) (Z:finset A) : finset A :=
  List.fold_right (fin_intersect A Hdec) Z l.

Lemma fin_list_intersect_elem : forall A Hdec l Z x,
  x fin_list_intersect A Hdec l Z <-> (x Z /\ forall X, X l -> x X).

We can remove an element from a finite set if the elements have decidable equality.
Fixpoint finset_remove {A:preord} (Hdec : ord_dec A) (X:finset A) (a:A) : finset A :=
  match X with
  | nil => nil
  | List.cons x xs => if PREORD_EQ_DEC A Hdec x a
                  then finset_remove Hdec xs a
                  else List.cons x (finset_remove Hdec xs a)
  end.

Lemma finset_remove_elem : forall A (Hdec:ord_dec A) X a x,
  x finset_remove Hdec X a <-> (x X /\ x a).

Lemma finset_remove_length1 A Hdec (X:finset A) (a:A) :
  length (finset_remove Hdec X a) <= length X.

Lemma finset_remove_length2 A Hdec (X:finset A) (a:A) :
  a X -> length (finset_remove Hdec X a) < length X.

We can take the powerset of a finite set; that is, all finite subsets of a finite set.
Fixpoint list_finsubsets {A:preord} (M:finset A) : finset (finset A) :=
  match M with
  | nil => List.cons nil nil
  | List.cons x xs =>
       let subs := list_finsubsets xs in
           List.app (subs) (List.map (List.cons x) subs)
  end.

Lemma list_finsubsets_correct A : forall (M X:finset A),
  X list_finsubsets M -> X M.

Lemma list_finsubsets_complete A (Hdec : ord_dec A) : forall (M X:finset A),
  X M -> X list_finsubsets M.

Decidability facts of various kinds can be pushed into finite sets.
Lemma finset_find_dec (A:preord)
  (P:A -> Prop)
  (HP : forall x y:A, x y -> P x -> P y)
  (Hdec : forall x:A, {P x}+{~P x}) :
  forall M:finset A, { z | z M /\ P z } + { forall z, z M -> ~P z }.

Lemma finset_find_dec' (A:preord)
  (P:A -> Prop)
  (HP : forall x y:A, x y -> P x -> P y)
  (Hdec : forall x:A, {P x}+{~P x}) :
  forall M:finset A, { z | z M /\ ~P z } + { forall z, z M -> P z }.

Lemma finsubset_dec (A:preord)
  (HAdec : ord_dec A)
  (P:finset A -> Prop)
  (HP : forall x y:finset A, x y -> P x -> P y)
  (Hdec : forall x:finset A, {P x}+{~P x}) :
  forall (M:finset A),
    { exists X:finset A, X M /\ P X } +
    { forall X:finset A, X M -> ~P X }.

Lemma finsubset_dec' (A:preord)
  (HAdec : ord_dec A)
  (P:finset A -> Prop)
  (HP : forall x y:finset A, x y -> P x -> P y)
  (Hdec : forall x:finset A, {P x}+{~P x}) :
  forall (M:finset A),
    { forall X:finset A, X M -> P X } +
    { exists X:finset A, X M /\ ~P X }.

Lemma finset_in_dec (A:preord) (Hdec : ord_dec A) : forall (M:finset A) (x:A),
  { x M } + { x M }.

Lemma finset_cons_eq (A:preord) (x y:A) (l1 l2:finset A) :
  x y -> l1 l2 ->
  (x::l1 : finset A) (y::l2).

Swelling

This lemma is used to construct certain finite sets. It works by starting with some small set and adding new elements to it until it satisfies some completeness property of interest. We know that the process must halt because every new element added is drawn from a finite set M.
Swelling is used to construct sets that are hard to get other ways, such as when the defining predicate is not decidable.
The swelling techinque is essentially unique to constructive settings; in a classical setting one would simply use a set comprehension principle to define the desired finite subset.
Lemma swelling_lemma (A:preord) (HA:ord_dec A)
  (M:finset A)
  (INV : finset A -> Prop)
  (P : finset A -> Prop)

  (HP : forall z, z M -> INV z ->
    P z \/ exists q, q M /\ q z /\ INV (q::z)) :

  (exists z0, z0 M /\ INV z0) ->
  exists z, z M /\ INV z /\ P z.