``` ```

# Definitions about De Bruijn's Indices

``` 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 Substitutions. Module My_Substitutions := Substitutions.SetProgram(My_Program). Import My_Substitutions. Import My_Subclassing. ```
 Function: lifts var `v` with amplitude `n` at depth `k`
``` Definition lift_at_depth_in_var (i: VarSym) (n: nat) (k: nat): VarSym :=   (match_comp_nat2 i k VarSym     i     (i + n)   ) . ```
 Function: lifts path `p` with amplitude `n` at depth `k`
``` Definition lift_at_depth_in_path (p: Path) (n: nat) (k: nat): Path :=   match p with     | (Path_this) => (Path_this)     | (Path_param x) => (Path_param x)     | (Path_var i) =>       (match_comp_nat2 i k Path         (Path_var i)         (Path_var (i + n))       )     | (Path_value v) => (Path_value v)   end . ```
 Function: lifts type `T` with amplitude `n` at depth `k`
``` Definition lift_at_depth_in_type (T: type) (n: nat) (k: nat): type :=   match T with     | (type_virtual p L) => (type_virtual (lift_at_depth_in_path p n k) L)     | (type_class C) => (type_class C)   end . ```
 Function: lifts term `t` with amplitude `n` at depth `k`
``` Fixpoint lift_at_depth_in_term (t: Term) (n: nat) (k: nat) {struct t}: Term :=   match t with     | (Term_this) => (Term_this)     | (Term_param x) => (Term_param x)     | (Term_var i) =>       (match_comp_nat2 i k Term         (Term_var i)         (Term_var (i + n))       )     | (Term_select p f) => (Term_select (lift_at_depth_in_path p n k) f)     | (Term_new C fts) => (Term_new C (lift_at_depth_in_fieldTermList fts n k))     | (Term_call p m xts) => (Term_call (lift_at_depth_in_path p n k) m (lift_at_depth_in_paramTermList xts n k))     | (Term_loc T u u') => (Term_loc (lift_at_depth_in_type T n k) (lift_at_depth_in_term u n k) (lift_at_depth_in_term u' n (S k)))   end ```
 Function: lifts bindings in `xts` with amplitude `n` at depth `k`
``` with lift_at_depth_in_paramTermList (xts: ParamTermList) (n: nat) (k: nat) {struct xts}: ParamTermList :=   match xts with     | (ParamTerm_nil) => (ParamTerm_nil)     | (ParamTerm_cons x t xts') => (ParamTerm_cons x (lift_at_depth_in_term t n k) (lift_at_depth_in_paramTermList xts' n k))   end ```
 Function: lifts bindings in `fts` with amplitude `n` at depth `k`
``` with lift_at_depth_in_fieldTermList (fts: FieldTermList) (n: nat) (k: nat) {struct fts}: FieldTermList :=   match fts with     | (FieldTerm_nil) => (FieldTerm_nil)     | (FieldTerm_cons f t fts') => (FieldTerm_cons f (lift_at_depth_in_term t n k) (lift_at_depth_in_fieldTermList fts' n k))   end . ```
 Function: lifts path `p` with amplitude `n`
``` Definition lift_in_path (p: Path) (n: nat): Path :=   (lift_at_depth_in_path p n 0). ```
 Function: lifts type `T` with amplitude `n`
``` Definition lift_in_type (T: type) (n: nat): type :=   (lift_at_depth_in_type T n 0). ```
 Function: lifts term `t` with amplitude `n`
``` Definition lift_in_term (t: Term) (n: nat): Term :=   (lift_at_depth_in_term t n 0) . ```
 Function: drops path `p` with amplitude 1 at depth `k`
``` Definition drop_at_depth_in_path (p: Path) (k: nat): Path :=   match p with     | (Path_this) => (Path_this)     | (Path_param x) => (Path_param x)     | (Path_var i) =>       (match_comp_nat2 i k Path         (Path_var i)         (Path_var (pred i))       )     | (Path_value v) => (Path_value v)   end . ```
 Function: drops type `T` with amplitude 1 at depth `k`
``` Definition drop_at_depth_in_type (T: type) (k: nat): type :=   match T with     | (type_virtual p L) => (type_virtual (drop_at_depth_in_path p k) L)     | (type_class C) => (type_class C)   end . ```
 Function: drops term `t` with amplitude 1 at depth `k`
