Commits

Dmitry Grebeniuk  committed d74ea76 Draft

.

  • Participants
  • Parent commits b40599e

Comments (0)

Files changed (5)

 \.(vo|glob)$
+\.old$
+~$

File ErrorMonad.v

-Require Import Monads.
-
-Require Import FunctionalExtensionality.
-
-
-Inductive resG (e : Type) (a : Type) :=
-  | Ok : a -> resG e a
-  | Error : e -> resG e a
-.
-
-Definition resT e {m : Type -> Type} (M : Monad m) a :=
-  m (resG e a).
-
-Definition res e := resT e Identity.
-
-Implicit Arguments Ok [e a].
-Implicit Arguments Error [e a].
-
-
-Class ErrorMonadT
-(e : Type)
-{m : Type -> Type}
-(M : Monad m)
-:=
-  { throw : forall {a : Type},
-      e -> res e (m a)
-  ; catch : forall {a : Type},
-      res e (m a) -> (e -> res e (m a)) -> res e (m a)
-  }
-.
-
-Instance ErrorT
-(e : Type)
-{m : Type -> Type}
-(M : Monad m)
-: ErrorMonadT e M
-:=
-  {| throw := fun {a : Type} (err : e) =>
-       Error err
-   ; catch := fun
-       {a : Type}
-       (ra : res e (m a))
-       (handler : e -> res e (m a)) =>
-         match ra with
-         | Ok r => Ok r
-         | Error r => handler r
-         end
-   |}.
-
-
-Instance ErrorT_Monad_inst
-  (e : Type)
-  {m : Type -> Type}
-  (M : Monad m)
-: Monad (resT e M)
-:=
-  {| ret := fun {A} (a : A) => ret (Ok a)
-   ; bind := fun
-       {A B}
-       (ma : resT e M A)
-       (f : A -> resT e M B) =>
-         (ma : m (res e A)) >>= fun (a : res e A) =>
-         match a with
-         | Ok r => f r
-         | Error r => ret (Error r)
-         end
-   |}
-.
-(* 0 *)
-  intros. rewrite Monad0. reflexivity.
-(* 1 *)
-  intros. unfold resT in *. rewrite <- Monad1.
-  f_equal. extensionality q. destruct q; reflexivity.
-(* 2 *)
-  intros. unfold resT in *.
-  rewrite Monad2.
-  f_equal. extensionality q.
-  destruct q.
-  (* 2.1 *)
-    reflexivity.
-  (* 2.2 *)
-    rewrite Monad0.
-    reflexivity.
-Defined.
-
-
-Instance ErrorT_MonadTrans_inst
-  (e : Type)
-  {m : Type -> Type}
-  {M : Monad m}
-: MonadTrans (@resT e)
-:=
-  {| lift := fun {A} ma =>
-       a <- ma;;
-       ret (Ok a)
-   |}
-.
-(* T0 *)
-  intros. extensionality q. rewrite Monad0. simpl. reflexivity.
-(* T1 *)
-  intros. simpl.
-  rewrite Monad2.
-  rewrite Monad2.
-  f_equal.
-  extensionality q.
-  rewrite Monad0.
-  reflexivity.
-Defined.
-
-
-Module Example.
-
-  Require Import StateMonad.
-
-  Inductive myerr :=
-    | Zero
-    | Empty
-  .
-
-  Require Import Eqdec.
-
-  Fixpoint test1_aux lst : res myerr nat :=
-    match lst with
-    | nil => ret 0
-    | cons h t =>
-        if eq_dec h 0
-        then throw Zero
-        else rest <- test1_aux t;; ret (h + rest)
-    end
-  .
-
-  Notation "f $ x" := (f x)
-    (at level 63, right associativity, only parsing).
-
-  Require Import List.
-
-  Definition test1 (lst : list nat) : res myerr (list nat) :=
-    if eq_dec lst nil
-    then throw Empty (M := Identity)
-    else
-      h <- test1_aux lst;;
-      ret $ h :: lst
-  .
-
-  Eval compute in test1 (1 :: 2 :: 3 :: nil).
-  Eval compute in test1 (1 :: 0 :: 3 :: nil).
-  Eval compute in test1 nil.
-
-Check test1.
-
-
-Typeclasses eauto := debug bfs.
-
-  Definition test2
- : resT myerr (@StateT_Monad_inst bool identity_type Identity) (list nat)
-   :=
-    lift $ (put true);;
-    r <-
-      (catch
-        (test1 nil)
-        (fun e =>
-           match e with
-           | Zero => ret (0 :: nil)
-           | _ => throw e
-           end
-        )
-      )
-      (fun e =>
-         match e with
-         | Empty =>
-             b <- lift $ get;;
-             if b:bool
-             then (100 :: nil)
-             else (200 :: nil)
-         | _ => throw e
-         end
-      );;
-    ret $ 123 :: r
-  .
-
-
-End Example.
-
-
+Require Import Monads.
+
+Require Import FunctionalExtensionality.
+
+
+Inductive resG (e : Type) (a : Type) :=
+  | Ok : a -> resG e a
+  | Error : e -> resG e a
+.
+
+Definition resT e {m : Type -> Type} (M : Monad m) a :=
+  m (resG e a).
+
+Definition res e := resT e Identity.
+
+Implicit Arguments Ok [e a].
+Implicit Arguments Error [e a].
+
+
+Class ErrorMonadT
+(e : Type)
+{m : Type -> Type}
+(M : Monad m)
+:=
+  { throw : forall {a : Type},
+      e -> res e (m a)
+  ; catch : forall {a : Type},
+      res e (m a) -> (e -> res e (m a)) -> res e (m a)
+  }
+.
+
+Instance ErrorT
+(e : Type)
+{m : Type -> Type}
+(M : Monad m)
+: ErrorMonadT e M
+:=
+  {| throw := fun {a : Type} (err : e) =>
+       Error err
+   ; catch := fun
+       {a : Type}
+       (ra : res e (m a))
+       (handler : e -> res e (m a)) =>
+         match ra with
+         | Ok r => Ok r
+         | Error r => handler r
+         end
+   |}.
+
+
+Instance ErrorT_Monad_inst
+  (e : Type)
+  {m : Type -> Type}
+  (M : Monad m)
+: Monad (resT e M)
+:=
+  {| ret := fun {A} (a : A) => ret (Ok a)
+   ; bind := fun
+       {A B}
+       (ma : resT e M A)
+       (f : A -> resT e M B) =>
+         (ma : m (res e A)) >>= fun (a : res e A) =>
+         match a with
+         | Ok r => f r
+         | Error r => ret (Error r)
+         end
+   |}
+.
+(* 0 *)
+  intros. rewrite Monad0. reflexivity.
+(* 1 *)
+  intros. unfold resT in *. rewrite <- Monad1.
+  f_equal. extensionality q. destruct q; reflexivity.
+(* 2 *)
+  intros. unfold resT in *.
+  rewrite Monad2.
+  f_equal. extensionality q.
+  destruct q.
+  (* 2.1 *)
+    reflexivity.
+  (* 2.2 *)
+    rewrite Monad0.
+    reflexivity.
+Defined.
+
+
+Instance ErrorT_MonadTrans_inst
+  (e : Type)
+  {m : Type -> Type}
+  {M : Monad m}
+: MonadTrans (@resT e)
+:=
+  {| lift := fun {A} ma =>
+       a <- ma;;
+       ret (Ok a)
+   |}
+.
+(* T0 *)
+  intros. extensionality q. rewrite Monad0. simpl. reflexivity.
+(* T1 *)
+  intros. simpl.
+  rewrite Monad2.
+  rewrite Monad2.
+  f_equal.
+  extensionality q.
+  rewrite Monad0.
+  reflexivity.
+Defined.
+
+
+Module Example.
+
+  Require Import StateMonad.
+
+  Inductive myerr :=
+    | Zero
+    | Empty
+  .
+
+  Require Import Eqdec.
+
+  Fixpoint test1_aux lst : res myerr nat :=
+    match lst with
+    | nil => ret 0
+    | cons h t =>
+        if eq_dec h 0
+        then throw Zero
+        else rest <- test1_aux t;; ret (h + rest)
+    end
+  .
+
+  Notation "f  x" := (f x)
+    (at level 63, right associativity, only parsing).
+
+  Require Import List.
+
+  Definition test1 (lst : list nat) : res myerr (list nat) :=
+    if eq_dec lst nil
+    then throw Empty (M := Identity)
+    else
+      h <- test1_aux lst;;
+      ret  h :: lst
+  .
+
+  Eval compute in test1 (1 :: 2 :: 3 :: nil).
+  Eval compute in test1 (1 :: 0 :: 3 :: nil).
+  Eval compute in test1 nil.
+
+Check test1.
+
+
+Typeclasses eauto := debug bfs.
+
+  Definition test2
+ : resT myerr (@StateT_Monad_inst bool identity_type Identity) (list nat)
+   :=
+    lift  (put true);;
+    r <-
+      (catch
+        (test1 nil)
+        (fun e =>
+           match e with
+           | Zero => ret (0 :: nil)
+           | _ => throw e
+           end
+        )
+      )
+      (fun e =>
+         match e with
+         | Empty =>
+             b <- lift  get;;
+             if b:bool
+             then (100 :: nil)
+             else (200 :: nil)
+         | _ => throw e
+         end
+      );;
+    ret  123 :: r
+  .
+
+
+End Example.
+
+

