Require Import List.
Require Import Arith.

Require Import MatchCompNat.
Require Import Util.

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

Require Confluence.
Module My_Confluence := Confluence.SetProgram(My_Program).
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 Substitution_preserves_class_types:
  forall (X: TypeVar) (R N: TypeS),
    (is_classType N) ->
    (is_classType (typeSubst_in_type N X R))
.



Lemma Lifting_preserves_class_types:
  forall (n k: nat) (N: TypeS),
    (is_classType N) ->
    (is_classType (lift_at_depth_in_type N n k))
.



Lemma Substitution_preserves_kind_of:
  forall (t: TypeS) (R: TypeS) (k: KindS),
    (kind_of t k) ->
    forall (X: TypeVar),
      (kind_of (typeSubst_in_type t X R) k)
.





Lemma Dropping_preserves_kind_of:
  forall (t: TypeS) (k: KindS) (d: nat),
    (kind_of t k) ->
    (kind_of (drop_at_depth_in_type t d) k)
.






Lemma typeSubst_of_snoc:
  forall (Pi: TypeS) (R: TypeS) (D: TypeEnv),
    forall (X: TypeVar),
      (typeSubst_in_typeEnv (snoc D Pi) X R) =
      (snoc (typeSubst_in_typeEnv D X R) (typeSubst_in_type Pi (X + length D) R))
.

Lemma lift_of_snoc_aux:
  forall (Pi: TypeS) (n: nat) (D: TypeEnv) (k: nat),
      (lift_at_depth_in_typeEnv (snoc D Pi) n k) =
      (snoc (lift_at_depth_in_typeEnv D n k) (lift_at_depth_in_type Pi n (k + length D)))
.



Lemma lift_of_snoc:
  forall (D: TypeEnv) (Pi: TypeS) (n: nat),
      (lift_in_typeEnv (snoc D Pi) n) =
      (snoc (lift_in_typeEnv D n) (lift_at_depth_in_type Pi n (length D)))
.


Lemma Lifting_preserves_kind_of:
  forall (t: TypeS) (k: KindS) (n: nat),
    (kind_of t k) ->
    forall (d: nat),
      (kind_of (lift_at_depth_in_type t n d) k)
.





