``` ```

# Definition of Substitutions

``` Require Import Calculus. Require Import Arith. Require Import MatchCompNat. Require Import List. Module SetProgram(My_Program: Program). Import My_Program. Require Subclassing. Module My_Subclassing := Subclassing.SetProgram(My_Program). Import My_Subclassing. ```
 Function: substitutes `q` for `this` in path `p`
``` Definition thisSubst_in_path (p: Path) (q: Path): Path :=   match p with     | (Path_this) => q     | _ => p   end . ```
 Function: substitutes `q` for `this` in type `T`
``` Definition thisSubst_in_type (T: type) (q: Path): type :=   match T with     | (type_virtual p L) => (type_virtual (thisSubst_in_path p q) L)     | (type_class C) => (type_class C)   end . ```
 Function: substitutes `q` for `this` in term `t`
``` Fixpoint thisSubst_in_term (t: Term) (q: Path) {struct t}: Term :=   match t with     | (Term_this) => (path_to_term q)     | (Term_param x) => (Term_param x)     | (Term_var n) => (Term_var n)     | (Term_select p f) => (Term_select (thisSubst_in_path p q) f)     | (Term_new C fts) => (Term_new C (thisSubst_in_fieldTermList fts q))     | (Term_call p m xts) => (Term_call (thisSubst_in_path p q) m (thisSubst_in_paramTermList xts q))     | (Term_loc T u u') => (Term_loc (thisSubst_in_type T q) (thisSubst_in_term u q) (thisSubst_in_term u' q))   end ```
 Function: substitutes `q` for `this` in bindings `fts`
``` with thisSubst_in_fieldTermList (fts: FieldTermList) (q: Path) {struct fts}: FieldTermList :=   match fts with     | FieldTerm_nil => FieldTerm_nil     | (FieldTerm_cons f t fts') => (FieldTerm_cons f (thisSubst_in_term t q) (thisSubst_in_fieldTermList fts' q))   end ```
 Function: substitutes `q` for `this` in bindings `xts`
``` with thisSubst_in_paramTermList (xts: ParamTermList) (q: Path) {struct xts}: ParamTermList :=   match xts with     | ParamTerm_nil => ParamTerm_nil     | (ParamTerm_cons x t xts') => (ParamTerm_cons x (thisSubst_in_term t q) (thisSubst_in_paramTermList xts' q))   end . ```
 Function: substitutes `v` for the variable `n` in path `p`
``` Definition varSubst_in_path (p: Path) (n: VarSym) (v: Value): Path :=   match p with     | (Path_this) => (Path_this)     | (Path_param x) => (Path_param x)     | (Path_var i) =>       (match_comp_nat3 i n Path         (Path_var i)         (Path_value v)         (Path_var (pred i))       )     | (Path_value v) => (Path_value v)   end . ```
 Function: substitutes `v` for the variable `n` in type `T`
``` Definition varSubst_in_type (T: type) (n: VarSym) (v: Value): type :=   match T with     | (type_virtual p L) => (type_virtual (varSubst_in_path p n v) L)     | (type_class C) => (type_class C)   end . ```
 Function: substitutes `v` for the variable `n` in term `t`
``` Fixpoint varSubst_in_term (t: Term) (n: VarSym) (v: Value) {struct t}: Term :=   match t with     | (Term_this) => (Term_this)     | (Term_param x) => (Term_param x)     | (Term_var i) =>       (match_comp_nat3 i n Term         (Term_var i)         (value_to_term v)         (Term_var (pred i))       )     | (Term_select p f) => (Term_select (varSubst_in_path p n v) f)     | (Term_new C fts) => (Term_new C (varSubst_in_fieldTermList fts n v))     | (Term_call p m xts) => (Term_call (varSubst_in_path p n v) m (varSubst_in_paramTermList xts n v))     | (Term_loc T u u') => (Term_loc (varSubst_in_type T n v) (varSubst_in_term u n v) (varSubst_in_term u' (S n) v))   end ```
 Function: substitutes `v` for the variable `n` in bindings `xts`
``` with varSubst_in_paramTermList (xts: ParamTermList) (n: VarSym) (v: Value) {struct xts}: ParamTermList :=   match xts with     | (ParamTerm_nil) => (ParamTerm_nil)     | (ParamTerm_cons x t xts') => (ParamTerm_cons x (varSubst_in_term t n v) (varSubst_in_paramTermList xts' n v))   end ```
 Function: substitutes `v` for the variable `n` in bindings `fts`
``` with varSubst_in_fieldTermList (fts: FieldTermList) (n: VarSym) (v: Value) {struct fts}: FieldTermList :=   match fts with     | (FieldTerm_nil) => (FieldTerm_nil)     | (FieldTerm_cons f t fts') => (FieldTerm_cons f (varSubst_in_term t n v) (varSubst_in_fieldTermList fts' n v))   end . ```
 Function: substitutes `v` for the parameter `x` in path `p`
``` Definition paramSubst_in_path (p: Path) (x: ParamSym) (v: Value): Path :=   match p with     | (Path_param y) => if (ParamSym_eq x y) then (Path_value v) else p     | _ => p   end . ```
 Function: substitutes `v` for the parameter `x` in type `T`
