Require Import List.

Require Import MatchCompNat.
Require Import Util.
Require Import WellFoundation.
Require Import SimplyTypedLambdaCalculus.
Require Import SimplyTypedLambdaCalculus_normalization.

Require Syntax.
Module SetProgram(My_Program: Syntax.Program).
Import My_Program.

Require Subtyping_proofs.
Module My_Subtyping_proofs := Subtyping_proofs.SetProgram(My_Program).
Import My_Subtyping_proofs.

Import My_Typing_proofs.
Import My_Confluence.
Import My_Auxiliary_proofs.
Import My_Substitutions_proofs.
Import My_Binders_proofs.
Import My_Semantics.
Import My_WellFormedness.
Import My_Typing.
Import My_Auxiliary.
Import My_Substitutions.
Import My_Binders.


Lemma wellKinded_implies_kind_of_exists:
  forall (D: TypeEnv) (t: TypeS) (c: TypeC),
    (Type_WK D t c) ->
    ((c = TypeSection) \/ (c = TypeParam) \/ (c = TypeParamList)) ->
    exists k: KindS,
      (kind_of t k)
.
























Lemma Class_kind_existence:
  forall (C: ClassSym),
    exists k: KindS,
      (kind_of (classTypeParams C) k)
.



Module My_Constants.

Inductive LConst_definition: Set :=
  | LConst_class : ClassSym -> LConst_definition
  | LConst_none : LConst_definition
  | LConst_nil : LConst_definition
.

Definition LConst: Set := LConst_definition.

Inductive LType: Set :=
  | LType_base : LType
  | LType_fun : LType -> LType -> LType
  | LType_prod : LType -> LType -> LType
.