Lemma TypeSection_at_is_a_partial_function:
  forall (ts: TypeEnv) (k: nat) (t: TypeS),
    (TypeSection_at ts k t) ->
    forall (t': TypeS),
      (TypeSection_at ts k t') ->
      (t = t')
.






Lemma decl_of_typeVar_is_a_partial_function:
  forall (D: TypeEnv) (X: TypeVar) (Pi Pi': TypeS),
    (decl_of_typeVar D X Pi) ->
    (decl_of_typeVar D X Pi') ->
    (Pi = Pi')
.




Lemma kind_of_is_a_partial_function:
  forall (t: TypeS) (k: KindS),
    (kind_of t k) ->
    forall (k': KindS),
      (kind_of t k') ->
      (k = k')
.






Lemma length_of_typeSubst:
  forall (R: TypeS) (D: TypeEnv) (X: TypeVar),
    (length (typeSubst_in_typeEnv D X R)) = (length D)
.



Lemma length_of_typeLift:
  forall (n: nat) (D: TypeEnv) (k: nat),
    (length (lift_at_depth_in_typeEnv D n k)) = (length D)
.




Lemma TypeSection_at_lem1:
  forall (D1 D2: TypeEnv) (Pi: TypeS) (k: nat),
    (TypeSection_at (D1 ++ D2) ((length D2) + k) Pi) ->
    (TypeSection_at D1 k Pi)
.







Lemma TypeSection_at_lem2:
  forall (D1 D2: TypeEnv) (Pi: TypeS) (k: nat),
    (TypeSection_at D1 k Pi) ->
    (TypeSection_at (D1 ++ D2) ((length D2) + k) Pi)
.





Lemma TypeSection_at_lem3:
  forall (D1 D2: TypeEnv) (Pi: TypeS) (k: nat),
    (TypeSection_at D2 k Pi) ->
    (TypeSection_at (D1 ++ D2) k Pi)
.



Lemma TypeSection_at_lem4:
  forall (D1 D2: TypeEnv) (Pi: TypeS) (k: nat),
    (TypeSection_at (D1 ++ D2) k Pi) ->
    (k < (length D2)) ->
    (TypeSection_at D2 k Pi)
.












Lemma TypeSection_at_lem5:
  forall (Pi R: TypeS) (D: TypeEnv) (X: TypeVar),
    (TypeSection_at D X Pi) ->
    (TypeSection_at (typeSubst_in_typeEnv D 0 R) X
                    (typeSubst_in_type Pi ((length D) - (S X)) R))
.





Lemma by_omega1: forall (x: nat), (x > 0) -> (S (pred x)) = x.

Lemma Declaration_of_type_variable_1:
  forall (D1 D2: TypeEnv) (Pi Pi' R: TypeS) (X: TypeVar),
    X > (length D2) ->
    (decl_of_typeVar (D1 ++ (Pi :: D2)) X Pi') ->
    (decl_of_typeVar (D1 ++ (typeSubst_in_typeEnv D2 0 R)) (pred X)
      (drop_in_type Pi'))
.









Lemma Declaration_of_type_variable_1_bis:
  forall (D1 D2: TypeEnv) (Pi Pi' R: TypeS) (X: TypeVar),
    X > (length D2) ->
    (decl_of_typeVar (D1 ++ (Pi :: D2)) X Pi') ->
    (decl_of_typeVar (D1 ++ (typeSubst_in_typeEnv D2 0 R)) (pred X)
      (typeSubst_in_type Pi' (length D2) R))
.








Lemma Declaration_of_type_variable_2:
  forall (D1 D2: TypeEnv) (Pi Pi' R: TypeS) (X: TypeVar),
    X < (length D2) ->
    (decl_of_typeVar (D1 ++ (Pi :: D2)) X Pi') ->
    (decl_of_typeVar (D1 ++ (typeSubst_in_typeEnv D2 0 R)) X (typeSubst_in_type Pi' (length D2) R))
.






Lemma TypeSection_at_lem6:
  forall (D1 D2: TypeEnv) (Pi: TypeS),
    (TypeSection_at (D1 ++ (Pi :: D2)) (length D2) Pi)
.




Lemma Declaration_of_type_variable_3:
  forall (D1 D2: TypeEnv) (Pi: TypeS),
    (decl_of_typeVar (D1 ++ (Pi :: D2)) (length D2) (lift_in_type Pi (S (length D2))))
.

Lemma TypeSection_at_lem7:
  forall (Pi: TypeS) (D: TypeEnv) (X: TypeVar) (n: nat),
    (TypeSection_at D X Pi) ->
    (TypeSection_at (lift_at_depth_in_typeEnv D n 0) X
                    (lift_at_depth_in_type Pi n ((length D) - (S X))))
.






Lemma TypeSection_at_lem8:
  forall (D1 D2 D3: TypeEnv) (X: TypeVar) (Pi: TypeS),
    (TypeSection_at (D1 ++ D3) X Pi) ->
    (TypeSection_at (D1 ++ D2 ++ D3)
                    (lift_at_depth_in_typeVar X (length D2) (length D3))
                     Pi)
.

Lemma Weakening_of_type_declaration_by_the_right:
  forall (D1 D2 D3: TypeEnv) (X: TypeVar) (Pi: TypeS),
    (decl_of_typeVar (D1 ++ D3) X Pi) ->
    (decl_of_typeVar
      (D1 ++ D2 ++ (lift_in_typeEnv D3 (length D2)))
      (lift_at_depth_in_typeVar X (length D2) (length D3))
      (lift_at_depth_in_type Pi (length D2) (length D3)))
.

Lemma Weakening_of_well_kindedness_by_the_right_aux:
  forall (D1 D2 D: TypeEnv) (s: TypeS) (c: TypeC),
    (Type_WK D s c) ->
    forall (D3: TypeEnv),
      D = (D1 ++ D3) ->
      (Type_WK (D1 ++ D2 ++ (lift_in_typeEnv D3 (length D2)))
         (lift_at_depth_in_type s (length D2) (length D3)) c)
.

Lemma Weakening_of_well_kindedness_by_the_right:
  forall (D: TypeEnv) (s: TypeS) (c: TypeC),
    (Type_WK D s c) ->
    forall (D': TypeEnv),
      (Type_WK (D ++ D') (lift_in_type s (length D')) c)
.

Lemma Weakening_of_well_kindedness_by_the_right_snoc:
  forall (D: TypeEnv) (s Pi: TypeS) (c: TypeC),
    (Type_WK D s c) ->
    (Type_WK (snoc D Pi) (lift_in_type s 1) c)
.



Lemma TypeSection_at_lem1_cor1:
  forall (D1 D2 : TypeEnv) (Pi : TypeS) (k : nat),
    k >= (length D2) ->
    (TypeSection_at (D1 ++ D2) k Pi) ->
    (TypeSection_at D1 (k - (length D2)) Pi)
.



Theorem Weakening_of_type_declaration:
  forall (D1 D2 D3: TypeEnv) (X: TypeVar) (Pi: TypeS),
    (decl_of_typeVar (D1 ++ D3) X Pi) ->
    (decl_of_typeVar (D1 ++ D2 ++ (lift_in_typeEnv D3 (length D2)))
                     (lift_at_depth_in_typeVar X (length D2) (length D3))
                     (lift_at_depth_in_type Pi (length D2) (length D3)))
.












Theorem Weakening_of_well_kindedness:
  forall (D1 D2 D3: TypeEnv) (t: TypeS) (c: TypeC),
    (Type_WK (D1 ++ D3) t c) ->
    (Type_WK (D1 ++ D2 ++ (lift_in_typeEnv D3 (length D2)))
             (lift_at_depth_in_type t (length D2) (length D3)) c)
.

Lemma Type_substitution_preserves_well_kindedness:
  forall (D1: TypeEnv) (Pi R: TypeS) (k: KindS),
    (Type_WK D1 R (TypeTuple k)) ->
    (kind_of Pi k) ->
    forall (D: TypeEnv) (s: TypeS) (c: TypeC),
      (Type_WK D s c) ->
      forall (D2: TypeEnv),
        D = (D1 ++ (Pi :: D2)) ->
        (Type_WK (D1 ++ (typeSubst_in_typeEnv D2 0 R))
                 (typeSubst_in_type s (length D2) R) c)
.



















Lemma Substitution_preserves_well_kindedness_snoc:
  forall (D : TypeEnv) (Pi R : TypeS) (k : KindS) (s : TypeS) (c : TypeC),
    (Type_WK D R (TypeTuple k)) ->
    (kind_of Pi k) ->
    (Type_WK (snoc D Pi) s c) ->
    (Type_WK D (typeSubst_in_type s 0 R) c)
.


Lemma Type_substitution_preserves_well_kindedness_cor1:
  forall (Pi1 Pi2 R: TypeS) (k: KindS) (t: TypeS) (c: TypeC),
    (Type_WK nil R (TypeTuple k)) ->
    (kind_of Pi1 k) ->
    (Type_WK (Pi1 :: Pi2 :: nil) t c) ->
    (Type_WK ((typeSubst_in_type Pi2 0 R) :: nil)
             (typeSubst_in_type t 1 R) c)
.


Lemma Type_substitution_preserves_well_kindedness_cor2:
  forall (Pi R : TypeS) (k : KindS) (t : TypeS) (c : TypeC),
    (Type_WK nil R (TypeTuple k)) ->
    (kind_of Pi k) ->
    (Type_WK (Pi :: nil) t c) ->
    (Type_WK nil (typeSubst_in_type t 0 R) c)
.

Lemma Weakening_of_type_declaration_by_the_left:
  forall (D1 D2: TypeEnv) (X: TypeVar) (Pi: TypeS),
    (decl_of_typeVar D2 X Pi) ->
    (decl_of_typeVar (D1 ++ D2) X Pi)
.

Lemma Weakening_of_well_kindedness_by_the_left:
  forall (D1 D2: TypeEnv) (t: TypeS) (c: TypeC),
    (Type_WK D2 t c) ->
    (Type_WK (D1 ++ D2) t c)
.













Hint Rewrite snoc_of_append snoc_of_cons: snoc_rewrite.


Lemma Lifting_preserves_kind_of_reverse:
  forall (t: TypeS) (k: KindS) (n: nat) (d: nat),
    (kind_of (lift_at_depth_in_type t n d) k) ->
    (kind_of t k)
.















Lemma Forall2_app:
  forall (A B: Set) (P: A -> B -> Prop) (xs1 xs2: (list A)) (ys1 ys2: (list B)),
    (Forall2 P xs1 ys1) ->
    (Forall2 P xs2 ys2) ->
    (Forall2 P (xs1 ++ xs2) (ys1 ++ ys2))
.





Lemma TypeSection_at_implies_List_from:
  forall (D: TypeEnv) (i: nat) (Pi: TypeS),
    (TypeSection_at D i Pi) ->
    (List_from D i Pi)
.


Lemma List_from_implies_TypeSection_at:
  forall (D: TypeEnv) (i: nat) (Pi: TypeS),
    (List_from D i Pi) ->
    (TypeSection_at D i Pi)
.


Lemma TypeSection_at_and_kind_of:
  forall (D1 D2: TypeEnv) (X: TypeVar) (Pi1: TypeS) (k: KindS),
  (Forall2 (fun Pi1 Pi2 => forall (k: KindS),
    (kind_of Pi1 k) ->(kind_of Pi2 k)) D1 D2) ->
  (TypeSection_at D1 X Pi1) ->
  (kind_of Pi1 k) ->
  exists Pi2: TypeS,
    (TypeSection_at D2 X Pi2) /\
    (kind_of Pi2 k)
.




Lemma decl_of_typeVar_and_kind_of:
  forall (D1 D2: TypeEnv) (X: TypeVar) (Pi1: TypeS) (k: KindS),
    (Forall2 (fun Pi1 Pi2 => forall (k: KindS),
      (kind_of Pi1 k) ->(kind_of Pi2 k)) D1 D2) ->
    (decl_of_typeVar D1 X Pi1) ->
    (kind_of Pi1 k) ->
    exists Pi2: TypeS,
      (decl_of_typeVar D2 X Pi2) /\
      (kind_of Pi2 k)
.







Lemma decl_of_typeVar_and_kind_of_cor1:
  forall (D1 D2: TypeEnv) (X: TypeVar) (Pi Pi' Pi1: TypeS) (k k1: KindS),
    (kind_of Pi k) ->
    (kind_of Pi' k) ->
    (decl_of_typeVar (D1 ++ Pi :: D2) X Pi1) ->
    (kind_of Pi1 k1) ->
    exists Pi2: TypeS,
      (decl_of_typeVar (D1 ++ Pi' :: D2) X Pi2) /\
      (kind_of Pi2 k1)
.







Theorem Well_kindedness_does_not_depend_on_bounds:
  forall (D1 D2: TypeEnv) (t Pi Pi': TypeS) (c: TypeC) (k: KindS),
    (kind_of Pi k) ->
    (kind_of Pi' k) ->
    (Type_WK (D1 ++ Pi :: D2) t c) ->
    (Type_WK (D1 ++ Pi' :: D2) t c)
.












End SetProgram.