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.