From 466847bfcd112ea19541a36cd986ffa6de0d0545 Mon Sep 17 00:00:00 2001
From: "Paolo G. Giarrusso"
Date: Sat, 2 Feb 2019 17:37:35 +0100
Subject: [PATCH] Deindex syntactic typing judgment
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit
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.
---
theories/Dot/fundamental.v | 26 ++++++------
theories/Dot/lr_lemma.v | 24 +++++------
theories/Dot/typing.v | 76 ++++++++++++++++-------------------
theories/Dot/typingExamples.v | 16 ++++----
4 files changed, 68 insertions(+), 74 deletions(-)
diff --git a/theories/Dot/fundamental.v b/theories/Dot/fundamental.v
index cf26e8660..6188f0e0b 100644
--- 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
index d6c9321c0..3c102f6da 100644
--- 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
index 594ec6d70..24ae18bcd 100644
--- 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
index 9acf71845..a7b5849c2 100644
--- 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))). *) *)