Library MemMonad

A monad for imperative computations with mutable, untyped memories

Require Import Arith.

Require Import Binding.

Set Implicit Arguments.

Untyped memories


Definition memory := nat -> nat.
Definition empty (_ : nat) := O.
Definition write (m : memory) a v x :=
  if eq_nat_dec a x
    then v
    else m x.

The memory monad


We define the values of the memory monad as heap transformers. This type memM is parameterized by the Set of the desired return type.
Definition memM (ret : Set) := memory -> memory * ret.

Definition Return (T : Set) (v : T) : memM T :=
  fun m => (m, v).

Definition Read (a : nat) : memM nat :=
  fun m => (m, m a).

Definition Write (a v : nat) : memM unit :=
  fun m => (write m a v, tt).

Definition Bind (T1 T2 : Set) (M1 : memM T1) (M2 : T1 -> memM T2) : memM T2 :=
  fun m =>
    let (m', v1) := M1 m in
      M2 v1 m'.

Some syntactic abbreviations for Bind

Notation "x <- m1 ; m2" := (Bind m1 (fun x => m2))
  (right associativity, at level 60).
Notation "m1 ;; m2" := (Bind m1 (fun _ => m2))
  (right associativity, at level 60).

Proving that monadic values meet specifications


Section mspec.
   Variables (T : Set) (P : memory -> T -> Prop).

This is the generic predicate for asserting that a monad meets a specification.
  Definition mspec (m1 : memM T) (m : memory) : Prop :=
    P (fst (m1 m)) (snd (m1 m)).

A Hoare-logic-style rule for deducing that a Return meets a spec.
  Lemma mspec_Return : forall m v,
    P m v
    -> mspec (Return v) m.
    trivial.
  Qed.
End mspec.

This section defines a rule analagous to the frame rule in Hoare logic, strengthening a specification to take advantage of known facts.

Section mspec_imp.
   Variable T : Set.
   Variables P1 P2 : memory -> T -> Prop.
  
   Variable m1 : memM T.
   Variable m : memory.

  Theorem mspec_imp : mspec P1 m1 m
    -> (forall m v, P1 m v -> P2 m v)
    -> mspec P2 m1 m.
    unfold mspec.
    intuition.
  Qed.
End mspec_imp.

...and the following sections provide not-so-interesting proof rules for the other monad constructors.

Section mspec_Read.
   Variable P : memory -> nat -> Prop.
  
   Variable addr : nat.
   Variable m : memory.

  Theorem mspec_Read :
    P m (m addr)
    -> mspec P (Read addr) m.
    trivial.
  Qed.
End mspec_Read.

Section mspec_Write.
   Variable P : memory -> unit -> Prop.
  
   Variables addr src : nat.
   Variable m : memory.

  Theorem mspec_Write :
    P (write m addr src) tt
    -> mspec P (Write addr src) m.
    trivial.
  Qed.
End mspec_Write.

Section mspec_Bind.
   Variables (T1 T2 : Set) (P : memory -> T2 -> Prop).

   Variable m1 : memM T1.
   Variable m2 : T1 -> memM T2.

  Theorem mspec_Bind : forall m,
    mspec (fun m v => mspec P (m2 v) m) m1 m
    -> mspec P (Bind m1 m2) m.
    unfold mspec, Bind; simpl; intro.
    destruct (m1 m); simpl.
    destruct (m2 t m0); trivial.
  Qed.
End mspec_Bind.

Automating proofs about the memory monad


First, we prove the standard memory axioms.

Lemma write_eq : forall m a v, write m a v a = v.
  unfold write.
  intros.
  destruct (eq_nat_dec a a); tauto.
Qed.

Hint Rewrite write_eq : write.

Lemma write_ne : forall m a v a', a <> a'
  -> write m a v a' = m a'.
  unfold write.
  intros.
  destruct (eq_nat_dec a a'); tauto.
Qed.

Hint Rewrite write_ne using omega : write.

Here's a tactic to apply the memory axioms in hypotheses.

Ltac hyp_rewriter :=
  match goal with
    | [ H : context[write _ ?A _ ?A] |- _ ] =>
      rewrite write_eq in H
    | [ H : context[write _ ?A1 _ ?A2] |- _ ] =>
      rewrite write_ne in H; [idtac | omega]
  end.

This tactic first tries applying a structure-specific proof rule to prove a mspec goal. If the structure of a monadic value is unknown, it tries to find a known mspec fact with a stronger spec and switch to proving that the spec we wanted is implied by the known spec.

Ltac monad_simplify :=
  match goal with
    | [ |- mspec _ (Return _) _ ] => apply mspec_Return
    | [ |- mspec _ (Read _) _ ] => apply mspec_Read
    | [ |- mspec _ (Write _ _) _ ] => apply mspec_Write
    | [ |- mspec _ (Bind _ _) _ ] => apply mspec_Bind
    | [ |- mspec _ _ _ ] => eapply mspec_imp; [eauto; fail | idtac]
  end.

The overall simplication tactic for mspec goals, which is able to prove many such goals completely automatically.

Ltac memM_simplify := repeat progress (simplify; autorewrite with write;
  repeat hyp_rewriter; repeat monad_simplify).


Index
This page has been generated by coqdoc