| 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).