Proofs about Substitution for a Local Variable |
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_SubstitutionLemmas2.
Module My_Proofs_SubstitutionLemmas2 := Proofs_SubstitutionLemmas2.SetProgram(My_Program).
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.
Substitution of the value v for the variable k in a list of types Ts
|
Fixpoint map_varSubst_in_typeList (Ts: TypeList) (k: nat) (v: Value) {struct Ts}: TypeList :=
match Ts with
| nil => nil
| T :: Ts' => (varSubst_in_type T k v) :: (map_varSubst_in_typeList Ts' (S k) v)
end
.
Lemma zero_fv_and_varSubst_0:
forall (p: Path) (k: nat) (v: Value),
~(varset_In 0 (fv_in_path p)) ->
~(varset_In 0 (fv_in_path (varSubst_in_path p (S k) v)))
.
Lemma zero_fv_and_varSubst_2:
forall (T: type) (k: nat) (v: Value),
~(varset_In 0 (fv_in_type T)) ->
~(varset_In 0 (fv_in_type (varSubst_in_type T (S k) v)))
.
Lemma lemmaA39_var_aux_1:
forall (Ts: TypeList) (k: nat) (v: Value),
(length (map_varSubst_in_typeList Ts k v)) = (length Ts)
.
Lemma lemmaA39_var_aux_2:
forall (Ts: TypeList) (n: nat) (T: type) (v: Value),
(TypeList_at Ts n T) ->
(TypeList_at (map_varSubst_in_typeList Ts 0 v) n (varSubst_in_type T n v))
.
Lemma lemmaA39_var_aux_3:
forall (T: type),
(forall (k : VarSym), (var_in_type k T) -> (k < 0)) ->
(fv_in_type T = empty_varset)
.
Lemma lemmaA39_var_aux_4:
forall (T: type),
(forall (n: nat), ~(varset_In n (fv_in_type T))) ->
(fv_in_type T = empty_varset)
.
Lemma lemmaA39_var_aux_5:
forall (xts: ParamTermList) (k: nat) (v: Value),
(params_of_paramTermList (varSubst_in_paramTermList xts k v)) =
(params_of_paramTermList xts)
.
Lemma lemmaA39_var_aux_6:
forall (fts: FieldTermList) (k: nat) (v: Value),
(fields_of_fieldTermList (varSubst_in_fieldTermList fts k v)) =
(fields_of_fieldTermList fts)
.
Lemma lemmaA39_var_aux_7:
forall (Ts Us: TypeList) (v: Value),
(map_varSubst_in_typeList (Ts ++ Us) 0 v) =
(map_varSubst_in_typeList Ts 0 v) ++ (map_varSubst_in_typeList Us (length Ts) v)
.
Lemma lemmaA39_var_aux_8:
forall (T: type),
(fv_in_type T = empty_varset) ->
(forall (k : VarSym), (var_in_type k T) -> (k < 0))
.
Definition lemmaA39_var_prop1 (G: Env) (p: Path) (T: type) (H: (Gen_PathTyping G p T)): Prop :=
forall (U: type) (Us: TypeList),
(G = (Env_mk Owner_root nil (U :: Us))) ->
(context_is_well_formed G) ->
forall (v: Value) (N: nat),
N = (length Us) ->
(Gen_PathTyping rootEnv (Path_value v) U) ->
(Gen_PathTyping (Env_mk Owner_root nil (map_varSubst_in_typeList Us 0 v))
(varSubst_in_path p N v) (varSubst_in_type T N v)
)
.
Definition lemmaA39_var_prop2 (G: Env) (S1 S2: type) (H: (Gen_Subtyping G S1 S2)): Prop :=
forall (U: type) (Us: TypeList),
(G = (Env_mk Owner_root nil (U :: Us))) ->
(context_is_well_formed G) ->
forall (v: Value) (N: nat),
N = (length Us) ->
(Gen_PathTyping rootEnv (Path_value v) U) ->
(Gen_Subtyping (Env_mk Owner_root nil (map_varSubst_in_typeList Us 0 v))
(varSubst_in_type S1 N v) (varSubst_in_type S2 N v)
)
.
Definition lemmaA39_var_prop3 (G: Env) (C: ClassSym) (fvs: FieldValueList)
(H: (Gen_FieldValueListTyping G C fvs)): Prop :=
forall (U: type) (Us: TypeList),
(G = (Env_mk Owner_root nil (U :: Us))) ->
(context_is_well_formed G) ->
forall (v: Value) (N: nat),
N = (length Us) ->
(Gen_PathTyping rootEnv (Path_value v) U) ->
(Gen_FieldValueListTyping (Env_mk Owner_root nil (map_varSubst_in_typeList Us 0 v))
C fvs
)
.
Lemma lemmaA39_var_main:
forall (G: Env) (p: Path) (T: type) (H: (Gen_PathTyping G p T)),
(lemmaA39_var_prop1 G p T H)
.
| Subtitution lemmas -- Var -- path |
Lemma lemmaA39_var_0:
forall (G: Env) (U: type) (Us: TypeList) (p: Path) (T: type),
(G = (Env_mk Owner_root nil (U :: Us))) ->
(context_is_well_formed G) ->
(Gen_PathTyping G p T) ->
forall (v: Value) (N: nat),
N = (length Us) ->
(Gen_PathTyping rootEnv (Path_value v) U) ->
(Gen_PathTyping (Env_mk Owner_root nil (map_varSubst_in_typeList Us 0 v))
(varSubst_in_path p N v) (varSubst_in_type T N v)
)
.
| Subtitution lemmas -- Var -- type |
Lemma lemmaA39_var_2:
forall (G: Env) (U: type) (Us: TypeList) (S1 S2: type),
(G = (Env_mk Owner_root nil (U :: Us))) ->
(context_is_well_formed G) ->
(Gen_Subtyping G S1 S2) ->
forall (v: Value) (N: nat),
N = (length Us) ->
(Gen_PathTyping rootEnv (Path_value v) U) ->
(Gen_Subtyping (Env_mk Owner_root nil (map_varSubst_in_typeList Us 0 v))
(varSubst_in_type S1 N v) (varSubst_in_type S2 N v)
)
.
Definition lemmaA39_var1_prop1 (G: Env) (t: Term) (T: type) (H: (Typing G t T)): Prop :=
forall (U: type) (Us: TypeList),
(G = (Env_mk Owner_root nil (U :: Us))) ->
(context_is_well_formed G) ->
forall (v: Value) (N: nat),
N = (length Us) ->
(Gen_PathTyping rootEnv (Path_value v) U) ->
(Typing (Env_mk Owner_root nil (map_varSubst_in_typeList Us 0 v))
(varSubst_in_term t N v) (varSubst_in_type T N v)
)
.
Definition lemmaA39_var1_prop2 (G: Env) (p: Path) (m: MethodSym) (xts: ParamTermList) (H: (ParamTermListTyping G p m xts)): Prop :=
forall (U: type) (Us: TypeList),
(G = (Env_mk Owner_root nil (U :: Us))) ->
(context_is_well_formed G) ->
forall (v: Value) (N: nat),
N = (length Us) ->
(Gen_PathTyping rootEnv (Path_value v) U) ->
(ParamTermListTyping (Env_mk Owner_root nil (map_varSubst_in_typeList Us 0 v))
(varSubst_in_path p N v)
m
(varSubst_in_paramTermList xts N v)
)
.
Definition lemmaA39_var1_prop3 (G: Env) (C: ClassSym) (fts: FieldTermList) (H: (FieldTermListTyping G C fts)): Prop :=
forall (U: type) (Us: TypeList),
(G = (Env_mk Owner_root nil (U :: Us))) ->
(context_is_well_formed G) ->
forall (v: Value) (N: nat),
N = (length Us) ->
(Gen_PathTyping rootEnv (Path_value v) U) ->
(FieldTermListTyping (Env_mk Owner_root nil (map_varSubst_in_typeList Us 0 v))
C (varSubst_in_fieldTermList fts N v)
)
.
| Subtitution lemmas -- Var -- term |
Lemma lemmaA39_var_1:
forall (G: Env) (U: type) (Us: TypeList) (t: Term) (T: type),
(G = (Env_mk Owner_root nil (U :: Us))) ->
(context_is_well_formed G) ->
(Typing G t T) ->
forall (v: Value) (N: nat),
N = (length Us) ->
(Gen_PathTyping rootEnv (Path_value v) U) ->
(Typing (Env_mk Owner_root nil (map_varSubst_in_typeList Us 0 v))
(varSubst_in_term t N v) (varSubst_in_type T N v)
)
.
| Subtitution lemmas -- Var -- term | Corollary |
Lemma lemmaA39_var_1_corollary:
forall (v: Value) (U: type) (t: Term) (T: type),
(Typing (Env_mk Owner_root nil (U :: nil)) t T) ->
(Gen_PathTyping rootEnv (Path_value v) U) ->
(Typing rootEnv (varSubst_in_term t 0 v) (varSubst_in_type T 0 v))
.
End SetProgram.