pl/frap
1
0
Fork 0
mirror of https://github.com/achlipala/frap.git synced 2024-11-27 23:06:20 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions

Ported to Coq 8.15

Browse source
This commit is contained in:
Adam Chlipala 2022-01-29 15:13:09 -05:00
parent 1b43aa9aea
commit d745f0802e
11 changed files with 25 additions and 17 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
ConcurrentSeparationLogic.v
View file

@ -426,7 +426,6 @@ Proof.
simp. simp.
cancel; auto. cancel; auto.
subst; cancel. subst; cancel.
cancel; auto.
Qed. Qed.
Theorem HtRead'' : forall linvs p P R, Theorem HtRead'' : forall linvs p P R,
@ -448,6 +447,8 @@ Proof.
constructor. constructor.
simp. simp.
cancel. cancel.
subst.
assumption.
Qed. Qed.
Ltac basic := apply HtReturn' || eapply HtWrite || eapply HtAlloc || eapply HtFree Ltac basic := apply HtReturn' || eapply HtWrite || eapply HtAlloc || eapply HtFree

3
ConcurrentSeparationLogic_template.v
View file

@ -407,7 +407,6 @@ Proof.
simp. simp.
cancel; auto. cancel; auto.
subst; cancel. subst; cancel.
cancel; auto.
Qed. Qed.
Theorem HtRead'' : forall linvs p P R, Theorem HtRead'' : forall linvs p P R,
@ -429,6 +428,8 @@ Proof.
constructor. constructor.
simp. simp.
cancel. cancel.
subst.
assumption.
Qed. Qed.
Ltac basic := apply HtReturn' || eapply HtWrite || eapply HtAlloc || eapply HtFree Ltac basic := apply HtReturn' || eapply HtWrite || eapply HtAlloc || eapply HtFree

11
Connecting.v
View file

@ -582,6 +582,8 @@ Module MixedEmbedded(Import BW : BIT_WIDTH).
constructor. constructor.
simp. simp.
cancel. cancel.
subst.
assumption.
Qed. Qed.
Transparent heq himp lift star exis ptsto. Transparent heq himp lift star exis ptsto.
@ -651,7 +653,7 @@ Module MixedEmbedded(Import BW : BIT_WIDTH).
repeat rewrite lookup_join2 by (simp; sets); reflexivity. repeat rewrite lookup_join2 by (simp; sets); reflexivity.
unfold disjoint in *; simp. unfold disjoint in *; simp.
cases (weq a0 a); simp. cases (weq a0 a); simp.
apply H1 with (a0 := a). apply H1 with (a := a).
unfold heap1; simp. unfold heap1; simp.
equality. equality.
assumption. assumption.
@ -817,7 +819,6 @@ Module MixedEmbedded(Import BW : BIT_WIDTH).
simp. simp.
cancel; auto. cancel; auto.
subst; cancel. subst; cancel.
cancel; auto.
Qed. Qed.
Theorem HtRead'' : forall p P R, Theorem HtRead'' : forall p P R,
@ -2666,7 +2667,7 @@ Module MixedToDeep(Import BW : BIT_WIDTH).
rewrite lookup_join2 by (eapply lookup_None_dom; simplify; eauto). rewrite lookup_join2 by (eapply lookup_None_dom; simplify; eauto).
eassumption. eassumption.
Grab Existential Variables. Unshelve.
exact (^0) || exact (Return (^0)). exact (^0) || exact (Return (^0)).
exact (^0) || exact (Return (^0)). exact (^0) || exact (Return (^0)).
exact (^0) || exact (Return (^0)). exact (^0) || exact (Return (^0)).
@ -3159,7 +3160,7 @@ Module MixedToDeep(Import BW : BIT_WIDTH).
eexists. eexists.
repeat econstructor. repeat econstructor.
Grab Existential Variables. Unshelve.
exact (^0) || exact (Return (^0)). exact (^0) || exact (Return (^0)).
exact (^0) || exact (Return (^0)). exact (^0) || exact (Return (^0)).
exact (^0) || exact (Return (^0)). exact (^0) || exact (Return (^0)).
@ -3313,8 +3314,6 @@ Module MixedToDeep(Import BW : BIT_WIDTH).
simp. simp.
step. step.
cancel. cancel.
subst.
cancel.
Qed. Qed.
Theorem incrementer_compiled_ok : forall p v, Theorem incrementer_compiled_ok : forall p v,

2
DataAbstraction.v
View file

@ -1328,7 +1328,7 @@ Module FindDuplicates (FS : FINITE_SET).
invert H0. invert H0.
exfalso. exfalso.
apply H with (x3 := x). apply H with (x := x).
exists x0. exists x0.
exists x1. exists x1.
exists x2. exists x2.

