Library ErrorMonad

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.