From 8f694a82e3291e4a3c2a4f805782846204cf348c Mon Sep 17 00:00:00 2001
From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Mon, 5 Sep 2011 13:55:42 +0000
Subject: [PATCH] - the substitution lemma is proved! - slight modification of
 parallel substitution and some renaming

---
 .../lambda-delta/Basic-2/reduction/cpr.ma     |  3 +-
 .../Basic-2/substitution/ltps_tps.ma          | 70 +++++++++++++++++++
 .../lambda-delta/Basic-2/substitution/tps.ma  | 17 +++--
 .../Basic-2/substitution/tps_lift.ma          |  7 +-
 .../Basic-2/substitution/tps_tps.ma           | 24 +++----
 5 files changed, 92 insertions(+), 29 deletions(-)
 create mode 100644 matita/matita/contribs/lambda-delta/Basic-2/substitution/ltps_tps.ma

diff --git a/matita/matita/contribs/lambda-delta/Basic-2/reduction/cpr.ma b/matita/matita/contribs/lambda-delta/Basic-2/reduction/cpr.ma
index fb79bdebc..e8a586d3d 100644
--- a/matita/matita/contribs/lambda-delta/Basic-2/reduction/cpr.ma
+++ b/matita/matita/contribs/lambda-delta/Basic-2/reduction/cpr.ma
@@ -44,7 +44,8 @@ lemma cpr_bind_dx: ∀I,L,V1,V2,T1,T2. V1 ⇒ V2 → L. 𝕓{I} V2 ⊢ T1 ⇒ T2
                    L ⊢ 𝕓{I} V1. T1 ⇒ 𝕓{I} V2. T2.
 #I #L #V1 #V2 #T1 #T2 #HV12 * #T #HT1 normalize #HT2
 elim (tps_split_up … HT2 1 ? ?) -HT2 // #T0 <minus_n_O #HT0 normalize <minus_plus_m_m #HT02
-lapply (tps_leq_repl … HT0 (⋆. 𝕓{I} V2) ?) -HT0 /2/ #HT0 /3 width=5/
+lapply (tps_leq_repl_dx … HT0 (⋆. 𝕓{I} V2) ?) -HT0 /2/ #HT0
+/3 width=5/
 qed.
 
 (* NOTE: new property *)
