Proof of the Subject Reduction Property |
Require Import Calculus.
Require Import Arith.
Require Import MatchCompNat.
Require Import Util.
Require Import List.
Require Import ListSet.
Module SetProgram(My_Program: Program).
Import My_Program.
Require Proofs_SubstitutionLemmas3.
Module My_Proofs_SubstitutionLemmas3 := Proofs_SubstitutionLemmas3.SetProgram(My_Program).
Import My_Proofs_SubstitutionLemmas3.
Import My_Proofs_SubstitutionLemmas2.
Import My_Proofs_SubstitutionLemmas.
Import My_Proofs_DeBruijnSIndices.
Import My_Proofs_Progress.
Import My_Proofs_AdmissibilityOfTransitivity.
Import My_Proofs_Subclassing.
Import My_Proofs_TypeOrdering.
Import My_Proofs_Miscellaneous.
Import My_WellFormedness.
Import My_Semantics.
Import My_Typing.
Import My_TypeOrdering.
Import My_DeBruijn.
Import My_Substitutions.
Import My_Subclassing.
Lemma lemmaA40_aux_1:
forall (G: Env) (C: ClassSym) (fvs: FieldValueList)
(f: FieldSym) (v: Value) (T: type),
(Gen_FieldValueListTyping G C fvs) ->
(FieldValueList_contains fvs f v) ->
(fieldType f) = T ->
exists U: type,
(Gen_PathTyping G (Path_value v) U) /\
(type_is_closed U) /\
(Subtyping (classEnv C) U T)
.
Lemma lemmaA40_aux_2:
forall (v: Value),
(thisSubst_in_paramTypeList nil (Path_value v)) = nil
.
Lemma lemmaA40_aux_3:
forall (v: Value),
(thisSubst_in_typeList nil (Path_value v)) = nil
.
Lemma lemmaA40_aux_5:
forall (xts: ParamTermList) (xts': ParamTermList),
(Red_paramTermList xts xts') ->
(params_of_paramTermList xts) = (params_of_paramTermList xts')
.
Lemma lemmaA40_aux_16:
forall (fts: FieldTermList) (fts': FieldTermList),
(Red_fieldTermList fts fts') ->
(fields_of_fieldTermList fts) = (fields_of_fieldTermList fts')
.
Lemma lemmaA40_aux_6:
forall (x: ParamSym) (T Tp: type) (m: MethodSym) (p: Path),
(In (x, Tp) (thisSubst_in_paramTypeList (method_parameters m) p)) ->
(paramType x) = T ->
(paramOwner x) = m /\ Tp = (thisSubst_in_type T p)
.
Inductive ParamValueListTyping: Env -> Path -> ParamValueList -> Prop :=
| ParamValueListTyping_nil:
forall (G : Env) (p : Path),
(ParamValueListTyping G p nil)
| ParamValueListTyping_cons:
forall (G : Env) (p : Path) (x : ParamSym) (v : Value) (xvs : ParamValueList) (T : type),
(paramType x = T) ->
(Gen_PathTyping G (Path_value v) (thisSubst_in_type T p)) ->
(ParamValueListTyping G p xvs) ->
(ParamValueListTyping G p ((x, v) :: xvs))
.
Lemma lemmaA40_aux_7:
forall (G: Env) (xvs: ParamValueList) (xts: ParamTermList) (p: Path) (m: MethodSym),
(ParamTermListTyping G p m xts) ->
(paramValueList_to_ParamTermList xvs = xts) ->
(ParamValueListTyping G p xvs)
.
Lemma lemmaA40_aux_11:
forall (xvs: ParamValueList) (xts: ParamTermList),
(paramValueList_to_ParamTermList xvs) = xts ->
(params_of_paramValueList xvs) = (params_of_paramTermList xts)
.
Lemma lemmaA40_aux_12:
forall (m: MethodSym) (xs: (list ParamSym)),
(IsComplete_params m xs) ->
(List_sublist _ (params_of_paramTypeList (method_parameters m)) xs)
.
Lemma lemmaA40_aux_13:
forall (xTs: ParamTypeList) (p: Path),
(params_of_paramTypeList (thisSubst_in_paramTypeList xTs p)) =
(params_of_paramTypeList xTs)
.
Lemma lemmaA40_aux_14:
forall (G: Env) (p: Path) (xvs: ParamValueList) (x: ParamSym) (v: Value) (T: type),
(ParamValueListTyping G p xvs) ->
(In (x, v) xvs) ->
(paramType x = T) ->
(Gen_PathTyping G (Path_value v) (thisSubst_in_type T p))
.
Lemma lemmaA40_aux_15:
forall (xvs: ParamValueList) (m: MethodSym) (p: Path),
(ParamValueListTyping rootEnv p xvs) ->
(args_are_correct xvs (thisSubst_in_paramTypeList (method_parameters m) p))
.
Definition lemmaA40_prop1 (G: Env) (t: Term) (T: type) (H: (Typing G t T)): Prop :=
G = rootEnv ->
forall (u: Term),
(Red_term t u) ->
(Typing rootEnv u T)
.
Definition lemmaA40_prop2 (G: Env) (p: Path) (m: MethodSym) (xts: ParamTermList) (H: (ParamTermListTyping G p m xts)): Prop :=
G = rootEnv ->
forall (xts': ParamTermList),
(Red_paramTermList xts xts') ->
(ParamTermListTyping rootEnv p m xts')
.
Definition lemmaA40_prop3 (G: Env) (C: ClassSym) (fts: FieldTermList) (H: (FieldTermListTyping G C fts)): Prop :=
G = rootEnv ->
forall (fts': FieldTermList),
(Red_fieldTermList fts fts') ->
(FieldTermListTyping rootEnv C fts')
.
| Subject-reduction |
Lemma lemmaA40:
forall (T: type) (t u: Term),
(Typing rootEnv t T) ->
(Red_term t u) ->
(Typing rootEnv u T)
.
rewrite <- R1.
eapply lemmaA3_3. apply H16. trivial.
simpl in H18. tauto.
assert (
forall (x: ParamSym) (U: type),
(paramType x) = U ->
(paramOwner x) = m ->
(fp_in_type (thisSubst_in_type U (Path_value v))) = empty_paramset
).
intros.
rewrite <- (H14 x U H15 H16).
apply new_lemma2_2.
simpl. trivial.
clear H13 H14.
assert (context_is_well_formed
(Env_mk Owner_root (thisSubst_in_paramTypeList (method_parameters m) (Path_value v)) nil)
).
apply context_is_well_formed_intro.
apply forall_is_listForall.
intros.
destruct x. rename p1 into x. rename t0 into Uv.
pose (U:= (paramType x)).
assert ((paramType x) = U). trivial.
destruct (lemmaA40_aux_6 _ _ _ _ _ H13 H14).
rewrite H17.
eapply H15. apply H14. trivial.
unfold local_types_well_formed.
simpl. tauto. clear H15.
assert (Typing rootEnv
(map_paramSubst_in_term (thisSubst_in_term t (Path_value v)) xvs)
(map_paramSubst_in_type (thisSubst_in_type S (Path_value v)) xvs)
).
unfold rootEnv.
replace (nil (A:= type)) with (map_paramSubst_in_typeList nil xvs).
eapply lemmaA39_param_1 with
(xTs:= (thisSubst_in_paramTypeList (method_parameters m) (Path_value v)))
(Us:= (nil (A:= type)))
(G:= (Env_mk Owner_root
(thisSubst_in_paramTypeList (method_parameters m) (Path_value v))
nil))
. trivial. trivial. trivial.
unfold args_conform_to_params.
split.
rewrite lemmaA40_aux_13.
apply lemmaA40_aux_12.
rewrite (lemmaA40_aux_11 xvs xts). trivial. trivial.
apply lemmaA40_aux_15.
eapply lemmaA40_aux_7.
rewrite <- H0. apply p0. trivial.
simpl. trivial.
clear H12 H13.
assert (Kinding (classEnv C) S).
eapply methodTypes_are_well_formed. apply e. trivial.
assert ((fp_in_type S) = empty_paramset).
unfold empty_paramset.
apply empty_is_empty_2 with (A:= ParamSym). apply ParamSym_eq.
intros.
fold (paramset_In x (fp_in_type S)).
intro.
cut (In x (paramTypeList_to_paramList nil)). simpl. tauto.
eapply lemmaA3_3. unfold classEnv in H12. apply H12. trivial.
assert (
(map_paramSubst_in_type (thisSubst_in_type S (Path_value v)) xvs) =
(thisSubst_in_type S (Path_value v))
).
cut ((map_paramSubst_in_path (Path_value v) xvs) = (Path_value v)). intros.
pattern (Path_value v) at 2. rewrite <- H15.
apply lemmaA9_2.
intros. unfold param_in_type. rewrite H13. simpl. tauto.
rewrite polySubst_in_pathValue. trivial.
rewrite H15 in H14. clear H15.
eapply lemmaA1. apply H14.
rewrite <- H0. trivial.
intros. red. intros.
inversion H1.
clear H4 fts0. clear H2 C0. clear H3 H1 u.
apply T_New.
assert ((fields_of_fieldTermList fts) = (fields_of_fieldTermList fts')).
apply lemmaA40_aux_16. trivial.
rewrite <- H1. trivial.
eapply H. trivial. trivial.
assert ((fields_of_fieldTermList fts) = (fields_of_fieldTermList fts')).
apply lemmaA40_aux_16. trivial.
rewrite <- H1. trivial.
rewrite <- H0. trivial.
intros. red. intros.
inversion H2.
eapply T_Let. rewrite H1 in e. apply e.
apply H. trivial. trivial. apply t1. trivial.
rewrite <- H1. trivial.
clear u0 H2 H4. clear T0 H3. clear t2 H5. clear u1 H6.
rewrite H1 in e.
clear H0.
unfold rootEnv in e. injection e; intros. clear e.
rewrite <- H0 in t1. simpl in t1. clear H0.
rewrite <- H2 in t1. clear H2.
rewrite <- H3 in t1. clear O H3.
clear H.
assert (Gen_PathTyping rootEnv (Path_value v) T).
apply lemmaA40_aux_8. rewrite H7. rewrite <- H1. trivial.
clear t0 H7.
cut ((fv_in_type U) = empty_varset). intros.
apply lemmaA1 with (T:= U).
rewrite <- (lemmaA37_2 U 0 v).
eapply lemmaA39_var_1_corollary. apply t1. trivial.
trivial.
rewrite <- (lemmaA31_2 U). rewrite <- H1. trivial.
trivial.
unfold empty_varset.
apply empty_is_empty_2 with (A:= VarSym). apply VarSym_eqdec.
intros. intro.
destruct x.
apply n.
apply fv_and_var_in_type2. trivial.
fold (varset_In (Datatypes.S x) (fv_in_type U)) in H0.
assert ((Datatypes.S x) < (length (T :: nil))).
eapply lemmaA4_1. apply t1.
unfold varset_In. unfold varset_union.
apply set_union_intro2. trivial.
simpl in H2.
assert (x < 0). omega.
unfold lt in H3.
apply (le_Sn_O x). trivial.
intros. red. intros.
inversion H0.
intros. red. intros.
inversion H2.
clear x0 t1 xts0 xts' H2 H3 H5 H6 H4.
eapply ParamTermListTyping_cons. apply e.
apply H. trivial. trivial. rewrite <- H1. trivial.
clear x0 t1 xts0 H3 H4 H6.
eapply ParamTermListTyping_cons. apply e.
rewrite <- H1. trivial.
apply H0. trivial. trivial.
intros. red. intros.
inversion H0.
intros. red. intros.
inversion H2.
clear f1 t2 fts0 fts' H2 H3 H5 H6 H4.
eapply FieldTermListTyping_cons.
apply H. trivial. trivial. trivial. apply e. trivial.
rewrite <- H1. trivial.
clear f1 t2 fts0 H3 H4 H6.
eapply FieldTermListTyping_cons.
rewrite <- H1. apply t0. trivial. apply e. trivial.
apply H0. trivial. trivial.
Qed.
End SetProgram.