Library CatSem.CAT.IO

Require Import Coq.Program.Equality.
Require Export CatSem.CAT.orders.
Require Export CatSem.CAT.cat_INDEXED_TYPE.
Require Export CatSem.CAT.SO.
Require Export CatSem.CAT.initial_terminal.
Require Export CatSem.CAT.monad_haskell.
Require Export CatSem.CAT.monad_h_module.

Set Implicit Arguments.
Unset Strict Implicit.

Unset Automatic Introduction.

Section base_cats.

Variable T : Type.

Class io_struct (A : T -> Type) := {
  IRel : forall t, relation (A t);
  IPOprf :> forall t, PreOrder (@IRel t)
}.

Notation "y <<< z" := (IRel y z) (at level 60).

Record io_obj := {
  ipo_obj_carrier :> T -> Type ;
  ipo_obj_s :> io_struct ipo_obj_carrier
}.

Existing Instance ipo_obj_s.

Instance IRel_Trans (A : io_obj) t : Transitive (IRel (A:=A) (t:=t)).
Proof.
  intros.
  apply IPOprf.
Qed.

Lemma IRel_refl (V : io_obj) t (x : V t) : x <<< x.
Proof.
  intros V t x.
  assert (H:=IPOprf (A:= V) t).
  destruct H.
  apply PreOrder_Reflexive.
Qed.

Lemma IRel_trans (V : io_obj) t (x y z : V t) :
       x <<< y -> y <<< z -> x <<< z.
Proof.
  intros V t x y z.
  assert (H:=IPOprf (A:= V) t).
  destruct H.
  apply PreOrder_Transitive.
Qed.



Lemma smap_equiv (A B: io_obj) :
     Equivalence (A:= forall t, A t -> B t)
          (fun p q => forall t:T, forall x: A t, p t x = q t x).
Proof.
  intros A B;
  constructor;
  unfold Reflexive,Symmetric,Transitive;
  intros; simpl; try etransitivity; auto.
Qed.

Definition smap_oid A B :=
         Build_Setoid (smap_equiv A B).

Ltac t := cat; unf_Proper ;
     mauto; repeat rew_all; mauto.

Obligation Tactic := t.

Program Instance IO_SMAP_s : Cat_struct (fun a b : io_obj =>
     forall t, a t -> b t) := {
  mor_oid := smap_oid;
  comp A B C f g := fun t => fun x => g t (f t x);
  id A := fun t x => x
}.

Definition IO := Build_Cat IO_SMAP_s.


Class iMonotone (a b : IO)
     (f : a ---> b) :=
  imonotone : forall t, Proper (IRel (t:=t) ==> IRel (t:=t)) (f t).

Obligation Tactic := unfold iMonotone; unfold Proper, respectful; t.

Program Instance IO_MAP_SubCat : SubCat_compat IO
      (fun x => True) (fun a b f => iMonotone f).

Definition IO_MAP := SubCat IO_MAP_SubCat.
Inductive optrelT (u:T) (V: IO) :
  forall t,relation (opt u V t):=
  | optrelTP_none : optrelT (none u V) (none u V)
  | optrelTP_some : forall t (y z:V t), y <<< z ->
          optrelT (some u y) (some u z).

Obligation Tactic := idtac.

Program Instance opt_TP_preorder (u:T)(A:IO):
     io_struct (opt u A) := {
 IRel := @optrelT u A
}.
Next Obligation.
Proof.
  intros.
  constructor;
  unfold Reflexive, Transitive.
  intro z; induction z;
  constructor. apply IPOprf.

  intros r y z H. generalize dependent z.
  induction H.
  intros z Hz.
  induction Hz.
  constructor.
  constructor. auto.

  intros x H'.
  generalize dependent y.
  dependent destruction H'.   intros y H'.
  constructor.
  transitivity z;
  auto.
Qed.

Definition opt_TP u A : IO := Build_io_obj (opt_TP_preorder u A).

Notation "V *" := (opt_TP _ V) (at level 5).

Section IND_PO_init_term.

Program Instance IO_SMAP_term_struct : io_struct (fun t => unit) := {
  IRel t := fun _ _ => True
}.
Next Obligation.
Proof.
  constructor;
  auto.
Qed.

Definition IO_SMAP_term := Build_io_obj IO_SMAP_term_struct.

Definition IO_SMAP_term_mor (a: IO) : a ---> IO_SMAP_term :=
              (fun _ _ => tt).

Instance IO_SMAP_term_mor_monotone a :
    iMonotone (a:=a) (b:= IO_SMAP_term) (@IO_SMAP_term_mor a).
Proof.
  unfold iMonotone.
  simpl;
  intros a.
  unfold Proper; red.
  auto.
Qed.

End IND_PO_init_term.

Definition Some_TP (u : T) (A : IO) : A ---> A* :=
           (@some _ u _).

Instance Some_TP_monotone (u:T) (A:IO):
     iMonotone (a:=A) (b:= A*) (@Some_TP u A) .
Proof.
  unfold iMonotone.
  intros.
  unfold Proper;
  red.
  constructor.
  auto.
Qed.

Definition opt_TP_default (u:T) (V W : IO)
      (f: V ---> W) (w:W u): V* ---> W := @opt_default _ u V W f w.

Instance opt_TP_default_monotone (u:T) (V W : IO)
      (f: V ---> W) (H' : iMonotone f) (w:W u) :
    iMonotone (@opt_TP_default u V W f w).
Proof.
  unfold iMonotone.
  unfold Proper; red.
  intros u V W f H' w t q y H;
  induction H; simpl.
  apply IPOprf.
  apply H'.
  auto.
Qed.

Definition opt_TP_kl (u:T)(V W : IO)(f : V ---> W* )
      t (v: V* t) : W* t :=
 match v with
 | none => none u _
 | some t' v' => f t' v'
 end.

Instance opt_TP_kl_monotone (u:T) (V W : IO)
       (f: V ---> opt_TP u W) (H : iMonotone f) :
       iMonotone (opt_TP_kl f).
Proof.
  intros.
  unfold iMonotone.
  unfold Proper;
  repeat red; intros.
  induction H0; simpl.
  constructor.
  apply H; auto.
Qed.

Obligation Tactic := simpl; intros; unfold Proper;
     unfold respectful; intros; elim_opt;
               try app_all; mauto.

Program Instance opt_TP_monad_struct (u:T) :
   Monad_struct (fun V => opt_TP u V) := {
  weta V := @Some_TP u V;
  kleisli V W f := opt_TP_kl (u:=u) f
}.

Canonical Structure opt_TP_monad (u:T):=
     Build_Monad (opt_TP_monad_struct u).

Instance opt_TP_lift_monotone (u : T) V W (f : V ---> W) (H : iMonotone f) :
      iMonotone (lift (M:= opt_TP_monad u) f).
Proof.
  intros u V W f H.
  unfold lift.
  simpl.
  apply opt_TP_kl_monotone.
  assert (H':=sub_comp (SubCat_compat:=IO_MAP_SubCat)).
  simpl in *.
  apply H';
  auto.
  apply Some_TP_monotone.
Qed.

Section proj.

Program Instance io_proj_struct (t : T) (A : IO) :
    PO_obj_struct (A t) := {
  Rel := IRel (t:=t)
}.

Definition io_proj t A : wOrd := Build_PO_obj (io_proj_struct t A).

Definition io_proj_mor t A B (f : A ---> B) :
          io_proj t A ---> io_proj t B := f t.

End proj.

End base_cats.