Library discrete

Require Import Setoid.
Require Import List.

Require Import basics.
Require Import preord.
Require Import categories.
Require Import sets.
Require Import finsets.
Require Import esets.
Require Import effective.
Require Import directed.
Require Import plotkin.
Require Import joinable.
Require Import approx_rels.
Require Import cpo.
Require Import profinite.

Discrete unpointed domains

Every finite type can be turned into a discrete profinite domain. These are useful for representing base types.

Module fintype.
  Record fintype :=
  { carrier :> Type
  ; fintype_list : list carrier
  ; fintype_complete : forall x, In x fintype_list
  ; fintype_dec : forall x y:carrier, {x=y}+{x<>y}

  Definition eq_mixin (X:fintype) : Eq.mixin_of (carrier X) :=
    Eq.Mixin (carrier X) (@eq _)
    (@Logic.refl_equal _) (@Logic.eq_sym _) (@Logic.eq_trans _).

  Definition preord_mixin (X:fintype) : Preord.mixin_of (carrier X) :=
    Preord.Mixin (carrier X) (@eq _) (@Logic.refl_equal _) (@Logic.eq_trans _).

  Canonical Structure setoid (X:fintype) : Eq.type :=
    Eq.Pack X (eq_mixin X).
  Canonical Structure ord (X:fintype) : preord :=
    Preord.Pack X (preord_mixin X).

  Lemma order_discrete (X:fintype) (x y:X) : x y -> x = y.

  Lemma strong_eq (X:fintype) (x y:X) : x y -> x = y.

  Program Definition fintype_effective X : effective_order (ord X) :=
    EffectiveOrder (ord X) (fintype_dec X) (elist (fintype_list X)) _.

  Program Definition fintype_has_normals hf (X:fintype) :
    has_normals (ord X) (fintype_effective X) hf.

  Definition fintype_plotkin hf (X:fintype) : plotkin_order hf (ord X) :=
    norm_plt (ord X) (fintype_effective X) hf (@fintype_has_normals hf X).
End fintype.

Notation fintype := fintype.fintype.
Notation Fintype := fintype.Fintype.

Canonical Structure fintype.setoid.
Canonical Structure fintype.ord.
Coercion fintype.carrier : fintype >-> Sortclass.

Canonical Structure disc (X:fintype) : PLT :=
    PLT.Ob false (fintype.carrier X)
      (PLT.Class _ _
        (fintype.preord_mixin X)
        (fintype.fintype_effective X)
        (fintype.fintype_plotkin false X)).

Program Definition disc_elem (Y:fintype) (y:Y) : 1 disc Y :=
  PLT.Hom false (PLT.unit false) (disc Y) (single (tt,y)) _ _.

Lemma disc_elem_inj Y : forall y1 y2,
  disc_elem Y y1 disc_elem Y y2 -> y1 = y2.

Section disc_cases.
  Variable X:fintype.
  Variables (A B:PLT).
  Variable f : X -> (A B).

  Program Definition insert_index (x:X) : Preord.hom (A×B) ((A×disc XB) :=
    Preord.Hom (A×B) ((A×disc XB) (fun ab => ((fst ab, x), snd ab)) _.

  Fixpoint mk_disc_cases_rel (ls:list X) : eset ((PLT.ord A×disc XB)%cat_ob :=
    match ls with
    | nil =>
    | x::xs => union2 (image (insert_index x) (PLT.hom_rel (f x)))
                      (mk_disc_cases_rel xs)

  Lemma mk_disc_cases_elem : forall ls x a b, (In x ls) ->
    ((a,b) PLT.hom_rel (f x) <-> (a,x,b) mk_disc_cases_rel ls).

  Program Definition disc_cases : (A × (disc X))%plt B :=
    PLT.Hom false ( A (disc X)) B
       (mk_disc_cases_rel (fintype.fintype_list X)) _ _.

  Lemma disc_cases_elem x h : disc_cases h, disc_elem x f x h.

End disc_cases.

Program Definition finbool : fintype :=
  Fintype bool (true::false::nil) _ _.

Canonical Structure finbool.

Lemma disc_cases_elem'
     : forall (X : fintype) (A B C : PLT)
       (f : X -> A B) (g: C 1) (x : X) (h : C A),
       disc_cases f PLT.pair h (disc_elem x g) f x h.

Lemma disc_cases_univ (X:fintype) (A B:PLT) (f:X -> A B) q :
  (forall x, f x q id, disc_elem x PLT.terminate _ _) ->
  disc_cases f q.

Lemma disc_cases_commute : forall (X : fintype) (A B C : PLT)
       (f : X -> A B) (g:C A) (h:C disc X),
       disc_cases f g, h disc_cases (fun x => f x g) id, h .