From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Thu, 7 Feb 2013 18:58:52 +0000 (+0000)
Subject: even more service lemmas ...
X-Git-Tag: make_still_working~1263
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;ds=sidebyside;h=06fae7628917399b6ceabace25607d6aafab0040;hp=fce70f3556b1b8eab9655006fe2e6928948f3a99;p=helm.git

even more service lemmas ...
---

diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/fprs_cprs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fprs_cprs.ma
index 0464705b9..0370df1f8 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/fprs_cprs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/fprs_cprs.ma
@@ -19,6 +19,16 @@ include "basic_2/computation/lfprs_fprs.ma".
 
 (* CONTEXT-FREE PARALLEL COMPUTATION ON CLOSURES ****************************)
 
+(* Advanced properties ******************************************************)
+
+lemma fprs_bind2_minus: ∀I,L1,L2,V1,T1,U2. ⦃L1, -ⓑ{I}V1.T1⦄ ➡* ⦃L2, U2⦄ →
+                        ∃∃V2,T2. ⦃L1.ⓑ{I}V1, T1⦄ ➡* ⦃L2.ⓑ{I}V2, T2⦄ &
+                                 U2 = -ⓑ{I}V2.T2.
+#I #L1 #L2 #V1 #T1 #U2 #H @(fprs_ind … H) -L2 -U2 /2 width=4/
+#L #L2 #U #U2 #_ #HU2 * #V #T #HT1 #H destruct
+elim (fpr_bind2_minus … HU2) -HU2 /3 width=4/
+qed-.
+
 (* Advanced inversion lemmas ************************************************)
 
 lemma fprs_inv_pair1: ∀I,K1,L2,V1,T1,T2. ⦃K1.ⓑ{I}V1, T1⦄ ➡* ⦃L2, T2⦄ →
@@ -58,6 +68,14 @@ elim (fprs_inv_pair1 … H) -H #K2 #V2 #HV12 #HT12 #H destruct
 elim (fprs_fwd_bind2_minus … HT12 b) -HT12 #W1 #U1 #HTU1 #H destruct /2 width=5/
 qed-.
 
+lemma fprs_fwd_abst2: ∀a,L1,L2,V1,T1,U2. ⦃L1, ⓛ{a}V1.T1⦄ ➡* ⦃L2, U2⦄ → ∀b,I,W.
+                      ∃∃V2,T2. ⦃L1, ⓑ{b,I}W.T1⦄ ➡* ⦃L2, ⓑ{b,I}W.T2⦄ &
+                               U2 = ⓛ{a}V2.T2.
+#a #L1 #L2 #V1 #T1 #U2 #H #b #I #W @(fprs_ind … H) -L2 -U2 /2 width=4/
+#L #L2 #U #U2 #_ #H2 * #V #T #HT1 #H destruct
+elim (fpr_fwd_abst2 … H2 b I W) -H2 /3 width=4/
+qed-.
+
 (* Properties on context-sensitive parallel computation for terms ***********)
 
 lemma cprs_fprs: ∀L,T1,T2. L ⊢ T1 ➡* T2 → ⦃L, T1⦄ ➡* ⦃L, T2⦄.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_ltpr.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_ltpr.ma
