Deindex syntactic typing judgment

Thanks to changes to definition typing, we needn't use level one for typing definition values. Do beware that the enabling changes loose precision, but I think in an acceptable and standard way. Using on-paper syntax, consider proving definition typing for a member value, specifically, proving `Γ | this : T ⊢ { a = v } : { a : U }`. - Without enabling commits, we must prove (something equivalent to) `Γ, this: TLater T ⊢ v : TLater U`. - With enabling commits, we must prove `Γ, this: T ⊢ v : U`: this discards the fact that `Γ` is in fact typed in an earlier world. However, that's standard for tuples when the product type is contractive, and removes an annoying index from the typing rules.
Blaisorblade · Feb 2, 2019 · 466847b · 466847b
1 parent 8f6df8e
commit 466847b
Show file tree

Hide file tree

Showing 4 changed files with 68 additions and 74 deletions.
diff --git a/theories/Dot/fundamental.v b/theories/Dot/fundamental.v
@@ -21,21 +21,21 @@ Section fundamental.
       (and probably add hypotheses to that effect). *)
   (* XXX lift translation and is_syn to contexts. Show that syntactic typing
      implies is_syn and closure. Stop talking about free variables inside is_syn? *)
-  Lemma typed_tm_is_syn Γ e T i:
-    Γ ⊢ₜ e : T, i →
+  Lemma typed_tm_is_syn Γ e T:
+    Γ ⊢ₜ e : T →
     is_syn_tm e.
   Admitted.
 
-  Lemma typed_ty_is_syn Γ e T i:
-    Γ ⊢ₜ e : T, i →
+  Lemma typed_ty_is_syn Γ e T:
+    Γ ⊢ₜ e : T →
     is_syn_ty T.
   Admitted.
 
   (* Check all types are syntactic. *)
   Definition is_syn_ctx Γ := Forall is_syn_ty Γ.
 
-  Lemma typed_ctx_is_syn Γ e T i:
-    Γ ⊢ₜ e : T, i →
+  Lemma typed_ctx_is_syn Γ e T:
+    Γ ⊢ₜ e : T →
     is_syn_ctx Γ.
   Admitted.
 
@@ -275,12 +275,12 @@ Section fundamental.
     - admit.
   Admitted.
 
-  Lemma translations_types_equivalent e T T' T'' Γ i:
-    (t_ty T T' → t_ty T T'' → Γ ⊨ e : T', i → Γ ⊨ e : T'', i )%I.
+  Lemma translations_types_equivalent e T T' T'' Γ:
+    (t_ty T T' → t_ty T T'' → Γ ⊨ e : T' → Γ ⊨ e : T'')%I.
   Proof.
     iIntros "#A #B #[% #HeT'] /="; iSplit => //. iIntros (ρ) "!> #HG".
     rewrite /interp_expr /=.
