From 9357c01334214663fbf023eda2f28906d737c4c3 Mon Sep 17 00:00:00 2001
From: Dan Frumin <dfrumin@cs.ru.nl>
Date: Wed, 31 Jan 2018 19:19:21 +0100
Subject: [PATCH] Move the -val-arrow rule to rules.v

---
 theories/logrel/rules.v | 27 +++++++++++++++++++++++++++
 1 file changed, 27 insertions(+)

diff --git a/theories/logrel/rules.v b/theories/logrel/rules.v
index 5657551..b613a56 100644
--- a/theories/logrel/rules.v
+++ b/theories/logrel/rules.v
@@ -47,6 +47,33 @@ Section properties.
     rewrite /env_subst. rewrite !Closed_subst_p_id. done.
   Qed.
 
+  Notation "P ∗-∗ Q" := ((P -∗ Q) ∗ (Q -∗ P))%I (at level 50).
+  Lemma interp_val_arrow τ σ Δ (v v' : val) ρ :
+    spec_ctx ρ -∗
+    ⟦ τ → σ ⟧ Δ (v, v')
+              ∗-∗
+    (□ (∀ (w w' : val), ⟦ τ ⟧ Δ (w, w')
+      -∗ {Δ;∅} ⊨ v w ≤log≤ v' w' : σ))%I.
+  Proof.
+    iIntros "#Hspec".
+    iSplitL.
+    - iIntros "/= #Hvv !#".
+      iIntros (w w') "#Hw".
+      iApply related_ret.
+      iApply ("Hvv" $! (w, w') with "Hw").
+    - iIntros "#Hvv /= !#".
+      iIntros ([w w']) "#Hww /=".
+      iSpecialize ("Hvv" with "Hww").
+      rewrite bin_log_related_eq /bin_log_related_def.
+      iIntros (j K) "Hj /=".
+      iSpecialize ("Hvv" $! ∅ ρ with "Hspec []").
+      { iAlways. by iApply interp_env_nil. }
+      rewrite /interp_expr /=.
+      iSpecialize ("Hvv" $! j K).
+      rewrite /env_subst !fmap_empty !subst_p_empty.
+      by iMod ("Hvv" with "Hj").
+  Qed.
+
   Lemma bin_log_related_weaken_2 τi E Δ Γ e1 e2 (τ : type) :
     {E;Δ;Γ} ⊨ e1 ≤log≤ e2 : τ -∗
     {E;τi::Δ;⤉Γ} ⊨ e1 ≤log≤ e2 : τ.[ren (+1)].
-- 
2.22.0