From f65e40d268845d70374ed4da780fa09cd2a1c336 Mon Sep 17 00:00:00 2001
From: Dan Frumin <dfrumin@cs.ru.nl>
Date: Fri, 15 Mar 2019 16:36:44 +0100
Subject: [PATCH] simplify lrel_forall

---
 theories/examples/bit.v        |  2 ++
 theories/examples/cell.v       | 20 ++++----------------
 theories/logic/compatibility.v | 10 ++++++++++
 theories/logic/model.v         |  2 +-
 theories/typing/fundamental.v  |  8 +++-----
 theories/typing/types.v        |  5 +++--
 6 files changed, 23 insertions(+), 24 deletions(-)

diff --git a/theories/examples/bit.v b/theories/examples/bit.v
index 0ca7c8b..d3c714b 100644
--- a/theories/examples/bit.v
+++ b/theories/examples/bit.v
@@ -1,3 +1,5 @@
+(* ReLoC -- Relational logic for fine-grained concurrency *)
+(** A simple bit module *)
 From iris.proofmode Require Import tactics.
 From reloc Require Import reloc.
 Set Default Proof Using "Type".
diff --git a/theories/examples/cell.v b/theories/examples/cell.v
index 9506143..c7e4ba8 100644
--- a/theories/examples/cell.v
+++ b/theories/examples/cell.v
@@ -59,22 +59,10 @@ Section cell_refinement.
   Lemma cell2_cell1_refinement :
     REL cell2 << cell1 : ∀ α, ∃ β, (α → β) * (β → α) * (β → α → ()).
   Proof.
-    (* TODO: this uuugly *)
-    pose (Ï„ := (TExists (TProd (TProd (TArrow (TVar 1) (TVar 0))
-                                 (TArrow (TVar 0) (TVar 1)))
-                                 (TArrow (TVar 0) (TArrow (TVar 1) TUnit))))%nat).
-    iPoseProof (bin_log_related_tlam [] ∅ _ _ τ) as "H".
-    iSpecialize ("H" with "[]"); last first.
-    { rewrite /bin_log_related.
-      iSpecialize ("H" $! ∅ with "[]").
-      - rewrite fmap_empty. iApply env_ltyped2_empty.
-      - rewrite !fmap_empty !subst_map_empty.
-        iSimpl in "H". iApply "H". }
-    iIntros (R) "!#".
-    iApply (bin_log_related_pack (cellR R)).
-    iIntros (vs) "Hvs". rewrite !fmap_empty env_ltyped2_empty_inv.
-    iDestruct "Hvs" as %->. rewrite !fmap_empty !subst_map_empty.
-    iSimpl. repeat iApply refines_pair.
+    unfold cell1, cell2. rel_pure_l. rel_pure_r.
+    iApply refines_forall. iAlways. iIntros (R).
+    iApply (refines_exists (cellR R)).
+    repeat iApply refines_pair.
     - (* New cell *)
       rel_pure_l. rel_pure_r.
       iApply refines_arrow_val.
diff --git a/theories/logic/compatibility.v b/theories/logic/compatibility.v
index 3ed171b..c6f7673 100644
--- a/theories/logic/compatibility.v
+++ b/theories/logic/compatibility.v
@@ -68,5 +68,15 @@ Section compatibility.
     iModIntro. iExists A. done.
   Qed.
 
+  Lemma refines_forall e e' (C : lrel Σ → lrel Σ) :
+    □ (∀ A, REL e << e' : C A) -∗
+    REL (λ: <>, e)%V << (λ: <>, e')%V : ∀ A, C A.
+  Proof.
+    iIntros "#H".
+    rel_values. iModIntro.
+    iIntros (A ? ?) "_ !#".
+    rel_rec_l. rel_rec_r. iApply "H".
+  Qed.
+
 End compatibility.
 
diff --git a/theories/logic/model.v b/theories/logic/model.v
index 2d472e7..6a4fa17 100644
--- a/theories/logic/model.v
+++ b/theories/logic/model.v
@@ -114,7 +114,7 @@ Section semtypes.
     ∃ A, C A w1 w2)%I.
 
   Definition lrel_forall (C : lrel Σ → lrel Σ) : lrel Σ := LRel (λ w1 w2,
-    □ ∀ A : lrel Σ, (lrel_arr lrel_unit (C A))%lrel w1 w2)%I.
+    ∀ A : lrel Σ, (lrel_arr lrel_unit (C A))%lrel w1 w2)%I.
 
   Definition lrel_true : lrel Σ := LRel (λ w1 w2, True)%I.
 
diff --git a/theories/typing/fundamental.v b/theories/typing/fundamental.v
index c394641..a47064b 100644
--- a/theories/typing/fundamental.v
+++ b/theories/typing/fundamental.v
@@ -142,11 +142,9 @@ Section fundamental.
     {Δ;Γ} ⊨ (Λ: e) ≤log≤ (Λ: e') : TForall τ.
   Proof.
     iIntros "#H".
-   intro_clause.
-    iApply refines_spec_ctx. iDestruct 1 as (ρ) "#Hs".
-    value_case. rewrite /lrel_forall /lrel_car /=.
-    iModIntro. iModIntro. iIntros (A) "!>". iIntros (? ?) "_".
-    rel_pure_l. rel_pure_r.
+    intro_clause. rel_pure_l. rel_pure_r.
+    iApply refines_forall.
+    iModIntro. iIntros (A).
     iDestruct ("H" $! A) as "#H1".
     iApply "H1".
     by rewrite (interp_ren A Δ Γ).
diff --git a/theories/typing/types.v b/theories/typing/types.v
index a4b524c..8b06755 100644
--- a/theories/typing/types.v
+++ b/theories/typing/types.v
@@ -78,8 +78,9 @@ Reserved Notation "Γ ⊢ₜ e : τ" (at level 74, e, τ at next level).
 Notation "⤉ Γ" := (Autosubst_Classes.subst (ren (+1)%nat) <$> Γ) (at level 10, format "⤉ Γ").
 
 (** We model type-level lambdas and applications as thunks *)
-Notation "Λ: e" := (λ: <>, e)%E (at level 200).
-Notation "'TApp' e" := (App e%E #()%E) (at level 200).
+Notation "Λ: e" := (λ: <>, e)%E (at level 200, only parsing).
+Notation "Λ: e" := (λ: <>, e)%V (at level 200, only parsing) : val_scope.
+Notation "'TApp' e" := (App e%E #()%E) (at level 200, only parsing).
 
 (* To unfold a recursive type, we need to take a step. We thus define the
 unfold operator to be the identity function. *)
-- 
GitLab