File Exceptions.v

-(* Author: AUGER Cédric *)
-
-(*Solution 1*)
-Set Implicit Arguments.
-Require Import String.
-
-Inductive Tree :=
-| Leaf : Tree
-| Node : Tree -> Tree -> Tree.
-Definition compTree (a b:Tree) : {a=b}+{a<>b}.
- decide equality.
-Defined.
-
-Class Serialize (A : Type) :=
-{ fromTree : Tree -> A
-; toTree : A -> Tree
-; Serialize0 : forall a, fromTree (toTree a) = a
- (*that means, you cannot serialize functions*)
-}.
-Instance SUnit : Serialize unit :=
- { fromTree := fun _ => tt; toTree := fun _ => Leaf }.
-Proof. (*Serialize0*)
- clear; abstract (intros []; split).
-Defined.
-Instance SPair A B `{Serialize A} `{Serialize B} : Serialize (prod A B) :=
-{ fromTree := fun t => match t with Leaf => (fromTree Leaf, fromTree Leaf)
-                                  | Node a b => (fromTree a, fromTree b)
-                       end
-; toTree := fun p => Node (toTree (fst p)) (toTree (snd p))
-}.
-Proof. (*Serialize0*)
- clear; abstract (intros [a b]; simpl; repeat rewrite Serialize0; split).
-Defined.
-Instance SNat : Serialize nat :=
-{ fromTree := fix fT t := match t with Leaf => O
-                                     | Node n _ => S (fT n)
-                          end
-; toTree := fix tT n := match n with O => Leaf | S n => Node (tT n) Leaf end
-}.
-Proof. (*Serialize0*)
- clear; abstract (intros n; induction n; simpl; [|rewrite IHn]; split).
-Defined.
-
-Require Import Monads.
-
-Inductive Res (A : Type) :=
-| Exn : Tree ->     (* kind          *)
-        Tree ->     (* value         *)
-        Res A       (* EXceptioN     *)
-| Nex : A -> Res A  (* Non-EXception *)
-.
-
-Instance MRes : Monad Res :=
- { ret := Nex
- ; bind := fun A B x f => match x with
-                          | Nex a => f a
-                          | Exn k v => Exn B k v
-                          end
- }.
-Proof. (*Monad0*)
- clear; abstract (split).
-Proof. (*Monad1*)
- clear; abstract (intros A [k v|a]; split).
-Proof. (*Monad2*)
- clear; abstract (intros A B C [k v|a] g h; split).
-Defined.
-
-Class Exception (A : Type) := { serialize : Serialize A; kind : Tree }.
-Instance SException (A : Type) `{Exception A} : Serialize A := serialize.
-
-Definition throw A B `{Exception B} (b:B): Res A :=
- Exn A kind (toTree b).
-
-Definition catch A B `{Exception B} (m : Res A) (f : B -> Res A) : Res A :=
- match m with
- | Nex a => ret a
- | Exn k v => if compTree k kind
-              then f (fromTree v)
-              else m
- end.
-
-(* Exemple of lemma *)
-Lemma catch_throw : forall B `{Exception B} (b:B),
-      catch (throw B b) (fun x => ret x) = ret b.
-Proof.
- unfold catch, throw; intros.
- destruct (compTree kind kind).
-  rewrite Serialize0.
-  split.
- now destruct n.
-Qed.
-
-Module Examples.
-
-Record DivisionByZero := DBZ.
-Instance SDivisionByZero : Serialize DivisionByZero :=
- { fromTree := fun _ => DBZ; toTree := fun _ => Leaf }.
-Proof. (*Serialize0*)
- clear; abstract (intros []; split).
-Defined.
-Instance EDivisionByZero : Exception DivisionByZero :=
-{ serialize := SDivisionByZero
-; kind := Leaf
-}.
-
-Record IndexOutOfBounds := IOOB { request : nat; max : nat }.
-Instance SIndexOutOfBounds : Serialize IndexOutOfBounds :=
-{ toTree := fun x => toTree (request x, max x)
-; fromTree := fun t => let p:prod nat nat := fromTree t in
-                       {|request := fst p; max := snd p|}
-}.
-Proof. (*Serialize0*)
- clear; abstract (intros a; rewrite Serialize0; destruct a; split).
-Defined.
-Instance EIndexOutOfBounds : Exception IndexOutOfBounds :=
-{ serialize := SIndexOutOfBounds
-; kind := Node Leaf Leaf
-}.
-
-Record NonPositiveResult := NPR.
-Instance SNonPositiveResult : Serialize NonPositiveResult :=
- { fromTree := fun _ => NPR; toTree := fun _ => Leaf }.
-Proof. (*Serialize0*)
- clear; abstract (intros []; split).
-Defined.
-Instance ENonPositiveResult : Exception NonPositiveResult :=
-{ serialize := SNonPositiveResult
-; kind := Leaf
-}.
-
-(* Example *)
-Definition get (A:Type) : nat -> list A -> Res A :=
- (fix _get_ acc i l :=
-      match l with
-      | nil => throw A (IOOB (i+acc) acc)
-      | cons a l => match i with
-                    | O => ret a
-                    | S i => _get_ (S acc) i l
-                    end
-      end) O.
-Fixpoint predminus (m n : nat) : Res {o : nat | o < m} :=
-(* computes m-n-1 *)
- match m as m0 return Res {o : nat | o < m0} with
- | O => throw _ NPR
- | S m => match n with
-          | O => ret (exist _ m (le_n _))
-          | S n => predminus m n >>=
-                   (fun (s : sig _) =>
-                    let (o, proof) := s in
-                    ret (exist _ o (le_S _ _ proof)))
-          end
- end
-.
-
-Lemma lt_acc : forall m, Acc (fun x y => x < y) m.
-Proof.
- intros m; induction m; split; intros.
-  change (match O with O => Acc (fun x y => x < y) y | _ => True end).
-  destruct H; split.
- change (Acc (fun x y => x < y) (match S m with S m => m | O => O end)) in IHm.
- destruct H.
-  assumption.
- destruct IHm; auto.
-Defined.
-
-Definition div (m n : nat) : Res nat :=
- match n with
- | O => throw nat DBZ
- | S n =>
- (fix _div_ m (acc : Acc (fun x y => x < y) m) {struct acc} : Res nat :=
-  match acc with Acc_intro f =>
-      catch ((predminus m n) >>=
-              fun (s:sig _) => let (x, p) := s in _div_ x (f x p) >>=
-              fun x => ret (S x))
-            (fun (_:NonPositiveResult) => ret O)
-  end) m (lt_acc m)
- end.
-
-Fixpoint string_of_nat (n:nat) :=
- match n with
- | O => "0"%string
- | S n => append "1+"%string (string_of_nat n)
- end.
-
-Definition div_in_list (divided:nat) (divider:list nat) (index:nat) : Res string :=
-  catch
- (catch (get index divider >>=
-         fun divi => div divided divi >>=
-         fun quo => ret (string_of_nat quo))
- (fun (_:DivisionByZero) => ret "Division by zero!"%string))
- (fun (e:IndexOutOfBounds) =>
-            ret (append "tried to access the "%string
-                (append (string_of_nat (request e))
-                (append " out of "%string
-                        (string_of_nat (max e))))))
-.
-
-Example L := cons 3 (cons 0 (cons 1 nil)).
-Compute (div_in_list 5 L 0).
-Compute (div_in_list 5 L 1).
-Compute (div_in_list 5 L 2).
-Compute (div_in_list 5 L 3).
-
-End Examples.
+(* Author: AUGER Cédric *)
+
+(*Solution 1*)
+Set Implicit Arguments.
+Require Import String.
+
+Inductive Tree :=
+| Leaf : Tree
+| Node : Tree -> Tree -> Tree.
+Definition compTree (a b:Tree) : {a=b}+{a<>b}.
+ decide equality.
+Defined.
+
+Class Serialize (A : Type) :=
+{ fromTree : Tree -> A
+; toTree : A -> Tree
+; Serialize0 : forall a, fromTree (toTree a) = a
+ (*that means, you cannot serialize functions*)
+}.
+Instance SUnit : Serialize unit :=
+ { fromTree := fun _ => tt; toTree := fun _ => Leaf }.
+Proof. (*Serialize0*)
+ clear; abstract (intros []; split).
+Defined.
+Instance SPair A B `{Serialize A} `{Serialize B} : Serialize (prod A B) :=
+{ fromTree := fun t => match t with Leaf => (fromTree Leaf, fromTree Leaf)
+                                  | Node a b => (fromTree a, fromTree b)
+                       end
+; toTree := fun p => Node (toTree (fst p)) (toTree (snd p))
+}.
+Proof. (*Serialize0*)
+ clear; abstract (intros [a b]; simpl; repeat rewrite Serialize0; split).
+Defined.
+Instance SNat : Serialize nat :=
+{ fromTree := fix fT t := match t with Leaf => O
+                                     | Node n _ => S (fT n)
+                          end
+; toTree := fix tT n := match n with O => Leaf | S n => Node (tT n) Leaf end
+}.
+Proof. (*Serialize0*)
+ clear; abstract (intros n; induction n; simpl; [|rewrite IHn]; split).
+Defined.
+
+Require Import Monads.
+
+Inductive Res (A : Type) :=
+| Exn : Tree ->     (* kind          *)
+        Tree ->     (* value         *)
+        Res A       (* EXceptioN     *)
+| Nex : A -> Res A  (* Non-EXception *)
+.
+
+Instance MRes : Monad Res :=
+ { ret := Nex
+ ; bind := fun A B x f => match x with
+                          | Nex a => f a
+                          | Exn k v => Exn B k v
+                          end
+ }.
+Proof. (*Monad0*)
+ clear; abstract (split).
+Proof. (*Monad1*)
+ clear; abstract (intros A [k v|a]; split).
+Proof. (*Monad2*)
+ clear; abstract (intros A B C [k v|a] g h; split).
+Defined.
+
+Class Exception (A : Type) := { serialize : Serialize A; kind : Tree }.
+Instance SException (A : Type) `{Exception A} : Serialize A := serialize.
+
+Definition throw A B `{Exception B} (b:B): Res A :=
+ Exn A kind (toTree b).
+
+Definition catch A B `{Exception B} (m : Res A) (f : B -> Res A) : Res A :=
+ match m with
+ | Nex a => ret a
+ | Exn k v => if compTree k kind
+              then f (fromTree v)
+              else m
+ end.
+
+(* Exemple of lemma *)
+Lemma catch_throw : forall B `{Exception B} (b:B),
+      catch (throw B b) (fun x => ret x) = ret b.
+Proof.
+ unfold catch, throw; intros.
+ destruct (compTree kind kind).
+  rewrite Serialize0.
+  split.
+ now destruct n.
+Qed.
+
+Module Examples.
+
+Record DivisionByZero := DBZ.
+Instance SDivisionByZero : Serialize DivisionByZero :=
+ { fromTree := fun _ => DBZ; toTree := fun _ => Leaf }.
+Proof. (*Serialize0*)
+ clear; abstract (intros []; split).
+Defined.
+Instance EDivisionByZero : Exception DivisionByZero :=
+{ serialize := SDivisionByZero
+; kind := Leaf
+}.
+
+Record IndexOutOfBounds := IOOB { request : nat; max : nat }.
+Instance SIndexOutOfBounds : Serialize IndexOutOfBounds :=
+{ toTree := fun x => toTree (request x, max x)
+; fromTree := fun t => let p:prod nat nat := fromTree t in
+                       {|request := fst p; max := snd p|}
+}.
+Proof. (*Serialize0*)
+ clear; abstract (intros a; rewrite Serialize0; destruct a; split).
+Defined.
+Instance EIndexOutOfBounds : Exception IndexOutOfBounds :=
+{ serialize := SIndexOutOfBounds
+; kind := Node Leaf Leaf
+}.
+
+Record NonPositiveResult := NPR.
+Instance SNonPositiveResult : Serialize NonPositiveResult :=
+ { fromTree := fun _ => NPR; toTree := fun _ => Leaf }.
+Proof. (*Serialize0*)
+ clear; abstract (intros []; split).
+Defined.
+Instance ENonPositiveResult : Exception NonPositiveResult :=
+{ serialize := SNonPositiveResult
+; kind := Leaf
+}.
+
+(* Example *)
+Definition get (A:Type) : nat -> list A -> Res A :=
+ (fix _get_ acc i l :=
+      match l with
+      | nil => throw A (IOOB (i+acc) acc)
+      | cons a l => match i with
+                    | O => ret a
+                    | S i => _get_ (S acc) i l
+                    end
+      end) O.
+Fixpoint predminus (m n : nat) : Res {o : nat | o < m} :=
+(* computes m-n-1 *)
+ match m as m0 return Res {o : nat | o < m0} with
+ | O => throw _ NPR
+ | S m => match n with
+          | O => ret (exist _ m (le_n _))
+          | S n => predminus m n >>=
+                   (fun (s : sig _) =>
+                    let (o, proof) := s in
+                    ret (exist _ o (le_S _ _ proof)))
+          end
+ end
+.
+
+Lemma lt_acc : forall m, Acc (fun x y => x < y) m.
+Proof.
+ intros m; induction m; split; intros.
+  change (match O with O => Acc (fun x y => x < y) y | _ => True end).
+  destruct H; split.
+ change (Acc (fun x y => x < y) (match S m with S m => m | O => O end)) in IHm.
+ destruct H.
+  assumption.
+ destruct IHm; auto.
+Defined.
+
+Definition div (m n : nat) : Res nat :=
+ match n with
+ | O => throw nat DBZ
+ | S n =>
+ (fix _div_ m (acc : Acc (fun x y => x < y) m) {struct acc} : Res nat :=
+  match acc with Acc_intro f =>
+      catch ((predminus m n) >>=
+              fun (s:sig _) => let (x, p) := s in _div_ x (f x p) >>=
+              fun x => ret (S x))
+            (fun (_:NonPositiveResult) => ret O)
+  end) m (lt_acc m)
+ end.
+
+Fixpoint string_of_nat (n:nat) :=
+ match n with
+ | O => "0"%string
+ | S n => append "1+"%string (string_of_nat n)
+ end.
+
+Definition div_in_list (divided:nat) (divider:list nat) (index:nat) : Res string :=
+  catch
+ (catch (get index divider >>=
+         fun divi => div divided divi >>=
+         fun quo => ret (string_of_nat quo))
+ (fun (_:DivisionByZero) => ret "Division by zero!"%string))
+ (fun (e:IndexOutOfBounds) =>
+            ret (append "tried to access the "%string
+                (append (string_of_nat (request e))
+                (append " out of "%string
+                        (string_of_nat (max e))))))
+.
+
+Example L := cons 3 (cons 0 (cons 1 nil)).
+Compute (div_in_list 5 L 0).
+Compute (div_in_list 5 L 1).
+Compute (div_in_list 5 L 2).
+Compute (div_in_list 5 L 3).
+
+End Examples.
-Class Monad (m : Type -> Type) :=
-{ ret : forall {A}, A -> m A
-; bind : forall {A B}, m A -> (A -> m B) -> m B
-; Monad0 : forall A B (f:A->m B) (a:A), bind (ret a) f = f a
-; Monad1 : forall A (x: m A), bind x (fun y => ret y) = x
-; Monad2 : forall A B C (f:m A) (g:A->m B) (h:B->m C),
-           bind (bind f g) h = bind f (fun x => bind (g x) h)
-}.
-
-
-
-Notation "m >>= f" := (@bind _ _ _ _ m f)
-(at level 64, right associativity).
-
-Notation "x <- y ;; z" := (@bind _ _ _ _ y (fun x : _ => z ))
-  ( (*only parsing,*) at level 66, right associativity, y at next level).
-Notation "y ;; z" := (@bind _ _ _ _ y (fun (_ : unit) => z ))
-  ( (*only parsing,*) at level 66, right associativity).
-
-
-Definition identity_type := fun A:Type => A.
-Definition identity A : A -> identity_type A := fun x => x.
-
-Instance Identity : Monad identity_type :=
-  {| ret := fun A x => x
-   ; bind := fun A B m f => f m
-   |}
-.
-auto. auto. auto.
-Defined.
-
-
-Instance Option : Monad option :=
- { ret := Some
- ; bind := fun A B x f => match x with
-                          | None => None
-                          | Some y => f y
-                          end
- }.
-Proof. (*Monad0*)
- clear; abstract (split).
-Proof. (*Monad1*)
- clear; abstract (intros A x; case x; split).
-Proof. (*Monad2*)
- clear; abstract (intros A B C [|a]; split).
-Defined.
-
-
-
-
-Class MonadTrans
-  (t : forall m {M : Monad m}, (Type -> Type))
-  {M : forall {m M}, Monad (@t m M)} :=
-{ lift : forall {A m M}, m A -> @t m M A
-; MonadT0 : forall {A m Mm} a,
-    lift (@ret m Mm A a) = ret a
-; MonadT1 : forall {A B m Mm} (k : A -> m B) (v : m A),
-    lift (@bind m Mm A B v k) = bind (lift v) (fun a => lift (k a))
-}
-.
+Class Monad (m : Type -> Type) :=
+{ ret : forall {A}, A -> m A
+; bind : forall {A B}, m A -> (A -> m B) -> m B
+; Monad0 : forall A B (f:A->m B) (a:A), bind (ret a) f = f a
+; Monad1 : forall A (x: m A), bind x (fun y => ret y) = x
+; Monad2 : forall A B C (f:m A) (g:A->m B) (h:B->m C),
+           bind (bind f g) h = bind f (fun x => bind (g x) h)
+}.
+
+
+
+Notation "m >>= f" := (@bind _ _ _ _ m f)
+(at level 64, right associativity).
+
+Notation "x <- y ;; z" := (@bind _ _ _ _ y (fun x : _ => z ))
+  ( (*only parsing,*) at level 66, right associativity, y at next level).
+Notation "y ;; z" := (@bind _ _ _ _ y (fun (_ : unit) => z ))
+  ( (*only parsing,*) at level 66, right associativity).
+
+
+Definition identity_type := fun A:Type => A.
+Definition identity A : A -> identity_type A := fun x => x.
+
+Instance Identity : Monad identity_type :=
+  {| ret := fun A x => x
+   ; bind := fun A B m f => f m
+   |}
+.
+auto. auto. auto.
+Defined.
+
+
+Instance Option : Monad option :=
+ { ret := Some
+ ; bind := fun A B x f => match x with
+                          | None => None
+                          | Some y => f y
+                          end
+ }.
+Proof. (*Monad0*)
+ clear; abstract (split).
+Proof. (*Monad1*)
+ clear; abstract (intros A x; case x; split).
+Proof. (*Monad2*)
+ clear; abstract (intros A B C [|a]; split).
+Defined.
+
+
+
+
+Class MonadTrans
+  (t : forall m {M : Monad m}, (Type -> Type))
+  {M : forall {m M}, Monad (@t m M)} :=
+{ lift : forall {A m M}, m A -> @t m M A
+; MonadT0 : forall {A m Mm} a,
+    lift (@ret m Mm A a) = ret a
+; MonadT1 : forall {A B m Mm} (k : A -> m B) (v : m A),
+    lift (@bind m Mm A B v k) = bind (lift v) (fun a => lift (k a))
+}
+.

