Proofs about Substitution for Parameters |
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_SubstitutionLemmas.
Module My_Proofs_SubstitutionLemmas := Proofs_SubstitutionLemmas.SetProgram(My_Program).
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.
| Substitution for this in a list of types |
Definition map_paramSubst_in_typeList (Ts: TypeList) (xvs: ParamValueList): TypeList :=
(map (fun T => (map_paramSubst_in_type T xvs)) Ts)
.
Predicate: list ys contains, at least, all elements of xs
|
Definition List_sublist (A: Set) (xs ys: (list A)): Prop :=
forall (x: A), (In x xs) -> (In x ys)
.
Predicate: bindings of xvs conforms to all corresponding bindings in xTs
|
Definition args_are_correct (xvs: ParamValueList) (xTs: ParamTypeList) :=
forall (x: ParamSym) (v: Value) (T: type),
(In (x, v) xvs) ->
(In (x, T) xTs) ->
(Gen_PathTyping rootEnv (Path_value v) T)
.
Definition params_of_paramValueList (xvs: ParamValueList): (list ParamSym) :=
(map (fun (xv: (ParamSym * Value)) => let (x, v) := xv in x) xvs)
.
Definition params_of_paramTypeList (xTs: ParamTypeList): (list ParamSym) :=
(map (fun (xT: (ParamSym * type)) => let (x, T) := xT in x) xTs)
.
Predicate: a list of arguments xvs conforms to a list of typed parameters xTs
|
Definition args_conform_to_params (xvs: ParamValueList) (xTs: ParamTypeList): Prop :=
(List_sublist _ (params_of_paramTypeList xTs) (params_of_paramValueList xvs)) /\
(args_are_correct xvs xTs)
.
Definition lemmaA39_param_prop1 (G: Env) (p: Path) (T: type) (H: (Gen_PathTyping G p T)): Prop :=
forall (xTs: ParamTypeList) (Us: TypeList),
(G = (Env_mk Owner_root xTs Us)) ->
(context_is_well_formed G) ->
forall (xvs: ParamValueList),
(args_conform_to_params xvs xTs) ->
(Gen_PathTyping (Env_mk Owner_root nil (map_paramSubst_in_typeList Us xvs))
(map_paramSubst_in_path p xvs) (map_paramSubst_in_type T xvs)
)
.
Definition lemmaA39_param_prop2 (G: Env) (T U: type) (H: (Gen_Subtyping G T U)): Prop :=
forall (xTs: ParamTypeList) (Us: TypeList),
(G = (Env_mk Owner_root xTs Us)) ->
(context_is_well_formed G) ->
forall (xvs: ParamValueList),
(args_conform_to_params xvs xTs) ->
(Gen_Subtyping (Env_mk Owner_root nil (map_paramSubst_in_typeList Us xvs))
(map_paramSubst_in_type T xvs) (map_paramSubst_in_type U xvs)
)
.
Definition lemmaA39_param_prop3 (G: Env) (C: ClassSym) (fvs: FieldValueList)
(H: (Gen_FieldValueListTyping G C fvs)): Prop :=
forall (xTs: ParamTypeList) (Us: TypeList),
(G = (Env_mk Owner_root xTs Us)) ->
(context_is_well_formed G) ->
forall (xvs: ParamValueList),
(args_conform_to_params xvs xTs) ->
(Gen_FieldValueListTyping (Env_mk Owner_root nil (map_paramSubst_in_typeList Us xvs))
C fvs
)
.
Lemma lemmaA39_param_main:
forall (G: Env) (p: Path) (T: type) (H: (Gen_PathTyping G p T)),
(lemmaA39_param_prop1 G p T H)
.
| Subtitution lemmas -- path |
Lemma lemmaA39_param_0:
forall (G: Env) (xTs: ParamTypeList) (Us: TypeList) (p: Path) (T: type),
(G = (Env_mk Owner_root xTs Us)) ->
(context_is_well_formed G) ->
(Gen_PathTyping G p T) ->
forall (xvs: ParamValueList),
(args_conform_to_params xvs xTs) ->
(Gen_PathTyping (Env_mk Owner_root nil (map_paramSubst_in_typeList Us xvs))
(map_paramSubst_in_path p xvs) (map_paramSubst_in_type T xvs)
)
.
| Subtitution lemmas -- type |
Lemma lemmaA39_param_2:
forall (G: Env) (xTs: ParamTypeList) (Us: TypeList) (T U: type),
(G = (Env_mk Owner_root xTs Us)) ->
(context_is_well_formed G) ->
(Gen_Subtyping G T U) ->
forall (xvs: ParamValueList),
(args_conform_to_params xvs xTs) ->
(Gen_Subtyping (Env_mk Owner_root nil (map_paramSubst_in_typeList Us xvs))
(map_paramSubst_in_type T xvs) (map_paramSubst_in_type U xvs)
)
.
Lemma lemmaA39_param_aux_1:
forall (xts: ParamTermList) (xvs: ParamValueList),
(params_of_paramTermList (map_paramSubst_in_paramTermList xts xvs)) =
(params_of_paramTermList xts)
.
Lemma lemmaA39_param_aux_2:
forall (fts: FieldTermList) (xvs: ParamValueList),
(fields_of_fieldTermList (map_paramSubst_in_fieldTermList fts xvs)) =
(fields_of_fieldTermList fts)
.
Lemma lemmaA39_param_aux_3:
forall (Ts: TypeList) (i: nat),
(local_types_well_formed_aux Ts i) ->
(local_types_well_formed_aux Ts (S i))
.
Lemma lemmaA39_param_aux_4:
forall (Ts: TypeList) (T: type) (i: nat),
(local_types_well_formed_aux Ts i) ->
(forall (k: VarSym), (varset_In k (fv_in_type T)) -> k < (length Ts) + i) ->
(local_types_well_formed_aux (Ts ++ T :: nil) i)
.
Lemma lemmaA39_param_aux_4_corollary:
forall (Ts: TypeList) (T: type),
(local_types_well_formed Ts) ->
(forall (k: VarSym), (varset_In k (fv_in_type T)) -> k < (length Ts)) ->
(local_types_well_formed (Ts ++ T :: nil))
.
Definition lemmaA39_param1_prop1 (G: Env) (t: Term) (T: type) (H: (Typing G t T)): Prop :=
forall (xTs: ParamTypeList) (Us: TypeList),
(G = (Env_mk Owner_root xTs Us)) ->
(context_is_well_formed G) ->
forall (xvs: ParamValueList),
(args_conform_to_params xvs xTs) ->
(Typing (Env_mk Owner_root nil (map_paramSubst_in_typeList Us xvs))
(map_paramSubst_in_term t xvs) (map_paramSubst_in_type T xvs)
)
.
Definition lemmaA39_param1_prop2 (G: Env) (p: Path) (m: MethodSym) (xts: ParamTermList) (H: (ParamTermListTyping G p m xts)): Prop :=
forall (xTs: ParamTypeList) (Us: TypeList),
(G = (Env_mk Owner_root xTs Us)) ->
(context_is_well_formed G) ->
forall (xvs: ParamValueList),
(args_conform_to_params xvs xTs) ->
(ParamTermListTyping (Env_mk Owner_root nil (map_paramSubst_in_typeList Us xvs))
(map_paramSubst_in_path p xvs)
m
(map_paramSubst_in_paramTermList xts xvs)
)
.
Definition lemmaA39_param1_prop3 (G: Env) (C: ClassSym) (fts: FieldTermList) (H: (FieldTermListTyping G C fts)): Prop :=
forall (xTs: ParamTypeList) (Us: TypeList),
(G = (Env_mk Owner_root xTs Us)) ->
(context_is_well_formed G) ->
forall (xvs: ParamValueList),
(args_conform_to_params xvs xTs) ->
(FieldTermListTyping (Env_mk Owner_root nil (map_paramSubst_in_typeList Us xvs))
C (map_paramSubst_in_fieldTermList fts xvs)
)
.
| Subtitution lemmas -- term |
Lemma lemmaA39_param_1:
forall (G: Env) (xTs: ParamTypeList) (Us: TypeList) (t: Term) (T: type),
(G = (Env_mk Owner_root xTs Us)) ->
(context_is_well_formed G) ->
(Typing G t T) ->
forall (xvs: ParamValueList),
(args_conform_to_params xvs xTs) ->
(Typing (Env_mk Owner_root nil (map_paramSubst_in_typeList Us xvs))
(map_paramSubst_in_term t xvs) (map_paramSubst_in_type T xvs)
)
.
End SetProgram.