2
DataAbstraction_template.v
View file

@ -1144,7 +1144,7 @@ Module FindDuplicates (FS : FINITE_SET).
invert H0. invert H0.
exfalso. exfalso.
apply H with (x3 := x). apply H with (x := x).
exists x0. exists x0.
exists x1. exists x1.
exists x2. exists x2.

2
DeepAndShallowEmbeddings.v
View file

@ -657,7 +657,7 @@ Module Deeper.
end). end).
cases (r ==n needle); ht. cases (r ==n needle); ht.
cases (i ==n acc); simp. cases (i ==n acc); simp.
apply H3 with (i0 := i); auto. apply H3 with (i := i); auto.
Qed. Qed.
(* The single-stepping interpreter forms the basis for defining transition (* The single-stepping interpreter forms the basis for defining transition

5
FrapWithoutSets.v
View file

@ -454,3 +454,8 @@ Ltac unfold_recurse f k :=
linear_arithmetic). *) linear_arithmetic). *)
Arguments N.mul: simpl never. Arguments N.mul: simpl never.
Arguments N.add: simpl never. Arguments N.add: simpl never.
Definition IF_then_else (p q1 q2 : Prop) :=
(p /\ q1) \/ (~p /\ q2).
Notation "'IF' p 'then' q1 'else' q2" := (IF_then_else p q1 q2) (at level 95).

2
ProgramDerivation.v
View file

@ -375,7 +375,7 @@ Proof.
| [ H : (_, _) = (_, _) |- _ ] => invert H | [ H : (_, _) = (_, _) |- _ ] => invert H
end; eauto. end; eauto.
Grab Existential Variables. Unshelve.
exact 0. exact 0.
Qed. Qed.

5
SeparationLogic.v
View file

@ -666,6 +666,8 @@ Proof.
constructor. constructor.
simp. simp.
cancel. cancel.
subst.
assumption.
Qed. Qed.
(* Temporarily transparent again! *) (* Temporarily transparent again! *)
@ -736,7 +738,7 @@ Proof.
repeat rewrite lookup_join2 by (simp; sets); reflexivity. repeat rewrite lookup_join2 by (simp; sets); reflexivity.
unfold disjoint in *; simp. unfold disjoint in *; simp.
cases (a0 ==n a); simp. cases (a0 ==n a); simp.
apply H1 with (a0 := a). apply H1 with (a := a).
unfold heap1; simp. unfold heap1; simp.
equality. equality.
assumption. assumption.
@ -959,7 +961,6 @@ Proof.
simp. simp.
cancel; auto. cancel; auto.
subst; cancel. subst; cancel.
cancel; auto.
Qed. Qed.
Theorem HtRead'' : forall p P R, Theorem HtRead'' : forall p P R,

5
SeparationLogic_template.v
View file

@ -371,7 +371,6 @@ Proof.
simp. simp.
cancel; auto. cancel; auto.
subst; cancel. subst; cancel.
cancel; auto.
Qed. Qed.
Theorem HtRead'' : forall p P R, Theorem HtRead'' : forall p P R,
@ -393,6 +392,8 @@ Proof.
constructor. constructor.
simp. simp.
cancel. cancel.
subst.
assumption.
Qed. Qed.
@ -984,7 +985,7 @@ Proof.
repeat rewrite lookup_join2 by (simp; sets); reflexivity. repeat rewrite lookup_join2 by (simp; sets); reflexivity.
unfold disjoint in *; simp. unfold disjoint in *; simp.
cases (a0 ==n a); simp. cases (a0 ==n a); simp.
apply H1 with (a0 := a). apply H1 with (a := a).
unfold heap1; simp. unfold heap1; simp.
equality. equality.
assumption. assumption.

2
frap_book.tex
View file

@ -6094,7 +6094,7 @@ The project home page is:
\begin{center} \begin{center}
\url{https://coq.inria.fr/} \url{https://coq.inria.fr/}
\end{center} \end{center}
The code associated with this book is designed to work with Coq versions 8.9 and higher. The code associated with this book is designed to work with Coq versions 8.11 and higher.
The project Web site makes a number of versions available, and versions are also available in popular OS package distributions, along with binaries for platforms where open-source package systems are less common. The project Web site makes a number of versions available, and versions are also available in popular OS package distributions, along with binaries for platforms where open-source package systems are less common.
We assume that readers have installed Coq by one of those means or another. We assume that readers have installed Coq by one of those means or another.
It will also be almost essential to use some graphical interface for Coq editing. It will also be almost essential to use some graphical interface for Coq editing.