From d745f0802e777d138b5064577037e422289aa447 Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Sat, 29 Jan 2022 15:13:09 -0500 Subject: [PATCH] Ported to Coq 8.15 --- ConcurrentSeparationLogic.v | 3 ++- ConcurrentSeparationLogic_template.v | 3 ++- Connecting.v | 11 +++++------ DataAbstraction.v | 2 +- DataAbstraction_template.v | 2 +- DeepAndShallowEmbeddings.v | 2 +- FrapWithoutSets.v | 5 +++++ ProgramDerivation.v | 2 +- SeparationLogic.v | 5 +++-- SeparationLogic_template.v | 5 +++-- frap_book.tex | 2 +- 11 files changed, 25 insertions(+), 17 deletions(-) diff --git a/ConcurrentSeparationLogic.v b/ConcurrentSeparationLogic.v index d0223e0..5c3ed11 100644 --- a/ConcurrentSeparationLogic.v +++ b/ConcurrentSeparationLogic.v @@ -426,7 +426,6 @@ Proof. simp. cancel; auto. subst; cancel. - cancel; auto. Qed. Theorem HtRead'' : forall linvs p P R, @@ -448,6 +447,8 @@ Proof. constructor. simp. cancel. + subst. + assumption. Qed. Ltac basic := apply HtReturn' || eapply HtWrite || eapply HtAlloc || eapply HtFree diff --git a/ConcurrentSeparationLogic_template.v b/ConcurrentSeparationLogic_template.v index 4e06763..f7ec4e0 100644 --- a/ConcurrentSeparationLogic_template.v +++ b/ConcurrentSeparationLogic_template.v @@ -407,7 +407,6 @@ Proof. simp. cancel; auto. subst; cancel. - cancel; auto. Qed. Theorem HtRead'' : forall linvs p P R, @@ -429,6 +428,8 @@ Proof. constructor. simp. cancel. + subst. + assumption. Qed. Ltac basic := apply HtReturn' || eapply HtWrite || eapply HtAlloc || eapply HtFree diff --git a/Connecting.v b/Connecting.v index 2374bab..de98097 100644 --- a/Connecting.v +++ b/Connecting.v @@ -582,6 +582,8 @@ Module MixedEmbedded(Import BW : BIT_WIDTH). constructor. simp. cancel. + subst. + assumption. Qed. 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. unfold disjoint in *; simp. cases (weq a0 a); simp. - apply H1 with (a0 := a). + apply H1 with (a := a). unfold heap1; simp. equality. assumption. @@ -817,7 +819,6 @@ Module MixedEmbedded(Import BW : BIT_WIDTH). simp. cancel; auto. subst; cancel. - cancel; auto. Qed. 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). eassumption. - Grab Existential Variables. + Unshelve. 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. repeat econstructor. - Grab Existential Variables. + Unshelve. 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. step. cancel. - subst. - cancel. Qed. Theorem incrementer_compiled_ok : forall p v, diff --git a/DataAbstraction.v b/DataAbstraction.v index bc371f7..516f8fd 100644 --- a/DataAbstraction.v +++ b/DataAbstraction.v @@ -1328,7 +1328,7 @@ Module FindDuplicates (FS : FINITE_SET). invert H0. exfalso. - apply H with (x3 := x). + apply H with (x := x). exists x0. exists x1. exists x2. diff --git a/DataAbstraction_template.v b/DataAbstraction_template.v index 1800038..a3acb78 100644 --- a/DataAbstraction_template.v +++ b/DataAbstraction_template.v @@ -1144,7 +1144,7 @@ Module FindDuplicates (FS : FINITE_SET). invert H0. exfalso. - apply H with (x3 := x). + apply H with (x := x). exists x0. exists x1. exists x2. diff --git a/DeepAndShallowEmbeddings.v b/DeepAndShallowEmbeddings.v index 309d2ed..c0459ef 100644 --- a/DeepAndShallowEmbeddings.v +++ b/DeepAndShallowEmbeddings.v @@ -657,7 +657,7 @@ Module Deeper. end). cases (r ==n needle); ht. cases (i ==n acc); simp. - apply H3 with (i0 := i); auto. + apply H3 with (i := i); auto. Qed. (* The single-stepping interpreter forms the basis for defining transition diff --git a/FrapWithoutSets.v b/FrapWithoutSets.v index e68f595..8bb3adc 100644 --- a/FrapWithoutSets.v +++ b/FrapWithoutSets.v @@ -454,3 +454,8 @@ Ltac unfold_recurse f k := linear_arithmetic). *) Arguments N.mul: 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). diff --git a/ProgramDerivation.v b/ProgramDerivation.v index 52c9c1d..b218c62 100644 --- a/ProgramDerivation.v +++ b/ProgramDerivation.v @@ -375,7 +375,7 @@ Proof. | [ H : (_, _) = (_, _) |- _ ] => invert H end; eauto. - Grab Existential Variables. + Unshelve. exact 0. Qed. diff --git a/SeparationLogic.v b/SeparationLogic.v index 6a9e3ba..3c436fa 100644 --- a/SeparationLogic.v +++ b/SeparationLogic.v @@ -666,6 +666,8 @@ Proof. constructor. simp. cancel. + subst. + assumption. Qed. (* Temporarily transparent again! *) @@ -736,7 +738,7 @@ Proof. repeat rewrite lookup_join2 by (simp; sets); reflexivity. unfold disjoint in *; simp. cases (a0 ==n a); simp. - apply H1 with (a0 := a). + apply H1 with (a := a). unfold heap1; simp. equality. assumption. @@ -959,7 +961,6 @@ Proof. simp. cancel; auto. subst; cancel. - cancel; auto. Qed. Theorem HtRead'' : forall p P R, diff --git a/SeparationLogic_template.v b/SeparationLogic_template.v index 42df9ee..dce0b58 100644 --- a/SeparationLogic_template.v +++ b/SeparationLogic_template.v @@ -371,7 +371,6 @@ Proof. simp. cancel; auto. subst; cancel. - cancel; auto. Qed. Theorem HtRead'' : forall p P R, @@ -393,6 +392,8 @@ Proof. constructor. simp. cancel. + subst. + assumption. Qed. @@ -984,7 +985,7 @@ Proof. repeat rewrite lookup_join2 by (simp; sets); reflexivity. unfold disjoint in *; simp. cases (a0 ==n a); simp. - apply H1 with (a0 := a). + apply H1 with (a := a). unfold heap1; simp. equality. assumption. diff --git a/frap_book.tex b/frap_book.tex index f27083b..757d58a 100644 --- a/frap_book.tex +++ b/frap_book.tex @@ -6094,7 +6094,7 @@ The project home page is: \begin{center} \url{https://coq.inria.fr/} \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. 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.