Library Progress_proofs
Require Import List.
Require Import Util.
Require Syntax.
Module SetProgram(My_Program: Syntax.Program).
Import My_Program.
Require TransitivityElimination_proofs.
Module My_TransitivityElimination_proofs := TransitivityElimination_proofs.SetProgram(My_Program).
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.
Lemma evaluated_term_dec:
forall (t: Term),
(evaluated_term t) \/ ~(evaluated_term t)
.
Lemma Progress_aux_1:
forall (f: FieldSym) (fts: Term),
(In f (fields_of_fieldTermList fts)) ->
exists t: Term,
(fieldTerm_lookup fts f t)
.
Lemma evaluated_term_new_inversion:
forall (D: TypeEnv) (G: TermEnv) (t: Term) (T: TypeS),
(Term_WT D G t (TermI T)) ->
(evaluated_term t) ->
exists N: TypeS, exists fts: Term,
t = (Term_new N fts) /\
(Term_WT D G fts (FieldTermListI N))
.
Lemma KindS_at_is_a_partial_function:
forall (ks k k': KindS) (i: nat),
(KindS_at ks i k) ->
(KindS_at ks i k') ->
(k = k')
.
Inductive SameCategory: TypeC -> TypeC -> Prop :=
| SameCategory_TypeConstr:
forall (k k': KindS),
(SameCategory (TypeConstr k) (TypeConstr k'))
| SameCategory_Type_:
(SameCategory Type_ Type_)
| SameCategory_TypeTuple:
forall (k k': KindS),
(SameCategory (TypeTuple k) (TypeTuple k'))
| SameCategory_TypeParam:
(SameCategory TypeParam TypeParam)
| SameCategory_TypeSection:
(SameCategory TypeSection TypeSection)
| SameCategory_TypeOption:
(SameCategory TypeOption TypeOption)
| SameCategory_TypeParamList:
(SameCategory TypeParamList TypeParamList)
| SameCategory_TypeConstrList:
forall (k k': KindS),
(SameCategory (TypeConstrList k) (TypeConstrList k'))
.
Lemma Uniqueness_of_well_kindedness:
forall (D: TypeEnv) (t: TypeS) (c1 c2: TypeC),
(Type_WK D t c1) ->
(Type_WK D t c2) ->
(SameCategory c1 c2) ->
(c1 = c2)
.
Lemma Satisfaction_implies_same_kind:
forall (D: TypeEnv) (R Pi: TypeS) (k: KindS),
(Type_WK D R (TypeTuple k)) ->
(SectionSat D R Pi) ->
(kind_of Pi k)
.
Lemma Substitution_in_field_type:
forall (D: TypeEnv) (f: FieldSym) (R: TypeS),
let C := (fieldOwner f) in
let T := (fieldType f) in
(Type_WK D (Class_type C R) Type_) ->
(Type_WK D (typeSubst_in_type T 0 R) Type_)
.
Lemma Substitution_in_method_type_params:
forall (D: TypeEnv) (m: MethodSym) (R: TypeS),
let C := (methodOwner m) in
let Pim := (methodTypeParams m) in
(Type_WK D (Class_type C R) Type_) ->
(Type_WK D (typeSubst_in_type Pim 0 R) TypeSection)
.
Lemma Substitution_in_method_type:
forall (D: TypeEnv) (m: MethodSym) (R R': TypeS),
let C := (methodOwner m) in
let T := (methodType m) in
let Pi := (methodTypeParams m) in
(Type_WK D (Class_type C R) Type_) ->
(SectionSat D R' (typeSubst_in_type Pi 0 R)) ->
(Type_WK D (typeSubst_in_type (typeSubst_in_type T 1 R) 0 R') Type_)
.
Lemma Substitution_in_method_param_types:
forall (D: TypeEnv) (m: MethodSym) (R R': TypeS),
let C := (methodOwner m) in
let Ts := (methodParams m) in
let Pi := (methodTypeParams m) in
(Type_WK D (Class_type C R) Type_) ->
(SectionSat D R' (typeSubst_in_type Pi 0 R)) ->
(List_forall
(fun T => (Type_WK D (typeSubst_in_type (typeSubst_in_type T 1 R) 0 R') Type_))
Ts)
.
Lemma Substitution_in_method_param_types_2:
forall (D: TypeEnv) (m: MethodSym) (R: TypeS),
let C := (methodOwner m) in
let Ts := (methodParams m) in
let Pim := (methodTypeParams m) in
(Type_WK D (Class_type C R) Type_) ->
(List_forall
(fun T => (Type_WK (D ++ (typeSubst_in_type Pim 0 R) :: nil)
(typeSubst_in_type T 1 R) Type_))
Ts)
.
Lemma Substitution_in_method_type_2:
forall (D: TypeEnv) (m: MethodSym) (R: TypeS),
let C := (methodOwner m) in
let T := (methodType m) in
let Pim := (methodTypeParams m) in
(Type_WK D (Class_type C R) Type_) ->
(Type_WK (D ++ (typeSubst_in_type Pim 0 R) :: nil)
(typeSubst_in_type T 1 R) Type_)
.
Definition Info_WK (D: TypeEnv) (info: TermInfo): Prop :=
match info with
| (TermI T) => (Type_WK D T Type_)
| (TermListI Ts) => List_forall (fun T => (Type_WK D T Type_)) Ts
| (FieldTermListI N) => True
end.
Theorem Typing_returns_well_kinded_types:
forall (D: TypeEnv) (G: TermEnv) (t: Term) (info: TermInfo),
(Term_WT D G t info) ->
(List_forall (fun T => (Type_WK D T Type_)) G) ->
(Info_WK D info)
.
Lemma Typing_returns_well_kinded_types_cor1:
forall (D: TypeEnv) (G: TermEnv) (t: Term) (T: TypeS),
(Term_WT D G t (TermI T)) ->
(List_forall (fun T => (Type_WK D T Type_)) G) ->
(Type_WK D T Type_)
.
Progress