1. Permit Coq 8.15.0 in Makefile

2. Make the concurrency part compatible with Coq 8.15.0
PrincetonUniversity · Jan 14, 2022 · 38b54f0 · 38b54f0
1 parent e00a515
commit 38b54f0
Show file tree

Hide file tree

Showing 5 changed files with 51 additions and 34 deletions.
diff --git a/Makefile b/Makefile
@@ -21,7 +21,7 @@ COQLIB=$(shell $(COQC) -where | tr -d '\r' | tr '\\' '/')
 
 # Check Coq version
 
-COQVERSION= 8.13.0 or-else 8.13.1 or-else 8.13.2 or-else 8.14.0 or-else 8.14.1
+COQVERSION= 8.13.0 or-else 8.13.1 or-else 8.13.2 or-else 8.14.0 or-else 8.14.1 or-else 8.15.0
 
 COQV=$(shell $(COQC) -v)
 ifneq ($(IGNORECOQVERSION),true)

diff --git a/atomics/general_locks.v b/atomics/general_locks.v
@@ -105,7 +105,7 @@ Lemma sync_commit_gen : forall {A B} {inv_names : invG} a Ei Eo (b : A -> B -> m
   (atomic_shift a Ei Eo b Q * my_half g sh x0 * R |-- |==> EX y, Q y * R' y)%I.
 Proof.
   intros; rewrite sepcon_assoc.
-  apply atomic_commit with (R'0 := fun y => R' y).
+  apply (@atomic_commit CS) with (R' := fun y => R' y).
   intros; iIntros "((my & R) & a)".
   iMod (Ha with "[$]") as (?) "[public a']".
   iPoseProof (ref_sub(P := P) with "[$my $public]") as "%".
@@ -120,7 +120,7 @@ Lemma sync_commit_same : forall {A B} {inv_names : invG} a Ei Eo (b : A -> B ->
   (atomic_shift a Ei Eo b Q * my_half g sh x0 * R |-- |==> EX y, Q y * R' y)%I.
 Proof.
   intros; rewrite sepcon_assoc.
-  apply atomic_commit with (R'0 := fun y => R' y).
+  apply (@atomic_commit CS) with (R' := fun y => R' y).
   intros; iIntros "((my & R) & a)".
   iMod (Ha with "[$]") as (?) "[public a']".
   iPoseProof (ref_sub(P := P) with "[$my $public]") as "%".
@@ -133,7 +133,8 @@ Lemma sync_commit_gen1 : forall {A B} {inv_names : invG} a Ei Eo (b : A -> B ->
     |==> (EX x0' x1' : G, !!(forall b, sepalg.join x0 b x1 -> sepalg.join x0' b x1') && (my_half g sh x0' * public_half g x1' -* |==> (EX y, b x y) * R')))%I)%I),
   (atomic_shift a Ei Eo b (fun _ => Q) * my_half g sh x0 * R |-- |==> Q * R')%I.
 Proof.
-  intros; rewrite sepcon_assoc; eapply derives_trans; [apply atomic_commit with (R'0 := fun _ => R')|].
+  intros; rewrite sepcon_assoc; eapply derives_trans; [apply (@atomic_commit CS) with
+      (R' := fun _ => R')|].
   - intros; iIntros "((my & R) & a)".
     iMod (Ha with "[$]") as (?) "[public a']".
     iPoseProof (ref_sub(P := P) with "[$my $public]") as "%".
@@ -149,7 +150,8 @@ Lemma sync_commit_same1 : forall {A B} {inv_names : invG} a Ei Eo (b : A -> B ->
     |==> (my_half g sh x0 * public_half g x1 -* |==> (EX y, b x y * R')))%I)%I),
   (atomic_shift a Ei Eo b (fun _ => Q) * my_half g sh x0 * R |-- |==> Q * R')%I.
 Proof.
-  intros; rewrite sepcon_assoc; eapply derives_trans; [apply atomic_commit with (R'0 := fun _ => R')|].
+  intros; rewrite sepcon_assoc; eapply derives_trans; [apply (@atomic_commit CS) with
+      (R' := fun _ => R')|].
   intros; iIntros "((my & R) & a)".
   iMod (Ha with "[$]") as (?) "[public a']".
   iPoseProof (ref_sub(P := P) with "[$my $public]") as "%".
@@ -197,7 +199,7 @@ Lemma two_sync_commit : forall {A B} {inv_names : invG} a Ei Eo (b : A -> B -> m
   (atomic_shift a Ei Eo b Q * my_half g1 sh1 x1 * my_half g2 sh2 x2 * R |-- |==> EX y, Q y * R' y)%I.
 Proof.
   intros; rewrite -> 2sepcon_assoc.
-  apply atomic_commit with (R'0 := fun y => R' y).
+  apply (@atomic_commit CS) with (R' := fun y => R' y).
   intros; iIntros "((my1 & my2 & R) & a)".
   iMod (Ha with "[$]") as (??) "((public1 & public2) &  a')".
   iPoseProof (ref_sub(P := P) with "[$my1 $public1]") as "%".
@@ -217,7 +219,7 @@ Lemma two_sync_commit1 : forall {A B} {inv_names : invG} a Ei Eo (b : A -> B ->
   (atomic_shift a Ei Eo b (fun _ => Q) * my_half g1 sh1 x1 * my_half g2 sh2 x2 * R |-- |==> Q * R')%I.
 Proof.
   intros; rewrite -> 2sepcon_assoc.
-  eapply derives_trans; [apply atomic_commit with (R'0 := fun _ => R')|].
+  eapply derives_trans; [apply (@atomic_commit CS) with (R' := fun _ => R')|].
   intros; iIntros "((my1 & my2 & R) & a)".
   iMod (Ha with "[$]") as (??) "((public1 & public2) &  a')".
   iPoseProof (ref_sub(P := P) with "[$my1 $public1]") as "%".

diff --git a/atomics/hashtable.v b/atomics/hashtable.v
@@ -419,7 +419,7 @@ Proof.
     intro Heq; apply In_Znth in Hin' as (i & Hi & ?); subst x.
     rewrite Zlength_sublist in Hi; try lia.
     rewrite Znth_sublist, Znth_rebase, Z.add_0_r in Heq by lia.
-    eapply NoDup_Znth_inj with (i0 := z)(j := (i + hash k) mod (Zlength m)) in Hwf.
+    eapply @NoDup_Znth_inj with (i := z)(j := (i + hash k) mod (Zlength m)) in Hwf.
     subst z.
     rewrite Zminus_mod_idemp_l, Z.add_simpl_r, Z.sub_0_r, Zmod_small in Hi; try lia.
     * destruct Hi; split; auto.

diff --git a/atomics/verif_hashtable_atomic.v b/atomics/verif_hashtable_atomic.v
@@ -318,8 +318,9 @@ Proof.
   { rewrite <- Hi1; intro Heq.
     apply Zmod_plus_inv in Heq; [|apply size_pos].
     rewrite !Zmod_small in Heq; lia. }
-  rewrite -> iter_sepcon_Znth_remove with (i0 := (j + hash k) mod size),
-                    iter_sepcon_Znth' with (i0 := j)(l := upto _)
+  rewrite -> @iter_sepcon_Znth_remove with (d := Inhabitant_Z)
+                                           (i := (j + hash k) mod size),
+                    @iter_sepcon_Znth' with (d := Inhabitant_Z) (i := j)(l := upto _)
     by (auto; rewrite -> Zlength_upto, Z2Nat.id; try lia).
   rewrite -> !Znth_upto by (rewrite -> Z2Nat.id; lia).
   unfold hashtable_entry at 1.
@@ -330,7 +331,7 @@ Proof.
   rewrite <- !sepcon_assoc, snap_master_join1 by auto.
   Intros; apply prop_right; simpl.
   eapply Forall_Znth in Hfail.
-  rewrite -> Znth_sublist, Z.add_0_r, Znth_rebase with (i0 := j) in Hfail; auto; try lia.
+  rewrite -> Znth_sublist, Z.add_0_r, @Znth_rebase with (i := j) in Hfail; auto; try lia.
   replace (Zlength keys) with size in Hfail; intuition; subst; intuition.
   { rewrite -> Zlength_sublist; auto; try lia.
     rewrite Zlength_rebase; lia. }
@@ -434,7 +435,7 @@ Proof.
       iIntros "([AS1 _] & P)".
       iMod ("AS1" with "P") as (HT) "[hashtable Hclose]".
       iDestruct "hashtable" as (T) "((% & excl) & entries)".
-      rewrite -> iter_sepcon_Znth' with (i0 := i1 mod size)
+      rewrite -> @iter_sepcon_Znth' with (d := Inhabitant_Z) (i := i1 mod size)
           by (rewrite -> ?Zlength_map, Zlength_upto, Z2Nat.id; lia).
       erewrite Znth_upto by (rewrite -> ?Zlength_upto, Z2Nat.id; lia).
       unfold hashtable_entry at 1.
@@ -497,7 +498,9 @@ Proof.
         iMod ("AS1" with "P") as (HT) "[hashtable Hclose]".
         iDestruct "hashtable" as (T) "((% & excl) & entries)".
         match goal with H : _ /\ _ /\ _ |- _ => destruct H as (? & ? & ?) end.
-        rewrite -> iter_sepcon_Znth with (i0 := i1 mod size)(f := hashtable_entry _ _ _)
+        rewrite -> @iter_sepcon_Znth with (d := Inhabitant_Z)
+                                          (i := i1 mod size)
+                                          (f := hashtable_entry _ _ _)
             by (rewrite -> ?Zlength_map, Zlength_upto, Z2Nat.id; try lia).
         erewrite Znth_upto by (rewrite -> ?Zlength_upto, Z2Nat.id; lia).
         unfold hashtable_entry at 1.
@@ -522,7 +525,8 @@ Proof.
         iFrame "snap snaps".
         iDestruct "Hclose" as "[Hclose _]"; iApply "Hclose".
         unfold hashtable; iExists (upd_Znth (i1 mod size) T (if eq_dec ki 0 then k else ki, vi)); iFrame "excl".
-        rewrite -> iter_sepcon_Znth with (i0 := i1 mod size)(l := upto (Z.to_nat size))
+        rewrite -> @iter_sepcon_Znth with (d := Inhabitant_Z) (i := i1 mod size)
+                                          (l := upto (Z.to_nat size))
           by (rewrite -> Zlength_upto, Z2Nat.id; lia).
         rewrite -> Znth_upto by (rewrite Z2Nat.id; lia).
         unfold hashtable_entry.
@@ -558,7 +562,7 @@ Proof.
           iIntros "(([AS1 _] & snap) & P)".
           iMod ("AS1" with "P") as (HT) "[hashtable Hclose]".
           iDestruct "hashtable" as (T) "((% & excl) & entries)".
-          rewrite -> iter_sepcon_Znth' with (i0 := i1 mod size)
+          rewrite -> @iter_sepcon_Znth' with (d := Inhabitant_Z) (i := i1 mod size)
             by (rewrite -> ?Zlength_map, Zlength_upto, Z2Nat.id; lia).
           erewrite Znth_upto by (rewrite -> ?Zlength_upto, Z2Nat.id; lia).
           unfold hashtable_entry at 1.
@@ -613,7 +617,8 @@ Proof.
         iMod ("AS1" with "P") as (HT) "[hashtable Hclose]".
         iDestruct "hashtable" as (T) "((% & excl) & entries)".
         match goal with H : _ /\ _ /\ _ |- _ => destruct H as (? & ? & ?) end.
-        rewrite -> iter_sepcon_Znth with (i0 := i1 mod size)(f := hashtable_entry _ _ _)
+        rewrite -> @iter_sepcon_Znth with (d := Inhabitant_Z)
+                                          (i := i1 mod size)(f := hashtable_entry _ _ _)
           by (rewrite -> Zlength_upto, Z2Nat.id; lia).
         rewrite -> Znth_upto by (rewrite -> Z2Nat.id; lia).
         unfold hashtable_entry at 1.
@@ -634,7 +639,8 @@ Proof.
         unfold hashtable.
         iFrame.
         iExists (upd_Znth (i1 mod size) T (k, v)).
-        rewrite -> iter_sepcon_Znth with (i0 := i1 mod size)(l := upto (Z.to_nat size))
+        rewrite -> @iter_sepcon_Znth with (d := Inhabitant_Z)
+                                          (i := i1 mod size)(l := upto (Z.to_nat size))
             by (rewrite -> Zlength_upto, Z2Nat.id; lia).
         rewrite -> Znth_upto by (rewrite Z2Nat.id; lia).
         unfold hashtable_entry.
@@ -726,7 +732,8 @@ Proof.
       iMod ("AS1" with "P") as (HT) "[hashtable Hclose]".
       iDestruct "hashtable" as (T) "((% & excl) & entries)".
       match goal with H : _ /\ _ /\ _ |- _ => destruct H as (? & ? & ?) end.
-      rewrite -> iter_sepcon_Znth with (i0 := i1 mod size)(f := hashtable_entry _ _ _)
+      rewrite -> @iter_sepcon_Znth with (d := Inhabitant_Z)
+                                        (i := i1 mod size)(f := hashtable_entry _ _ _)
         by (rewrite -> Zlength_upto, Z2Nat.id; lia).
       rewrite -> Znth_upto by (rewrite -> Z2Nat.id; lia).
       unfold hashtable_entry at 1.
@@ -753,7 +760,8 @@ Proof.
           rewrite Hindex; congruence. }
         unfold hashtable; iExists T.
         iSplitL ""; [auto|].
-        rewrite -> iter_sepcon_Znth with (i0 := i1 mod size)(l := upto (Z.to_nat size))
+        rewrite -> @iter_sepcon_Znth with (d := Inhabitant_Z)
+                                          (i := i1 mod size)(l := upto (Z.to_nat size))
           by (rewrite -> Zlength_upto, Z2Nat.id; lia).
         rewrite -> Znth_upto by (rewrite Z2Nat.id; lia).
         unfold hashtable_entry.
@@ -762,7 +770,8 @@ Proof.
         iFrame "snap snaps".
         iDestruct "Hclose" as "[Hclose _]"; iApply "Hclose".
         unfold hashtable; iExists T.
-        rewrite -> iter_sepcon_Znth with (i0 := i1 mod size)(l := upto (Z.to_nat size))
+        rewrite -> @iter_sepcon_Znth with (d := Inhabitant_Z)
+                                          (i := i1 mod size)(l := upto (Z.to_nat size))
           by (rewrite -> Zlength_upto, Z2Nat.id; lia).
         rewrite -> Znth_upto by (rewrite Z2Nat.id; lia).
         unfold hashtable_entry.
@@ -778,7 +787,8 @@ Proof.
         iMod ("AS1" with "P") as (HT) "[hashtable Hclose]".
         iDestruct "hashtable" as (T) "((% & excl) & entries)".
         match goal with H : _ /\ _ /\ _ |- _ => destruct H as (? & ? & ?) end.
-        rewrite -> iter_sepcon_Znth with (i0 := i1 mod size)(f := hashtable_entry _ _ _)
+        rewrite -> @iter_sepcon_Znth with (d := Inhabitant_Z)
+                                          (i := i1 mod size)(f := hashtable_entry _ _ _)
           by (rewrite -> Zlength_upto, Z2Nat.id; lia).
         rewrite -> Znth_upto by (rewrite -> Z2Nat.id; lia).
         unfold hashtable_entry at 1.
@@ -812,7 +822,8 @@ Proof.
             rewrite HHi; auto. }
         unfold hashtable; iExists T.
         iSplitL ""; [iSplit; auto; iPureIntro; split; auto; tauto|].
-       rewrite -> iter_sepcon_Znth with (i0 := i1 mod size)(l := upto (Z.to_nat size))
+        rewrite -> @iter_sepcon_Znth with (d := Inhabitant_Z)
+                                          (i := i1 mod size)(l := upto (Z.to_nat size))
           by (rewrite -> Zlength_upto, Z2Nat.id; lia).
         rewrite -> Znth_upto by (rewrite Z2Nat.id; lia).
         unfold hashtable_entry.
@@ -919,7 +930,7 @@ Proof.
       iIntros "([AS1 _] & P)".
       iMod ("AS1" with "P") as (HT) "[hashtable Hclose]".
       iDestruct "hashtable" as (T) "((% & excl) & entries)".
-      rewrite -> iter_sepcon_Znth' with (i0 := i1 mod size)
+      rewrite -> @iter_sepcon_Znth' with (d := Inhabitant_Z) (i := i1 mod size)
           by (rewrite -> ?Zlength_map, Zlength_upto, Z2Nat.id; lia).
       erewrite Znth_upto by (rewrite -> ?Zlength_upto, Z2Nat.id; lia).
       unfold hashtable_entry at 1.
@@ -983,7 +994,8 @@ Proof.
         iMod ("AS1" with "P") as (HT) "[hashtable Hclose]".
         iDestruct "hashtable" as (T) "((% & excl) & entries)".
         match goal with H : _ /\ _ /\ _ |- _ => destruct H as (? & ? & ?) end.
-        rewrite -> iter_sepcon_Znth with (i0 := i1 mod size)(f := hashtable_entry _ _ _)
+        rewrite -> @iter_sepcon_Znth with (d := Inhabitant_Z)
+                                          (i := i1 mod size)(f := hashtable_entry _ _ _)
             by (rewrite -> ?Zlength_map, Zlength_upto, Z2Nat.id; try lia).
         erewrite Znth_upto by (rewrite -> ?Zlength_upto, Z2Nat.id; lia).
         unfold hashtable_entry at 1.
@@ -1008,7 +1020,8 @@ Proof.
         iFrame "snap snaps".
         iDestruct "Hclose" as "[Hclose _]"; iApply "Hclose".
         unfold hashtable; iExists (upd_Znth (i1 mod size) T (if eq_dec ki 0 then k else ki, vi)); iFrame "excl".
-        rewrite -> iter_sepcon_Znth with (i0 := i1 mod size)(l := upto (Z.to_nat size))
+        rewrite -> @iter_sepcon_Znth with (d := Inhabitant_Z) (i := i1 mod size)
+                                          (l := upto (Z.to_nat size))
           by (rewrite -> Zlength_upto, Z2Nat.id; lia).
         rewrite -> Znth_upto by (rewrite Z2Nat.id; lia).
         unfold hashtable_entry.
@@ -1042,7 +1055,7 @@ Proof.
           iIntros "(([AS1 _] & snap) & P)".
           iMod ("AS1" with "P") as (HT) "[hashtable Hclose]".
           iDestruct "hashtable" as (T) "((% & excl) & entries)".
-          rewrite -> iter_sepcon_Znth' with (i0 := i1 mod size)
+          rewrite -> @iter_sepcon_Znth' with (d := Inhabitant_Z) (i := i1 mod size)
             by (rewrite -> ?Zlength_map, Zlength_upto, Z2Nat.id; lia).
           erewrite Znth_upto by (rewrite -> ?Zlength_upto, Z2Nat.id; lia).
           unfold hashtable_entry at 1.
@@ -1099,7 +1112,8 @@ Proof.
         iMod ("AS1" with "P") as (HT) "[hashtable Hclose]".
         iDestruct "hashtable" as (T) "((% & excl) & entries)".
         match goal with H : _ /\ _ /\ _ |- _ => destruct H as (? & ? & ?) end.
-        rewrite -> iter_sepcon_Znth with (i0 := i1 mod size)(f := hashtable_entry _ _ _)
+        rewrite -> @iter_sepcon_Znth with (d := Inhabitant_Z) (i := i1 mod size)
+                                          (f := hashtable_entry _ _ _)
           by (rewrite -> Zlength_upto, Z2Nat.id; lia).
         rewrite -> Znth_upto by (rewrite -> Z2Nat.id; lia).
         unfold hashtable_entry at 1.
@@ -1124,7 +1138,8 @@ Proof.
         unfold hashtable.
         rewrite exp_andp2.
         iExists ((if eq_dec vi 0 then upd_Znth (i1 mod size) T (k, v) else T)).
-        rewrite -> iter_sepcon_Znth with (i0 := i1 mod size)(l := upto (Z.to_nat size))
+        rewrite -> @iter_sepcon_Znth with (d := Inhabitant_Z) (i := i1 mod size)
+                                          (l := upto (Z.to_nat size))
             by (rewrite -> Zlength_upto, Z2Nat.id; lia).
         rewrite -> Znth_upto by (rewrite Z2Nat.id; lia).
         unfold hashtable_entry.
@@ -1857,7 +1872,7 @@ Proof.
           destruct (eq_dec j i).
           + subst; rewrite -> upd_Znth_same by auto; apply derives_refl.
           + rewrite -> upd_Znth_diff by auto.
-            setoid_rewrite Znth_repeat with (n0 := 3%nat); apply stronger_default_val. }
+            setoid_rewrite @Znth_repeat with (n := 3%nat); apply stronger_default_val. }
       rewrite <- !sepcon_assoc, (sepcon_comm _ (data_at (Znth i shs) _ _ (gv _results))),
         !sepcon_assoc; apply sepcon_derives.
       { apply stronger_array_ext.
@@ -1866,7 +1881,7 @@ Proof.
           destruct (eq_dec j i).
           + subst; rewrite -> upd_Znth_same by auto; apply derives_refl.
           + rewrite -> upd_Znth_diff' by auto.
-            setoid_rewrite Znth_repeat with (n0 := 3%nat); apply stronger_default_val. }
+            setoid_rewrite @Znth_repeat with (n := 3%nat); apply stronger_default_val. }
       erewrite sublist_next by (auto; lia); simpl; fast_cancel.
       { intro; subst; contradiction unreadable_bot.
         eapply join_readable1, readable_share_list_join; eauto. } }

diff --git a/concurrency/invariants.v b/concurrency/invariants.v
@@ -215,7 +215,7 @@ Proof.
   destruct b.
   erewrite ghost_list_nth with (n := i) by (erewrite nth_map' with (d' := None), Hi'; eauto; lia).
   iDestruct "dis" as "[token dis]".
-  rewrite -> iter_sepcon_eq, iter_sepcon_Znth with (i0 := Z.of_nat i)
+  rewrite -> @iter_sepcon_eq, iter_sepcon_Znth with (i := Z.of_nat i)
     by (rewrite Zlength_upto; split; [|apply Nat2Z.inj_lt]; lia).
   erewrite Znth_upto, Hi by lia.
   iDestruct "I" as "((agree' & HP) & I)".
@@ -244,7 +244,7 @@ Proof.
     + destruct (eq_dec x i); [subst; right; constructor | left].
       unfold Ensembles.In in *.
       rewrite nth_replace_nth' in X; auto.
-  - erewrite iter_sepcon_Znth with (i0 := Z.of_nat i)(l0 := upto _)
+  - erewrite @iter_sepcon_Znth with (i := Z.of_nat i)(l := upto _)
       by (rewrite Zlength_upto; split; [|apply Nat2Z.inj_lt]; lia).
     erewrite Znth_upto, Znth_replace_nth by lia; iFrame.
     erewrite iter_sepcon_func_strong; auto.
@@ -322,9 +322,9 @@ Proof.
       * intro X'; inv X'.
         unfold Ensembles.In in X.
         rewrite -> nth_replace_nth in X by lia; inv X.
-  - erewrite !iter_sepcon_eq, iter_sepcon_Znth with (i0 := Z.of_nat i)
+  - erewrite !iter_sepcon_eq, @iter_sepcon_Znth with (i := Z.of_nat i)
       by (rewrite Zlength_upto; split; [|apply Nat2Z.inj_lt]; lia).
-    erewrite iter_sepcon_Znth with (i0 := Z.of_nat i)(l0 := upto _)
+    erewrite @iter_sepcon_Znth with (i := Z.of_nat i)(l := upto _)
       by (rewrite Zlength_upto; split; [|apply Nat2Z.inj_lt]; lia).
     erewrite !Znth_upto, !Znth_replace_nth by lia.
     rewrite Hi.