From 6a6f8375ceaa5b2d4d7fdf465d8d2c6f48c27a16 Mon Sep 17 00:00:00 2001
From: jihgfee <jihgfee@gmail.com>
Date: Fri, 5 Jun 2020 11:53:00 +0200
Subject: [PATCH] Added operation typing rules

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

diff --git a/theories/logrel/term_typing_rules.v b/theories/logrel/term_typing_rules.v
index 2637dbd..f40a5db 100644
--- a/theories/logrel/term_typing_rules.v
+++ b/theories/logrel/term_typing_rules.v
@@ -6,7 +6,7 @@ From iris.bi.lib Require Import core.
 From iris.base_logic.lib Require Import invariants.
 From iris.heap_lang Require Import metatheory.
 From iris.heap_lang.lib Require Export spawn par assert.
-From actris.logrel Require Export subtyping term_typing_judgment session_types.
+From actris.logrel Require Export subtyping term_typing_judgment operators session_types.
 From actris.logrel Require Import environments.
 From actris.utils Require Import switch.
 From actris.channel Require Import proofmode.
@@ -63,6 +63,31 @@ Section properties.
   Lemma ltyped_int Γ (i : Z) : ⊢ Γ ⊨ #i : lty_int.
   Proof. iIntros "!>" (vs) "HΓ /=". iApply wp_value. eauto. Qed.
 
+  (** Operations *)
+  Lemma ltyped_un_op Γ1 Γ2 op e A B :
+    LTyUnOp op A B →
+    (Γ1 ⊨ e : A ⫤ Γ2) -∗
+    Γ1 ⊨ UnOp op e : B ⫤ Γ2.
+  Proof.
+    iIntros (Hop) "#He !>". iIntros (vs) "HΓ1"=> /=.
+    wp_apply (wp_wand with "(He [HΓ1 //])"). iIntros (v1) "[HA HΓ2]".
+    iDestruct (Hop with "HA") as (w Heval) "HB".
+    wp_unop. iFrame.
+  Qed.
+
+  Lemma ltyped_bin_op Γ1 Γ2 Γ3 op e1 e2 A1 A2 B :
+    LTyBinOp op A1 A2 B →
+    (Γ1 ⊨ e2 : A2 ⫤ Γ2) -∗
+    (Γ2 ⊨ e1 : A1 ⫤ Γ3) -∗
+    Γ1 ⊨ BinOp op e1 e2 : B ⫤ Γ3.
+  Proof.
+    iIntros (Hop) "#He2 #He1 !>". iIntros (vs) "HΓ1"=> /=.
+    wp_apply (wp_wand with "(He2 [HΓ1 //])"). iIntros (v2) "[HA2 HΓ2]".
+    wp_apply (wp_wand with "(He1 [HΓ2 //])"). iIntros (v1) "[HA1 HΓ3]".
+    iDestruct (Hop with "HA1 HA2") as (w Heval) "HB".
+    wp_binop. iFrame.
+  Qed.
+
   (** Arrow properties *)
   Lemma ltyped_app Γ1 Γ2 Γ3 e1 e2 A1 A2 :
     (Γ2 ⊨ e1 : A1 ⊸ A2 ⫤ Γ3) -∗ (Γ1 ⊨ e2 : A1 ⫤ Γ2) -∗
-- 
GitLab