Proofs 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 Proofs_Progress.
Module My_Proofs_Progress := Proofs_Progress.SetProgram(My_Program).
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.
| Lifting a closed term or type |
Lemma lemmaA30_0:
forall (p: Path) (n: nat),
(path_is_var_closed p) ->
(lift_in_path p n) = p
.
| Lifting a closed term or type |
Lemma lemmaA30_2:
forall (T: type) (n: nat),
(type_is_var_closed T) ->
(lift_in_type T n) = T
.
| Lifting a closed path |
Lemma lemmaA30_0':
forall (p: Path) (n k: nat),
(fv_at_depth_in_path p k) = empty_varset ->
(lift_at_depth_in_path p n k) = p
.
| Lifting a closed type |
Lemma lemmaA30_2':
forall (T: type) (n k: nat),
(fv_at_depth_in_type T k) = empty_varset ->
(lift_at_depth_in_type T n k) = T
.
Definition lemmaA30_1_prop1 (t: Term): Prop :=
forall (n k: nat),
(fv_at_depth_in_term t k) = empty_varset ->
(lift_at_depth_in_term t n k) = t
.
Definition lemmaA30_1_prop2 (fts: FieldTermList): Prop :=
forall (n k: nat),
(fv_at_depth_in_fieldTermList fts k) = empty_varset ->
(lift_at_depth_in_fieldTermList fts n k) = fts
.
Definition lemmaA30_1_prop3 (xts: ParamTermList): Prop :=
forall (n k: nat),
(fv_at_depth_in_paramTermList xts k) = empty_varset ->
(lift_at_depth_in_paramTermList xts n k) = xts
.
| Lifting a closed term |
Lemma lemmaA30_1':
forall (t: Term) (n k: nat),
(fv_at_depth_in_term t k) = empty_varset ->
(lift_at_depth_in_term t n k) = t
.
| Lifting a closed term |
Lemma lemmaA30_1:
forall (t: Term) (n: nat),
(term_is_var_closed t) ->
(lift_in_term t n) = t
.
| Dropping a closed term or type |
Lemma lemmaA31_0:
forall (p: Path),
(path_is_var_closed p) ->
(drop_in_path p) = p
.
| Dropping a closed term or type |
Lemma lemmaA31_2:
forall (T: type),
(type_is_var_closed T) ->
(drop_in_type T) = T
.
| Dropping a closed path |
Lemma lemmaA31_0':
forall (p: Path) (k: nat),
(fv_at_depth_in_path p k) = empty_varset ->
(drop_at_depth_in_path p k) = p
.
| Dropping a closed type |
Lemma lemmaA31_2':
forall (T: type) (k: nat),
(fv_at_depth_in_type T k) = empty_varset ->
(drop_at_depth_in_type T k) = T
.
Definition lemmaA31_1_prop1 (t: Term): Prop :=
forall (k: nat),
(fv_at_depth_in_term t k) = empty_varset ->
(drop_at_depth_in_term t k) = t
.
Definition lemmaA31_1_prop2 (fts: FieldTermList): Prop :=
forall (k: nat),
(fv_at_depth_in_fieldTermList fts k) = empty_varset ->
(drop_at_depth_in_fieldTermList fts k) = fts
.
Definition lemmaA31_1_prop3 (xts: ParamTermList): Prop :=
forall (k: nat),
(fv_at_depth_in_paramTermList xts k) = empty_varset ->
(drop_at_depth_in_paramTermList xts k) = xts
.
| Dropping a closed term |
Lemma lemmaA31_1':
forall (t: Term) (k: nat),
(fv_at_depth_in_term t k) = empty_varset ->
(drop_at_depth_in_term t k) = t
.
| Dropping a closed term |
Lemma lemmaA31_1:
forall (t: Term),
(term_is_var_closed t) ->
(drop_in_term t) = t
.
Definition lemmaA32_prop1 (v: Value): Prop :=
forall (n k: nat),
(lift_at_depth_in_term (value_to_term v) n k) = (value_to_term v)
.
Definition lemmaA32_prop2 (fvs: FieldValueList): Prop :=
forall (n k: nat),
(lift_at_depth_in_fieldTermList (fieldValueList_to_fieldTermList fvs) n k) =
(fieldValueList_to_fieldTermList fvs)
.
| Values are invariant by lifting |
Lemma lemmaA32:
forall (v: Value) (n k: nat),
(lift_at_depth_in_term (value_to_term v) n k) = (value_to_term v)
.
| Permuting lifting and self substitution |
| Permuting lifting and self substitution |
Lemma lemmaA33_0:
forall (p: Path) (n: VarSym) (v: Value),
(lift_in_path (thisSubst_in_path p (Path_value v)) n) =
(thisSubst_in_path (lift_in_path p n) (Path_value v))
.
| Permuting lifting and self substitution |
Lemma lemmaA33_2:
forall (T: type) (n: VarSym) (v: Value),
(lift_in_type (thisSubst_in_type T (Path_value v)) n) =
(thisSubst_in_type (lift_in_type T n) (Path_value v))
.
| Permuting lifting and self substitution |
Lemma lemmaA33_0':
forall (p: Path) (n k: nat) (v: Value),
(lift_at_depth_in_path (thisSubst_in_path p (Path_value v)) n k) =
(thisSubst_in_path (lift_at_depth_in_path p n k) (Path_value v))
.
| Permuting lifting and self substitution |
Lemma lemmaA33_2':
forall (T: type) (n k: nat) (v: Value),
(lift_at_depth_in_type (thisSubst_in_type T (Path_value v)) n k) =
(thisSubst_in_type (lift_at_depth_in_type T n k) (Path_value v))
.
Definition lemmaA33_1_prop1 (t: Term): Prop :=
forall (n k: nat) (v: Value),
(lift_at_depth_in_term (thisSubst_in_term t (Path_value v)) n k) =
(thisSubst_in_term (lift_at_depth_in_term t n k) (Path_value v))
.
Definition lemmaA33_1_prop2 (fts: FieldTermList): Prop :=
forall (n k: nat) (v: Value),
(lift_at_depth_in_fieldTermList (thisSubst_in_fieldTermList fts (Path_value v)) n k) =
(thisSubst_in_fieldTermList (lift_at_depth_in_fieldTermList fts n k) (Path_value v))
.
Definition lemmaA33_1_prop3 (xts: ParamTermList): Prop :=
forall (n k: nat) (v: Value),
(lift_at_depth_in_paramTermList (thisSubst_in_paramTermList xts (Path_value v)) n k) =
(thisSubst_in_paramTermList (lift_at_depth_in_paramTermList xts n k) (Path_value v))
.
Lemma lemmaA33_1':
forall (t: Term) (n k: nat) (v: Value),
(lift_at_depth_in_term (thisSubst_in_term t (Path_value v)) n k) =
(thisSubst_in_term (lift_at_depth_in_term t n k) (Path_value v))
.
| Permuting lifting and self substitutions |
Lemma lemmaA33_1:
forall (t: Term) (n: nat) (v: Value),
(lift_in_term (thisSubst_in_term t (Path_value v)) n) =
(thisSubst_in_term (lift_in_term t n) (Path_value v))
.
| Permuting lifting and variable substitution |
Lemma lemmaA35_0':
forall (p: Path) (n k k': VarSym) (v: Value),
(k' <= k) ->
(lift_at_depth_in_path (varSubst_in_path p k v) n k') =
(varSubst_in_path (lift_at_depth_in_path p n k') (k + n) v)
.
| Permuting lifting and variable substitution |
Lemma lemmaA35_0:
forall (p: Path) (n k: VarSym) (v: Value),
(lift_in_path (varSubst_in_path p k v) n) =
(varSubst_in_path (lift_in_path p n) (k + n) v)
.
Lemma lemmaA35_2':
forall (T: type) (n k k': nat) (v: Value),
(k' <= k) ->
(lift_at_depth_in_type (varSubst_in_type T k v) n k') =
(varSubst_in_type (lift_at_depth_in_type T n k') (k + n) v)
.
| Permuting lifting and variable substitution |
Lemma lemmaA35_2:
forall (T: type) (n k: VarSym) (v: Value),
(lift_in_type (varSubst_in_type T k v) n) =
(varSubst_in_type (lift_in_type T n) (k + n) v)
.
Definition lemmaA35_1_prop1 (n: nat) (v: Value) (t: Term): Prop :=
forall (k k': VarSym),
(k' <= k) ->
(lift_at_depth_in_term (varSubst_in_term t k v) n k') =
(varSubst_in_term (lift_at_depth_in_term t n k') (k + n) v)
.
Definition lemmaA35_1_prop2 (n: nat) (v: Value) (fts: FieldTermList): Prop :=
forall (k k': VarSym),
(k' <= k) ->
(lift_at_depth_in_fieldTermList (varSubst_in_fieldTermList fts k v) n k') =
(varSubst_in_fieldTermList (lift_at_depth_in_fieldTermList fts n k') (k + n) v)
.
Definition lemmaA35_1_prop3 (n: nat) (v: Value) (xts: ParamTermList): Prop :=
forall (k k': VarSym),
(k' <= k) ->
(lift_at_depth_in_paramTermList (varSubst_in_paramTermList xts k v) n k') =
(varSubst_in_paramTermList (lift_at_depth_in_paramTermList xts n k') (k + n) v)
.
Lemma lemmaA35_1':
forall (t: Term) (n k k': nat) (v: Value),
(k' <= k) ->
(lift_at_depth_in_term (varSubst_in_term t k v) n k') =
(varSubst_in_term (lift_at_depth_in_term t n k') (k + n) v)
.
| Permuting lifting and variable substitutions |
Lemma lemmaA35_1:
forall (t: Term) (n k: VarSym) (v: Value),
(lift_in_term (varSubst_in_term t k v) n) =
(varSubst_in_term (lift_in_term t n) (k + n) v)
.
| Permuting lifting and parameter substitution |
| Permuting lifting and parameter substitution |
Lemma lemmaA34_0':
forall (p: Path) (n k: VarSym) (xvs: list (ParamSym * Value)),
(lift_at_depth_in_path (map_paramSubst_in_path p xvs) n k) =
(map_paramSubst_in_path (lift_at_depth_in_path p n k) xvs)
.
| Permuting lifting and parameter substitution |
Lemma lemmaA34_0:
forall (p: Path) (n: VarSym) (xvs: list (ParamSym * Value)),
(lift_in_path (map_paramSubst_in_path p xvs) n) =
(map_paramSubst_in_path (lift_in_path p n) xvs)
.
| Permuting lifting and parameter substitution |
Lemma lemmaA34_2':
forall (T: type) (n k: VarSym) (xvs: list (ParamSym * Value)),
(lift_at_depth_in_type (map_paramSubst_in_type T xvs) n k) =
(map_paramSubst_in_type (lift_at_depth_in_type T n k) xvs)
.
| Permuting lifting and parameter substitution |
Lemma lemmaA34_2:
forall (T: type) (n: VarSym) (xvs: list (ParamSym * Value)),
(lift_in_type (map_paramSubst_in_type T xvs) n) =
(map_paramSubst_in_type (lift_in_type T n) xvs)
.
Definition lemmaA34_1_prop1 (n: nat) (xvs: list (ParamSym * Value)) (t: Term): Prop :=
forall (k: nat) ,
(lift_at_depth_in_term (map_paramSubst_in_term t xvs) n k) =
(map_paramSubst_in_term (lift_at_depth_in_term t n k) xvs)
.
Definition lemmaA34_1_prop2 (n: nat) (xvs: list (ParamSym * Value)) (fts: FieldTermList): Prop :=
forall (k: nat) ,
(lift_at_depth_in_fieldTermList (map_paramSubst_in_fieldTermList fts xvs) n k) =
(map_paramSubst_in_fieldTermList (lift_at_depth_in_fieldTermList fts n k) xvs)
.
Definition lemmaA34_1_prop3 (n: nat) (xvs: list (ParamSym * Value)) (xts: ParamTermList): Prop :=
forall (k: nat) ,
(lift_at_depth_in_paramTermList (map_paramSubst_in_paramTermList xts xvs) n k) =
(map_paramSubst_in_paramTermList (lift_at_depth_in_paramTermList xts n k) xvs)
.
Lemma lemmaA34_1':
forall (t: Term) (n k: nat) (xvs: (list (ParamSym * Value))),
(lift_at_depth_in_term (map_paramSubst_in_term t xvs) n k) =
(map_paramSubst_in_term (lift_at_depth_in_term t n k) xvs)
.
| Permuting lifting and self substitutions |
Lemma lemmaA34_1:
forall (t: Term) (n: nat) (xvs: (list (ParamSym * Value))),
(lift_in_term (map_paramSubst_in_term t xvs) n) =
(map_paramSubst_in_term (lift_in_term t n) xvs)
.
| Facts about variable substitution |
| Facts about variable substitution |
Lemma lemmaA37_0:
forall (p: Path) (k: nat) (v: Value),
(path_is_var_closed p) ->
(varSubst_in_path p k v) = p
.
| Facts about variable substitution |
Lemma lemmaA37_2:
forall (T: type) (k: nat) (v: Value),
(type_is_var_closed T) ->
(varSubst_in_type T k v) = T
.
Lemma lemmaA37_0':
forall (p: Path) (k: nat) (v: Value),
(fv_at_depth_in_path p k) = empty_varset ->
(varSubst_in_path p k v) = p
.
Lemma lemmaA37_2':
forall (T: type) (k: nat) (v: Value),
(fv_at_depth_in_type T k) = empty_varset ->
(varSubst_in_type T k v) = T
.
Definition lemmaA37_1_prop1 (t: Term): Prop :=
forall (k: nat) (v: Value),
(fv_at_depth_in_term t k) = empty_varset ->
(varSubst_in_term t k v) = t
.
Definition lemmaA37_1_prop2 (fts: FieldTermList): Prop :=
forall (k: nat) (v: Value),
(fv_at_depth_in_fieldTermList fts k) = empty_varset ->
(varSubst_in_fieldTermList fts k v) = fts
.
Definition lemmaA37_1_prop3 (xts: ParamTermList): Prop :=
forall (k: nat) (v: Value),
(fv_at_depth_in_paramTermList xts k) = empty_varset ->
(varSubst_in_paramTermList xts k v) = xts
.
| Lifting a closed term |
Lemma lemmaA37_1':
forall (t: Term) (k: nat) (v: Value),
(fv_at_depth_in_term t k) = empty_varset ->
(varSubst_in_term t k v) = t
.
| Facts about variable substitution -- term |
Lemma lemmaA37_1:
forall (t: Term) (k: nat) (v: Value),
(term_is_var_closed t) ->
(varSubst_in_term t 0 v) = t
.
Definition lemmaA36_32_prop1 (v: Value): Prop :=
forall (k: nat),
(drop_at_depth_in_term (value_to_term v) k) = (value_to_term v)
.
Definition lemmaA36_32_prop2 (fvs: FieldValueList): Prop :=
forall (k: nat),
(drop_at_depth_in_fieldTermList (fieldValueList_to_fieldTermList fvs) k) =
(fieldValueList_to_fieldTermList fvs)
.
| Values are invariant by dropping |
Lemma lemmaA36_32:
forall (v: Value) (k: nat),
(drop_at_depth_in_term (value_to_term v) k) = (value_to_term v)
.
| Permuting dropping and self substitution |
| Permuting dropping and self substitution |
Lemma lemmaA36_33_0:
forall (p: Path) (v: Value),
(drop_in_path (thisSubst_in_path p (Path_value v))) =
(thisSubst_in_path (drop_in_path p) (Path_value v))
.
| Permuting dropping and self substitution |
Lemma lemmaA36_33_2:
forall (T: type) (v: Value),
(drop_in_type (thisSubst_in_type T (Path_value v))) =
(thisSubst_in_type (drop_in_type T) (Path_value v))
.
| Permuting dropping and self substitution |
Lemma lemmaA36_33_0':
forall (p: Path) (k: nat) (v: Value),
(drop_at_depth_in_path (thisSubst_in_path p (Path_value v)) k) =
(thisSubst_in_path (drop_at_depth_in_path p k) (Path_value v))
.
| Permuting dropping and self substitution |
Lemma lemmaA36_33_2':
forall (T: type) (k: nat) (v: Value),
(drop_at_depth_in_type (thisSubst_in_type T (Path_value v)) k) =
(thisSubst_in_type (drop_at_depth_in_type T k) (Path_value v))
.
Definition lemmaA36_33_1_prop1 (t: Term): Prop :=
forall (k: nat) (v: Value),
(drop_at_depth_in_term (thisSubst_in_term t (Path_value v)) k) =
(thisSubst_in_term (drop_at_depth_in_term t k) (Path_value v))
.
Definition lemmaA36_33_1_prop2 (fts: FieldTermList): Prop :=
forall (k: nat) (v: Value),
(drop_at_depth_in_fieldTermList (thisSubst_in_fieldTermList fts (Path_value v)) k) =
(thisSubst_in_fieldTermList (drop_at_depth_in_fieldTermList fts k) (Path_value v))
.
Definition lemmaA36_33_1_prop3 (xts: ParamTermList): Prop :=
forall (k: nat) (v: Value),
(drop_at_depth_in_paramTermList (thisSubst_in_paramTermList xts (Path_value v)) k) =
(thisSubst_in_paramTermList (drop_at_depth_in_paramTermList xts k) (Path_value v))
.
Lemma lemmaA36_33_1':
forall (t: Term) (k: nat) (v: Value),
(drop_at_depth_in_term (thisSubst_in_term t (Path_value v)) k) =
(thisSubst_in_term (drop_at_depth_in_term t k) (Path_value v))
.
| Permuting dropping and self substitutions |
Lemma lemmaA36_33_1:
forall (t: Term) (v: Value),
(drop_in_term (thisSubst_in_term t (Path_value v))) =
(thisSubst_in_term (drop_in_term t) (Path_value v))
.
| Permuting dropping and variable substitution |
Lemma lemmaA36_35_0':
forall (p: Path) (k k': VarSym) (v: Value),
k' <= k ->
((k' = 0) -> ~(varset_In 0 (fv_in_path p))) ->
(drop_at_depth_in_path (varSubst_in_path p (S k) v) k') =
(varSubst_in_path (drop_at_depth_in_path p k') k v)
.
| Permuting dropping and variable substitution |
Lemma lemmaA36_35_0:
forall (p: Path) (k: VarSym) (v: Value),
~(varset_In 0 (fv_in_path p)) ->
(drop_in_path (varSubst_in_path p (S k) v)) =
(varSubst_in_path (drop_in_path p) k v)
.
Lemma lemmaA36_35_2':
forall (T: type) (k k': nat) (v: Value),
k' <= k ->
((k' = 0) -> ~(varset_In 0 (fv_in_type T))) ->
(drop_at_depth_in_type (varSubst_in_type T (S k) v) k') =
(varSubst_in_type (drop_at_depth_in_type T k') k v)
.
| Permuting dropping and variable substitution |
Lemma lemmaA36_35_2:
forall (T: type) (k: VarSym) (v: Value),
~(varset_In 0 (fv_in_type T)) ->
(drop_in_type (varSubst_in_type T (S k) v)) =
(varSubst_in_type (drop_in_type T) k v)
.
Definition lemmaA36_35_1_prop1 (v: Value) (t: Term): Prop :=
forall (k k': VarSym),
(k' <= k) ->
((k' = 0) -> ~(varset_In 0 (fv_in_term t))) ->
(drop_at_depth_in_term (varSubst_in_term t (S k) v) k') =
(varSubst_in_term (drop_at_depth_in_term t k') k v)
.
Definition lemmaA36_35_1_prop2 (v: Value) (fts: FieldTermList): Prop :=
forall (k k': VarSym),
(k' <= k) ->
((k' = 0) -> ~(varset_In 0 (fv_at_depth_in_fieldTermList fts 0))) ->
(drop_at_depth_in_fieldTermList (varSubst_in_fieldTermList fts (S k) v) k') =
(varSubst_in_fieldTermList (drop_at_depth_in_fieldTermList fts k') k v)
.
Definition lemmaA36_35_1_prop3 (v: Value) (xts: ParamTermList): Prop :=
forall (k k': VarSym),
(k' <= k) ->
((k' = 0) -> ~(varset_In 0 (fv_at_depth_in_paramTermList xts 0))) ->
(drop_at_depth_in_paramTermList (varSubst_in_paramTermList xts (S k) v) k') =
(varSubst_in_paramTermList (drop_at_depth_in_paramTermList xts k') k v)
.
Lemma lemmaA36_35_1':
forall (t: Term) (k k': nat) (v: Value),
(k' <= k) ->
((k' = 0) -> ~(varset_In 0 (fv_in_term t))) ->
(drop_at_depth_in_term (varSubst_in_term t (S k) v) k') =
(varSubst_in_term (drop_at_depth_in_term t k') k v)
.
| Permuting dropping and variable substitutions |
Lemma lemmaA36_35_1:
forall (t: Term) (k: VarSym) (v: Value),
~(varset_In 0 (fv_in_term t)) ->
(drop_in_term (varSubst_in_term t (S k) v)) =
(varSubst_in_term (drop_in_term t) k v)
.
| Permuting dropping and parameter substitution |
| Permuting dropping and parameter substitution |
Lemma lemmaA36_34_0':
forall (p: Path) (k: VarSym) (xvs: list (ParamSym * Value)),
(drop_at_depth_in_path (map_paramSubst_in_path p xvs) k) =
(map_paramSubst_in_path (drop_at_depth_in_path p k) xvs)
.
| Permuting dropping and parameter substitution |
Lemma lemmaA36_34_0:
forall (p: Path) (xvs: list (ParamSym * Value)),
(drop_in_path (map_paramSubst_in_path p xvs)) =
(map_paramSubst_in_path (drop_in_path p) xvs)
.
| Permuting dropping and parameter substitution |
Lemma lemmaA36_34_2':
forall (T: type) (k: VarSym) (xvs: list (ParamSym * Value)),
(drop_at_depth_in_type (map_paramSubst_in_type T xvs) k) =
(map_paramSubst_in_type (drop_at_depth_in_type T k) xvs)
.
| Permuting dropping and parameter substitution |
Lemma lemmaA36_34_2:
forall (T: type) (xvs: list (ParamSym * Value)),
(drop_in_type (map_paramSubst_in_type T xvs)) =
(map_paramSubst_in_type (drop_in_type T) xvs)
.
Definition lemmaA36_34_1_prop1 (xvs: list (ParamSym * Value)) (t: Term): Prop :=
forall (k: nat) ,
(drop_at_depth_in_term (map_paramSubst_in_term t xvs) k) =
(map_paramSubst_in_term (drop_at_depth_in_term t k) xvs)
.
Definition lemmaA36_34_1_prop2 (xvs: list (ParamSym * Value)) (fts: FieldTermList): Prop :=
forall (k: nat) ,
(drop_at_depth_in_fieldTermList (map_paramSubst_in_fieldTermList fts xvs) k) =
(map_paramSubst_in_fieldTermList (drop_at_depth_in_fieldTermList fts k) xvs)
.
Definition lemmaA36_34_1_prop3 (xvs: list (ParamSym * Value)) (xts: ParamTermList): Prop :=
forall (k: nat) ,
(drop_at_depth_in_paramTermList (map_paramSubst_in_paramTermList xts xvs) k) =
(map_paramSubst_in_paramTermList (drop_at_depth_in_paramTermList xts k) xvs)
.
Lemma lemmaA36_34_1':
forall (t: Term) (k: nat) (xvs: (list (ParamSym * Value))),
(drop_at_depth_in_term (map_paramSubst_in_term t xvs) k) =
(map_paramSubst_in_term (drop_at_depth_in_term t k) xvs)
.
| Permuting dropping and self substitutions |
Lemma lemmaA36_34_1:
forall (t: Term) (xvs: (list (ParamSym * Value))),
(drop_in_term (map_paramSubst_in_term t xvs)) =
(map_paramSubst_in_term (drop_in_term t) xvs)
.
End SetProgram.