From 869aaaf0ddcdce0427783d80cc62d1bf44cda9ae Mon Sep 17 00:00:00 2001
From: Dan Frumin <dfrumin@cs.ru.nl>
Date: Wed, 27 Mar 2019 17:37:06 +0100
Subject: [PATCH] Add `rel_resolveproph_r`.

---
 theories/examples/coinflip.v        |  4 ++--
 theories/examples/lateearlychoice.v |  3 +--
 theories/logic/proofmode/tactics.v  | 21 +++++++++++++++++++++
 3 files changed, 24 insertions(+), 4 deletions(-)

diff --git a/theories/examples/coinflip.v b/theories/examples/coinflip.v
index 7eaf54a..c9745b6 100644
--- a/theories/examples/coinflip.v
+++ b/theories/examples/coinflip.v
@@ -148,7 +148,7 @@ Section proofs.
       iDestruct "H" as "[Hcl|Hcl]"; rel_load_r; repeat rel_pure_r.
       + rel_apply_r (refines_rand_r b). repeat rel_pure_r.
         rel_store_r. repeat rel_pure_r.
-        rel_apply_r refines_resolveproph_r. repeat rel_pure_r.
+        rel_resolveproph_r. repeat rel_pure_r.
         rel_apply_r (refines_release_r with "Hlk"). iIntros "Hlk".
         repeat rel_pure_r. iMod ("Hclose" with "[-]") as "_".
         { eauto with iFrame. }
@@ -281,7 +281,7 @@ Section proofs.
           iIntros "Hlk". repeat rel_pure_r. rel_load_r.
           repeat rel_pure_r. rel_apply_r (refines_rand_r b).
           repeat rel_pure_r. rel_store_r.
-          repeat rel_pure_r. rel_apply_r refines_resolveproph_r.
+          repeat rel_pure_r. rel_resolveproph_r.
           repeat rel_pure_r. rel_apply_r (refines_release_r with "Hlk").
           iIntros "Hlk". repeat rel_pure_r.
           iMod ("Hclose" with "[-]") as "_".
diff --git a/theories/examples/lateearlychoice.v b/theories/examples/lateearlychoice.v
index ec29969..1486e54 100644
--- a/theories/examples/lateearlychoice.v
+++ b/theories/examples/lateearlychoice.v
@@ -123,8 +123,7 @@ Section proof.
     rel_apply_l refines_rand_l.
     iNext. iIntros (b). repeat rel_pure_l.
     rel_apply_r (refines_rand_r b).
-    repeat rel_pure_r.
-    rel_apply_r refines_resolveproph_r.
+    repeat rel_pure_r. rel_resolveproph_r.
     repeat rel_pure_r. rel_values.
   Qed.
 
diff --git a/theories/logic/proofmode/tactics.v b/theories/logic/proofmode/tactics.v
index de21aa0..cf2b55d 100644
--- a/theories/logic/proofmode/tactics.v
+++ b/theories/logic/proofmode/tactics.v
@@ -567,6 +567,27 @@ Tactic Notation "rel_newproph_l" :=
 
 (** ResolveProph *)
 (* TODO: implement this lol *)
+Lemma tac_rel_resolveproph_r `{relocG Σ} K' ℶ E (p :proph_id) w e t A :
+  t = fill K' (ResolveProph #p (of_val w)) →
+  nclose specN ⊆ E →
+  envs_entails ℶ (refines E e (fill K' #()) A) →
+  envs_entails ℶ (refines E e t A).
+Proof.
+  intros ???. subst t.
+  rewrite -refines_resolveproph_r //.
+Qed.
+
+Tactic Notation "rel_resolveproph_r" :=
+  iStartProof;
+  first
+    [rel_reshape_cont_r ltac:(fun K e' =>
+       eapply (tac_rel_resolveproph_r K);
+       [reflexivity  (** t = K'[resolveproph] *)
+       |idtac..])
+    |fail 1 "rel_resolveproph_r: cannot find 'ResolveProph'"];
+  [solve_ndisj || fail "rel_resolveproph_r: cannot prove 'nclose specN ⊆ ?'"
+  |rel_finish  (** new goal *)].
+
 
 (** Fork *)
 Lemma tac_rel_fork_l `{relocG Σ} K ℶ E e' eres e t A :
-- 
GitLab