ContT and ContsT instances (for scalaz)

ContT.v

Set Implicit Arguments.
Unset Strict Implicit.

(** Type Definitions *)

Inductive IndexedContsT (W M : Type -> Type) (R O A : Type) : Type :=
| mkIndexedContsT : (W (A -> M O) -> M R) -> IndexedContsT W M R O A.

Definition runIndexedContsT W M R O A (c : IndexedContsT W M R O A) : W (A -> M O) -> M R :=
  match c with
  | mkIndexedContsT run => run
  end.

Definition Id (X : Type) := X.

Definition ContsT W M R A := IndexedContsT W M R R A.

Definition ContT M R A := ContsT Id M R A.

(** Type Class Definitions *)

Class Functor (F : Type -> Type) :=
  {
    map : forall A B, F A -> (A -> B) -> F B;
    functor_identity : forall A (fa : F A),
        map fa (fun a => a) = fa;
    functor_composite : forall A B C (fa : F A) (f1 : A -> B) (f2 : B -> C),
        map (map fa f1) f2 = map fa (fun a => f2 (f1 a))
  }.

Class Apply (F : Type -> Type) :=
  {
    apply_functor : Functor F;
    ap : forall A B, F A -> F (A -> B) -> F B;
    apply_composition : forall A B C (fbc : F (B -> C)) (fab : F (A -> B)) (fa : F A),
        ap (ap fa fab) fbc = ap fa (ap fab (map fbc (fun bc ab a => bc (ab a))))
  }.

Class Applicative (F : Type -> Type) :=
  {
    applicative_apply : Apply F;
    applicative_functor := @apply_functor F applicative_apply;
    point : forall A, A -> F A;
    applicative_identity_ap : forall A (fa : F A),
        ap fa (point (fun a => a)) = fa;
    applicative_homomorphism : forall A B (ab : A -> B) (a : A),
        ap (point a) (point ab) = point (ab a);
    applicative_interchange : forall A B (f : F (A -> B)) (a : A),
        ap (point a) f = ap f (point (fun f => f a));
    applicative_map_like_derived : forall A B (f : A -> B) (fa : F A),
        map fa f = ap fa (point f)
  }.

Class Bind (F : Type -> Type) :=
  {
    bind_apply : Apply F;
    bind_functor := @apply_functor F bind_apply;
    bind : forall A B, F A -> (A -> F B) -> F B;
    bind_associative_bind : forall A B C (fa : F A) (f : A -> F B) (g : B -> F C),
        bind (bind fa f) g = bind fa (fun a => bind (f a) g);
    bind_ap_like_derived : forall A B (fa : F A) (f : F (A -> B)),
        ap fa f = bind f (fun f' => map fa f')
  }.

Class Monad (F : Type -> Type) :=
  {
    monad_applicative : Applicative F;
    monad_bind : Bind F;
    monad_right_identity : forall A (fa : F A),
        bind fa (fun a => point a) = fa;
    monad_left_identity : forall A B (a : A) (f : A -> F B),
        bind (point a) f = f a
  }.

Class Plus (F : Type -> Type) :=
  {
    plus : forall A, F A -> F A -> F A;
    plus_associative : forall A (f1 f2 f3 : F A),
        plus f1 (plus f2 f3) = plus (plus f1 f2) f3
  }.

Class PlusEmpty (F : Type -> Type) :=
  {
    plus_empty_plus : Plus F;
    empty : forall A, F A;
    plus_empty_right_plus_identiry : forall A (f1 : F A),
        plus f1 (@empty A) = f1;
    plus_empty_left_plus_identiry : forall A (f1 : F A),
        plus (@empty A) f1 = f1
  }.

Class ApplicativePlus (F : Type -> Type) :=
  {
    applicative_plus_applicative : Applicative F;
    applicative_plus_plus_empty : PlusEmpty F
  }.

Class MonadPlus (F : Type -> Type) :=
  {
    monad_plus_monad : Monad F;
    moand_plus_bind := @monad_bind F monad_plus_monad;
    monad_plus_applicative := @monad_applicative F monad_plus_monad;
    monad_plus_apply := @applicative_apply F monad_plus_applicative;
    monad_plus_functor := @apply_functor F monad_plus_apply;
    monad_plus_applicative_plus : ApplicativePlus F;
    monad_plus_plus_empty := @applicative_plus_plus_empty F monad_plus_applicative_plus;
    monad_plus_empty_map : forall A (f : A -> A),
        map (@empty F monad_plus_plus_empty A) f = @empty F monad_plus_plus_empty A;
    monad_plus_left_zero : forall A (f : A -> F A),
        bind (@empty F monad_plus_plus_empty A) f = @empty F monad_plus_plus_empty A;
    monad_plus_right_zero : forall A (fa : F A),
        bind fa (fun _ => @empty F monad_plus_plus_empty A) = @empty F monad_plus_plus_empty A
  }.

