DeepAndShallowEmbeddings: Deep

This commit is contained in:
Adam Chlipala 2016-04-10 15:10:56 -04:00
parent 01d550e4b0
commit 290fec1e5b
4 changed files with 455 additions and 5 deletions

1
.gitignore vendored
View file

@ -16,3 +16,4 @@ Makefile.coq
frap.tgz
.coq-native
Deep.ml*
Deeper.ml*

View file

@ -5,6 +5,8 @@
Require Import Frap.
Set Implicit Arguments.
(** * Shared notations and definitions *)
Notation "m $! k" := (match m $? k with Some n => n | None => O end) (at level 30).
@ -146,8 +148,8 @@ End Shallow.
(** * A basic deep embedding *)
Module Deep.
Inductive cmd : Type -> Type :=
| Return {result} (r : result) : cmd result
Inductive cmd : Set -> Type :=
| Return {result : Set} (r : result) : cmd result
| Bind {result result'} (c1 : cmd result') (c2 : result' -> cmd result) : cmd result
| Read (a : nat) : cmd nat
| Write (a v : nat) : cmd unit.
@ -197,7 +199,7 @@ Module Deep.
Qed.
Inductive hoare_triple : assertion -> forall {result}, cmd result -> (result -> assertion) -> Prop :=
| HtReturn : forall P {result} (v : result),
| HtReturn : forall P {result : Set} (v : result),
hoare_triple P (Return v) (fun r h => P h /\ r = v)
| HtBind : forall P {result' result} (c1 : cmd result') (c2 : result' -> cmd result) Q R,
hoare_triple P c1 Q
@ -213,6 +215,111 @@ Module Deep.
-> (forall r h, Q r h -> Q' r h)
-> hoare_triple P' c Q'.
Lemma HtStrengthen : forall {result} (c : cmd result) P Q (Q' : _ -> assertion),
hoare_triple P c Q
-> (forall r h, Q r h -> Q' r h)
-> hoare_triple P c Q'.
Proof.
simplify.
eapply HtConsequence; eauto.
Qed.
Notation "{{ h ~> P }} c {{ r & h' ~> Q }}" :=
(hoare_triple (fun h => P) c (fun r h' => Q)) (at level 90, c at next level).
Lemma array_max_ok' : forall len i acc,
{{ h ~> forall j, i <= j < len -> h $! j <= acc }}
array_max i acc
{{ r&h ~> forall j, j < len -> h $! j <= r }}.
Proof.
induct i; simplify.
eapply HtStrengthen.
econstructor.
simplify.
propositional.
subst.
auto.
econstructor.
constructor.
simplify.
eapply HtConsequence.
apply IHi.
simplify; propositional.
subst.
cases (j ==n i); subst; auto.
assert (h $! j <= acc) by auto.
linear_arithmetic.
simplify; auto.
Qed.
Theorem array_max_ok : forall len,
{{ _ ~> True }}
array_max len 0
{{ r&h ~> forall i, i < len -> h $! i <= r }}.
Proof.
simplify.
eapply HtConsequence.
apply array_max_ok' with (len := len).
simplify.
linear_arithmetic.
auto.
Qed.
Lemma increment_all_ok' : forall len h0 i,
{{ h ~> (forall j, j < i -> h $! j = h0 $! j)
/\ (forall j, i <= j < len -> h $! j = S (h0 $! j)) }}
increment_all i
{{ _&h ~> forall j, j < len -> h $! j = S (h0 $! j) }}.
Proof.
induct i; simplify; propositional.
eapply HtStrengthen.
econstructor.
simplify.
propositional.
auto.
econstructor.
econstructor.
simplify.
econstructor.
econstructor.
simplify.
eapply HtConsequence.
apply IHi.
simplify.
invert H; propositional; subst.
simplify.
auto.
cases (j ==n i); subst; auto.
simplify; auto.
simplify; auto.
simplify; auto.
Qed.
Theorem increment_all_ok : forall len h0,
{{ h ~> h = h0 }}
increment_all len
{{ _&h ~> forall j, j < len -> h $! j = S (h0 $! j) }}.
Proof.
simplify.
eapply HtConsequence.
apply increment_all_ok' with (len := len).
simplify; subst; propositional.
linear_arithmetic.
simplify.
auto.
Qed.
Theorem hoare_triple_sound : forall P {result} (c : cmd result) Q,
hoare_triple P c Q
-> forall h, P h
@ -232,3 +339,319 @@ Module Deep.
Extraction "Deep.ml" array_max increment_all.
End Deep.
(** * A slightly fancier deep embedding, adding unbounded loops *)
Module Deeper.
Inductive loop_outcome acc :=
| Done (a : acc)
| Again (a : acc).
Inductive cmd : Set -> Type :=
| Return {result : Set} (r : result) : cmd result
| Bind {result result'} (c1 : cmd result') (c2 : result' -> cmd result) : cmd result
| Read (a : nat) : cmd nat
| Write (a v : nat) : cmd unit
| Loop {acc : Set} (init : acc) (body : acc -> cmd (loop_outcome acc)) : cmd acc.
Notation "x <- c1 ; c2" := (Bind c1 (fun x => c2)) (right associativity, at level 80).
Notation "'for' x := i 'loop' c1 'done'" := (Loop i (fun x => c1)) (right associativity, at level 80).
Definition index_of (needle : nat) : cmd nat :=
for i := 0 loop
h_i <- Read i;
if h_i ==n needle then
Return (Done i)
else
Return (Again (S i))
done.
Inductive stepResult (result : Set) :=
| Answer (r : result)
| Stepped (h : heap) (c : cmd result).
Fixpoint step {result} (c : cmd result) (h : heap) : stepResult result :=
match c with
| Return r => Answer r
| Bind c1 c2 =>
match step c1 h with
| Answer r => Stepped h (c2 r)
| Stepped h' c1' => Stepped h' (Bind c1' c2)
end
| Read a => Answer (h $! a)
| Write a v => Stepped (h $+ (a, v)) (Return tt)
| Loop init body =>
Stepped h (r <- body init;
match r with
| Done r' => Return r'
| Again r' => Loop r' body
end)
end.
Fixpoint multiStep {result} (c : cmd result) (h : heap) (n : nat) : stepResult result :=
match n with
| O => Stepped h c
| S n' => match step c h with
| Answer r => Answer r
| Stepped h' c' => multiStep c' h' n'
end
end.
Example run_index_of : multiStep (index_of 6) h0 20 = Answer 3.
Proof.
unfold h0.
simplify.
reflexivity.
Qed.
Inductive hoare_triple : assertion -> forall {result}, cmd result -> (result -> assertion) -> Prop :=
| HtReturn : forall P {result : Set} (v : result),
hoare_triple P (Return v) (fun r h => P h /\ r = v)
| HtBind : forall P {result' result} (c1 : cmd result') (c2 : result' -> cmd result) Q R,
hoare_triple P c1 Q
-> (forall r, hoare_triple (Q r) (c2 r) R)
-> hoare_triple P (Bind c1 c2) R
| HtRead : forall P a,
hoare_triple P (Read a) (fun r h => P h /\ r = h $! a)
| HtWrite : forall P a v,
hoare_triple P (Write a v) (fun _ h => exists h', P h' /\ h = h' $+ (a, v))
| HtConsequence : forall {result} (c : cmd result) P Q (P' : assertion) (Q' : _ -> assertion),
hoare_triple P c Q
-> (forall h, P' h -> P h)
-> (forall r h, Q r h -> Q' r h)
-> hoare_triple P' c Q'
| HtLoop : forall {acc : Set} (init : acc) (body : acc -> cmd (loop_outcome acc)) I,
(forall acc, hoare_triple (I (Again acc)) (body acc) I)
-> hoare_triple (I (Again init)) (Loop init body) (fun r h => I (Done r) h).
Notation "{{ h ~> P }} c {{ r & h' ~> Q }}" :=
(hoare_triple (fun h => P) c (fun r h' => Q)) (at level 90, c at next level).
Lemma HtStrengthen : forall {result} (c : cmd result) P Q (Q' : _ -> assertion),
hoare_triple P c Q
-> (forall r h, Q r h -> Q' r h)
-> hoare_triple P c Q'.
Proof.
simplify.
eapply HtConsequence; eauto.
Qed.
Lemma HtWeaken : forall {result} (c : cmd result) P Q (P' : assertion),
hoare_triple P c Q
-> (forall h, P' h -> P h)
-> hoare_triple P' c Q.
Proof.
simplify.
eapply HtConsequence; eauto.
Qed.
Theorem index_of_ok : forall hinit needle,
{{ h ~> h = hinit }}
index_of needle
{{ r&h ~> h = hinit
/\ hinit $! r = needle
/\ forall i, i < r -> hinit $! i <> needle }}.
Proof.
unfold index_of.
simplify.
eapply HtConsequence.
apply HtLoop with (I := fun r h => h = hinit
/\ match r with
| Done r' => hinit $! r' = needle
/\ forall i, i < r' -> hinit $! i <> needle
| Again r' => forall i, i < r' -> hinit $! i <> needle
end); simplify.
econstructor.
econstructor.
simplify.
cases (r ==n needle); subst.
eapply HtStrengthen.
econstructor.
simplify; propositional; subst.
auto.
eapply HtStrengthen.
econstructor.
simplify.
propositional; subst.
simplify.
cases (i ==n acc); subst; auto.
apply H3 with (i0 := i); auto.
simplify.
propositional.
linear_arithmetic.
simplify.
propositional.
Qed.
Definition trsys_of {result} (c : cmd result) (h : heap) := {|
Initial := {(c, h)};
Step := fun p1 p2 => step (fst p1) (snd p1) = Stepped (snd p2) (fst p2)
|}.
Lemma invert_Return : forall {result : Set} (r : result) P Q,
hoare_triple P (Return r) Q
-> forall h, P h -> Q r h.
Proof.
induct 1; propositional; eauto.
Qed.
Lemma invert_Bind : forall {result' result} (c1 : cmd result') (c2 : result' -> cmd result) P Q,
hoare_triple P (Bind c1 c2) Q
-> exists R, hoare_triple P c1 R
/\ forall r, hoare_triple (R r) (c2 r) Q.
Proof.
induct 1; propositional; eauto.
invert IHhoare_triple; propositional.
eexists; propositional.
eapply HtWeaken.
eassumption.
auto.
eapply HtStrengthen.
apply H4.
auto.
Qed.
Lemma unit_not_nat : unit = nat -> False.
Proof.
simplify.
assert (exists x : unit, forall y : unit, x = y).
exists tt; simplify.
cases y; reflexivity.
rewrite H in H0.
invert H0.
specialize (H1 (S x)).
linear_arithmetic.
Qed.
Lemma invert_Read : forall a P Q,
hoare_triple P (Read a) Q
-> forall h, P h -> Q (h $! a) h.
Proof.
induct 1; propositional; eauto.
apply unit_not_nat in x0.
propositional.
Qed.
Lemma invert_Write : forall a v P Q,
hoare_triple P (Write a v) Q
-> forall h, P h -> Q tt (h $+ (a, v)).
Proof.
induct 1; propositional; eauto.
symmetry in x0.
apply unit_not_nat in x0.
propositional.
Qed.
Lemma invert_Loop : forall {acc : Set} (init : acc) (body : acc -> cmd (loop_outcome acc)) P Q,
hoare_triple P (Loop init body) Q
-> exists I, (forall acc, hoare_triple (I (Again acc)) (body acc) I)
/\ (forall h, P h -> I (Again init) h)
/\ (forall r h, I (Done r) h -> Q r h).
Proof.
induct 1; propositional; eauto.
invert IHhoare_triple; propositional.
exists x; propositional; eauto.
Qed.
Lemma step_sound : forall {result} (c : cmd result) h Q,
hoare_triple (fun h' => h' = h) c Q
-> match step c h with
| Answer r => Q r h
| Stepped h' c' => hoare_triple (fun h'' => h'' = h') c' Q
end.
Proof.
induct c; simplify; propositional.
eapply invert_Return.
eauto.
simplify; auto.
apply invert_Bind in H0.
invert H0; propositional.
apply IHc in H0.
cases (step c h); auto.
econstructor.
apply H2.
equality.
auto.
econstructor; eauto.
eapply invert_Read; eauto.
simplify; auto.
eapply HtStrengthen.
econstructor.
simplify; propositional; subst.
eapply invert_Write; eauto.
simplify; auto.
apply invert_Loop in H0.
invert H0; propositional.
econstructor.
eapply HtWeaken.
apply H0.
equality.
simplify.
cases r.
eapply HtStrengthen.
econstructor.
simplify.
propositional; subst; eauto.
eapply HtStrengthen.
eapply HtLoop.
auto.
simplify.
eauto.
Qed.
Lemma hoare_triple_sound' : forall P {result} (c : cmd result) Q,
hoare_triple P c Q
-> forall h, P h
-> invariantFor (trsys_of c h)
(fun p => hoare_triple (fun h => h = snd p)
(fst p)
Q).
Proof.
simplify.
apply invariant_induction; simplify.
propositional; subst; simplify.
eapply HtConsequence.
eassumption.
equality.
auto.
eapply step_sound in H1.
rewrite H2 in H1.
auto.
Qed.
Theorem hoare_triple_sound : forall P {result} (c : cmd result) Q,
hoare_triple P c Q
-> forall h, P h
-> invariantFor (trsys_of c h)
(fun p => forall r, fst p = Return r
-> Q r (snd p)).
Proof.
simplify.
eapply invariant_weaken.
eapply hoare_triple_sound'; eauto.
simplify.
rewrite H2 in H1.
eapply invert_Return; eauto.
simplify; auto.
Qed.
Extraction "Deeper.ml" index_of.
End Deeper.

View file

@ -20,5 +20,4 @@ let interp c =
with Not_found -> O)
| Write (a, v) -> Obj.magic (Hashtbl.replace h a v)
in let v = interp' c in
h, v
in h, interp' c

27
DeeperInterp.ml Normal file
View file

@ -0,0 +1,27 @@
let rec i2n n =
match n with
| 0 -> O
| _ -> S (i2n (n - 1))
let interp c =
let h : (nat, nat) Hashtbl.t = Hashtbl.create 0 in
Hashtbl.add h (i2n 0) (i2n 2);
Hashtbl.add h (i2n 1) (i2n 1);
Hashtbl.add h (i2n 2) (i2n 8);
Hashtbl.add h (i2n 3) (i2n 6);
let rec interp' (c : 'a cmd) : 'a =
match c with
| Return v -> v
| Bind (c1, c2) -> interp' (c2 (interp' c1))
| Read a ->
Obj.magic (try
Hashtbl.find h a
with Not_found -> O)
| Write (a, v) -> Obj.magic (Hashtbl.replace h a v)
| Loop (i, b) ->
match Obj.magic (interp' (Obj.magic (b i))) with
| Done r -> r
| Again r -> interp' (Loop (r, b))
in h, interp' c