standardization: equivalence between paths and left residuals started

[helm.git] / matita / matita / contribs / lambda / terms / delifting_substitution.ma

diff --git a/matita/matita/contribs/lambda/terms/delifting_substitution.ma b/matita/matita/contribs/lambda/terms/delifting_substitution.ma
index 7926c3948bec077d2a8ecb69e4b49b0d1d914f6d..3603fc031bf5104175636b56d3775730dcc37378 100644 (file)
--- a/matita/matita/contribs/lambda/terms/delifting_substitution.ma
+++ b/matita/matita/contribs/lambda/terms/delifting_substitution.ma
@@ -17,30 +17,30 @@ include "terms/lift.ma".
 (* DELIFTING SUBSTITUTION ***************************************************)
 
 (* Policy: depth (level) metavariables: d, e (as for lift) *)
-let rec dsubst D d M on M ≝ match M with
-[ VRef i   ⇒ tri … i d (#i) (↑[i] D) (#(i-1))
-| Abst A   ⇒ 𝛌. (dsubst D (d+1) A)
-| Appl B A ⇒ @ (dsubst D d B). (dsubst D d A)
+let rec dsubst N d M on M ≝ match M with
+[ VRef i   ⇒ tri … i d (#i) (↑[i] N) (#(i-1))
+| Abst A   ⇒ 𝛌. (dsubst N (d+1) A)
+| Appl B A ⇒ @ (dsubst N d B). (dsubst N d A)
 ].
 
 interpretation "delifting substitution"
-   'DSubst D d M = (dsubst D d M).
+   'DSubst N d M = (dsubst N d M).
 
-lemma dsubst_vref_lt: ∀i,d,D. i < d → [d ↙ D] #i = #i.
+lemma dsubst_vref_lt: ∀i,d,N. i < d → [d ↙ N] #i = #i.
 normalize /2 width=1/
 qed.
 
-lemma dsubst_vref_eq: ∀i,D. [i ↙ D] #i = ↑[i]D.
+lemma dsubst_vref_eq: ∀i,N. [i ↙ N] #i = ↑[i]N.
 normalize //
 qed.
 
-lemma dsubst_vref_gt: ∀i,d,D. d < i → [d ↙ D] #i = #(i-1).
+lemma dsubst_vref_gt: ∀i,d,N. d < i → [d ↙ N] #i = #(i-1).
 normalize /2 width=1/
 qed.
 
-theorem dsubst_lift_le: ∀h,D,M,d1,d2. d2 ≤ d1 →
-                        [d2 ↙ ↑[d1 - d2, h] D] ↑[d1 + 1, h] M = ↑[d1, h] [d2 ↙ D] M.
-#h #D #M elim M -M
+theorem dsubst_lift_le: ∀h,N,M,d1,d2. d2 ≤ d1 →
+                        [d2 ↙ ↑[d1 - d2, h] N] ↑[d1 + 1, h] M = ↑[d1, h] [d2 ↙ N] M.
+#h #N #M elim M -M
 [ #i #d1 #d2 #Hd21 elim (lt_or_eq_or_gt i d2) #Hid2
   [ lapply (lt_to_le_to_lt … Hid2 Hd21) -Hd21 #Hid1
     >(dsubst_vref_lt … Hid2) >(lift_vref_lt … Hid1) >lift_vref_lt /2 width=1/
@@ -58,9 +58,9 @@ theorem dsubst_lift_le: ∀h,D,M,d1,d2. d2 ≤ d1 →
 ]
 qed.
 
-theorem dsubst_lift_be: ∀h,D,M,d1,d2. d1 ≤ d2 → d2 ≤ d1 + h →
-                        [d2 ↙ D] ↑[d1, h + 1] M = ↑[d1, h] M.
-#h #D #M elim M -M
+theorem dsubst_lift_be: ∀h,N,M,d1,d2. d1 ≤ d2 → d2 ≤ d1 + h →
+                        [d2 ↙ N] ↑[d1, h + 1] M = ↑[d1, h] M.
+#h #N #M elim M -M
 [ #i #d1 #d2 #Hd12 #Hd21 elim (lt_or_ge i d1) #Hid1
   [ lapply (lt_to_le_to_lt … Hid1 Hd12) -Hd12 -Hd21 #Hid2
     >(lift_vref_lt … Hid1) >(lift_vref_lt … Hid1) /2 width=1/
@@ -75,9 +75,9 @@ theorem dsubst_lift_be: ∀h,D,M,d1,d2. d1 ≤ d2 → d2 ≤ d1 + h →
 ]
 qed.
 
-theorem dsubst_lift_ge: ∀h,D,M,d1,d2. d1 + h ≤ d2 →
-                        [d2 ↙ D] ↑[d1, h] M = ↑[d1, h] [d2 - h ↙ D] M.
-#h #D #M elim M -M
+theorem dsubst_lift_ge: ∀h,N,M,d1,d2. d1 + h ≤ d2 →
+                        [d2 ↙ N] ↑[d1, h] M = ↑[d1, h] [d2 - h ↙ N] M.
+#h #N #M elim M -M
 [ #i #d1 #d2 #Hd12 elim (lt_or_eq_or_gt i (d2-h)) #Hid2h
   [ >(dsubst_vref_lt … Hid2h) elim (lt_or_ge i d1) #Hid1
     [ lapply (lt_to_le_to_lt … (d1+h) Hid1 ?) -Hid2h // #Hid1h
@@ -102,9 +102,9 @@ theorem dsubst_lift_ge: ∀h,D,M,d1,d2. d1 + h ≤ d2 →
 ]
 qed.
 
-theorem dsubst_dsubst_ge: ∀D1,D2,M,d1,d2. d1 ≤ d2 →
-                          [d2 ↙ D2] [d1 ↙ D1] M = [d1 ↙ [d2 - d1 ↙ D2] D1] [d2 + 1 ↙ D2] M.
-#D1 #D2 #M elim M -M
+theorem dsubst_dsubst_ge: ∀N1,N2,M,d1,d2. d1 ≤ d2 →
+                          [d2 ↙ N2] [d1 ↙ N1] M = [d1 ↙ [d2 - d1 ↙ N2] N1] [d2 + 1 ↙ N2] M.
+#N1 #N2 #M elim M -M
 [ #i #d1 #d2 #Hd12 elim (lt_or_eq_or_gt i d1) #Hid1
   [ lapply (lt_to_le_to_lt … Hid1 Hd12) -Hd12 #Hid2
     >(dsubst_vref_lt … Hid1) >(dsubst_vref_lt … Hid2) >dsubst_vref_lt /2 width=1/
@@ -125,30 +125,30 @@ theorem dsubst_dsubst_ge: ∀D1,D2,M,d1,d2. d1 ≤ d2 →
 ]
 qed.
 
-theorem dsubst_dsubst_lt: ∀D1,D2,M,d1,d2. d2 < d1 →
-                          [d2 ↙ [d1 - d2 -1 ↙ D1] D2] [d1 ↙ D1] M = [d1 - 1 ↙ D1] [d2 ↙ D2] M.
-#D1 #D2 #M #d1 #d2 #Hd21
+theorem dsubst_dsubst_lt: ∀N1,N2,M,d1,d2. d2 < d1 →
+                          [d2 ↙ [d1 - d2 -1 ↙ N1] N2] [d1 ↙ N1] M = [d1 - 1 ↙ N1] [d2 ↙ N2] M.
+#N1 #N2 #M #d1 #d2 #Hd21
 lapply (ltn_to_ltO … Hd21) #Hd1
 >dsubst_dsubst_ge in ⊢ (???%); /2 width=1/ <plus_minus_m_m //
 qed.
 
 definition dsubstable_dx: predicate (relation term) ≝ λR.
-                          ∀D,M1,M2. R M1 M2 → ∀d. R ([d ↙ D] M1) ([d ↙ D] M2).
+                          ∀N,M1,M2. R M1 M2 → ∀d. R ([d ↙ N] M1) ([d ↙ N] M2).
 
 definition dsubstable: predicate (relation term) ≝ λR.
-                       ∀D1,D2. R D1 D2 → ∀M1,M2. R M1 M2 → ∀d. R ([d ↙ D1] M1) ([d ↙ D2] M2).
+                       ∀N1,N2. R N1 N2 → ∀M1,M2. R M1 M2 → ∀d. R ([d ↙ N1] M1) ([d ↙ N2] M2).
 
 lemma star_dsubstable_dx: ∀R. dsubstable_dx R → dsubstable_dx (star … R).
-#R #HR #D #M1 #M2 #H elim H -M2 // /3 width=3/
+#R #HR #N #M1 #M2 #H elim H -M2 // /3 width=3/
 qed.
 
 lemma lstar_dsubstable_dx: ∀S,R. (∀a. dsubstable_dx (R a)) →
                            ∀l. dsubstable_dx (lstar S … R l).
-#S #R #HR #l #D #M1 #M2 #H
+#S #R #HR #l #N #M1 #M2 #H
 @(lstar_ind_l ????????? H) -l -M1 // /3 width=3/
 qed.
 
 lemma star_dsubstable: ∀R. reflexive ? R →
                        dsubstable R → dsubstable (star … R).
-#R #H1R #H2 #D1 #D2 #H elim H -D2 /3 width=1/ /3 width=5/
+#R #H1R #H2 #N1 #N2 #H elim H -N2 /3 width=1/ /3 width=5/
 qed.