Fixpoint type_of_kind (k': KindS): LType :=
  match k' with
    | (Kind_tuple ks) => (type_of_kind ks)
    | (Kind_constr kr) => (LType_prod (LType_fun (type_of_kind kr) LType_base)
                                      (LType_fun (type_of_kind kr) (type_of_kind kr)))
    | Kind_nil => LType_base
    | (Kind_cons k ks) => (LType_prod (type_of_kind k) (type_of_kind ks))
  end
.

Inductive type_of (t: TypeS): LType -> Prop :=

  | Type_of_intro:
    forall (k: KindS),
      (kind_of t k) ->
      (type_of t (type_of_kind k))
.

Lemma Type_of_is_a_partial_function:
  forall (t: TypeS) (T1 T2: LType),
    (type_of t T1) ->
    (type_of t T2) ->
    T1 = T2
.


Inductive type_of_const_def: LConst -> LType -> Prop :=

  | type_of_const_class:
    forall (C: ClassSym) (k: KindS),
      (kind_of (classTypeParams C) k) ->
      (type_of_const_def (LConst_class C) (type_of_kind (Kind_constr k)))

  | type_of_const_none:
    (type_of_const_def LConst_none LType_base)

  | type_of_const_nil:
    (type_of_const_def LConst_nil LType_base)
.

Definition type_of_const := type_of_const_def.

End My_Constants.


Module My_LambdaCalculusNormalization := LambdaCalculusNormalization(My_Constants).

Import My_LambdaCalculusNormalization.
Import My_LambdaCalculus.
Import My_Constants.


Fixpoint LTerm_proj (t: LTerm) (i: nat) {struct i}: LTerm :=
  match i with
    | 0 => (LTerm_fst t)
    | (S n) => (LTerm_proj (LTerm_snd t) n)
  end
.

Inductive trans: TypeS -> LTerm -> Prop :=

  | trans_class:
    forall (C: ClassSym),
      (trans (Type_class C) (LTerm_const (LConst_class C)))

  | trans_proj:
    forall (R: TypeS) (R': LTerm) (i: nat),
      (trans R R') ->
      (trans (Type_proj R i) (LTerm_proj R' i))

  | trans_fun:
    forall (Pi T: TypeS) (U: LType) (Pi' T': LTerm),
      (trans Pi Pi') ->
      (trans T T') ->
      (type_of Pi U) ->
      (trans (Type_fun Pi T) (LTerm_pair (LTerm_fun U T') Pi'))

  | trans_var:
    forall (X: TypeVar),
      (trans (Type_var X) (LTerm_var X))

  | trans_tuple:
    forall (Ks: TypeS) (Ks': LTerm),
      (trans Ks Ks') ->
      (trans (Type_tuple Ks) Ks')

  | trans_apply:
    forall (K Ks: TypeS) (K' Ks': LTerm),
      (trans K K') ->
      (trans Ks Ks') ->
      (trans (Type_apply K Ks) (LTerm_app (LTerm_fst K') Ks'))

  | trans_param:
    forall (Pi T_opt: TypeS) (U: LType) (Pi' T_opt': LTerm),
      (trans Pi Pi') ->
      (trans T_opt T_opt') ->
      (type_of Pi U) ->
      (trans (Type_param Pi T_opt) (LTerm_pair (LTerm_fun U T_opt') Pi'))

  | trans_section:
    forall (Ps: TypeS) (U: LType) (Ps': LTerm),
      (trans Ps Ps') ->
      (type_of (Type_section Ps) U) ->
      (trans (Type_section Ps) (LTerm_fun U Ps'))

  | trans_none:
    (trans Type_none (LTerm_const LConst_none))

  | trans_some:
    forall (T: TypeS) (T': LTerm),
      (trans T T') ->
      (trans (Type_some T) T')

  | trans_nil:
    (trans Type_nil (LTerm_const LConst_nil))

  | trans_cons:
    forall (t ts: TypeS) (t' ts':LTerm),
      (trans t t') ->
      (trans ts ts') ->
      (trans (Type_cons t ts) (LTerm_pair t' ts'))
.

Inductive trans_category (t: TypeS): TypeC -> LType -> Prop :=

  | transcat_TypeConstr:
    forall (k: KindS),
      (trans_category t (TypeConstr k) (type_of_kind k))

  | transcat_Type_:
    (trans_category t Type_ LType_base)

  | transcat_TypeTuple:
    forall (kr: KindS),
      (trans_category t (TypeTuple kr) (type_of_kind kr))

  | transcat_TypeParam:
    forall (k: KindS),
      (kind_of t k) ->
      (trans_category t TypeParam (type_of_kind k))

  | transcat_TypeSection:
    forall (k: KindS),
      (kind_of t k) ->
      (trans_category t TypeSection (LType_fun (type_of_kind k) (type_of_kind k)))

  | transcat_TypeOption:
    (trans_category t TypeOption LType_base)
    
  | transcat_TypeParamList:
    forall (k: KindS),
      (kind_of t k) ->
      (trans_category t TypeParamList (type_of_kind k))

  | transcat_TypeConstrList:
    forall (ks: KindS),
      (trans_category t (TypeConstrList ks) (type_of_kind ks))
.


Lemma R_proj_cong:
  forall (t t': LTerm) (i: nat),
    (RedTerm t t') ->
    (RedTerm (LTerm_proj t i) (LTerm_proj t' i))
.




Lemma Rplus_proj_cong:
  forall (t t': LTerm) (i: nat),
    (Rplus RedTerm t t') ->
    (Rplus RedTerm (LTerm_proj t i) (LTerm_proj t' i))
.



Lemma Rplus_fun:
  forall (t t': LTerm) (T: LType),
    (Rplus RedTerm t t') ->
    (Rplus RedTerm (LTerm_fun T t) (LTerm_fun T t'))
.



Lemma Rplus_app_left:
  forall (t t' u: LTerm),
    (Rplus RedTerm t t') ->
    (Rplus RedTerm (LTerm_app t u) (LTerm_app t' u))
.



Lemma Rplus_app_right:
  forall (t u u': LTerm),
    (Rplus RedTerm u u') ->
    (Rplus RedTerm (LTerm_app t u) (LTerm_app t u'))
.



Lemma Rplus_pair_left:
  forall (t t' u: LTerm),
    (Rplus RedTerm t t') ->
    (Rplus RedTerm (LTerm_pair t u) (LTerm_pair t' u))
.



Lemma Rplus_pair_right:
  forall (t u u': LTerm),
    (Rplus RedTerm u u') ->
    (Rplus RedTerm (LTerm_pair t u) (LTerm_pair t u'))
.



Lemma Rplus_fst_cong:
  forall (t t': LTerm),
    (Rplus RedTerm t t') ->
    (Rplus RedTerm (LTerm_fst t) (LTerm_fst t'))
.



Lemma Rplus_snd_cong:
  forall (t t': LTerm) (T: LType),
    (Rplus RedTerm t t') ->
    (Rplus RedTerm (LTerm_snd t) (LTerm_snd t'))
.




Lemma typeSubst_of_LTerm_proj:
  forall (t s: LTerm) (i k: nat),
  (subst_in_term (LTerm_proj t i) k s) =
  (LTerm_proj (subst_in_term t k s) i)
.




Lemma type_of_of_typeSubst:
  forall (t R: TypeS) (U: LType) (k: nat),
    (type_of t U) ->
    (type_of (typeSubst_in_type t k R) U)
.



Lemma lift_of_LTerm_proj:
  forall (t: LTerm) (i k n: nat),
    (lift_at_depth_in_term (LTerm_proj t i) k n) =
    (LTerm_proj (lift_at_depth_in_term t k n) i)
.




Lemma type_of_of_lift:
  forall (t: TypeS) (U: LType) (k n: nat),
    (type_of t U) ->
    (type_of (lift_at_depth_in_type t k n) U)
.



Lemma trans_of_lift:
  forall (t: TypeS) (k n: nat) (t': LTerm),
    (trans t t') ->
    (trans (lift_at_depth_in_type t n k) (lift_at_depth_in_term t' k n))
.















Lemma trans_of_typeSubst:
  forall (t R: TypeS) (k: nat) (t' R': LTerm),
    (trans t t') ->
    (trans R R') ->
    (trans (typeSubst_in_type t k R) (subst_in_term t' k R'))
.







Require Import Arith.























Lemma trans_is_a_partial_function:
  forall (t: TypeS) (u1 u2: LTerm),
    (trans t u1) ->
    (trans t u2) ->
    (u1 = u2)
.





















Lemma R_proj_redex:
  forall (i: nat) (Ks Ki: TypeS) (Ks' Ki': LTerm),
    (TypeS_at Ks i Ki) ->
    (trans Ks Ks') ->
    (trans Ki Ki') ->
    (Rplus RedTerm (LTerm_proj Ks' i) Ki')
.







Lemma Reduction_preserves_type_of:
  forall (t t': TypeS) (T: LType),
    (type_of t T) ->
    (RedType t t') ->
    (type_of t' T)
.



Theorem Preservation_of_semantics:
  forall (t u: TypeS) (t' u': LTerm),
    (RedType t u) ->
    (trans t t') ->
    (trans u u') ->
    (Rplus RedTerm t' u')
.


































Lemma WT_proj:
  forall (G: LEnv) (ks ki: KindS) (t: LTerm) (i: nat),
    (WellTyped G t (type_of_kind ks)) ->
    (KindS_at ks i ki) ->
    (WellTyped G (LTerm_proj t i) (type_of_kind ki))
.





Inductive trans_typeEnv: TypeEnv -> LEnv -> Prop :=

  | trans_typeEnv_nil:
    (trans_typeEnv nil nil)

  | trans_typeEnv_snoc:
    forall (Pi: TypeS) (D: TypeEnv) (k: KindS) (D': LEnv),
    (kind_of Pi k) ->
    (trans_typeEnv D D') ->
    (trans_typeEnv (snoc D Pi) (snoc D' (type_of_kind k)))
 .

Lemma trans_typeEnv_and_TypeSection_at:
  forall (D: TypeEnv) (G: LEnv) (i: nat) (Pi: TypeS) (k: KindS),
    (TypeSection_at D i Pi) ->
    (trans_typeEnv D G) ->
    (kind_of Pi k) ->
    (List_from G i (type_of_kind k))
.









Theorem Preservation_of_typing:
  forall (D: TypeEnv) (t: TypeS) (c: TypeC),
    (Type_WK D t c) ->
    forall (G: LEnv),
      (trans_typeEnv D G) ->
      exists t': LTerm, exists c': LType,
        (trans t t') /\
        (trans_category t c c') /\
        (WellTyped G t' c')
.












































































Lemma Preservation_of_semantics_cor1:
  forall (D: TypeEnv) (t: TypeS) (c: TypeC) (t': LTerm),
    (Type_WK D t c) ->
    (exists G: LEnv, (trans_typeEnv D G)) ->
    (trans t t') ->
    (Acc (symRel RedTerm) t') ->
    (Acc (symRel RedType) t)
.












Inductive TypeEnv_WK: TypeEnv -> Prop :=

  | WK_typeEnv_nil:
    (TypeEnv_WK nil)

  | WK_typeEnv_snoc:
    forall (D: TypeEnv) (Pi: TypeS),
      (TypeEnv_WK D) ->
      (Type_WK D Pi TypeSection) ->
      (TypeEnv_WK (snoc D Pi))
.

Lemma wellKinded_implies_trans_typeEnv_exists:
  forall (D: TypeEnv),
    (TypeEnv_WK D) ->
    exists D': LEnv,
      (trans_typeEnv D D')
.






Lemma Type_reduction_is_well_founded:
  forall (D: TypeEnv) (t: TypeS) (c: TypeC),
    (Type_WK D t c) ->
    (TypeEnv_WK D) ->
    (Acc (symRel RedType) t)
.


End SetProgram.