add preconditions of expr_lc in eval; use coinductive quantification in T_TypeAbs

coq/_CoqProject

@@ -16,6 +16,7 @@ typing/morph.v
 typing/typing.v
 lemmas/subst_lemmas.v
 lemmas/typing_weakening.v
+lemmas/typing_regular.v
 soundness/translate_morph.v
 
 

coq/lemmas/typing_regular.v

@@ -0,0 +1,46 @@
+From Coq Require Import Lists.List.
+Require Import Atom.
+Require Import Environment.
+Require Import Metatheory.
+Require Import debruijn.
+Require Import subtype.
+Require Import env.
+Require Import morph.
+Require Import typing.
+
+
+Lemma type_lc_sub : forall τ1 τ2,
+  type_lc τ1 ->
+  τ1 :<= τ2 ->
+  type_lc τ2
+.
+Proof.
+  intros.
+Admitted.
+
+Lemma type_morph_lc_inv : forall τ1 τ2,
+  type_lc (ty_morph τ1 τ2) ->
+  type_lc τ1 /\ type_lc τ2
+.
+Proof.
+  intros.
+  inversion H.
+  auto.
+Qed.
+
+Lemma typing_regular_expr_lc : forall Γ e τ,
+  (Γ |- e \is τ) ->
+  expr_lc e.
+Proof.
+  intros Γ e τ H.
+  induction H; eauto.
+  - apply Elc_Var.
+  - apply Elc_Let with (L:=L).
+    apply IHtyping.
+Admitted.
+
+Lemma typing_regular_type_lc : forall Γ e τ,
+  (Γ |- e \is τ) ->
+  type_lc τ.
+Proof.
+Admitted.

coq/soundness/translate_morph.v

@@ -8,6 +8,7 @@ Require Import env.
 Require Import morph.
 Require Import subst_lemmas.
 Require Import typing.
+Require Import typing_regular.
 Require Import typing_weakening.
 
 
@@ -35,18 +36,52 @@ Proof.
 *)
 Admitted.
 
