Library SSProve.Mon.MonadExamples
From Stdlib Require Import ssreflect List.
From SSProve.Mon Require Export Base.
From SSProve.Mon Require Import SPropBase SPropMonadicStructures Monoid.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Set Primitive Projections.
Set Universe Polymorphism.
(* The identity monad *)
Program Definition Identity : Monad :=
@mkMonad (fun X ⇒ X) (fun _ x ⇒ x) (fun X Y x f ⇒ f x) _ _ _.
(* The identity monad has a monad morphism to any other monad *)
Section IdentityInitial.
Context (M:Monad).
Program Definition ret_mmorph : MonadMorphism Identity M :=
@mkMorphism _ _ (@ret M) _ _.
Next Obligation. rewrite /bind monad_law1 //. Qed.
(* We just prove the existence, not the unicity... *)
End IdentityInitial.
Section State.
Context (S: Type).
Program Definition St : Monad :=
@mkMonad (fun X ⇒ S → X × S) (fun A a s ⇒ ⟨a, s⟩)
(fun A B m f s ⇒ let ms := m s in f (nfst ms) (nsnd ms))
_ _ _.
Definition get : St S := fun s ⇒ ⟨s, s⟩.
Definition put (s:S) : St unit := fun s0 ⇒ ⟨tt, s⟩.
End State.
Section Update.
Context (M:monoid) (X:monoid_action M).
Definition UpdFromLaws pf1 pf2 pf3 : Monad :=
@mkMonad (fun A ⇒ X → A × M) (fun A a x ⇒ ⟨a, e M⟩)
(fun A B m f x ⇒ let mx := m x in
let fx := f (nfst mx) (nsnd mx ⧕ x) in
⟨nfst fx, nsnd fx ⋅ nsnd mx⟩) pf1 pf2 pf3.
Program Definition Upd : Monad :=
UpdFromLaws _ _ _.
Next Obligation.
apply boolp.funext ⇒ x ; rewrite monact_unit monoid_law2 //.
Qed.
Next Obligation.
apply boolp.funext ⇒ x; rewrite monoid_law1 //.
Qed.
Next Obligation.
apply boolp.funext ⇒ x. rewrite - !monact_mult !monoid_law3 //.
Qed.
End Update.
Section FreeMonad.
(* A signature where S is the type of operations and P describes the
arity of each operations *)
Context (S : Type) (P : S → Type).
Inductive FreeF A : Type :=
| retFree : A → FreeF A
| opr : ∀ s, (P s → FreeF A) → FreeF A.
Arguments opr [A] _ _.
Fixpoint bindFree A B (c : FreeF A) (f : A → FreeF B) : FreeF B :=
match c with
| retFree a ⇒ f a
| opr s k ⇒ opr s (fun p ⇒ bindFree (k p) f)
end.
Program Definition Free : Monad :=
@mkMonad FreeF retFree bindFree _ _ _.
Next Obligation.
elim c ⇒ //= ? ? IH ; f_equal ; apply boolp.funext ⇒ p ; apply IH.
Qed.
Next Obligation.
elim c ⇒ //= ? ? IH ; f_equal ; apply boolp.funext ⇒ p ; apply IH.
Qed.
Definition op (s : S) : Free (P s) :=
opr s (@retFree _).
Definition trace := list { s : S & P s }.
Program Definition from_free (M:Monad) (f:∀ s, M (P s))
: MonadMorphism Free M :=
@mkMorphism _ _
(fix from_free A (m:Free A) {struct m} :=
match m return M A with
| retFree a ⇒ ret a
| opr s k ⇒ bind (f s) (fun x ⇒ from_free A (k x))
end
) _ _.
Next Obligation.
induction m⇒ //=.
rewrite /bind monad_law1 //.
rewrite /bind monad_law3.
f_equal. apply boolp.funext ⇒ a. apply H.
Qed.
End FreeMonad.
Section Partiality.
Inductive DivS := Omega.
Definition DivAr : DivS → Type := fun 'Omega ⇒ False.
Definition Div := @Free DivS DivAr.
Definition Ω : Div False := op _ Omega.
End Partiality.
Section Exceptions.
Context (E:Type).
Inductive ExnS := Raise of E.
Definition ExnAr : ExnS → Type := fun '(Raise _) ⇒ False.
Definition Exn := @Free ExnS ExnAr.
Definition raise : E → Exn False := fun e ⇒ op _ (Raise e).
Definition catch {A} (m : Exn A) (merr : E → Exn A) : Exn A :=
match m with
| retFree a ⇒ m
| @opr _ _ _ (Raise e) _ ⇒ merr e
end.
End Exceptions.
Section NonDeterminismSet.
Import SPropNotations SPropAxioms.
Program Definition NDSet : Monad :=
@mkMonad (fun X ⇒ X → Prop)
(fun X x ⇒ fun x' ⇒ x = x')
(fun X Y c f ⇒ fun y ⇒ ∃ x, c x ∧ f x y) _ _ _.
Next Obligation.
apply boolp.funext ⇒ y; apply sprop_ext; do 2 split.
+ intros [x [eq H]]; induction eq⇒ //.
+ intro; ∃ a; intuition.
Qed.
Next Obligation.
apply boolp.funext ⇒ y; apply sprop_ext; do 2 split.
+ intros [x [H eq]]. induction eq⇒ //.
+ intro. ∃ y. intuition.
Qed.
Next Obligation.
apply boolp.funext ⇒ y; apply sprop_ext; do 2 split.
+ intros [b [[a [H1 H2]] H3]].
eexists ; split ; [|eexists;split]; eassumption.
+ intros [a [H1 [b [H2 H3]]]].
eexists ; split ; [eexists;split|]; eassumption.
Qed.
Definition pick_set : NDSet bool := fun b ⇒ True.
End NonDeterminismSet.
Section NonDeterminismList.
Lemma concat_map_nil : ∀ A (l : list A),
concat (List.map (fun x ⇒ x :: nil) l) = l.
Proof.
induction l.
- reflexivity.
- simpl. rewrite IHl. reflexivity.
Qed.
Program Definition ListM : Monad :=
@mkMonad (fun A ⇒ list A)
(fun A a ⇒ a :: nil)
(fun A B m f ⇒ concat (List.map f m)) _ _ _.
Next Obligation. apply app_nil_r. Qed.
Next Obligation. apply concat_map_nil. Qed.
Next Obligation.
induction c⇒ //=.
rewrite map_app concat_app IHc //.
Qed.
Definition choose {A} (l : list A) : ListM A := l.
Definition pick : ListM bool := true :: false :: nil.
End NonDeterminismList.
Section IO.
Context (Inp Oup : Type).
Inductive IOS : Type := Read : IOS | Write : Oup → IOS.
Definition IOAr (op : IOS) : Type :=
match op with
| Read ⇒ Inp
| Write _ ⇒ unit
end.
Definition IO := @Free IOS IOAr.
Definition read : IO Inp := op _ Read.
Definition write (o:Oup) : IO unit := op _ (Write o).
End IO.
From SSProve.Mon Require Export Base.
From SSProve.Mon Require Import SPropBase SPropMonadicStructures Monoid.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Set Primitive Projections.
Set Universe Polymorphism.
(* The identity monad *)
Program Definition Identity : Monad :=
@mkMonad (fun X ⇒ X) (fun _ x ⇒ x) (fun X Y x f ⇒ f x) _ _ _.
(* The identity monad has a monad morphism to any other monad *)
Section IdentityInitial.
Context (M:Monad).
Program Definition ret_mmorph : MonadMorphism Identity M :=
@mkMorphism _ _ (@ret M) _ _.
Next Obligation. rewrite /bind monad_law1 //. Qed.
(* We just prove the existence, not the unicity... *)
End IdentityInitial.
Section State.
Context (S: Type).
Program Definition St : Monad :=
@mkMonad (fun X ⇒ S → X × S) (fun A a s ⇒ ⟨a, s⟩)
(fun A B m f s ⇒ let ms := m s in f (nfst ms) (nsnd ms))
_ _ _.
Definition get : St S := fun s ⇒ ⟨s, s⟩.
Definition put (s:S) : St unit := fun s0 ⇒ ⟨tt, s⟩.
End State.
Section Update.
Context (M:monoid) (X:monoid_action M).
Definition UpdFromLaws pf1 pf2 pf3 : Monad :=
@mkMonad (fun A ⇒ X → A × M) (fun A a x ⇒ ⟨a, e M⟩)
(fun A B m f x ⇒ let mx := m x in
let fx := f (nfst mx) (nsnd mx ⧕ x) in
⟨nfst fx, nsnd fx ⋅ nsnd mx⟩) pf1 pf2 pf3.
Program Definition Upd : Monad :=
UpdFromLaws _ _ _.
Next Obligation.
apply boolp.funext ⇒ x ; rewrite monact_unit monoid_law2 //.
Qed.
Next Obligation.
apply boolp.funext ⇒ x; rewrite monoid_law1 //.
Qed.
Next Obligation.
apply boolp.funext ⇒ x. rewrite - !monact_mult !monoid_law3 //.
Qed.
End Update.
Section FreeMonad.
(* A signature where S is the type of operations and P describes the
arity of each operations *)
Context (S : Type) (P : S → Type).
Inductive FreeF A : Type :=
| retFree : A → FreeF A
| opr : ∀ s, (P s → FreeF A) → FreeF A.
Arguments opr [A] _ _.
Fixpoint bindFree A B (c : FreeF A) (f : A → FreeF B) : FreeF B :=
match c with
| retFree a ⇒ f a
| opr s k ⇒ opr s (fun p ⇒ bindFree (k p) f)
end.
Program Definition Free : Monad :=
@mkMonad FreeF retFree bindFree _ _ _.
Next Obligation.
elim c ⇒ //= ? ? IH ; f_equal ; apply boolp.funext ⇒ p ; apply IH.
Qed.
Next Obligation.
elim c ⇒ //= ? ? IH ; f_equal ; apply boolp.funext ⇒ p ; apply IH.
Qed.
Definition op (s : S) : Free (P s) :=
opr s (@retFree _).
Definition trace := list { s : S & P s }.
Program Definition from_free (M:Monad) (f:∀ s, M (P s))
: MonadMorphism Free M :=
@mkMorphism _ _
(fix from_free A (m:Free A) {struct m} :=
match m return M A with
| retFree a ⇒ ret a
| opr s k ⇒ bind (f s) (fun x ⇒ from_free A (k x))
end
) _ _.
Next Obligation.
induction m⇒ //=.
rewrite /bind monad_law1 //.
rewrite /bind monad_law3.
f_equal. apply boolp.funext ⇒ a. apply H.
Qed.
End FreeMonad.
Section Partiality.
Inductive DivS := Omega.
Definition DivAr : DivS → Type := fun 'Omega ⇒ False.
Definition Div := @Free DivS DivAr.
Definition Ω : Div False := op _ Omega.
End Partiality.
Section Exceptions.
Context (E:Type).
Inductive ExnS := Raise of E.
Definition ExnAr : ExnS → Type := fun '(Raise _) ⇒ False.
Definition Exn := @Free ExnS ExnAr.
Definition raise : E → Exn False := fun e ⇒ op _ (Raise e).
Definition catch {A} (m : Exn A) (merr : E → Exn A) : Exn A :=
match m with
| retFree a ⇒ m
| @opr _ _ _ (Raise e) _ ⇒ merr e
end.
End Exceptions.
Section NonDeterminismSet.
Import SPropNotations SPropAxioms.
Program Definition NDSet : Monad :=
@mkMonad (fun X ⇒ X → Prop)
(fun X x ⇒ fun x' ⇒ x = x')
(fun X Y c f ⇒ fun y ⇒ ∃ x, c x ∧ f x y) _ _ _.
Next Obligation.
apply boolp.funext ⇒ y; apply sprop_ext; do 2 split.
+ intros [x [eq H]]; induction eq⇒ //.
+ intro; ∃ a; intuition.
Qed.
Next Obligation.
apply boolp.funext ⇒ y; apply sprop_ext; do 2 split.
+ intros [x [H eq]]. induction eq⇒ //.
+ intro. ∃ y. intuition.
Qed.
Next Obligation.
apply boolp.funext ⇒ y; apply sprop_ext; do 2 split.
+ intros [b [[a [H1 H2]] H3]].
eexists ; split ; [|eexists;split]; eassumption.
+ intros [a [H1 [b [H2 H3]]]].
eexists ; split ; [eexists;split|]; eassumption.
Qed.
Definition pick_set : NDSet bool := fun b ⇒ True.
End NonDeterminismSet.
Section NonDeterminismList.
Lemma concat_map_nil : ∀ A (l : list A),
concat (List.map (fun x ⇒ x :: nil) l) = l.
Proof.
induction l.
- reflexivity.
- simpl. rewrite IHl. reflexivity.
Qed.
Program Definition ListM : Monad :=
@mkMonad (fun A ⇒ list A)
(fun A a ⇒ a :: nil)
(fun A B m f ⇒ concat (List.map f m)) _ _ _.
Next Obligation. apply app_nil_r. Qed.
Next Obligation. apply concat_map_nil. Qed.
Next Obligation.
induction c⇒ //=.
rewrite map_app concat_app IHc //.
Qed.
Definition choose {A} (l : list A) : ListM A := l.
Definition pick : ListM bool := true :: false :: nil.
End NonDeterminismList.
Section IO.
Context (Inp Oup : Type).
Inductive IOS : Type := Read : IOS | Write : Oup → IOS.
Definition IOAr (op : IOS) : Type :=
match op with
| Read ⇒ Inp
| Write _ ⇒ unit
end.
Definition IO := @Free IOS IOAr.
Definition read : IO Inp := op _ Read.
Definition write (o:Oup) : IO unit := op _ (Write o).
End IO.