From 6867432f8a9ee2e4490ea2440e56daae85d0286c Mon Sep 17 00:00:00 2001
From: Dan Frumin <dfrumin@cs.ru.nl>
Date: Fri, 15 Mar 2019 11:56:47 +0100
Subject: [PATCH] Update to the new Iris withpout locked lambdas

See https://gitlab.mpi-sws.org/iris/iris/merge_requests/223
---
 opam                               | 14 +++++++++++
 theories/examples/bit.v            |  2 +-
 theories/examples/generative.v     |  3 +--
 theories/examples/symbol.v         | 21 +++++++----------
 theories/examples/ticket_lock.v    | 38 ++++++++++--------------------
 theories/lib/Y.v                   | 12 +++++-----
 theories/lib/counter.v             |  2 +-
 theories/logic/proofmode/tactics.v |  4 ++--
 8 files changed, 45 insertions(+), 51 deletions(-)
 create mode 100644 opam

diff --git a/opam b/opam
new file mode 100644
index 0000000..7a115b0
--- /dev/null
+++ b/opam
@@ -0,0 +1,14 @@
+opam-version: "1.2"
+name: "coq-reloc"
+maintainer: "Ralf Jung <jung@mpi-sws.org>"
+authors: "Dan Frumin, Robbert Krebbers"
+homepage: "http://iris-project.org/"
+bug-reports: "https://gitlab.mpi-sws.org/dfrumin/reloc/issues"
+dev-repo: "https://gitlab.mpi-sws.org/dfrumin/reloc.git"
+build: [make "-j%{jobs}%"]
+install: [make "install"]
+remove: ["rm" "-rf" "%{lib}%/coq/user-contrib/reloc"]
+depends: [
+  "coq-iris" { (= "dev.2019-03-15.0.33ee70bf") | (= "dev") }
+  "coq-autosubst" { = "dev.coq86" }
+]
diff --git a/theories/examples/bit.v b/theories/examples/bit.v
index 36bc970..0ca7c8b 100644
--- a/theories/examples/bit.v
+++ b/theories/examples/bit.v
@@ -40,7 +40,7 @@ Section bit_refinement.
     iApply (refines_exists bitτi).
     progress repeat iApply refines_pair.
     - rel_values.
-    - unfold flip_nat. rel_pure_l. unlock. (* TODO: can we make the tactics do unlocking? *)
+    - unfold flip_nat. rel_pure_l.
       iApply refines_arrow_val.
       iIntros "!#" (v1 v2) "/=".
       iIntros ([b [? ?]]); simplify_eq/=.
diff --git a/theories/examples/generative.v b/theories/examples/generative.v
index fd43f80..534acdf 100644
--- a/theories/examples/generative.v
+++ b/theories/examples/generative.v
@@ -40,7 +40,7 @@ Section namegen_refinement.
   Lemma nameGen_ref1 :
     REL nameGen1 << nameGen2 : ∃ α, (() → α) * (α → α → lrel_bool).
   Proof.
-    unlock nameGen1 nameGen2.
+    unfold nameGen1, nameGen2.
     rel_alloc_r c as "Hc".
     iMod alloc_empty_bij as (γ) "HB".
     pose (N:=relocN.@"ng").
@@ -173,7 +173,6 @@ Section cell_refinement.
   Lemma cell2_cell1_refinement :
     REL cell2 << cell1 : ∀ α, ∃ β, (α → β) * (β → α) * (β → α → ()).
   Proof.
