some restructuring

diff --git a/matita/matita/lib/lambda-delta/reduction/pr.ma b/matita/matita/lib/lambda-delta/reduction/pr.ma
deleted file mode 100644 (file)
index 3c5f4ca..0000000
--- a/matita/matita/lib/lambda-delta/reduction/pr.ma
+++ /dev/null
@@ -1,59 +0,0 @@
-(*
-    ||M||  This file is part of HELM, an Hypertextual, Electronic
-    ||A||  Library of Mathematics, developed at the Computer Science
-    ||T||  Department of the University of Bologna, Italy.
-    ||I||
-    ||T||
-    ||A||  This file is distributed under the terms of the
-    \   /  GNU General Public License Version 2
-     \ /
-      V_______________________________________________________________ *)
-
-include "lambda-delta/substitution/thin.ma".
-
-(* SINGLE STEP PARALLEL REDUCTION ON TERMS **********************************)
-
-inductive pr: lenv → term → term → Prop ≝
-| pr_sort : ∀L,k. pr L (⋆k) (⋆k)
-| pr_lref : ∀L,i. pr L (#i) (#i)
-| pr_bind : ∀L,I,V1,V2,T1,T2. pr L V1 V2 → pr (L. 𝕓{I} V1) T1 T2 →
-            pr L (𝕓{I} V1. T1) (𝕓{I} V2. T2)
-| pr_flat : ∀L,I,V1,V2,T1,T2. pr L V1 V2 → pr L T1 T2 →
-            pr L (𝕗{I} V1. T1) (𝕗{I} V2. T2)
-| pr_beta : ∀L,V1,V2,W,T1,T2.
-            pr L V1 V2 → pr (L. 𝕓{Abst} W) T1 T2 → (*𝕓*)
-            pr L (𝕚{Appl} V1. 𝕚{Abst} W. T1) (𝕚{Abbr} V2. T2)
-| pr_delta: ∀L,K,V1,V2,V,i.
-            ↓[0,i] L ≡ K. 𝕓{Abbr} V1 → pr K V1 V2 → ↑[0,i+1] V2 ≡ V →
-            pr L (#i) V
-| pr_theta: ∀L,V,V1,V2,W1,W2,T1,T2.
-            pr L V1 V2 → ↑[0,1] V2 ≡ V → pr L W1 W2 → pr (L. 𝕓{Abbr} W1) T1 T2 → (*𝕓*)
-            pr L (𝕚{Appl} V1. 𝕚{Abbr} W1. T1) (𝕚{Abbr} W2. 𝕚{Appl} V. T2)
-| pr_zeta : ∀L,V,T,T1,T2. ↑[0,1] T1 ≡ T → pr L T1 T2 →
-            pr L (𝕚{Abbr} V. T) T2
-| pr_tau  : ∀L,V,T1,T2. pr L T1 T2 → pr L (𝕚{Cast} V. T1) T2
-.
-
-interpretation
-   "single step parallel reduction (term)"
-   'PR L T1 T2 = (pr L T1 T2).
-
-(* The basic properties *****************************************************)
-
-lemma pr_refl: ∀T,L. L ⊢ T ⇒ T.
-#T elim T -T //
-#I elim I -I /2/
-qed.
-(*
-lemma subst_pr: ∀d,e,L,T1,U2. L ⊢ ↓[d,e] T1 ≡ U2 → ∀T2. ↑[d,e] U2 ≡ T2 →
-                L ⊢ T1 ⇒ T2.
-#d #e #L #T1 #U2 #H elim H -H d e L T1 U2
-[ #L #k #d #e #X #HX lapply (lift_inv_sort1 … HX) -HX #HX destruct -X // 
-| #L #i #d #e #Hid #X #HX lapply (lift_inv_sort1 … HX) -HX #HX destruct -X //
-| #L #V1 #V2 #e #HV12 * #V #HV2 #HV1
-  elim (lift_total 0 1 V1) #W1 #HVW1
-  @(ex2_1_intro … W1)
-  [
-  | /2 width=6/  
-
-*)
\ No newline at end of file

diff --git a/matita/matita/lib/lambda-delta/reduction/pr_defs.ma b/matita/matita/lib/lambda-delta/reduction/pr_defs.ma
new file mode 100644 (file)
index 0000000..e1cd216
--- /dev/null
+++ b/matita/matita/lib/lambda-delta/reduction/pr_defs.ma
@@ -0,0 +1,59 @@
+(*
+    ||M||  This file is part of HELM, an Hypertextual, Electronic
+    ||A||  Library of Mathematics, developed at the Computer Science
+    ||T||  Department of the University of Bologna, Italy.
+    ||I||
+    ||T||
+    ||A||  This file is distributed under the terms of the
+    \   /  GNU General Public License Version 2
+     \ /
+      V_______________________________________________________________ *)
+
+include "lambda-delta/substitution/thin_defs.ma".
+
+(* SINGLE STEP PARALLEL REDUCTION ON TERMS **********************************)
+
+inductive pr: lenv → term → term → Prop ≝
+| pr_sort : ∀L,k. pr L (⋆k) (⋆k)
+| pr_lref : ∀L,i. pr L (#i) (#i)
+| pr_bind : ∀L,I,V1,V2,T1,T2. pr L V1 V2 → pr (L. 𝕓{I} V1) T1 T2 →
+            pr L (𝕓{I} V1. T1) (𝕓{I} V2. T2)
+| pr_flat : ∀L,I,V1,V2,T1,T2. pr L V1 V2 → pr L T1 T2 →
+            pr L (𝕗{I} V1. T1) (𝕗{I} V2. T2)
+| pr_beta : ∀L,V1,V2,W,T1,T2.
+            pr L V1 V2 → pr (L. 𝕓{Abst} W) T1 T2 → (*𝕓*)
+            pr L (𝕚{Appl} V1. 𝕚{Abst} W. T1) (𝕚{Abbr} V2. T2)
+| pr_delta: ∀L,K,V1,V2,V,i.
+            ↓[0,i] L ≡ K. 𝕓{Abbr} V1 → pr K V1 V2 → ↑[0,i+1] V2 ≡ V →
+            pr L (#i) V
+| pr_theta: ∀L,V,V1,V2,W1,W2,T1,T2.
+            pr L V1 V2 → ↑[0,1] V2 ≡ V → pr L W1 W2 → pr (L. 𝕓{Abbr} W1) T1 T2 → (*𝕓*)
+            pr L (𝕚{Appl} V1. 𝕚{Abbr} W1. T1) (𝕚{Abbr} W2. 𝕚{Appl} V. T2)
+| pr_zeta : ∀L,V,T,T1,T2. ↑[0,1] T1 ≡ T → pr L T1 T2 →
+            pr L (𝕚{Abbr} V. T) T2
+| pr_tau  : ∀L,V,T1,T2. pr L T1 T2 → pr L (𝕚{Cast} V. T1) T2
+.
+
+interpretation
+   "single step parallel reduction (term)"
+   'PR L T1 T2 = (pr L T1 T2).
+
+(* The basic properties *****************************************************)
+
+lemma pr_refl: ∀T,L. L ⊢ T ⇒ T.
+#T elim T -T //
+#I elim I -I /2/
+qed.
+(*
+lemma subst_pr: ∀d,e,L,T1,U2. L ⊢ ↓[d,e] T1 ≡ U2 → ∀T2. ↑[d,e] U2 ≡ T2 →
+                L ⊢ T1 ⇒ T2.
+#d #e #L #T1 #U2 #H elim H -H d e L T1 U2
+[ #L #k #d #e #X #HX lapply (lift_inv_sort1 … HX) -HX #HX destruct -X // 
+| #L #i #d #e #Hid #X #HX lapply (lift_inv_sort1 … HX) -HX #HX destruct -X //
+| #L #V1 #V2 #e #HV12 * #V #HV2 #HV1
+  elim (lift_total 0 1 V1) #W1 #HVW1
+  @(ex2_1_intro … W1)
+  [
+  | /2 width=6/  
+
+*)
\ No newline at end of file

diff --git a/matita/matita/lib/lambda-delta/substitution/lift.ma b/matita/matita/lib/lambda-delta/substitution/lift.ma
deleted file mode 100644 (file)
index 60b1b62..0000000
--- a/matita/matita/lib/lambda-delta/substitution/lift.ma
+++ /dev/null
@@ -1,266 +0,0 @@
-(*
-    ||M||  This file is part of HELM, an Hypertextual, Electronic
-    ||A||  Library of Mathematics, developed at the Computer Science
-    ||T||  Department of the University of Bologna, Italy.
-    ||I||
-    ||T||
-    ||A||  This file is distributed under the terms of the
-    \   /  GNU General Public License Version 2
-     \ /
-      V_______________________________________________________________ *)
-
-include "lambda-delta/syntax/term.ma".
-
-(* RELOCATION ***************************************************************)
-
-inductive lift: term → nat → nat → term → Prop ≝
-| lift_sort   : ∀k,d,e. lift (⋆k) d e (⋆k)
-| lift_lref_lt: ∀i,d,e. i < d → lift (#i) d e (#i)
-| lift_lref_ge: ∀i,d,e. d ≤ i → lift (#i) d e (#(i + e))
-| lift_bind   : ∀I,V1,V2,T1,T2,d,e.
-                lift V1 d e V2 → lift T1 (d + 1) e T2 →
-                lift (𝕓{I} V1. T1) d e (𝕓{I} V2. T2)
-| lift_flat   : ∀I,V1,V2,T1,T2,d,e.
-                lift V1 d e V2 → lift T1 d e T2 →
-                lift (𝕗{I} V1. T1) d e (𝕗{I} V2. T2)
-.
-
-interpretation "relocation" 'RLift T1 d e T2 = (lift T1 d e T2).
-
-(* The basic properties *****************************************************)
-
-lemma lift_lref_ge_minus: ∀d,e,i. d + e ≤ i → ↑[d,e] #(i - e) ≡ #i.
-#d #e #i #H >(plus_minus_m_m i e) in ⊢ (? ? ? ? %) /3/
-qed.
-
-(* The basic inversion lemmas ***********************************************)
-
-lemma lift_inv_sort1_aux: ∀d,e,T1,T2. ↑[d,e] T1 ≡ T2 → ∀k. T1 = ⋆k → T2 = ⋆k.
-#d #e #T1 #T2 #H elim H -H d e T1 T2 //
-[ #i #d #e #_ #k #H destruct
-| #I #V1 #V2 #T1 #T2 #d #e #_ #_ #_ #_ #k #H destruct
-| #I #V1 #V2 #T1 #T2 #d #e #_ #_ #_ #_ #k #H destruct
-]
-qed.
-
-lemma lift_inv_sort1: ∀d,e,T2,k. ↑[d,e] ⋆k ≡ T2 → T2 = ⋆k.
-#d #e #T2 #k #H lapply (lift_inv_sort1_aux … H) /2/
-qed.
-
-lemma lift_inv_lref1_aux: ∀d,e,T1,T2. ↑[d,e] T1 ≡ T2 → ∀i. T1 = #i →
-                          (i < d ∧ T2 = #i) ∨ (d ≤ i ∧ T2 = #(i + e)).
-#d #e #T1 #T2 #H elim H -H d e T1 T2
-[ #k #d #e #i #H destruct
-| #j #d #e #Hj #i #Hi destruct /3/
-| #j #d #e #Hj #i #Hi destruct /3/
-| #I #V1 #V2 #T1 #T2 #d #e #_ #_ #_ #_ #i #H destruct
-| #I #V1 #V2 #T1 #T2 #d #e #_ #_ #_ #_ #i #H destruct
-]
-qed.
-
-lemma lift_inv_lref1: ∀d,e,T2,i. ↑[d,e] #i ≡ T2 →
-                      (i < d ∧ T2 = #i) ∨ (d ≤ i ∧ T2 = #(i + e)).
-#d #e #T2 #i #H lapply (lift_inv_lref1_aux … H) /2/
-qed.
-
-lemma lift_inv_bind1_aux: ∀d,e,T1,T2. ↑[d,e] T1 ≡ T2 →
-                          ∀I,V1,U1. T1 = 𝕓{I} V1.U1 →
-                          ∃∃V2,U2. ↑[d,e] V1 ≡ V2 & ↑[d+1,e] U1 ≡ U2 &
-                                   T2 = 𝕓{I} V2. U2.
-#d #e #T1 #T2 #H elim H -H d e T1 T2
-[ #k #d #e #I #V1 #U1 #H destruct
-| #i #d #e #_ #I #V1 #U1 #H destruct
-| #i #d #e #_ #I #V1 #U1 #H destruct
-| #J #W1 #W2 #T1 #T2 #d #e #HW #HT #_ #_ #I #V1 #U1 #H destruct /2 width=5/
-| #J #W1 #W2 #T1 #T2 #d #e #HW #HT #_ #_ #I #V1 #U1 #H destruct
-]
-qed.
-
-lemma lift_inv_bind1: ∀d,e,T2,I,V1,U1. ↑[d,e] 𝕓{I} V1. U1 ≡ T2 →
-                      ∃∃V2,U2. ↑[d,e] V1 ≡ V2 & ↑[d+1,e] U1 ≡ U2 &
-                               T2 = 𝕓{I} V2. U2.
-#d #e #T2 #I #V1 #U1 #H lapply (lift_inv_bind1_aux … H) /2/
-qed.
-
-lemma lift_inv_flat1_aux: ∀d,e,T1,T2. ↑[d,e] T1 ≡ T2 →
-                          ∀I,V1,U1. T1 = 𝕗{I} V1.U1 →
-                          ∃∃V2,U2. ↑[d,e] V1 ≡ V2 & ↑[d,e] U1 ≡ U2 &
-                                   T2 = 𝕗{I} V2. U2.
-#d #e #T1 #T2 #H elim H -H d e T1 T2
-[ #k #d #e #I #V1 #U1 #H destruct
-| #i #d #e #_ #I #V1 #U1 #H destruct
-| #i #d #e #_ #I #V1 #U1 #H destruct
-| #J #W1 #W2 #T1 #T2 #d #e #HW #HT #_ #_ #I #V1 #U1 #H destruct
-| #J #W1 #W2 #T1 #T2 #d #e #HW #HT #_ #_ #I #V1 #U1 #H destruct /2 width=5/
-]
-qed.
-
-lemma lift_inv_flat1: ∀d,e,T2,I,V1,U1. ↑[d,e] 𝕗{I} V1. U1 ≡ T2 →
-                      ∃∃V2,U2. ↑[d,e] V1 ≡ V2 & ↑[d,e] U1 ≡ U2 &
-                               T2 = 𝕗{I} V2. U2.
-#d #e #T2 #I #V1 #U1 #H lapply (lift_inv_flat1_aux … H) /2/
-qed.
-
-lemma lift_inv_sort2_aux: ∀d,e,T1,T2. ↑[d,e] T1 ≡ T2 → ∀k. T2 = ⋆k → T1 = ⋆k.
-#d #e #T1 #T2 #H elim H -H d e T1 T2 //
-[ #i #d #e #_ #k #H destruct
-| #I #V1 #V2 #T1 #T2 #d #e #_ #_ #_ #_ #k #H destruct
-| #I #V1 #V2 #T1 #T2 #d #e #_ #_ #_ #_ #k #H destruct
-]
-qed.
-
-lemma lift_inv_sort2: ∀d,e,T1,k. ↑[d,e] T1 ≡ ⋆k → T1 = ⋆k.
-#d #e #T1 #k #H lapply (lift_inv_sort2_aux … H) /2/
-qed.
-
-lemma lift_inv_lref2_aux: ∀d,e,T1,T2. ↑[d,e] T1 ≡ T2 → ∀i. T2 = #i →
-                          (i < d ∧ T1 = #i) ∨ (d + e ≤ i ∧ T1 = #(i - e)).
-#d #e #T1 #T2 #H elim H -H d e T1 T2
-[ #k #d #e #i #H destruct
-| #j #d #e #Hj #i #Hi destruct /3/
-| #j #d #e #Hj #i #Hi destruct <minus_plus_m_m /4/
-| #I #V1 #V2 #T1 #T2 #d #e #_ #_ #_ #_ #i #H destruct
-| #I #V1 #V2 #T1 #T2 #d #e #_ #_ #_ #_ #i #H destruct
-]
-qed.
-
-lemma lift_inv_lref2: ∀d,e,T1,i. ↑[d,e] T1 ≡ #i →
-                      (i < d ∧ T1 = #i) ∨ (d + e ≤ i ∧ T1 = #(i - e)).
-#d #e #T1 #i #H lapply (lift_inv_lref2_aux … H) /2/
-qed.
-
-lemma lift_inv_bind2_aux: ∀d,e,T1,T2. ↑[d,e] T1 ≡ T2 →
-                          ∀I,V2,U2. T2 = 𝕓{I} V2.U2 →
-                          ∃∃V1,U1. ↑[d,e] V1 ≡ V2 & ↑[d+1,e] U1 ≡ U2 &
-                                   T1 = 𝕓{I} V1. U1.
-#d #e #T1 #T2 #H elim H -H d e T1 T2
-[ #k #d #e #I #V2 #U2 #H destruct
-| #i #d #e #_ #I #V2 #U2 #H destruct
-| #i #d #e #_ #I #V2 #U2 #H destruct
-| #J #W1 #W2 #T1 #T2 #d #e #HW #HT #_ #_ #I #V2 #U2 #H destruct /2 width=5/
-| #J #W1 #W2 #T1 #T2 #d #e #HW #HT #_ #_ #I #V2 #U2 #H destruct
-]
-qed.
-
-lemma lift_inv_bind2: ∀d,e,T1,I,V2,U2. ↑[d,e] T1 ≡  𝕓{I} V2. U2 →
-                      ∃∃V1,U1. ↑[d,e] V1 ≡ V2 & ↑[d+1,e] U1 ≡ U2 &
-                               T1 = 𝕓{I} V1. U1.
-#d #e #T1 #I #V2 #U2 #H lapply (lift_inv_bind2_aux … H) /2/
-qed.
-
-lemma lift_inv_flat2_aux: ∀d,e,T1,T2. ↑[d,e] T1 ≡ T2 →
-                          ∀I,V2,U2. T2 = 𝕗{I} V2.U2 →
-                          ∃∃V1,U1. ↑[d,e] V1 ≡ V2 & ↑[d,e] U1 ≡ U2 &
-                                   T1 = 𝕗{I} V1. U1.
-#d #e #T1 #T2 #H elim H -H d e T1 T2
-[ #k #d #e #I #V2 #U2 #H destruct
-| #i #d #e #_ #I #V2 #U2 #H destruct
-| #i #d #e #_ #I #V2 #U2 #H destruct
-| #J #W1 #W2 #T1 #T2 #d #e #HW #HT #_ #_ #I #V2 #U2 #H destruct
-| #J #W1 #W2 #T1 #T2 #d #e #HW #HT #_ #_ #I #V2 #U2 #H destruct /2 width = 5/
-]
-qed.
-
-lemma lift_inv_flat2: ∀d,e,T1,I,V2,U2. ↑[d,e] T1 ≡  𝕗{I} V2. U2 →
-                      ∃∃V1,U1. ↑[d,e] V1 ≡ V2 & ↑[d,e] U1 ≡ U2 &
-                               T1 = 𝕗{I} V1. U1.
-#d #e #T1 #I #V2 #U2 #H lapply (lift_inv_flat2_aux … H) /2/
-qed.
-
-(* the main properies *******************************************************)
-
-axiom lift_total: ∀d,e,T1. ∃T2. ↑[d,e] T1 ≡ T2.
-
-axiom lift_mono:  ∀d,e,T,U1. ↑[d,e] T ≡ U1 → ∀U2. ↑[d,e] T ≡ U2 → U1 = U2.
-
-theorem lift_conf_rev: ∀d1,e1,T1,T. ↑[d1,e1] T1 ≡ T →
-                       ∀d2,e2,T2. ↑[d2 + e1, e2] T2 ≡ T →
-                       d1 ≤ d2 →
-                       ∃∃T0. ↑[d1, e1] T0 ≡ T2 & ↑[d2, e2] T0 ≡ T1.
-#d1 #e1 #T1 #T #H elim H -H d1 e1 T1 T
-[ #k #d1 #e1 #d2 #e2 #T2 #Hk #Hd12
-  lapply (lift_inv_sort2 … Hk) -Hk #Hk destruct -T2 /3/
-| #i #d1 #e1 #Hid1 #d2 #e2 #T2 #Hi #Hd12
-  lapply (lift_inv_lref2 … Hi) -Hi * * #Hid2 #H destruct -T2
-  [ -Hid2 /4/
-  | elim (lt_false d1 ?)
-    @(le_to_lt_to_lt … Hd12) -Hd12 @(le_to_lt_to_lt … Hid1) -Hid1 /2/
-  ]
-| #i #d1 #e1 #Hid1 #d2 #e2 #T2 #Hi #Hd12
-  lapply (lift_inv_lref2 … Hi) -Hi * * #Hid2 #H destruct -T2
-  [ -Hd12; lapply (lt_plus_to_lt_l … Hid2) -Hid2 #Hid2 /3/
-  | -Hid1; lapply (arith1 … Hid2) -Hid2 #Hid2
-    @(ex2_1_intro … #(i - e2))
-    [ >le_plus_minus_comm [ @lift_lref_ge @(transitive_le … Hd12) -Hd12 /2/ | -Hd12 /2/ ]
-    | -Hd12 >(plus_minus_m_m i e2) in ⊢ (? ? ? ? %) /3/
-    ]
-  ]
-| #I #W1 #W #U1 #U #d1 #e1 #_ #_ #IHW #IHU #d2 #e2 #T2 #H #Hd12
-  lapply (lift_inv_bind2 … H) -H * #W2 #U2 #HW2 #HU2 #H destruct -T2;
-  elim (IHW … HW2 ?) // -IHW HW2 #W0 #HW2 #HW1
-  >plus_plus_comm_23 in HU2 #HU2 elim (IHU … HU2 ?) /3 width = 5/
-| #I #W1 #W #U1 #U #d1 #e1 #_ #_ #IHW #IHU #d2 #e2 #T2 #H #Hd12
-  lapply (lift_inv_flat2 … H) -H * #W2 #U2 #HW2 #HU2 #H destruct -T2;
-  elim (IHW … HW2 ?) // -IHW HW2 #W0 #HW2 #HW1
-  elim (IHU … HU2 ?) /3 width = 5/
-]
-qed.
-
-theorem lift_free: ∀d1,e2,T1,T2. ↑[d1, e2] T1 ≡ T2 → ∀d2,e1.
-                                 d1 ≤ d2 → d2 ≤ d1 + e1 → e1 ≤ e2 →
-                                 ∃∃T. ↑[d1, e1] T1 ≡ T & ↑[d2, e2 - e1] T ≡ T2.
-#d1 #e2 #T1 #T2 #H elim H -H d1 e2 T1 T2
-[ /3/
-| #i #d1 #e2 #Hid1 #d2 #e1 #Hd12 #_ #_
-  lapply (lt_to_le_to_lt … Hid1 Hd12) -Hd12 #Hid2 /4/
-| #i #d1 #e2 #Hid1 #d2 #e1 #_ #Hd21 #He12
-  lapply (transitive_le …(i+e1) Hd21 ?) /2/ -Hd21 #Hd21
-  <(plus_plus_minus_m_m e1 e2 i) /3/
-| #I #V1 #V2 #T1 #T2 #d1 #e2 #_ #_ #IHV #IHT #d2 #e1 #Hd12 #Hd21 #He12
-  elim (IHV … Hd12 Hd21 He12) -IHV #V0 #HV0a #HV0b
-  elim (IHT (d2+1) … ? ? He12) /3 width = 5/
-| #I #V1 #V2 #T1 #T2 #d1 #e2 #_ #_ #IHV #IHT #d2 #e1 #Hd12 #Hd21 #He12
-  elim (IHV … Hd12 Hd21 He12) -IHV #V0 #HV0a #HV0b
-  elim (IHT d2 … ? ? He12) /3 width = 5/
-]
-qed.
-
-theorem lift_trans: ∀d1,e1,T1,T. ↑[d1, e1] T1 ≡ T →
-                    ∀d2,e2,T2. ↑[d2, e2] T ≡ T2 →
-                    d1 ≤ d2 → d2 ≤ d1 + e1 → ↑[d1, e1 + e2] T1 ≡ T2.
-#d1 #e1 #T1 #T #H elim H -d1 e1 T1 T
-[ #k #d1 #e1 #d2 #e2 #T2 #HT2 #_ #_
-  >(lift_inv_sort1 … HT2) -HT2 //
-| #i #d1 #e1 #Hid1 #d2 #e2 #T2 #HT2 #Hd12 #_
-  lapply (lift_inv_lref1 … HT2) -HT2 * * #Hid2 #H destruct -T2
-  [ -Hd12 Hid2 /2/
-  | lapply (le_to_lt_to_lt … d1 Hid2 ?) // -Hid1 Hid2 #Hd21
-    lapply (le_to_lt_to_lt … d1 Hd12 ?) // -Hd12 Hd21 #Hd11
-    elim (lt_false … Hd11)
-  ]
-| #i #d1 #e1 #Hid1 #d2 #e2 #T2 #HT2 #_ #Hd21
-  lapply (lift_inv_lref1 … HT2) -HT2 * * #Hid2 #H destruct -T2
-  [ lapply (lt_to_le_to_lt … (d1+e1) Hid2 ?) // -Hid2 Hd21 #H
-    lapply (lt_plus_to_lt_l … H) -H #H
-    lapply (le_to_lt_to_lt … d1 Hid1 ?) // -Hid1 H #Hd11
-    elim (lt_false … Hd11)
-  | -Hd21 Hid2 /2/
-  ]
-| #I #V1 #V2 #T1 #T2 #d1 #e1 #_ #_ #IHV12 #IHT12 #d2 #e2 #X #HX #Hd12 #Hd21
-  lapply (lift_inv_bind1 … HX) -HX * #V0 #T0 #HV20 #HT20 #HX destruct -X;
-  lapply (IHV12 … HV20 ? ?) // -IHV12 HV20 #HV10
-  lapply (IHT12 … HT20 ? ?) /2/
-| #I #V1 #V2 #T1 #T2 #d1 #e1 #_ #_ #IHV12 #IHT12 #d2 #e2 #X #HX #Hd12 #Hd21
-  lapply (lift_inv_flat1 … HX) -HX * #V0 #T0 #HV20 #HT20 #HX destruct -X;
-  lapply (IHV12 … HV20 ? ?) // -IHV12 HV20 #HV10
-  lapply (IHT12 … HT20 ? ?) /2/
-]
-qed.
-
-axiom lift_trans_le: ∀d1,e1,T1,T. ↑[d1, e1] T1 ≡ T →
-                     ∀d2,e2,T2. ↑[d2, e2] T ≡ T2 → d2 ≤ d1 →
-                     ∃∃T0. ↑[d2, e2] T1 ≡ T0 & ↑[d1 + e2, e1] T0 ≡ T2.
-
-axiom lift_trans_ge: ∀d1,e1,T1,T. ↑[d1, e1] T1 ≡ T →
-                     ∀d2,e2,T2. ↑[d2, e2] T ≡ T2 → d1 + e1 ≤ d2 →
-                     ∃∃T0. ↑[d2 - e1, e2] T1 ≡ T0 & ↑[d1, e1] T0 ≡ T2.

diff --git a/matita/matita/lib/lambda-delta/substitution/lift_defs.ma b/matita/matita/lib/lambda-delta/substitution/lift_defs.ma
new file mode 100644 (file)
index 0000000..86e1b75
--- /dev/null
+++ b/matita/matita/lib/lambda-delta/substitution/lift_defs.ma
@@ -0,0 +1,168 @@
+(*
+    ||M||  This file is part of HELM, an Hypertextual, Electronic
+    ||A||  Library of Mathematics, developed at the Computer Science
+    ||T||  Department of the University of Bologna, Italy.
+    ||I||
+    ||T||
+    ||A||  This file is distributed under the terms of the
+    \   /  GNU General Public License Version 2
+     \ /
+      V_______________________________________________________________ *)
+
+include "lambda-delta/syntax/term.ma".
+
+(* RELOCATION ***************************************************************)
+
+inductive lift: term → nat → nat → term → Prop ≝
+| lift_sort   : ∀k,d,e. lift (⋆k) d e (⋆k)
+| lift_lref_lt: ∀i,d,e. i < d → lift (#i) d e (#i)
+| lift_lref_ge: ∀i,d,e. d ≤ i → lift (#i) d e (#(i + e))
+| lift_bind   : ∀I,V1,V2,T1,T2,d,e.
+                lift V1 d e V2 → lift T1 (d + 1) e T2 →
+                lift (𝕓{I} V1. T1) d e (𝕓{I} V2. T2)
+| lift_flat   : ∀I,V1,V2,T1,T2,d,e.
+                lift V1 d e V2 → lift T1 d e T2 →
+                lift (𝕗{I} V1. T1) d e (𝕗{I} V2. T2)
+.
+
+interpretation "relocation" 'RLift T1 d e T2 = (lift T1 d e T2).
+
+(* The basic properties *****************************************************)
+
+lemma lift_lref_ge_minus: ∀d,e,i. d + e ≤ i → ↑[d,e] #(i - e) ≡ #i.
+#d #e #i #H >(plus_minus_m_m i e) in ⊢ (? ? ? ? %) /3/
+qed.
+
+(* The basic inversion lemmas ***********************************************)
+
+lemma lift_inv_sort1_aux: ∀d,e,T1,T2. ↑[d,e] T1 ≡ T2 → ∀k. T1 = ⋆k → T2 = ⋆k.
+#d #e #T1 #T2 #H elim H -H d e T1 T2 //
+[ #i #d #e #_ #k #H destruct
+| #I #V1 #V2 #T1 #T2 #d #e #_ #_ #_ #_ #k #H destruct
+| #I #V1 #V2 #T1 #T2 #d #e #_ #_ #_ #_ #k #H destruct
+]
+qed.
+
+lemma lift_inv_sort1: ∀d,e,T2,k. ↑[d,e] ⋆k ≡ T2 → T2 = ⋆k.
+#d #e #T2 #k #H lapply (lift_inv_sort1_aux … H) /2/
+qed.
+
+lemma lift_inv_lref1_aux: ∀d,e,T1,T2. ↑[d,e] T1 ≡ T2 → ∀i. T1 = #i →
+                          (i < d ∧ T2 = #i) ∨ (d ≤ i ∧ T2 = #(i + e)).
+#d #e #T1 #T2 #H elim H -H d e T1 T2
+[ #k #d #e #i #H destruct
+| #j #d #e #Hj #i #Hi destruct /3/
+| #j #d #e #Hj #i #Hi destruct /3/
+| #I #V1 #V2 #T1 #T2 #d #e #_ #_ #_ #_ #i #H destruct
+| #I #V1 #V2 #T1 #T2 #d #e #_ #_ #_ #_ #i #H destruct
+]
+qed.
+
+lemma lift_inv_lref1: ∀d,e,T2,i. ↑[d,e] #i ≡ T2 →
+                      (i < d ∧ T2 = #i) ∨ (d ≤ i ∧ T2 = #(i + e)).
+#d #e #T2 #i #H lapply (lift_inv_lref1_aux … H) /2/
+qed.
+
+lemma lift_inv_bind1_aux: ∀d,e,T1,T2. ↑[d,e] T1 ≡ T2 →
+                          ∀I,V1,U1. T1 = 𝕓{I} V1.U1 →
+                          ∃∃V2,U2. ↑[d,e] V1 ≡ V2 & ↑[d+1,e] U1 ≡ U2 &
+                                   T2 = 𝕓{I} V2. U2.
+#d #e #T1 #T2 #H elim H -H d e T1 T2
+[ #k #d #e #I #V1 #U1 #H destruct
+| #i #d #e #_ #I #V1 #U1 #H destruct
+| #i #d #e #_ #I #V1 #U1 #H destruct
+| #J #W1 #W2 #T1 #T2 #d #e #HW #HT #_ #_ #I #V1 #U1 #H destruct /2 width=5/
+| #J #W1 #W2 #T1 #T2 #d #e #HW #HT #_ #_ #I #V1 #U1 #H destruct
+]
+qed.
+
+lemma lift_inv_bind1: ∀d,e,T2,I,V1,U1. ↑[d,e] 𝕓{I} V1. U1 ≡ T2 →
+                      ∃∃V2,U2. ↑[d,e] V1 ≡ V2 & ↑[d+1,e] U1 ≡ U2 &
+                               T2 = 𝕓{I} V2. U2.
+#d #e #T2 #I #V1 #U1 #H lapply (lift_inv_bind1_aux … H) /2/
+qed.
+
+lemma lift_inv_flat1_aux: ∀d,e,T1,T2. ↑[d,e] T1 ≡ T2 →
+                          ∀I,V1,U1. T1 = 𝕗{I} V1.U1 →
+                          ∃∃V2,U2. ↑[d,e] V1 ≡ V2 & ↑[d,e] U1 ≡ U2 &
+                                   T2 = 𝕗{I} V2. U2.
+#d #e #T1 #T2 #H elim H -H d e T1 T2
+[ #k #d #e #I #V1 #U1 #H destruct
+| #i #d #e #_ #I #V1 #U1 #H destruct
+| #i #d #e #_ #I #V1 #U1 #H destruct
+| #J #W1 #W2 #T1 #T2 #d #e #HW #HT #_ #_ #I #V1 #U1 #H destruct
+| #J #W1 #W2 #T1 #T2 #d #e #HW #HT #_ #_ #I #V1 #U1 #H destruct /2 width=5/
+]
+qed.
+
+lemma lift_inv_flat1: ∀d,e,T2,I,V1,U1. ↑[d,e] 𝕗{I} V1. U1 ≡ T2 →
+                      ∃∃V2,U2. ↑[d,e] V1 ≡ V2 & ↑[d,e] U1 ≡ U2 &
+                               T2 = 𝕗{I} V2. U2.
+#d #e #T2 #I #V1 #U1 #H lapply (lift_inv_flat1_aux … H) /2/
+qed.
+
+lemma lift_inv_sort2_aux: ∀d,e,T1,T2. ↑[d,e] T1 ≡ T2 → ∀k. T2 = ⋆k → T1 = ⋆k.
+#d #e #T1 #T2 #H elim H -H d e T1 T2 //
+[ #i #d #e #_ #k #H destruct
+| #I #V1 #V2 #T1 #T2 #d #e #_ #_ #_ #_ #k #H destruct
+| #I #V1 #V2 #T1 #T2 #d #e #_ #_ #_ #_ #k #H destruct
+]
+qed.
+
+lemma lift_inv_sort2: ∀d,e,T1,k. ↑[d,e] T1 ≡ ⋆k → T1 = ⋆k.
+#d #e #T1 #k #H lapply (lift_inv_sort2_aux … H) /2/
+qed.
+
+lemma lift_inv_lref2_aux: ∀d,e,T1,T2. ↑[d,e] T1 ≡ T2 → ∀i. T2 = #i →
+                          (i < d ∧ T1 = #i) ∨ (d + e ≤ i ∧ T1 = #(i - e)).
+#d #e #T1 #T2 #H elim H -H d e T1 T2
+[ #k #d #e #i #H destruct
+| #j #d #e #Hj #i #Hi destruct /3/
+| #j #d #e #Hj #i #Hi destruct <minus_plus_m_m /4/
+| #I #V1 #V2 #T1 #T2 #d #e #_ #_ #_ #_ #i #H destruct
+| #I #V1 #V2 #T1 #T2 #d #e #_ #_ #_ #_ #i #H destruct
+]
+qed.
+
+lemma lift_inv_lref2: ∀d,e,T1,i. ↑[d,e] T1 ≡ #i →
+                      (i < d ∧ T1 = #i) ∨ (d + e ≤ i ∧ T1 = #(i - e)).
+#d #e #T1 #i #H lapply (lift_inv_lref2_aux … H) /2/
+qed.
+
+lemma lift_inv_bind2_aux: ∀d,e,T1,T2. ↑[d,e] T1 ≡ T2 →
+                          ∀I,V2,U2. T2 = 𝕓{I} V2.U2 →
+                          ∃∃V1,U1. ↑[d,e] V1 ≡ V2 & ↑[d+1,e] U1 ≡ U2 &
+                                   T1 = 𝕓{I} V1. U1.
+#d #e #T1 #T2 #H elim H -H d e T1 T2
+[ #k #d #e #I #V2 #U2 #H destruct
+| #i #d #e #_ #I #V2 #U2 #H destruct
+| #i #d #e #_ #I #V2 #U2 #H destruct
+| #J #W1 #W2 #T1 #T2 #d #e #HW #HT #_ #_ #I #V2 #U2 #H destruct /2 width=5/
+| #J #W1 #W2 #T1 #T2 #d #e #HW #HT #_ #_ #I #V2 #U2 #H destruct
+]
+qed.
+
+lemma lift_inv_bind2: ∀d,e,T1,I,V2,U2. ↑[d,e] T1 ≡  𝕓{I} V2. U2 →
+                      ∃∃V1,U1. ↑[d,e] V1 ≡ V2 & ↑[d+1,e] U1 ≡ U2 &
+                               T1 = 𝕓{I} V1. U1.
+#d #e #T1 #I #V2 #U2 #H lapply (lift_inv_bind2_aux … H) /2/
+qed.
+
+lemma lift_inv_flat2_aux: ∀d,e,T1,T2. ↑[d,e] T1 ≡ T2 →
+                          ∀I,V2,U2. T2 = 𝕗{I} V2.U2 →
+                          ∃∃V1,U1. ↑[d,e] V1 ≡ V2 & ↑[d,e] U1 ≡ U2 &
+                                   T1 = 𝕗{I} V1. U1.
+#d #e #T1 #T2 #H elim H -H d e T1 T2
+[ #k #d #e #I #V2 #U2 #H destruct
+| #i #d #e #_ #I #V2 #U2 #H destruct
+| #i #d #e #_ #I #V2 #U2 #H destruct
+| #J #W1 #W2 #T1 #T2 #d #e #HW #HT #_ #_ #I #V2 #U2 #H destruct
+| #J #W1 #W2 #T1 #T2 #d #e #HW #HT #_ #_ #I #V2 #U2 #H destruct /2 width = 5/
+]
+qed.
+
+lemma lift_inv_flat2: ∀d,e,T1,I,V2,U2. ↑[d,e] T1 ≡  𝕗{I} V2. U2 →
+                      ∃∃V1,U1. ↑[d,e] V1 ≡ V2 & ↑[d,e] U1 ≡ U2 &
+                               T1 = 𝕗{I} V1. U1.
+#d #e #T1 #I #V2 #U2 #H lapply (lift_inv_flat2_aux … H) /2/
+qed.

diff --git a/matita/matita/lib/lambda-delta/substitution/lift_fun.ma b/matita/matita/lib/lambda-delta/substitution/lift_fun.ma
new file mode 100644 (file)
index 0000000..ee54ded
--- /dev/null
+++ b/matita/matita/lib/lambda-delta/substitution/lift_fun.ma
@@ -0,0 +1,25 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "lambda-delta/substitution/lift_defs.ma".
+
+(* RELOCATION ***************************************************************)
+
+(* the functional properties **************************************************)
+
+axiom lift_total: ∀d,e,T1. ∃T2. ↑[d,e] T1 ≡ T2.
+
+axiom lift_mono:  ∀d,e,T,U1. ↑[d,e] T ≡ U1 → ∀U2. ↑[d,e] T ≡ U2 → U1 = U2.
+
+axiom lift_inj:  ∀d,e,T1,U. ↑[d,e] T1 ≡ U → ∀T2. ↑[d,e] T2 ≡ U → T1 = T2.

diff --git a/matita/matita/lib/lambda-delta/substitution/lift_main.ma b/matita/matita/lib/lambda-delta/substitution/lift_main.ma
new file mode 100644 (file)
index 0000000..2f588c1
--- /dev/null
+++ b/matita/matita/lib/lambda-delta/substitution/lift_main.ma
@@ -0,0 +1,111 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "lambda-delta/substitution/lift_defs.ma".
+
+(* RELOCATION ***************************************************************)
+
+(* the main properies *******************************************************)
+
+theorem lift_conf_rev: ∀d1,e1,T1,T. ↑[d1,e1] T1 ≡ T →
+                       ∀d2,e2,T2. ↑[d2 + e1, e2] T2 ≡ T →
+                       d1 ≤ d2 →
+                       ∃∃T0. ↑[d1, e1] T0 ≡ T2 & ↑[d2, e2] T0 ≡ T1.
+#d1 #e1 #T1 #T #H elim H -H d1 e1 T1 T
+[ #k #d1 #e1 #d2 #e2 #T2 #Hk #Hd12
+  lapply (lift_inv_sort2 … Hk) -Hk #Hk destruct -T2 /3/
+| #i #d1 #e1 #Hid1 #d2 #e2 #T2 #Hi #Hd12
+  lapply (lift_inv_lref2 … Hi) -Hi * * #Hid2 #H destruct -T2
+  [ -Hid2 /4/
+  | elim (lt_false d1 ?)
+    @(le_to_lt_to_lt … Hd12) -Hd12 @(le_to_lt_to_lt … Hid1) -Hid1 /2/
+  ]
+| #i #d1 #e1 #Hid1 #d2 #e2 #T2 #Hi #Hd12
+  lapply (lift_inv_lref2 … Hi) -Hi * * #Hid2 #H destruct -T2
+  [ -Hd12; lapply (lt_plus_to_lt_l … Hid2) -Hid2 #Hid2 /3/
+  | -Hid1; lapply (arith1 … Hid2) -Hid2 #Hid2
+    @(ex2_1_intro … #(i - e2))
+    [ >le_plus_minus_comm [ @lift_lref_ge @(transitive_le … Hd12) -Hd12 /2/ | -Hd12 /2/ ]
+    | -Hd12 >(plus_minus_m_m i e2) in ⊢ (? ? ? ? %) /3/
+    ]
+  ]
+| #I #W1 #W #U1 #U #d1 #e1 #_ #_ #IHW #IHU #d2 #e2 #T2 #H #Hd12
+  lapply (lift_inv_bind2 … H) -H * #W2 #U2 #HW2 #HU2 #H destruct -T2;
+  elim (IHW … HW2 ?) // -IHW HW2 #W0 #HW2 #HW1
+  >plus_plus_comm_23 in HU2 #HU2 elim (IHU … HU2 ?) /3 width = 5/
+| #I #W1 #W #U1 #U #d1 #e1 #_ #_ #IHW #IHU #d2 #e2 #T2 #H #Hd12
+  lapply (lift_inv_flat2 … H) -H * #W2 #U2 #HW2 #HU2 #H destruct -T2;
+  elim (IHW … HW2 ?) // -IHW HW2 #W0 #HW2 #HW1
+  elim (IHU … HU2 ?) /3 width = 5/
+]
+qed.
+
+theorem lift_free: ∀d1,e2,T1,T2. ↑[d1, e2] T1 ≡ T2 → ∀d2,e1.
+                                 d1 ≤ d2 → d2 ≤ d1 + e1 → e1 ≤ e2 →
+                                 ∃∃T. ↑[d1, e1] T1 ≡ T & ↑[d2, e2 - e1] T ≡ T2.
+#d1 #e2 #T1 #T2 #H elim H -H d1 e2 T1 T2
+[ /3/
+| #i #d1 #e2 #Hid1 #d2 #e1 #Hd12 #_ #_
+  lapply (lt_to_le_to_lt … Hid1 Hd12) -Hd12 #Hid2 /4/
+| #i #d1 #e2 #Hid1 #d2 #e1 #_ #Hd21 #He12
+  lapply (transitive_le …(i+e1) Hd21 ?) /2/ -Hd21 #Hd21
+  <(plus_plus_minus_m_m e1 e2 i) /3/
+| #I #V1 #V2 #T1 #T2 #d1 #e2 #_ #_ #IHV #IHT #d2 #e1 #Hd12 #Hd21 #He12
+  elim (IHV … Hd12 Hd21 He12) -IHV #V0 #HV0a #HV0b
+  elim (IHT (d2+1) … ? ? He12) /3 width = 5/
+| #I #V1 #V2 #T1 #T2 #d1 #e2 #_ #_ #IHV #IHT #d2 #e1 #Hd12 #Hd21 #He12
+  elim (IHV … Hd12 Hd21 He12) -IHV #V0 #HV0a #HV0b
+  elim (IHT d2 … ? ? He12) /3 width = 5/
+]
+qed.
+
+theorem lift_trans: ∀d1,e1,T1,T. ↑[d1, e1] T1 ≡ T →
+                    ∀d2,e2,T2. ↑[d2, e2] T ≡ T2 →
+                    d1 ≤ d2 → d2 ≤ d1 + e1 → ↑[d1, e1 + e2] T1 ≡ T2.
+#d1 #e1 #T1 #T #H elim H -d1 e1 T1 T
+[ #k #d1 #e1 #d2 #e2 #T2 #HT2 #_ #_
+  >(lift_inv_sort1 … HT2) -HT2 //
+| #i #d1 #e1 #Hid1 #d2 #e2 #T2 #HT2 #Hd12 #_
+  lapply (lift_inv_lref1 … HT2) -HT2 * * #Hid2 #H destruct -T2
+  [ -Hd12 Hid2 /2/
+  | lapply (le_to_lt_to_lt … d1 Hid2 ?) // -Hid1 Hid2 #Hd21
+    lapply (le_to_lt_to_lt … d1 Hd12 ?) // -Hd12 Hd21 #Hd11
+    elim (lt_false … Hd11)
+  ]
+| #i #d1 #e1 #Hid1 #d2 #e2 #T2 #HT2 #_ #Hd21
+  lapply (lift_inv_lref1 … HT2) -HT2 * * #Hid2 #H destruct -T2
+  [ lapply (lt_to_le_to_lt … (d1+e1) Hid2 ?) // -Hid2 Hd21 #H
+    lapply (lt_plus_to_lt_l … H) -H #H
+    lapply (le_to_lt_to_lt … d1 Hid1 ?) // -Hid1 H #Hd11
+    elim (lt_false … Hd11)
+  | -Hd21 Hid2 /2/
+  ]
+| #I #V1 #V2 #T1 #T2 #d1 #e1 #_ #_ #IHV12 #IHT12 #d2 #e2 #X #HX #Hd12 #Hd21
+  lapply (lift_inv_bind1 … HX) -HX * #V0 #T0 #HV20 #HT20 #HX destruct -X;
+  lapply (IHV12 … HV20 ? ?) // -IHV12 HV20 #HV10
+  lapply (IHT12 … HT20 ? ?) /2/
+| #I #V1 #V2 #T1 #T2 #d1 #e1 #_ #_ #IHV12 #IHT12 #d2 #e2 #X #HX #Hd12 #Hd21
+  lapply (lift_inv_flat1 … HX) -HX * #V0 #T0 #HV20 #HT20 #HX destruct -X;
+  lapply (IHV12 … HV20 ? ?) // -IHV12 HV20 #HV10
+  lapply (IHT12 … HT20 ? ?) /2/
+]
+qed.
+
+axiom lift_trans_le: ∀d1,e1,T1,T. ↑[d1, e1] T1 ≡ T →
+                     ∀d2,e2,T2. ↑[d2, e2] T ≡ T2 → d2 ≤ d1 →
+                     ∃∃T0. ↑[d2, e2] T1 ≡ T0 & ↑[d1 + e2, e1] T0 ≡ T2.
+
+axiom lift_trans_ge: ∀d1,e1,T1,T. ↑[d1, e1] T1 ≡ T →
+                     ∀d2,e2,T2. ↑[d2, e2] T ≡ T2 → d1 + e1 ≤ d2 →
+                     ∃∃T0. ↑[d2 - e1, e2] T1 ≡ T0 & ↑[d1, e1] T0 ≡ T2.

diff --git a/matita/matita/lib/lambda-delta/substitution/subst.ma b/matita/matita/lib/lambda-delta/substitution/subst.ma
deleted file mode 100644 (file)
index 18eb6c5..0000000
--- a/matita/matita/lib/lambda-delta/substitution/subst.ma
+++ /dev/null
@@ -1,39 +0,0 @@
-(*
-    ||M||  This file is part of HELM, an Hypertextual, Electronic
-    ||A||  Library of Mathematics, developed at the Computer Science
-    ||T||  Department of the University of Bologna, Italy.
-    ||I||
-    ||T||
-    ||A||  This file is distributed under the terms of the
-    \   /  GNU General Public License Version 2
-     \ /
-      V_______________________________________________________________ *)
-
-include "lambda-delta/syntax/lenv.ma".
-include "lambda-delta/substitution/lift.ma".
-
-(* TELESCOPIC SUBSTITUTION **************************************************)
-
-inductive subst: lenv → term → nat → nat → term → Prop ≝
-| subst_sort   : ∀L,k,d,e. subst L (⋆k) d e (⋆k)
-| subst_lref_lt: ∀L,i,d,e. i < d → subst L (#i) d e (#i)
-| subst_lref_O : ∀L,V1,V2,e. subst L V1 0 e V2 →
-                 subst (L. 𝕓{Abbr} V1) #0 0 (e + 1) V2
-| subst_lref_S : ∀L,I,V,i,T1,T2,d,e.
-                 d ≤ i → i < d + e → subst L #i d e T1 → ↑[d,1] T1 ≡ T2 →
-                 subst (L. 𝕓{I} V) #(i + 1) (d + 1) e T2
-| subst_lref_ge: ∀L,i,d,e. d + e ≤ i → subst L (#i) d e (#(i - e))
-| subst_bind   : ∀L,I,V1,V2,T1,T2,d,e.
-                 subst L V1 d e V2 → subst (L. 𝕓{I} V1) T1 (d + 1) e T2 →
-                 subst L (𝕓{I} V1. T1) d e (𝕓{I} V2. T2)
-| subst_flat   : ∀L,I,V1,V2,T1,T2,d,e.
-                 subst L V1 d e V2 → subst L T1 d e T2 →
-                 subst L (𝕗{I} V1. T1) d e (𝕗{I} V2. T2)
-.
-
-interpretation "telescopic substritution" 'RSubst L T1 d e T2 = (subst L T1 d e T2).
-
-lemma subst_lift_inv: ∀d,e,T1,T2. ↑[d,e] T1 ≡ T2 → ∀L. L ⊢ ↓[d,e] T2 ≡ T1.
-#d #e #T1 #T2 #H elim H -H d e T1 T2 /2/
-#i #d #e #Hdi #L >(minus_plus_m_m i e) in ⊢ (? ? ? ? ? %) /3/ (**) (* use \ldots *)
-qed.

diff --git a/matita/matita/lib/lambda-delta/substitution/subst_defs.ma b/matita/matita/lib/lambda-delta/substitution/subst_defs.ma
new file mode 100644 (file)
index 0000000..5ef3438
--- /dev/null
+++ b/matita/matita/lib/lambda-delta/substitution/subst_defs.ma
@@ -0,0 +1,41 @@
+(*
+    ||M||  This file is part of HELM, an Hypertextual, Electronic
+    ||A||  Library of Mathematics, developed at the Computer Science
+    ||T||  Department of the University of Bologna, Italy.
+    ||I||
+    ||T||
+    ||A||  This file is distributed under the terms of the
+    \   /  GNU General Public License Version 2
+     \ /
+      V_______________________________________________________________ *)
+
+include "lambda-delta/syntax/lenv.ma".
+include "lambda-delta/substitution/lift_defs.ma".
+
+(* TELESCOPIC SUBSTITUTION **************************************************)
+
+inductive subst: lenv → term → nat → nat → term → Prop ≝
+| subst_sort   : ∀L,k,d,e. subst L (⋆k) d e (⋆k)
+| subst_lref_lt: ∀L,i,d,e. i < d → subst L (#i) d e (#i)
+| subst_lref_O : ∀L,V1,V2,e. subst L V1 0 e V2 →
+                 subst (L. 𝕓{Abbr} V1) #0 0 (e + 1) V2
+| subst_lref_S : ∀L,I,V,i,T1,T2,d,e.
+                 d ≤ i → i < d + e → subst L #i d e T1 → ↑[d,1] T1 ≡ T2 →
+                 subst (L. 𝕓{I} V) #(i + 1) (d + 1) e T2
+| subst_lref_ge: ∀L,i,d,e. d + e ≤ i → subst L (#i) d e (#(i - e))
+| subst_bind   : ∀L,I,V1,V2,T1,T2,d,e.
+                 subst L V1 d e V2 → subst (L. 𝕓{I} V1) T1 (d + 1) e T2 →
+                 subst L (𝕓{I} V1. T1) d e (𝕓{I} V2. T2)
+| subst_flat   : ∀L,I,V1,V2,T1,T2,d,e.
+                 subst L V1 d e V2 → subst L T1 d e T2 →
+                 subst L (𝕗{I} V1. T1) d e (𝕗{I} V2. T2)
+.
+
+interpretation "telescopic substritution" 'RSubst L T1 d e T2 = (subst L T1 d e T2).
+
+(* The basic properties *****************************************************)
+
+lemma subst_lift_inv: ∀d,e,T1,T2. ↑[d,e] T1 ≡ T2 → ∀L. L ⊢ ↓[d,e] T2 ≡ T1.
+#d #e #T1 #T2 #H elim H -H d e T1 T2 /2/
+#i #d #e #Hdi #L >(minus_plus_m_m i e) in ⊢ (? ? ? ? ? %) /3/ (**) (* use \ldots *)
+qed.

diff --git a/matita/matita/lib/lambda-delta/substitution/thin.ma b/matita/matita/lib/lambda-delta/substitution/thin.ma
deleted file mode 100644 (file)
index be79574..0000000
--- a/matita/matita/lib/lambda-delta/substitution/thin.ma
+++ /dev/null
@@ -1,61 +0,0 @@
-(*
-    ||M||  This file is part of HELM, an Hypertextual, Electronic
-    ||A||  Library of Mathematics, developed at the Computer Science
-    ||T||  Department of the University of Bologna, Italy.
-    ||I||
-    ||T||
-    ||A||  This file is distributed under the terms of the
-    \   /  GNU General Public License Version 2
-     \ /
-      V_______________________________________________________________ *)
-
-include "lambda-delta/substitution/subst.ma".
-
-(* THINNING *****************************************************************)
-
-inductive thin: lenv → nat → nat → lenv → Prop ≝
-| thin_refl: ∀L. thin L 0 0 L
-| thin_thin: ∀L1,L2,I,V,e. thin L1 0 e L2 → thin (L1. 𝕓{I} V) 0 (e + 1) L2
-| thin_skip: ∀L1,L2,I,V1,V2,d,e.
-             thin L1 d e L2 → L1 ⊢ ↓[d,e] V1 ≡ V2 →
-             thin (L1. 𝕓{I} V1) (d + 1) e (L2. 𝕓{I} V2)
-.
-
-interpretation "thinning" 'RSubst L1 d e L2 = (thin L1 d e L2).
-
-(* the basic inversion lemmas ***********************************************)
-
-lemma thin_inv_skip2_aux: ∀d,e,L1,L2. ↓[d, e] L1 ≡ L2 → 0 < d →
-                          ∀I,K2,V2. L2 = K2. 𝕓{I} V2 →
-                          ∃∃K1,V1. ↓[d - 1, e] K1 ≡ K2 &
-                                   K1 ⊢ ↓[d - 1, e] V1 ≡ V2 & 
-                                   L1 = K1. 𝕓{I} V1.
-#d #e #L1 #L2 #H elim H -H d e L1 L2
-[ #L #H elim (lt_false … H)
-| #L1 #L2 #I #V #e #_ #_ #H elim (lt_false … H)
-| #L1 #X #Y #V1 #Z #d #e #HL12 #HV12 #_ #_ #I #L2 #V2 #H destruct -X Y Z;
-  /2 width=5/
-]
-qed.
-
-lemma thin_inv_skip2: ∀d,e,I,L1,K2,V2. ↓[d, e] L1 ≡ K2. 𝕓{I} V2 → 0 < d →
-                      ∃∃K1,V1. ↓[d - 1, e] K1 ≡ K2 & K1 ⊢ ↓[d - 1, e] V1 ≡ V2 &
-                               L1 = K1. 𝕓{I} V1.
-/2/ qed.
-
-(* the main properties ******************************************************)
-
-axiom thin_conf_ge: ∀d1,e1,L,L1. ↓[d1,e1] L ≡ L1 →
-                    ∀e2,L2. ↓[0,e2] L ≡ L2 → d1 + e1 ≤ e2 → ↓[0,e2-e1] L1 ≡ L2.
-
-axiom thin_conf_lt: ∀d1,e1,L,L1. ↓[d1,e1] L ≡ L1 →
-                    ∀e2,K2,I,V2. ↓[0,e2] L ≡ K2. 𝕓{I} V2 →
-                    e2 < d1 → let d ≝ d1 - e2 - 1 in
-                    ∃∃K1,V1. ↓[0,e2] L1 ≡ K1. 𝕓{I} V1 & ↓[d,e1] K2 ≡ K1 & ↑[d,e1] V1 ≡ V2.
-
-axiom thin_trans_le: ∀d1,e1,L1,L. ↓[d1, e1] L1 ≡ L →
-                     ∀e2,L2. ↓[0, e2] L ≡ L2 → e2 ≤ d1 →
-                     ∃∃L0. ↓[0, e2] L1 ≡ L0 & ↓[d1 - e2, e1] L0 ≡ L2.
-
-axiom thin_trans_ge: ∀d1,e1,L1,L. ↓[d1, e1] L1 ≡ L →
-                     ∀e2,L2. ↓[0, e2] L ≡ L2 → d1 ≤ e2 → ↓[0, e1 + e2] L1 ≡ L2.

diff --git a/matita/matita/lib/lambda-delta/substitution/thin_defs.ma b/matita/matita/lib/lambda-delta/substitution/thin_defs.ma
new file mode 100644 (file)
index 0000000..1e78476
--- /dev/null
+++ b/matita/matita/lib/lambda-delta/substitution/thin_defs.ma
@@ -0,0 +1,44 @@
+(*
+    ||M||  This file is part of HELM, an Hypertextual, Electronic
+    ||A||  Library of Mathematics, developed at the Computer Science
+    ||T||  Department of the University of Bologna, Italy.
+    ||I||
+    ||T||
+    ||A||  This file is distributed under the terms of the
+    \   /  GNU General Public License Version 2
+     \ /
+      V_______________________________________________________________ *)
+
+include "lambda-delta/substitution/subst_defs.ma".
+
+(* THINNING *****************************************************************)
+
+inductive thin: lenv → nat → nat → lenv → Prop ≝
+| thin_refl: ∀L. thin L 0 0 L
+| thin_thin: ∀L1,L2,I,V,e. thin L1 0 e L2 → thin (L1. 𝕓{I} V) 0 (e + 1) L2
+| thin_skip: ∀L1,L2,I,V1,V2,d,e.
+             thin L1 d e L2 → L1 ⊢ ↓[d,e] V1 ≡ V2 →
+             thin (L1. 𝕓{I} V1) (d + 1) e (L2. 𝕓{I} V2)
+.
+
+interpretation "thinning" 'RSubst L1 d e L2 = (thin L1 d e L2).
+
+(* the basic inversion lemmas ***********************************************)
+
+lemma thin_inv_skip2_aux: ∀d,e,L1,L2. ↓[d, e] L1 ≡ L2 → 0 < d →
+                          ∀I,K2,V2. L2 = K2. 𝕓{I} V2 →
+                          ∃∃K1,V1. ↓[d - 1, e] K1 ≡ K2 &
+                                   K1 ⊢ ↓[d - 1, e] V1 ≡ V2 & 
+                                   L1 = K1. 𝕓{I} V1.
+#d #e #L1 #L2 #H elim H -H d e L1 L2
+[ #L #H elim (lt_false … H)
+| #L1 #L2 #I #V #e #_ #_ #H elim (lt_false … H)
+| #L1 #X #Y #V1 #Z #d #e #HL12 #HV12 #_ #_ #I #L2 #V2 #H destruct -X Y Z;
+  /2 width=5/
+]
+qed.
+
+lemma thin_inv_skip2: ∀d,e,I,L1,K2,V2. ↓[d, e] L1 ≡ K2. 𝕓{I} V2 → 0 < d →
+                      ∃∃K1,V1. ↓[d - 1, e] K1 ≡ K2 & K1 ⊢ ↓[d - 1, e] V1 ≡ V2 &
+                               L1 = K1. 𝕓{I} V1.
+/2/ qed.

diff --git a/matita/matita/lib/lambda-delta/substitution/thin_main.ma b/matita/matita/lib/lambda-delta/substitution/thin_main.ma
new file mode 100644 (file)
index 0000000..f16fb3a
--- /dev/null
+++ b/matita/matita/lib/lambda-delta/substitution/thin_main.ma
@@ -0,0 +1,34 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "lambda-delta/substitution/thin_defs.ma".
+
+(* THINNING *****************************************************************)
+
+(* the main properties ******************************************************)
+
+axiom thin_conf_ge: ∀d1,e1,L,L1. ↓[d1,e1] L ≡ L1 →
+                    ∀e2,L2. ↓[0,e2] L ≡ L2 → d1 + e1 ≤ e2 → ↓[0,e2-e1] L1 ≡ L2.
+
+axiom thin_conf_lt: ∀d1,e1,L,L1. ↓[d1,e1] L ≡ L1 →
+                    ∀e2,K2,I,V2. ↓[0,e2] L ≡ K2. 𝕓{I} V2 →
+                    e2 < d1 → let d ≝ d1 - e2 - 1 in
+                    ∃∃K1,V1. ↓[0,e2] L1 ≡ K1. 𝕓{I} V1 & ↓[d,e1] K2 ≡ K1 & ↑[d,e1] V1 ≡ V2.
+
+axiom thin_trans_le: ∀d1,e1,L1,L. ↓[d1, e1] L1 ≡ L →
+                     ∀e2,L2. ↓[0, e2] L ≡ L2 → e2 ≤ d1 →
+                     ∃∃L0. ↓[0, e2] L1 ≡ L0 & ↓[d1 - e2, e1] L0 ≡ L2.
+
+axiom thin_trans_ge: ∀d1,e1,L1,L. ↓[d1, e1] L1 ≡ L →
+                     ∀e2,L2. ↓[0, e2] L ≡ L2 → d1 ≤ e2 → ↓[0, e1 + e2] L1 ≡ L2.