From eb63606276aa68efd3923c7e20d8bffbcfbc5ac5 Mon Sep 17 00:00:00 2001
From: jihgfee <jihgfee@gmail.com>
Date: Tue, 8 Sep 2020 12:21:11 +0200
Subject: [PATCH] Updated order of typing rules

---
 theories/logrel/examples/mapper.v   | 13 +++++++------
 theories/logrel/term_typing_rules.v | 14 +++++++-------
 2 files changed, 14 insertions(+), 13 deletions(-)

diff --git a/theories/logrel/examples/mapper.v b/theories/logrel/examples/mapper.v
index 3183772..88145bb 100644
--- a/theories/logrel/examples/mapper.v
+++ b/theories/logrel/examples/mapper.v
@@ -108,9 +108,10 @@ Section mapper_example.
     { iApply ltyped_recv=> //. }
     iApply ltyped_pair.
     - iApply ltyped_var. apply lookup_insert.
-    - rewrite (insert_commute _ "c" "x") //= (insert_commute _ "y" "x") //=.
+    - rewrite insert_insert.
+      rewrite (insert_commute _ "c" "x") //=.
       rewrite insert_insert.
-      iApply (ltyped_frame _ _ _ _ {["x":=_]}).
+      iApply (ltyped_frame _ _ _ _ {["y":=_]}).
       { iApply env_split_right=> //=. iApply env_split_id_r. }
       iApply ltyped_var. apply lookup_insert.
       iApply env_split_right=> //; last by iApply env_split_id_r=> //=. eauto.
@@ -198,9 +199,9 @@ Section mapper_example.
     { iApply ltyped_recv=> //. }
     iApply ltyped_pair.
     - iApply ltyped_var. apply lookup_insert.
-    - rewrite (insert_commute _ "c" "x") //= (insert_commute _ "y" "x") //=.
+    - rewrite insert_insert. rewrite (insert_commute _ "c" "x") //=.
       rewrite insert_insert.
-      iApply (ltyped_frame _ _ _ _ {["x":=_]}).
+      iApply (ltyped_frame _ _ _ _ {["y":=_]}).
       { iApply env_split_right=> //=. iApply env_split_id_r. }
       iApply ltyped_var. apply lookup_insert.
       iApply env_split_right=> //; last by iApply env_split_id_r=> //=. eauto.
@@ -236,8 +237,8 @@ Section mapper_example.
     { iApply env_split_right=> //. iApply env_split_id_r. }
     { iApply ltyped_app.
       - iApply ltyped_var. apply lookup_insert.
-      - rewrite insert_commute //.
-        iApply (ltyped_frame _ _ _ _ {["f":=_]}).
+      - rewrite insert_insert.
+        iApply (ltyped_frame _ _ _ _ {["v":=_]}).
         { iApply env_split_right=> //. iApply env_split_id_r. }
         { iApply ltyped_var. apply lookup_insert. }
         { iApply env_split_right=> //; last by iApply env_split_id_r. eauto. }
diff --git a/theories/logrel/term_typing_rules.v b/theories/logrel/term_typing_rules.v
index 408d8e2..c3a6f93 100644
--- a/theories/logrel/term_typing_rules.v
+++ b/theories/logrel/term_typing_rules.v
@@ -106,10 +106,10 @@ Section properties.
 
   (** Arrow properties *)
   Lemma ltyped_app Γ1 Γ2 Γ3 e1 e2 A1 A2 :
-    (Γ2 ⊨ e1 : A1 ⊸ A2 ⫤ Γ3) -∗ (Γ1 ⊨ e2 : A1 ⫤ Γ2) -∗
+    (Γ1 ⊨ e2 : A1 ⫤ Γ2) -∗ (Γ2 ⊨ e1 : A1 ⊸ A2 ⫤ Γ3) -∗
     Γ1 ⊨ e1 e2 : A2 ⫤ Γ3.
   Proof.
-    iIntros "#H1 #H2". iIntros (vs) "!> HΓ /=".
+    iIntros "#H2 #H1". iIntros (vs) "!> HΓ /=".
     wp_apply (wp_wand with "(H2 [HΓ //])"). iIntros (v) "[HA1 HΓ]".
     wp_apply (wp_wand with "(H1 [HΓ //])"). iIntros (f) "[Hf HΓ]".
     iApply wp_frame_r. iFrame "HΓ". iApply ("Hf" $! v with "HA1").
@@ -172,10 +172,10 @@ Section properties.
 
   (** Product properties  *)
   Lemma ltyped_pair Γ1 Γ2 Γ3 e1 e2 A1 A2 :
-    (Γ2 ⊨ e1 : A1 ⫤ Γ3) -∗ (Γ1 ⊨ e2 : A2 ⫤ Γ2) -∗
+    (Γ1 ⊨ e2 : A2 ⫤ Γ2) -∗ (Γ2 ⊨ e1 : A1 ⫤ Γ3) -∗ 
     Γ1 ⊨ (e1,e2) : A1 * A2 ⫤ Γ3.
   Proof.
-    iIntros "#H1 #H2". iIntros (vs) "!> HΓ /=".
+    iIntros "#H2 #H1". iIntros (vs) "!> HΓ /=".
     wp_apply (wp_wand with "(H2 [HΓ //])"); iIntros (w2) "[HA2 HΓ]".
     wp_apply (wp_wand with "(H1 [HΓ //])"); iIntros (w1) "[HA1 HΓ]".
     wp_pures. iFrame "HΓ". iExists w1, w2. by iFrame.
@@ -590,10 +590,10 @@ Section properties.
       let: "y" := recv "c" in
       switch_body "y" 0 xs (assert: #false) $ λ i, ("f" +:+ pretty i) "c".
 
-    Lemma ltyped_branch Ss A xs :
+    Lemma ltyped_branch Γ Ss A xs :
       (∀ x, x ∈ xs ↔ is_Some (Ss !! x)) →
-      ⊢ ∅ ⊨ branch xs : chan (lty_branch Ss) ⊸
-        lty_arr_list ((λ x, (chan (Ss !!! x) ⊸ A)%lty) <$> xs) A.
+      ⊢ Γ ⊨ branch xs : chan (lty_branch Ss) ⊸
+        lty_arr_list ((λ x, (chan (Ss !!! x) ⊸ A)%lty) <$> xs) A ⫤ ∅.
     Proof.
       iIntros (Hdom) "!>". iIntros (vs) "Hvs".
       iApply wp_value.
-- 
GitLab