Library Lambda.LiftSubst


Require
 Import
 Lambda.Terms.




  Lemma
 lift_ref_ge :

   ∀ k
 n
 p
, p
 ≤ n
 → lift_rec k
 (Ref n
) p
 = Ref (k
 + n
).




  Lemma
 lift_ref_lt : ∀ k
 n
 p
, p
 > n
 → lift_rec k
 (Ref n
) p
 = Ref n
.




  Lemma
 subst_ref_lt : ∀ u
 n
 k
, k
 > n
 → subst_rec u
 (Ref n
) k
 = Ref n
.




  Lemma
 subst_ref_gt :

   ∀ u
 n
 k
, n
 > k
 → subst_rec u
 (Ref n
) k
 = Ref (pred n
).




  Lemma
 subst_ref_eq : ∀ u
 n
, subst_rec u
 (Ref n
) n
 = lift n
 u
.




  Lemma
 lift_rec0 : ∀ M
 k
, lift_rec 0 M
 k
 = M
.




Lemma
 lift0 : ∀ M
, lift 0 M
 = M
.




  Lemma
 simpl_lift_rec :

   ∀ M
 n
 k
 p
 i
,

   i
 ≤ k
 + n
 →

   k
 ≤ i
 → lift_rec p
 (lift_rec n
 M
 k
) i
 = lift_rec (p
 + n
) M
 k
.




  Lemma
 simpl_lift : ∀ M
 n
, lift (S n
) M
 = lift 1 (lift n
 M
).




Lemma
 permute_lift_rec :

   ∀ M
 n
 k
 p
 i
,

   i
 ≤ k
 →

   lift_rec p
 (lift_rec n
 M
 k
) i
 = lift_rec n
 (lift_rec p
 M
 i
) (p
 + k
).




  Lemma
 permute_lift :

   ∀ M
 k
, lift 1 (lift_rec 1 M
 k
) = lift_rec 1 (lift 1 M
) (S k
).




Require
 Import
 Omega.




  Lemma
 simpl_subst_rec :

   ∀ M
 N
 n
 p
 k
,

   p
 ≤ n
 + k
 →

   k
 ≤ p
 → subst_rec N
 (lift_rec (S n
) M
 k
) p
 = lift_rec n
 M
 k
.




  Lemma
 simpl_subst :

   ∀ N
 M
 n
 p
, p
 ≤ n
 → subst_rec N
 (lift (S n
) M
) p
 = lift n
 M
.




  Lemma
 commut_lift_subst_rec :

   ∀ M
 N
 n
 p
 k
,

   k
 ≤ p
 →

   lift_rec n
 (subst_rec N
 M
 p
) k
 = subst_rec N
 (lift_rec n
 M
 k
) (n
 + p
).




  Lemma
 commut_lift_subst :

   ∀ M
 N
 k
, subst_rec N
 (lift 1 M
) (S k
) = lift 1 (subst_rec N
 M
 k
).




  Lemma
 distr_lift_subst_rec :

   ∀ M
 N
 n
 p
 k
,

   lift_rec n
 (subst_rec N
 M
 p
) (p
 + k
) =

   subst_rec (lift_rec n
 N
 k
) (lift_rec n
 M
 (S (p
 + k
))) p
.




Lemma
 distr_lift_subst :

   ∀ M
 N
 n
 k
,

   lift_rec n
 (subst N
 M
) k
 = subst (lift_rec n
 N
 k
) (lift_rec n
 M
 (S k
)).




  Lemma
 distr_subst_rec :

   ∀ M
 N
 (P
 : term) n
 p
,

   subst_rec P
 (subst_rec N
 M
 p
) (p
 + n
) =

   subst_rec (subst_rec P
 N
 n
) (subst_rec P
 M
 (S (p
 + n
))) p
.




  Lemma
 distr_subst :

   ∀ (P
 : term) N
 M
 k
,

   subst_rec P
 (subst N
 M
) k
 = subst (subst_rec P
 N
 k
) (subst_rec P
 M
 (S k
)).