From f1a8bd8dbe7593e5db95d4ccfc15c95117a8f59a Mon Sep 17 00:00:00 2001
From: Dan Frumin <dfrumin@cs.ru.nl>
Date: Thu, 1 Feb 2018 00:22:56 +0100
Subject: [PATCH] Cleaner proof of the stack refinement

---
 theories/examples/stack/module_refinement.v |  2 +-
 theories/examples/stack/refinement.v        | 11 ++++-------
 theories/examples/stack/stack_rules.v       | 10 +++++-----
 3 files changed, 10 insertions(+), 13 deletions(-)

diff --git a/theories/examples/stack/module_refinement.v b/theories/examples/stack/module_refinement.v
index b86454b..ad52bc4 100644
--- a/theories/examples/stack/module_refinement.v
+++ b/theories/examples/stack/module_refinement.v
@@ -46,7 +46,7 @@ Section Mod_refinement.
       { rewrite /prestack_owns big_sepM_empty fmap_empty.
         iFrame "Hemp". }
       iMod (stack_owns_alloc with "[$Hoe $Histk]") as "[Hoe #Histk]".
-      iAssert (preStackLink γ (R τi) (#istk, FoldV (InjLV #()))) with "[Histk]" as "#HLK".
+      iAssert (preStackLink γ τi (#istk, FoldV (InjLV #()))) with "[Histk]" as "#HLK".
       { rewrite preStackLink_unfold.
         iExists _, _. iSplitR; simpl; trivial.
         iFrame "Histk". iLeft. iSplit; trivial. }
diff --git a/theories/examples/stack/refinement.v b/theories/examples/stack/refinement.v
index e0d57d7..4b5689a 100644
--- a/theories/examples/stack/refinement.v
+++ b/theories/examples/stack/refinement.v
@@ -11,14 +11,11 @@ Section Stack_refinement.
   Implicit Types Δ : listC D.
   Import lang.
 
-  Program Definition R (τi : prodC valC valC -> iProp Σ) := λne ww, (□ τi ww)%I.
-  Next Obligation. solve_proper. Qed.
-
   Definition sinv' {SPG : authG Σ stackUR} γ τi stk stk' l' : iProp Σ :=
     (∃ (istk : loc) v h, (prestack_owns γ h)
         ∗ stk' ↦ₛ v
         ∗ stk ↦ᵢ (FoldV #istk)
-        ∗ preStackLink γ (R τi) (#istk, v)
+        ∗ preStackLink γ τi (#istk, v)
         ∗ l' ↦ₛ #false)%I.
 
   Context `{stackG Σ}.
@@ -26,7 +23,7 @@ Section Stack_refinement.
     (∃ (istk : loc) v h, (stack_owns h)
         ∗ stk' ↦ₛ v
         ∗ stk ↦ᵢ (FoldV #istk)
-        ∗ StackLink (R τi) (#istk, v)
+        ∗ StackLink τi (#istk, v)
         ∗ l ↦ₛ #false)%I.
   Lemma sinv_unfold τi stk stk' l :
     sinv τi stk stk' l = sinv' stack_name τi stk stk' l.
@@ -38,7 +35,7 @@ Section Stack_refinement.
 
   Lemma FG_CG_push_refinement N st st' (τi : D) (v v' : val) l Γ :
     N ## logrelN →
-    inv N (sinv τi st st' l) -∗ (R τi) (v,v') -∗
+    inv N (sinv τi st st' l) -∗ □ τi (v,v') -∗
     Γ ⊨ (FG_push $/ (LitV (Loc st))) v ≤log≤ (CG_locked_push $/ (LitV (Loc st')) $/ (LitV (Loc l))) v' : TUnit.
   Proof.
     iIntros (?) "#Hinv #Hvv'". iIntros (Δ).
@@ -344,7 +341,7 @@ Section Full_refinement.
     { rewrite /stack_owns /prestack_owns big_sepM_empty fmap_empty.
       iFrame "Hemp". }
     iMod (stack_owns_alloc with "[$Hoe $Histk]") as "[Hoe #Histk]".
-    iAssert (StackLink (R τi) (#istk, FoldV (InjLV Unit))) with "[Histk]" as "#HLK".
+    iAssert (StackLink τi (#istk, FoldV (InjLV Unit))) with "[Histk]" as "#HLK".
     { rewrite StackLink_unfold.
       iExists _, _. iSplitR; simpl; trivial.
       iFrame "Histk". iLeft. iSplit; trivial. }
diff --git a/theories/examples/stack/stack_rules.v b/theories/examples/stack/stack_rules.v
index bbe3b52..10eb517 100644
--- a/theories/examples/stack/stack_rules.v
+++ b/theories/examples/stack/stack_rules.v
@@ -55,7 +55,7 @@ Section Rules_pre.
     (∃ (l : loc) w, ⌜v.1 = # l⌝ ∗ l ↦ˢᵗᵏ w ∗
             ((⌜w = InjLV #()⌝ ∧ ⌜v.2 = FoldV (InjLV #())⌝) ∨
             (∃ y1 z1 y2 z2, ⌜w = InjRV (PairV y1 (FoldV z1))⌝ ∗
-              ⌜v.2 = FoldV (InjRV (PairV y2 z2))⌝ ∗ Q (y1, y2) ∗ ▷ P(z1, z2))))%I.
+              ⌜v.2 = FoldV (InjRV (PairV y2 z2))⌝ ∗ □ Q (y1, y2) ∗ ▷ P(z1, z2))))%I.
   Solve Obligations with solve_proper.
 
   Global Instance StackLink_pre_contractive Q : Contractive (preStackLink_pre Q).
@@ -69,12 +69,12 @@ Section Rules_pre.
       ((⌜w = InjLV #()⌝ ∧ ⌜v.2 = FoldV (InjLV #())⌝) ∨
       (∃ y1 z1 y2 z2, ⌜w = InjRV (PairV y1 (FoldV z1))⌝
                       ∗ ⌜v.2 = FoldV (InjRV (PairV y2 z2))⌝
-                      ∗ Q (y1, y2) ∗ ▷ preStackLink Q (z1, z2))))%I.
+                      ∗ □ Q (y1, y2) ∗ ▷ preStackLink Q (z1, z2))))%I.
   Proof. by rewrite {1}/preStackLink fixpoint_unfold. Qed.
 
   Global Opaque preStackLink. (* So that we can only use the unfold above. *)
 
-  Global Instance preStackLink_persistent (Q : D) v `{∀ vw, Persistent (Q vw)} :
+  Global Instance preStackLink_persistent (Q : D) v :
     Persistent (preStackLink Q v).
   Proof.
     rewrite /Persistent.
@@ -166,10 +166,10 @@ Section Rules.
       ((⌜w = InjLV #()⌝ ∧ ⌜v.2 = FoldV (InjLV #())⌝) ∨
       (∃ y1 z1 y2 z2, ⌜w = InjRV (PairV y1 (FoldV z1))⌝
                       ∗ ⌜v.2 = FoldV (InjRV (PairV y2 z2))⌝
-                      ∗ Q (y1, y2) ∗ ▷ StackLink Q (z1, z2))))%I.
+                      ∗ □ Q (y1, y2) ∗ ▷ StackLink Q (z1, z2))))%I.
   Proof. by rewrite /StackLink preStackLink_unfold. Qed.
 
-  Global Instance StackLink_persistent (Q : D) v `{∀ vw, Persistent (Q vw)} :
+  Global Instance StackLink_persistent (Q : D) v :
     Persistent (StackLink Q v).
   Proof. apply _. Qed.
   Global Opaque StackLink.
-- 
2.22.0