diff --git a/matita/matita/contribs/lambda-delta/Basic-2/substitution/ltps_tps.ma b/matita/matita/contribs/lambda-delta/Basic-2/substitution/ltps_tps.ma
new file mode 100644
index 000000000..b5f524cfc
--- /dev/null
+++ b/matita/matita/contribs/lambda-delta/Basic-2/substitution/ltps_tps.ma
@@ -0,0 +1,70 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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 "Basic-2/substitution/tps_lift.ma".
+include "Basic-2/substitution/ltps_drop.ma".
+
+(* PARALLEL SUBSTITUTION ON LOCAL ENVIRONMENTS ******************************)
+
+lemma ltps_tps_conf_ge: ∀L0,T2,U2,d2,e2. L0 ⊢ T2 [d2, e2] ≫ U2 →
+                        ∀L1,d1,e1. L0 [d1, e1] ≫ L1 → d1 + e1 ≤ d2 →
+                        L1 ⊢ T2 [d2, e2] ≫ U2.
+#L0 #T2 #U2 #d2 #e2 #H elim H -H L0 T2 U2 d2 e2
+[ //
+| #L0 #K0 #V0 #W0 #i2 #d2 #e2 #Hdi2 #Hide2 #HLK0 #HVW0 #L1 #d1 #e1 #HL01 #Hde1d2
+  lapply (transitive_le … Hde1d2 Hdi2) -Hde1d2 #Hde1i2
+  lapply (ltps_drop_conf_ge … HL01 … HLK0 ?) -HL01 HLK0 /2/
+| #L0 #I #V2 #W2 #T2 #U2 #d2 #e2 #_ #_ #IHVW2 #IHTU2 #L1 #d1 #e1 #HL01 #Hde1d2
+  @tps_bind [ /2/ | @IHTU2 [3: /2/ |1,2: skip | /2/ ] ] (**) (* /3/ is too slow *)
+| /3/
+]
+qed.
+
+lemma ltps_tps_conf: ∀L0,T2,U2,d2,e2. L0 ⊢ T2 [d2, e2] ≫ U2 →
+                     ∀L1,d1,e1. L0 [d1, e1] ≫ L1 →
+                     ∃∃T. L1 ⊢ T2 [d2, e2] ≫ T &
+                          L1 ⊢ U2 [d1, e1] ≫ T.
+#L0 #T2 #U2 #d2 #e2 #H elim H -H L0 T2 U2 d2 e2
+[ /2/
+| #L0 #K0 #V0 #W0 #i2 #d2 #e2 #Hdi2 #Hide2 #HLK0 #HVW0 #L1 #d1 #e1 #HL01
+  elim (lt_or_ge i2 d1) #Hi2d1
+  [ elim (ltps_drop_conf_le … HL01 … HLK0 ?) -HL01 HLK0 /2/ #X #H #HLK1
+    elim (ltps_inv_tps11 … H ?) -H [2: /2/ ] #K1 #V1 #_ #HV01 #H destruct -X;
+    lapply (drop_fwd_drop2 … HLK1) #H
+    elim (lift_total V1 0 (i2 + 1)) #W1 #HVW1
+    lapply (tps_lift_ge … HV01 … H HVW0 HVW1 ?) -H HV01 HVW0 // >arith_a2 /3/
+  | elim (lt_or_ge i2 (d1 + e1)) #Hde1i2
+    [ elim (ltps_drop_conf_be … HL01 … HLK0 ? ?) -HL01 HLK0 [2,3: /2/ ] #X #H #HLK1
+      elim (ltps_inv_tps21 … H ?) -H [2: /2/ ] #K1 #V1 #_ #HV01 #H destruct -X;
+      lapply (drop_fwd_drop2 … HLK1) #H
+      elim (lift_total V1 0 (i2 + 1)) #W1 #HVW1
+      lapply (tps_lift_ge … HV01 … H HVW0 HVW1 ?) -H HV01 HVW0 // normalize #HW01
+      lapply (tps_weak … HW01 d1 e1 ? ?) [2,3: /3/ ] >arith_i2 //
+    | lapply (ltps_drop_conf_ge … HL01 … HLK0 ?) -HL01 HLK0 /3/
+    ]
+  ]
+| #L0 #I #V2 #W2 #T2 #U2 #d2 #e2 #_ #_ #IHVW2 #IHTU2 #L1 #d1 #e1 #HL01
+  elim (IHVW2 … HL01) -IHVW2 #V #HV2 #HVW2
+  elim (IHTU2 (L1. 𝕓{I} V) (d1 + 1) e1 ?) -IHTU2 [2: /2/ ] -HL01 /3 width=5/
+| #L0 #I #V2 #W2 #T2 #U2 #d2 #e2 #_ #_ #IHVW2 #IHTU2 #L1 #d1 #e1 #HL01
+  elim (IHVW2 … HL01) -IHVW2;
+  elim (IHTU2 … HL01) -IHTU2 HL01 /3 width=5/
+]
+qed.
+(*  
+lemma ltps_tps_trans: (t1,t2,u2:?; j:?) (subst0 j u2 t1 t2) ->
+                      (u1,u:?; i:?) (subst0 i u u1 u2) ->
+                      (EX t | (subst0 j u1 t1 t) & (subst0 (S (plus i j)) u t t2)).
+
+*)
\ No newline at end of file
diff --git a/matita/matita/contribs/lambda-delta/Basic-2/substitution/tps.ma b/matita/matita/contribs/lambda-delta/Basic-2/substitution/tps.ma
index 7f43bd332..0acbc3d4f 100644
--- a/matita/matita/contribs/lambda-delta/Basic-2/substitution/tps.ma
+++ b/matita/matita/contribs/lambda-delta/Basic-2/substitution/tps.ma
@@ -21,7 +21,7 @@ inductive tps: lenv → term → nat → nat → term → Prop ≝
 | tps_subst: ∀L,K,V,W,i,d,e. d ≤ i → i < d + e →
              ↓[0, i] L ≡ K. 𝕓{Abbr} V → ↑[0, i + 1] V ≡ W → tps L (#i) d e W
 | tps_bind : ∀L,I,V1,V2,T1,T2,d,e.
-             tps L V1 d e V2 → tps (L. 𝕓{I} V1) T1 (d + 1) e T2 →
+             tps L V1 d e V2 → tps (L. 𝕓{I} V2) T1 (d + 1) e T2 →
              tps L (𝕓{I} V1. T1) d e (𝕓{I} V2. T2)
 | tps_flat : ∀L,I,V1,V2,T1,T2,d,e.
              tps L V1 d e V2 → tps L T1 d e T2 →
@@ -33,8 +33,8 @@ interpretation "parallel substritution (term)"
 
 (* Basic properties *********************************************************)
 
-lemma tps_leq_repl: ∀L1,T1,T2,d,e. L1 ⊢ T1 [d, e] ≫ T2 →
-                    ∀L2. L1 [d, e] ≈ L2 → L2 ⊢ T1 [d, e] ≫ T2.
+lemma tps_leq_repl_dx: ∀L1,T1,T2,d,e. L1 ⊢ T1 [d, e] ≫ T2 →
+                       ∀L2. L1 [d, e] ≈ L2 → L2 ⊢ T1 [d, e] ≫ T2.
 #L1 #T1 #T2 #d #e #H elim H -H L1 T1 T2 d e
 [ //
 | #L1 #K1 #V #W #i #d #e #Hdi #Hide #HLK1 #HVW #L2 #HL12
@@ -98,8 +98,7 @@ lemma tps_split_up: ∀L,T1,T2,d,e. L ⊢ T1 [d, e] ≫ T2 → ∀i. d ≤ i →
   elim (IHV12 i ? ?) -IHV12 // #V #HV1 #HV2
   elim (IHT12 (i + 1) ? ?) -IHT12 [2: /2 by arith4/ |3: /2/ ] (* just /2/ is too slow *)
   -Hdi Hide >arith_c1 >arith_c1x #T #HT1 #HT2
-  @ex2_1_intro [2,3: @tps_bind | skip ] (**) (* explicit constructors *)
-  [3: @HV1 |4: @HT1 |5: // |1,2: skip | /3 width=5/ ]
+  lapply (tps_leq_repl_dx … HT1 (L. 𝕓{I} V) ?) -HT1 /3 width=5/
 | #L #I #V1 #V2 #T1 #T2 #d #e #_ #_ #IHV12 #IHT12 #i #Hdi #Hide
   elim (IHV12 i ? ?) -IHV12 // elim (IHT12 i ? ?) -IHT12 //
   -Hdi Hide /3 width=5/
@@ -152,7 +151,7 @@ qed.
 fact tps_inv_bind1_aux: ∀d,e,L,U1,U2. L ⊢ U1 [d, e] ≫ U2 →
                         ∀I,V1,T1. U1 = 𝕓{I} V1. T1 →
                         ∃∃V2,T2. L ⊢ V1 [d, e] ≫ V2 & 
-                                 L. 𝕓{I} V1 ⊢ T1 [d + 1, e] ≫ T2 &
+                                 L. 𝕓{I} V2 ⊢ T1 [d + 1, e] ≫ T2 &
                                  U2 =  𝕓{I} V2. T2.
 #d #e #L #U1 #U2 * -d e L U1 U2
 [ #L #k #d #e #I #V1 #T1 #H destruct
@@ -164,7 +163,7 @@ qed.
 
 lemma tps_inv_bind1: ∀d,e,L,I,V1,T1,U2. L ⊢ 𝕓{I} V1. T1 [d, e] ≫ U2 →
                      ∃∃V2,T2. L ⊢ V1 [d, e] ≫ V2 & 
-                              L. 𝕓{I} V1 ⊢ T1 [d + 1, e] ≫ T2 &
+                              L. 𝕓{I} V2 ⊢ T1 [d + 1, e] ≫ T2 &
                               U2 =  𝕓{I} V2. T2.
 /2/ qed.
 
@@ -202,9 +201,9 @@ lemma tps_inv_refl_O2: ∀L,T1,T2,d. L ⊢ T1 [d, 0] ≫ T2 → T1 = T2.
 (* Basic-1: removed theorems 23:
             subst0_gen_sort subst0_gen_lref subst0_gen_head subst0_gen_lift_lt
             subst0_gen_lift_false subst0_gen_lift_ge subst0_refl subst0_trans
-	    subst0_lift_lt subst0_lift_ge subst0_lift_ge_S subst0_lift_ge_s
+	          subst0_lift_lt subst0_lift_ge subst0_lift_ge_S subst0_lift_ge_s
             subst0_subst0 subst0_subst0_back subst0_weight_le subst0_weight_lt
-	    subst0_confluence_neq subst0_confluence_eq subst0_tlt_head
+	          subst0_confluence_neq subst0_confluence_eq subst0_tlt_head
             subst0_confluence_lift subst0_tlt
             subst1_head subst1_gen_head  
 *)
diff --git a/matita/matita/contribs/lambda-delta/Basic-2/substitution/tps_lift.ma b/matita/matita/contribs/lambda-delta/Basic-2/substitution/tps_lift.ma
index e3b6ee39e..80ed80f1c 100644
--- a/matita/matita/contribs/lambda-delta/Basic-2/substitution/tps_lift.ma
+++ b/matita/matita/contribs/lambda-delta/Basic-2/substitution/tps_lift.ma
@@ -85,8 +85,9 @@ lemma tps_inv_lift1_le: ∀L,U1,U2,dt,et. L ⊢ U1 [dt, et] ≫ U2 →
   elim (lift_trans_le … HUV … HVW ?) -HUV HVW V // >arith_a2 // -Hid /3/
 | #L #I #V1 #V2 #U1 #U2 #dt #et #_ #_ #IHV12 #IHU12 #K #d #e #HLK #X #H #Hdetd
   elim (lift_inv_bind2 … H) -H #W1 #T1 #HWV1 #HTU1 #H destruct -X;
-  elim (IHV12 … HLK … HWV1 ?) -IHV12 //
-  elim (IHU12 … HTU1 ?) -IHU12 HTU1 [3: /2/ |4: @drop_skip // |2: skip ] -HLK HWV1 Hdetd /3 width=5/ (**) (* just /3 width=5/ is too slow *)
+  elim (IHV12 … HLK … HWV1 ?) -IHV12 HWV1 // #W2 #HW12 #HWV2
+  elim (IHU12 … HTU1 ?) -IHU12 HTU1 [3: /2/ |4: @drop_skip // |2: skip ] -HLK Hdetd (**) (* /3 width=5/ is too slow *)
+  /3 width=5/
 | #L #I #V1 #V2 #U1 #U2 #dt #et #_ #_ #IHV12 #IHU12 #K #d #e #HLK #X #H #Hdetd
   elim (lift_inv_flat2 … H) -H #W1 #T1 #HWV1 #HTU1 #H destruct -X;
   elim (IHV12 … HLK … HWV1 ?) -IHV12 HWV1 //
@@ -118,7 +119,7 @@ lemma tps_inv_lift1_ge: ∀L,U1,U2,dt,et. L ⊢ U1 [dt, et] ≫ U2 →
 | #L #I #V1 #V2 #U1 #U2 #dt #et #_ #_ #IHV12 #IHU12 #K #d #e #HLK #X #H #Hdetd
   elim (lift_inv_bind2 … H) -H #W1 #T1 #HWV1 #HTU1 #H destruct -X;
   lapply (plus_le_weak … Hdetd) #Hedt
-  elim (IHV12 … HLK … HWV1 ?) -IHV12 // #W2 #HW12 #HWV2
+  elim (IHV12 … HLK … HWV1 ?) -IHV12 HWV1 // #W2 #HW12 #HWV2
   elim (IHU12 … HTU1 ?) -IHU12 HTU1 [4: @drop_skip // |2: skip |3: /2/ ]
   <plus_minus // /3 width=5/
 | #L #I #V1 #V2 #U1 #U2 #dt #et #_ #_ #IHV12 #IHU12 #K #d #e #HLK #X #H #Hdetd
diff --git a/matita/matita/contribs/lambda-delta/Basic-2/substitution/tps_tps.ma b/matita/matita/contribs/lambda-delta/Basic-2/substitution/tps_tps.ma
index a969da023..3daf6fbe2 100644
--- a/matita/matita/contribs/lambda-delta/Basic-2/substitution/tps_tps.ma
+++ b/matita/matita/contribs/lambda-delta/Basic-2/substitution/tps_tps.ma
@@ -33,10 +33,11 @@ theorem tps_conf_eq: ∀L,T0,T1,d1,e1. L ⊢ T0 [d1, e1] ≫ T1 →
   ]
 | #L #I #V0 #V1 #T0 #T1 #d1 #e1 #_ #_ #IHV01 #IHT01 #X #d2 #e2 #HX
   elim (tps_inv_bind1 … HX) -HX #V2 #T2 #HV02 #HT02 #HX destruct -X;
+  lapply (tps_leq_repl_dx … HT02 (L. 𝕓{I} V1) ?) -HT02 /2/ #HT02  
   elim (IHV01 … HV02) -IHV01 HV02 #V #HV1 #HV2
   elim (IHT01 … HT02) -IHT01 HT02 #T #HT1 #HT2
-  lapply (tps_leq_repl … HT1 (L. 𝕓{I} V1) ?) -HT1 /2/
-  lapply (tps_leq_repl … HT2 (L. 𝕓{I} V2) ?) -HT2 /3 width=5/
+  lapply (tps_leq_repl_dx … HT1 (L. 𝕓{I} V) ?) -HT1 /2/
+  lapply (tps_leq_repl_dx … HT2 (L. 𝕓{I} V) ?) -HT2 /3 width=5/
 | #L #I #V0 #V1 #T0 #T1 #d1 #e1 #_ #_ #IHV01 #IHT01 #X #d2 #e2 #HX
   elim (tps_inv_flat1 … HX) -HX #V2 #T2 #HV02 #HT02 #HX destruct -X;
   elim (IHV01 … HV02) -IHV01 HV02;
@@ -70,8 +71,8 @@ theorem tps_conf_neq: ∀L1,T0,T1,d1,e1. L1 ⊢ T0 [d1, e1] ≫ T1 →
   elim (IHV01 … HV02 H) -IHV01 HV02 #V #HV1 #HV2
   elim (IHT01 … HT02 ?) -IHT01 HT02
   [ -H #T #HT1 #HT2
-    lapply (tps_leq_repl … HT1 (L2. 𝕓{I} V1) ?) -HT1 /2/
-    lapply (tps_leq_repl … HT2 (L1. 𝕓{I} V2) ?) -HT2 /3 width=5/
+    lapply (tps_leq_repl_dx … HT1 (L2. 𝕓{I} V) ?) -HT1 /2/
+    lapply (tps_leq_repl_dx … HT2 (L1. 𝕓{I} V) ?) -HT2 /3 width=5/
   | -HV1 HV2 >plus_plus_comm_23 >plus_plus_comm_23 in ⊢ (? ? %) elim H -H #H
     [ @or_introl | @or_intror ] /2 by monotonic_le_plus_l/ (**) (* /3/ is too slow *)
   ]
@@ -93,23 +94,14 @@ theorem tps_trans_down: ∀L,T1,T0,d1,e1. L ⊢ T1 [d1, e1] ≫ T0 →
   <(tps_inv_lift1_eq … HWT2 … HVW) -HWT2 /4/
 | #L #I #V1 #V0 #T1 #T0 #d1 #e1 #_ #_ #IHV10 #IHT10 #X #d2 #e2 #HX #de2d1
   elim (tps_inv_bind1 … HX) -HX #V2 #T2 #HV02 #HT02 #HX destruct -X;
-  lapply (tps_leq_repl … HT02 (L. 𝕓{I} V1) ?) -HT02 /2/ #HT02
+  lapply (tps_leq_repl_dx … HT02 (L. 𝕓{I} V0) ?) -HT02 /2/ #HT02
   elim (IHV10 … HV02 ?) -IHV10 HV02 // #V
   elim (IHT10 … HT02 ?) -IHT10 HT02 [2: /2/ ] #T #HT1 #HT2
-  lapply (tps_leq_repl … HT2 (L. 𝕓{I} V) ?) -HT2 /3 width=6/
+  lapply (tps_leq_repl_dx … HT1 (L. 𝕓{I} V) ?) -HT1;
+  lapply (tps_leq_repl_dx … HT2 (L. 𝕓{I} V2) ?) -HT2 /3 width=6/
 | #L #I #V1 #V0 #T1 #T0 #d1 #e1 #_ #_ #IHV10 #IHT10 #X #d2 #e2 #HX #de2d1
   elim (tps_inv_flat1 … HX) -HX #V2 #T2 #HV02 #HT02 #HX destruct -X;
   elim (IHV10 … HV02 ?) -IHV10 HV02 //
   elim (IHT10 … HT02 ?) -IHT10 HT02 // /3 width=6/
 ]
 qed.
-(*
-      Theorem subst0_subst0: (t1,t2,u2:?; j:?) (subst0 j u2 t1 t2) ->
-                             (u1,u:?; i:?) (subst0 i u u1 u2) ->
-                             (EX t | (subst0 j u1 t1 t) & (subst0 (S (plus i j)) u t t2)).
-
-      Theorem subst0_subst0_back: (t1,t2,u2:?; j:?) (subst0 j u2 t1 t2) ->
-                                  (u1,u:?; i:?) (subst0 i u u2 u1) ->
-                                  (EX t | (subst0 j u1 t1 t) & (subst0 (S (plus i j)) u t2 t)).
-
-*)
-- 
2.39.2