``` Fixpoint drop_at_depth_in_term (t: Term) (k: nat) {struct t}: Term :=   match t with     | (Term_this) => (Term_this)     | (Term_param x) => (Term_param x)     | (Term_var i) =>       (match_comp_nat2 i k Term         (Term_var i)         (Term_var (pred i))       )     | (Term_select p f) => (Term_select (drop_at_depth_in_path p k) f)     | (Term_call p m xts) => (Term_call (drop_at_depth_in_path p k) m (drop_at_depth_in_paramTermList xts k))     | (Term_new C fts) => (Term_new C (drop_at_depth_in_fieldTermList fts k))     | (Term_loc T u u') => (Term_loc (drop_at_depth_in_type T k) (drop_at_depth_in_term u k) (drop_at_depth_in_term u' (S k)))   end ```
 Function: drops bindings in `xts` with amplitude 1 at depth `k`
``` with drop_at_depth_in_paramTermList (xts: ParamTermList) (k: nat) {struct xts}: ParamTermList :=   match xts with     | (ParamTerm_nil) => (ParamTerm_nil)     | (ParamTerm_cons x t xts') => (ParamTerm_cons x (drop_at_depth_in_term t k) (drop_at_depth_in_paramTermList xts' k))   end ```
 Function: drops bindings in `fts` with amplitude 1 at depth `k`
``` with drop_at_depth_in_fieldTermList (fts: FieldTermList) (k: nat) {struct fts}: FieldTermList :=   match fts with     | (FieldTerm_nil) => (FieldTerm_nil)     | (FieldTerm_cons f t fts') => (FieldTerm_cons f (drop_at_depth_in_term t k) (drop_at_depth_in_fieldTermList fts' k))   end . ```
 Function: drops path `p` with amplitude 1
``` Definition drop_in_path (p: Path): Path :=   (drop_at_depth_in_path p 0) . ```
 Function: drops type `T` with amplitude 1
``` Definition drop_in_type (T: type): type :=   (drop_at_depth_in_type T 0) . ```
 Function: drops term `t` with amplitude 1
``` Definition drop_in_term (t: Term): Term :=   (drop_at_depth_in_term t 0) . Definition VarSet := (set VarSym). Definition empty_varset := (empty_set VarSym). Definition varset_add (n: VarSym) (vs: VarSet) := (set_add (VarSym_eqdec) n vs). Definition varset_union (vs: VarSet) (vs': VarSet) := (set_union (VarSym_eqdec) vs vs'). Definition varset_In (n: VarSym) (vs: VarSet): Prop := (set_In n vs). ```
 Function: free variables of path `p` at depth `k`
``` Definition fv_at_depth_in_path (p: Path) (k: nat): VarSet :=   match p with     | (Path_this) => empty_varset     | (Path_param x) => empty_varset     | (Path_var i) =>       (match_comp_nat2 i k _         empty_varset         (varset_add (i - k) empty_varset)       )     | (Path_value v) => empty_varset   end . ```
 Function: free variables of type `T` at depth `k`
``` Definition fv_at_depth_in_type (T: type) (k: nat): VarSet :=   match T with     | (type_virtual p L) => (fv_at_depth_in_path p k)     | (type_class C) => empty_varset   end . ```
 Function: free variables of term `t` at depth `k`
``` Fixpoint fv_at_depth_in_term (t: Term) (k: nat) {struct t}: VarSet :=   match t with     | (Term_this) => empty_varset     | (Term_param x) => empty_varset     | (Term_var i) =>       (match_comp_nat2 i k _        empty_varset        (varset_add (i - k) empty_varset)       )     | (Term_select p f) => (fv_at_depth_in_path p k)     | (Term_new C fts) => (fv_at_depth_in_fieldTermList fts k)     | (Term_call p m xts) => (varset_union (fv_at_depth_in_path p k) (fv_at_depth_in_paramTermList xts k))     | (Term_loc T u u') => (varset_union (varset_union (fv_at_depth_in_type T k) (fv_at_depth_in_term u k)) (fv_at_depth_in_term u' (S k)))   end ```
 Function: free variables of the bindings `xts` at depth `k`
``` with fv_at_depth_in_paramTermList (xts: ParamTermList) (k: nat) {struct xts}: VarSet :=   match xts with     | (ParamTerm_nil) => empty_varset     | (ParamTerm_cons x t xts') => (varset_union (fv_at_depth_in_term t k) (fv_at_depth_in_paramTermList xts' k))   end ```
 Function: free variables of the bindings `fts` at depth `k`
``` with fv_at_depth_in_fieldTermList (fts: FieldTermList) (k: nat) {struct fts}: VarSet :=   match fts with     | (FieldTerm_nil) => empty_varset     | (FieldTerm_cons f t fts') => (varset_union (fv_at_depth_in_term t k) (fv_at_depth_in_fieldTermList fts' k))   end . ```
 Function: free variables in type `T`
``` Definition fv_in_path (p: Path): VarSet := (fv_at_depth_in_path p 0). ```
 Function: free variables in path `p`
