cpr_cast closed! (after a bugfix in the "destruct" tactic)

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 0e123f64cf733bf31a0d5ba545070051245363f0..9187765da85eaf478808ed40586cc0149b4edb68 100644 (file)
--- a/matita/matita/contribs/lambda-delta/Basic-2/reduction/cpr.ma
+++ b/matita/matita/contribs/lambda-delta/Basic-2/reduction/cpr.ma
@@ -64,7 +64,7 @@ lemma cpr_inv_sort1: ∀L,T2,k. L ⊢ ⋆k ⇒ T2 → T2 = ⋆k.
 >(tpr_inv_atom1 … H) -H #H
 >(tpss_inv_sort1 … H) -H //
 qed.
-(*
+
 (* Basic-1: was: pr2_gen_cast *)
 lemma cpr_inv_cast1: ∀L,V1,T1,U2. L ⊢ 𝕔{Cast} V1. T1 ⇒ U2 → (
                         ∃∃V2,T2. L ⊢ V1 ⇒ V2 & L ⊢ T1 ⇒ T2 &
@@ -72,9 +72,9 @@ lemma cpr_inv_cast1: ∀L,V1,T1,U2. L ⊢ 𝕔{Cast} V1. T1 ⇒ U2 → (
                      ) ∨ L ⊢ T1 ⇒ U2.
 #L #V1 #T1 #U2 * #X #H #HU2
 elim (tpr_inv_cast1 … H) -H /3/
-* #V #T #HV1 #HT1 #H whd  (* >H in HU2; *) destruct -X;
-elim (tps_inv_flat1 … HU2) -HU2 #V2 #T2 #HV2 #HT2 #H
-*)
+* #V #T #HV1 #HT1 #H destruct -X;
+elim (tpss_inv_flat1 … HU2) -HU2 #V2 #T2 #HV2 #HT2 #H destruct -U2 /4 width=5/
+qed.
 
 (* Basic-1: removed theorems 5: 
             pr2_head_1 pr2_head_2 pr2_cflat pr2_gen_cflat clear_pr2_trans

diff --git a/matita/matita/contribs/lambda-delta/Basic-2/unfold/ltpss_drop.ma b/matita/matita/contribs/lambda-delta/Basic-2/unfold/ltpss_drop.ma
new file mode 100644 (file)
index 0000000..4b50886
--- /dev/null
+++ b/matita/matita/contribs/lambda-delta/Basic-2/unfold/ltpss_drop.ma
@@ -0,0 +1,132 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/ltps.ma".
+
+(* PARALLEL SUBSTITUTION ON LOCAL ENVIRONMENTS ******************************)
+
+lemma ltps_drop_conf_ge: ∀L0,L1,d1,e1. L0 [d1, e1] ≫ L1 →
+                         ∀L2,e2. ↓[0, e2] L0 ≡ L2 →
+                         d1 + e1 ≤ e2 → ↓[0, e2] L1 ≡ L2.
+#L0 #L1 #d1 #e1 #H elim H -H L0 L1 d1 e1
+[ #d1 #e1 #L2 #e2 #H >(drop_inv_atom1 … H) -H //
+| //
+| normalize #K0 #K1 #I #V0 #V1 #e1 #_ #_ #IHK01 #L2 #e2 #H #He12
+  lapply (plus_le_weak … He12) #He2
+  lapply (drop_inv_drop1 … H ?) -H // #HK0L2
+  lapply (IHK01 … HK0L2 ?) -IHK01 HK0L2 /2/
+| #K0 #K1 #I #V0 #V1 #d1 #e1 >plus_plus_comm_23 #_ #_ #IHK01 #L2 #e2 #H #Hd1e2
+  lapply (plus_le_weak … Hd1e2) #He2
+  lapply (drop_inv_drop1 … H ?) -H // #HK0L2
+  lapply (IHK01 … HK0L2 ?) -IHK01 HK0L2 /2/
+]
+qed.
+
+lemma ltps_drop_trans_ge: ∀L1,L0,d1,e1. L1 [d1, e1] ≫ L0 →
+                          ∀L2,e2. ↓[0, e2] L0 ≡ L2 →
+                          d1 + e1 ≤ e2 → ↓[0, e2] L1 ≡ L2.
+#L1 #L0 #d1 #e1 #H elim H -H L1 L0 d1 e1
+[ #d1 #e1 #L2 #e2 #H >(drop_inv_atom1 … H) -H //
+| //
+| normalize #K1 #K0 #I #V1 #V0 #e1 #_ #_ #IHK10 #L2 #e2 #H #He12
+  lapply (plus_le_weak … He12) #He2
+  lapply (drop_inv_drop1 … H ?) -H // #HK0L2
+  lapply (IHK10 … HK0L2 ?) -IHK10 HK0L2 /2/
+| #K0 #K1 #I #V1 #V0 #d1 #e1 >plus_plus_comm_23 #_ #_ #IHK10 #L2 #e2 #H #Hd1e2
+  lapply (plus_le_weak … Hd1e2) #He2
+  lapply (drop_inv_drop1 … H ?) -H // #HK0L2
+  lapply (IHK10 … HK0L2 ?) -IHK10 HK0L2 /2/
+]
+qed.
+
+lemma ltps_drop_conf_be: ∀L0,L1,d1,e1. L0 [d1, e1] ≫ L1 →
+                         ∀L2,e2. ↓[0, e2] L0 ≡ L2 → d1 ≤ e2 → e2 ≤ d1 + e1 →
+                         ∃∃L. L2 [0, d1 + e1 - e2] ≫ L & ↓[0, e2] L1 ≡ L.
+#L0 #L1 #d1 #e1 #H elim H -H L0 L1 d1 e1
+[ #d1 #e1 #L2 #e2 #H >(drop_inv_atom1 … H) -H /2/
+| normalize #L #I #V #L2 #e2 #HL2 #_ #He2
+  lapply (le_n_O_to_eq … He2) -He2 #H destruct -e2;
+  lapply (drop_inv_refl … HL2) -HL2 #H destruct -L2 /2/
+| normalize #K0 #K1 #I #V0 #V1 #e1 #HK01 #HV01 #IHK01 #L2 #e2 #H #_ #He21
+  lapply (drop_inv_O1 … H) -H * * #He2 #HK0L2
+  [ destruct -IHK01 He21 e2 L2 <minus_n_O /3/
+  | -HK01 HV01 <minus_le_minus_minus_comm //
+    elim (IHK01 … HK0L2 ? ?) -IHK01 HK0L2 /3/
+  ]
+| #K0 #K1 #I #V0 #V1 #d1 #e1 >plus_plus_comm_23 #_ #_ #IHK01 #L2 #e2 #H #Hd1e2 #He2de1
+  lapply (plus_le_weak … Hd1e2) #He2
+  <minus_le_minus_minus_comm //
+  lapply (drop_inv_drop1 … H ?) -H // #HK0L2
+  elim (IHK01 … HK0L2 ? ?) -IHK01 HK0L2 /3/
+]
+qed.
+
+lemma ltps_drop_trans_be: ∀L1,L0,d1,e1. L1 [d1, e1] ≫ L0 →
+                          ∀L2,e2. ↓[0, e2] L0 ≡ L2 → d1 ≤ e2 → e2 ≤ d1 + e1 →
+                          ∃∃L. L [0, d1 + e1 - e2] ≫ L2 & ↓[0, e2] L1 ≡ L.
+#L1 #L0 #d1 #e1 #H elim H -H L1 L0 d1 e1
+[ #d1 #e1 #L2 #e2 #H >(drop_inv_atom1 … H) -H /2/
+| normalize #L #I #V #L2 #e2 #HL2 #_ #He2
+  lapply (le_n_O_to_eq … He2) -He2 #H destruct -e2;
+  lapply (drop_inv_refl … HL2) -HL2 #H destruct -L2 /2/
+| normalize #K1 #K0 #I #V1 #V0 #e1 #HK10 #HV10 #IHK10 #L2 #e2 #H #_ #He21
+  lapply (drop_inv_O1 … H) -H * * #He2 #HK0L2
+  [ destruct -IHK10 He21 e2 L2 <minus_n_O /3/
+  | -HK10 HV10 <minus_le_minus_minus_comm //
+    elim (IHK10 … HK0L2 ? ?) -IHK10 HK0L2 /3/
+  ]
+| #K1 #K0 #I #V1 #V0 #d1 #e1 >plus_plus_comm_23 #_ #_ #IHK10 #L2 #e2 #H #Hd1e2 #He2de1
+  lapply (plus_le_weak … Hd1e2) #He2
+  <minus_le_minus_minus_comm //
+  lapply (drop_inv_drop1 … H ?) -H // #HK0L2
+  elim (IHK10 … HK0L2 ? ?) -IHK10 HK0L2 /3/
+]
+qed.
+
+lemma ltps_drop_conf_le: ∀L0,L1,d1,e1. L0 [d1, e1] ≫ L1 →
+                         ∀L2,e2. ↓[0, e2] L0 ≡ L2 → e2 ≤ d1 →
+                         ∃∃L. L2 [d1 - e2, e1] ≫ L & ↓[0, e2] L1 ≡ L.
+#L0 #L1 #d1 #e1 #H elim H -H L0 L1 d1 e1
+[ #d1 #e1 #L2 #e2 #H >(drop_inv_atom1 … H) -H /2/
+| /2/
+| normalize #K0 #K1 #I #V0 #V1 #e1 #HK01 #HV01 #_ #L2 #e2 #H #He2
+  lapply (le_n_O_to_eq … He2) -He2 #He2 destruct -e2;
+  lapply (drop_inv_refl … H) -H #H destruct -L2 /3/
+| #K0 #K1 #I #V0 #V1 #d1 #e1 #HK01 #HV01 #IHK01 #L2 #e2 #H #He2d1
+  lapply (drop_inv_O1 … H) -H * * #He2 #HK0L2
+  [ destruct -IHK01 He2d1 e2 L2 <minus_n_O /3/
+  | -HK01 HV01 <minus_le_minus_minus_comm //
+    elim (IHK01 … HK0L2 ?) -IHK01 HK0L2 /3/
+  ]
+]
+qed.
+
+lemma ltps_drop_trans_le: ∀L1,L0,d1,e1. L1 [d1, e1] ≫ L0 →
+                          ∀L2,e2. ↓[0, e2] L0 ≡ L2 → e2 ≤ d1 →
+                          ∃∃L. L [d1 - e2, e1] ≫ L2 & ↓[0, e2] L1 ≡ L.
+#L1 #L0 #d1 #e1 #H elim H -H L1 L0 d1 e1
+[ #d1 #e1 #L2 #e2 #H >(drop_inv_atom1 … H) -H /2/
+| /2/
+| normalize #K1 #K0 #I #V1 #V0 #e1 #HK10 #HV10 #_ #L2 #e2 #H #He2
+  lapply (le_n_O_to_eq … He2) -He2 #He2 destruct -e2;
+  lapply (drop_inv_refl … H) -H #H destruct -L2 /3/
+| #K1 #K0 #I #V1 #V0 #d1 #e1 #HK10 #HV10 #IHK10 #L2 #e2 #H #He2d1
+  lapply (drop_inv_O1 … H) -H * * #He2 #HK0L2
+  [ destruct -IHK10 He2d1 e2 L2 <minus_n_O /3/
+  | -HK10 HV10 <minus_le_minus_minus_comm //
+    elim (IHK10 … HK0L2 ?) -IHK10 HK0L2 /3/
+  ]
+]
+qed.
+*)