From 79cb9880c5a91398c9c88268b174646590a0d7f2 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sun, 14 Jun 2020 21:08:08 +0200
Subject: [PATCH] Remove redundant expression typing rules for nat/unit/bool.

---
 theories/typing/fundamental.v | 12 -------
 theories/typing/types.v       | 66 ++++++++++++++++-------------------
 2 files changed, 31 insertions(+), 47 deletions(-)

diff --git a/theories/typing/fundamental.v b/theories/typing/fundamental.v
index e60a907..5ced5e1 100644
--- a/theories/typing/fundamental.v
+++ b/theories/typing/fundamental.v
@@ -36,15 +36,6 @@ Section fundamental.
     by iApply refines_ret.
   Qed.
 
-  Lemma bin_log_related_unit Î” Î“ : âŠ¢ {Î”;Î“} âŠ¨ #() â‰¤logâ‰¤ #() : ().
-  Proof. value_case. Qed.
-
-  Lemma bin_log_related_nat Î” Î“ (n : nat) : âŠ¢ {Î”;Î“} âŠ¨ #n â‰¤logâ‰¤ #n : TNat.
-  Proof. value_case. Qed.
-
-  Lemma bin_log_related_bool Î” Î“ (b : bool) : âŠ¢ {Î”;Î“} âŠ¨ #b â‰¤logâ‰¤ #b : TBool.
-  Proof. value_case. Qed.
-
   Lemma bin_log_related_pair Î” Î“ e1 e2 e1' e2' (Ï„1 Ï„2 : type) :
     ({Î”;Î“} âŠ¨ e1 â‰¤logâ‰¤ e1' : Ï„1) -âˆ—
     ({Î”;Î“} âŠ¨ e2 â‰¤logâ‰¤ e2' : Ï„2) -âˆ—
@@ -502,9 +493,6 @@ Section fundamental.
       + by iApply bin_log_related_var.
       + iIntros (Î³) "#H". simpl. rel_values.
         iModIntro. by iApply fundamental_val.
-      + iApply bin_log_related_unit.
-      + by iApply bin_log_related_nat.
-      + by iApply bin_log_related_bool.
       + iApply bin_log_related_nat_binop; first done;
           by iApply fundamental.
       + iApply bin_log_related_bool_binop; first done;
diff --git a/theories/typing/types.v b/theories/typing/types.v
index 6df35ff..9a7c675 100644
--- a/theories/typing/types.v
+++ b/theories/typing/types.v
@@ -104,16 +104,12 @@ Instance insert_binder (A : Type): Insert binder A (stringmap A) :=
 
 (** Typing itself *)
 Inductive typed : stringmap type â†’ expr â†’ type â†’ Prop :=
-  | Var_typed Î“ x Ï„ : Î“ !! x = Some Ï„ â†’ Î“ âŠ¢â‚œ Var x : Ï„
+  | Var_typed Î“ x Ï„ :
+     Î“ !! x = Some Ï„ â†’
+     Î“ âŠ¢â‚œ Var x : Ï„
   | Val_typed Î“ v Ï„ :
-      âŠ¢áµ¥ v : Ï„ â†’
-      Î“ âŠ¢â‚œ Val v : Ï„
-  | Unit_typed Î“ :
-      Î“ âŠ¢â‚œ #() : ()
-  | Nat_typed Î“ (n : nat) :
-      Î“ âŠ¢â‚œ #n : TNat
-  | Bool_typed Î“ (b : bool) :
-      Î“ âŠ¢â‚œ #b : TBool
+     âŠ¢áµ¥ v : Ï„ â†’
+     Î“ âŠ¢â‚œ Val v : Ï„
   | BinOp_typed_nat Î“ op e1 e2 Ï„ :
      Î“ âŠ¢â‚œ e1 : TNat â†’ Î“ âŠ¢â‚œ e2 : TNat â†’
      binop_nat_res_type op = Some Ï„ â†’
@@ -126,20 +122,20 @@ Inductive typed : stringmap type â†’ expr â†’ type â†’ Prop :=
      Î“ âŠ¢â‚œ e1 : ref Ï„ â†’ Î“ âŠ¢â‚œ e2 : ref Ï„ â†’
      Î“ âŠ¢â‚œ BinOp EqOp e1 e2 : TBool
   | Pair_typed Î“ e1 e2 Ï„1 Ï„2 :
-      Î“ âŠ¢â‚œ e1 : Ï„1 â†’ Î“ âŠ¢â‚œ e2 : Ï„2 â†’
-      Î“ âŠ¢â‚œ (e1, e2) : Ï„1 * Ï„2
+     Î“ âŠ¢â‚œ e1 : Ï„1 â†’ Î“ âŠ¢â‚œ e2 : Ï„2 â†’
+     Î“ âŠ¢â‚œ (e1, e2) : Ï„1 * Ï„2
   | Fst_typed Î“ e Ï„1 Ï„2 :
-      Î“ âŠ¢â‚œ e : Ï„1 * Ï„2 â†’
-      Î“ âŠ¢â‚œ Fst e : Ï„1
+     Î“ âŠ¢â‚œ e : Ï„1 * Ï„2 â†’
+     Î“ âŠ¢â‚œ Fst e : Ï„1
   | Snd_typed Î“ e Ï„1 Ï„2 :
-      Î“ âŠ¢â‚œ e : Ï„1 * Ï„2 â†’
-      Î“ âŠ¢â‚œ Snd e : Ï„2
+     Î“ âŠ¢â‚œ e : Ï„1 * Ï„2 â†’
+     Î“ âŠ¢â‚œ Snd e : Ï„2
   | InjL_typed Î“ e Ï„1 Ï„2 :
-      Î“ âŠ¢â‚œ e : Ï„1 â†’
-      Î“ âŠ¢â‚œ InjL e : Ï„1 + Ï„2
+     Î“ âŠ¢â‚œ e : Ï„1 â†’
+     Î“ âŠ¢â‚œ InjL e : Ï„1 + Ï„2
   | InjR_typed Î“ e Ï„1 Ï„2 :
-      Î“ âŠ¢â‚œ e : Ï„2 â†’
-      Î“ âŠ¢â‚œ InjR e : Ï„1 + Ï„2
+     Î“ âŠ¢â‚œ e : Ï„2 â†’
+     Î“ âŠ¢â‚œ InjR e : Ï„1 + Ï„2
   | Case_typed Î“ e0 e1 e2 Ï„1 Ï„2 Ï„3 :
      Î“ âŠ¢â‚œ e0 : Ï„1 + Ï„2 â†’
      Î“ âŠ¢â‚œ e1 : (Ï„1 â†’ Ï„3) â†’
@@ -164,18 +160,18 @@ Inductive typed : stringmap type â†’ expr â†’ type â†’ Prop :=
      Î“ âŠ¢â‚œ e : (âˆ€: Ï„) â†’
      Î“ âŠ¢â‚œ e #() : Ï„.[Ï„'/]
   | TFold Î“ e Ï„ :
-      Î“ âŠ¢â‚œ e : Ï„.[(Î¼: Ï„)%ty/] â†’
-      Î“ âŠ¢â‚œ e : (Î¼: Ï„)
+     Î“ âŠ¢â‚œ e : Ï„.[(Î¼: Ï„)%ty/] â†’
+     Î“ âŠ¢â‚œ e : (Î¼: Ï„)
   | TUnfold Î“ e Ï„ :
-      Î“ âŠ¢â‚œ e : (Î¼: Ï„)%ty â†’
-      Î“ âŠ¢â‚œ rec_unfold e : Ï„.[(Î¼: Ï„)%ty/]
+     Î“ âŠ¢â‚œ e : (Î¼: Ï„)%ty â†’
+     Î“ âŠ¢â‚œ rec_unfold e : Ï„.[(Î¼: Ï„)%ty/]
   | TPack Î“ e Ï„ Ï„' :
-      Î“ âŠ¢â‚œ e : Ï„.[Ï„'/] â†’
-      Î“ âŠ¢â‚œ e : (âˆƒ: Ï„)
+     Î“ âŠ¢â‚œ e : Ï„.[Ï„'/] â†’
+     Î“ âŠ¢â‚œ e : (âˆƒ: Ï„)
   | TUnpack Î“ e1 x e2 Ï„ Ï„2 :
-      Î“ âŠ¢â‚œ e1 : (âˆƒ: Ï„) â†’
-      <[x:=Ï„]>(â¤‰ Î“) âŠ¢â‚œ e2 : (Autosubst_Classes.subst (ren (+1)) Ï„2) â†’
-      Î“ âŠ¢â‚œ (unpack: x := e1 in e2) : Ï„2
+     Î“ âŠ¢â‚œ e1 : (âˆƒ: Ï„) â†’
+     <[x:=Ï„]>(â¤‰ Î“) âŠ¢â‚œ e2 : (Autosubst_Classes.subst (ren (+1)) Ï„2) â†’
+     Î“ âŠ¢â‚œ (unpack: x := e1 in e2) : Ï„2
   | TFork Î“ e : Î“ âŠ¢â‚œ e : () â†’ Î“ âŠ¢â‚œ Fork e : ()
   | TAlloc Î“ e Ï„ : Î“ âŠ¢â‚œ e : Ï„ â†’ Î“ âŠ¢â‚œ Alloc e : ref Ï„
   | TLoad Î“ e Ï„ : Î“ âŠ¢â‚œ e : ref Ï„ â†’ Î“ âŠ¢â‚œ Load e : Ï„
@@ -193,15 +189,15 @@ with val_typed : val â†’ type â†’ Prop :=
   | Nat_val_typed (n : nat) : âŠ¢áµ¥ #n : TNat
   | Bool_val_typed (b : bool) : âŠ¢áµ¥ #b : TBool
   | Pair_val_typed v1 v2 Ï„1 Ï„2 :
-      âŠ¢áµ¥ v1 : Ï„1 â†’
-      âŠ¢áµ¥ v2 : Ï„2 â†’
-      âŠ¢áµ¥ PairV v1 v2 : (Ï„1 * Ï„2)
+     âŠ¢áµ¥ v1 : Ï„1 â†’
+     âŠ¢áµ¥ v2 : Ï„2 â†’
+     âŠ¢áµ¥ PairV v1 v2 : (Ï„1 * Ï„2)
   | InjL_val_typed v Ï„1 Ï„2 :
-      âŠ¢áµ¥ v : Ï„1 â†’
-      âŠ¢áµ¥ InjLV v : (Ï„1 + Ï„2)
+     âŠ¢áµ¥ v : Ï„1 â†’
+     âŠ¢áµ¥ InjLV v : (Ï„1 + Ï„2)
   | InjR_val_typed v Ï„1 Ï„2 :
-      âŠ¢áµ¥ v : Ï„2 â†’
-      âŠ¢áµ¥ InjRV v : (Ï„1 + Ï„2)
+     âŠ¢áµ¥ v : Ï„2 â†’
+     âŠ¢áµ¥ InjRV v : (Ï„1 + Ï„2)
   | Rec_val_typed f x e Ï„1 Ï„2 :
      <[f:=TArrow Ï„1 Ï„2]>(<[x:=Ï„1]>âˆ…) âŠ¢â‚œ e : Ï„2 â†’
      âŠ¢áµ¥ RecV f x e : (Ï„1 â†’ Ï„2)
-- 
GitLab