ContPropMonadTrans.v

Set Universe Polymorphism.

From Coq Require Import Setoid Morphisms.

From ExtLib Require Import Structures.Monad.

From ITree Require Import ITree.

Variant Cont (R A : Type) : Type :=
| MkCont (runCont : (A -> R) -> R)
.

Arguments MkCont {R A}.

Definition runCont {R A} (f : Cont R A) : (A -> R) -> R :=
  match f with
  | MkCont f' => f'
  end.

Definition retCont {R A} (a : A) : Cont R A :=
  MkCont (fun k => k a).

Definition bindCont {R A B} (u : Cont R A) (h : A -> Cont R B) :=
  MkCont (fun k =>
    runCont u (fun a =>
    runCont (h a) k)).

Instance Monad_Cont {R} : Monad (Cont R) :=
  {| ret := @retCont R
  ; bind := @bindCont R
  |}.

Class RelMonad (M : Type -> Type) : Type :=
  { rret : forall A, A -> M A -> Prop
  ; rsubst : forall A B, (A -> M B -> Prop) -> M A -> M B -> Prop
  ; rfmap : forall A B, (A -> B -> Prop) -> M A -> M B -> Prop
  }.

Arguments rret {M _ _}.
Arguments rfmap {M _ _ _}.
Arguments rsubst {M _ _ _}.

Definition lift_ContProp {M} {_ : RelMonad M} {_ : Monad M} {S A}
           (u : M A) : Cont (M S -> Prop) A :=
  MkCont (fun k v => rsubst k u v).

Definition eq_rel {A B} (RL RR : A -> B -> Prop) : Prop :=
  forall a b, RL a b <-> RR a b.

Infix "⩯" := eq_rel (at level 40).

Definition catrel {A B C} (RL : A -> B -> Prop) (RR : B -> C -> Prop)
  : A -> C -> Prop :=
  fun a c => exists b, RL a b /\ RR b c.

Class RelMonadLaws (M : Type -> Type) {RM : RelMonad M} : Prop :=
  { Proper_rsubst : forall A B, Proper (eq_rel ==> eq_rel) (rsubst (A := A) (B := B))
  ; rsubst_ret : forall A,
      rsubst rret ⩯ @eq (M A)
  ; cat_rsubst_ret : forall A B (f : A -> M B -> Prop),
      catrel rret (rsubst f) ⩯ f
  ; rsubst_rsubst : forall A B C (f : A -> M B -> Prop) (g : B -> M C -> Prop),
      catrel (rsubst f) (rsubst g) ⩯ rsubst (catrel f (rsubst g))
  }.

Definition funrel {A B} (f : A -> B) (a : A) : B -> Prop :=
  eq (f a).

Notation subst k := (fun u => bind u k).

(* [funrel] is a monad morphism between [M] as a monad on functions
   and [M] as a monad on relations. *)
Class RelMonadMorphism (M : Type -> Type) {MM : Monad M} {RM : RelMonad M} : Prop :=
  { rret_ret : forall A, rret (A := A) ⩯ funrel ret
  ; rsubst_subst : forall A B (k : A -> M B),
      rsubst (funrel k) ⩯ funrel (subst k)
  }.

Section RMM.

Context
  {M : Type -> Type}
  {MM : Monad M}
  {RM : RelMonad M}
  {RMM : RelMonadMorphism M}.

Lemma rret_ret_rel {A} (a : A) : rret a (ret a).
Proof.
  apply rret_ret; reflexivity.
Qed.

Lemma rsubst_subst_rel {A B} (u : M A) (k : A -> M B)
  : rsubst (funrel k) u (bind u k).
Proof.
  apply rsubst_subst; reflexivity.
Qed.

End RMM.

Notation LCP := lift_ContProp.

Section Proof.

Context
  (M : Type -> Type)
  {MM : Monad M}
  {RM : RelMonad M}
  {RML : RelMonadLaws M}
  {RMM : RelMonadMorphism M}.

Definition rel_cont {S A B} (RR : A -> B -> Prop) (RM : M S -> M S -> Prop)
  (ua : Cont (M S -> Prop) A) (ub : Cont (M S -> Prop) B)
  : Prop :=
  forall ka kb,
    (forall a b, RR a b -> forall va vb, RM va vb -> ka a va <-> kb b vb) ->
    forall wa wb, RM wa wb -> runCont ua ka wa <-> runCont ub kb wb.

Theorem lift_bind {S A B} (u : M A) (k : A -> M B)
  : rel_cont (@eq B)
             (rfmap (@eq S))
             (LCP (S := S) (bind u k))
             (bind (LCP u) (fun a => LCP (k a))).
Proof.
  cbn.
  unfold rel_cont.
  unfold LCP; cbn.
  intros.
  assert (EE : (fun (a : A) (v : M S) => rsubst kb (k a) v) ⩯ catrel (funrel k) (rsubst kb)).
  { clear; intros a v; split; intros.
    { red; exists (k a); split; auto. reflexivity. }
    { destruct H as [? []]. destruct H. auto. }
  }
  split; intros HH.
  - eapply Proper_rsubst; [ apply EE | ].
    apply rsubst_rsubst.
    red; exists (bind u k); split.
    + apply rsubst_subst_rel.
    + admit. (* Not quite OK (we would like to say that [rfmap] is a functor,
                so [rfmap eq ⩯ eq], but that's a bit too strong
                (think that [rfmap] is [eutt]).
                Solutions:
                - redefine [rel_cont] to just assume [ka = kb] (preferred)
                - redefine [eq_rel] in a category of setoids
                  (type * equivalence relation)
              *)
  - eapply Proper_rsubst in HH; [ | red; symmetry; auto ].
    apply rsubst_rsubst in HH.
    destruct HH as [? []].
    apply rsubst_subst in H1.
    destruct H1.
    admit. (* Same reason as above. *)
Admitted.

Theorem lift_ret {S A} (a : A)
  : rel_cont (@eq A)
             (rfmap (@eq S))
             (LCP (S := S) (ret a))
             (ret a).
Proof.
  cbn.
  unfold rel_cont.
  unfold LCP; cbn.
  intros.
  rewrite <- H; eauto. (* We wouldn't need this if we just assumed [ka = kb] *)
  admit. (* should be a law or a consequence of the others *)
Admitted.

End Proof.

SomethingElseMaybe.v

Class RelMonad (M : Type -> Type) : Type :=
  { rret : forall A, (M A -> Prop) -> A -> Prop
  ; rjoin : forall A, (M A -> Prop) -> M (M A) -> Prop
  ; rfmap : forall A B, ((B -> Prop) -> A -> Prop) -> (M B -> Prop) -> M A -> Prop
  ; rsubst : forall A B, ((M B -> Prop) -> A -> Prop) -> (M B -> Prop) -> (M A -> Prop)
  }.

Arguments rret {M _ _}.
Arguments rsubst {M _ _ _}.
Arguments rfmap {M _ _ _}.

Definition bindCProp {M A B} {_ : RelMonad M}
  : Cont Prop (M A) -> (A -> Cont Prop (M B)) -> Cont Prop (M B) :=
  fun u h =>
    MkCont (fun k =>
      runCont u (fun ma =>
      rsubst (fun kmb a => runCont (h a) kmb) k ma)). 

Definition lift_ContProp {M} {_ : RelMonad M} {_ : Monad M} {A}
           (u : M A) : Cont Prop (M A) :=
  MkCont (fun k => k u).