Library effective

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

Require Import NArith.

Effective preorders.

We define the notion of "effective" preorders: those for which the order relation is decidable and the members of the preorder are enumerable.

Record effective_order (A:preord) :=
  { eff_ord_dec : forall x y:A, {x y} + {x y}
  ; eff_enum : eset A
  ; eff_complete : forall x:A, x eff_enum

Effective orders have a decidable equality.
Canonical Structure eff_to_ord_dec A (Heff:effective_order A) : ord_dec A :=
  OrdDec A (eff_ord_dec A Heff).
Coercion eff_to_ord_dec : effective_order >-> ord_dec.

The positive integers form an effective preorder.
Program Definition Ndisc_ord : preord :=
  Preord.Pack N (Preord.Mixin N (@eq N) _ _).
Solve Obligations of Ndisc_ord using intros; subst; auto.
Canonical Structure Ndisc_ord.

Program Definition effective_Nord : effective_order Ndisc_ord
  := EffectiveOrder Ndisc_ord _ (fun n => Some n) _.

Given an effective preorder, we can calculate a canonical index value for any given element of the preorder.
We do this by first generating the subset of the enumeration set containing all elements equal to x; then we choose the smallest index from that set that is defined. Such an element exists because we know the set is inhabited. The weak principle of countable choice then suffices to choose the index.

Definition unenumerate_set (A:preord) (Heff:effective_order A) (x:A)
  : eset A :=
  fun n =>
    match eff_enum A Heff n with
    | Some x' =>
        if PREORD_EQ_DEC A (eff_to_ord_dec A Heff) x x'
           then Some x'
           else None
    | None => None

Lemma unenumerate_set_inhabited A Heff x :
  einhabited (unenumerate_set A Heff x).

Definition unenumerate (A:preord) (Heff:effective_order A) (x:A) : N :=
  proj1_sig (projT2
    (find_inhabitant A
      (unenumerate_set A Heff x)
      (unenumerate_set_inhabited A Heff x))).

Lemma unenumerate_correct A Heff x :
  exists x', eff_enum A Heff (unenumerate A Heff x) = Some x' /\ x x'.

The unenumeration index is unique (up to Leibniz equality) and equal indexes imply equal elements.
Lemma unenumerate_uniq A Heff x x' :
  x x' ->
  unenumerate A Heff x = unenumerate A Heff x'.

Lemma unenumerate_reflects A Heff x x' :
  unenumerate A Heff x = unenumerate A Heff x' ->
  x x'.

Lemma eff_in_dec : forall {A:preord} (Heff:effective_order A) (M:finset A) (x:A),
  { x M } + { x M }.

The one-point preorder is effective.
Program Definition effective_unit : effective_order unitpo
   := EffectiveOrder unitpo (fun _ _ => left I) (single tt) _.

The empty preorder is effective.
Program Definition effective_empty : effective_order emptypo :=
  EffectiveOrder _ _ (fun x => None) _.

The binary product of effective preorders is effective.
Program Definition effective_prod {A B:preord}
  (HA:effective_order A)
  (HB:effective_order B)
  : effective_order (A×B)
  := EffectiveOrder _ _ (eprod (eff_enum A HA) (eff_enum B HB)) _.

The binary sum of effective preorders is effective.
Program Definition effective_sum {A B:preord}
  (HA:effective_order A)
  (HB:effective_order B)
  : effective_order (sum_preord A B)
  := EffectiveOrder _ _ (esum (eff_enum A HA) (eff_enum B HB)) _.

The lift of an effective preorder is effective.
Definition enum_lift (A:preord) (X:eset A) : eset (lift A) :=
  union2 (single None) (image (liftup A) X).

Program Definition effective_lift {A:preord}
  (HA:effective_order A)
  : effective_order (lift A) :=
  EffectiveOrder _ _ (enum_lift A (eff_enum A HA)) _.

FIXME? this doesn't really fit here, but the current module tree means it can't go in esets.v. Maybe semidec should get split out into a separate file?
Lemma semidec_ex (A B:preord) (P:A -> B -> Prop)
  (Hok : forall a b c, b c -> P a b -> P a c)
  (HB:effective_order B) :
  (forall ab, semidec (P (fst ab) (snd ab))) ->
  (forall a, semidec (@ex B (P a))).