wip on preservation proof

coq/soundness.v

@@ -16,40 +16,405 @@ Include Typing.
 
 Module Soundness.
 
+
+Lemma typing_weakening : forall Γ e τ x σ,
+  (Γ |- e \is τ) ->
+  ((ctx_assign x σ Γ) |- e \is τ)
+.
+Proof.
+  intros.
+  induction H.
+
+  apply T_Var.
+  apply C_shuffle.
+  apply H.
+  
+  apply T_Let with (σ:=σ0).
+  apply IHexpr_type1.
+  admit.
+
+Admitted.
+
+
+Lemma morphism_path_solves_type : forall Γ τ τ' m,
+  (translate_morphism_path Γ τ τ' m) ->
+  Γ |- m \is (type_morph τ τ')
+.
+Proof.
+  intros.
+  induction H.
+
+  (* Sub *)
+  apply T_MorphAbs.
+  apply T_DescendImplicit with (τ:=τ).
+  apply T_Var.
+  apply C_take.
+  apply H.
+
+  (* Lift *)
+  apply T_MorphAbs.
+  apply T_Ascend with (τ:=τ').
+  apply T_App with (σ':=τ) (σ:=τ).
+  apply T_MorphFun.
+  apply typing_weakening.
+  apply IHtranslate_morphism_path.
+  apply T_Descend with (τ:=(type_ladder σ τ)).
+  apply T_Var.
+  apply C_take.
+  apply TSubRepr_Ladder, TSubRepr_Refl, TEq_Refl.
+  apply M_Sub, TSubRepr_Refl, TEq_Refl.
+  apply TSubRepr_Ladder, TSubRepr_Refl, TEq_Refl.
+
+  (* Single *)
+  apply T_Var.
+  apply H.
+
+  (* Chain *)
+  apply T_MorphAbs.
+  apply T_App with (σ':=τ') (σ:=τ') (τ:=τ'').
+  apply T_MorphFun.
+  apply typing_weakening.
+  apply IHtranslate_morphism_path2.
+  
+  apply T_App with (σ':=τ) (σ:=τ) (τ:=τ').
+  apply T_MorphFun.
+  apply typing_weakening.
+  apply IHtranslate_morphism_path1.
+
+  apply T_Var.
+  apply C_take.
+  apply M_Sub, TSubRepr_Refl, TEq_Refl.
+  apply M_Sub, TSubRepr_Refl, TEq_Refl.
+
+  (* Map Sequence *)
+  apply T_MorphAbs.
+  apply T_App with (σ':=(type_spec (type_id "Seq") τ)) (σ:=(type_spec (type_id "Seq") τ)).
+  apply T_App with (σ':=(type_fun τ τ')) (σ:=(type_fun τ τ')).
+
+  admit.
+
+  apply T_MorphFun.
+  apply typing_weakening.
+  apply IHtranslate_morphism_path.
+  apply M_Sub, TSubRepr_Refl, TEq_Refl.
+
+  apply T_Var.
+  apply C_take.
+  apply M_Sub, TSubRepr_Refl, TEq_Refl.
+Admitted.
+
+(* reduction step preserves well-typedness *)
+Lemma preservation : forall Γ e e' τ,
+  ~(is_value e) ->
+  (Γ |- e \is τ) ->
+  (e -->β e') ->
+  (Γ |- e' \is τ)
+.
+Proof.
+  intros.
+  induction e.
+
+  (* `e` is Variable *)
+  contradict H.
+  apply V_Abs, VAbs_Var.
+
+  (* `e` is Type-Abstraction *)
+  contradict H.
+  apply V_Abs, VAbs_TypAbs.
+
+  (* `e` is Type-Application *)
+  admit.
+
+  (* `e` is Abstraction *)
+  contradict H.
+  apply V_Abs, VAbs_Abs.
+
+  (* `e` is morphism *)
+  contradict H.
+  apply V_Abs, VAbs_Morph.
+
+  (* `e` is Application *)
+  admit.
+
+  (* `e` is Let-Binding *)
+  admit.
+
+  (* `e` is Ascension *)
+  admit.
+
+  (* `e` is Descension *)
+  admit.
+Admitted.
+
+(* translation of expression preserves typing *)
+Lemma translation_preservation : forall Γ e e' τ,
+  (Γ |- e \is τ) ->
+  (translate_typing Γ e τ e') ->
+  (Γ |- e' \is τ)
+.
+Proof.
+  intros.  
+  induction H0.
+
+  (* e is Variable *)
+  apply H.
+
+  (* e is Let-Binding *)
+  apply T_Let with (τ:=τ) (σ:=σ).
+  apply IHtranslate_typing1.
+  apply H0.
+  apply IHtranslate_typing2.
+  apply H1.
+
+  (* e is Type-Abstraction *)
+  apply T_TypeAbs.
+  apply IHtranslate_typing.
+  apply H0.
+
+  (* e is Type-Application *)
+  admit.
+
+  (* e is Abstraction *)
+  apply T_Abs.
+  apply IHtranslate_typing.
+  apply H0.
+
+  (* e is Morphism-Abstraction *)
+  apply T_MorphAbs.
+  apply IHtranslate_typing.
+  apply H0.
+
+  (* e is Application *)
+  apply T_App with (σ':=σ) (σ:=σ) (τ:=τ).
+  apply IHtranslate_typing1.
+  apply H0.
+
+  induction H3.
+
+    (* Repr-Subtype *)
+    apply T_App with (σ':=τ0) (σ:=τ0) (τ:=τ').
+    apply T_MorphFun.
+    apply T_MorphAbs.
+    apply T_DescendImplicit with (τ:=τ0).
+    apply T_Var.
+    apply C_take.
+    apply H3.
+
+    apply T_DescendImplicit with (τ:=τ0).
+    apply IHtranslate_typing2.
+    apply H1.
+    apply TSubRepr_Refl, TEq_Refl.
+    apply M_Sub, TSubRepr_Refl, TEq_Refl.
+
+    (* Lifted Morphism *)
+    apply T_App with (σ':=(type_ladder σ τ0)) (σ:=(type_ladder σ τ0)) (τ:=(type_ladder σ τ')).
+    apply T_MorphFun.
+    apply T_MorphAbs.
+    apply T_Ascend with (τ:=τ').
+    apply T_App with (σ':=τ0) (σ:=τ0) (τ:=τ').
+    apply T_MorphFun.
+    apply typing_weakening.
+    apply morphism_path_solves_type.
+    apply H4.
+    
+    apply T_Descend with (τ:=(type_ladder σ τ0)).
+    apply T_Var.
+    apply C_take.
+
+    apply TSubRepr_Ladder, TSubRepr_Refl, TEq_Refl.
+    apply M_Sub, TSubRepr_Refl, TEq_Refl.
+    apply TSubRepr_Ladder, TSubRepr_Refl, TEq_Refl.
+    apply IHtranslate_typing2.
+    apply H1.
+
+    apply M_Sub, TSubRepr_Refl, TEq_Refl.
+
+    (* argument coecrion is single function variable *)
+    apply T_App with (σ':= τ0) (σ:=τ0).
+    apply T_MorphFun.
+    apply T_Var.
+    apply H3.
+    apply IHtranslate_typing2.
+    apply H1.
+    (* lemma: every context implies identity morphism *)
+    apply M_Sub, TSubRepr_Refl, TEq_Refl.
+
+    (* argument coecrion is chain of coercions *)
+    apply T_App with (σ':=τ0) (σ:=τ0).
+    apply T_MorphFun.
+    apply T_MorphAbs.
+    apply T_App with (σ':=τ') (σ:=τ').
+    apply T_MorphFun.
+    apply typing_weakening.
+    apply morphism_path_solves_type.
+    apply H3_0.
+    apply T_App with (σ':=τ0) (σ:=τ0).
+    apply T_MorphFun.
+    apply typing_weakening.
+    apply morphism_path_solves_type.
+    apply H3_.
+    apply T_Var.
+    apply C_take.
+    (* lemma: every context implies identity morphism *)
+    apply M_Sub, TSubRepr_Refl, TEq_Refl.
+    (* lemma: every context implies identity morphism *)
+    apply M_Sub, TSubRepr_Refl, TEq_Refl.
+    apply IHtranslate_typing2.
+    apply H1.
+    (* lemma: every context implies identity morphism *)
+    apply M_Sub, TSubRepr_Refl, TEq_Refl.
+
+    (* argument coercion is is map *)
+(*
+    apply T_App with (σ':=(type_spec (type_id "Seq") τ0)) (σ:=(type_spec (type_id "Seq") τ0)).
+    apply T_MorphFun.
+    apply T_MorphAbs.
+    apply T_App with (σ':=(type_spec (type_id "Seq") τ0)) (σ:=(type_spec (type_id "Seq") τ0)).
+    apply T_App with (σ':=(type_fun τ0 τ')) (σ:=(type_fun τ0 τ')).
+    apply T_TypeApp with
+      (α:="T2"%string)
+      (e:=(expr_ty_app (expr_var "map") τ0))
+      (τ:=(type_fun
+            (type_fun τ0 τ')
+            (type_fun
+              (type_spec (type_id "Seq") τ0)
+              (type_spec (type_id "Seq") τ')))).
+
+    apply T_TypeApp with
+      (α:="T1"%string)
+      (e:=(expr_var "map"))
+      (τ:=(type_univ "T2"
+          (type_fun
+            (type_fun τ0 τ')
+            (type_fun
+              (type_spec (type_id "Seq") (type_var "T1"))
+              (type_spec (type_id "Seq") (type_var "T2")))))).
+
+    apply T_Var.
+    admit.
+
+    apply TSubst_VarReplace.
+    apply TSubst_UnivReplace.
+*)
+    admit.
+
+    (* argument coercion *)
+    apply M_Sub, TSubRepr_Refl, TEq_Refl.
+
+  (* end case `e application` *)
+
+  (* e is Morphism *)
+  apply T_MorphFun.
+  apply IHtranslate_typing.
+  apply H0.
+
+  (* e is Ascension *)
+  apply T_Ascend with (τ:=τ).
+  apply IHtranslate_typing.
+  apply H0.
+  apply H1.
+
+  (* e is Desecension *)
+  apply T_DescendImplicit with (τ:=τ).
+  apply IHtranslate_typing.
+  apply H0.
+  apply H1.
+Admitted.
+
 (* e is stuck when it is neither a value, nor can it be reduced *)
 Definition is_stuck (e:expr_term) : Prop :=
   ~(is_value e) ->
   ~(exists e', e -->β e')
 .
 
-(* every well typed term is not stuck *)
+(* the translation any well typed term is not stuck *)
 Lemma progress :
-  forall (e:expr_term),
+  forall Γ e τ e',
-  (is_well_typed e) -> ~(is_stuck e)
+  (Γ |- e \is τ) ->
+  (translate_typing Γ e τ e') ->
+  ~(is_stuck e')
 .
 Proof.
-  
 Admitted.
 
-(* reduction step preserves well-typedness *)
+(* every well-typed expression is translated,
-Lemma preservation :
+ * such that it be reduced to a value
+ *)
+Theorem soundness :
   forall Γ e e' τ,
   (Γ |- e \is τ) ->
-  (e -->β e') ->
+  (translate_typing Γ e τ e') ->
-  (Γ |- e' \is τ)
+  (exists v, (e' -->β* v) /\ (is_value v) /\ (Γ |- v \is τ))
-.
-Proof.
-Admitted.
-
-(* every well-typed expression can be reduced to a value *)
-Theorem soundness :
-  forall (e:expr_term),
-  (is_well_typed e) ->
-  (exists e', e -->β* e' /\ (is_value e'))
 .
 Proof.
   intros.
 
+  (* `e` is Variable *)
+  induction H0.
+  exists (expr_var x).
+  split. apply Multi_Refl.
+  split. apply V_Abs,VAbs_Var.
+  apply H.
+
+  (* `e` is Let-Binding *)
+  exists (expr_subst x e' t').
+  split.
+  apply Multi_Step with (y:=(expr_subst x e' t')).
+  apply E_Let with (x:=x) (a:=e') (e:=t').
+  apply Multi_Refl.
+(*
+  split.
+  unfold expr_subst.
+  induction t'.
+  
+  exists (expr_subst x e' (expr_var s)).
+  split.
+  unfold expr_subst.
+  apply E_Let.
+  *)
+  admit.
+
+  (* `e` is Type-Abstraction *)
+  exists (expr_ty_abs α e').
+  split.
+  apply Multi_Refl.
+  split.
+  apply V_Abs, VAbs_TypAbs.
+  apply T_TypeAbs.
+  apply translation_preservation with (e:=e).
+  apply H0.
+  apply H1.
+
+  (* `e` is Type-Application *)
+  admit.
+
+  (* `e`is Abstraction *)
+  exists (expr_abs x σ e').
+  split. apply Multi_Refl.
+  split. apply V_Abs, VAbs_Abs.
+  apply T_Abs.
+  apply translation_preservation with (e:=e).
+  apply H0.
+  apply H2.
+
+  (* `e` is Morphism Abstraction *)
+  exists (expr_morph x σ e').
+  split. apply Multi_Refl.
+  split. apply V_Abs, VAbs_Morph.
+  apply T_MorphAbs.
+  apply translation_preservation with (e:=e).
+  apply H0.
+  apply H2.
+
+  (* `e` is Application *)
+  admit.
+  admit.
+
+  (* `e` is Ascension *)
+  admit.
+
+  (* `e` is Descension *)
+  admit.
 Admitted.
 
 End Soundness.

coq/terms.v

@@ -30,45 +30,34 @@ Inductive expr_term : Type :=
   | expr_descend : type_term -> expr_term -> expr_term
 .
 
-(* TODO
-
-Inductive type_DeBruijn : Type :=
-  | id : nat -> type_DeBruijn
-  | var : nat -> type_DeBruijn
-  | fun : type_DeBruijn -> type_DeBruijn -> type_DeBruijn
-  | univ : type_DeBruijn -> type_DeBruijn
-  | spec : type_DeBruijn -> type_DeBruijn -> type_DeBruijn
-  | morph : type_DeBruijn -> type_DeBruijn -> type_DeBruijn
-  | ladder : type_DeBruijn -> type_DeBruijn -> type_DeBruijn
-
-Inductive expr_DeBruijn : Type :=
-  | var : nat -> expr_DeBruijn
-  | ty_abs : expr_DeBruijn -> expr_DeBruijn
-  | ty_app : expr_DeBruijn -> type_DeBruijn -> expr_Debruijn
-  | abs   : type_DeBruijn -> expr_DeBruijn -> expr_DeBruijn
-  | morph : type_DeBruijn -> expr_DeBruijn -> expr_Debruijn
-  | app : expr_DeBruijn -> expr_DeBruijn -> expr_Debruijn
-  | let : type_DeBruijn -> expr_DeBruijn -> expr_Debruijn -> expr_Debruijn
-  | ascend : type_DeBruijn -> expr_DeBruijn -> expr_DeBruijn
-  | descend : type_DeBruijn -> expr_DeBruijn -> expr_DeBruijn
-.
-*)
-
-
-
 (* values *)
-Inductive is_value : expr_term -> Prop :=
+Inductive is_abs_value : expr_term -> Prop :=
-  | V_Abs : forall x τ e,
+  | VAbs_Var : forall x,
-    (is_value (expr_abs x τ e))
+    (is_abs_value (expr_var x))
 
-  | V_TypAbs : forall τ e,
+  | VAbs_Abs : forall x τ e,
-    (is_value (expr_ty_abs τ e))
+    (is_abs_value (expr_abs x τ e))
+
+  | VAbs_Morph : forall x τ e,
+    (is_abs_value (expr_morph x τ e))
+
+  | VAbs_TypAbs : forall τ e,
+    (is_abs_value (expr_ty_abs τ e))
+.
+
+Inductive is_value : expr_term -> Prop :=
+  | V_Abs : forall e,
+    (is_abs_value e) ->
+    (is_value e)
 
   | V_Ascend : forall τ e,
-    (is_value e) ->
+    (is_abs_value e) ->
     (is_value (expr_ascend τ e))
-.
 
+  | V_Descend : forall τ e,
+    (is_abs_value e) ->
+    (is_value (expr_descend τ e))
+.
 
 Declare Scope ladder_type_scope.
 Declare Scope ladder_expr_scope.