index 07ac7b543..ace4e08d2 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_ltpr.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_ltpr.ma
@@ -73,8 +73,7 @@ fact ssta_ltpr_tpr_aux: ∀h,g,n. (
     [ #U #HTU20 #HU20 -HWV0 -HL12 -W1 -W2
       @(ex2_intro … (ⓓ{b}V2.U)) [ /2 width=1/ ] -h -l -l1 -V -V0 -T2 -T20 -U0
       @(fpcs_fprs_strap2 ? L1 … (ⓓ{b}V2.U2)) [ /4 width=1/ ] -V1
-      @fpcs_shift_full -b
-      @(fpcs_canc_dx ?? (L2.ⓓV2) … U20) [2: /2 width=1/ ] -U
+      /4 width=4 by fpcs_fwd_shift, fpcs_canc_dx, cpcs_fpcs, fpcs_fwd_abst13/
     | -b -l -V -V1 -T2 -T20 -U0 -U2 -U20
       /6 width=6 by lsubse_abbr, fpcs_inv_cpcs, fpcs_canc_sn, fpcs_fprs_strap1, cpcs_fpcs, bi_inj/
     ]
diff --git a/matita/matita/contribs/lambdadelta/basic_2/equivalence/fpcs_cpcs.ma b/matita/matita/contribs/lambdadelta/basic_2/equivalence/fpcs_cpcs.ma
index eda395e98..75e69cf08 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/equivalence/fpcs_cpcs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/equivalence/fpcs_cpcs.ma
@@ -20,25 +20,49 @@ include "basic_2/equivalence/fpcs_fpcs.ma".
 
 (* Advanced properties ******************************************************)
 
-lemma fpcs_shift: ∀I,L1,L2,V1,V2,T1,T2. ⦃L1.ⓑ{I}V1, T1⦄ ⬌* ⦃L2.ⓑ{I}V2, T2⦄ →
-                     ⦃L1, -ⓑ{I}V1.T1⦄ ⬌* ⦃L2, -ⓑ{I}V2.T2⦄.
+lemma fpcs_shift: ∀I,L1,L2,V1,V2,T1,T2. ⦃L1, -ⓑ{I}V1.T1⦄ ⬌* ⦃L2, -ⓑ{I}V2.T2⦄ →
+                  ⦃L1.ⓑ{I}V1, T1⦄ ⬌* ⦃L2.ⓑ{I}V2, T2⦄.
+#I #L1 #L2 #V1 #V2 #T1 #T2 #H12
+elim (fpcs_inv_fprs … H12) -H12 #L #T #H1 #H2
+elim (fprs_bind2_minus … H1) -H1 #W1 #U1 #HTU1 #H destruct
+elim (fprs_bind2_minus … H2) -H2 #W2 #U2 #HTU2 #H destruct /2 width=4/
+qed.
+
+(* Advanced inversion lemmas ************************************************)
+
+lemma fpcs_inv_shift: ∀I,L1,L2,V1,V2,T1,T2. ⦃L1.ⓑ{I}V1, T1⦄ ⬌* ⦃L2.ⓑ{I}V2, T2⦄ →
+                         ⦃L1, -ⓑ{I}V1.T1⦄ ⬌* ⦃L2, -ⓑ{I}V2.T2⦄.
 #I #L1 #L2 #V1 #V2 #T1 #T2 #H12
 elim (fpcs_inv_fprs … H12) -H12 #L #T #H1 #H2
 elim (fprs_inv_pair1 … H1) -H1 #K1 #U1 #_ #HTU1 #H destruct
 elim (fprs_inv_pair1 … H2) -H2 #K2 #U2 #_ #HTU2 #H destruct /2 width=4/
-qed.
+qed-.
 
-lemma fpcs_bind_minus: ∀I,L1,L2,V1,V2,T1,T2. ⦃L1, -ⓑ{I}V1.T1⦄ ⬌* ⦃L2, -ⓑ{I}V2.T2⦄ →
-                       ∀b. ⦃L1, ⓑ{b,I}V1.T1⦄ ⬌* ⦃L2, ⓑ{b,I}V2.T2⦄.
+(* Advanced forward lemmas **************************************************)
+
+lemma fpcs_fwd_bind_minus: ∀I,L1,L2,V1,V2,T1,T2. ⦃L1, -ⓑ{I}V1.T1⦄ ⬌* ⦃L2, -ⓑ{I}V2.T2⦄ →
+                           ∀b. ⦃L1, ⓑ{b,I}V1.T1⦄ ⬌* ⦃L2, ⓑ{b,I}V2.T2⦄.
 #I #L1 #L2 #V1 #V2 #T1 #T2 #H12 #b
 elim (fpcs_inv_fprs … H12) -H12 #L #T #H1 #H2
 elim (fprs_fwd_bind2_minus … H1 b) -H1 #W1 #U1 #HTU1 #H destruct
 elim (fprs_fwd_bind2_minus … H2 b) -H2 #W2 #U2 #HTU2 #H destruct /2 width=4/
-qed.
+qed-.
+
+lemma fpcs_fwd_shift: ∀I,L1,L2,V1,V2,T1,T2. ⦃L1.ⓑ{I}V1, T1⦄ ⬌* ⦃L2.ⓑ{I}V2, T2⦄ →
+                      ∀b. ⦃L1, ⓑ{b,I}V1.T1⦄ ⬌* ⦃L2, ⓑ{b,I}V2.T2⦄.
+/3 width=1 by fpcs_inv_shift, fpcs_fwd_bind_minus/ qed-.
+
+lemma fpcs_fwd_abst24: ∀a,L1,L2,V1,V2,T1,T2. ⦃L1, ⓛ{a}V1.T1⦄ ⬌* ⦃L2, ⓛ{a}V2.T2⦄ →
+                       ∀b,I,W. ⦃L1, ⓑ{b,I}W.T1⦄ ⬌* ⦃L2, ⓑ{b,I}W.T2⦄.
+#a #L1 #L2 #V1 #V2 #T1 #T2 #H12 #b #I #W
+elim (fpcs_inv_fprs … H12) -H12 #L #U #H1 #H2
+elim (fprs_fwd_abst2 … H1 b I W) -H1 #W1 #U1 #HTU1 #H destruct
+elim (fprs_fwd_abst2 … H2 b I W) -H2 #W2 #U2 #HTU2 #H destruct /2 width=4/
+qed-.
 
-lemma fpcs_shift_full: ∀I,L1,L2,V1,V2,T1,T2. ⦃L1.ⓑ{I}V1, T1⦄ ⬌* ⦃L2.ⓑ{I}V2, T2⦄ →
-                       ∀b. ⦃L1, ⓑ{b,I}V1.T1⦄ ⬌* ⦃L2, ⓑ{b,I}V2.T2⦄.
-/3 width=1/ qed.
+lemma fpcs_fwd_abst13: ∀L1,L2,V1,V2,T1,T2. ⦃L1.ⓛV1, T1⦄ ⬌* ⦃L2.ⓛV2, T2⦄ →
+                       ∀I,W. ⦃L1.ⓑ{I}W, T1⦄ ⬌* ⦃L2.ⓑ{I}W, T2⦄.
+/4 width=4 by fpcs_fwd_shift, fpcs_fwd_abst24, fpcs_shift/ qed-.
 
 (* Properties on context-sensitive parallel equivalence for terms ***********)
 
diff --git a/matita/matita/contribs/lambdadelta/basic_2/reducibility/cpr_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/reducibility/cpr_lift.ma
index ae4617f80..bcef7bb74 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/reducibility/cpr_lift.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/reducibility/cpr_lift.ma
@@ -134,7 +134,18 @@ elim (cpr_inv_appl1 … H) -H *
   elim (simple_inv_bind … HT1)
 ]
 qed-.