File StateMonad.v

-Require Import Monads.
-Require Import Exceptions.
-
-Require Import FunctionalExtensionality.
-
-
-Definition stateT
-  (S : Type) m {M : Monad m} (A : Type) : Type
-:= S -> m ((A * S)%type).
-
-
-Instance StateT_Monad_inst
- (S : Type) m {M : Monad m}
-: Monad (stateT S m)
-:=
-  {| ret := fun A a => fun s => ret (a, s)
-   ; bind := fun A B m f =>
-       fun s =>
-         ma <- m s;;
-         let (ma_r, ma_s) := ma in
-         (f ma_r) ma_s
-   |}
-.
-(* 1 *)
-intros; extensionality s; rewrite Monad0; reflexivity.
-(* 2 *)
-intros; extensionality s; generalize (x s); intro;
-  rewrite <- Monad1; f_equal; extensionality s2;
-  destruct s2; reflexivity.
-(* 3 *)
-intros; extensionality s; rewrite -> Monad2; f_equal;
-  extensionality s2; destruct s2; reflexivity.
-Defined.
-
-
-Class StateMonadT
-(S : Type)
-{m : Type -> Type}
-(M : Monad m)
-:=
-  { get : stateT S m S
-  ; put : S -> stateT S m unit
-  }
-.
-
-
-
-Instance StateT
-(S : Type)
-{m : Type -> Type}
-{ M : Monad m}
-: StateMonadT S M
-:=
-  {| get := fun s => ret (s, s)
-   ; put := fun new_state =>
-       fun _s => ret (tt, new_state)
-   |}
-.
-
-Instance State_monadT_inst S
-: @MonadTrans (stateT S) (StateT_Monad_inst S)
-:=
-  { lift := fun A m M (v : m A) =>
-      fun s =>
-        a <- v ;;
-        ret (a, s)
-  }
-.
-(* T0 *)
-intros; simpl.
-extensionality x.
-rewrite Monad0.
-reflexivity.
-(* T1 *)
-intros. simpl.
-extensionality q.
-repeat rewrite Monad2.
-f_equal.
-extensionality r.
-repeat rewrite Monad0.
-reflexivity.
-Defined.
-
-
-Instance State S : StateMonadT S Identity
- :=
-  {| get := fun s => (s, s)
-   ; put := fun new_state _s => (tt, new_state)
-   |}
-.
-
-
-Definition evalState
-  {S A : Type}
-  {m}
-  {M : Monad m}
-  (v : stateT S m A)
-  (init : S)
-  : m A
-  :=
-    ma <- v init;;
-    let (ma_r, _ma_s) := ma in
-    ret ma_r
-.
-
-Definition execState
-  {S A : Type}
-  {m}
-  {M : Monad m}
-  (v : stateT S m A)
-  (init : S)
-  : m S
-  :=
-    ma <- v init;;
-    let (_ma_r, ma_s) := ma in
-    ret ma_s
-.
-     
-
-Module Examples.
-
-Definition test1 :=
-  x <- ret 10;;
-  put false;;
-  r <- get;;
-  if r:bool then ret (x + 1) else ret (x + 2)
-.
-
-Print test1.
-
-Eval compute in evalState test1 true.
-
-End Examples.
+Require Import Monads.
+Require Import Exceptions.
+
+Require Import FunctionalExtensionality.
+
+
+Definition stateT
+  (S : Type) m {M : Monad m} (A : Type) : Type
+:= S -> m ((A * S)%type).
+
+
+Instance StateT_Monad_inst
+ (S : Type) m {M : Monad m}
+: Monad (stateT S m)
+:=
+  {| ret := fun A a => fun s => ret (a, s)
+   ; bind := fun A B m f =>
+       fun s =>
+         ma <- m s;;
+         let (ma_r, ma_s) := ma in
+         (f ma_r) ma_s
+   |}
+.
+(* 1 *)
+intros; extensionality s; rewrite Monad0; reflexivity.
+(* 2 *)
+intros; extensionality s; generalize (x s); intro;
+  rewrite <- Monad1; f_equal; extensionality s2;
+  destruct s2; reflexivity.
+(* 3 *)
+intros; extensionality s; rewrite -> Monad2; f_equal;
+  extensionality s2; destruct s2; reflexivity.
+Defined.
+
+
+Class StateMonadT
+(S : Type)
+{m : Type -> Type}
+(M : Monad m)
+:=
+  { get : stateT S m S
+  ; put : S -> stateT S m unit
+  }
+.
+
+
+
+Instance StateT
+(S : Type)
+{m : Type -> Type}
+{ M : Monad m}
+: StateMonadT S M
+:=
+  {| get := fun s => ret (s, s)
+   ; put := fun new_state =>
+       fun _s => ret (tt, new_state)
+   |}
+.
+
+Instance State_monadT_inst S
+: @MonadTrans (stateT S) (StateT_Monad_inst S)
+:=
+  { lift := fun A m M (v : m A) =>
+      fun s =>
+        a <- v ;;
+        ret (a, s)
+  }
+.
+(* T0 *)
+intros; simpl.
+extensionality x.
+rewrite Monad0.
+reflexivity.
+(* T1 *)
+intros. simpl.
+extensionality q.
+repeat rewrite Monad2.
+f_equal.
+extensionality r.
+repeat rewrite Monad0.
+reflexivity.
+Defined.
+
+
+Instance State S : StateMonadT S Identity
+ :=
+  {| get := fun s => (s, s)
+   ; put := fun new_state _s => (tt, new_state)
+   |}
+.
+
+
+Definition evalState
+  {S A : Type}
+  {m}
+  {M : Monad m}
+  (v : stateT S m A)
+  (init : S)
+  : m A
+  :=
+    ma <- v init;;
+    let (ma_r, _ma_s) := ma in
+    ret ma_r
+.
+
+Definition execState
+  {S A : Type}
+  {m}
+  {M : Monad m}
+  (v : stateT S m A)
+  (init : S)
+  : m S
+  :=
+    ma <- v init;;
+    let (_ma_r, ma_s) := ma in
+    ret ma_s
+.
+     
+
+Module Examples.
+
+Definition test1 :=
+  x <- ret 10;;
+  put false;;
+  r <- get;;
+  if r:bool then ret (x + 1) else ret (x + 2)
+.
+
+Print test1.
+
+Eval compute in evalState test1 true.
+
+End Examples.