Require Import List.

Require Import Util.
Require Import WellFoundation.

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

Require Normalization_proofs.
Module My_Normalization_proofs := Normalization_proofs.SetProgram(My_Program).
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 SubtypingWTR: TypeEnv -> TypeS -> TypeS -> Prop :=

  | SWTR_Refl:
    forall (D: TypeEnv) (T: TypeS),
      (SubtypingWTR D T T)

  | SWTR_Var:
    forall (D: TypeEnv) (X: TypeVar) (i: nat) (R Ps Pi N N': TypeS),
      (decl_of_typeVar D X (Type_section Ps)) ->
      (TypeS_at Ps i (Type_param Pi (Type_some N))) ->
      (SubtypingWTR D (typeSubst_in_type N 0 R) N') ->
      (SubtypingWTR D (Var_type X i R) N')

  | SWTR_Class:
    forall (D: TypeEnv) (C: ClassSym) (R: TypeS) (N N': TypeS),
      (classSuper C) = (Some N) ->
      (SubtypingWTR D (typeSubst_in_type N 0 R) N') ->
      (SubtypingWTR D (Class_type C R) N')

  | SWTR_Beta_Left:
    forall (D: TypeEnv) (T T' U: TypeS),
      (RedType T T') ->
      (SubtypingWTR D T' U) ->
      (SubtypingWTR D T U)

  | SWTR_Beta_Right:
    forall (D: TypeEnv) (T U' U: TypeS),
      (RedType U U') ->
      (SubtypingWTR D T U') ->
      (SubtypingWTR D T U)
.

Inductive TypeExp: TypeEnv -> TypeS -> TypeS -> Prop :=







  | TE_Class:
    forall (D: TypeEnv) (C: ClassSym) (R: TypeS) (N: TypeS),
      (classSuper C) = (Some N) ->
      (TypeExp D (Class_type C R) (typeSubst_in_type N 0 R))

  | TE_Beta:
    forall (D: TypeEnv) (T T': TypeS),
      (RedType T T') ->
      (TypeExp D T T')
.


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



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

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






















Lemma Class_type_expansion_preserves_well_kindedness:
  forall (D: TypeEnv) (C: ClassSym) (R N: TypeS),
  (Type_WK D (Class_type C R) Type_) ->
  (classSuper C) = (Some N) ->
  (Type_WK D (typeSubst_in_type N 0 R) Type_)
.





Lemma classtype_expansion_preserves_well_kindedness_1:
  forall (D: TypeEnv) (C C': ClassSym) (R R': TypeS),
  (Type_WK D (Class_type C R) Type_) ->
  (classSuper C) = (Some (Class_type C' R')) ->
  (Type_WK D (Class_type C' (typeSubst_in_type R' 0 R)) Type_)
.





Lemma Type_expansion_is_well_founded_aux1:
  forall (D: TypeEnv) (C: ClassSym) (R: TypeS),
    (Type_WK D (Class_type C R) Type_) ->
    (TypeEnv_WK D) ->
    (Acc (symRel (TypeExp D)) (Class_type C R))
.

















Lemma Type_expansion_is_well_founded:
  forall (D: TypeEnv) (T: TypeS),
    (TypeEnv_WK D) ->
    (Type_WK D T Type_) ->
    (Acc (symRel (TypeExp D)) T)
.










Lemma SWTR_Trans_aux:
    forall (T S U: TypeS),
    (Acc (symRel (TypeExp nil)) T) ->
    (Acc (symRel (TypeExp nil)) S) ->
    (Acc (symRel (TypeExp nil)) U) ->
    (SubtypingWTR nil T S) ->
    (SubtypingWTR nil S U) ->
    (SubtypingWTR nil T U)
.
































Lemma SWTR_Trans:
  forall (T S U: TypeS),
    (Type_WK nil T Type_) ->
    (Type_WK nil S Type_) ->
    (Type_WK nil U Type_) ->
    (SubtypingWTR nil T S) ->
    (SubtypingWTR nil S U) ->
    (SubtypingWTR nil T U)
.



Lemma TransitivityElimination_aux:
  forall (T U: TypeS),
    (Acc (symRel (TypeExp nil)) T) ->
    (Acc (symRel (TypeExp nil)) U) ->
    (Subtyping nil T U) ->
    (SubtypingWTR nil T U)
.
















Theorem TransitivityElimination:
  forall (T U: TypeS),
    (Type_WK nil T Type_) ->
    (Type_WK nil U Type_) ->
    (Subtyping nil T U) ->
    (SubtypingWTR nil T U)
.



Lemma SubtypingWTR_is_consistent_with_subclassing:
  forall (D: TypeEnv) (C C': ClassSym) (R R': TypeS),
    (SubtypingWTR D (Class_type C R) (Class_type C' R')) ->
    (Subclass C C')
.

















Theorem Subtyping_is_consistent_with_subclassing:
  forall (C C': ClassSym) (R R': TypeS),
    (Type_WK nil (Class_type C R) Type_) ->
    (Type_WK nil (Class_type C' R') Type_) ->
    (Subtyping nil (Class_type C R) (Class_type C' R')) ->
    (Subclass C C')
.


End SetProgram.