-     
+
+(* Advanced forward lemmas **************************************************)
+
+lemma cpr_fwd_abst1: ∀a,L,V1,T1,U2. L ⊢ ⓛ{a}V1.T1 ➡ U2 → ∀b,I,W.
+                     ∃∃V2,T2. L ⊢ ⓑ{b,I}W.T1 ➡ ⓑ{b,I}W.T2 &
+                              U2 = ⓛ{a}V2.T2.
+#a #L #V1 #T1 #U2 * #U #H #HU2 #b #I #W
+elim (tpr_fwd_abst1 … H b I W) -H #V #T #HT1 #H destruct
+elim (tpss_inv_bind1 … HU2) -HU2 #V2 #T2 #_ #HT2
+lapply (tpss_lsubs_trans … HT2 (L.ⓑ{I}W) ?) -HT2 /2 width=1/ /4 width=5/
+qed-.
+
 (* Relocation properties ****************************************************)
 
 (* Basic_1: was: pr2_lift *)
diff --git a/matita/matita/contribs/lambdadelta/basic_2/reducibility/fpr_cpr.ma b/matita/matita/contribs/lambdadelta/basic_2/reducibility/fpr_cpr.ma
index 9bd19002a..95aef01d4 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/reducibility/fpr_cpr.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/reducibility/fpr_cpr.ma
@@ -29,6 +29,14 @@ lemma fpr_bind_sn: ∀L1,L2,V1,V2. ⦃L1, V1⦄ ➡ ⦃L2, V2⦄ → ∀T1,T2. T
 elim (fpr_inv_all … H) /3 width=4/
 qed.
 
+lemma fpr_bind2_minus: ∀I,L1,L2,V1,T1,U2. ⦃L1, -ⓑ{I}V1.T1⦄ ➡ ⦃L2, U2⦄ →
+                       ∃∃V2,T2. ⦃L1.ⓑ{I}V1, T1⦄ ➡ ⦃L2.ⓑ{I}V2, T2⦄ &
+                                U2 = -ⓑ{I}V2.T2.
+#I1 #L1 #L2 #V1 #T1 #U2 #H
+elim (fpr_inv_all … H) -H #L #HL1 #H #HL2
+elim (cpr_fwd_bind1_minus … H false) -H /4 width=4/
+qed-.
+
 (* Advanced forward lemmas **************************************************)
 
 lemma fpr_fwd_bind2_minus: ∀I,L1,L,V1,T1,T. ⦃L1, -ⓑ{I}V1.T1⦄ ➡ ⦃L, T⦄ → ∀b.
@@ -53,6 +61,14 @@ elim (fpr_inv_all … H) -H #L #HL1 #H #HL2
 ]
 qed-.
 
