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

Require Import MatchCompNat.
Require Import Util.

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

Require Substitutions.
Module My_Substitutions := Substitutions.SetProgram(My_Program).

Import My_Substitutions.
Import My_Binders.

Inductive Subclass: ClassSym -> ClassSym -> Prop :=

  | SC_Refl:
    forall (C: ClassSym),
      (Subclass C C)
      
  | SC_Extends:
    forall (A B C: ClassSym) (Ks: TypeS),
      (classSuper A) = (Some (Class_type B Ks)) ->
      (Subclass B C) ->
      (Subclass A C)
.

Inductive Class_subtyping: TypeS -> TypeS -> Prop :=

  | CS_Refl:
    forall (C: ClassSym) (R: TypeS),
      (Class_subtyping (Class_type C R) (Class_type C R))

  | CS_Extends:
    forall (C: ClassSym) (N N': TypeS) (R: TypeS),
      (classSuper C) = (Some N) ->
      (Class_subtyping (typeSubst_in_type N 0 R) N') ->
      (Class_subtyping (Class_type C R) N')
.

Inductive TypeS_at: TypeS -> nat -> TypeS -> Prop :=

  | TypeS_at_head:
    forall (t ts: TypeS),
      (TypeS_at (Type_cons t ts) 0 t)

  | TypeS_at_tail:
    forall (t ts u: TypeS) (n: nat),
      (TypeS_at ts n u) ->
      (TypeS_at (Type_cons t ts) (S n) u)
.

Inductive kind_of: TypeS -> KindS -> Prop :=

  | Kind_of_section:
    forall (Ps: TypeS) (k: KindS),
      (kind_of Ps k) ->
      (kind_of (Type_section Ps) (Kind_tuple k))

  | Kind_of_param:
    forall (Pi T_opt: TypeS) (k: KindS),
      (kind_of Pi k) ->
      (kind_of (Type_param Pi T_opt) (Kind_constr k))

  | Kind_of_paramList_nil:
    (kind_of Type_nil Kind_nil)

  | Kind_of_paramList_cons:
    forall (P Ps: TypeS) (k: KindS) (ks: KindS),
      (kind_of P k) ->
      (kind_of Ps ks) ->
      (kind_of (Type_cons P Ps) (Kind_cons k ks))
.

Inductive KindS_at: KindS -> nat -> KindS -> Prop :=

  | Kind_at_head:
    forall (k: KindS) (ks: KindS),
      (KindS_at (Kind_cons k ks) 0 k)

  | Kind_at_tail:
    forall (ks: KindS) (k k': KindS) (n: nat),
      (KindS_at ks n k') ->
      (KindS_at (Kind_cons k ks) (S n) k')
.

Inductive TypeSection_at: TypeEnv -> nat -> TypeS -> Prop :=

  | TypeSection_at_tail:
    forall (D: TypeEnv) (Pi: TypeS),
      (TypeSection_at (snoc D Pi) 0 Pi)

  | TypeSection_at_head:
    forall (D: TypeEnv) (Pi Pi': TypeS) (n: nat),
      (TypeSection_at D n Pi') ->
      (TypeSection_at (snoc D Pi) (S n) Pi')
.

Inductive decl_of_typeVar: TypeEnv -> TypeVar -> TypeS -> Prop :=

  | decl_of_typeVar_intro:
    forall (D: TypeEnv) (X: TypeVar) (Pi: TypeS),
      (TypeSection_at D X Pi) ->
      (decl_of_typeVar D X (lift_in_type Pi (S X)))
.

Inductive RedType: TypeS -> TypeS -> Prop :=

  

  | RT_proj_sub:
    forall (R R': TypeS) (i: nat),
      (RedType R R') ->
      (RedType (Type_proj R i) (Type_proj R' i))

  | RT_proj_redex:
    forall (Ks Ki: TypeS) (i: nat),
      (TypeS_at Ks i Ki ) ->
      (RedType (Type_proj (Type_tuple Ks) i) Ki)

  | RT_fun_left:
    forall (Pi Pi': TypeS) (T: TypeS),
      (RedType Pi Pi') ->
      (RedType (Type_fun Pi T) (Type_fun Pi' T))

  | RT_fun_right:
    forall (Pi: TypeS) (T T': TypeS),
      (RedType T T') ->
      (RedType (Type_fun Pi T) (Type_fun Pi T'))

  

  | RT_apply_redex:
    forall (Pi: TypeS) (T: TypeS) (R: TypeS),
      (RedType (Type_apply (Type_fun Pi T) R) (typeSubst_in_type T 0 R))

  | RT_apply_left:
    forall (K K': TypeS) (R: TypeS),
      (RedType K K') ->
      (RedType (Type_apply K R) (Type_apply K' R))

  | RT_apply_right:
    forall (K: TypeS) (R R': TypeS),
      (RedType R R') ->
      (RedType (Type_apply K R) (Type_apply K R'))

  

  | RT_tuple:
    forall (Ks Ks': TypeS),
    (RedType Ks Ks') ->
    (RedType (Type_tuple Ks) (Type_tuple Ks'))

  

  | RT_param_left:
    forall (Pi Pi': TypeS) (T: TypeS),
      (RedType Pi Pi') ->
      (RedType (Type_param Pi T) (Type_param Pi' T))

  | RT_param_right:
    forall (Pi: TypeS) (T T': TypeS),
      (RedType T T') ->
      (RedType (Type_param Pi T) (Type_param Pi T'))

  

  | RT_section:
    forall (Ps Ps': TypeS),
      (RedType Ps Ps') ->
      (RedType (Type_section Ps) (Type_section Ps'))

  

  | RT_some:
    forall (T T': TypeS),
    (RedType T T') ->
    (RedType (Type_some T) (Type_some T'))

  

  | RT_cons_head:
    forall (t t': TypeS) (ts: TypeS),
      (RedType t t') ->
      (RedType (Type_cons t ts) (Type_cons t' ts))

  | RT_cons_tail:
    forall (t: TypeS) (ts ts': TypeS),
      (RedType ts ts') ->
      (RedType (Type_cons t ts) (Type_cons t ts'))
.

Inductive RedTypeEnv: TypeEnv -> TypeEnv -> Prop :=

  | RTE_head:
    forall (Pi Pi': TypeS) (D: TypeEnv),
      (RedType Pi Pi') ->
      (RedTypeEnv (Pi :: D) (Pi' :: D))

  | RTE_tail:
    forall (Pi: TypeS) (D D': TypeEnv),
      (RedTypeEnv D D') ->
      (RedTypeEnv (Pi :: D) (Pi :: D'))
.

Inductive Bound (D: TypeEnv): TypeS -> TypeS -> Prop :=

  | B_Class:
    forall (C: ClassSym) (R: TypeS),
      (Bound D (Class_type C R) (Class_type C R))

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

  | B_Red:
    forall (T T' N: TypeS),
      (RedType T T') ->
      (Bound D T' N) ->
      (Bound D T N)
.


End SetProgram.