Library esets


Require Import Relations.
Require Import List.
Require Import NArith.

Require Import basics.
Require Import preord.
Require Import categories.
Require Import pairing.
Require Import sets.
Require Import finsets.

The theory of enumerable sets.

Here we define the theory of "enumerable" sets. Concretely, enumerable sets of A represented by functions N -> option A. We consider an element x to be in a set X if there exists an n such that X n = Some x' with x x'.
The singleton set is given by the constant function. The image function is defined in the straightforward way as a composition of functions. Union is defined by using the isomorphism between N and N×N defined in pairing.
Module eset.
Section eset.
  Definition eset (A:preord) := N -> option A.
  Definition esingle (A:preord) (a:A) := fun n:N => Some a.
  Definition emember (A:preord) (a:A) (P:eset A) :=
      exists n, match P n with None => False | Some a' => a a' end.
  Definition eimage (A B:preord) (f:A B) (P:eset A) (n:N) :=
      match P n with None => None | Some x => Some (f#x) end.
  Definition eunion (A:preord) (PS : eset (set.set_preord eset emember A)) : eset A :=
    fun n => let (p,q) := unpairing n in
       match PS p with
       | None => None
       | Some P => P q
       end.

  Theorem mixin : set.mixin_of eset emember esingle eimage eunion.
End eset.
End eset.

Canonical Structure eset_theory : set.theory :=
  set.Theory
    eset.eset
    eset.emember
    eset.esingle
    eset.eimage
    eset.eunion
    eset.mixin.

Notation eset := (set_preord eset_theory).

Definition cl_eset_theory CL := cset_theory eset_theory CL.
Notation cl_eset CL := (set_preord (cl_eset_theory CL)).

Countable indefinite description

A version of the principle of indefinite description can be proved for enumerable sets. This takes the form of a choice function which, given an inhabited enumerable set, calculates an inhabitant of the set.
The choice function works by simply counting upwards through the set's indexes until it finds an element. This process terminates because we assume the set is inhabited. We convince Coq's termination checker of this fact by using an auxilary inductive definition einhabited.
Section countable_ID.
  Variable A:preord.

Here we define inhabitedness of an enumerable set as an inductive predicate with a single constructor. This enables us to define a constructive choice function on inhabited enumerable sets.
  Inductive einhabited (P:eset A) : Prop :=
    | einh :
        (P N0 = None -> einhabited (fun n => P (Nsucc n))) ->
        einhabited P.

  Lemma member_inhabited : forall (P:eset A), (exists a, a P) -> einhabited P.

find_inhabitant is defined by recursion on the einhabited fact, and it finds the smallest index in the set P that is defined.
  Definition find_inhabitant : forall P (H:einhabited P),
    { a:A & { n | P n = Some a /\
      forall n' a', P n' = Some a' -> (n <= n')%N} }.

Global Opaque find_inhabitant.

  Definition choose P (H:einhabited P) : A
    := projT1 (find_inhabitant P H).

  Lemma choose_elem : forall P H, (choose P H) P.

  Lemma inhabited_einhabited : forall P, color_prop inhabited P <-> einhabited P.
End countable_ID.

Theorem countable_indefinite_description (A:preord) (X:eset A) :
  (exists x:A, x X) -> { x:A | x X }.

Additional operations on enumerable sets.

The empty set is easily definable.
Definition empty (A:preord) : eset A := fun n => None.

Every list (qua finite set) generates an enumerable set.
Definition elist (A:preord) (l:list A) : eset A := fun n => nth_error l (N.to_nat n).

The intersection of enumerable sets can be defined if we have a decidable equality on the elements.
Definition intersection {A:preord} (eqdec:forall x y:A, {x y}+{x y}) (P Q:eset A) : eset A :=
    fun n => let (p,q) := unpairing n in
       match P p, Q q with
       | Some x, Some y => if eqdec x y then Some x else None
       | _, _ => None
       end.

We also have binary unions
Definition union2 {A} (P:eset A) (Q:eset A) : eset A :=
  fun n =>
    match n with
    | N0 => P N0
    | Npos xH => Q N0
    | Npos (xO p) => P (Npos p)
    | Npos (xI q) => Q (Npos q)
    end.

The disjoint union of two enumerable sets.
Definition esum {A B} (P:eset A) (Q:eset B) : eset (sum_preord A B) :=
  fun n =>
    match n with
    | N0 => match P N0 with | None => None | Some x => Some (inl _ x) end
    | Npos xH => match Q N0 with | None => None | Some y => Some (inr _ y) end
    | Npos (xO p) => match P (Npos p) with | None => None | Some x => Some (inl _ x) end
    | Npos (xI q) => match Q (Npos q) with | None => None | Some y => Some (inr _ y) end
    end.

The binary product of enumerable sets.
Definition eprod {A B} (P:eset A) (Q:eset B) : eset (prod_preord A B) :=
  fun n => let (p,q) := unpairing n in
    match P p, Q q with
    | Some x, Some y => Some (x,y)
    | _, _ => None
    end.

Correctness lemmas for the above.
Lemma union2_elem : forall A (P Q:eset A) x,
  x (union2 P Q) <-> (x P \/ x Q).

Lemma esum_left_elem : forall A B (P:eset A) (Q:eset B) x,
  (inl B x) (esum P Q) <-> x P.

Lemma esum_right_elem : forall (A B:preord) (P:eset A) (Q:eset B) (y:B),
  (inr _ y) (esum P Q) <-> y Q.

Lemma eprod_elem : forall (A B:preord) (P:eset A) (Q:eset B) (x:A) (y:B),
  (x,y) (eprod P Q) <-> x P /\ y Q.

Notation "∅" := (empty _).

Lemma empty_elem : forall (A:preord) (x:A),
  x -> False.

Lemma elist_elem : forall (A:preord) (l:finset A) (x:A),
  x (elist l) <-> x l.

Lemma intersection_elem : forall (A:preord) eqdec (P Q:eset A) (x:A),
  x (intersection eqdec P Q) <->
  (x P /\ x Q).

The finite subets of an enumerable set are enumerable.

Fixpoint choose_finset (A:preord) (X:eset A) (n:nat) (z:N) : finset A :=
  match n with
  | 0 => nil
  | S n' => let (p,q) := unpairing z in
              match X p with
              | None => choose_finset A X n' q
              | Some a => a :: choose_finset A X n' q
              end
  end.

Lemma choose_finset_sub : forall A X n z,
  choose_finset A X n z X.

Lemma choose_finset_in : forall A X (Q:finset A),
  Q X -> exists n, exists z, choose_finset A X n z Q.

Definition finsubsets A (X:eset A) : eset (finset A) :=
  fun n => let (p,q) := unpairing n in Some (choose_finset A X (N.to_nat p) q).

Definition ne_finsubsets A (X:eset A) : eset (finset A) :=
  fun n =>
    let (p,q) := unpairing n in
    let l := choose_finset A X (N.to_nat p) q in
    match l with
    | nil => None
    | _ => Some l
    end.

Lemma finsubsets_complete : forall A (X:eset A) (Q:finset A),
  Q X <-> Q finsubsets A X.

Lemma ne_finsubsets_complete : forall A (X:eset A) (Q:finset A),
  ((exists x, x Q) /\ Q X) <-> Q ne_finsubsets A X.

Lemma unitpo_dec : ord_dec unitpo.

A predicate is semidecidable if its truth is equal to the inhabitedness of an enumerable set.
Record semidec (P:Prop) :=
  Semidec
  { decset : eset unitpo
  ; decset_correct : tt decset <-> P
  }.

Decidable predicates are semidecidable.
Program Definition dec_semidec (P:Prop)
  (Hdec : {P}+{~P}) :
  semidec P :=
  Semidec _ (if Hdec then single tt else ) _.

Program Definition semidec_true : semidec True
  := Semidec _ (single tt) _.

Program Definition semidec_false : semidec False
  := Semidec _ _.

Program Definition semidec_disj (P Q:Prop) (HP:semidec P) (HQ:semidec Q)
  : semidec (P \/ Q)
  := Semidec _ (union2 (decset P HP) (decset Q HQ)) _.

Program Definition semidec_conj (P Q:Prop) (HP:semidec P) (HQ:semidec Q)
  : semidec (P /\ Q)
  := Semidec _ (intersection (PREORD_EQ_DEC _ unitpo_dec)
                     (decset P HP) (decset Q HQ)) _.

Lemma semidec_iff (P Q:Prop) :
  (P <-> Q) ->
  semidec P -> semidec Q.

Program Definition const {A B:preord} (x:B) : A B :=
  Preord.Hom A B (fun _ => x) _.

Lemma semidec_in (A:preord) (HA:ord_dec A) (X:eset A) x :
  semidec (x X).


Fixpoint all_finset_setdec
  (A:preord) (DECSET:A -> eset unitpo) (X:finset A) : eset unitpo :=
  match X with
  | nil => single tt
  | x::xs => intersection (PREORD_EQ_DEC _ unitpo_dec)
                (DECSET x) (all_finset_setdec A DECSET xs)
  end.

Program Definition all_finset_semidec {A:preord} (P:A -> Prop)
  (Hok : forall a b, a b -> P a -> P b)
  (H:forall a, semidec (P a)) (X:finset A)
  : semidec (forall a:A, a X -> P a)
  := Semidec _ (all_finset_setdec A (fun a => decset (P a) (H a)) X) _.

Fixpoint ex_finset_setdec
  (A:preord) (DECSET:A -> eset unitpo) (X:finset A) : eset unitpo :=
  match X with
  | nil => empty unitpo
  | x::xs => union2 (DECSET x) (ex_finset_setdec A DECSET xs)
  end.

Program Definition ex_finset_semidec {A:preord} (P:A -> Prop)
  (Hok:forall a b, a b -> P a -> P b)
  (H:forall a, semidec (P a))
  (X:finset A)
  : semidec (exists a:A, a X /\ P a)
  := Semidec _ (ex_finset_setdec A (fun a => decset (P a) (H a)) X) _.

Definition eimage' (A B:preord) (f:A -> B) (P:eset A) : eset B :=
  fun n => match P n with None => None | Some x => Some (f x) end.

Program Definition esubset {A:preord} (P:A -> Prop)
  (H:forall a, semidec (P a)) (X:eset A) :=
  eset.eunion A
    (eimage' _ _ (fun x => eimage' _ _ (fun _ => x) (decset (P x) (H x))) X).

Lemma esubset_elem (A:preord) (P:A->Prop) (dec:forall a, semidec (P a))
  (Hok:forall a b, a b -> P a -> P b)
  X x :
  x esubset P dec X <-> (x X /\ P x).

Definition esubset_dec (A:preord) (P:A -> Prop) (dec:forall x:A, {P x}+{~P x})
  (X:eset A) : eset A :=
  fun n => match X n with
           | None => None
           | Some a =>
               match dec a with
               | left H => Some a
               | right _ => None
               end
           end.

Lemma esubset_dec_elem : forall (A:preord) (P:A->Prop) dec X x,
  (forall x y, x y -> P x -> P y) ->
  (x esubset_dec A P dec X <-> (x X /\ P x)).

Definition erel (A B:preord) := eset (A × B).

Definition erel_image (A B:preord) (dec : ord_dec A) (R:erel A B) (x:A) : eset B :=
  image π (esubset_dec
                    (A×B)
                    (fun p => π#p x)
                    (fun p => PREORD_EQ_DEC A dec (π#p) x) R).

Lemma erel_image_elem : forall A B dec R x y,
  y erel_image A B dec R x <-> (x,y) R.

Definition erel_inv_image
  (A B:preord) (dec : ord_dec B) (R:erel A B) (y:B) : eset A :=
  image π (esubset_dec (A×B)
                    (fun p => π#p y)
                    (fun p => PREORD_EQ_DEC B dec (π#p) y) R).

Lemma erel_inv_image_elem : forall A B dec R x y,
  x erel_inv_image A B dec R y <-> (x,y) R.

Weak countable choice

Countable indefinite description gives rise to a functional choice principle: "Every total enumerable relation gives rise to a (computable) function."
There are two subtle points regarding the formal statemet: first, we need need to assume a decidable order on A (and thus decidable setoid equality); second, the choice function is constructed not just asserted to exist.
This statement is weaker than the "standard" version of countable choice. In countable choice, the domain A is assumed to be countable, but the cardinality of the relation R is unconstrained.
Here, we instead require R to be enumerable and A to have a decidable order. Because R is total, this implies A is countable (and effective, as defined in "effective.v.") Hence this statement is implied by countable choice (more precisely, a statmenet of countable choice that constructs a function, rather than merely asserting it to exist). This statement is strictly weaker, as the usual version of countable choice is not provable in Coq.
Theorem weak_countable_choice (A B:preord) (HA:ord_dec A) (R:erel A B) :
  (forall a:A, exists b, (a,b) R) ->
  { f:A -> B | forall a, (a, f a) R }.