``` ```

# The error monad

``` Require Import Coqlib. Set Implicit Arguments. Definition bind (A B: Set) (f: option A) (g: A -> option B) : option B :=   match f with   | Some x => g x   | None => None   end. Definition bind2 (A B C: Set) (f: option (A * B)) (g: A -> B -> option C) : option C :=   match f with   | Some (x, y) => g x y   | None => None   end. ```
The `do` notation, inspired by Haskell's, keeps the code readable.
``` Notation "'do' X <- A ; B" := (bind A (fun X => B))  (at level 200, X ident, A at level 100, B at level 200)  : error_monad_scope. Notation "'do' ( X , Y ) <- A ; B" := (bind2 A (fun X Y => B))  (at level 200, X ident, Y ident, A at level 100, B at level 200)  : error_monad_scope. Remark bind_inversion:   forall (A B: Set) (f: option A) (g: A -> option B) (y: B),   bind f g = Some y ->   exists x, f = Some x /\ g x = Some y. Proof.   intros until y. destruct f; simpl; intros.   exists a; auto.   discriminate. Qed. Remark bind2_inversion:   forall (A B C: Set) (f: option (A*B)) (g: A -> B -> option C) (z: C),   bind2 f g = Some z ->   exists x, exists y, f = Some (x, y) /\ g x y = Some z. Proof.   intros until z. destruct f; simpl.   destruct p; simpl; intros. exists a; exists b; auto.   intros; discriminate. Qed. Open Local Scope error_monad_scope. ```
This is the familiar monadic map iterator.
``` Fixpoint mmap (A B: Set) (f: A -> option B) (l: list A) {struct l} : option (list B) :=   match l with   | nil => Some nil   | hd :: tl => do hd' <- f hd; do tl' <- mmap f tl; Some (hd' :: tl')   end. Remark mmap_inversion:   forall (A B: Set) (f: A -> option B) (l: list A) (l': list B),   mmap f l = Some l' ->   list_forall2 (fun x y => f x = Some y) l l'. Proof.   induction l; simpl; intros.   inversion_clear H. constructor.   destruct (bind_inversion _ _ H) as [hd' [P Q]].   destruct (bind_inversion _ _ Q) as [tl' [R S]].   inversion_clear S.   constructor. auto. auto. Qed. ```

# Reasoning over monadic computations

``` ```
The `monadInv H` tactic below simplifies hypotheses of the form
```        H: (do x <- a; b) = OK res
```

By definition of the bind operation, both computations `a` and `b` must succeed for their composition to succeed. The tactic therefore generates the following hypotheses:

x: ... H1: a = OK x H2: b x = OK res
``` Ltac monadInv1 H :=   match type of H with   | (Some _ = Some _) =>       inversion H; clear H; try subst   | (None = Some _) =>       discriminate   | (bind ?F ?G = Some ?X) =>       let x := fresh "x" in (       let EQ1 := fresh "EQ" in (       let EQ2 := fresh "EQ" in (       destruct (bind_inversion F G H) as [x [EQ1 EQ2]];       clear H;       try (monadInv1 EQ2))))   | (bind2 ?F ?G = Some ?X) =>       let x1 := fresh "x" in (       let x2 := fresh "x" in (       let EQ1 := fresh "EQ" in (       let EQ2 := fresh "EQ" in (       destruct (bind2_inversion F G H) as [x1 [x2 [EQ1 EQ2]]];       clear H;       try (monadInv1 EQ2)))))   | (mmap ?F ?L = Some ?M) =>       generalize (mmap_inversion F L H); intro   end. Ltac monadInv H :=   match type of H with   | (Some _ = Some _) => monadInv1 H   | (None = Some _) => monadInv1 H   | (bind ?F ?G = Some ?X) => monadInv1 H   | (bind2 ?F ?G = Some ?X) => monadInv1 H   | (?F _ _ _ _ _ _ _ _ = Some _) =>       ((progress simpl in H) || unfold F in H); monadInv1 H   | (?F _ _ _ _ _ _ _ = Some _) =>       ((progress simpl in H) || unfold F in H); monadInv1 H   | (?F _ _ _ _ _ _ = Some _) =>       ((progress simpl in H) || unfold F in H); monadInv1 H   | (?F _ _ _ _ _ = Some _) =>       ((progress simpl in H) || unfold F in H); monadInv1 H   | (?F _ _ _ _ = Some _) =>       ((progress simpl in H) || unfold F in H); monadInv1 H   | (?F _ _ _ = Some _) =>       ((progress simpl in H) || unfold F in H); monadInv1 H   | (?F _ _ = Some _) =>       ((progress simpl in H) || unfold F in H); monadInv1 H   | (?F _ = Some _) =>       ((progress simpl in H) || unfold F in H); monadInv1 H   end. Unset Implicit Arguments. ```