Require Import List.
Require Import Arith.
Require Import Relations.

Require Import MatchCompNat.
Require Import Util.

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

Require Typing_proofs.
Module My_Typing_proofs := Typing_proofs.SetProgram(My_Program).
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 S_beta_right_star:
  forall (D : TypeEnv) (T U' U : TypeS),
    (Subtyping D T U') ->
    (RedTypeStar U U') ->
    (Subtyping D T U)
.



Lemma S_beta_left_star:
  forall (D : TypeEnv) (T T' U : TypeS),
    (RedTypeStar T T') ->
    (Subtyping D T' U) ->
    (Subtyping D T U)
.



Lemma RT_snoc_left:
  forall (D D': TypeEnv) (Pi: TypeS),
    (RedTypeEnv D D') ->
    (RedTypeEnv (snoc D Pi) (snoc D' Pi))
.



Lemma RT_snoc_right:
  forall (D: TypeEnv) (Pi Pi': TypeS),
    (RedType Pi Pi') ->
    (RedTypeEnv (snoc D Pi) (snoc D Pi'))
.




Lemma Reduction_preserves_kind_of:
  forall (t t': TypeS) (k: KindS),
    (kind_of t k) ->
    (RedType t t') ->
    (kind_of t' k)
.











Lemma Reduction_of_class_types:
  forall (C: ClassSym) (R T: TypeS),
    (RedType (Class_type C R) T) ->
    exists R': TypeS,
      T = (Class_type C R') /\
      (RedType R R')
.



Lemma Reduction_preserves_class_types:
  forall (T T': TypeS),
    (is_classType T) ->
    (RedType T T') ->
    (is_classType T')
.




Inductive clos_refl (A: Set) (R: A -> A -> Prop): A -> A -> Prop :=
  | r_step: forall (x y: A), (R x y) -> (clos_refl A R x y)
  | r_refl: forall (x: A), (clos_refl A R x x)
.

Inductive RedTypeEnv_snoc: TypeEnv -> TypeEnv -> Prop :=

  | RTE_snoc_tail:
    forall (D: TypeEnv) (Pi Pi': TypeS),
    (RedType Pi Pi') ->
    (RedTypeEnv_snoc (snoc D Pi) (snoc D Pi'))

  | RTE_snoc_head:
    forall (D D': TypeEnv) (Pi: TypeS),
    (RedTypeEnv_snoc D D') ->
    (RedTypeEnv_snoc (snoc D Pi) (snoc D' Pi))
.

Lemma RedTypeEnv_included_in_RedTypeEnv_snoc_aux1:
  forall (Pi Pi': TypeS) (D: TypeEnv),
    (RedType Pi Pi') ->
    (RedTypeEnv_snoc (Pi :: D) (Pi' :: D))
.





Lemma RedTypeEnv_included_in_RedTypeEnv_snoc_aux2:
  forall (Pi: TypeS) (D D': TypeEnv),
    (RedTypeEnv_snoc D D') ->
    (RedTypeEnv_snoc (Pi :: D) (Pi :: D'))
.




Lemma RedTypeEnv_included_in_RedTypeEnv_snoc:
  (SubRelation _ RedTypeEnv RedTypeEnv_snoc)
.


Lemma RedTypeEnv_snoc_included_in_RedTypeEnv_aux1:
  forall (Pi Pi': TypeS) (D: TypeEnv),
    (RedType Pi Pi') ->
    (RedTypeEnv (snoc D Pi) (snoc D Pi'))
.




Lemma RedTypeEnv_snoc_included_in_RedTypeEnv_aux2:
  forall (Pi: TypeS) (D D': TypeEnv),
    (RedTypeEnv D D') ->
    (RedTypeEnv (snoc D Pi) (snoc D' Pi))
.




Lemma RedTypeEnv_snoc_included_in_RedTypeEnv:
  (SubRelation _ RedTypeEnv_snoc RedTypeEnv)
.


Lemma Reduction_preserves_TypeSection_at:
  forall (D D': TypeEnv) (n: nat) (Pi: TypeS),
    (TypeSection_at D n Pi) ->
    (RedTypeEnv D D') ->
    exists Pi': TypeS,
      (TypeSection_at D' n Pi') /\
      (clos_refl _ RedType Pi Pi')
.

















Lemma Reduction_preserves_type_declaration_lookup:
  forall (D D': TypeEnv) (X: TypeVar) (Pi: TypeS),
    (decl_of_typeVar D X Pi) ->
    (RedTypeEnv D D') ->
    exists Pi': TypeS,
      (decl_of_typeVar D' X Pi') /\
      (clos_refl _ RedType Pi Pi')
.





Lemma StarReduction_preserves_type_declaration_lookup:
  forall (D D': TypeEnv) (X: TypeVar) (Pi: TypeS),
    (decl_of_typeVar D X Pi) ->
    (RedTypeEnvStar D D') ->
    exists Pi': TypeS,
      (decl_of_typeVar D' X Pi') /\
      (RedTypeStar Pi Pi')
.








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




















Lemma Well_kindedness_of_tuple:
  forall (D: TypeEnv) (Ks Ki: TypeS) (ks ki: KindS) (i: nat),
  (Type_WK D (Type_tuple Ks) (TypeTuple (Kind_tuple ks))) ->
  (TypeS_at Ks i Ki) ->
  (KindS_at ks i ki) ->
  (Type_WK D Ki (TypeConstr ki))
.








Theorem Well_kindedness_is_preserved_by_type_reduction:
  forall (D: TypeEnv) (t t': TypeS) (c: TypeC),
    (Type_WK D t c) ->
    (RedType t t') ->
    (Type_WK D t' c)
.






























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




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




Lemma Reduction_of_variable_types:
  forall (X: TypeVar) (i: nat) (R T: TypeS),
    (RedType (Var_type X i R) T) ->
    exists R': TypeS,
      T = (Var_type X i R') /\
      (RedType R R')
.



Lemma Reduction_of_variable_types_star:
  forall (X: TypeVar) (i: nat) (R T: TypeS),
    (RedTypeStar (Var_type X i R) T) ->
    exists R': TypeS,
      T = (Var_type X i R') /\
      (RedTypeStar R R')
.









Lemma Reduction_of_class_types_star:
  forall (C: ClassSym) (R T: TypeS),
    (RedTypeStar (Class_type C R) T) ->
    exists R': TypeS,
      T = (Class_type C R') /\
      (RedTypeStar R R')
.









Lemma RTS_section_inversion:
  forall (Ps Pi: TypeS),
    (RedTypeStar (Type_section Ps) Pi) ->
    exists Ps': TypeS,
      Pi = (Type_section Ps') /\
      (RedTypeStar Ps Ps')
.








Lemma Declaration_of_type_variable_is_preserved_by_reduction:
  forall (D D': TypeEnv) (X: TypeVar) (Ps: TypeS),
  (decl_of_typeVar D X (Type_section Ps)) ->
  (RedTypeEnvStar D D') ->
  exists Ps': TypeS,
    (decl_of_typeVar D' X (Type_section Ps')) /\
    (RedTypeStar Ps Ps')
.




Lemma Reduction_preserves_TypeS_at:
  forall (ts ts': TypeS) (i: nat) (t: TypeS),
    (TypeS_at ts i t) ->
    (RedType ts ts') ->
    exists t': TypeS,
      (TypeS_at ts' i t') /\
      (clos_refl _ RedType t t')
.









Lemma StarReduction_preserves_TypeS_at:
  forall (ts ts': TypeS) (i: nat) (t: TypeS),
    (TypeS_at ts i t) ->
    (RedTypeStar ts ts') ->
    exists t': TypeS,
      (TypeS_at ts' i t') /\
      (RedTypeStar t t')
.








Lemma RTS_param_inversion:
  forall (Pi T P: TypeS),
    (RedTypeStar (Type_param Pi T) P) ->
    exists Pi': TypeS, exists T': TypeS,
      P = (Type_param Pi' T') /\
      (RedTypeStar Pi Pi') /\
      (RedTypeStar T T')
.












Lemma RTS_some_inversion:
  forall (Ps Pi: TypeS),
    (RedTypeStar (Type_some Ps) Pi) ->
    exists Ps': TypeS,
      Pi = (Type_some Ps') /\
      (RedTypeStar Ps Ps')
.








Lemma TypeS_at_is_preserved_by_reduction:
  forall (Ps Ps' Pi N: TypeS) (i: nat),
    (TypeS_at Ps i (Type_param Pi (Type_some N))) ->
    (RedTypeStar Ps Ps') ->
    exists Pi': TypeS, exists N': TypeS,
      (TypeS_at Ps' i (Type_param Pi' (Type_some N'))) /\
      (RedTypeStar Pi Pi') /\
      (RedTypeStar N N')
.

Lemma Reduction_preserves_subtyping:
  forall (D D': TypeEnv) (T U T' U': TypeS),
    (Subtyping D T U) ->
    (RedTypeEnvStar D D') ->
    (RedTypeStar T T') ->
    (RedTypeStar U U') ->
    (Subtyping D' T' U')
.

























Lemma Reduction_preserves_removeBounds:
  forall (Pi Pi' x: TypeS),
    (removeBounds Pi x) ->
    (RedType Pi Pi') ->
    (removeBounds Pi' x)
.










Lemma StarReduction_preserves_removeBounds:
  forall (Pi Pi' x: TypeS),
    (removeBounds Pi x) ->
    (RedTypeStar Pi Pi') ->
    (removeBounds Pi' x)
.



Lemma RTS_snoc_left:
  forall (D D' : TypeEnv) (Pi : TypeS),
    (RedTypeEnvStar D D') ->
    (RedTypeEnvStar (snoc D Pi) (snoc D' Pi))
.




Lemma RTS_snoc_right:
  forall (D: TypeEnv) (Pi Pi' : TypeS),
    (RedTypeStar Pi Pi') ->
    (RedTypeEnvStar (snoc D Pi) (snoc D Pi'))
.




Lemma RTS_some_inversion_right:
  forall (D: TypeEnv) (t t1': TypeS),
    (Type_WK D t TypeOption) ->
    (RedTypeStar t (Type_some t1')) ->
    exists t1: TypeS,
      t = (Type_some t1) /\
      (RedTypeStar t1 t1')
.













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




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

Theorem Reduction_preserves_satisfaction:
  forall (D D': TypeEnv) (K P K' P': TypeS),
    (Type_WK D P TypeParam) ->
    (ParamSat D K P) ->
    (RedTypeEnvStar D D') ->
    (RedTypeStar K K') ->
    (RedTypeStar P P') ->
    (ParamSat D' K' P')
.










Lemma RTS_nil_inversion:
  forall (t': TypeS),
    (RedTypeStar Type_nil t') ->
    t' = Type_nil
.






Lemma RTS_cons_inversion:
  forall (t ts us: TypeS),
    (RedTypeStar (Type_cons t ts) us) ->
    exists t': TypeS, exists ts': TypeS,
      us = (Type_cons t' ts') /\
      (RedTypeStar t t') /\
      (RedTypeStar ts ts')
.












Lemma RTS_cons_inversion_right:
  forall (D: TypeEnv) (Ps Ps' P': TypeS) (i: nat),
    (Type_WK D Ps TypeParamList) ->
    (RedTypeStar Ps Ps') ->
    (TypeS_at Ps' i P') ->
    exists P: TypeS,
      (TypeS_at Ps i P) /\
      (RedTypeStar P P')
.















Lemma TypeParamList_WK_inversion:
  forall (D: TypeEnv) (i: nat) (Ps P: TypeS),
    (Type_WK D Ps TypeParamList) ->
    (TypeS_at Ps i P) ->
    (Type_WK D P TypeParam)
.

Theorem Reduction_preserves_forall_satisfaction:
  forall (D D': TypeEnv) (R Ps R' Ps': TypeS),
    (Type_WK D Ps TypeParamList) ->
    (Forall_ParamSat D R Ps) ->
    (RedTypeEnvStar D D') ->
    (RedTypeStar R R') ->
    (RedTypeStar Ps Ps') ->
    (Forall_ParamSat D' R' Ps')
.

Theorem Reduction_preserves_forall_satisfaction_build:
  forall (D D': TypeEnv) (i: nat) (R Ps R' Ps': TypeS),
    (Type_WK D Ps TypeParamList) ->
    (Forall_ParamSat_build D R i Ps) ->
    (RedTypeEnvStar D D') ->
    (RedTypeStar R R') ->
    (RedTypeStar Ps Ps') ->
    (Forall_ParamSat_build D' R' i Ps')
.







Lemma StarReduction_preserves_kind_of:
   forall (t t' : TypeS) (k : KindS),
     (kind_of t k) ->
     (RedTypeStar t t') ->
     (kind_of t' k)
.

Theorem Reduction_preserves_simultaneous_satisfaction:
  forall (D D': TypeEnv) (R R' Pi Pi': TypeS),
    (Type_WK D Pi TypeSection) ->
    (SectionSat D R Pi) ->
    (RedTypeEnvStar D D') ->
    (RedTypeStar R R') ->
    (RedTypeStar Pi Pi') ->
    (SectionSat D' R' Pi')
.












Lemma Subtyping_left_weakening:
  forall (D D': TypeEnv) (T U: TypeS),
    (Subtyping D T U) ->
    (Subtyping (D' ++ D) T U)
.




Lemma Param_satisfaction_left_weakening:
  forall (D D': TypeEnv) (K P: TypeS),
    (ParamSat D K P) ->
    (ParamSat (D' ++ D) K P)
.




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





Lemma TypeSection_at_lem9:
  forall (D: TypeEnv) (i: nat) (Pi: TypeS),
    (TypeSection_at D i Pi) ->
    i < (length D)
.


Lemma Lifting_in_closed_type_aux:
  forall (D: TypeEnv) (t: TypeS) (c: TypeC) (k n: nat),
    (Type_WK D t c) ->
    (lift_at_depth_in_type t n ((length D) + k)) = t
.





















Lemma Lifting_in_closed_type_cor1:
  forall (t: TypeS) (c: TypeC) (k n: nat),
    (Type_WK nil t c) ->
    (lift_at_depth_in_type t n k) = t
.



Lemma Lifting_in_closed_type_cor2:
  forall (Pi t: TypeS) (c: TypeC) (k n: nat),
    (Type_WK (Pi :: nil) t c) ->
    (lift_at_depth_in_type t n (S k)) = t
.


Lemma Weakening_of_subtyping:
  forall (D1 D2 D3: TypeEnv) (T U: TypeS),
    (Subtyping (D1 ++ D3) T U) ->
    (Subtyping (D1 ++ D2 ++ (lift_in_typeEnv D3 (length D2)))
               (lift_at_depth_in_type T (length D2) (length D3))
               (lift_at_depth_in_type U (length D2) (length D3)))
.











End SetProgram.