``` Definition paramSubst_in_type (T: type) (x: ParamSym) (v: Value): type :=   match T with     | (type_virtual p L) => (type_virtual (paramSubst_in_path p x v) L)     | (type_class C) => (type_class C)   end . ```
 Function: substitutes `v` for the parameter `x` in term `t`
``` Fixpoint paramSubst_in_term (t: Term) (x: ParamSym) (v: Value) {struct t}: Term :=   match t with     | (Term_this) => (Term_this)     | (Term_param y) => if (ParamSym_eq x y) then (value_to_term v) else (Term_param y)     | (Term_var n) => (Term_var n)     | (Term_select p f) => (Term_select (paramSubst_in_path p x v) f)     | (Term_new C fts) => (Term_new C (paramSubst_in_fieldTermList fts x v))     | (Term_call p m xts) => (Term_call (paramSubst_in_path p x v) m (paramSubst_in_paramTermList xts x v))     | (Term_loc T u u') => (Term_loc (paramSubst_in_type T x v) (paramSubst_in_term u x v) (paramSubst_in_term u' x v))   end ```
 Function: substitutes `v` for the parameter `x` in bindings `fts`
``` with paramSubst_in_fieldTermList (fts: FieldTermList) (x: ParamSym) (v: Value) {struct fts}: FieldTermList :=   match fts with     | FieldTerm_nil => FieldTerm_nil     | (FieldTerm_cons f t fts') => (FieldTerm_cons f (paramSubst_in_term t x v) (paramSubst_in_fieldTermList fts' x v))   end ```
 Function: substitutes `v` for the parameter `x` in bindings `xts`
``` with paramSubst_in_paramTermList (xts: ParamTermList) (x: ParamSym) (v: Value) {struct xts}: ParamTermList :=   match xts with     | ParamTerm_nil => ParamTerm_nil     | (ParamTerm_cons y t xts') => (ParamTerm_cons y (paramSubst_in_term t x v) (paramSubst_in_paramTermList xts' x v))   end . ```
 Function: converts a list of values to a list of terms
``` Fixpoint paramValueList_to_ParamTermList (xvs: list (ParamSym * Value)) {struct xvs}: ParamTermList :=   match xvs with     | nil => (ParamTerm_nil)     | (x,v) :: xvs' => (ParamTerm_cons x (value_to_term v) (paramValueList_to_ParamTermList xvs'))   end . ```
 Function: substitutes values `vs` for the parameter `xs` in term `t` when `xvs` = (`xs`,`vs`)