+Lemma type_lc_spec_inv : forall τ,
+  type_lc [< [τ] >] ->
+  type_lc τ
+.
+Proof.
+Admitted.
+
+Lemma type_lc_ladder_inv2 : forall σ τ,
+  type_lc [< σ ~ τ >] ->
+  type_lc τ
+.
+Proof.
+Admitted.
+
+Lemma morph_regular_lc : forall Γ τ τ',
+  env_wf Γ ->
+  type_lc τ ->
+  (Γ |- τ ~~> τ') ->
+  type_lc τ'
+.
+Proof.
+  intros.
+  induction H1.
+  - apply type_lc_sub with (τ1:=τ).
+    assumption.
+    assumption.
+Admitted.
+
+Lemma morph_path_inv : forall Γ τ τ' m,
+  (Γ |- [[ τ ~~> τ' ]] = m) ->
+  (Γ |- τ ~~> τ')
+.
+Proof.
+Admitted.
+
 (*
  * translated morphism path is locally closed
  *)
-Lemma morphism_path_lc : forall Γ τ τ' m,
+Lemma morph_path_lc : forall Γ τ τ' m,
   type_lc τ ->
-  type_lc τ' ->
   env_wf Γ ->
   (Γ |- [[ τ ~~> τ' ]] = m) ->
   expr_lc m
 .
 Proof.
-  intros Γ τ τ' m Wfτ1 Wfτ2 WfEnv H.
+  intros Γ τ τ' m Wfτ WfEnv H.
   induction H.
 
   (* Subtype / Identity *)
@@ -56,6 +91,8 @@ Proof.
     unfold expr_open.
     simpl.
     apply Elc_Descend.
+    apply type_lc_sub with (τ1:=τ).
+    assumption.
     assumption.
     apply Elc_Var.
 
@@ -66,22 +103,20 @@ Proof.
     unfold expr_open.
     simpl.
     apply Elc_Ascend.
-    inversion Wfτ1; assumption.
+    inversion Wfτ; assumption.
     apply Elc_App.
     rewrite expr_open_lc.
 
     apply IHtranslate_morphism_path.
-    inversion Wfτ1; assumption.
-    inversion Wfτ2; assumption.
-    assumption.
+    inversion Wfτ; assumption.
+    inversion Wfτ; assumption.
 
     apply IHtranslate_morphism_path.
-    inversion Wfτ1; assumption.
-    inversion Wfτ2; assumption.
-    assumption.
+    inversion Wfτ; assumption.
+    inversion Wfτ; assumption.
 
     apply Elc_Descend, Elc_Var.
-    inversion Wfτ1; assumption.
+    inversion Wfτ; assumption.
 
   (* Single Morphism *)
   - apply Elc_Var.
@@ -95,16 +130,35 @@ Proof.
     apply Elc_App.
     rewrite expr_open_lc.
     apply IHtranslate_morphism_path2.
-    1-3:assumption.
+
+
+    apply morph_regular_lc with (Γ:=Γ) (τ:=τ).
+    assumption. assumption.
+    apply morph_path_inv with (m:=m1),  H.
+    assumption.
+
     apply IHtranslate_morphism_path2.
-    1-3:assumption.
+
+    apply morph_regular_lc with (Γ:=Γ) (τ:=τ).
+    assumption. assumption.
+    apply morph_path_inv with (m:=m1),  H.
+    assumption.
+
 
     apply Elc_App.
     rewrite expr_open_lc.
     apply IHtranslate_morphism_path1.
-    1-3:assumption.
+
+    apply morph_regular_lc with (Γ:=Γ) (τ:=τ).
+    assumption. assumption.
+    apply id_morphism_path.
+    assumption.
+    assumption.
+
     apply IHtranslate_morphism_path1.
-    1-3:assumption.
+    assumption.
+    assumption.
+
     apply Elc_Var.
 
   (* Map *)
@@ -118,17 +172,21 @@ Proof.
     apply Elc_TypApp.
     apply Elc_TypApp.
     apply Elc_Var.
-    inversion Wfτ1; assumption.
-    inversion Wfτ2; assumption.
 
-    rewrite expr_open_lc.
-    apply IHtranslate_morphism_path.
-    inversion Wfτ1; assumption.
-    inversion Wfτ2; assumption.
+    apply type_lc_spec_inv; assumption.
+    apply morph_path_inv in H.
+    apply morph_regular_lc with (Γ:=Γ) (τ:=τ).
     assumption.
+    apply type_lc_spec_inv; assumption.
+    assumption.
+    rewrite expr_open_lc.
+
     apply IHtranslate_morphism_path.
-    inversion Wfτ1; assumption.
-    inversion Wfτ2; assumption.
+    apply type_lc_spec_inv; assumption.
+    assumption.
+
+    apply IHtranslate_morphism_path.
+    apply type_lc_spec_inv; assumption.
     assumption.
 Qed.
 
@@ -137,13 +195,12 @@ Qed.
  *)
 Lemma morphism_path_correct : forall Γ τ τ' m,
   type_lc τ ->
-  type_lc τ' ->
   env_wf Γ ->
   (Γ |- [[ τ ~~> τ' ]] = m) ->
   (Γ |- m \is [< τ ->morph τ' >])
 .
 Proof.
-  intros Γ τ τ' m Lcτ1 Lcτ2 Ok H.
+  intros Γ τ τ' m Lcτ WfEnv H.
   induction H.
 
   (* Sub *)
@@ -153,7 +210,8 @@ Proof.
     simpl.
     apply T_Descend with (τ:=τ).
     apply T_Var.
-    2:assumption.
+    apply env_wf_type.
+    1-3,5:assumption.
     simpl_env.
     apply binds_head, binds_singleton.
 
@@ -167,6 +225,7 @@ Proof.
     2: {
       apply T_Descend with (τ:=[< σ ~ τ >]).
       apply T_Var.
+      apply env_wf_type; assumption.
       simpl_env.
       unfold binds. simpl.
       destruct (x==x).
@@ -177,20 +236,27 @@ Proof.
       apply equiv.TEq_Refl.
     }
 
-    inversion Lcτ1.
-    inversion Lcτ2.
-    subst.
-    apply morphism_path_lc in H0.
-
+    inversion Lcτ; subst.
     rewrite expr_open_lc.
     apply typing_weakening with (Γ':=(x,[< σ ~ τ >])::[]).
     apply T_MorphFun.
     apply IHtranslate_morphism_path.
-    4: apply env_wf_type.
+    apply type_lc_ladder_inv2 with (σ:=σ); assumption; assumption.
+    assumption.
+    apply env_wf_type.
+    assumption.
+    assumption.
+    assumption.
+    apply morph_path_lc with (Γ:=Γ) (τ:=τ) (τ':=τ').
+    assumption.
+    assumption.
+    assumption.
+    apply type_lc_ladder_inv2 with (σ:=σ).
     all: assumption.
 
   (* Single *)
   - apply T_Var.
+    assumption.
     apply H.
 
   (* Chain *)
@@ -205,24 +271,38 @@ Proof.
       rewrite expr_open_lc.
       simpl_env; apply typing_weakening.
       apply IHtranslate_morphism_path2.
+
+      apply morph_path_inv in H.
+      apply morph_regular_lc with (Γ:=Γ) (τ:=τ).
       1-3: assumption.
+
+      assumption.
       apply env_wf_type.
       1-3: assumption.
-      apply morphism_path_lc with (Γ:=Γ) (τ:=τ') (τ':=τ'').
-      1-4: assumption.
+      apply morph_path_lc with (Γ:=Γ) (τ:=τ') (τ':=τ'').
+      2-3: assumption.
+      apply morph_path_inv in H.
+      apply morph_regular_lc with (Γ:=Γ) (τ:=τ).
+      all: assumption.
 
     * apply T_App with (σ':=τ) (σ:=τ) (τ:=τ').
       rewrite expr_open_lc.
       apply typing_weakening with (Γ':=(x,τ)::[]).
       apply T_MorphFun.
       apply IHtranslate_morphism_path1.
-      4: apply env_wf_type.
-      1-6: assumption.
-      apply morphism_path_lc with (Γ:=Γ) (τ:=τ) (τ':=τ').
-      1-4: assumption.
+      3: apply env_wf_type.
+      1-5: assumption.
+      apply morph_path_lc with (Γ:=Γ) (τ:=τ) (τ':=τ').
+      1-3: assumption.
       apply T_Var.
+      apply env_wf_type; assumption.
       2: apply id_morphism_path.
       simpl_env; apply binds_head, binds_singleton.
+      assumption.
+
+    * apply morph_path_inv in H.
+      apply morph_regular_lc with (Γ:=Γ) (τ:=τ).
+      all: assumption.
 
   (* Map Sequence *)
   - apply T_MorphAbs with (L:=dom Γ).
@@ -239,14 +319,24 @@ Proof.
     simpl_env; apply typing_weakening.
     apply T_MorphFun.
     apply IHtranslate_morphism_path.
-    3: assumption.
-    3: apply env_wf_type; assumption.
-    inversion Lcτ1; assumption.
-    inversion Lcτ2; assumption.
-    apply morphism_path_lc with (Γ:=Γ) (τ:=τ) (τ':=τ').
-    inversion Lcτ1; assumption.
-    inversion Lcτ2; assumption.
+    2: assumption.
+    2: apply env_wf_type; assumption.
+
+    inversion Lcτ; assumption.
+    apply morph_path_lc with (Γ:=Γ) (τ:=τ) (τ':=τ').
+    inversion Lcτ; assumption.
     1-2: assumption.
+    apply Tlc_Func.
+    apply type_lc_spec_inv; assumption.
+
+    apply morph_path_inv in H.
+    apply morph_regular_lc in H.
+    assumption.
+    assumption.
+    apply type_lc_spec_inv; assumption.
+
     apply T_Var.
+    apply env_wf_type; assumption.
     simpl_env; apply binds_head, binds_singleton.
+    assumption.
 Qed.

coq/terms/eval.v

@@ -10,9 +10,11 @@ Open Scope ladder_expr_scope.
 
 Inductive is_value : expr_DeBruijn -> Prop :=
   | V_TAbs : forall e,
+    expr_lc [{ Λ e }] ->
     is_value [{ Λ e }]
 
   | V_Abs : forall σ e,
+    expr_lc [{ λ σ ↦ e }] ->
     is_value [{ λ σ ↦ e }]
 
   | V_Morph : forall σ e,
@@ -32,6 +34,7 @@ Reserved Notation " s '-->eval' t " (at level 40).
 
 Inductive eval : expr_DeBruijn -> expr_DeBruijn -> Prop :=
   | E_App1 : forall e1 e1' e2,
+    (expr_lc e2) ->
     e1 -->eval e1' ->
     [{ e1 e2 }] -->eval [{ e1' e2 }]
 
@@ -41,27 +44,26 @@ Inductive eval : expr_DeBruijn -> expr_DeBruijn -> Prop :=
     [{ v1 e2 }] -->eval [{ v1 e2' }]
 
   | E_TypApp : forall e e',
+    expr_lc [{ Λ e }] ->
     e -->eval e' ->
     [{ Λ e }] -->eval [{ Λ e' }]
 
   | E_TypAppLam : forall e τ,
+    expr_lc [{ (Λ e ) }] ->
     [{ (Λ e) # τ }] -->eval (expr_open_type τ e)
 
   | E_AppLam : forall τ e a,
+    expr_lc [{ (λ τ ↦ e) }] ->
     [{ (λ τ ↦ e) a }] -->eval (expr_open a e)
 
   | E_AppMorph : forall τ e a,
+    expr_lc [{ (λ τ ↦morph e) }] ->
     [{ (λ τ ↦morph e) a }] -->eval (expr_open a e)
 
   | E_Let : forall e a,
+    expr_lc [{ let a in e }] ->
     [{ let a in e }] -->eval (expr_open a e)
 
-  | E_StripAscend : forall τ e,
-    [{ e as τ }] -->eval e
-
-  | E_StripDescend : forall τ e,
-    [{ e des τ }] -->eval e
-
   | E_Ascend : forall τ e e',
     (e -->eval e') ->
     [{ e as τ }] -->eval [{ e' as τ }]

coq/typing/morph.v

@@ -16,6 +16,7 @@ Reserved Notation "Γ '|-' σ '~~>' τ" (at level 101).
 
 Inductive morphism_path : env -> type_DeBruijn -> type_DeBruijn -> Prop :=
   | M_Sub : forall Γ τ τ',
+    type_lc τ ->
     τ :<= τ' ->
     (Γ |- τ ~~> τ')
 
@@ -38,10 +39,14 @@ Inductive morphism_path : env -> type_DeBruijn -> type_DeBruijn -> Prop :=
 
 where "Γ '|-' s '~~>' t" := (morphism_path Γ s t).
 
-Lemma id_morphism_path : forall Γ τ, Γ |- τ ~~> τ.
+Create HintDb morph_path_hints.
+Hint Constructors morphism_path :morph_path_hints.
+
+Lemma id_morphism_path : forall Γ τ,
+  type_lc τ ->
+  Γ |- τ ~~> τ.
 Proof.
-  intros.
-  apply M_Sub, TSubRepr_Refl, TEq_Refl.
+  eauto with morph_path_hints subtype_hints.
 Qed.
 
 
@@ -68,7 +73,6 @@ Inductive translate_morphism_path : env -> type_DeBruijn -> type_DeBruijn -> exp
     (Γ |- [[ τ ~~> τ' ]] = [{ $h }])
 
   | Translate_Chain : forall Γ τ τ' τ'' m1 m2,
-    (type_lc τ') ->
     (Γ |- [[ τ ~~> τ' ]] = m1) ->
     (Γ |- [[ τ' ~~> τ'' ]] = m2) ->
     (Γ |- [[ τ ~~> τ'' ]] = [{ λ τ ↦morph (m2 (m1 %0)) }])

coq/typing/subtype.v

@@ -37,6 +37,7 @@ where "s '~<=' t" := (is_conv_subtype s t).
 
 Hint Constructors is_repr_subtype :subtype_hints.
 Hint Constructors is_conv_subtype :subtype_hints.
+Hint Constructors type_eq :subtype_hints.
 
 (* Every Representational Subtype is a Convertible Subtype *)
 

coq/typing/typing.v

@@ -13,6 +13,7 @@ Open Scope ladder_expr_scope.
 Reserved Notation "Γ '|-' x '\is' X"  (at level 101).
 Inductive typing : env -> expr_DeBruijn -> type_DeBruijn -> Prop :=
   | T_Var : forall Γ x τ,
+    (env_wf Γ) ->
     (binds x τ Γ) ->
     (Γ |- [{ $x }] \is τ)
 
@@ -22,8 +23,9 @@ Inductive typing : env -> expr_DeBruijn -> type_DeBruijn -> Prop :=
       ( (x,σ)::Γ |- (expr_open (ex_fvar x) t) \is τ)) ->
     (Γ |- [{ let s in t }] \is τ)
 
-  | T_TypeAbs : forall Γ e τ,
-    (Γ |- e \is τ) ->
+  | T_TypeAbs : forall Γ L e τ,
+    (forall x : atom, x `notin` L ->
+      ( Γ |- (expr_open_type (ty_fvar x) e) \is τ)) ->
     (Γ |- [{ Λ e }] \is [< ∀ τ >])
 
   | T_TypeApp : forall Γ e σ τ,
@@ -67,6 +69,9 @@ Inductive typing : env -> expr_DeBruijn -> type_DeBruijn -> Prop :=
 where "Γ '|-' x '\is' τ" := (typing Γ x τ).
 
 
+Create HintDb typing_hints.
+Hint Constructors typing :typing_hints.
+
 
 Reserved Notation "Γ '|-' '[[' e \is τ ']]' '=' f"  (at level 101).
 
@@ -80,14 +85,16 @@ Inductive translate_typing : env -> expr_DeBruijn -> type_DeBruijn -> expr_DeBru
     (Γ |- e \is σ) ->
     (forall x : atom, x `notin` L ->
       ( (x,σ)::Γ |- (expr_open (ex_fvar x) t) \is τ) ->
-      ( (x,σ)::Γ |- [[ t \is τ ]] = t' )
+      ( (x,σ)::Γ |- [[ (expr_open (ex_fvar x) t) \is τ ]] = (expr_open (ex_fvar x) t') )
     ) ->
     (Γ |- [[ e \is σ ]] = e') ->
     (Γ |- [[  [{ let e in t }] \is τ  ]] = [{ let e' in t' }])
 
-  | Expand_TypeAbs : forall Γ e e' τ,
-    (Γ |- e \is τ) ->
-    (Γ |- [[ e \is τ ]] = e') ->
+  | Expand_TypeAbs : forall Γ L e e' τ,
+    (forall x : atom, x `notin` L ->
+      (Γ |- (expr_open_type (ty_fvar x) e) \is τ) ->
+      (Γ |- [[ (expr_open_type (ty_fvar x) e) \is τ ]] = (expr_open_type (ty_fvar x) e'))
+    ) ->
     (Γ |- [[ [{ Λ e }] \is [< ∀ τ >] ]] = [{ Λ e' }])
 
   | Expand_TypeApp : forall Γ e e' σ τ,
@@ -99,7 +106,7 @@ Inductive translate_typing : env -> expr_DeBruijn -> type_DeBruijn -> expr_DeBru
     (Γ |- [{ λ σ ↦ e }] \is [< σ -> τ >]) ->
     (forall x : atom, x `notin` L ->
       ( (x,σ)::Γ |- (expr_open (ex_fvar x) e) \is τ) ->
-      ( (x,σ)::Γ |- [[ e \is τ ]] = e' )
+      ( (x,σ)::Γ |- [[ (expr_open (ex_fvar x) e) \is τ ]] = (expr_open (ex_fvar x) e') )
     ) ->
     (Γ |- [[ [{ λ σ ↦ e }] \is [< σ -> τ >] ]] = [{ λ σ ↦ e' }])
 
@@ -107,7 +114,7 @@ Inductive translate_typing : env -> expr_DeBruijn -> type_DeBruijn -> expr_DeBru
     (Γ |- [{ λ σ ↦ e }] \is [< σ -> τ >]) ->
     (forall x : atom, x `notin` L ->
       ( (x,σ)::Γ |- (expr_open (ex_fvar x) e) \is τ) ->
-      ( (x,σ)::Γ |- [[ e \is τ ]] = e' )
+      ( (x,σ)::Γ |- [[ (expr_open (ex_fvar x) e) \is τ ]] = (expr_open (ex_fvar x) e') )
     ) ->
     (Γ |- [[ [{ λ σ ↦morph e }] \is [< σ ->morph τ >] ]] = [{ λ σ ↦morph e' }])