Library SubjectReduction_proofs
Require Import List.
Require Import Arith.
Require Import MatchCompNat.
Require Import Util.
Require Syntax.
Module SetProgram(My_Program: Syntax.Program).
Import My_Program.
Require SubjectReduction_preliminaries.
Module My_SubjectReduction_preliminaries := SubjectReduction_preliminaries.SetProgram(My_Program).
Import My_SubjectReduction_preliminaries.
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.
Lemma Typed_term_list:
forall (D: TypeEnv) (G: TermEnv) (ts: Term) (Ts: (list TypeS)),
(Term_WT D G ts (TermListI Ts)) ->
(Forall2 (fun t T => (Term_WT D G t (TermI T))) (list_of_termList ts) Ts)
.
Inductive FieldVal_WF (D: TypeEnv) (G: TermEnv) (N: TypeS)
(f: FieldSym) (t: Term): Prop :=
| FieldVal_WF_intro:
forall (S R: TypeS),
let C := (fieldOwner f) in
let T := (fieldType f) in
(Type_WK D N Type_) ->
(Subtyping D N (Class_type C R)) ->
(Type_WK D (Class_type C R) Type_) ->
(Term_WT D G t (TermI S)) ->
(Subtyping D S (typeSubst_in_type T 0 R)) ->
(FieldVal_WF D G N f t)
.
Lemma Well_formed_field_value:
forall (D: TypeEnv) (G: TermEnv) (N: TypeS) (f: FieldSym) (t fts: Term),
(Term_WT D G fts (FieldTermListI N)) ->
(fieldTerm_lookup fts f t) ->
(FieldVal_WF D G N f t)
.
Lemma Term_reduction_preserves_fields_of_fieldTermList:
forall (D: TypeEnv) (G: TermEnv) (N: TypeS) (fts fts': Term),
(Term_WT D G fts (FieldTermListI N)) ->
(RedTerm fts fts') ->
(fields_of_fieldTermList fts') =
(fields_of_fieldTermList fts)
.
Lemma Class_subtyping_implies_subtyping:
forall (D: TypeEnv) (C C': ClassSym) (R R': TypeS),
(Class_subtyping (Class_type C R) (Class_type C' R')) ->
(Subtyping D (Class_type C R) (Class_type C' R'))
.
Lemma Self_type_is_well_kinded:
forall (C: ClassSym),
let Pi := (classTypeParams C) in
(Type_WK (Pi :: nil) (Class_type C (Type_var 0)) Type_)
.
Lemma Type_env_reduction_preserves_typing:
forall (D D': TypeEnv) (G: TermEnv) (t: Term) (info: TermInfo),
(RedTypeEnvStar D D') ->
(Term_WT D G t info) ->
(Term_WT D' G t info)
.
Lemma RTS_class_type:
forall (C: ClassSym) (R R': TypeS),
(RedTypeStar R R') ->
(RedTypeStar (Class_type C R) (Class_type C R'))
.
Lemma RTE_head_star:
forall (D: TypeEnv) (T T': TypeS),
(RedTypeStar T T') ->
(RedTypeEnvStar (T :: D) (T' :: D))
.
Lemma RTE_tail_star:
forall (D D': TypeEnv) (T: TypeS),
(RedTypeEnvStar D D') ->
(RedTypeEnvStar (T :: D) (T :: D'))
.
Lemma Subject_reduction_case_T_call_redex_aux1:
forall (m: MethodSym) (Ci: ClassSym) (R Ri Ri0 R' Rm S: TypeS),
let C := (methodOwner m) in
let Pim := (methodTypeParams m) in
let T := (methodType m) in
let PiCi := (classTypeParams Ci) in
(Type_WK nil (Class_type C R) Type_) ->
(Type_WK (PiCi :: nil) (Class_type C Ri0) Type_) ->
(Type_WK nil (Class_type C (typeSubst_in_type Ri0 0 Ri)) Type_) ->
(Conform nil Ci Ri) ->
(SectionSat nil Rm (typeSubst_in_type Pim 0 R)) ->
(SectionSat nil Rm (typeSubst_in_type Pim 0 R')) ->
(RedTypeStar R R') ->
(RedTypeStar (typeSubst_in_type Ri0 0 Ri) R') ->
let D := (PiCi :: (typeSubst_in_type Pim 0 Ri0) :: nil) in
(Type_WK D S Type_) ->
(Subtyping D S (typeSubst_in_type T 1 Ri0)) ->
(Subtyping nil
(typeSubst_in_type (typeSubst_in_type S 1 Ri) 0 Rm)
(typeSubst_in_type (typeSubst_in_type T 1 R) 0 Rm))
.
Lemma Subject_reduction_case_T_call_redex_aux2:
forall (m: MethodSym) (Ci: ClassSym) (R Ri Ri0 R' Rm S: TypeS) (tb: Term),
let C := (methodOwner m) in
let Pim := (methodTypeParams m) in
let Ts := (methodParams m) in
let PiCi := (classTypeParams Ci) in
(Type_WK nil (Class_type C R) Type_) ->
(Type_WK (PiCi :: nil) (Class_type C Ri0) Type_) ->
(Type_WK nil (Class_type C (typeSubst_in_type Ri0 0 Ri)) Type_) ->
(Conform nil Ci Ri) ->
(SectionSat nil Rm (typeSubst_in_type Pim 0 R')) ->
(RedTypeStar R R') ->
(RedTypeStar (typeSubst_in_type Ri0 0 Ri) R') ->
let D := (PiCi :: (typeSubst_in_type Pim 0 Ri0) :: nil) in
let G := ((Class_type Ci (Type_var 1)) :: (typeSubst_in_termEnv Ts 1 Ri0)) in
(TermEnv_WK D G) ->
(Term_WT D G tb (TermI S)) ->
let G0 := ((Class_type Ci Ri) ::
(typeSubst_in_termEnv
(typeSubst_in_termEnv Ts 1 (typeSubst_in_type Ri0 0 Ri)) 0 Rm)) in
(Term_WT nil G0
(typeSubst_in_term (typeSubst_in_term tb 1 Ri) 0 Rm)
(TermI (typeSubst_in_type (typeSubst_in_type S 1 Ri) 0 Rm)))
.
Lemma Subject_reduction_case_T_call_redex_aux3:
forall (m: MethodSym) (Ci: ClassSym) (R Ri Ri0 R' Rm S N: TypeS) (tb t ts: Term)
(Ss: (list TypeS)),
let C := (methodOwner m) in
let Pim := (methodTypeParams m) in
let Ts := (methodParams m) in
let PiCi := (classTypeParams Ci) in
(Type_WK nil (Class_type C R) Type_) ->
(Type_WK (PiCi :: nil) (Class_type C Ri0) Type_) ->
(Type_WK nil (Class_type C (typeSubst_in_type Ri0 0 Ri)) Type_) ->
(Conform nil Ci Ri) ->
(SectionSat nil Rm (typeSubst_in_type Pim 0 R')) ->
(RedTypeStar R R') ->
(RedTypeStar (typeSubst_in_type Ri0 0 Ri) R') ->
(Term_WT nil nil t (TermI N)) ->
(Subtyping nil N (Class_type Ci Ri)) ->
let Ts1 := (typeSubst_in_termEnv (typeSubst_in_termEnv Ts 1 R) 0 Rm) in
(Term_WT nil nil ts (TermListI Ss)) ->
(Pointwise_subtyping nil Ss Ts1) ->
let Ts' := (typeSubst_in_termEnv (typeSubst_in_termEnv
Ts 1 (typeSubst_in_type Ri0 0 Ri)) 0 Rm) in
let Us := ((Class_type Ci Ri) :: Ts') in
let tb1 := (typeSubst_in_term (typeSubst_in_term tb 1 Ri) 0 Rm) in
let S1 := (typeSubst_in_type (typeSubst_in_type S 1 Ri) 0 Rm) in
(Term_WT nil Us tb1 (TermI S1)) ->
exists S': TypeS,
(Term_WT nil nil (polyTermSubst_in_term tb1 0 (t :: (list_of_termList ts)))
(TermI S')) /\
(Subtyping nil S' S1)
.
Lemma Subject_reduction_case_T_call_redex_aux4:
forall (m: MethodSym) (Ci: ClassSym) (R Ri Ri0 R' Rm S N: TypeS) (tb t ts: Term)
(Ss: (list TypeS)),
let C := (methodOwner m) in
let Pim := (methodTypeParams m) in
let Ts := (methodParams m) in
let T := (methodType m) in
let PiCi := (classTypeParams Ci) in
let D := (PiCi :: (typeSubst_in_type Pim 0 Ri0) :: nil) in
let G := ((Class_type Ci (Type_var 1)) :: (typeSubst_in_termEnv Ts 1 Ri0)) in
(Type_WK nil (Class_type C R) Type_) ->
(Type_WK (PiCi :: nil) (Class_type C Ri0) Type_) ->
(Type_WK nil (Class_type C (typeSubst_in_type Ri0 0 Ri)) Type_) ->
(Conform nil Ci Ri) ->
(SectionSat nil Rm (typeSubst_in_type Pim 0 R)) ->
(SectionSat nil Rm (typeSubst_in_type Pim 0 R')) ->
(RedTypeStar R R') ->
(RedTypeStar (typeSubst_in_type Ri0 0 Ri) R') ->
(Type_WK D S Type_) ->
(Subtyping D S (typeSubst_in_type T 1 Ri0)) ->
(Term_WT nil nil t (TermI N)) ->
(Subtyping nil N (Class_type Ci Ri)) ->
let Ts1 := (typeSubst_in_termEnv (typeSubst_in_termEnv Ts 1 R) 0 Rm) in
(Term_WT nil nil ts (TermListI Ss)) ->
(Pointwise_subtyping nil Ss Ts1) ->
(Term_WT D G tb (TermI S)) ->
(TermEnv_WK D G) ->
let tb1 := (typeSubst_in_term (typeSubst_in_term tb 1 Ri) 0 Rm) in
exists S': TypeS,
(Term_WT nil nil (polyTermSubst_in_term tb1 0 (t :: (list_of_termList ts)))
(TermI S')) /\
(Subtyping nil S' (typeSubst_in_type (typeSubst_in_type T 1 R) 0 Rm))
.
Theorem Subject_reduction:
forall (t u: Term) (info: TermInfo),
(Term_WT nil nil t info) ->
(RedTerm t u) ->
exists info': TermInfo,
(Term_WT nil nil u info') /\
(SubInfo nil info' info)
.
End SetProgram.