coq: add preliminary preservation proof

coq/soundness/preservation.v

@@ -0,0 +1,246 @@
+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 subst_lemmas.
+Require Import typing.
+Require Import eval.
+Require Import typing_weakening.
+Require Import typing_inv.
+Require Import translate_morph.
+Require Import translate_expr.
+Require Import transl_inv.
+
+Lemma typing_subst : forall Γ e τ z σ u,
+  (((z,σ)::Γ) |- e \is τ) ->
+  (Γ |- u \is σ) ->
+  (Γ |- ([z ~ee~> u] e) \is τ)
+.
+Proof.
+  intros E e u S T z H J.
+  rewrite <- (nil_concat _ E).
+Admitted.
+  (*
+  eapply typing_subst_strengthened.
+    rewrite nil_concat. apply H.
+    apply J.
+Qed.
+*)
+
+
+Lemma subst_intro : forall (x : atom) u e,
+  x `notin` (expr_fv e) ->
+  expr_lc u ->
+  expr_open u e = [x ~ee~> u](expr_open (ex_fvar x) e).
+Proof.
+  intros x u e H J.
+  unfold expr_open.
+  (*
+  rewrite subst_open_rec; auto.
+  simpl.
+  destruct (x == x).
+  Case "x = x".
+    rewrite subst_fresh; auto.
+  Case "x <> x".
+    destruct n; auto.
+Qed.
+*)
+Admitted.
+
+Lemma typing_subst_type : forall Γ x σ e τ,
+  (Γ |- e \is τ) ->
+  (Γ |- ([x ~et~> σ] e) \is τ)
+.
+Proof.
+Admitted.
+
+Lemma subst_intro_type : forall (x : atom) τ e,
+  x `notin` (expr_fv_type e) ->
+  type_lc τ ->
+  expr_open_type τ e = [x ~et~> τ](expr_open_type (ty_fvar x) e).
+Proof.
+  intros x u e H J.
+  unfold expr_open.
+Admitted.
+
+
+Lemma preservation : forall Γ e e' e'' τ,
+  (Γ |- e \is τ) ->
+  (Γ |- [[ e \is τ ]] = e') ->
+  (e' -->eval e'') ->
+  (Γ |- e'' \is τ)
+.
+Proof with simpl_env.
+
+  intros E e e' e'' τ Typing Transl Eval.
+  induction Transl.
+
+  (* Var *)
+  - inversion Eval.
+
+  (* Let *)
+  - inversion Eval.
+    pick fresh y.
+    rewrite (subst_intro y); subst.
+    2: fsetdec.
+    2: inversion H5; assumption.
+
+    apply typing_subst with (σ:=σ).
+    apply transl_preservation with (e:=(expr_open [{ $y }] t)).
+    apply typing_inv_let with (L:=L) (s:=e) (t:=t).
+    1-2:assumption.
+    fsetdec.
+
+    apply transl_inv_let with (L:=L) (s:=e) (s':=e').
+    assumption.
+    2:fsetdec.
+    2:apply transl_preservation with (e:=e).
+    2-3:assumption.
+
+    apply Expand_Let with (L:=L) (σ:=σ).
+    assumption.
+    assumption.
+    assumption.
+
+  (* Type-Abs *)
+  - admit.
+  (*
+    inversion Eval; subst.
+    pick fresh y.
+    apply typing_inv_tabs.
+    apply T_TypeAbs with (L:=L).
+    intros x Fr.
+    rewrite (subst_intro_type x); subst.
+    apply typing_subst_type.
+*)
+
+  (* Type-App *)
+  - inversion Eval; subst.
+    pick fresh y.
+    admit.
+
+  (* func *)
+  - inversion Eval.
+
+  (* morph *)
+  - inversion Eval.
+
+  (* app *)
+  - inversion Eval; subst.
+    (* f is reduced *)
+    * apply T_App with (σ':=σ) (σ:=σ).
+      3: apply id_morphism_path.
+      
+      apply IHTransl1.
+      assumption.
+      inversion Transl1; subst; auto.
+      apply T_App with (σ':=σ') (σ:=σ') (τ:=σ).
+      3: apply id_morphism_path.
+      apply T_MorphFun.
+      apply morphism_path_correct with (τ:=σ') (τ':=σ).
+
+      admit. (* σ' is lc *)
+      admit. (* σ is lc *)
+      admit. (* Γ is wf *)
+
+      assumption.
+      apply transl_preservation with (e:=a).
+      assumption.
+      assumption.
+
+    (* f is value *)
+    * apply T_App with (σ':=σ) (σ:=σ) (τ:=τ).
+      3: apply id_morphism_path.
+      -- apply transl_preservation with (e:=f).
+         all:assumption.
+
+      -- apply transl_preservation with (e:=[{m a'}]).
+         apply T_App with (σ':=σ') (σ:=σ') (τ:=σ).
+         3: apply id_morphism_path.
+         apply T_MorphFun.
+         apply morphism_path_correct.
+         admit. (* σ' is lc *)
+         admit. (* σ is lc *)
+         admit. (* Γ is wf *)
+         assumption.
+         apply transl_preservation with (e:=a).
+         assumption.
+         assumption.
+
+         
+         admit.
+
+    (* f is lambda *)
+    * 
+    * inversion Eval; subst.
+      apply T_App with (σ':=σ) (σ:=σ).
+      auto.
+      apply T_App with (σ':=σ') (σ:=σ').
+      apply T_MorphFun.
+      apply morphism_path_correct.
+      admit. (* σ' is lc *)
+      admit. (* σ is lc *)
+      admit. (* Γ is wf *)
+      assumption.
+      apply transl_preservation with (e:=a).
+      assumption.
+      assumption.
+      apply id_morphism_path.
+      apply id_morphism_path.
+      apply T_App with (σ':=σ) (σ:=σ).
+      3: apply id_morphism_path.
+
+  (* morph-app *)
+  - apply T_MorphFun.
+    apply IHTransl.
+    assumption.
+    assumption.
+
+  (* ascension *)
+  - apply transl_preservation with (e:=[{e' as τ'}]).
+    apply T_Ascend.
+    apply transl_preservation with (e:=e).
+    assumption.
+    assumption.
+    admit.
+    (*
+    apply Expand_Ascend with (Γ:=Γ) (e:=e) (τ':=τ') (τ:=τ) (e':=e').
+    *)
+
+  - apply transl_preservation with (e:=[{e' des τ'}]).
+    apply T_Descend with (τ:=τ).
+    apply transl_preservation with (e:=e).
+    assumption.
+    assumption.
+    assumption.
+    apply Expand_
+    admit.
+
+  (* descension *)
+  - inversion Eval; subst.
+
+    * apply T_DescendImplicit with (τ:=τ).
+      apply transl_preservation with (e:=e).
+      all: assumption.
+
+    * inversion Eval; subst.
+      apply transl_preservation with (e:=e).
+      assumption.
+      apply Expand_Descend with (τ:=τ).
+      assumption.
+      assumption.
+      assumption.
+      apply T_DescendImplicit with (τ:=τ').
+      2: assumption.
+      
+      
+      inversion Transl; subst.
+
+      admit.
+      apply transl_preservation with (e:=e0).
+      
+Admitted.