From 41ecbafdc28dba38ba3e49fd8f62c423afec0772 Mon Sep 17 00:00:00 2001
From: jihgfee <jihgfee@gmail.com>
Date: Fri, 5 Jun 2020 13:28:30 +0200
Subject: [PATCH] Added a typing rule for conditionals

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

diff --git a/theories/logrel/term_typing_rules.v b/theories/logrel/term_typing_rules.v
index f40a5db..54f29b0 100644
--- a/theories/logrel/term_typing_rules.v
+++ b/theories/logrel/term_typing_rules.v
@@ -88,6 +88,22 @@ Section properties.
     wp_binop. iFrame.
   Qed.
 
+  (** Conditionals *)
+  Lemma ltyped_if Γ1 Γ2 Γ3 e1 e2 e3 A :
+    (Γ1 ⊨ e1 : lty_bool ⫤ Γ2) -∗
+    (Γ2 ⊨ e2 : A ⫤ Γ3) -∗
+    (Γ2 ⊨ e3 : A ⫤ Γ3) -∗
+    Γ1 ⊨ (if: e1 then e2 else e3) : A ⫤ Γ3.
+  Proof.
+    iIntros "#He1 #He2 #He3 !>" (v) "HΓ1".
+    simpl.
+    wp_apply (wp_wand with "(He1 [HΓ1 //])"). iIntros (b) "[Hbool HΓ2]".
+    rewrite /lty_bool. iDestruct "Hbool" as ([]) "->".
+    - wp_apply (wp_wand with "(He2 [HΓ2 //])"). iIntros (w) "[HA HΓ3]". iFrame.
+    - wp_apply (wp_wand with "(He3 [HΓ2 //])"). iIntros (w) "[HA HΓ3]". iFrame.
+  Qed.
+
+
   (** Arrow properties *)
   Lemma ltyped_app Γ1 Γ2 Γ3 e1 e2 A1 A2 :
     (Γ2 ⊨ e1 : A1 ⊸ A2 ⫤ Γ3) -∗ (Γ1 ⊨ e2 : A1 ⫤ Γ2) -∗
-- 
GitLab