Proofs about Substitution for the Current Instance |
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_DeBruijnSIndices.
Module My_Proofs_DeBruijnSIndices := Proofs_DeBruijnSIndices.SetProgram(My_Program).
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.
Predicate: P is true for all elements of the list xs
|
Fixpoint list_forall (A: Set) (xs: (list A)) (P: A -> Prop) {struct xs}: Prop :=
match xs with
| nil => True
| x :: xs' => (P x) /\ (list_forall A xs' P)
end
.
Lemma listForall_is_forall:
forall (A: Set) (xs: (list A)) (P: A -> Prop),
(list_forall A xs P) -> (forall (x: A), (In x xs) -> (P x))
.
Lemma forall_is_listForall:
forall (A: Set) (xs: (list A)) (P: A -> Prop),
(forall (x: A), (In x xs) -> (P x)) -> (list_forall A xs P)
.
Predicate: for all i in 0,|Ts|-1, for all k in fv(Ts_i), k < i
|
Fixpoint local_types_well_formed_aux (Ts: TypeList) (i: nat) {struct Ts}: Prop :=
match Ts with
| nil => True
| T :: Ts' =>
(forall (k: VarSym), (var_in_type k T) -> (k < i)) /\
(local_types_well_formed_aux Ts' (S i))
end
.
Definition local_types_well_formed (Ts: TypeList): Prop :=
(local_types_well_formed_aux Ts 0)
.
| Well-formed contexts |
Inductive context_is_well_formed: Env -> Prop :=
| context_is_well_formed_intro:
forall (O: Owner) (xTs: ParamTypeList) (Ts: TypeList),
(list_forall _ xTs (fun xT => let (x, T) := xT in (fp_in_type T) = empty_paramset)) ->
(local_types_well_formed Ts) ->
(context_is_well_formed (Env_mk O xTs Ts))
.
Definition lemmaA40_aux_4_prop1 (v: Value): Prop :=
forall (G: Env) (T: type),
(Gen_PathTyping G (Path_value v) T) ->
(Typing G (value_to_term v) T)
.
Definition lemmaA40_aux_4_prop2 (fvs: FieldValueList): Prop :=
forall (G: Env) (C: ClassSym),
(Gen_FieldValueListTyping G C fvs) ->
(FieldTermListTyping G C (fieldValueList_to_fieldTermList fvs))
.
Lemma lemmaA40_aux_4:
forall (G: Env) (v: Value) (T: type),
(Gen_PathTyping G (Path_value v) T) ->
(Typing G (value_to_term v) T)
.
rewrite temp_lemma. trivial.
apply H. trivial.
rewrite temp_lemma. trivial. trivial.
red. intros. simpl.
apply FieldTermListTyping_nil.
red. intros. simpl.
rename f0 into fvs.
inversion_clear H1.
eapply FieldTermListTyping_cons.
apply H. apply H2. trivial. apply H4. trivial.
apply H0. trivial.
Qed.
Definition lemmaA40_aux_8_prop1 (v: Value): Prop :=
forall (G: Env) (T: type),
(Typing G (value_to_term v) T) ->
(Gen_PathTyping G (Path_value v) T)
.
Definition lemmaA40_aux_8_prop2 (fvs: FieldValueList): Prop :=
forall (G: Env) (C: ClassSym),
(FieldTermListTyping G C (fieldValueList_to_fieldTermList fvs)) ->
(Gen_FieldValueListTyping G C fvs)
.
Lemma lemmaA40_aux_8:
forall (G: Env) (v: Value) (T: type),
(Typing G (value_to_term v) T) ->
(Gen_PathTyping G (Path_value v) T)
.
rewrite temp_lemma1 in H1. trivial.
apply H. trivial.
rewrite temp_lemma1 in H3. trivial. trivial.
red. intros. simpl.
apply Gen_FieldValueListTyping_nil.
red. intros. simpl.
rename f0 into fvs.
inversion_clear H1.
eapply Gen_FieldValueListTyping_cons.
apply H. apply H2. trivial. apply H4. trivial.
apply H0. trivial.
Qed.
Lemma lemmaA40_aux_9:
forall (G: Env) (p: Path) (T: type),
(Gen_PathTyping G p T) ->
(Typing G (path_to_term p) T)
.
Lemma lemmaA40_aux_10:
forall (G: Env) (p: Path) (T: type),
(Typing G (path_to_term p) T) ->
(Gen_PathTyping G p T)
.
Definition lemmaA38_0_prop1 (G: Env) (p: Path) (T: type) (H: (Gen_PathTyping G p T)): Prop :=
forall (xTs: ParamTypeList) (Ts Us: TypeList),
G = (Env_mk Owner_root nil Ts) ->
(Gen_PathTyping (Env_mk Owner_root xTs (app Us Ts)) p T)
.
Definition lemmaA38_0_prop2 (G: Env) (C: ClassSym) (fvs: FieldValueList) (H: (Gen_FieldValueListTyping G C fvs)): Prop :=
forall (xTs: ParamTypeList) (Ts Us: TypeList),
G = (Env_mk Owner_root nil Ts) ->
(Gen_FieldValueListTyping (Env_mk Owner_root xTs (app Us Ts)) C fvs)
.
Definition lemmaA38_0_prop3 (G: Env) (T U: type) (H: (Gen_Subtyping G T U)): Prop :=
forall (xTs: ParamTypeList) (Ts Us: TypeList),
G = (Env_mk Owner_root nil Ts) ->
(Gen_Subtyping (Env_mk Owner_root xTs (app Us Ts)) T U)
.
Lemma lemmaA38_0:
forall (xTs: ParamTypeList) (Ts Us: TypeList) (p: Path) (T: type),
(Gen_PathTyping (Env_mk Owner_root nil Ts) p T) ->
(Gen_PathTyping (Env_mk Owner_root xTs (app Us Ts)) p T)
.
Lemma lemmaA38_2:
forall (xTs: ParamTypeList) (Ts Us: TypeList) (T U: type),
(Gen_Subtyping (Env_mk Owner_root nil Ts) T U) ->
(Gen_Subtyping (Env_mk Owner_root xTs (app Us Ts)) T U)
.
Lemma lemmaA38_0_corollary:
forall (xTs: ParamTypeList) (Ts: TypeList) (p: Path) (T: type),
(Gen_PathTyping rootEnv p T) ->
(Gen_PathTyping (Env_mk Owner_root xTs Ts) p T)
.
| Substitution for this in a list of types |
Definition thisSubst_in_typeList (Ts: TypeList) (p: Path): TypeList :=
(map (fun T => (thisSubst_in_type T p)) Ts)
.
| Substitution for this in a list of bindings (Param * Type) |
Definition thisSubst_in_paramTypeList (xTs: ParamTypeList) (p: Path): ParamTypeList :=
(map (fun xT => match xT with (x, T) => (x, (thisSubst_in_type T p)) end) xTs)
.
Lemma lemmaA1_for_paths:
forall (G: Env) (p: Path) (T U: type),
(Gen_PathTyping G p T) ->
(Gen_Subtyping G T U) ->
(Gen_PathTyping G p U)
.
Definition lemmaA39_this_prop1 (G: Env) (p: Path) (T: type) (H: (Gen_PathTyping G p T)): Prop :=
forall (C: ClassSym) (xTs: ParamTypeList) (Us: TypeList),
G = (Env_mk (Owner_class C) xTs Us) ->
forall (v: Value),
(Gen_PathTyping rootEnv (Path_value v) (type_class C)) ->
(Gen_PathTyping (Env_mk Owner_root (thisSubst_in_paramTypeList xTs (Path_value v)) (thisSubst_in_typeList Us (Path_value v)))
(thisSubst_in_path p (Path_value v)) (thisSubst_in_type T (Path_value v))
)
.
Definition lemmaA39_this_prop2 (G: Env) (T U: type) (H: (Gen_Subtyping G T U)): Prop :=
forall (C: ClassSym) (xTs: ParamTypeList) (Us: TypeList),
G = (Env_mk (Owner_class C) xTs Us) ->
forall (v: Value),
(Gen_PathTyping rootEnv (Path_value v) (type_class C)) ->
(Gen_Subtyping (Env_mk Owner_root (thisSubst_in_paramTypeList xTs (Path_value v)) (thisSubst_in_typeList Us (Path_value v)))
(thisSubst_in_type T (Path_value v)) (thisSubst_in_type U (Path_value v))
)
.
Definition lemmaA39_this_prop3 (G: Env) (A: ClassSym) (fvs: FieldValueList) (H: (Gen_FieldValueListTyping G A fvs)): Prop :=
forall (C: ClassSym) (xTs: ParamTypeList) (Us: TypeList),
G = (Env_mk (Owner_class C) xTs Us) ->
forall (v: Value),
(Gen_PathTyping rootEnv (Path_value v) (type_class C)) ->
(Gen_FieldValueListTyping (Env_mk Owner_root (thisSubst_in_paramTypeList xTs (Path_value v)) (thisSubst_in_typeList Us (Path_value v)))
A fvs
)
.
Lemma lemmaA39_this_main:
forall (G: Env) (p: Path) (T: type) (H: (Gen_PathTyping G p T)),
(lemmaA39_this_prop1 G p T H)
.
| Subtitution lemmas -- path |
Lemma lemmaA39_this_0:
forall (C: ClassSym) (xTs: ParamTypeList) (Us: TypeList) (p: Path) (T: type),
(Gen_PathTyping (Env_mk (Owner_class C) xTs Us) p T) ->
forall (v: Value),
(Gen_PathTyping rootEnv (Path_value v) (type_class C)) ->
(Gen_PathTyping (Env_mk Owner_root (thisSubst_in_paramTypeList xTs (Path_value v)) (thisSubst_in_typeList Us (Path_value v)))
(thisSubst_in_path p (Path_value v)) (thisSubst_in_type T (Path_value v))
)
.
| Subtitution lemmas -- type |
Lemma lemmaA39_this_2:
forall (C: ClassSym) (xTs: ParamTypeList) (Us: TypeList) (T U: type),
(Gen_Subtyping (Env_mk (Owner_class C) xTs Us) T U) ->
forall (v: Value),
(Gen_PathTyping rootEnv (Path_value v) (type_class C)) ->
(Gen_Subtyping (Env_mk Owner_root (thisSubst_in_paramTypeList xTs (Path_value v)) (thisSubst_in_typeList Us (Path_value v)))
(thisSubst_in_type T (Path_value v)) (thisSubst_in_type U (Path_value v))
)
.
Definition lemmaA39_this1_prop1 (G: Env) (t: Term) (T: type) (H: (Typing G t T)): Prop :=
forall (C: ClassSym) (xTs: ParamTypeList) (Us: TypeList),
G = (Env_mk (Owner_class C) xTs Us) ->
forall (v: Value),
(Gen_PathTyping rootEnv (Path_value v) (type_class C)) ->
(Typing
(Env_mk Owner_root (thisSubst_in_paramTypeList xTs (Path_value v))
(thisSubst_in_typeList Us (Path_value v)))
(thisSubst_in_term t (Path_value v)) (thisSubst_in_type T (Path_value v))
)
.
Definition lemmaA39_this1_prop2 (G: Env) (p: Path) (m: MethodSym) (xts: ParamTermList)
(H: (ParamTermListTyping G p m xts)): Prop :=
forall (C: ClassSym) (xTs: ParamTypeList) (Us: TypeList),
G = (Env_mk (Owner_class C) xTs Us) ->
forall (v: Value),
(Gen_PathTyping rootEnv (Path_value v) (type_class C)) ->
(ParamTermListTyping
(Env_mk Owner_root (thisSubst_in_paramTypeList xTs (Path_value v)) (thisSubst_in_typeList Us (Path_value v)))
(thisSubst_in_path p (Path_value v))
m
(thisSubst_in_paramTermList xts (Path_value v))
)
.
Definition lemmaA39_this1_prop3 (G: Env) (A: ClassSym) (fts: FieldTermList)
(H: (FieldTermListTyping G A fts)): Prop :=
forall (C: ClassSym) (xTs: ParamTypeList) (Us: TypeList),
G = (Env_mk (Owner_class C) xTs Us) ->
forall (v: Value),
(Gen_PathTyping rootEnv (Path_value v) (type_class C)) ->
(FieldTermListTyping
(Env_mk Owner_root (thisSubst_in_paramTypeList xTs (Path_value v)) (thisSubst_in_typeList Us (Path_value v)))
A
(thisSubst_in_fieldTermList fts (Path_value v))
)
.
Lemma lemmaA39_this1_aux_1:
forall (xts: ParamTermList) (p: Path),
(params_of_paramTermList (thisSubst_in_paramTermList xts p)) =
(params_of_paramTermList xts)
.
Lemma lemmaA39_this1_aux_2:
forall (fts: FieldTermList) (p: Path),
(fields_of_fieldTermList (thisSubst_in_fieldTermList fts p)) =
(fields_of_fieldTermList fts)
.
| Subtitution lemmas -- term |
Lemma lemmaA39_this_1:
forall (C: ClassSym) (xTs: ParamTypeList) (Us: TypeList) (t: Term) (T: type),
(Typing (Env_mk (Owner_class C) xTs Us) t T) ->
forall (v: Value),
(Gen_PathTyping rootEnv (Path_value v) (type_class C)) ->
(Typing
(Env_mk Owner_root (thisSubst_in_paramTypeList xTs (Path_value v)) (thisSubst_in_typeList Us (Path_value v)))
(thisSubst_in_term t (Path_value v))
(thisSubst_in_type T (Path_value v))
)
.
End SetProgram.