Library Proofs_SubjectReduction

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')

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
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.
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))
. trivial. trivial. trivial.
unfold args_conform_to_params.
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.
fold (paramset_In x (fp_in_type S)).
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.
rewrite <- (lemmaA31_2 U). rewrite <- H1. 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.

End SetProgram.

This page has been generated by coqdoc