Library Lambda.TPOSR.LiftSubst


Require
 Import
 Lambda.TPOSR.Terms.

  Lemma
 llift_ref_ge :

   ∀ k
 n
 p
, p
 ≤ n
 → llift_rec k
 (Ref_l n
) p
 = Ref_l (k
 + n
).




  Lemma
 llift_ref_lt : ∀ k
 n
 p
, p
 > n
 → llift_rec k
 (Ref_l n
) p
 = Ref_l n
.




  Lemma
 lsubst_ref_lt : ∀ u
 n
 k
, k
 > n
 → lsubst_rec u
 (Ref_l n
) k
 = Ref_l n
.




  Lemma
 lsubst_ref_gt :

   ∀ u
 n
 k
, n
 > k
 → lsubst_rec u
 (Ref_l n
) k
 = Ref_l (pred n
).




  Lemma
 lsubst_ref_eq : ∀ u
 n
, lsubst_rec u
 (Ref_l n
) n
 = llift n
 u
.




  Lemma
 llift_rec0 : ∀ M
 k
, llift_rec 0 M
 k
 = M
.




Lemma
 llift0 : ∀ M
, llift 0 M
 = M
.




Require
 Import
 Omega.

  Lemma
 simpl_llift_rec :

   ∀ M
 n
 k
 p
 i
,

   i
 ≤ k
 + n
 →

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




  Lemma
 simpl_llift : ∀ M
 n
, llift (S n
) M
 = llift 1 (llift n
 M
).




Lemma
 permute_llift_rec :

   ∀ M
 n
 k
 p
 i
,

   i
 ≤ k
 →

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




  Lemma
 permute_llift :

   ∀ M
 k
, llift 1 (llift_rec 1 M
 k
) = llift_rec 1 (llift 1 M
) (S k
).




Require
 Import
 Omega.




  Lemma
 simpl_lsubst_rec :

   ∀ M
 N
 n
 p
 k
,

   p
 ≤ n
 + k
 →

   k
 ≤ p
 → lsubst_rec N
 (llift_rec (S n
) M
 k
) p
 = llift_rec n
 M
 k
.




  Lemma
 simpl_lsubst :

   ∀ N
 M
 n
 p
, p
 ≤ n
 → lsubst_rec N
 (llift (S n
) M
) p
 = llift n
 M
.




  Lemma
 commut_llift_lsubst_rec :

   ∀ M
 N
 n
 p
 k
,

   k
 ≤ p
 →

   llift_rec n
 (lsubst_rec N
 M
 p
) k
 = lsubst_rec N
 (llift_rec n
 M
 k
) (n
 + p
).




  Lemma
 commut_llift_lsubst :

   ∀ M
 N
 k
, lsubst_rec N
 (llift 1 M
) (S k
) = llift 1 (lsubst_rec N
 M
 k
).




  Lemma
 distr_llift_lsubst_rec :

   ∀ M
 N
 n
 p
 k
,

   llift_rec n
 (lsubst_rec N
 M
 p
) (p
 + k
) =

   lsubst_rec (llift_rec n
 N
 k
) (llift_rec n
 M
 (S (p
 + k
))) p
.




Lemma
 distr_llift_lsubst :

   ∀ M
 N
 n
 k
,

   llift_rec n
 (lsubst N
 M
) k
 = lsubst (llift_rec n
 N
 k
) (llift_rec n
 M
 (S k
)).




  Lemma
 distr_lsubst_rec :

   ∀ M
 N
 (P
 : lterm) n
 p
,

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

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




  Lemma
 distr_lsubst :

   ∀ (P
 : lterm) N
 M
 k
,

   lsubst_rec P
 (lsubst N
 M
) k
 = lsubst (lsubst_rec P
 N
 k
) (lsubst_rec P
 M
 (S k
)).