SeparationLogic: change HtFree to make automation easier

This commit is contained in:
Adam Chlipala 2016-04-18 14:05:13 -04:00
parent 63be3681c8
commit 3261ad2809

View file

@ -56,7 +56,7 @@ Fixpoint initialize (h : heap) (base numWords : nat) : heap :=
Fixpoint deallocate (h : heap) (base numWords : nat) : heap := Fixpoint deallocate (h : heap) (base numWords : nat) : heap :=
match numWords with match numWords with
| O => h | O => h
| S numWords' => deallocate (h $- (base + numWords')) base numWords' | S numWords' => deallocate (h $- base) (base+1) numWords'
end. end.
(* Let's do the semantics a bit differently this time, falling back on classic (* Let's do the semantics a bit differently this time, falling back on classic
@ -381,10 +381,27 @@ Module Sep(Import S : SEP).
intros; apply star_cancel; auto using himp_refl. intros; apply star_cancel; auto using himp_refl.
Qed. Qed.
Theorem star_cancel'' : forall p q, lift True ===> q
-> p ===> p * q.
Proof.
intros.
eapply himp_trans.
rewrite extra_lift with (P := True); auto.
instantiate (1 := p * q).
rewrite star_comm.
apply star_cancel; auto.
reflexivity.
reflexivity.
Qed.
Ltac cancel1 := Ltac cancel1 :=
match goal with match goal with
| _ => apply himp_refl | [ |- _ ===> ?Q ] =>
| _ => apply star_cancel' match Q with
| _ => is_evar Q; fail 1
| ?Q _ => is_evar Q; fail 1
| _ => apply himp_refl
end
| [ |- ?p ===> ?q ] => | [ |- ?p ===> ?q ] =>
forAllAtoms p ltac:(fun p0 => forAllAtoms p ltac:(fun p0 =>
sendToBack p0; sendToBack p0;
@ -472,6 +489,11 @@ Module Sep(Import S : SEP).
repeat match goal with repeat match goal with
| [ H : True |- _ ] => clear H | [ H : True |- _ ] => clear H
end; end;
try match goal with
| [ |- _ ===> ?p * ?q ] =>
((is_evar p; fail 1) || apply star_cancel'')
|| ((is_evar q; fail 1) || (rewrite (star_comm p q); apply star_cancel''))
end;
try match goal with try match goal with
| [ |- ?P ===> _ ] => sendToBack P; | [ |- ?P ===> _ ] => sendToBack P;
match goal with match goal with
@ -684,6 +706,14 @@ Fixpoint zeroes (n : nat) : list nat :=
| S n' => zeroes n' ++ 0 :: nil | S n' => zeroes n' ++ 0 :: nil
end. end.
Fixpoint allocated (a n : nat) : hprop :=
match n with
| O => emp
| S n' => (exists v, a |-> v) * allocated (a+1) n'
end%sep.
Infix "|->?" := allocated (at level 30) : sep_scope.
(** * Finally, the Hoare logic *) (** * Finally, the Hoare logic *)
@ -708,7 +738,7 @@ Inductive hoare_triple : forall {result}, assertion -> cmd result -> (result ->
| HtAlloc : forall numWords, | HtAlloc : forall numWords,
hoare_triple emp%sep (Alloc numWords) (fun r => r |--> zeroes numWords)%sep hoare_triple emp%sep (Alloc numWords) (fun r => r |--> zeroes numWords)%sep
| HtFree : forall a numWords, | HtFree : forall a numWords,
hoare_triple (exists vs, a |--> vs * [| length vs = numWords |])%sep (Free a numWords) (fun _ => emp)%sep hoare_triple (a |->? numWords)%sep (Free a numWords) (fun _ => emp)%sep
| HtConsequence : forall {result} (c : cmd result) P Q (P' : assertion) (Q' : _ -> assertion), | HtConsequence : forall {result} (c : cmd result) P Q (P' : assertion) (Q' : _ -> assertion),
hoare_triple P c Q hoare_triple P c Q
@ -874,6 +904,8 @@ Proof.
cancel. cancel.
cancel. cancel.
rewrite <- H2.
cancel.
Qed. Qed.
Lemma invert_Alloc : forall numWords P Q, Lemma invert_Alloc : forall numWords P Q,
@ -973,7 +1005,7 @@ Qed.
Lemma invert_Free : forall a numWords P Q, Lemma invert_Free : forall a numWords P Q,
hoare_triple P (Free a numWords) Q hoare_triple P (Free a numWords) Q
-> P ===> (exists vs, a |--> vs * [| length vs = numWords |]) * Q tt. -> P ===> a |->? numWords * Q tt.
Proof. Proof.
induct 1; simp; eauto. induct 1; simp; eauto.
@ -993,51 +1025,6 @@ Proof.
cancel; auto. cancel; auto.
Qed. Qed.
Lemma grab_last' : forall n2 n1 a,
(exists vs, a |--> vs * [|length vs = n1 + n2|])
===> (exists vs, a |--> vs * [| length vs = n1 |])
* (exists vs, (a + n1) |--> vs * [| length vs = n2 |]).
Proof.
induct n1; simp.
cancel.
instantiate (1 := nil); simp.
replace (a + 0) with a by linear_arithmetic.
cancel; auto.
apply himp_trans with ((exists v, a |-> v)
* (exists vs : list nat,
(a+1) |--> vs * [|length vs = n1 + n2|]))%sep.
cancel.
instantiate (1 := tl x).
cases x; simp.
instantiate (1 := hd 0 x).
cases x; simp.
cancel.
rewrite IHn1.
clear IHn1.
replace (a + S n1) with (a + 1 + n1) by linear_arithmetic.
cancel.
instantiate (1 := x1 :: x0); simp.
cancel.
Qed.
Lemma grab_last : forall n a,
(exists vs, a |--> vs * [|length vs = S n|])
===> (exists vs, a |--> vs * [|length vs = n|])
* (exists v, (a + n) |-> v).
Proof.
simplify.
replace (S n) with (n + 1) by linear_arithmetic.
rewrite grab_last'.
cancel; auto.
instantiate (1 := hd 0 x).
cases x; simp.
cases x; simp.
cancel.
Qed.
(* Temporarily transparent again! *) (* Temporarily transparent again! *)
Transparent heq himp lift star exis ptsto. Transparent heq himp lift star exis ptsto.
@ -1059,35 +1046,26 @@ Proof.
simp. simp.
Qed. Qed.
Lemma do_deallocate : forall Q a numWords h, Lemma do_deallocate : forall Q numWords a h,
((exists vs, a |--> vs * [|length vs = numWords|]) * Q)%sep h (a |->? numWords * Q)%sep h
-> Q (deallocate h a numWords). -> Q (deallocate h a numWords).
Proof. Proof.
induct numWords; simp. induct numWords; simp.
unfold star, exis, lift in H; simp. unfold star, exis, lift in H; simp.
cases x1; simp. apply split_empty_fwd' in H0; simp.
unfold emp in *; simp.
replace h with x0.
equality.
apply split_empty_fwd in H1; simp.
apply split_empty_fwd' in H0; equality.
apply IHnumWords. apply IHnumWords.
clear IHnumWords. clear IHnumWords.
Opaque heq himp lift star exis ptsto.
assert ((exists vs : list nat,
a |--> vs * [|Datatypes.length vs = S numWords|]) * Q
===> (exists vs, a |--> vs * [|length vs = numWords|])
* (exists v, (a + numWords) |-> v) * Q) by (rewrite grab_last; cancel; auto).
apply H0 in H; clear H0.
assert ((exists vs, a |--> vs * [|length vs = numWords|])
* (exists v : nat, (a + numWords) |-> v) * Q
===> (exists v : nat, (a + numWords) |-> v) *
((exists vs, a |--> vs * [|length vs = numWords|]) * Q)) by (cancel; auto).
apply H0 in H; clear H0.
apply do_deallocate'. apply do_deallocate'.
assumption. Opaque heq himp lift star exis ptsto.
match goal with
| [ H : ?P h |- ?Q h ] => assert (P ===> Q) by cancel
end.
Transparent himp.
apply H0; auto.
Opaque himp.
Qed. Qed.
Lemma HtReturn' : forall P {result : Set} (v : result) Q, Lemma HtReturn' : forall P {result : Set} (v : result) Q,
@ -1183,7 +1161,7 @@ Proof.
assumption. assumption.
apply invert_Free in H. apply invert_Free in H.
assert (((exists vs : list nat, a |--> vs * [|Datatypes.length vs = numWords|]) * Q tt)%sep h) by auto. assert ((a |->? numWords * Q tt)%sep h) by auto.
apply HtReturn'. apply HtReturn'.
unfold himp; simp. unfold himp; simp.
eapply do_deallocate. eapply do_deallocate.
@ -1196,7 +1174,7 @@ Lemma deallocate_None : forall a' numWords h a,
Proof. Proof.
induct numWords; simp. induct numWords; simp.
rewrite IHnumWords; simp. rewrite IHnumWords; simp.
cases (a + numWords ==n a'); simp. cases (a ==n a'); simp.
Qed. Qed.
Lemma preservation_finite : forall {result} (c : cmd result) h c' h' bound, Lemma preservation_finite : forall {result} (c : cmd result) h c' h' bound,
@ -1400,10 +1378,11 @@ Proof.
assumption. assumption.
Qed. Qed.
Ltac basic := apply HtReturn' || eapply HtRead' || eapply HtWrite || eapply HtAlloc Ltac basic := apply HtReturn' || eapply HtWrite || eapply HtAlloc || eapply HtFree.
|| (eapply HtRead''; solve [ cancel ]).
Ltac step0 := basic || eapply HtBind || (eapply use_lemma; [ basic | cancel; auto ]) Ltac step0 := basic || eapply HtBind || (eapply use_lemma; [ basic | cancel; auto ])
|| (eapply use_lemma; [ eapply HtRead' | solve [ cancel; auto ] ])
|| (eapply HtRead''; solve [ cancel ])
|| (eapply HtStrengthen; [ eapply use_lemma; [ basic | cancel; auto ] | ]) || (eapply HtStrengthen; [ eapply use_lemma; [ basic | cancel; auto ] | ])
|| (eapply HtConsequence; [ apply HtFail | .. ]). || (eapply HtConsequence; [ apply HtFail | .. ]).
Ltac step := step0; simp. Ltac step := step0; simp.
@ -1501,6 +1480,19 @@ Qed.
Opaque init. Opaque init.
Theorem the_circle_of_life_ok :
{{emp}}
p <- init;
Free p 2
{{_ ~> emp}}.
Proof.
step.
use init_ok.
simp.
step.
cancel.
Qed.
Theorem ultra_combo_ok : Theorem ultra_combo_ok :
{{emp}} {{emp}}
p <- init; p <- init;