ladder-calculus/coq/soundness.v

From Coq Require Import Strings.String.
Require Import terms.
Require Import subst.
Require Import equiv.
Require Import subtype.
Require Import context.
Require Import morph.
Require Import smallstep.
Require Import typing.

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 typing_subst : forall Γ x σ s e τ,
  (ctx_assign x σ Γ) |- e \is τ ->
  Γ |- s \is σ ->
  Γ |- (expr_subst x s e) \is τ.
Proof.
Admitted.

Lemma typing_tsubst : forall Γ α σ e τ,
  Γ |- e \is τ ->
  Γ |- (expr_specialize α σ e) \is (type_subst α σ τ).
Proof.
Admitted.



Lemma map_type : forall Γ,
  Γ |- [{ %"map"% }] \is [<
       ∀"σ",∀"τ", (%"σ"% -> %"τ"%) -> [%"σ"%] -> [%"τ"%]
  >].
Proof.
Admitted.

Lemma specialized_map_type : forall Γ τ τ',
  Γ |- [{ %"map"% # τ # τ' }] \is [<
    (τ -> τ') -> [τ] -> [τ']
  >].
Proof.
Admitted.




(* morphism has valid typing *)
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_Descend with (τ:=τ).
  apply T_Var.
  apply C_take.
  apply H.

  (* Lift *)
  apply T_MorphAbs.
  apply T_Ascend.
  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 id_morphism_path.

  (* 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 id_morphism_path.
  apply id_morphism_path.

  (* 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 τ τ')).

  apply specialized_map_type.
  apply typing_weakening.
  apply T_MorphFun.
  apply IHtranslate_morphism_path.

  apply id_morphism_path.
  auto using T_Var, C_take.
  apply id_morphism_path.
Qed.




(* reduction step preserves well-typedness *)
Lemma preservation : forall Γ e e' τ,
  (Γ |- e \is τ) ->
  (e -->β e') ->
  (Γ |- e' \is τ)
.
Proof.
  intros Γ e e' τ Typ Red.
  generalize dependent e'.
  induction Typ; intros e' Red.

  (* `e` is Variable *)
  - inversion Red.

  (* `e` is Let *)
  - inversion Red.
    subst.
    apply typing_subst with (σ:=σ).
    auto.
    auto.

  (* `e` is Type-Abstraction *)
  - inversion Red.
    subst.
    apply T_TypeAbs.
    auto.

  (* `e` is Type-Application *)
  - inversion Red.
    admit.
    (*
    apply typing_tsubst.
    admit.
    *)

  (* `e` is abstraction *)
  - inversion Red.

  (* `e` is morphism *)
  - inversion Red.

  (* `e` is Application *)
  - inversion Red.

    * apply T_App with (σ':=σ') (σ:=σ).
      apply IHTyp1.
      auto. auto. auto.

    * apply T_App with (σ':=σ') (σ:=σ).
      auto using IHTyp2.
      auto. auto.

    * apply typing_subst with (σ:=σ').
      subst.
      admit.
      auto.

    * apply typing_subst with (σ:=σ').
      admit.
      auto.

  (* `e` is Morphism *)
  - auto using T_MorphFun.

  (* `e` is Ascend *)
  - admit.
    (*
    apply IHexpr_type.
    inversion Red.
    *)

  (* `e` is Descension *)
  - intros.
    apply T_DescendImplicit with (τ:=τ).
    auto. auto.

  (* `e` is descension *)
  - apply T_DescendImplicit with (τ:=τ).
    apply IHTyp.
    admit.
    auto.
Admitted.

(* translation of expression preserves typing *)
Lemma translation_preservation : forall Γ e e' τ,
  (Γ |- e \is τ) ->
  (translate_typing Γ e τ e') ->
  (Γ |- e' \is τ)
.
Proof.
  intros Γ e e' τ Typ Transl.
  generalize dependent e'.
  intros e' Transl.
  induction Transl.

  (* e is Variable *)
  - apply H.

  (* e is Let-Binding *)
  - apply T_Let with (τ:=τ) (σ:=σ).
    auto. auto.

  - auto using T_TypeAbs.

  (* e is Type-Application *)
  - apply T_TypeApp.
    admit.

  - auto using T_Abs.
  - auto using T_MorphAbs.

  (* e is Application *)
  - apply T_App with (σ':=σ) (σ:=σ) (τ:=τ).
    auto.
    apply T_App with (σ':=σ') (σ:=σ') (τ:=σ).
    apply T_MorphFun.
    apply morphism_path_solves_type.
    auto. auto.
    apply id_morphism_path.
    apply id_morphism_path.

  (* e is Morphism *)
  - auto using T_MorphFun.

  (* e is Ascension *)
  - auto using T_Ascend.

  (* e is Desecension *)
  - apply T_Descend with (τ:=τ).
    auto. auto.
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')
.

(* the translation any well typed term is not stuck *)
Lemma progress :
  forall Γ e τ e',
  (Γ |- e \is τ) ->
  (translate_typing Γ e τ e') ->
  ~(is_stuck e')
.
Proof.
Admitted.



(* every well-typed expression is translated,
 * such that it be reduced to a value
 *)
Theorem soundness :
  forall Γ e e' τ,
  (Γ |- e \is τ) ->
  (translate_typing Γ e τ e') ->
  (exists v, (e' -->β* v) /\ (is_value v) /\ (Γ |- v \is τ))
.
Proof.
  intros.
  induction H0.

  (* `e` is Variable *)
  - 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.
    admit.
(*
  split.
  unfold expr_subst.
  induction t'.
  
  exists (expr_subst x e' (expr_var s)).
  split.
  unfold expr_subst.
  apply E_Let.
  *)

  (* `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.
  
  (* `e` is morphism *)
  - admit.

  (* `e` is Ascension *)
  - admit.

  (* `e` is Descension *)
  - admit.
Admitted.