- lambdadelta: more service lemmas ...

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / computation / fprs_cprs.ma

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 4e7a633c32e3bbf4df83e573ae1d4656bbe21ed1..0464705b99eaaf1ae66a95812af79aafcb88c315 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/fprs_cprs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/fprs_cprs.ma
@@ -13,18 +13,67 @@
 (**************************************************************************)
 
 include "basic_2/reducibility/fpr_cpr.ma".
-include "basic_2/computation/cprs.ma".
-include "basic_2/computation/fprs.ma".
+include "basic_2/computation/cprs_lfprs.ma".
+include "basic_2/computation/lfprs_ltprs.ma".
+include "basic_2/computation/lfprs_fprs.ma".
 
 (* CONTEXT-FREE PARALLEL COMPUTATION ON CLOSURES ****************************)
 
+(* Advanced inversion lemmas ************************************************)
+
+lemma fprs_inv_pair1: ∀I,K1,L2,V1,T1,T2. ⦃K1.ⓑ{I}V1, T1⦄ ➡* ⦃L2, T2⦄ →
+                      ∃∃K2,V2. ⦃K1, V1⦄  ➡* ⦃K2, V2⦄ &
+                               ⦃K1, -ⓑ{I}V1.T1⦄ ➡* ⦃K2, -ⓑ{I}V2.T2⦄  &
+                               L2 = K2.ⓑ{I}V2.
+#I #K1 #L2 #V1 #T1 #T2 #H @(fprs_ind … H) -L2 -T2 /2 width=5/
+#L #L2 #T #T2 #_ #HT2 * #K #V #HV1 #HT1 #H destruct
+elim (fpr_inv_pair1 … HT2) -HT2 #K2 #V2 #HV2 #HT2 #H destruct /3 width=5/
+qed-.
+
+lemma fprs_inv_pair3: ∀I,L1,K2,V2,T1,T2. ⦃L1, T1⦄ ➡* ⦃K2.ⓑ{I}V2, T2⦄ →
+                      ∃∃K1,V1. ⦃K1, V1⦄  ➡* ⦃K2, V2⦄ &
+                               ⦃K1, -ⓑ{I}V1.T1⦄ ➡* ⦃K2, -ⓑ{I}V2.T2⦄  &
+                               L1 = K1.ⓑ{I}V1.
+#I2 #L1 #K2 #V2 #T1 #T2 #H @(fprs_ind_dx … H) -L1 -T1 /2 width=5/
+#L1 #L #T1 #T #HT1 #_ * #K #V #HV2 #HT2 #H destruct
+elim (fpr_inv_pair3 … HT1) -HT1 #K1 #V1 #HV1 #HT1 #H destruct /3 width=5/
+qed-.
+
+(* Advanced forward lemmas **************************************************)
+
+lemma fprs_fwd_bind2_minus: ∀I,L1,L,V1,T1,T. ⦃L1, -ⓑ{I}V1.T1⦄ ➡* ⦃L, T⦄ → ∀b.
+                            ∃∃V2,T2. ⦃L1, ⓑ{b,I}V1.T1⦄ ➡* ⦃L, ⓑ{b,I}V2.T2⦄ &
+                                     T = -ⓑ{I}V2.T2.
+#I #L1 #L #V1 #T1 #T #H1 #b @(fprs_ind … H1) -L -T /2 width=4/
+#L0 #L #T0 #T #_ #H0 * #W1 #U1 #HTU1 #H destruct
+elim (fpr_fwd_bind2_minus … H0 b) -H0 /3 width=4/
+qed-.
+
+lemma fprs_fwd_pair1_full: ∀I,K1,L2,V1,T1,T2. ⦃K1.ⓑ{I}V1, T1⦄ ➡* ⦃L2, T2⦄ →
+                           ∀b. ∃∃K2,V2. ⦃K1, V1⦄  ➡* ⦃K2, V2⦄ &
+                                        ⦃K1, ⓑ{b,I}V1.T1⦄ ➡* ⦃K2, ⓑ{b,I}V2.T2⦄ &
+                                        L2 = K2.ⓑ{I}V2.
+#I #K1 #L2 #V1 #T1 #T2 #H #b
+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-.
+
 (* Properties on context-sensitive parallel computation for terms ***********)
 
 lemma cprs_fprs: ∀L,T1,T2. L ⊢ T1 ➡* T2 → ⦃L, T1⦄ ➡* ⦃L, T2⦄.
 #L #T1 #T2 #H @(cprs_ind … H) -T2 // /3 width=4/
 qed.
+
+(* Forward lemmas on context-sensitive parallel computation for terms *******)
+
+lemma fprs_fwd_cprs: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ➡* ⦃L2, T2⦄ → L1 ⊢ T1 ➡* T2.
+#L1 #L2 #T1 #T2 #H @(fprs_ind … H) -L2 -T2 //
+#L #L2 #T #T2 #H1 #H2 #IH1
+elim (fpr_inv_all … H2) -H2 #L0 #HL0 #HT2 #_ -L2
+lapply (lfprs_cpr_trans L1 … HT2) -HT2 /3 width=3/
+qed-.
 (*
-(* Advanced propertis *******************************************************)
+(* Advanced properties ******************************************************)
 
 lamma fpr_bind_sn: ∀L1,L2,V1,V2. ⦃L1, V1⦄ ➡ ⦃L2, V2⦄ → ∀T1,T2. T1 ➡ T2 →
                    ∀a,I. ⦃L1, ⓑ{a,I}V1.T1⦄ ➡ ⦃L2, ⓑ{a,I}V2.T2⦄.
@@ -47,24 +96,4 @@ elim (fpr_inv_all … H) -H #L #HL1 #H #HL2
   #V #T #HV1 #_ #H destruct /3 width=4/
 ]
 qed-.
-
-(* Advanced inversion lemmas ************************************************)
-
-lamma fpr_inv_pair1: ∀I,K1,L2,V1,T1,T2. ⦃K1.ⓑ{I}V1, T1⦄ ➡ ⦃L2, T2⦄ →
-                     ∃∃K2,V2. ⦃K1, V1⦄  ➡ ⦃K2, V2⦄ &
-                              ⦃K1, -ⓑ{I}V1.T1⦄ ➡ ⦃K2, -ⓑ{I}V2.T2⦄  &
-                              L2 = K2.ⓑ{I}V2.
-#I1 #K1 #X #V1 #T1 #T2 #H
-elim (fpr_fwd_pair1 … H) -H #I2 #K2 #V2 #HT12 #H destruct
-elim (fpr_fwd_shift_bind_minus … HT12) #HV12 #H destruct /2 width=5/
-qed-.
-
-lamma fpr_inv_pair3: ∀I,L1,K2,V2,T1,T2. ⦃L1, T1⦄ ➡ ⦃K2.ⓑ{I}V2, T2⦄ →
-                     ∃∃K1,V1. ⦃K1, V1⦄  ➡ ⦃K2, V2⦄ &
-                              ⦃K1, -ⓑ{I}V1.T1⦄ ➡ ⦃K2, -ⓑ{I}V2.T2⦄  &
-                              L1 = K1.ⓑ{I}V1.
-#I2 #X #K2 #V2 #T1 #T2 #H
-elim (fpr_fwd_pair3 … H) -H #I1 #K1 #V1 #HT12 #H destruct
-elim (fpr_fwd_shift_bind_minus … HT12) #HV12 #H destruct /2 width=5/
-qed-.
 *)