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

Finalizing ConcurrentSeparationLogic

Browse source
This commit is contained in:
Adam Chlipala 2016-05-01 19:45:51 -04:00
parent 035bfa57ee
commit daac5734b0
5 changed files with 1578 additions and 20 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

16
ConcurrentSeparationLogic.v
View file

@ -662,10 +662,10 @@ Proof.
fork (emp%sep) (emp%sep); ht. fork (emp%sep) (emp%sep); ht.
loop_inv (fun o => [| isEven (valueOf o) = true |]%sep). loop_inv (fun o => [| isEven (valueOf o) = true |]%sep).
erewrite (linkedList_nonnull _ H0). erewrite (linkedList_nonnull _ f).
cancel. cancel.
simp. simp.
rewrite H1, H4. rewrite e, e0.
simp. simp.
simp. simp.
cancel. cancel.
@ -684,7 +684,7 @@ Proof.
cancel. cancel.
cancel. cancel.
simp. simp.
rewrite Heq in H2. rewrite Heq in H0.
simp. simp.
equality. equality.
cancel. cancel.
@ -768,10 +768,10 @@ Proof.
fork (emp%sep) (emp%sep); ht. fork (emp%sep) (emp%sep); ht.
loop_inv (fun o => [| isEven (valueOf o) = true |]%sep). loop_inv (fun o => [| isEven (valueOf o) = true |]%sep).
erewrite (linkedList_nonnull _ H0). erewrite (linkedList_nonnull _ f).
cancel. cancel.
simp. simp.
rewrite H1, H4. rewrite e, e0.
simp. simp.
simp. simp.
cancel. cancel.
@ -787,10 +787,10 @@ Proof.
ht. ht.
apply andb_true_iff in H. apply andb_true_iff in H.
simp. simp.
erewrite (linkedList_nonnull _ H1). erewrite (linkedList_nonnull _ n).
cancel. cancel.
simp. simp.
apply andb_true_iff in H0. apply andb_true_iff in H1.
apply andb_true_iff. apply andb_true_iff.
simp. simp.
cancel. cancel.
@ -811,7 +811,7 @@ Proof.
cancel. cancel.
cancel. cancel.
simp. simp.
rewrite Heq in H2. rewrite Heq in H0.
simp. simp.
equality. equality.
cancel. cancel.

1554
ConcurrentSeparationLogic_template.v Normal file
View file

File diff suppressed because it is too large Load diff

3
README.md
View file

@ -2,7 +2,7 @@
This is an in-progress, open-source book by [Adam Chlipala](http://adam.chlipala.net/) simultaneously introducing [the Coq proof assistant](http://coq.inria.fr/) and techniques for proving correctness of programs. That is, the game is doing completely rigorous, machine-checked mathematical proofs, showing that programs meet their specifications. This is an in-progress, open-source book by [Adam Chlipala](http://adam.chlipala.net/) simultaneously introducing [the Coq proof assistant](http://coq.inria.fr/) and techniques for proving correctness of programs. That is, the game is doing completely rigorous, machine-checked mathematical proofs, showing that programs meet their specifications.
Just run `make` here to build everything, including the book `frap.pdf` and the accompanying Coq source modules. Just run `make` here to build everything, including the book `frap.pdf` and the accompanying Coq source modules. Alternatively, run `make lib' to build just the book library, not the chapter example files or PDF.
# Code associated with the different chapters # Code associated with the different chapters
@ -18,3 +18,4 @@ Just run `make` here to build everything, including the book `frap.pdf` and the
* Chapter 11: `DeepAndShallowEmbeddings.v` * Chapter 11: `DeepAndShallowEmbeddings.v`
* Chapter 12: `SeparationLogic.v` * Chapter 12: `SeparationLogic.v`
* Chapter 13: `SharedMemory.v` * Chapter 13: `SharedMemory.v`
* Chapter 14: `ConcurrentSeparationLogic.v`

23
SepCancel.v
View file

@ -430,13 +430,18 @@ Module Make(Import S : SEP).
normalize; repeat cancel1; repeat match goal with normalize; repeat cancel1; repeat match goal with
| [ H : _ /\ _ |- _ ] => destruct H | [ H : _ /\ _ |- _ ] => destruct H
| [ |- _ /\ _ ] => split | [ |- _ /\ _ ] => split
end; eassumption. end; eassumption || apply I.
Ltac cancel := hide_evars; normalize; repeat cancel1; restore_evars; Ltac beautify := repeat match goal with
repeat match goal with | [ H : True |- _ ] => clear H
| [ H : True |- _ ] => clear H | [ H : ?P, H' : ?P |- _ ] =>
| [ H : ?P, H' : ?P |- _ ] => clear H' match type of P with
end; | Prop => clear H'
end
| [ H : _ /\ _ |- _ ] => destruct H
end.
Ltac cancel := hide_evars; normalize; repeat cancel1; restore_evars; beautify;
try match goal with try match goal with
| [ |- _ ===> ?p * ?q ] => | [ |- _ ===> ?p * ?q ] =>
((is_evar p; fail 1) || apply star_cancel'') ((is_evar p; fail 1) || apply star_cancel'')
@ -478,9 +483,5 @@ Module Make(Import S : SEP).
basic_cancel basic_cancel
end) end)
| [ |- _ ===> _ ] => intuition (try congruence) | [ |- _ ===> _ ] => intuition (try congruence)
end; intuition idtac; end; intuition idtac; beautify.
repeat match goal with
| [ H : True |- _ ] => clear H
| [ H : ?P, H' : ?P |- _ ] => clear H'
end.
End Make. End Make.

2
_CoqProject
View file

@ -28,3 +28,5 @@ SepCancel.v
SeparationLogic_template.v SeparationLogic_template.v
SeparationLogic.v SeparationLogic.v
SharedMemory.v SharedMemory.v
ConcurrentSeparationLogic_template.v
ConcurrentSeparationLogic.v