Class Cobind (F : Type -> Type) :=
  {
    cobind_functor : Functor F;
    cobind : forall A B, F A -> (F A -> B) -> F B;
    cobind_associative : forall A B C (fa : F A) (f : F A -> B) (g : F B -> C),
        cobind fa (fun fa' => g (cobind fa' f)) = cobind (cobind fa f) g
  }.

Class Comonad (F : Type -> Type) :=
  {
    comonad_cobind : Cobind F;
    copoint : forall A, F A -> A;
    comonad_cobind_left_identity : forall A (fa : F A),
        cobind fa (@copoint A) = fa;
    comonad_cobind_right_identity : forall A B (fa : F A) (f : F A -> B),
        copoint (cobind fa f) = f fa
  }.

(** Instance Definitions *)

Require Import Coq.Logic.FunctionalExtensionality.
Require Import Coq.Program.Basics Coq.Program.Tactics.
Require Import Ssreflect.ssreflect.

(** ContT *)

(*** ContT is an instance of Functor *)

Definition ContT_map M R A B (fa : ContT M R A) (ab : A -> B) : ContT M R B :=
  mkIndexedContsT (fun f : Id (B -> M R) => runIndexedContsT fa (fun a => f (ab a))).

Arguments ContT_map M R A B / fa ab.

Program Instance ContT_Functor M R : Functor (ContT M R) :=
  {
    map := @ContT_map M R
  }.
Next Obligation.
  by case: fa.
Qed.

(*** ContT is an instance of Apply *)

Definition ContT_ap M R A B (fa : ContT M R A) (fab : ContT M R (A -> B)) : ContT M R B :=
  mkIndexedContsT (fun (f : Id (B -> M R)) =>
                     runIndexedContsT fab (fun ab =>
                                             runIndexedContsT fa (fun a => f (ab a)))).

Arguments ContT_ap M R A B / fa fab.

Program Instance ContT_Apply M R : Apply (ContT M R) :=
  {
    apply_functor := ContT_Functor M R;
    ap := @ContT_ap M R
  }.

(*** ContT is an instance of Applicative *)

Definition ContT_point M R A (a : A) : ContT M R A :=
  mkIndexedContsT (fun (f : Id (A -> M R)) => f a).

Arguments ContT_point M R A a.

Program Instance ContT_Applicative M R : Applicative (ContT M R) :=
  {
    applicative_apply := ContT_Apply M R;
    point := @ContT_point M R
  }.
Next Obligation.
  by case: fa.
Qed.

(** ContsT *)

(*** Tactics, Coercions, Axioms, etc *)

Coercion cobind_functor : Cobind >-> Functor.
Coercion comonad_cobind : Comonad >-> Cobind.
Definition comonad_functor W (CW : Comonad W) : Functor W := comonad_cobind.
Coercion comonad_functor : Comonad >-> Functor.

Coercion plus_empty_plus : PlusEmpty >-> Plus.

Ltac destruct_functor FW :=
  case: FW; move=> map_w f_map_id f_map_assoc /=.

Ltac destruct_cobind CW :=
  case: CW; case;
  move=> map_w f_map_id f_map_assoc cobind_w cb_assoc /=.

Ltac destruct_comonad CW :=
  case: CW; case; case;
  move=> map_w f_map_id f_map_assoc cobind_w cb_assoc copoint_w cm_left cm_right /=.

Ltac destruct_plus PM :=
  case: PM;
  move=> plus_m p_plus_assoc.

Ltac destruct_plus_empty PM :=
  case: PM; case;
  move=> plus_m p_plus_assoc empty_m pe_right pe_left.

Ltac fun_ext_move wf :=
  f_equal; apply: functional_extensionality=> wf /=.

(* TODO: axiom... *)
Axiom map_cobind_copoint : forall W (ComonadW : Comonad W) A B (w : W A) (f : A -> B),
    (* map f = cobind w (fun wa => f (copoint wa)) *)
    @map W ComonadW A B w f = @cobind W ComonadW A B w (fun wa => f (copoint wa)).

(*** ContsT is an instance of Functor *)

Definition ContsT_map W {FunctorW : Functor W} M R A B (fa : ContsT W M R A) (f : A -> B) : ContsT W M R B :=
  mkIndexedContsT (fun wf => runIndexedContsT fa (map wf (fun fb => fun a => fb (f a)))).

Arguments ContsT_map W FunctorW M R A B / fa f.

