pl/frap
1
0
Fork 0
mirror of https://github.com/achlipala/frap.git synced 2024-11-10 00:07:51 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions

DeepAndShallowEmbeddings: proof automation for examples

Browse source
This commit is contained in:
Adam Chlipala 2016-04-10 17:01:03 -04:00
parent 4849bf22a2
commit 11e1c74b1c
1 changed files with 75 additions and 180 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

237
DeepAndShallowEmbeddings.v
View file

@ -20,6 +20,11 @@ Example h0 : heap := $0 $+ (0, 2) $+ (1, 1) $+ (2, 8) $+ (3, 6).
Hint Rewrite max_l max_r using linear_arithmetic. Hint Rewrite max_l max_r using linear_arithmetic.
Ltac simp := repeat (simplify; subst; propositional;
try match goal with
| [ H : ex _ |- _ ] => invert H
end); try linear_arithmetic.
(** * Shallow embedding of a language very similar to the one we used last chapter *) (** * Shallow embedding of a language very similar to the one we used last chapter *)
@ -224,6 +229,13 @@ Module Deep.
eapply HtConsequence; eauto. eapply HtConsequence; eauto.
Qed. Qed.
Ltac basic := apply HtReturn || eapply HtRead || eapply HtWrite.
Ltac step0 := basic || eapply HtBind || (eapply HtStrengthen; [ basic | ]).
Ltac step := step0; simp.
Ltac ht := simp; repeat step; eauto.
Ltac conseq := simplify; eapply HtConsequence.
Ltac use_IH H := conseq; [ apply H | .. ]; ht.
Notation "{{ h ~> P }} c {{ r & h' ~> Q }}" := Notation "{{ h ~> P }} c {{ r & h' ~> Q }}" :=
(hoare_triple (fun h => P) c (fun r h' => Q)) (at level 90, c at next level). (hoare_triple (fun h => P) c (fun r h' => Q)) (at level 90, c at next level).
@ -232,27 +244,11 @@ Module Deep.
array_max i acc array_max i acc
{{ r&h ~> forall j, j < len -> h $! j <= r }}. {{ r&h ~> forall j, j < len -> h $! j <= r }}.
Proof. Proof.
induct i; simplify. induct i; ht.
use_IH IHi.
eapply HtStrengthen. cases (j ==n i); simp.
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. assert (h $! j <= acc) by auto.
linear_arithmetic. linear_arithmetic.
simplify; auto.
Qed. Qed.
Theorem array_max_ok : forall len, Theorem array_max_ok : forall len,
@ -260,13 +256,10 @@ Module Deep.
array_max len 0 array_max len 0
{{ r&h ~> forall i, i < len -> h $! i <= r }}. {{ r&h ~> forall i, i < len -> h $! i <= r }}.
Proof. Proof.
simplify. conseq.
eapply HtConsequence.
apply array_max_ok' with (len := len). apply array_max_ok' with (len := len).
simp.
simplify. simp.
linear_arithmetic.
auto. auto.
Qed. Qed.
@ -276,32 +269,11 @@ Module Deep.
increment_all i increment_all i
{{ _&h ~> forall j, j < len -> h $! j = S (h0 $! j) }}. {{ _&h ~> forall j, j < len -> h $! j = S (h0 $! j) }}.
Proof. Proof.
induct i; simplify; propositional. induct i; ht.
use_IH IHi.
eapply HtStrengthen. cases (j ==n i); simp.
econstructor.
simplify.
propositional.
auto. auto.
econstructor.
econstructor.
simplify.
econstructor.
econstructor.
simplify.
eapply HtConsequence.
apply IHi.
simplify.
invert H; propositional; subst.
simplify.
auto. auto.
cases (j ==n i); subst; auto.
simplify; auto.
simplify; auto.
simplify; auto.
Qed. Qed.
Theorem increment_all_ok : forall len h0, Theorem increment_all_ok : forall len h0,
@ -309,14 +281,10 @@ Module Deep.
increment_all len increment_all len
{{ _&h ~> forall j, j < len -> h $! j = S (h0 $! j) }}. {{ _&h ~> forall j, j < len -> h $! j = S (h0 $! j) }}.
Proof. Proof.
simplify. conseq.
eapply HtConsequence.
apply increment_all_ok' with (len := len). apply increment_all_ok' with (len := len).
simp.
simplify; subst; propositional. simp.
linear_arithmetic.
simplify.
auto. auto.
Qed. Qed.
@ -447,6 +415,14 @@ Module Deeper.
eapply HtConsequence; eauto. eapply HtConsequence; eauto.
Qed. Qed.
Ltac basic := apply HtReturn || eapply HtRead || eapply HtWrite.
Ltac step0 := basic || eapply HtBind || (eapply HtStrengthen; [ basic | ]).
Ltac step := step0; simp.
Ltac ht := simp; repeat step; eauto.
Ltac conseq := simplify; eapply HtConsequence.
Ltac use_IH H := conseq; [ apply H | .. ]; ht.
Ltac loop_inv Inv := eapply HtConsequence; [ apply HtLoop with (I := Inv) | .. ]; ht.
Theorem index_of_ok : forall hinit needle, Theorem index_of_ok : forall hinit needle,
{{ h ~> h = hinit }} {{ h ~> h = hinit }}
index_of needle index_of needle
@ -454,40 +430,16 @@ Module Deeper.
/\ hinit $! r = needle /\ hinit $! r = needle
/\ forall i, i < r -> hinit $! i <> needle }}. /\ forall i, i < r -> hinit $! i <> needle }}.
Proof. Proof.
unfold index_of.
simplify. simplify.
eapply HtConsequence. loop_inv (fun r h => h = hinit
apply HtLoop with (I := fun r h => h = hinit
/\ match r with /\ match r with
| Done r' => hinit $! r' = needle | Done r' => hinit $! r' = needle
/\ forall i, i < r' -> hinit $! i <> needle /\ forall i, i < r' -> hinit $! i <> needle
| Again r' => forall i, i < r' -> hinit $! i <> needle | Again r' => forall i, i < r' -> hinit $! i <> needle
end); simplify. end).
cases (r ==n needle); ht.
econstructor. cases (i ==n acc); simp.
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. apply H3 with (i0 := i); auto.
simplify.
propositional.
linear_arithmetic.
simplify.
propositional.
Qed. Qed.
Definition trsys_of {result} (c : cmd result) (h : heap) := {| Definition trsys_of {result} (c : cmd result) (h : heap) := {|
@ -772,51 +724,29 @@ Module DeeperWithFail.
eapply HtConsequence; eauto. eapply HtConsequence; eauto.
Qed. Qed.
Ltac basic := apply HtReturn || eapply HtRead || eapply HtWrite.
Ltac step0 := basic || eapply HtBind || (eapply HtStrengthen; [ basic | ])
|| (eapply HtConsequence; [ apply HtFail | .. ]).
Ltac step := step0; simp.
Ltac ht := simp; repeat step.
Ltac conseq := simplify; eapply HtConsequence.
Ltac use_IH H := conseq; [ apply H | .. ]; ht.
Ltac use_lemma H := eapply HtWeaken; [ apply H | .. ]; ht.
Ltac loop_inv0 Inv := (eapply HtWeaken; [ apply HtLoop with (I := Inv) | .. ])
|| (eapply HtConsequence; [ apply HtLoop with (I := Inv) | .. ]).
Ltac loop_inv Inv := loop_inv0 Inv; ht.
Theorem forever_ok : Theorem forever_ok :
{{ _ ~> True }} {{ _ ~> True }}
forever forever
{{ _&_ ~> False }}. {{ _&_ ~> False }}.
Proof. Proof.
unfold forever. ht.
econstructor. loop_inv (fun (r : loop_outcome nat) h => h $! 0 > 0 /\ match r with
econstructor.
simplify.
eapply HtConsequence.
apply HtLoop with (I := fun r h => h $! 0 > 0 /\ match r with
| Done _ => False | Done _ => False
| _ => True | _ => True
end); simplify. end).
cases r1; ht.
econstructor.
econstructor.
simplify.
econstructor.
econstructor.
simplify.
cases r1.
eapply HtConsequence.
apply HtFail.
simplify.
linear_arithmetic.
simplify.
linear_arithmetic.
econstructor.
econstructor.
simplify.
eapply HtStrengthen.
econstructor.
simplify.
propositional; subst.
invert H0; propositional; subst.
simplify.
linear_arithmetic.
invert H0; propositional; subst.
simplify.
invert H; propositional; subst.
simplify.
linear_arithmetic.
simplify.
propositional.
Qed. Qed.
Definition trsys_of {result} (c : cmd result) (h : heap) := {| Definition trsys_of {result} (c : cmd result) (h : heap) := {|
@ -1047,51 +977,23 @@ Module DeeperWithFail.
{{r&h ~> (forall i, i < length ls -> h $! i = nth_default 0 ls i) {{r&h ~> (forall i, i < length ls -> h $! i = nth_default 0 ls i)
/\ r = fold_left f ls init}}. /\ r = fold_left f ls init}}.
Proof. Proof.
unfold heapfold. ht.
simplify. loop_inv (fun r h => (forall i, i < length ls -> h $! i = nth_default 0 ls i)
econstructor.
eapply HtWeaken.
apply HtLoop with (I := fun r h => (forall i, i < length ls -> h $! i = nth_default 0 ls i)
/\ match r with /\ match r with
| Done (_, acc) => acc = fold_left f ls init | Done (_, acc) => acc = fold_left f ls init
| Again (i, acc) => acc = fold_left f (firstn i ls) init | Again (i, acc) => acc = fold_left f (firstn i ls) init
end). end).
simplify. cases (length ls <=? a); ht.
cases acc; simplify. use_lemma (H (fun h => (forall i, i < Datatypes.length ls -> h $! i = nth_default 0 ls i)
cases (length ls <=? n); simplify. /\ b = fold_left f (firstn a ls) init
/\ r = h $! a)).
eapply HtStrengthen. simp; auto.
econstructor. simp.
simplify.
propositional; subst.
reflexivity.
econstructor.
econstructor.
simplify.
econstructor.
eapply HtWeaken.
apply H with (P := fun h => (forall i, i < Datatypes.length ls -> h $! i = nth_default 0 ls i)
/\ a = fold_left f (firstn n ls) init
/\ r = h $! n).
simplify; propositional; subst; auto.
simplify.
eapply HtStrengthen.
econstructor.
simplify; propositional; subst.
rewrite H1 by assumption. rewrite H1 by assumption.
simplify. simplify.
reflexivity. reflexivity.
simp; auto.
simplify; propositional. simp.
simplify.
eapply HtStrengthen.
econstructor.
simplify.
propositional; subst.
cases r; simplify.
assumption.
Qed. Qed.
Definition array_max (len : nat) : cmd nat := Definition array_max (len : nat) : cmd nat :=
@ -1126,17 +1028,10 @@ Module DeeperWithFail.
array_max (length ls) array_max (length ls)
{{ r&h ~> forall i, i < length ls -> h $! i <= r }}. {{ r&h ~> forall i, i < length ls -> h $! i <= r }}.
Proof. Proof.
simplify. conseq.
eapply HtConsequence. apply heapfold_ok with (f := max); ht.
apply heapfold_ok with (f := max). simp; auto.
simplify. simp.
eapply HtStrengthen.
econstructor.
simplify; propositional.
simplify; auto.
simplify.
subst.
propositional; subst.
rewrite H1 by assumption. rewrite H1 by assumption.
auto. auto.
Qed. Qed.