Require Import List.
Require Import Arith.
Require Import Wf_nat.

Require Import MatchCompNat.
Require Import Util.

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

Require Progress_proofs.
Module My_Progress_proofs := Progress_proofs.SetProgram(My_Program).
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.


Lemma Lifting_preserves_removeBounds:
  forall (t t': TypeS) (k n: nat),
    (removeBounds t t') ->
    (removeBounds (lift_at_depth_in_type t n k) t')
.


Lemma removeBounds_invariant_by_lifting:
  forall (t t': TypeS) (k n: nat),
    (removeBounds t t') ->
    (lift_at_depth_in_type t' n k) = t'
.






Lemma lift_of_some_inversion:
  forall (t N: TypeS) (n k: nat),
    (lift_at_depth_in_type t n k) = (Type_some N) ->
    exists N0: TypeS,
      t = (Type_some N0) /\
      N = (lift_at_depth_in_type N0 n k)
.


Lemma lift_of_cons_inversion:
  forall (t u us: TypeS) (n k: nat),
    (lift_at_depth_in_type t n k) = (Type_cons u us) ->
    exists u0: TypeS, exists us0: TypeS,
      t = (Type_cons u0 us0) /\
      u = (lift_at_depth_in_type u0 n k) /\
      us = (lift_at_depth_in_type us0 n k)
.


Lemma TypeS_at_of_lift_inversion:
  forall (t u: TypeS) (i n k: nat),
    (TypeS_at (lift_at_depth_in_type t n k) i u) ->
    exists u0: TypeS,
      (TypeS_at t i u0) /\
      u = (lift_at_depth_in_type u0 n k)
.











Lemma Weakening_of_param_satisfaction:
  forall (D1 D2 D3: TypeEnv) (K P: TypeS),
    (ParamSat (D1 ++ D3) K P) ->
    (ParamSat (D1 ++ D2 ++ (lift_in_typeEnv D3 (length D2)))
                (lift_at_depth_in_type K (length D2) (length D3))
                (lift_at_depth_in_type P (length D2) (length D3)))
.












Lemma Weakening_of_satisfaction:
  forall (D1 D2 D3: TypeEnv) (R Pi: TypeS),
    (SectionSat (D1 ++ D3) R Pi) ->
    (SectionSat (D1 ++ D2 ++ (lift_in_typeEnv D3 (length D2)))
                (lift_at_depth_in_type R (length D2) (length D3))
                (lift_at_depth_in_type Pi (length D2) (length D3)))
.






Lemma Weakening_of_satisfaction_by_the_right:
  forall (D D': TypeEnv) (R Pi: TypeS),
    (SectionSat D R Pi) ->
    (SectionSat (D ++ D')
                (lift_in_type R (length D'))
                (lift_in_type Pi (length D')))
.




Fixpoint size_of_kind (k: KindS): nat :=
  match k with
    | (Kind_tuple k1) => (size_of_kind k1) + 1
    | (Kind_constr k1) => (size_of_kind k1) + 1
    | Kind_nil => 0
    | (Kind_cons k1 k2) => (size_of_kind k1) + (size_of_kind k2) + 1
  end
.

Lemma typeSubst_of_class_type:
  forall (C: ClassSym) (R R': TypeS) (n: nat),
    (typeSubst_in_type (Class_type C R) n R') =
    (Class_type C (typeSubst_in_type R n R'))
.

Lemma Substitution_in_closed_type_aux:
  forall (D: TypeEnv) (t R: TypeS) (c: TypeC) (k: nat),
    (Type_WK D t c) ->
    (typeSubst_in_type t ((length D) + k) R) = t
.






















Lemma removeBounds_is_idempotent:
  forall (t t': TypeS),
    (removeBounds t t') ->
    (removeBounds t' t')
.


Lemma removeBounds_preserves_kind_of:
  forall (t t': TypeS) (k: KindS),
    (kind_of t k) ->
    (removeBounds t t') ->
    (kind_of t' k)
.






Lemma Substitution_preserves_removeBounds:
  forall (t t' R: TypeS) (k: nat),
    (removeBounds t t') ->
    (removeBounds (typeSubst_in_type t k R) t')
.






Lemma removeBounds_then_substitution:
  forall (t t' R: TypeS) (k: nat),
    (removeBounds t t') ->
    (typeSubst_in_type t' k R) = t'
.






Lemma removeBounds_invariant_by_substitution:
  forall (t t' R: TypeS) (k: nat),
    (removeBounds t t') ->
    (typeSubst_in_type t' k R) = t'
.







Lemma TypeParamList_ind:
  forall (D: TypeEnv) (Q: TypeS -> Prop),
    (Q Type_nil) ->
    (forall (P Ps: TypeS),
      (Type_WK D P TypeParam) ->
      (Type_WK D Ps TypeParamList) ->
      (Q Ps) ->
      (Q (Type_cons P Ps))
    ) ->
    forall (Ps: TypeS),
      (Type_WK D Ps TypeParamList) ->
      (Q Ps)
.



















Lemma kind_of_params_inversion:
  forall (Ps P: TypeS) (k ks: KindS) (i: nat),
    (kind_of Ps ks) ->
    (TypeS_at Ps i P) ->
    (KindS_at ks i k) ->
    (kind_of P k)
.




Lemma kind_of_params_inversion_variant1:
  forall (Ps P: TypeS) (ks: KindS) (i: nat),
    (kind_of Ps ks) ->
    (TypeS_at Ps i P) ->
    exists k: KindS,
      (KindS_at ks i k) /\
      (kind_of P k)
.







Lemma removeBounds_of_params_inversion:
  forall (Ps Ps' P': TypeS) (i: nat),
    (removeBounds Ps Ps') ->
    (TypeS_at Ps' i P') ->
    exists P: TypeS,
      (TypeS_at Ps i P) /\
      (removeBounds P P')
.







Lemma removeBounds_and_kind_of_inversion:
  forall (t t': TypeS) (k: KindS),
    (removeBounds t t') ->
    (kind_of t' k) ->
    (kind_of t k)
.







Lemma kind_equality_implies_param_satisfaction:
  forall (D: TypeEnv) (K P P' Pi N_opt: TypeS) (k: KindS),
    P = (Type_param Pi N_opt) ->
    (Type_WK D K (TypeConstr k)) ->
    (removeBounds P P') ->
    (kind_of P k) ->
    (ParamSat D K P')
.



Theorem kind_equality_implies_poly_satisfaction:
  forall (D: TypeEnv) (R Pi Pi': TypeS) (k: KindS),
    (Type_WK D R (TypeTuple k)) ->
    (Type_WK D Pi TypeSection) ->
    (kind_of Pi k) ->
    (removeBounds Pi Pi') ->
    (SectionSat D R Pi')
.













Lemma TypeEnv_WK_inversion:
  forall (D: TypeEnv) (i: nat) (Pi: TypeS),
    (TypeEnv_WK D) ->
    (TypeSection_at D i Pi) ->
    (Type_WK D (lift_in_type Pi (S i)) TypeSection)
.









Lemma TypeEnv_WK_inversion_cor1:
  forall (D: TypeEnv) (X: TypeVar) (Pi: TypeS),
    (TypeEnv_WK D) ->
    (decl_of_typeVar D X Pi) ->
    (Type_WK D Pi TypeSection)
.



Lemma Var_expansion_preserves_well_kindedness_aux:
  forall (Ps Pi N_opt: TypeS) (i: nat) (k ks: KindS),
    (TypeS_at Ps i (Type_param Pi N_opt)) ->
    (kind_of Ps ks) ->
    (KindS_at ks i (Kind_constr k)) ->
    (kind_of Pi k)
.











Theorem Var_expansion_preserves_well_kindedness:
  forall (D: TypeEnv) (X: TypeVar) (R Ps Pi N: TypeS) (i: nat),
    (TypeEnv_WK D) ->
    (decl_of_typeVar D X (Type_section Ps)) ->
    (TypeS_at (typeSubst_in_type Ps 0 (Type_var X)) i (Type_param Pi (Type_some N))) ->
    (Type_WK D (Var_type X i R) Type_) ->
    (Type_WK D (typeSubst_in_type N 0 R) Type_)
.











Lemma TypeEnv_WK_inversion_cor2:
  forall (D1 D2: TypeEnv) (Pi: TypeS),
    (TypeEnv_WK (D1 ++ (Pi :: D2))) ->
    (Type_WK D1 Pi TypeSection)
.










Lemma KindS_at_and_size:
  forall (k ks: KindS) (i: nat),
    (KindS_at ks i k) ->
    (size_of_kind k) < (size_of_kind ks)
.





Lemma Substitution_in_well_kinded_type_env:
  forall (D1 D2: TypeEnv) (Pi R: TypeS) (k: KindS),
    (TypeEnv_WK (D1 ++ Pi :: D2)) ->
    (Type_WK D1 R (TypeTuple k)) ->
    (kind_of Pi k) ->
    (TypeEnv_WK (D1 ++ (typeSubst_in_typeEnv D2 0 R)))
.










Lemma removeBounds_preserves_well_kindedness:
  forall (D: TypeEnv) (t t': TypeS) (c: TypeC),
    (Type_WK D t c) ->
    (removeBounds t t') ->
    forall (D': TypeEnv),
      (Type_WK D' t' c)
.

















Lemma Type_substitution_preserves_subtyping_aux1:
  forall (D1 D2: TypeEnv) (R Pi': TypeS) (i: nat) (k0 k1: KindS),
    (Type_WK D1 R (TypeTuple (Kind_tuple k1))) ->
    (KindS_at k1 i (Kind_constr k0)) ->
    (kind_of Pi' k0) ->
    (Type_WK (snoc (D1 ++ typeSubst_in_typeEnv D2 0 R) Pi')
             (Type_apply (lift_in_type (Type_proj (lift_in_type R (length D2)) i) 1)
             (Type_var 0)) Type_)
.







Theorem Type_substitution_preserves_subtyping:
  forall (D1 D2: TypeEnv) (Pi R T U: TypeS) (k: KindS),
    (Type_WK D1 R (TypeTuple k)) ->
    (SectionSat D1 R Pi) ->
    (TypeEnv_WK (D1 ++ (Pi :: D2))) ->
    (Subtyping (D1 ++ (Pi :: D2)) T U) ->
    (Type_WK (D1 ++ (Pi :: D2)) T Type_) ->
    (Type_WK (D1 ++ (Pi :: D2)) U Type_) ->
    (Subtyping (D1 ++ (typeSubst_in_typeEnv D2 0 R))
               (typeSubst_in_type T (length D2) R)
               (typeSubst_in_type U (length D2) R))
.






































































































Theorem Type_substitution_preserves_subtyping_snoc:
  forall (D1: TypeEnv) (Pi R T U: TypeS) (k: KindS),
    (Type_WK D1 R (TypeTuple k)) ->
    (SectionSat D1 R Pi) ->
    (TypeEnv_WK (snoc D1 Pi)) ->
    (Subtyping (snoc D1 Pi) T U) ->
    (Type_WK (snoc D1 Pi) T Type_) ->
    (Type_WK (snoc D1 Pi) U Type_) ->
    (Subtyping D1 (typeSubst_in_type T 0 R) (typeSubst_in_type U 0 R))
.


Lemma Type_substitution_preserves_subtyping_cor1:
  forall (Pi1 Pi2 R T U: TypeS) (k: KindS),
    (Type_WK nil R (TypeTuple k)) ->
    (SectionSat nil R Pi1) ->
    let D := (Pi1 :: Pi2 :: nil) in
    (TypeEnv_WK D) ->
    (Type_WK D T Type_) ->
    (Type_WK D U Type_) ->
    (Subtyping D T U) ->
    (Subtyping ((typeSubst_in_type Pi2 0 R) :: nil)
               (typeSubst_in_type T 1 R)
               (typeSubst_in_type U 1 R))
.


Lemma Type_substitution_preserves_subtyping_cor2:
  forall (Pi R T U: TypeS) (k: KindS),
    (Type_WK nil R (TypeTuple k)) ->
    (SectionSat nil R Pi) ->
    let D := (Pi :: nil) in
    (TypeEnv_WK D) ->
    (Type_WK D T Type_) ->
    (Type_WK D U Type_) ->
    (Subtyping D T U) ->
    (Subtyping nil
               (typeSubst_in_type T 0 R)
               (typeSubst_in_type U 0 R))
.



Lemma typeSubst_of_some_inversion:
  forall (D: TypeEnv) (t N R: TypeS) (k: nat),
    (Type_WK D t TypeOption) ->
    (typeSubst_in_type t k R) = (Type_some N) ->
    exists N0: TypeS,
      t = (Type_some N0) /\
      N = (typeSubst_in_type N0 k R)
.



Lemma typeSubst_of_cons_inversion:
  forall (D: TypeEnv) (t u us R: TypeS) (k: nat),
    (Type_WK D t TypeParamList) ->
    (typeSubst_in_type t k R) = (Type_cons u us) ->
    exists u0: TypeS, exists us0: TypeS,
      t = (Type_cons u0 us0) /\
      u = (typeSubst_in_type u0 k R) /\
      us = (typeSubst_in_type us0 k R)
.



Lemma TypeS_at_of_typeSubst_inversion:
  forall (D: TypeEnv) (t u R: TypeS) (i k: nat),
    (Type_WK D t TypeParamList) ->
    (TypeS_at (typeSubst_in_type t k R) i u) ->
    exists u0: TypeS,
      (TypeS_at t i u0) /\
      u = (typeSubst_in_type u0 k R)
.











Lemma Type_substitution_preserves_param_satisfaction:
  forall (D1 D2: TypeEnv) (Pi R K P: TypeS) (k k': KindS),
    let D := (D1 ++ (Pi :: D2)) in
    (Type_WK D1 R (TypeTuple k)) ->
    (SectionSat D1 R Pi) ->
    (TypeEnv_WK D) ->
    (ParamSat D K P) ->
    (Type_WK D K (TypeConstr k')) ->
    (Type_WK D P TypeParam) ->
    (kind_of P k') ->
    (ParamSat (D1 ++ (typeSubst_in_typeEnv D2 0 R))
              (typeSubst_in_type K (length D2) R)
              (typeSubst_in_type P (length D2) R))
.



























Theorem Type_substitution_preserves_satisfaction:
  forall (D1 D2: TypeEnv) (Pi R R' Pi': TypeS) (k: KindS),
    let D := (D1 ++ (Pi :: D2)) in
    (Type_WK D1 R (TypeTuple k)) ->
    (SectionSat D1 R Pi) ->
    (TypeEnv_WK D) ->
    (SectionSat D R' Pi') ->
    (Type_WK D Pi' TypeSection) ->
    (SectionSat (D1 ++ (typeSubst_in_typeEnv D2 0 R))
               (typeSubst_in_type R' (length D2) R)
               (typeSubst_in_type Pi' (length D2) R))
.
















Theorem Type_substitution_preserves_satisfaction_snoc:
  forall (D1: TypeEnv) (Pi R R' Pi': TypeS) (k: KindS),
    let D := (snoc D1 Pi) in
    (Type_WK D1 R (TypeTuple k)) ->
    (SectionSat D1 R Pi) ->
    (TypeEnv_WK D) ->
    (SectionSat D R' Pi') ->
    (Type_WK D Pi' TypeSection) ->
    (SectionSat D1 (typeSubst_in_type R' 0 R) (typeSubst_in_type Pi' 0 R))
.


End SetProgram.