-    iSpecialize ("HeT'" with "HG"). iModIntro.
+    iSpecialize ("HeT'" with "HG").
     iApply wp_strong_mono => //.
     iIntros (v) "HT' !>". by iApply (translations_types_equivalent_vals T T' T'').
   Qed.
@@ -300,9 +300,9 @@ Section fundamental.
   Admitted.
   (* But I guess we'll we actually need to say that two substitutions translate each other. *)
 
-  Fixpoint not_yet_fundamental Γ e T e' T' i (HT: Γ ⊢ₜ e : T, i) {struct HT}:
+  Fixpoint not_yet_fundamental Γ e T e' T' (HT: Γ ⊢ₜ e : T) {struct HT}:
   (* Lemma not_yet_fundamental Γ e T e' T' (HT: Γ ⊢ₜ e : T): *)
-    (t_tm e e' → t_ty T T' → |==> Γ ⊨ e' : T', i)%I.
+    (t_tm e e' → t_ty T T' → |==> Γ ⊨ e' : T')%I.
   Proof.
     iIntros "#HtrE #HtrT".
     (* destruct HT. *)
@@ -330,7 +330,7 @@ Section fundamental.
       { by iApply t_ty_subst_special. }
       iApply translations_types_equivalent; try done.
 
-      by iApply (T_Forall_Ex  with "toto tata").
+      admit; by iApply (T_Forall_Ex  with "toto tata").
     -
       (* I'm careful with simplification to avoid unfolding too much. *)
       cbn [t_tm] in * |- *; case_match; try done.
@@ -343,7 +343,7 @@ Section fundamental.
       { cbn; by iSplit. }
       iMod ("IHT"with "Htr1 HtrTAll") as "#HsT1".
       iMod ("IHT1" with "Htr2 HTTr") as "#HsT2".
-      by iApply (T_Forall_E with "HsT1 HsT2").
+      admit; by iApply (T_Forall_E with "HsT1 HsT2").
     (* pose proof (typed_tm_is_syn Γ e T HT) as HeSyn. *)
     (* pose proof (typed_ty_is_syn Γ e T HT) as HTSyn. *)
     (* pose proof (typed_ctx_is_syn Γ e T HT) as HΓSyn. *)

diff --git a/theories/Dot/lr_lemma.v b/theories/Dot/lr_lemma.v
@@ -116,14 +116,14 @@ Section Sec.
     iApply ("Hstp" $! (_ :: _) _); rewrite ?iterate_TLater_later //; by iSplit.
   Qed.
 
-  Lemma T_Forall_E e1 e2 T1 T2 i:
-    (Γ ⊨ e1: TAll T1 T2.|[ren (+1)], i →
-     Γ ⊨ e2 : T1, i →
+  Lemma T_Forall_E e1 e2 T1 T2:
+    (Γ ⊨ e1: TAll T1 T2.|[ren (+1)] →
+     Γ ⊨ e2 : T1 →
     (*────────────────────────────────────────────────────────────*)
-     Γ ⊨ tapp e1 e2 : T2, i)%I.
+     Γ ⊨ tapp e1 e2 : T2)%I.
   Proof.
     iIntros "/= #[% He1] #[% Hv2]". iSplit; eauto using fv_tapp. iIntros " !> * #HG".
-    iSpecialize ("He1" with "HG"); iSpecialize ("Hv2" with "HG"). iModIntro.
+    iSpecialize ("He1" with "HG"); iSpecialize ("Hv2" with "HG").
     smart_wp_bind (AppLCtx (e2.|[to_subst ρ])) v "#Hr" "He1".
     smart_wp_bind (AppRCtx v) w "#Hw" "Hv2".
     iDestruct "Hr" as (Hclv t ->) "#Hv".
@@ -133,17 +133,17 @@ Section Sec.
     by iApply interp_weaken_one.
   Qed.
 
-  Lemma T_Forall_Ex e1 v2 T1 T2 i:
-    (Γ ⊨ e1: TAll T1 T2, i →
-     Γ ⊨ tv v2 : T1, i →
+  Lemma T_Forall_Ex e1 v2 T1 T2:
+    (Γ ⊨ e1: TAll T1 T2 →
+     Γ ⊨ tv v2 : T1 →
     (*────────────────────────────────────────────────────────────*)
-     Γ ⊨ tapp e1 (tv v2) : T2.|[v2/], i)%I.
+     Γ ⊨ tapp e1 (tv v2) : T2.|[v2/])%I.
   Proof.
     iIntros "/= #[% He1] #[% Hv2Arg]". move: H H0 => Hcle1 Hclv2. iSplit; eauto using fv_tapp. iIntros " !> * #HG".
     (* iAssert (⌜ length ρ = length Γ ⌝)%I as "%". by iApply interp_env_len_agree. move: H => Hlen. *)
     iAssert (⌜ nclosed_vl v2 (length Γ) ⌝)%I as "%". by iPureIntro; apply fv_tv_inv. move: H => Hcl.
     (* assert (nclosed_vl v2 (length ρ)). by rewrite Hlen. *)
-    iSpecialize ("He1" with "HG"); iSpecialize ("Hv2Arg" with "HG"). iModIntro.
+    iSpecialize ("He1" with "HG"); iSpecialize ("Hv2Arg" with "HG").
     smart_wp_bind (AppLCtx (tv v2.[to_subst ρ])) v "#Hr" "He1".
     iDestruct "Hr" as (Hclv t ->) "#HvFun".
     iApply wp_pure_step_later; trivial. iNext.
@@ -159,9 +159,9 @@ Section Sec.
       We'd need this swap, and then [iIntros (v)], to specialize the hypothesis
       and drop the [▷^i] modality.*)
   Lemma T_Forall_I T1 T2 e:
-    (T1.|[ren (+1)] :: Γ ⊨ e : T2, 0 →
+    (T1.|[ren (+1)] :: Γ ⊨ e : T2 →
     (*─────────────────────────*)
-    Γ ⊨ tv (vabs e) : TAll T1 T2, 0)%I.
+    Γ ⊨ tv (vabs e) : TAll T1 T2)%I.
   Proof.
     iIntros "/= #[% #HeT]". move: H => Hcle.
     iSplit; eauto using fv_tv, fv_vabs.

diff --git a/theories/Dot/typing.v b/theories/Dot/typing.v
@@ -1,7 +1,7 @@
 From D Require Import tactics.
 From D.Dot Require Import dotsyn.
 
-Reserved Notation "Γ ⊢ₜ e : T , i" (at level 74, e, T at next level).
+Reserved Notation "Γ ⊢ₜ e : T" (at level 74, e, T at next level).
 Reserved Notation "Γ ⊢ₚ p : T , i" (at level 74, p, T, i at next level).
 Reserved Notation "Γ |d V ⊢ d : T" (at level 74, d, T, V at next level).
 Reserved Notation "Γ |ds V ⊢ ds : T" (at level 74, ds, T, V at next level).
@@ -15,66 +15,60 @@ Here we follow Nada Amin's judgment for definition typing: it is Γ ⊢ { l = d
 meaning: this definition, with label l, has type T.
 This works, but requires reformulating again a bit semantic definition typing for proofs.
 *)
-Inductive typed Γ: tm → ty → nat → Prop :=
+Inductive typed Γ: tm → ty → Prop :=
 (** First, elimination forms *)
 (** Dependent application; only allowed if the argument is a value . *)
-| Appv_typed e1 v2 T1 T2 i:
-    Γ ⊢ₜ e1: TAll T1 T2, i →                        Γ ⊢ₜ tv v2 : T1, i →
+| Appv_typed e1 v2 T1 T2:
+    Γ ⊢ₜ e1: TAll T1 T2 →                        Γ ⊢ₜ tv v2 : T1 →
     (*────────────────────────────────────────────────────────────*)
-    Γ ⊢ₜ tapp e1 (tv v2) : T2.|[v2/], i
+    Γ ⊢ₜ tapp e1 (tv v2) : T2.|[v2/]
 (** Non-dependent application; allowed for any argument. *)
-| App_typed e1 e2 T1 T2 i:
-    Γ ⊢ₜ e1: TAll T1 T2.|[ren (+1)], i →      Γ ⊢ₜ e2 : T1, i →
+| App_typed e1 e2 T1 T2:
+    Γ ⊢ₜ e1: TAll T1 T2.|[ren (+1)] →      Γ ⊢ₜ e2 : T1 →
     (*────────────────────────────────────────────────────────────*)
-    Γ ⊢ₜ tapp e1 e2 : T2, i
-| Proj_typed e T l i:
-    Γ ⊢ₜ e : TVMem l T, i →
+    Γ ⊢ₜ tapp e1 e2 : T2
+| Proj_typed e T l:
+    Γ ⊢ₜ e : TVMem l T →
     (*─────────────────────────*)
-    Γ ⊢ₜ tproj e l : T, i
-| TMuE_typed v T i:
-    Γ ⊢ₜ tv v: TMu T, i →
+    Γ ⊢ₜ tproj e l : T
+| TMuE_typed v T:
+    Γ ⊢ₜ tv v: TMu T →
     (*──────────────────────*)
-    Γ ⊢ₜ tv v: T.|[v/], i
+    Γ ⊢ₜ tv v: T.|[v/]
 (** Introduction forms *)
-| Lam_typed e T1 T2 :
+| Lam_typed e T1 T2:
     (* T1 :: Γ ⊢ₜ e : T2 → (* Would work, but allows the argument to occur in its own type. *) *)
-    T1.|[ren (+1)] :: Γ ⊢ₜ e : T2, 0 →
+    T1.|[ren (+1)] :: Γ ⊢ₜ e : T2 →
     (*─────────────────────────*)
-    Γ ⊢ₜ tv (vabs e) : TAll T1 T2, 0
+    Γ ⊢ₜ tv (vabs e) : TAll T1 T2
 | VObj_typed ds T:
     Γ |ds T ⊢ ds: T →
     (*──────────────────────*)
-    Γ ⊢ₜ tv (vobj ds): TMu T, 0
-| TMuI_typed v T i:
-    Γ ⊢ₜ tv v: T.|[v/], i →
+    Γ ⊢ₜ tv (vobj ds): TMu T
+| TMuI_typed v T:
+    Γ ⊢ₜ tv v: T.|[v/] →
     (*──────────────────────*)
-    Γ ⊢ₜ tv v: TMu T, i
+    Γ ⊢ₜ tv v: TMu T
 | Nat_typed n:
-    Γ ⊢ₜ tv (vnat n): TNat, 0
+    Γ ⊢ₜ tv (vnat n): TNat
 
 (** "General" rules *)
 | Var_typed x T :
     (* After looking up in Γ, we must weaken T for the variables on top of x. *)
     Γ !! x = Some T →
     (*──────────────────────*)
-    Γ ⊢ₜ tv (var_vl x) : T.|[ren (+x)], 0
-| Subs_typed e T1 T2 j :
-    Γ ⊢ₜ T1, 0 <: T2, j → Γ ⊢ₜ e : T1, 0 →
+    Γ ⊢ₜ tv (var_vl x) : T.|[ren (+x)]
+| Subs_typed e T1 T2 i :
+    Γ ⊢ₜ T1, 0 <: T2, i → Γ ⊢ₜ e : T1 →
     (*───────────────────────────────*)
-    Γ ⊢ₜ iterate tskip j e : T2, 0
-(* XXX Must be generalized to something like the following, but that needs either
-   skip instructions, or an indexed typing judgment. *)
-(* | Subs_typed e i1 i2 T1 T2 : *)
-(*     Γ ⊢ₜ T1, i1 <: T2, i2 → Γ ⊢ₜ  e : T1 → *)
-(*     (*──────────────────────*) *)
-(*     Γ ⊢ₜ e : T2 *)
+    Γ ⊢ₜ iterate tskip i e : T2
 (* A bit surprising this is needed, but appears in the DOT papers, and this is
    only admissible if t has a type U that is a proper subtype of TAnd T1 T2. *)
-| TAndI_typed T1 T2 t i:
-    Γ ⊢ₜ t : T1, i →
-    Γ ⊢ₜ t : T2, i →
-    Γ ⊢ₜ t : TAnd T1 T2, i
-where "Γ ⊢ₜ e : T , i" := (typed Γ e T i)
+| TAndI_typed T1 T2 t:
+    Γ ⊢ₜ t : T1 →
+    Γ ⊢ₜ t : T2 →
+    Γ ⊢ₜ t : TAnd T1 T2
+where "Γ ⊢ₜ e : T " := (typed Γ e T)
 with dms_typed Γ: ty → dms → ty → Prop :=
 | dnil_typed V : Γ |ds V ⊢ [] : TTop
 (* This demands definitions and members to be defined in aligned lists. I think
@@ -94,13 +88,13 @@ with dm_typed Γ : ty → dm → ty → Prop :=
     TLater V :: Γ ⊢ₜ T, 1 <: U, 1 →
     Γ |d V ⊢ dtysyn T : TTMem l L U
 | dvl_typed V l v T:
-    V :: Γ ⊢ₜ tv v : T, 0 →
+    V :: Γ ⊢ₜ tv v : T →
     Γ |d V ⊢ dvl v : TVMem l T
 where "Γ |d V ⊢ d : T" := (dm_typed Γ V d T)
 with path_typed Γ: path → ty → nat → Prop :=
-| pv_typed v T i:
-    Γ ⊢ₜ tv v : T, i →
-    Γ ⊢ₚ pv v : T, i
+| pv_typed v T:
+    Γ ⊢ₜ tv v : T →
+    Γ ⊢ₚ pv v : T, 0
 | pv_dlater p T i:
     Γ ⊢ₚ p : TLater T, i →
     Γ ⊢ₚ p : T, S i

diff --git a/theories/Dot/typingExamples.v b/theories/Dot/typingExamples.v
@@ -67,11 +67,11 @@ Check (pv (var_vl 0) @; "A").
 Check (pself (pself (pv (var_vl 0)) "A") "B" @; "C").
 Check (var_vl 0 @ "A" @ "B" @; "C").
 
-Example ex0 e Γ T i:
-  Γ ⊢ₜ e : T, i →
-  Γ ⊢ₜ e : TTop, i.
+Example ex0 e Γ T:
+  Γ ⊢ₜ e : T →
+  Γ ⊢ₜ e : TTop.
 Proof.
-  (* eauto 2. *)
+  intro HeT. change e with (iterate tskip 0 e).
   econstructor. apply Top_stp. eassumption.
 Qed.
 
@@ -81,7 +81,7 @@ Qed.
 Local Notation "Γ ⊢ds ds : T"  := (dms_typed Γ ds T) (at level 74, ds, T at next level).
 
 Example ex1 Γ n T:
-  Γ ⊢ₜ tv (ν {@ val "a" = vnat n}) : μ {@ val "a" : TNat }, 0.
+  Γ ⊢ₜ tv (ν {@ val "a" = vnat n}) : μ {@ val "a" : TNat }.
 Proof.
   (* Help proof search: *)
   apply VObj_typed. (* Avoid trying TMuI_typed, that's slow. *)
@@ -107,7 +107,7 @@ Qed.
 
 Example ex2 Γ T:
   Γ ⊢ₜ tv (vobj [("A", dtysyn (TSel (pv (var_vl 0)) "B"))]) :
-    TMu (TAnd (TTMem "A" TBot TTop) TTop), 0.
+    TMu (TAnd (TTMem "A" TBot TTop) TTop).
 Proof.
   apply VObj_typed.
   econstructor => //=.
@@ -120,7 +120,7 @@ Definition F3 T :=
 
 Example ex3 Γ T:
   Γ ⊢ₜ tv (ν {@ type "A" = (F3 (TSel (pv (var_vl 0)) "A")) } ) :
-    F3 (F3 (TSel (pv (var_vl 0)) "A")), 0.
+    F3 (F3 (TSel (pv (var_vl 0)) "A")).
 Proof.
   apply VObj_typed. (* Avoid trying TMuI_typed, that's slow. *)
   econstructor => //=.
@@ -145,7 +145,7 @@ Print F4.
 (* XXX Not sure I got this right. *)
 Example ex4 Γ T:
   Γ ⊢ₜ tv (ν {@ val "a" = var_vl 0; type "B" = TSel (pv (var_vl 0)) "A" }) :
-    F4 (F4 (TSel (pv (var_vl 0)) "A")), 0.
+    F4 (F4 (TSel (pv (var_vl 0)) "A")).
 Abort.
 (*     (* TMu (TAnd (TAnd TTop (TTMem 0 ?))  *) *)
 (*     (*                      (TVMem 1 (TSel (pv (var_vl 0)) 0))). *) *)