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

Revising SeparationLogic before class

Browse source
This commit is contained in:
Adam Chlipala 2020-04-11 14:33:14 -04:00
parent 000c22f7f1
commit 8a554ded4c
2 changed files with 16 additions and 18 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

22
SeparationLogic.v
View file

@ -12,8 +12,8 @@ Set Asymmetric Patterns.
Definition heap := fmap nat nat. Definition heap := fmap nat nat.
Hint Extern 1 (_ <= _) => linear_arithmetic. Hint Extern 1 (_ <= _) => linear_arithmetic : core.
Hint Extern 1 (@eq nat _ _) => linear_arithmetic. Hint Extern 1 (@eq nat _ _) => linear_arithmetic : core.
Ltac simp := repeat (simplify; subst; propositional; Ltac simp := repeat (simplify; subst; propositional;
try match goal with try match goal with
@ -181,7 +181,7 @@ Module Import S <: SEP.
t. t.
Qed. Qed.
Hint Resolve split_empty_bwd'. Hint Resolve split_empty_bwd' : core.
Theorem extra_lift : forall (P : Prop) p, Theorem extra_lift : forall (P : Prop) p,
P P
@ -376,7 +376,7 @@ Proof.
unfold star, himp in *; simp; eauto 7. unfold star, himp in *; simp; eauto 7.
Qed. Qed.
Hint Constructors hoare_triple. Hint Constructors hoare_triple : core.
Lemma invert_Bind : forall {result' result} (c1 : cmd result') (c2 : result' -> cmd result) P Q, Lemma invert_Bind : forall {result' result} (c1 : cmd result') (c2 : result' -> cmd result) P Q,
hoare_triple P (Bind c1 c2) Q hoare_triple P (Bind c1 c2) Q
@ -785,7 +785,7 @@ Proof.
eauto using deallocate_None. eauto using deallocate_None.
Qed. Qed.
Hint Constructors step. Hint Constructors step : core.
Lemma progress : forall {result} (c : cmd result) P Q, Lemma progress : forall {result} (c : cmd result) P Q,
hoare_triple P c Q hoare_triple P c Q
@ -1151,7 +1151,7 @@ Proof.
heq; cases ls; cancel. heq; cases ls; cancel.
Qed. Qed.
Theorem linkedList_nonnull : forall p ls, Theorem linkedList_nonnull : forall {p ls},
p <> 0 p <> 0
-> linkedList p ls === exists x ls' p', [| ls = x :: ls' |] * p |--> [x; p'] * linkedList p' ls'. -> linkedList p ls === exists x ls' p', [| ls = x :: ls' |] * p |--> [x; p'] * linkedList p' ls'.
Proof. Proof.
@ -1210,14 +1210,14 @@ Proof.
(* We use [setoid_rewrite] for rewriting under binders ([exists], in this (* We use [setoid_rewrite] for rewriting under binders ([exists], in this
* case). Note that we also specify hypothesis [n] explicitly, since * case). Note that we also specify hypothesis [n] explicitly, since
* [setoid_rewrite] isn't smart enough to infer parameters otherwise. *) * [setoid_rewrite] isn't smart enough to infer parameters otherwise. *)
setoid_rewrite (linkedList_nonnull _ n). setoid_rewrite (linkedList_nonnull n).
step. step.
simp. simp.
step. step.
step. step.
simp. simp.
step. step.
setoid_rewrite (linkedList_nonnull _ n). setoid_rewrite (linkedList_nonnull n).
cancel. cancel.
simp. simp.
setoid_rewrite linkedList_null. setoid_rewrite linkedList_null.
@ -1313,7 +1313,7 @@ Proof.
simp. simp.
Qed. Qed.
Hint Resolve move_along. Hint Resolve move_along : core.
Theorem length_ok : forall p ls, Theorem length_ok : forall p ls,
{{linkedList p ls}} {{linkedList p ls}}
@ -1344,12 +1344,11 @@ Proof.
cancel. cancel.
simp. simp.
step. step.
setoid_rewrite (linkedList_nonnull _ n). setoid_rewrite (linkedList_nonnull n).
step. step.
simp. simp.
step. step.
cancel. cancel.
eauto.
simp. simp.
setoid_rewrite <- linkedListSegment_append. setoid_rewrite <- linkedListSegment_append.
cancel. cancel.
@ -1362,7 +1361,6 @@ Proof.
step. step.
cancel. cancel.
simp. simp.
simp.
rewrite linkedListSegment_null. rewrite linkedListSegment_null.
rewrite linkedList_null. rewrite linkedList_null.
cancel. cancel.

12
SeparationLogic_template.v
View file

@ -9,8 +9,8 @@ Notation "m $! k" := (match m $? k with Some n => n | None => O end) (at level 3
Definition heap := fmap nat nat. Definition heap := fmap nat nat.
Definition assertion := heap -> Prop. Definition assertion := heap -> Prop.
Hint Extern 1 (_ <= _) => linear_arithmetic. Hint Extern 1 (_ <= _) => linear_arithmetic : core.
Hint Extern 1 (@eq nat _ _) => linear_arithmetic. Hint Extern 1 (@eq nat _ _) => linear_arithmetic : core.
Ltac simp := repeat (simplify; subst; propositional; Ltac simp := repeat (simplify; subst; propositional;
try match goal with try match goal with
@ -165,7 +165,7 @@ Module Import S <: SEP.
t. t.
Qed. Qed.
Hint Resolve split_empty_bwd'. Hint Resolve split_empty_bwd' : core.
Theorem extra_lift : forall (P : Prop) p, Theorem extra_lift : forall (P : Prop) p,
P P
@ -601,7 +601,7 @@ Proof.
simp. simp.
Qed. Qed.
Hint Resolve move_along. Hint Resolve move_along : core.
Theorem length_ok : forall p ls, Theorem length_ok : forall p ls,
{{linkedList p ls}} {{linkedList p ls}}
@ -637,7 +637,7 @@ Proof.
unfold star, himp in *; simp; eauto 7. unfold star, himp in *; simp; eauto 7.
Qed. Qed.
Hint Constructors hoare_triple. Hint Constructors hoare_triple : core.
Lemma invert_Bind : forall {result' result} (c1 : cmd result') (c2 : result' -> cmd result) P Q, Lemma invert_Bind : forall {result' result} (c1 : cmd result') (c2 : result' -> cmd result) P Q,
hoare_triple P (Bind c1 c2) Q hoare_triple P (Bind c1 c2) Q
@ -1033,7 +1033,7 @@ Proof.
eauto using deallocate_None. eauto using deallocate_None.
Qed. Qed.
Hint Constructors step. Hint Constructors step : core.
Lemma progress : forall {result} (c : cmd result) P Q, Lemma progress : forall {result} (c : cmd result) P Q,
hoare_triple P c Q hoare_triple P c Q