Program Instance ContsT_Functor W {FunctorW : Functor W}  M R : Functor (ContsT W M R) :=
  {
    map := @ContsT_map W FunctorW M R
  }.
Next Obligation.
  case: fa=> run.
  fun_ext_move wf.
  destruct_functor FunctorW.
  by rewrite f_map_id.
Qed.
Next Obligation.
  fun_ext_move wf.
  case: fa=> run /=.
  destruct_functor FunctorW.
  by rewrite f_map_assoc.
Qed.

(*** ContsT is an instance of Apply *)

Definition ContsT_ap W {CobindW : Cobind W} M R A B
           (fa : ContsT W M R A)
           (fab : ContsT W M R (A -> B)) : ContsT W M R B :=
  let FunctorW := cobind_functor in
  mkIndexedContsT
    (fun wf =>
       runIndexedContsT
         fab
         (cobind wf (fun wf f =>
                       runIndexedContsT
                         fa
                         (map wf (fun f' a => f' (f a)))))).

Arguments ContsT_ap W CobindW M R A B / fa fab.

Program Instance ContsT_Apply W {ComonadW : Comonad W} M R : Apply (ContsT W M R) :=
  {
    apply_functor := @ContsT_Functor W ComonadW M R;
    ap := @ContsT_ap W ComonadW M R
  }.
Next Obligation.
  fun_ext_move wf.
  f_equal.
  move: (map_cobind_copoint ComonadW).
  destruct_comonad ComonadW=> map_def.
  rewrite !map_def =>/=.
Admitted.

(*** ContsT is an instance of Applicative *)

Definition ContsT_point W {ComonadW : Comonad W} M R A (a : A) : ContsT W M R A :=
  mkIndexedContsT (fun wf => copoint wf a).

Arguments ContsT_point W ComonadW M R A / a.

Definition cojoin W {CobindW : Cobind W} A (wa :W A) : W (W A) :=
  cobind wa (fun a => a).

Program Instance ContsT_Applicative W {ComonadW : Comonad W} M R : Applicative (ContsT W M R) :=
  {
    applicative_apply := @ContsT_Apply W ComonadW M R;
    point := @ContsT_point W ComonadW M R
  }.
Next Obligation.
  case: fa=> run.
  fun_ext_move wf.
  destruct_comonad ComonadW.
  rewrite cm_right.
  by rewrite f_map_id.
Qed.
Next Obligation.
  fun_ext_move wf.
  move: (map_cobind_copoint ComonadW).
  destruct_comonad ComonadW.
  rewrite cm_right.
  move=> -> /=.
  by rewrite cm_right.
Qed.
Next Obligation.
  fun_ext_move wf.
  move: (map_cobind_copoint ComonadW).
  destruct_comonad ComonadW=> map_def.
  rewrite cm_right.
  rewrite map_def.
  f_equal.
  fun_ext_move wf'.
  fun_ext_move ab.
  by rewrite map_def cm_right.
Qed.
Next Obligation.
  fun_ext_move wf.
  move: (map_cobind_copoint ComonadW).
  destruct_comonad ComonadW=> map_def.
  by rewrite cm_right.
Qed.

(*** ContsT is an instance of Bind *)

Definition ContsT_bind W {CobindW : Cobind W} M R A B
           (fa : ContsT W M R A)
           (f : A -> ContsT W M R B) : ContsT W M R B :=
  mkIndexedContsT (fun wf =>
                     runIndexedContsT fa (cobind wf (fun wa =>
                                                       fun a =>
                                                         runIndexedContsT (f a) wa))).

Arguments ContsT_bind W CobindW M R A B / fa f.

Program Instance ContsT_Bind W {ComonadW : Comonad W} M R : Bind (ContsT W M R) :=
  {
    bind_apply := @ContsT_Apply W ComonadW M R;
    bind := @ContsT_bind W ComonadW M R
  }.
Next Obligation.
  fun_ext_move wf.
  f_equal.
  destruct_comonad ComonadW.
  by rewrite -cb_assoc.
Qed.

(*** ContsT is an instance of Monad *)

Program Instance ContsT_Monad W {ComonadW : Comonad W} M R : Monad (ContsT W M R) :=
  {
    monad_applicative := @ContsT_Applicative W ComonadW M R;
    monad_bind := @ContsT_Bind W ComonadW M R
  }.
Next Obligation.
  case: fa=> run.
  fun_ext_move wf.
  destruct_comonad ComonadW.
  by move: (cm_left (A -> M R) wf); rewrite/cobind=> ->.
Qed.
Next Obligation.
  case H : (f a) =>[run].
  fun_ext_move wf.
  destruct_comonad ComonadW.
  rewrite cm_right.
  by rewrite H.
Qed.