``` Definition fv_in_type (T: type): VarSet := (fv_at_depth_in_type T 0). ```
 Function: free variables in term `t`
``` Definition fv_in_term (t: Term): VarSet := (fv_at_depth_in_term t 0). ```
 Function: free variables in bindings `xts`
``` Definition fv_in_paramTermList (xts: ParamTermList): VarSet := (fv_at_depth_in_paramTermList xts 0). ```
 Function: free variables in bindings `fts`
``` Definition fv_in_fieldTermList (fts: FieldTermList): VarSet := (fv_at_depth_in_fieldTermList fts 0). ```
 Predicate: term `t` has no free variables
``` Definition path_is_var_closed (p: Path): Prop :=   (fv_in_path p) = empty_varset . ```
 Predicate: term `t` has no free variables
``` Definition type_is_var_closed (T: type): Prop :=   (fv_in_type T) = empty_varset . ```
 Predicate: term `t` has no free variables
``` Definition term_is_var_closed (t: Term): Prop :=   (fv_in_term t) = empty_varset . ```
 Predicate: the variable `n` is free in the path `p`
``` Definition var_in_path (n: VarSym) (p: Path): Prop :=   match p with     | Path_this => False     | (Path_param y) => False     | (Path_var m) => m = n     | (Path_value v) => False   end . ```
 Predicate: the variable `n` is free in the type `T`
``` Definition var_in_type (n: VarSym) (T: type): Prop :=   match T with     | (type_class C) => False     | (type_virtual p L) => (var_in_path n p)   end . ```
 Predicate: the variable `n` is free in the term `t`
``` Definition var_in_term (n: VarSym) (t: Term): Prop :=   (varset_In n (fv_in_term t)) . ```
 Predicate: path `p` has no free variables
``` Definition path_is_var_closed' (p: Path): Prop :=   forall (n: VarSym),     ~(var_in_path n p) . ```
 Predicate: type `T` has no free variables
``` Definition type_is_var_closed' (T: type): Prop :=   forall (n: VarSym),     ~(var_in_type n T) . ```
 Predicate: term `t` has no free variables
``` Definition term_is_var_closed' (t: Term): Prop :=   forall (n: VarSym),     ~(var_in_term n t) . Lemma path_is_var_closed_eq_r:   forall (p: Path),     (path_is_var_closed p) -> (path_is_var_closed' p) . Lemma path_is_var_closed_eq_l:   forall (p: Path),     (path_is_var_closed' p) -> (path_is_var_closed p) . Lemma type_is_var_closed_eq_r:   forall (T: type),     (type_is_var_closed T) -> (type_is_var_closed' T) . Lemma type_is_var_closed_eq_l:   forall (T: type),     (type_is_var_closed' T) -> (type_is_var_closed T) . Lemma fv_termvar_non_empty:   forall (i: VarSym),     (fv_in_term (Term_var i)) <> empty_varset . Lemma fv_pathvar_non_empty:   forall (i: VarSym),     (fv_in_path (Path_var i)) <> empty_varset . Lemma fv_termvar_empty:   forall (i: VarSym) (k: nat),     (fv_at_depth_in_term (Term_var i) k) = empty_varset ->     i < k . Lemma fv_pathvar_empty:   forall (i: VarSym) (k: nat),     (fv_at_depth_in_path (Path_var i) k) = empty_varset ->     i < k . Lemma fv_and_var_in_path:   forall (n: nat) (p: Path),     (var_in_path n p) <-> (varset_In n (fv_in_path p)) . Lemma fv_and_var_in_path1:   forall (n: nat) (p: Path),     (var_in_path n p) ->     (varset_In n (fv_in_path p)) . Lemma fv_and_var_in_path2:   forall (n: nat) (p: Path),     (varset_In n (fv_in_path p)) ->     (var_in_path n p) . Lemma fv_and_var_in_type:   forall (n: nat) (T: type),     (var_in_type n T) <-> (varset_In n (fv_in_type T)) . Lemma fv_and_var_in_type1:   forall (n: nat) (T: type),     (var_in_type n T) ->     (varset_In n (fv_in_type T)) . Lemma fv_and_var_in_type2:   forall (n: nat) (T: type),     (varset_In n (fv_in_type T)) ->     (var_in_type n T) . Lemma fv_and_thisSubst_in_path:   forall (p: Path) (v: Value),     (fv_in_path (thisSubst_in_path p (Path_value v))) = (fv_in_path p) . Lemma fv_and_thisSubst_in_type:   forall (T: type) (v: Value),     (fv_in_type (thisSubst_in_type T (Path_value v))) = (fv_in_type T) . End SetProgram. ```
Index