(************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) (* eqβ)%signature. *) Class Monad `{pointed : Pointed η} := { join : Π {α}, η (η α) --> η α ; (* Natural transformations. *) fmap_join : Π {α β} (f : α --> β), fmap f ∙ join =∙= join ∙ fmap (fmap f) ; (* Monad laws *) join_fmap_point : Π {α}, join ∙ fmap point =∙= (@idS (η α)) ; join_point : Π {α}, join ∙ (point (α:=η α)) =∙= idS ; join_fmap : Π {α}, join ∙ (@join (η α)) =∙= join ∙ fmap (@join α) }. Implicit Arguments Monad [[F] [pointed]]. Definition bind `{M : Monad η} {α β} (a : η α) (f : α ---> η β) : η β := join (fmap f a). Instance bind_morphism `{M : Monad η} {α β : Setoid} : Proper (η α ==> (α ===> η β) ==> η β) bind. Proof. intros. do 3 red ; intros. unfold bind. rewrite H, H0. reflexivity. Qed. Program Definition bindM `{M : Monad η} {α β : Setoid} : η α --> (α ---> η β) ---> η β := mkMap2 bind. Ltac reflex := match goal with | [ |- @Proper _ _ _ ] => typeclasses eauto | [ |- ?R ?x ?y ] => change (Proper R x) ; typeclasses eauto end. Lemma bind_point_left `{Monad η} {α β} x (f : α --> η β) : bind (point x) f == f x. Proof. intros. unfold bind. pose (fmap_point f x). rewrite s. pose (join_point (f x)). rewrite s0. reflexivity. Qed. Lemma bind_point_right `{m : Monad η} α (x : η α) : bind x point == x. Proof. intros. unfold bind. pose (join_fmap_point x). rewrite s. reflexivity. Qed. Instance join_params : Params (@join) 5. Instance fmap_params : Params (@fmap) 4. Instance pequiv_params : Params (@pequiv) 3. (*Lemma lambda_morphism [ pα : PER α R ] [ pβ : PER β R' ] (f : α -> β) (H : forall (x y : α), R x y -> R' (f x) (f y)) : Morphism (R ==> R') (λ x : α, f x). Proof with auto. intros. simpl_relation. Qed. Ltac lambda_morphism_tactic := match goal with [ |- @Morphism _ _ (λ x, _) ] => eapply @lambda_morphism end. Hint Extern 4 (@Morphism _ _ _) => lambda_morphism_tactic : typeclass_instances.*) (* How to prove (automatically): Morphism (eqα ==> feq (feq eqδ)) (fun x0 : α => fmap g (f x0)) ? *) (* Program Definition bind_assoc_stmt [ M : Monad η ] {α β δ} (x : η α) (f : α --> η β) (g : β --> η δ) := *) (* bind x (fun a : α => bind (f a) g) =∙= bind (bind x f) g. *) (* Next Obligation. *) (* Proof. intros a a' Haa'. rewrite Haa' ; reflexivity. Qed. *) (* Lemma bind_assoc [ M : Monad η ] {α β δ} (x : η α) (f : α --> η β) (g : β --> η δ) : *) (* bind_assoc_stmt x f g. *) (* Proof with try typeclasses eauto. intros. red. *) (* unfold bind. *) (* rewrite (fmap_join g (fmap f x))... *) (* rewrite (join_fmap (fmap (fmap g) (fmap f x)))... *) (* unfold composeS; simpl. unfold compose. *) (* rewrite <- (fmap_compose (fmap g) f x)... *) (* rewrite <- (fmap_compose join (fmap g ∙ f) x)... *) (* unfold composeS, compose ; simpl. *) (* clear_subset_proofs. unfold compose, bind in *. clear_subset_proofs. reflexivity. *) (* Qed. *) (* Hint Resolve @bind_point_left @bind_point_right @bind_assoc : monad. *) Notation "T >>= U" := (bindM T U) (at level 55). Notation "T >> U" := (bindM T (constS U)) (at level 55). Notation "x <- T ;; E" := (bindM T (mkMap (fun x => E))) (at level 30, T at next level, right associativity). Notation "'return' t" := (point t) (at level 20) : monad. Open Local Scope monad. Obligation Tactic := program_simplify ; try typeclasses eauto. Require Import Datatypes. Require Import Prelude.List. Definition unit_equivalence (x y : unit) := True. Instance unit_equiv_equiv : Equivalence unit_equivalence. Proof. constructor ; red ; intros ; firstorder. Qed. Definition unit_setoid : Setoid := mkSetoid _ unit_equivalence _. Program Instance const_functor (S : Setoid) : Functor (const S) := { fmap α β := flipS constS }. Obligation Tactic := idtac. (* Instance reflexive_pointwise {A} `(Reflexive B R) : Reflexive (pointwise_relation A R). *) (* Proof. intros. intro. intro y. reflexivity. Qed. *) Next Obligation. intros. intro ; reflexivity. Qed. Next Obligation. intros. intro ; reflexivity. Qed. Definition bool_setoid : Setoid := mkSetoid bool eq _. Section Monad_Defs. Context `{mon : Monad m}. Program Definition ap {α β} (f : α ---> β) (x : m α) : m β := bindM x (composeS point f). Program Definition apS {α β} : (α ---> β) ---> m α ---> m β := mkMap2 ap. Next Obligation. Proof. unfold ap. intros. intros f g Hfg ma ma' Hmaa'. rewrite Hmaa', Hfg. reflexivity. Qed. Program Definition seq {a b} (x : m a) (y : m b) : m b := x >> y. Program Definition liftM2 {a b r} (f : a --> b ---> r) : m a -> m b -> m r := fun x y => a <- x ;; b <- y ;; return (f a b). Solve Obligations using program_simpl ; simpl_morph. Next Obligation. Proof. intros. intros a1 a2 Ha. simpl. apply bind_morphism. reflexivity. intro. simpl. rewrite Ha. reflexivity. Qed. (** Definition liftM3 {a b c r} (f : a -> b -> c -> r) : m a -> m b -> m c -> m r := fun x y z => a <- x ;; b <- y ;; c <- z ;; return (f a b c). Definition liftM4 {a b c d r} (f : a -> b -> c -> d -> r) : m a -> m b -> m c -> m d -> m r := fun x y z w => a <- x ;; b <- y ;; c <- z ;; d <- w ;; return (f a b c d). Definition liftM5 {a b c d e r} (f : a -> b -> c -> d -> e -> r) : m a -> m b -> m c -> m d -> m e -> m r := fun x y z w v => a <- x ;; b <- y ;; c <- z ;; d <- w ;; e <- v ;; return (f a b c d e). *) Obligation Tactic := program_simpl ; simpl_morph. Program Lemma do_return_eta : Π α (u : m α), x <- u ;; return x === u. Proof. intros ; clear_subset_proofs. simpl. transitivity (bind u point). apply bind_morphism; repeat intro; reflexivity. apply (bind_point_right _ u). Qed. Program Fixpoint sequence {a} (l : list_setoid (m a)) { struct l } : m (list_setoid a) := match l with | nil => point (nil:list_setoid a) | hd :: tl => x <- hd ;; r <- sequence tl ;; return (x :: r) end. Next Obligation. Proof. program_simpl. clear_subset_proofs. apply @bind_morphism ; try reflexivity. simpl_morph. now constructor ; auto. Defined. (* Fixpoint sequence_ {a} (l : list (m a)) { struct l } : m unit := *) (* match l with *) (* | nil => return tt *) (* | hd :: tl => hd >> (sequence_ tl) *) (* end. *) Instance sequence_mor a : Proper (list_setoid (m a) ==> m (list_setoid a)) sequence. Proof with auto. unfold sequence. intros a x y Hxy. induction Hxy. reflexivity. fold @sequence in *. simpl. apply @bind_morphism... simpl_morph. apply @bind_morphism... simpl_morph. Qed. Program Definition mapM {a b} (f : a --> m b) : list_setoid a -> m (list_setoid b) := sequence ∘ fmap f. Program Definition mapMS {a b} : (a ---> m b) ---> list_setoid a ---> m (list_setoid b) := mkMap2 mapM. Next Obligation. intros ; simpl_morph. unfold mapM. unfold composeS ; clear_subset_proofs. simpl @Map_fn. unfold compose. rewrite Hxy, Hxy0. reflexivity. Qed. (* Definition mapM_ {a b} (f : a -> m b) : list a -> m unit := *) (* sequence_ ∘ map f. *) (* Definition dnib {a b} (f : a -> m b) (x : m a) : m b := x >>= f. *) (* Definition compM {a b c} (f : a -> m b) (g : b -> m c) (a : a) : m c := *) (* x <- f a ;; g x. *) (* Definition Mcomp {a b c} (g : b -> m c) (f : a -> m b) (a : a) : m c := *) (* x <- f a ;; g x. *) Definition when (x : bool) (e : m unit_setoid) : m unit_setoid := if x then e else return (tt:unit_setoid). Instance when_mor : Proper (bool_setoid ==> m unit_setoid ==> m unit_setoid) when. Proof. simpl_morph. subst. unfold when. destruct y ; auto. reflexivity. Qed. Program Definition whenS : bool_setoid --> m unit_setoid ---> m unit_setoid := mkMap2 when. Definition unless (x : bool) := when (negb x). End Monad_Defs. Hint Resolve @do_return_eta : monad. (* Notation "T =<< U" := (dnib T U) (at level 55). *) (* Notation "T >=> U" := (compM T U) (at level 55). *) (* Notation "T <=< U" := (Mcomp T U) (at level 55). *) (* Require Import Prelude.Applicative. Program Instance ap_morphism [ mon : Monad η, PER α eqα, PER β eqβ ] : Morphism ((eqα ==> eqβ) ==> feq eqα ==> feq eqβ) Top.ap. Next Obligation. Proof. unfold Top.ap. do 2 red ; intros. apply (bind_morphism _ _ H0). red ; intros. apply @point_morphism ; auto. Qed. Lemma per_refl_left [ PER α eqα ] (x y : α) (H : eqα x y) : Morphism eqα x. Proof. simpl_relation. transitivity y ; [ | symmetry ] ; assumption. Qed. Lemma per_refl_right [ PER α eqα ] (x y : α) (H : eqα x y) : Morphism eqα y. Proof. simpl_relation. transitivity x ; [ symmetry | ] ; assumption. Qed. Program Instance monad_applicative [ mon : Monad i ] : ! Applicative i := ap α β a x := f <- a ;; Top.ap f x. Next Obligation. Proof. do 3 red ; intros. apply (bind_morphism _ _ H1). red ; intros. apply (ap_morphism _ _ H3 _ _ H2). Qed. Next Obligation. Proof. intros x xmor. unfold Top.ap. About bind_point_left. pose (bind_point_left (eqα:=eq) (eqβ:=eq) f (f:=λ f0, a <- x;; return f0 a)). rewrite p. setoid_rewrite bind_point_left. Set Printing All. intros. About bind_point_left. Set Printing All. unfold ap. rewrite (bind_point_left (x:=f) (f:=λ f0, Top.ap f0 x)). Print bind_point_left. Print respectful_eq_default. Set Printing All. intros. Typeclasses eauto := debug 4. Print bind_point_left. pose (bind_point_left (x:=f)). unfold id ; simpl. apply do_return_eta. Qed. Next Obligation. Proof. rewrite bind_point_left. do 2 rewrite <- bind_assoc. apply bind_eq_l. extensionality x. rewrite bind_point_left. do 2 rewrite <- bind_assoc. apply bind_eq_l. extensionality y. rewrite bind_point_left. rewrite <- bind_assoc. apply bind_eq_l ; extensionality z. rewrite bind_point_left. auto. Qed. Next Obligation. intros. repeat rewrite bind_point_left. reflexivity. Qed. Next Obligation. (* interchange *) Proof. intros. rewrite bind_point_left. apply bind_eq_l ; extensionality y. rewrite bind_point_left. reflexivity. Qed. *)