``` Definition map_paramSubst_in_term (t: Term) (xvs: list (ParamSym * Value)): Term :=   (fold_left     (fun t' (xv: (ParamSym * Value)) => let (x,v) := xv in (paramSubst_in_term t' x v))     xvs     t   ) . Definition map_paramSubst_in_path (p: Path) (xvs: list (ParamSym * Value)): Path :=   (fold_left     (fun p' (xv: (ParamSym * Value)) => let (x,v) := xv in (paramSubst_in_path p' x v))     xvs     p   ) . Definition map_paramSubst_in_type (T: type) (xvs: list (ParamSym * Value)): type :=   (fold_left     (fun T' (xv: (ParamSym * Value)) => let (x,v) := xv in (paramSubst_in_type T' x v))     xvs     T   ) . Definition map_paramSubst_in_fieldTermList (fts: FieldTermList) (xvs: list (ParamSym * Value)): FieldTermList :=   (fold_left     (fun fts' (xv: (ParamSym * Value)) => let (x,v) := xv in (paramSubst_in_fieldTermList fts' x v))     xvs     fts   ) . Definition map_paramSubst_in_paramTermList (xts: ParamTermList) (xvs: list (ParamSym * Value)): ParamTermList :=   (fold_left     (fun xts' (xv: (ParamSym * Value)) => let (x,v) := xv in (paramSubst_in_paramTermList xts' x v))     xvs     xts   ) . Lemma polySubst_in_pathThis:   forall (xvs: list (ParamSym * Value)),     (map_paramSubst_in_path Path_this xvs) = Path_this . Lemma polySubst_in_pathVar:   forall (xvs: list (ParamSym * Value)),     forall (i: VarSym),       (map_paramSubst_in_path (Path_var i) xvs) = (Path_var i) . Lemma polySubst_in_pathValue:   forall (xvs: list (ParamSym * Value)),     forall (v: Value),       (map_paramSubst_in_path (Path_value v) xvs) = (Path_value v) . Lemma polySubst_in_pathParam:   forall (xvs: list (ParamSym * Value)) (x: ParamSym),     (       (forall (v: Value), ~(In (x, v) xvs)) /\       (map_paramSubst_in_path (Path_param x) xvs) = (Path_param x)     ) \/     exists v: Value,       (In (x, v) xvs) /\       (map_paramSubst_in_path (Path_param x) xvs) = (Path_value v) . Lemma polySubst_in_pathParam_corollary:   forall (xvs: list (ParamSym * Value)),     forall (x: ParamSym),       (map_paramSubst_in_path (Path_param x) xvs) = (Path_param x) \/       exists v: Value,         (map_paramSubst_in_path (Path_param x) xvs) = (Path_value v) . Lemma polySubst_in_fieldTermNil:   forall (xvs : list (ParamSym * Value)),     (map_paramSubst_in_fieldTermList FieldTerm_nil xvs) = FieldTerm_nil . Lemma polySubst_in_fieldTermCons:   forall (xvs : list (ParamSym * Value)),     forall (f: FieldSym) (t: Term) (fts: FieldTermList),       (map_paramSubst_in_fieldTermList (FieldTerm_cons f t fts) xvs) =       (FieldTerm_cons f (map_paramSubst_in_term t xvs) (map_paramSubst_in_fieldTermList fts xvs)) . Lemma polySubst_in_paramTermNil:   forall (xvs : list (ParamSym * Value)),     (map_paramSubst_in_paramTermList ParamTerm_nil xvs) = ParamTerm_nil . Lemma polySubst_in_paramTermCons:   forall (xvs : list (ParamSym * Value)),     forall (x: ParamSym) (t: Term) (xts: ParamTermList),       (map_paramSubst_in_paramTermList (ParamTerm_cons x t xts) xvs) =       (ParamTerm_cons x (map_paramSubst_in_term t xvs) (map_paramSubst_in_paramTermList xts xvs)) . Lemma polySubst_in_termThis:   forall (xvs: list (ParamSym * Value)),     (map_paramSubst_in_term Term_this xvs) = Term_this . Lemma polySubst_in_termVar:   forall (i: VarSym) (xvs: list (ParamSym * Value)),     (map_paramSubst_in_term (Term_var i) xvs) = (Term_var i) . Lemma polySubst_in_termSelect:   forall (xvs: list (ParamSym * Value)),     forall (p: Path) (f: FieldSym),       (map_paramSubst_in_term (Term_select p f) xvs) =       (Term_select (map_paramSubst_in_path p xvs) f) . Lemma polySubst_in_termNew:   forall (xvs: (list (ParamSym * Value))),     forall (C: ClassSym) (fts: FieldTermList),       (map_paramSubst_in_term (Term_new C fts) xvs) =       (Term_new C (map_paramSubst_in_fieldTermList fts xvs)) . Lemma polySubst_in_termCall:   forall (xvs: (list (ParamSym * Value))),     forall (p: Path) (m: MethodSym) (xts: ParamTermList),       (map_paramSubst_in_term (Term_call p m xts) xvs) =       (Term_call (map_paramSubst_in_path p xvs) m (map_paramSubst_in_paramTermList xts xvs)) . Lemma polySubst_in_termLet:   forall (xvs: (list (ParamSym * Value))),     forall (T: type) (t u: Term),       (map_paramSubst_in_term (Term_loc T t u) xvs) =       (Term_loc (map_paramSubst_in_type T xvs) (map_paramSubst_in_term t xvs) (map_paramSubst_in_term u xvs)) . Lemma polySubst_in_typeVirtual:   forall (xvs: list (ParamSym * Value)),     forall (p: Path) (L: TypeSym),       (map_paramSubst_in_type (type_virtual p L) xvs) =       (type_virtual (map_paramSubst_in_path p xvs) L) . Lemma polySubst_in_typeClass:   forall (xvs: list (ParamSym * Value)),     forall (C: ClassSym),       (map_paramSubst_in_type (type_class C) xvs) =       (type_class C) . Definition polySubst_in_termValue_prop1 (v: Value): Prop :=   forall (xvs: (list (ParamSym * Value))),     (map_paramSubst_in_term (value_to_term v) xvs) = (value_to_term v) . Definition polySubst_in_termValue_prop2 (fvs: FieldValueList): Prop :=   forall (xvs: (list (ParamSym * Value))),     (map_paramSubst_in_fieldTermList (fieldValueList_to_fieldTermList fvs) xvs) =     (fieldValueList_to_fieldTermList fvs) . ```
 Values are invariant by repeated substitutions for parameters
``` Lemma polySubst_in_termValue:   forall (v: Value) (xvs: (list (ParamSym * Value))),     (map_paramSubst_in_term (value_to_term v) xvs) = (value_to_term v) . Lemma polySubst_in_termParam:   forall (xvs: list (ParamSym * Value)) (x: ParamSym),     (       (forall (v: Value), ~(In (x, v) xvs)) /\       (map_paramSubst_in_term (Term_param x) xvs) = (Term_param x)     ) \/     exists v: Value,       (In (x, v) xvs) /\       (map_paramSubst_in_term (Term_param x) xvs) = (value_to_term v) . Lemma polySubst_in_termParam_corollary:   forall (xvs: list (ParamSym * Value)),     forall (x: ParamSym),       (map_paramSubst_in_term (Term_param x) xvs) = (Term_param x) \/       exists v: Value,         (map_paramSubst_in_term (Term_param x) xvs) = (value_to_term v) . End SetProgram. ```
Index