Require Import List.
Require Import Arith.

Require Import MatchCompNat.
Require Import Util.

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

Require TypeSubstitutionInTyping.
Module My_TypeSubstitutionInTyping := TypeSubstitutionInTyping.SetProgram(My_Program).
Import My_TypeSubstitutionInTyping.

Import My_BoundCompliantSubstitutions_proofs.
Import My_Progress_proofs.
Import My_TransitivityElimination_proofs.
Import My_Normalization_proofs.
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.


Inductive SubInfo (D: TypeEnv): TermInfo -> TermInfo -> Prop :=

  | SubInfo_term:
    forall (T U: TypeS),
      (Subtyping D T U) ->
      (SubInfo D (TermI T) (TermI U))

  | SubInfo_termList:
    forall (Ts Us: (list TypeS)),
      (Pointwise_subtyping D Ts Us) ->
      (SubInfo D (TermListI Ts) (TermListI Us))

  | SubInfo_fieldTermList:
    forall (N: TypeS),
      (SubInfo D (FieldTermListI N) (FieldTermListI N))
.


Lemma SubInfo_refl:
  forall (D: TypeEnv) (info: TermInfo),
    (SubInfo D info info)
.







Lemma SubInfo_trans:
  forall (D: TypeEnv) (info1 info2 info3: TermInfo),
    (Info_WK D info2) ->
    (SubInfo D info1 info2) ->
    (SubInfo D info2 info3) ->
    (SubInfo D info1 info3)
.








Lemma SubInfo_trans_cor1:
  forall (D: TypeEnv) (Ts1 Ts2 Ts3: (list TypeS)),
    (Info_WK D (TermListI Ts2)) ->
    (Pointwise_subtyping D Ts1 Ts2) ->
    (Pointwise_subtyping D Ts2 Ts3) ->
    (Pointwise_subtyping D Ts1 Ts3)
.




Lemma Term_substitution_preserves_fields_of_fieldTermList:
  forall (D: TypeEnv) (G: TermEnv) (N: TypeS) (fts: Term) (k: nat) (v: Term),
    (Term_WT D G fts (FieldTermListI N)) ->
    (fields_of_fieldTermList (termSubst_in_term fts k v)) =
    (fields_of_fieldTermList fts)
.











Lemma Term_lifting_preserves_fields_of_fieldTermList:
  forall (D: TypeEnv) (G: TermEnv) (N: TypeS) (fts: Term) (k n: nat),
    (Term_WT D G fts (FieldTermListI N)) ->
    (fields_of_fieldTermList (lift_at_depth_in_term fts k n)) =
    (fields_of_fieldTermList fts)
.












Lemma Typing_right_weakening:
  forall (D: TypeEnv) (G1 G2: TermEnv) (t: Term) (info: TermInfo),
    (Term_WT D G1 t info) ->
    (Term_WT D (G1 ++ G2) (lift_in_term t (length G2)) info)
.













Theorem Term_substitution_preserves_typing:
  forall (D: TypeEnv) (G1 G2: TypeEnv) (U U': TypeS) (u t: Term) (info: TermInfo),
    (TypeEnv_WK D) ->
    (TermEnv_WK D (G1 ++ (U :: G2))) ->
    (Term_WT D G1 u (TermI U')) ->
    (Subtyping D U' U) ->
    (Term_WT D (G1 ++ (U :: G2)) t info) ->
    exists info': TermInfo,
      (Term_WT D (G1 ++ G2) (termSubst_in_term t (length G2) u) info') /\
      (SubInfo D info' info)
.

















































































Lemma polySubst_by_snoc:
  forall (t u: Term) (k: nat) (us: (list Term)),
    (polyTermSubst_in_term t k (snoc us u)) =
    (termSubst_in_term (polyTermSubst_in_term t (S k) us) k u)
.

Theorem Poly_term_substitution_preserves_typing:
  forall (D: TypeEnv) (G1 G2: TypeEnv) (Us Us': (list TypeS)) (t: Term)
         (us: (list Term)) (info: TermInfo),
    (TypeEnv_WK D) ->
    (TermEnv_WK D (G1 ++ Us ++ G2)) ->
    (Forall2 (fun u U' => (Term_WT D G1 u (TermI U'))) us Us') ->
    (Pointwise_subtyping D Us' Us) ->
    (Term_WT D (G1 ++ Us ++ G2) t info) ->
    exists info': TermInfo,
      (Term_WT D (G1 ++ G2) (polyTermSubst_in_term t (length G2) us) info') /\
      (SubInfo D info' info)
.

Lemma Poly_term_substitution_preserves_typing_cor1:
  forall (D: TypeEnv) (G1: TypeEnv) (Us Us': (list TypeS)) (t: Term)
         (us: (list Term)) (info: TermInfo),
    (TypeEnv_WK D) ->
    (TermEnv_WK D (G1 ++ Us)) ->
    (Forall2 (fun u U' => (Term_WT D G1 u (TermI U'))) us Us') ->
    (Pointwise_subtyping D Us' Us) ->
    (Term_WT D (G1 ++ Us) t info) ->
    exists info': TermInfo,
      (Term_WT D G1 (polyTermSubst_in_term t 0 us) info') /\
      (SubInfo D info' info)
.

Lemma Poly_term_substitution_preserves_typing_cor2:
  forall (Us Us': (list TypeS)) (t: Term) (us: (list Term)) (T: TypeS),
    (TermEnv_WK nil Us) ->
    (Forall2 (fun u U' => (Term_WT nil nil u (TermI U'))) us Us') ->
    (Pointwise_subtyping nil Us' Us) ->
    (Term_WT nil Us t (TermI T)) ->
    exists T': TypeS,
      (Term_WT nil nil (polyTermSubst_in_term t 0 us) (TermI T')) /\
      (Subtyping nil T' T)
.






End SetProgram.