+lemma fpr_fwd_abst2: ∀a,L1,L2,V1,T1,U2. ⦃L1, ⓛ{a}V1.T1⦄ ➡ ⦃L2, U2⦄ → ∀b,I,W.
+                     ∃∃V2,T2. ⦃L1, ⓑ{b,I}W.T1⦄ ➡ ⦃L2, ⓑ{b,I}W.T2⦄ &
+                              U2 = ⓛ{a}V2.T2.
+#a #L1 #L2 #V1 #T1 #U2 #H
+elim (fpr_inv_all … H) #L #HL1 #H #HL2 #b #I #W
+elim (cpr_fwd_abst1 … H b I W) -H /3 width=4/
+qed-.
+
 (* Advanced inversion lemmas ************************************************)
 
 lemma fpr_inv_pair1: ∀I,K1,L2,V1,T1,T2. ⦃K1.ⓑ{I}V1, T1⦄ ➡ ⦃L2, T2⦄ →
diff --git a/matita/matita/contribs/lambdadelta/basic_2/reducibility/tpr.ma b/matita/matita/contribs/lambdadelta/basic_2/reducibility/tpr.ma
index 280410b80..735836d0e 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/reducibility/tpr.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/reducibility/tpr.ma
@@ -234,5 +234,5 @@ qed-.
 
 (* Basic_1: removed theorems 3:
             pr0_subst0_back pr0_subst0_fwd pr0_subst0
-   Basic_1: removed local theorems: 1: pr0_delta_tau
-*)
+*)   
+(* Basic_1: removed local theorems: 1: pr0_delta_tau *)
diff --git a/matita/matita/contribs/lambdadelta/basic_2/reducibility/tpr_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/reducibility/tpr_lift.ma
index 438cefbca..8d6b0363a 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/reducibility/tpr_lift.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/reducibility/tpr_lift.ma
@@ -98,21 +98,24 @@ qed-.
 
 (* Advanced inversion lemmas ************************************************)
 
-fact tpr_inv_abst1_aux: ∀U1,U2. U1 ➡ U2 → ∀a,V1,T1. U1 = ⓛ{a}V1. T1 →
-                        ∃∃V2,T2. V1 ➡ V2 & T1 ➡ T2 & U2 = ⓛ{a}V2. T2.
-#U1 #U2 * -U1 -U2
-[ #I #a #V #T #H destruct
-| #I #V1 #V2 #T1 #T2 #_ #_ #a #V #T #H destruct
-| #b #V1 #V2 #W #T1 #T2 #_ #_ #a #V #T #H destruct
-| #b #I #V1 #V2 #T1 #T #T2 #HV12 #HT1 #HT2 #a #V0 #T0 #H destruct
-  <(tps_inv_refl_SO2 … HT2 ? ? ?) -T2 /2 width=5/
-| #b #V #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #_ #a #V0 #T0 #H destruct
-| #V #T1 #T #T2 #_ #_ #a #V0 #T0 #H destruct
-| #V #T1 #T2 #_ #a #V0 #T0 #H destruct
-]
-qed.
-
 (* Basic_1: was pr0_gen_abst *)
 lemma tpr_inv_abst1: ∀a,V1,T1,U2. ⓛ{a}V1. T1 ➡ U2 →
                      ∃∃V2,T2. V1 ➡ V2 & T1 ➡ T2 & U2 = ⓛ{a}V2. T2.
-/2 width=3/ qed-.
+#a #V1 #T1 #U2 #H elim (tpr_inv_bind1 … H) -H *
+[ #V2 #T #T2 #HV12 #HT1 #HT2
+  lapply (tps_inv_refl_SO2 … HT2 ???) -HT2 // /2 width=5/
+| #T2 #_ #_ #_ #H destruct
+]
+qed-.
+
+(* Advanced forward lemmas **************************************************)
+
+lemma tpr_fwd_abst1: ∀a,V1,T1,U2. ⓛ{a}V1.T1 ➡ U2 → ∀b,I,W.
+                     ∃∃V2,T2. ⓑ{b,I}W.T1 ➡ ⓑ{b,I}W.T2 &
+                              U2 = ⓛ{a}V2.T2.
+#a #V1 #T1 #U2 #H #b #I #W elim (tpr_inv_bind1 … H) -H *
+[ #V2 #T #T2 #HV12 #HT1 #HT2
+  lapply (tps_inv_refl_SO2 … HT2 ???) -HT2 // /3 width=4/
+| #T2 #_ #_ #_ #H destruct
+]
+qed-.