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

Require Import Util.

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

Require TermSubstitutionInTyping.
Module My_TermSubstitutionInTyping := TermSubstitutionInTyping.SetProgram(My_Program).
Import My_TermSubstitutionInTyping.

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 BetaType: TypeS -> TypeS -> Prop :=

  | BetaType_step:
    forall (t u: TypeS),
      (RedType t u) ->
      (BetaType t u)

  | BetaType_refl:
    forall (t: TypeS),
      (BetaType t t)

  | BetaType_sym:
    forall (t u: TypeS),
      (BetaType t u) ->
      (BetaType u t)

  | BetaType_trans:
    forall (t1 t2 t3: TypeS),
      (BetaType t1 t2) ->
      (BetaType t2 t3) ->
      (BetaType t1 t3)
.


Lemma Class_type_subtyping_injection_aux1:
  forall (C C': ClassSym) (R R': TypeS),
    (Class_subtyping (Class_type C R) (Class_type C' R')) ->
    (Class_type C R) = (Class_type C' R') \/
    (Rplus classInheritance C C')
.












Lemma Accessibility_is_anti_reflexive:
  forall (A: Set) (R: A -> A -> Prop) (x: A),
    (Acc R x) ->
    ~(R x x)
.



Lemma Class_inheritance_is_anti_reflexive:
  forall (C: ClassSym),
    ~(Rplus classInheritance C C)
.



Lemma Class_type_subtyping_injection:
  forall (C: ClassSym) (R R': TypeS),
  (Class_subtyping (Class_type C R) (Class_type C R')) ->
  R = R'
.



Lemma Class_type_subtyping_is_linear:
  forall (N N1 N2: TypeS),
  (Class_subtyping N N1) ->
  (Class_subtyping N N2) ->
  (Class_subtyping N1 N2) \/ (Class_subtyping N2 N1)
.






Theorem Uniqueness_of_class_type_subtyping:
  forall (A B: ClassSym) (R R1 R2: TypeS),
    (Class_subtyping (Class_type A R) (Class_type B R1)) ->
    (Class_subtyping (Class_type A R) (Class_type B R2)) ->
    R1 = R2
.



Lemma Class_subtyping_aux1:
  forall (C B: ClassSym) (R R' RB': TypeS),
    (RedTypeStar R R') ->
    (Class_subtyping (Class_type C R') (Class_type B RB')) ->
    exists RB: TypeS,
      (Class_subtyping (Class_type C R) (Class_type B RB)) /\
      (RedTypeStar RB RB')
.
















Lemma RedTypeStar_implies_BetaType:
  forall (t t': TypeS),
    (RedTypeStar t t') ->
    (BetaType t t')
.



Lemma SubtypingWTR_implies_class_type_subtyping:
  forall (D: TypeEnv) (C1 C2: ClassSym) (R1 R2: TypeS),
    (SubtypingWTR D (Class_type C1 R1) (Class_type C2 R2)) ->
    exists R2': TypeS,
      (Class_subtyping (Class_type C1 R1) (Class_type C2 R2')) /\
      (BetaType R2 R2')
.




























Theorem Uniqueness_of_subtyping:
  forall (A B: ClassSym) (R R1 R2: TypeS),
    (Type_WK nil (Class_type A R) Type_) ->
    (Type_WK nil (Class_type B R1) Type_) ->
    (Type_WK nil (Class_type B R2) Type_) ->
    (Subtyping nil (Class_type A R) (Class_type B R1)) ->
    (Subtyping nil (Class_type A R) (Class_type B R2)) ->
    (BetaType R1 R2)
.









Theorem ChurchRosser:
  forall (t u: TypeS),
    (BetaType t u) ->
    exists s: TypeS,
      (RedTypeStar t s) /\
      (RedTypeStar u s)
.










Lemma BetaType_implies_subtyping_lem1:
  forall (D: TypeEnv) (T R R': TypeS) (k: nat),
    (BetaType R R') ->
    (Subtyping D (typeSubst_in_type T k R) (typeSubst_in_type T k R'))
.






Lemma classTypeParams_closed:
  forall (C: ClassSym) (k: nat) (R: TypeS),
    let Pi := (classTypeParams C) in
    (typeSubst_in_type Pi k R) = Pi
.


Lemma methodTypeParams_closed:
  forall (m: MethodSym) (k: nat) (R: TypeS),
    let Pi := (methodTypeParams m) in
    (typeSubst_in_type Pi (S k) R) = Pi
.


Lemma methodType_closed:
  forall (m: MethodSym) (k: nat) (R: TypeS),
    let T := (methodType m) in
    (typeSubst_in_type T (S (S k)) R) = T
.


Lemma methodParams_closed:
  forall (m: MethodSym) (k: nat) (R: TypeS),
    let Ts := (methodParams m) in
    (typeSubst_in_termEnv Ts (S (S k)) R) = Ts
.



Inductive Conform (D: TypeEnv) (C: ClassSym) (R: TypeS): Prop :=

  | Conform_intro:
    (Type_WK D (Class_type C R) Type_) ->
    
    (SectionSat D R (classTypeParams C)) ->
    (Conform D C R)
.

Theorem Class_subtyping_subject_reduction:
  forall (D: TypeEnv) (C C': ClassSym) (R R': TypeS),
    let N := (Class_type C R) in
    let N' := (Class_type C' R') in
    (TypeEnv_WK D) ->
    (Conform D C R) ->
    (Class_subtyping N N') ->
    (Conform D C' R')
.






















End SetProgram.