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

Fixes for Coq 8.4

Browse source
This commit is contained in:
Adam Chlipala 2016-05-01 20:09:39 -04:00
parent daac5734b0
commit 1cb930d8d1
2 changed files with 28 additions and 23 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

30
ConcurrentSeparationLogic.v
View file

@ -662,12 +662,12 @@ 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 _ f). match goal with
| [ H : r = 0 -> False |- _ ] => erewrite (linkedList_nonnull _ H)
end.
cancel. cancel.
simp. simp.
rewrite e, e0. apply andb_true_iff; propositional.
simp.
simp.
cancel. cancel.
cancel. cancel.
cancel. cancel.
@ -768,12 +768,12 @@ 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 _ f). match goal with
| [ H : r = 0 -> False |- _ ] => erewrite (linkedList_nonnull _ H)
end.
cancel. cancel.
simp. simp.
rewrite e, e0. apply andb_true_iff; propositional.
simp.
simp.
cancel. cancel.
cancel. cancel.
cancel. cancel.
@ -1314,7 +1314,7 @@ Proof.
Qed. Qed.
Lemma guarded_impl : forall P Q p, Lemma guarded_impl : forall P Q p,
P <-> Q (P <-> Q)
-> (P ===> p) ===> (Q ===> p). -> (P ===> p) ===> (Q ===> p).
Proof. Proof.
simp. simp.
@ -1333,7 +1333,7 @@ Lemma lockChunks_lock' : forall l I linvs (f : nat -> nat) a,
Proof. Proof.
induct linvs; simplify. induct linvs; simplify.
cases a; simplify; equality. cases a; simplify; try unfold error in *; equality.
cases a0; simplify. cases a0; simplify.
invert H0. invert H0.
@ -1376,7 +1376,7 @@ Lemma lockChunks_unlock' : forall l I linvs (f : nat -> nat) a,
Proof. Proof.
induct linvs; simplify. induct linvs; simplify.
cases a; simplify; equality. cases a; simplify; try unfold error in *; equality.
cases a0; simplify. cases a0; simplify.
invert H0. invert H0.
@ -1645,8 +1645,10 @@ Proof.
simp. simp.
cases (notAboutToFail c0); auto. cases (notAboutToFail c0); auto.
eapply hoare_triple_notAboutToFail in Heq; eauto. eapply hoare_triple_notAboutToFail in Heq; eauto.
apply use_himp with (Q := [| False |]%sep) in H3. assert ([| False |]%sep f).
invert H3; propositional. apply use_himp with (x * lockChunks s linvs)%sep.
rewrite Heq. rewrite Heq.
cancel. apply False_star.
assumption.
invert H2; propositional.
Qed. Qed.

21
ConcurrentSeparationLogic_template.v
View file

@ -684,11 +684,12 @@ 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 _ f). match goal with
| [ H : r = 0 -> False |- _ ] => erewrite (linkedList_nonnull _ H)
end.
cancel. cancel.
simp. simp.
rewrite e, e0. apply andb_true_iff; propositional.
simp.
cancel. cancel.
cancel. cancel.
cancel. cancel.
@ -1216,7 +1217,7 @@ Proof.
Qed. Qed.
Lemma guarded_impl : forall P Q p, Lemma guarded_impl : forall P Q p,
P <-> Q (P <-> Q)
-> (P ===> p) ===> (Q ===> p). -> (P ===> p) ===> (Q ===> p).
Proof. Proof.
simp. simp.
@ -1235,7 +1236,7 @@ Lemma lockChunks_lock' : forall l I linvs (f : nat -> nat) a,
Proof. Proof.
induct linvs; simplify. induct linvs; simplify.
cases a; simplify; equality. cases a; simplify; try unfold error in *; equality.
cases a0; simplify. cases a0; simplify.
invert H0. invert H0.
@ -1278,7 +1279,7 @@ Lemma lockChunks_unlock' : forall l I linvs (f : nat -> nat) a,
Proof. Proof.
induct linvs; simplify. induct linvs; simplify.
cases a; simplify; equality. cases a; simplify; try unfold error in *; equality.
cases a0; simplify. cases a0; simplify.
invert H0. invert H0.
@ -1547,8 +1548,10 @@ Proof.
simp. simp.
cases (notAboutToFail c0); auto. cases (notAboutToFail c0); auto.
eapply hoare_triple_notAboutToFail in Heq; eauto. eapply hoare_triple_notAboutToFail in Heq; eauto.
apply use_himp with (Q := [| False |]%sep) in H3. assert ([| False |]%sep f).
invert H3; propositional. apply use_himp with (x * lockChunks s linvs)%sep.
rewrite Heq. rewrite Heq.
cancel. apply False_star.
assumption.
invert H2; propositional.
Qed. Qed.