From be74f7c13cd78014501ae3b4211efeb97c185ade Mon Sep 17 00:00:00 2001
From: Dan Frumin <dfrumin@cs.ru.nl>
Date: Fri, 13 Dec 2019 15:53:49 +0100
Subject: [PATCH] simplify refines_arrow_val

---
 theories/examples/coinflip.v    |  4 ++--
 theories/examples/symbol.v      |  4 ++--
 theories/examples/ticket_lock.v | 16 ++++++++--------
 theories/logic/derived.v        |  6 ++----
 theories/logic/rules.v          |  6 ++----
 5 files changed, 16 insertions(+), 20 deletions(-)

diff --git a/theories/examples/coinflip.v b/theories/examples/coinflip.v
index 6f9f11e..af934a7 100644
--- a/theories/examples/coinflip.v
+++ b/theories/examples/coinflip.v
@@ -19,8 +19,8 @@ Definition flip_lazy' : val := λ: "c" "lk" "p" <>,
 
 Definition read_lazy : val := rec: "read" "c" <> :=
   match: !"c" with
-    InjR "v" => "v"
-  | InjL <>  =>
+    SOME "v" => "v"
+  | NONE  =>
       let: "x" := rand #() in
       if: CAS "c" NONEV (SOME "x")
       then "x"
diff --git a/theories/examples/symbol.v b/theories/examples/symbol.v
index e3d70b1..d96628a 100644
--- a/theories/examples/symbol.v
+++ b/theories/examples/symbol.v
@@ -218,7 +218,7 @@ Section proof.
   Lemma refinement1 :
     REL symbol1 << symbol2 : () → lrel_symbol.
   Proof.
-    iApply refines_arrow_val; [done|done|].
+    iApply refines_arrow_val.
     iAlways. iIntros (? ?) "[% %]"; simplify_eq/=.
     rel_rec_l. rel_rec_r.
     rel_alloc_l size1 as "[Hs1 Hs1']"; repeat rel_pure_l.
@@ -297,7 +297,7 @@ Section proof.
   Lemma refinement2 :
     REL symbol2 << symbol1 : () → lrel_symbol.
   Proof.
-    iApply refines_arrow_val; [done|done|].
+    iApply refines_arrow_val.
     iAlways. iIntros (? ?) "[% %]"; simplify_eq/=.
     rel_rec_l. rel_rec_r.
     rel_alloc_l size1 as "[Hs1 Hs1']"; repeat rel_pure_l.
diff --git a/theories/examples/ticket_lock.v b/theories/examples/ticket_lock.v
index c4491dc..9155750 100644
--- a/theories/examples/ticket_lock.v
+++ b/theories/examples/ticket_lock.v
@@ -104,8 +104,8 @@ Section refinement.
   Lemma newlock_refinement :
     REL newlock << reloc.lib.lock.newlock : () → lockInt.
   Proof.
-    iApply refines_arrow_val; [done|done|].
-    iAlways. iIntros (? ?) "/= [% %]"; simplify_eq.
+    rel_arrow_val.
+    iIntros (? ?) "/= [% %]"; simplify_eq.
     (* Reducing to a value on the LHS *)
     rel_rec_l.
     rel_alloc_l ln as "Hln".
@@ -209,8 +209,8 @@ Section refinement.
   Lemma acquire_refinement :
     REL acquire << reloc.lib.lock.acquire : lockInt → ().
   Proof.
-    iApply refines_arrow_val; [done|done|].
-    iAlways. iIntros (? lk) "/= #Hl".
+    rel_arrow_val.
+    iIntros (? lk) "/= #Hl".
     iDestruct "Hl" as (lo ln γ) "(% & Hin)". simplify_eq/=.
     rel_apply_l (acquire_l_logatomic
                    (fun o => ∃ st, is_locked_r lk st ∗
@@ -241,8 +241,8 @@ Section refinement.
   Lemma acquire_refinement_direct :
     REL acquire << reloc.lib.lock.acquire : lockInt → ().
   Proof.
-    iApply refines_arrow_val; [done|done|].
-    iAlways. iIntros (? ?) "/= #Hl".
+    rel_arrow_val.
+    iIntros (? ?) "/= #Hl".
     iDestruct "Hl" as (lo ln γ) "(% & Hin)". simplify_eq.
     rel_rec_l. repeat rel_proj_l.
     rel_apply_l (FG_increment_atomic_l (issuedTickets γ)%I True%I); first done.
@@ -307,8 +307,8 @@ Section refinement.
   Lemma release_refinement :
     REL release << reloc.lib.lock.release : lockInt → ().
   Proof.
-    iApply refines_arrow_val; [done|done|].
-    iAlways. iIntros (? lk) "/= #Hl".
+    rel_arrow_val.
+    iIntros (? lk) "/= #Hl".
     iDestruct "Hl" as (lo ln γ) "(% & Hin)". simplify_eq.
     rel_rec_l. rel_proj_l.
     pose (R := fun (o : nat) =>
diff --git a/theories/logic/derived.v b/theories/logic/derived.v
index 431d95b..8b40823 100644
--- a/theories/logic/derived.v
+++ b/theories/logic/derived.v
@@ -21,14 +21,12 @@ Section rules.
     by iApply "HAA".
   Qed.
 
-  Lemma refines_arrow v v' (f x f' x' : binder) (eb eb' : expr) A A' :
-    AsRecV v f x eb →
-    AsRecV v' f' x' eb' →
+  Lemma refines_arrow (v v' : val) A A' :
     □ (∀ v1 v2 : val, □(REL of_val v1 << of_val v2 : A) -∗
       REL App v (of_val v1) << App v' (of_val v2) : A') -∗
     REL v << v' : (A → A')%lrel.
   Proof.
-    iIntros (??) "#H".
+    iIntros "#H".
     iApply refines_arrow_val; eauto.
     iAlways. iIntros (v1 v2) "#HA".
     iApply "H". iAlways.
diff --git a/theories/logic/rules.v b/theories/logic/rules.v
index 64205c6..98df0d5 100644
--- a/theories/logic/rules.v
+++ b/theories/logic/rules.v
@@ -290,14 +290,12 @@ Section rules.
   Qed.
 
   (** This rule is useful for proving that functions refine each other *)
-  Lemma refines_arrow_val v v' (f x f' x' : binder) eb eb' A A' :
-    AsRecV v f x eb →
-    AsRecV v' f' x' eb' →
+  Lemma refines_arrow_val v v' A A' :
     □(∀ v1 v2, A v1 v2 -∗
       REL App v (of_val v1) << App v' (of_val v2) : A') -∗
     REL v << v' : (A → A')%lrel.
   Proof.
-    rewrite /AsRecV. iIntros (-> ->) "#H".
+    rewrite /AsRecV. iIntros "#H".
     iApply refines_spec_ctx. iIntros "Hs".
     iApply refines_ret. iModIntro.
     iModIntro. iIntros (v1 v2) "HA".
-- 
GitLab