pl/frap
1
0
Fork 0
mirror of https://github.com/achlipala/frap.git synced 2025-01-24 15:26:10 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions

ConcurrentSeparationLogic: more automation in examples

Browse source
This commit is contained in:
Adam Chlipala 2016-04-28 10:07:43 -04:00
parent a242a93a7e
commit 6e80356fed
1 changed files with 14 additions and 90 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

104
ConcurrentSeparationLogic.v
View file

@ -493,50 +493,23 @@ Theorem incrementers_ok :
Proof. Proof.
unfold incrementer, incrementer_inv. unfold incrementer, incrementer_inv.
fork (emp%sep) (emp%sep). fork (emp%sep) (emp%sep).
loop_inv0 (fun _ : loop_outcome unit => emp%sep).
simp. loop_inv (fun _ : loop_outcome unit => emp%sep).
step. cases (r0 ==n 0); ht.
step.
simp.
step.
step.
simp.
step.
step.
simp.
step.
step.
simp.
cases (r0 ==n 0).
step.
cancel. cancel.
linear_arithmetic. linear_arithmetic.
cancel. cancel.
step.
cancel. cancel.
cancel. cancel.
loop_inv0 (fun _ : loop_outcome unit => emp%sep).
simp. loop_inv (fun _ : loop_outcome unit => emp%sep).
step. cases (r0 ==n 0); ht.
step.
simp.
step.
step.
simp.
step.
step.
simp.
step.
step.
simp.
cases (r0 ==n 0).
step.
cancel. cancel.
linear_arithmetic. linear_arithmetic.
cancel. cancel.
step.
cancel. cancel.
cancel. cancel.
cancel. cancel.
cancel. cancel.
Qed. Qed.
@ -618,79 +591,29 @@ Theorem producer_consumer_ok :
[producer_consumer_inv] ||- {{emp}} producer || consumer {{_ ~> emp}}. [producer_consumer_inv] ||- {{emp}} producer || consumer {{_ ~> emp}}.
Proof. Proof.
unfold producer_consumer_inv, producer, consumer. unfold producer_consumer_inv, producer, consumer.
fork (emp%sep) (emp%sep). fork (emp%sep) (emp%sep); ht.
step. loop_inv (fun o => [| isEven (valueOf o) = true |]%sep).
loop_inv0 (fun o => [| isEven (valueOf o) = true |]%sep).
simp.
step.
step.
simp.
step.
step.
simp.
step.
step.
simp.
step.
step.
simp.
step.
step.
simp.
step.
step.
simp.
step.
step.
erewrite (linkedList_nonnull _ H0). erewrite (linkedList_nonnull _ H0).
cancel. cancel.
simp. simp.
rewrite H1, H4. rewrite H1, H4.
simp. simp.
simp. simp.
step.
cancel. cancel.
cancel. cancel.
cancel. cancel.
step.
cancel.
loop_inv0 (fun _ : loop_outcome unit => emp%sep). loop_inv (fun _ : loop_outcome unit => emp%sep).
simp.
step.
step.
simp.
step.
step.
simp.
cases (r0 ==n 0). cases (r0 ==n 0).
step. ht.
step.
simp.
step.
cancel. cancel.
setoid_rewrite (linkedList_nonnull _ n). setoid_rewrite (linkedList_nonnull _ n).
step. ht.
step.
simp.
step.
step.
simp.
step.
step.
apply andb_true_iff in H. apply andb_true_iff in H.
simp. simp.
step. cases (isEven r4); ht.
step.
simp.
step.
step.
simp.
cases (isEven r4).
step.
cancel. cancel.
step.
cancel. cancel.
simp. simp.
rewrite Heq in H2. rewrite Heq in H2.
@ -699,6 +622,7 @@ Proof.
cancel. cancel.
cancel. cancel.
cancel. cancel.
cancel. cancel.
Qed. Qed.