-    unlock cell2 cell1.
     (* TODO: this uuugly *)
     pose (Ï„ := (TExists (TProd (TProd (TArrow (TVar 1) (TVar 0))
                                  (TArrow (TVar 0) (TVar 1)))
diff --git a/theories/examples/symbol.v b/theories/examples/symbol.v
index 9957ce7..cec9e57 100644
--- a/theories/examples/symbol.v
+++ b/theories/examples/symbol.v
@@ -119,7 +119,7 @@ Section proof.
   Lemma eqKey_refinement γ :
     REL eqKey << eqKey : tableR γ → tableR γ → lrel_bool.
   Proof.
-    unlock eqKey.
+    unfold eqKey.
     iApply refines_arrow_val.
     iAlways. iIntros (k1 k2) "/= #Hk".
     iDestruct "Hk" as (n) "(% & % & #Hn)"; simplify_eq.
@@ -142,7 +142,7 @@ Section proof.
       (tableR γ → lrel_int).
   Proof.
     iIntros "#Hinv".
-    unlock. iApply refines_arrow_val.
+    iApply refines_arrow_val.
     iAlways. iIntros (k1 k2) "/= #Hk".
     iDestruct "Hk" as (n) "(% & % & #Hn)"; simplify_eq.
     rel_let_l. rel_let_r.
@@ -181,7 +181,6 @@ Section proof.
       (λ: "n", (nth ! #tbl2) (! #size2 - "n"))%V : (tableR γ → lrel_int).
   Proof.
     iIntros "#Hinv".
-    unlock.
     iApply refines_arrow_val.
     iAlways. iIntros (k1 k2) "#Hk /=".
     iDestruct "Hk" as (n) "(% & % & #Hn)"; simplify_eq.
@@ -219,10 +218,9 @@ Section proof.
   Lemma refinement1 :
     REL symbol1 << symbol2 : () → lrel_symbol.
   Proof.
-    unlock symbol1 symbol2.
-    iApply refines_arrow_val.
+    iApply refines_arrow_val; [done|done|].
     iAlways. iIntros (? ?) "[% %]"; simplify_eq/=.
-    rel_let_l. rel_let_r.
+    rel_rec_l. rel_rec_r.
     rel_alloc_l size1 as "[Hs1 Hs1']"; repeat rel_pure_l.
     rel_alloc_r size2 as "[Hs2 Hs2']"; repeat rel_pure_r.
     rel_alloc_l tbl1 as "[Htbl1 Htbl1']"; repeat rel_pure_l.
@@ -292,17 +290,15 @@ Section proof.
       iExists m'. eauto.
     (* Lookup *)
     - rel_pure_l. rel_pure_r.
-      iPoseProof (lookup_refinement1 with "Hinv") as "H".
-      unlock. iApply "H". (* TODO how to avoid this? *)
+      iApply (lookup_refinement1 with "Hinv").
   Qed.
 
   Lemma refinement2 :
     REL symbol2 << symbol1 : () → lrel_symbol.
   Proof.
-    unlock symbol1 symbol2.
-    iApply refines_arrow_val.
+    iApply refines_arrow_val; [done|done|].
     iAlways. iIntros (? ?) "[% %]"; simplify_eq/=.
-    rel_let_l. rel_let_r.
+    rel_rec_l. rel_rec_r.
     rel_alloc_l size1 as "[Hs1 Hs1']"; repeat rel_pure_l.
     rel_alloc_r size2 as "[Hs2 Hs2']"; repeat rel_pure_r.
     rel_alloc_l tbl1 as "[Htbl1 Htbl1']"; repeat rel_pure_l.
@@ -372,8 +368,7 @@ Section proof.
       iExists m'. eauto.
     (* Lookup *)
     - rel_pure_l. rel_pure_r.
-      iPoseProof (lookup_refinement2 with "Hinv") as "H".
-      unlock. iApply "H". (* TODO how to avoid this? *)
+      iApply (lookup_refinement2 with "Hinv").
   Qed.
 End proof.
 
diff --git a/theories/examples/ticket_lock.v b/theories/examples/ticket_lock.v
index 27b5073..55d0743 100644
--- a/theories/examples/ticket_lock.v
+++ b/theories/examples/ticket_lock.v
@@ -105,16 +105,13 @@ Section refinement.
   Lemma newlock_refinement :
     REL newlock << reloc.lib.lock.newlock : () → lockInt.
   Proof.
-    unlock newlock.
-    iApply refines_arrow_val.
-    { by unlock reloc.lib.lock.newlock. }
+    iApply refines_arrow_val; [done|done|].
     iAlways. iIntros (? ?) "/= [% %]"; simplify_eq.
     (* Reducing to a value on the LHS *)
-    repeat rel_pure_l.
+    rel_rec_l.
     rel_alloc_l ln as "Hln".
     rel_alloc_l lo as "Hlo".
     (* Reducing to a value on the RHS *)
-    repeat rel_pure_r.
     rel_apply_r refines_newlock_r.
     iIntros (l') "Hl'".
     (* Establishing the invariant *)
@@ -136,7 +133,6 @@ Section refinement.
     iIntros "#Hinv Hticket".
     rel_rec_l.
     iLöb as "IH".
-    unlock {2}wait_loop.
     repeat rel_pure_l.
     rel_load_l_atomic.
     openI.
@@ -151,7 +147,7 @@ Section refinement.
       closeI. rel_values.
     - iMod ("Hcl" with "[-Hticket]") as "_".
       { iNext. iExists _,_,_; by iFrame. }
-      rel_pure_l. unlock wait_loop. by iApply "IH".
+      rel_rec_l. by iApply "IH".
   Qed.
 
   (** Logically atomic spec for `acquire`.
@@ -169,7 +165,7 @@ Section refinement.
     -∗ (REL fill K (acquire (#lo, #ln)%V) << t : A).
   Proof.
     iIntros "HP #H".
-    rewrite /acquire. unlock. simpl.
+    rewrite /acquire.
     repeat rel_pure_l.
     rel_apply_l (FG_increment_atomic_l (fun n : nat => ∃ o : nat, lo ↦ #o ∗ issuedTickets γ n ∗ R o)%I P%I with "HP").
     iAlways.
@@ -195,8 +191,7 @@ Section refinement.
       clear o o'.
       repeat rel_pure_l.
       iLöb as "IH".
-      unlock wait_loop. simpl.
-      repeat rel_pure_l.
+      rel_rec_l. repeat rel_pure_l.
       rel_load_l_atomic.
       iMod "H2" as (o n') "(Hlo & Hln & Hissued & HR & Hrest)". iModIntro.
       iExists _. iFrame. iNext. iIntros "Hlo".
@@ -215,9 +210,7 @@ Section refinement.
   Lemma acquire_refinement :
     REL acquire << reloc.lib.lock.acquire : lockInt → ().
   Proof.
-    iApply refines_arrow_val;
-      [ by unlock acquire
-      | by unlock reloc.lib.lock.acquire |].
+    iApply refines_arrow_val; [done|done|].
     iAlways. iIntros (? ?) "/= #Hl".
     iDestruct "Hl" as (lo ln γ l') "(% & % & Hin)". simplify_eq/=.
     rel_apply_l (acquire_l_logatomic
@@ -250,12 +243,10 @@ Section refinement.
   Lemma acquire_refinement_direct :
     REL acquire << reloc.lib.lock.acquire : lockInt → ().
   Proof.
-    unlock acquire; simpl.
-    iApply refines_arrow_val.
-    { by unlock reloc.lib.lock.acquire. }
+    iApply refines_arrow_val; [done|done|].
     iAlways. iIntros (? ?) "/= #Hl".
     iDestruct "Hl" as (lo ln γ l') "(% & % & Hin)". simplify_eq.
-    rel_let_l. repeat rel_proj_l.
+    rel_rec_l. repeat rel_proj_l.
     rel_apply_l (FG_increment_atomic_l (issuedTickets γ)%I True%I); first done.
     iAlways.
     openI.
@@ -280,8 +271,7 @@ Section refinement.
     (x ↦ #(n+1) -∗ REL fill K (of_val #()) << t : A) -∗
     (REL fill K (wkincr #x) << t : A).
   Proof.
-    iIntros "Hx Hlog".
-    unlock wkincr. rel_rec_l.
+    iIntros "Hx Hlog". rel_rec_l.
     rel_load_l. rel_op_l. rel_store_l.
     by iApply "Hlog".
   Qed.
@@ -301,7 +291,6 @@ Section refinement.
     -∗ (REL fill K (wkincr #x) << t : A).
   Proof.
     iIntros "HR2 #H".
-    unlock wkincr.
     rel_rec_l.
     iPoseProof "H" as "H2".
     rel_load_l_atomic.
@@ -320,12 +309,10 @@ Section refinement.
   Lemma release_refinement :
     REL release << reloc.lib.lock.release : lockInt → ().
   Proof.
-    unlock release.
-    iApply refines_arrow_val; eauto.
-    { by unlock reloc.lib.lock.release. }
+    iApply refines_arrow_val; [done|done|].
     iAlways. iIntros (? ?) "/= #Hl".
     iDestruct "Hl" as (lo ln γ l') "(% & % & Hin)". simplify_eq.
-    rel_let_l. rel_proj_l.
+    rel_rec_l. rel_proj_l.
     pose (R := fun (o : nat) =>
                  (∃ (n : nat) (b : bool), ln ↦ #n
                  ∗ issuedTickets γ n ∗ l' ↦ₛ #b
@@ -359,8 +346,7 @@ Section refinement.
         (reloc.lib.lock.newlock, reloc.lib.lock.acquire, reloc.lib.lock.release)
     : interp lockT Δ.
   Proof.
-    simpl.
-    iApply (refines_exists lockInt).
+    simpl. iApply (refines_exists lockInt).
     repeat iApply refines_pair.
     - by iApply newlock_refinement.
     - by iApply acquire_refinement_direct.
diff --git a/theories/lib/Y.v b/theories/lib/Y.v
index e00da89..44debb6 100644
--- a/theories/lib/Y.v
+++ b/theories/lib/Y.v
@@ -32,7 +32,7 @@ Section contents.
   Lemma Y_semtype A :
     REL Y << Y : (A → A) → A.
   Proof.
-    unlock Y.
+    unfold Y.
     iApply refines_arrow.
     iAlways. iIntros (f1 f2) "#Hff".
     rel_let_l. rel_let_r.
@@ -47,7 +47,7 @@ Section contents.
   Lemma FIX_semtype A :
     REL F << F : (A → A) → A.
   Proof.
-    unlock F.
+    unfold F.
     iApply refines_arrow.
     iAlways. iIntros (f1 f2) "#Hff".
     iLöb as "IH".
@@ -60,7 +60,7 @@ Section contents.
   Lemma KNOT_Y A :
     REL Knot << Y : (A → A) → A.
   Proof.
-    unlock Y Knot.
+    unfold Y, Knot.
     iApply refines_arrow.
     iAlways. iIntros (f1 f2) "#Hff".
     rel_let_l. rel_let_r.
@@ -77,7 +77,7 @@ Section contents.
   Lemma Y_KNOT A :
     REL Y << Knot : (A → A) → A.
   Proof.
-    unlock Y Knot.
+    unfold Y, Knot.
     iApply refines_arrow.
     iAlways. iIntros (f1 f2) "#Hff".
     rel_let_l. rel_let_r.
@@ -95,7 +95,7 @@ Section contents.
   Lemma FIX_Y A :
     REL F << Y : (A → A) → A.
   Proof.
-    unlock Y F.
+    unfold Y, F.
     iApply refines_arrow.
     iAlways. iIntros (f1 f2) "#Hff".
     rel_pure_r. rel_pure_r. rel_pure_r.
@@ -108,7 +108,7 @@ Section contents.
   Lemma Y_FIX A :
     REL Y << F : (A → A) → A.
   Proof.
-    unlock Y F.
+    unfold Y, F.
     iApply refines_arrow.
     iAlways. iIntros (f1 f2) "#Hff".
     rel_pure_l. rel_pure_l. rel_pure_l.
diff --git a/theories/lib/counter.v b/theories/lib/counter.v
index 0ab62f0..8864560 100644
--- a/theories/lib/counter.v
+++ b/theories/lib/counter.v
@@ -194,7 +194,7 @@ Section CG_Counter.
   Lemma FG_CG_counter_refinement :
     REL FG_counter << CG_counter : () → (() → lrel_int) * (() → lrel_int).
   Proof.
-    unfold FG_counter, CG_counter. unlock.
+    unfold FG_counter, CG_counter.
     iApply refines_arrow_val.
     iAlways. iIntros (? ?) "_"; simplify_eq/=.
     rel_rec_l. rel_rec_r.
diff --git a/theories/logic/proofmode/tactics.v b/theories/logic/proofmode/tactics.v
index cf72879..3495eab 100644
--- a/theories/logic/proofmode/tactics.v
+++ b/theories/logic/proofmode/tactics.v
@@ -562,12 +562,12 @@ Tactic Notation "rel_fork_r" ident(i) "as" constr(H) :=
  *)
 Tactic Notation "rel_rec_l" :=
   let H := fresh in
-  assert (H := AsRecV_recv_locked);
+  assert (H := AsRecV_recv);
   rel_pure_l (App _ _);
   clear H.
 Tactic Notation "rel_rec_r" :=
   let H := fresh in
-  assert (H := AsRecV_recv_locked);
+  assert (H := AsRecV_recv);
   rel_pure_r (App _ _);
   clear H.
 
-- 
GitLab