(*** ContsT is an instance of Plus *)

Definition ContsT_plus W M {PlusM : Plus M} R A (fa1 fa2 : ContsT W M R A) : ContsT W M R A :=
  mkIndexedContsT (fun wf : W (A -> M R) =>
                     plus (runIndexedContsT fa1 wf) (runIndexedContsT fa2 wf)).

Arguments ContsT_plus W M PlusM R A / fa1 fa2.

Program Instance ContsT_Plus W M {PlusM : Plus M} R : Plus (ContsT W M R) :=
  {
    plus := @ContsT_plus W M PlusM R
  }.
Next Obligation.
  destruct_plus PlusM.
  fun_ext_move wf.
  by rewrite p_plus_assoc.
Qed.

(*** ContsT is an instance of PlusEmpty *)

Definition ContsT_empty W M {PlusEmptyM : PlusEmpty M} R A : ContsT W M R A :=
  mkIndexedContsT (fun _ : W (A -> M R) => @empty M PlusEmptyM R).

Arguments ContsT_empty W M PlusEmptyM R A /.

Program Instance ContsT_PlusEmpty W M {PlusEmptyM : PlusEmpty M} R : PlusEmpty (ContsT W M R) :=
  {
    plus_empty_plus := @ContsT_Plus W M PlusEmptyM R;
    empty := @ContsT_empty W M PlusEmptyM R
  }.
Next Obligation.
  case: f1=> run.
  fun_ext_move wf.
  destruct_plus_empty PlusEmptyM.
  by rewrite pe_right.
Qed.
Next Obligation.
  case: f1=> run.
  fun_ext_move wf.
  destruct_plus_empty PlusEmptyM.
  by rewrite pe_left.
Qed.

(*** ContsT is an instance of ApplicativePlus *)

Program Instance ContsT_ApplicativePlus W {ComonadW : Comonad W} M {PlusEmptyM : PlusEmpty M} R : ApplicativePlus (ContsT W M R) :=
  {
    applicative_plus_applicative := @ContsT_Applicative W ComonadW M R;
    applicative_plus_plus_empty := @ContsT_PlusEmpty W M PlusEmptyM R
  }.

(*** ContsT is an instance of MonadPlus *)

Program Instance ContsT_MonadPlus W {ComonadW : Comonad W} M {PlusEmptyM : PlusEmpty M} R : MonadPlus (ContsT W M R) :=
  {
    monad_plus_monad := @ContsT_Monad W ComonadW M R;
    monad_plus_applicative_plus := @ContsT_ApplicativePlus W ComonadW M PlusEmptyM R
  }.
Next Obligation.
  fun_ext_move wf.
  case: fa=> run /=.
  destruct_comonad ComonadW.
  destruct_plus_empty PlusEmptyM.
  rewrite/empty.
  (* impossible *)
  (* run がなにか適当な値を返すなら成り立たない *)
Admitted.




(** Counter Example of ContsT/monad_plus_right_zero *)

(*** Id is an instance of Comonad *)
Definition Id_map A B (a : Id A) (f : A -> B) : Id B := f a.
Program Instance Id_Functor : Functor Id :=
  {
    map := Id_map
  }.
Definition Id_cobind A B (a : Id A) (f : Id A -> B) : Id B := f a.
Program Instance Id_Cobind : Cobind Id :=
  {
    cobind := Id_cobind
  }.
Definition Id_copoint A (a : Id A) : A := a.
Program Instance Id_Comonad : Comonad Id :=
  {
    copoint := Id_copoint
  }.

(*** list is an instance of PlusEmpty *)
Require Import Lists.List.
Definition list_plus A (l1 l2 : list A) : list A := app l1 l2.
Arguments list_plus A / l1 l2.
Program Instance list_Plus : Plus list :=
  {
    plus := list_plus
  }.
Next Obligation.
  by rewrite app_assoc.
Qed.
Definition list_empty A : list A := nil.
Arguments list_empty A /.
Program Instance list_PlusEmpty : PlusEmpty list :=
  {
    empty := list_empty
  }.
Next Obligation.
  by rewrite app_nil_r.
Qed.

(*** Proof of counter example *)
(* ContsT Id list nat  *)
Theorem MonadPlus_right_zero_ContsT_counter_example A B :
  @bind (ContsT Id list nat)
        (@ContsT_Bind Id Id_Comonad list nat)
        A B
        (mkIndexedContsT (fun _ : Id (A -> list nat) => 1 :: nil)) (fun _ : A => empty B)
  <> empty B.
Proof.
  rewrite/bind/empty/=.
  case; move/equal_f.
  move/(_ (fun _ => nil))=> contra.
  inversion contra.
Qed.