``` ```

# 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. ```
Index
This page has been generated by coqdoc