From: Ferruccio Guidi Date: Tue, 25 Mar 2014 19:55:08 +0000 (+0000) Subject: - partial commit: just the components below "computation" X-Git-Tag: make_still_working~945 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=956df16197063a88b3858e3d212d7ed0f2c5ff46;p=helm.git - partial commit: just the components below "computation" the development of lazy pointwise extensions continues ... - we parked not-lazy pointwise extensions in etc --- diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/llpx_sn/llpx_sn_tc.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/llpx_sn/llpx_sn_tc.etc new file mode 100644 index 000000000..682b48c68 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/llpx_sn/llpx_sn_tc.etc @@ -0,0 +1,160 @@ +(**************************************************************************) +(* ___ *) +(* ||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/relocation/ldrop_leq.ma". +include "basic_2/relocation/llpx_sn.ma". + +(* LAZY SN POINTWISE EXTENSION OF A CONTEXT-SENSITIVE REALTION FOR TERMS ****) + +definition TC_llpx_sn_confluent1: relation (relation3 lenv term term) ≝ λS,R. + ∀Ls,T1,T2. S Ls T1 T2 → + ∀Ld. TC … (llpx_sn R 0 T1) Ls Ld → TC … (llpx_sn R 0 T2) Ls Ld. + +lemma TC_llpx_sn_s_confluent: ∀S,R. (llpx_sn_confluent1 S R) → TC_llpx_sn_confluent1 S R. +#S #R #HSR #Ls #T1 #T2 #HT12 #Ld #H +generalize in match HT12; -HT12 +@(TC_ind_dx … Ls H) -Ls +[ /3 width=3 by inj/ +| #Ls #L #HLs #_ #IHLd #HT12 + @(TC_strap … L) /2 width=3 by/ @IHLd -IHLd + +lemma TC_llpx_sn_lref_refl: ∀R. (∀L.reflexive … (R L)) → + ∀I,L1,K1,K2,V,d,i. d ≤ yinj i → ⇩[i] L1 ≡ K1.ⓑ{I}V → + TC lenv (llpx_sn R 0 V) K1 K2 → + ∀L2. ⇩[i] L2 ≡ K2.ⓑ{I}V → TC … (llpx_sn R d (#i)) L1 L2. +#R #HR #I #L1 #K1 #K2 #V #d #i #Hdi #HLK1 #H @(TC_star_ind … K2 H) -K2 +[ /2 width=1 by llpx_sn_refl/ +| /4 width=9 by llpx_sn_refl, llpx_sn_lref, inj/ +| #K #K2 #_ #HV #IHK1 #L2 #HLK2 lapply (ldrop_fwd_length … HLK2) + #H elim (ldrop_O1_ex (K.ⓑ{I}V) i L2) [2: normalize in H ⊢ %; >(llpx_sn_fwd_length … HV) ] + /4 width=11 by llpx_sn_lref, step/ +] +qed-. + +lemma TC_llpx_sn_lref: ∀R. (∀L.reflexive … (R L)) → (llpx_sn_confluent1 R R) → + ∀I,K1,V1,V2,d,i. d ≤ yinj i → LTC … R K1 V1 V2 → + ∀K2. TC lenv (llpx_sn R 0 V1) K1 K2 → ∀L1. ⇩[i] L1 ≡ K1.ⓑ{I}V1 → + ∀L2. ⇩[i] L2 ≡ K2.ⓑ{I}V2 → TC … (llpx_sn R d (#i)) L1 L2. +#R #H1R #H2R #I #K1 #V1 #V2 #d #i #Hdi #H @(TC_star_ind_dx … V1 H) -V1 +[ /2 width=1 by llpx_sn_refl/ +| /2 width=7 by TC_llpx_sn_lref_refl/ +| #V1 #V #HV1 #_ #IHV2 #K2 #HK12 #L1 #HLK1 #L2 #HLK2 + lapply (ldrop_fwd_length … HLK1) + #H elim (ldrop_O1_ex (K1.ⓑ{I}V) i L1) [2: normalize in H ⊢ %; // ] -H + #L #_ #HLK @(TC_strap … L) + [ @(llpx_sn_lref … HLK1 … HLK) /2 width=1 by llpx_sn_refl/ + | @(IHV2 … HLK … HLK2) + -HLK1 -HLK2 -HLK -IHV2 -Hdi @(TC_llpx_sn_s_confluent R R … HK12) // + ] +] + + +lemma llpx_sn_LTC_TC_llpx_sn: ∀R. (∀L. reflexive … (R L)) → + ∀L1,L2,T,d. llpx_sn (LTC … R) d T L1 L2 → + TC … (llpx_sn R d T) L1 L2. +#R #HR #L1 #L2 #T #d #H elim H -L1 -L2 +/3 width=3 by llpx_sn_gref, llpx_sn_free, llpx_sn_skip, llpx_sn_sort, inj/ +[ #I #L1 #L2 #K1 #K2 #V1 #V2 #d #i #Hdi #HLK1 #HLK2 #_ #HV12 #IHV1 + +(* Properties on transitive_closure *****************************************) + +lemma TC_lpx_sn_pair: ∀R. (∀L. reflexive … (R L)) → + ∀I,L1,L2. TC … (lpx_sn R) L1 L2 → + ∀V1,V2. LTC … R L1 V1 V2 → + TC … (lpx_sn R) (L1. ⓑ{I} V1) (L2. ⓑ{I} V2). +#R #HR #I #L1 #L2 #HL12 #V1 #V2 #H @(TC_star_ind_dx … V1 H) -V1 // +[ /2 width=1 by TC_lpx_sn_pair_refl/ +| /4 width=3 by TC_strap, lpx_sn_pair, lpx_sn_refl/ +] +qed-. + +lemma lpx_sn_LTC_TC_lpx_sn: ∀R. (∀L. reflexive … (R L)) → + ∀L1,L2. lpx_sn (LTC … R) L1 L2 → + TC … (lpx_sn R) L1 L2. +#R #HR #L1 #L2 #H elim H -L1 -L2 +/2 width=1 by TC_lpx_sn_pair, lpx_sn_atom, inj/ +qed-. + +(* Inversion lemmas on transitive closure ***********************************) + +lemma TC_lpx_sn_inv_atom2: ∀R,L1. TC … (lpx_sn R) L1 (⋆) → L1 = ⋆. +#R #L1 #H @(TC_ind_dx … L1 H) -L1 +[ /2 width=2 by lpx_sn_inv_atom2/ +| #L1 #L #HL1 #_ #IHL2 destruct /2 width=2 by lpx_sn_inv_atom2/ +] +qed-. + +lemma TC_lpx_sn_inv_pair2: ∀R. s_rs_trans … R (lpx_sn R) → + ∀I,L1,K2,V2. TC … (lpx_sn R) L1 (K2.ⓑ{I}V2) → + ∃∃K1,V1. TC … (lpx_sn R) K1 K2 & LTC … R K1 V1 V2 & L1 = K1. ⓑ{I} V1. +#R #HR #I #L1 #K2 #V2 #H @(TC_ind_dx … L1 H) -L1 +[ #L1 #H elim (lpx_sn_inv_pair2 … H) -H /3 width=5 by inj, ex3_2_intro/ +| #L1 #L #HL1 #_ * #K #V #HK2 #HV2 #H destruct + elim (lpx_sn_inv_pair2 … HL1) -HL1 #K1 #V1 #HK1 #HV1 #H destruct + lapply (HR … HV2 … HK1) -HR -HV2 /3 width=5 by TC_strap, ex3_2_intro/ +] +qed-. + +lemma TC_lpx_sn_ind: ∀R. s_rs_trans … R (lpx_sn R) → + ∀S:relation lenv. + S (⋆) (⋆) → ( + ∀I,K1,K2,V1,V2. + TC … (lpx_sn R) K1 K2 → LTC … R K1 V1 V2 → + S K1 K2 → S (K1.ⓑ{I}V1) (K2.ⓑ{I}V2) + ) → + ∀L2,L1. TC … (lpx_sn R) L1 L2 → S L1 L2. +#R #HR #S #IH1 #IH2 #L2 elim L2 -L2 +[ #X #H >(TC_lpx_sn_inv_atom2 … H) -X // +| #L2 #I #V2 #IHL2 #X #H + elim (TC_lpx_sn_inv_pair2 … H) // -H -HR + #L1 #V1 #HL12 #HV12 #H destruct /3 width=1 by/ +] +qed-. + +lemma TC_lpx_sn_inv_atom1: ∀R,L2. TC … (lpx_sn R) (⋆) L2 → L2 = ⋆. +#R #L2 #H elim H -L2 +[ /2 width=2 by lpx_sn_inv_atom1/ +| #L #L2 #_ #HL2 #IHL1 destruct /2 width=2 by lpx_sn_inv_atom1/ +] +qed-. + +fact TC_lpx_sn_inv_pair1_aux: ∀R. s_rs_trans … R (lpx_sn R) → + ∀L1,L2. TC … (lpx_sn R) L1 L2 → + ∀I,K1,V1. L1 = K1.ⓑ{I}V1 → + ∃∃K2,V2. TC … (lpx_sn R) K1 K2 & LTC … R K1 V1 V2 & L2 = K2. ⓑ{I} V2. +#R #HR #L1 #L2 #H @(TC_lpx_sn_ind … H) // -HR -L1 -L2 +[ #J #K #W #H destruct +| #I #L1 #L2 #V1 #V2 #HL12 #HV12 #_ #J #K #W #H destruct /2 width=5 by ex3_2_intro/ +] +qed-. + +lemma TC_lpx_sn_inv_pair1: ∀R. s_rs_trans … R (lpx_sn R) → + ∀I,K1,L2,V1. TC … (lpx_sn R) (K1.ⓑ{I}V1) L2 → + ∃∃K2,V2. TC … (lpx_sn R) K1 K2 & LTC … R K1 V1 V2 & L2 = K2. ⓑ{I} V2. +/2 width=3 by TC_lpx_sn_inv_pair1_aux/ qed-. + +lemma TC_lpx_sn_inv_lpx_sn_LTC: ∀R. s_rs_trans … R (lpx_sn R) → + ∀L1,L2. TC … (lpx_sn R) L1 L2 → + lpx_sn (LTC … R) L1 L2. +/3 width=4 by TC_lpx_sn_ind, lpx_sn_pair/ qed-. + +(* Forward lemmas on transitive closure *************************************) + +lemma TC_lpx_sn_fwd_length: ∀R,L1,L2. TC … (lpx_sn R) L1 L2 → |L1| = |L2|. +#R #L1 #L2 #H elim H -L2 +[ #L2 #HL12 >(lpx_sn_fwd_length … HL12) -HL12 // +| #L #L2 #_ #HL2 #IHL1 + >IHL1 -L1 >(lpx_sn_fwd_length … HL2) -HL2 // +] +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/ldrop_lpx_sn.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/ldrop_lpx_sn.etc new file mode 100644 index 000000000..3dc3b2f79 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/ldrop_lpx_sn.etc @@ -0,0 +1,78 @@ +(**************************************************************************) +(* ___ *) +(* ||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/grammar/lpx_sn.ma". +include "basic_2/relocation/ldrop_leq.ma". + +(* DROPPING *****************************************************************) + +(* Properties on sn pointwise extension *************************************) + +lemma lpx_sn_deliftable_dropable: ∀R. l_deliftable_sn R → dropable_sn (lpx_sn R). +#R #HR #L1 #K1 #s #d #e #H elim H -L1 -K1 -d -e +[ #d #e #He #X #H >(lpx_sn_inv_atom1 … H) -H + /4 width=3 by ldrop_atom, lpx_sn_atom, ex2_intro/ +| #I #K1 #V1 #X #H elim (lpx_sn_inv_pair1 … H) -H + #L2 #V2 #HL12 #HV12 #H destruct + /3 width=5 by ldrop_pair, lpx_sn_pair, ex2_intro/ +| #I #L1 #K1 #V1 #e #_ #IHLK1 #X #H elim (lpx_sn_inv_pair1 … H) -H + #L2 #V2 #HL12 #HV12 #H destruct + elim (IHLK1 … HL12) -L1 /3 width=3 by ldrop_drop, ex2_intro/ +| #I #L1 #K1 #V1 #W1 #d #e #HLK1 #HWV1 #IHLK1 #X #H + elim (lpx_sn_inv_pair1 … H) -H #L2 #V2 #HL12 #HV12 #H destruct + elim (HR … HV12 … HLK1 … HWV1) -V1 + elim (IHLK1 … HL12) -L1 /3 width=5 by ldrop_skip, lpx_sn_pair, ex2_intro/ +] +qed-. + +lemma lpx_sn_liftable_dedropable: ∀R. (∀L. reflexive ? (R L)) → + l_liftable R → dedropable_sn (lpx_sn R). +#R #H1R #H2R #L1 #K1 #s #d #e #H elim H -L1 -K1 -d -e +[ #d #e #He #X #H >(lpx_sn_inv_atom1 … H) -H + /4 width=4 by ldrop_atom, lpx_sn_atom, ex3_intro/ +| #I #K1 #V1 #X #H elim (lpx_sn_inv_pair1 … H) -H + #K2 #V2 #HK12 #HV12 #H destruct + lapply (lpx_sn_fwd_length … HK12) + #H @(ex3_intro … (K2.ⓑ{I}V2)) (**) (* explicit constructor *) + /3 width=1 by lpx_sn_pair, monotonic_le_plus_l/ + @leq_O2 normalize // +| #I #L1 #K1 #V1 #e #_ #IHLK1 #K2 #HK12 elim (IHLK1 … HK12) -K1 + /3 width=5 by ldrop_drop, leq_pair, lpx_sn_pair, ex3_intro/ +| #I #L1 #K1 #V1 #W1 #d #e #HLK1 #HWV1 #IHLK1 #X #H + elim (lpx_sn_inv_pair1 … H) -H #K2 #W2 #HK12 #HW12 #H destruct + elim (lift_total W2 d e) #V2 #HWV2 + lapply (H2R … HW12 … HLK1 … HWV1 … HWV2) -W1 + elim (IHLK1 … HK12) -K1 + /3 width=6 by ldrop_skip, leq_succ, lpx_sn_pair, ex3_intro/ +] +qed-. + +fact lpx_sn_dropable_aux: ∀R,L2,K2,s,d,e. ⇩[s, d, e] L2 ≡ K2 → ∀L1. lpx_sn R L1 L2 → + d = 0 → ∃∃K1. ⇩[s, 0, e] L1 ≡ K1 & lpx_sn R K1 K2. +#R #L2 #K2 #s #d #e #H elim H -L2 -K2 -d -e +[ #d #e #He #X #H >(lpx_sn_inv_atom2 … H) -H + /4 width=3 by ldrop_atom, lpx_sn_atom, ex2_intro/ +| #I #K2 #V2 #X #H elim (lpx_sn_inv_pair2 … H) -H + #K1 #V1 #HK12 #HV12 #H destruct + /3 width=5 by ldrop_pair, lpx_sn_pair, ex2_intro/ +| #I #L2 #K2 #V2 #e #_ #IHLK2 #X #H #_ elim (lpx_sn_inv_pair2 … H) -H + #L1 #V1 #HL12 #HV12 #H destruct + elim (IHLK2 … HL12) -L2 /3 width=3 by ldrop_drop, ex2_intro/ +| #I #L2 #K2 #V2 #W2 #d #e #_ #_ #_ #L1 #_ + (length_inv_zero_dx … H) -L1 /3 width=5 by ex3_intro, conj/ +| #I2 #L2 #K2 #V2 #W2 #_ #HVW2 #IHLK2 #Y #H + elim (length_inv_pos_dx … H) -H #I #L1 #V1 #HL12 #H destruct + elim (IHLK2 … HL12) -IHLK2 #K1 #HLK1 #HK12 #IH + elim (eq_term_dec V1 V2) #H destruct + [ @(ex3_intro … (K1.ⓑ{I}W2)) normalize /2 width=1 by / +*) +axiom lleq_lpx_trans: ∀h,g,G,L2,K2. ⦃G, L2⦄ ⊢ ➡[h, g] K2 → + ∀L1,T,d. L1 ⋕[T, d] L2 → + ∃∃K1. ⦃G, L1⦄ ⊢ ➡[h, g] K1 & K1 ⋕[T, d] K2. +(* +#h #g #G #L2 #K2 #H elim H -L2 -K2 +[ #L1 #T #d #H lapply (lleq_fwd_length … H) -H + #H >(length_inv_zero_dx … H) -L1 /2 width=3 by ex2_intro/ +| #I2 #L2 #K2 #V2 #W2 #HLK2 #HVW2 #IHLK2 #Y #T #d #HT + lapply (lleq_fwd_length … HT) #H + elim (length_inv_pos_dx … H) -H #I1 #L1 #V1 #HL12 #H destruct + elim (eq_term_dec V1 V2) #H destruct + [ @ex2_intro … +*) + +lemma lpx_lleq_fqu_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃ ⦃G2, L2, T2⦄ → + ∀K1. ⦃G1, K1⦄ ⊢ ➡[h, g] L1 → K1 ⋕[T1, 0] L1 → + ∃∃K2. ⦃G1, K1, T1⦄ ⊃ ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡[h, g] L2 & K2 ⋕[T2, 0] L2. +#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2 +[ #I #G1 #L1 #V1 #X #H1 #H2 elim (lpx_inv_pair2 … H1) -H1 + #K0 #V0 #H1KL1 #_ #H destruct + elim (lleq_inv_lref_ge_dx … H2 ? I L1 V1) -H2 // + #K1 #H #H2KL1 lapply (ldrop_inv_O2 … H) -H #H destruct + /2 width=4 by fqu_lref_O, ex3_intro/ +| * [ #a ] #I #G1 #L1 #V1 #T1 #K1 #HLK1 #H + [ elim (lleq_inv_bind … H) + | elim (lleq_inv_flat … H) + ] -H /2 width=4 by fqu_pair_sn, ex3_intro/ +| #a #I #G1 #L1 #V1 #T1 #K1 #HLK1 #H elim (lleq_inv_bind_O … H) -H + /3 width=4 by lpx_pair, fqu_bind_dx, ex3_intro/ +| #I #G1 #L1 #V1 #T1 #K1 #HLK1 #H elim (lleq_inv_flat … H) -H + /2 width=4 by fqu_flat_dx, ex3_intro/ +| #G1 #L1 #L #T1 #U1 #e #HL1 #HTU1 #K1 #H1KL1 #H2KL1 + elim (ldrop_O1_le (e+1) K1) + [ #K #HK1 lapply (lleq_inv_lift_le … H2KL1 … HK1 HL1 … HTU1 ?) -H2KL1 // + #H2KL elim (lpx_ldrop_trans_O1 … H1KL1 … HL1) -L1 + #K0 #HK10 #H1KL lapply (ldrop_mono … HK10 … HK1) -HK10 #H destruct + /3 width=4 by fqu_drop, ex3_intro/ + | lapply (ldrop_fwd_length_le2 … HL1) -L -T1 -g + lapply (lleq_fwd_length … H2KL1) // + ] +] +qed-. + +lemma lpx_lleq_fquq_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃⸮ ⦃G2, L2, T2⦄ → + ∀K1. ⦃G1, K1⦄ ⊢ ➡[h, g] L1 → K1 ⋕[T1, 0] L1 → + ∃∃K2. ⦃G1, K1, T1⦄ ⊃⸮ ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡[h, g] L2 & K2 ⋕[T2, 0] L2. +#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H #K1 #H1KL1 #H2KL1 +elim (fquq_inv_gen … H) -H +[ #H elim (lpx_lleq_fqu_trans … H … H1KL1 H2KL1) -L1 + /3 width=4 by fqu_fquq, ex3_intro/ +| * #HG #HL #HT destruct /2 width=4 by ex3_intro/ +] +qed-. + +lemma lpx_lleq_fqup_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃+ ⦃G2, L2, T2⦄ → + ∀K1. ⦃G1, K1⦄ ⊢ ➡[h, g] L1 → K1 ⋕[T1, 0] L1 → + ∃∃K2. ⦃G1, K1, T1⦄ ⊃+ ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡[h, g] L2 & K2 ⋕[T2, 0] L2. +#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H @(fqup_ind … H) -G2 -L2 -T2 +[ #G2 #L2 #T2 #H #K1 #H1KL1 #H2KL1 elim (lpx_lleq_fqu_trans … H … H1KL1 H2KL1) -L1 + /3 width=4 by fqu_fqup, ex3_intro/ +| #G #G2 #L #L2 #T #T2 #_ #HT2 #IHT1 #K1 #H1KL1 #H2KL1 elim (IHT1 … H2KL1) // -L1 + #K #HT1 #H1KL #H2KL elim (lpx_lleq_fqu_trans … HT2 … H1KL H2KL) -L + /3 width=5 by fqup_strap1, ex3_intro/ +] +qed-. + +lemma lpx_lleq_fqus_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃* ⦃G2, L2, T2⦄ → + ∀K1. ⦃G1, K1⦄ ⊢ ➡[h, g] L1 → K1 ⋕[T1, 0] L1 → + ∃∃K2. ⦃G1, K1, T1⦄ ⊃* ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡[h, g] L2 & K2 ⋕[T2, 0] L2. +#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H #K1 #H1KL1 #H2KL1 +elim (fqus_inv_gen … H) -H +[ #H elim (lpx_lleq_fqup_trans … H … H1KL1 H2KL1) -L1 + /3 width=4 by fqup_fqus, ex3_intro/ +| * #HG #HL #HT destruct /2 width=4 by ex3_intro/ +] +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lpx_sn.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lpx_sn.etc new file mode 100644 index 000000000..fddde2de5 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lpx_sn.etc @@ -0,0 +1,89 @@ +(**************************************************************************) +(* ___ *) +(* ||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/grammar/lenv_length.ma". + +(* SN POINTWISE EXTENSION OF A CONTEXT-SENSITIVE REALTION FOR TERMS *********) + +inductive lpx_sn (R:lenv→relation term): relation lenv ≝ +| lpx_sn_atom: lpx_sn R (⋆) (⋆) +| lpx_sn_pair: ∀I,K1,K2,V1,V2. + lpx_sn R K1 K2 → R K1 V1 V2 → + lpx_sn R (K1. ⓑ{I} V1) (K2. ⓑ{I} V2) +. + +(* Basic properties *********************************************************) + +lemma lpx_sn_refl: ∀R. (∀L. reflexive ? (R L)) → reflexive … (lpx_sn R). +#R #HR #L elim L -L /2 width=1 by lpx_sn_atom, lpx_sn_pair/ +qed-. + +(* Basic inversion lemmas ***************************************************) + +fact lpx_sn_inv_atom1_aux: ∀R,L1,L2. lpx_sn R L1 L2 → L1 = ⋆ → L2 = ⋆. +#R #L1 #L2 * -L1 -L2 +[ // +| #I #K1 #K2 #V1 #V2 #_ #_ #H destruct +] +qed-. + +lemma lpx_sn_inv_atom1: ∀R,L2. lpx_sn R (⋆) L2 → L2 = ⋆. +/2 width=4 by lpx_sn_inv_atom1_aux/ qed-. + +fact lpx_sn_inv_pair1_aux: ∀R,L1,L2. lpx_sn R L1 L2 → ∀I,K1,V1. L1 = K1. ⓑ{I} V1 → + ∃∃K2,V2. lpx_sn R K1 K2 & R K1 V1 V2 & L2 = K2. ⓑ{I} V2. +#R #L1 #L2 * -L1 -L2 +[ #J #K1 #V1 #H destruct +| #I #K1 #K2 #V1 #V2 #HK12 #HV12 #J #L #W #H destruct /2 width=5 by ex3_2_intro/ +] +qed-. + +lemma lpx_sn_inv_pair1: ∀R,I,K1,V1,L2. lpx_sn R (K1. ⓑ{I} V1) L2 → + ∃∃K2,V2. lpx_sn R K1 K2 & R K1 V1 V2 & L2 = K2. ⓑ{I} V2. +/2 width=3 by lpx_sn_inv_pair1_aux/ qed-. + +fact lpx_sn_inv_atom2_aux: ∀R,L1,L2. lpx_sn R L1 L2 → L2 = ⋆ → L1 = ⋆. +#R #L1 #L2 * -L1 -L2 +[ // +| #I #K1 #K2 #V1 #V2 #_ #_ #H destruct +] +qed-. + +lemma lpx_sn_inv_atom2: ∀R,L1. lpx_sn R L1 (⋆) → L1 = ⋆. +/2 width=4 by lpx_sn_inv_atom2_aux/ qed-. + +fact lpx_sn_inv_pair2_aux: ∀R,L1,L2. lpx_sn R L1 L2 → ∀I,K2,V2. L2 = K2. ⓑ{I} V2 → + ∃∃K1,V1. lpx_sn R K1 K2 & R K1 V1 V2 & L1 = K1. ⓑ{I} V1. +#R #L1 #L2 * -L1 -L2 +[ #J #K2 #V2 #H destruct +| #I #K1 #K2 #V1 #V2 #HK12 #HV12 #J #K #W #H destruct /2 width=5 by ex3_2_intro/ +] +qed-. + +lemma lpx_sn_inv_pair2: ∀R,I,L1,K2,V2. lpx_sn R L1 (K2. ⓑ{I} V2) → + ∃∃K1,V1. lpx_sn R K1 K2 & R K1 V1 V2 & L1 = K1. ⓑ{I} V1. +/2 width=3 by lpx_sn_inv_pair2_aux/ qed-. + +lemma lpx_sn_inv_pair: ∀R,I1,I2,L1,L2,V1,V2. + lpx_sn R (L1.ⓑ{I1}V1) (L2.ⓑ{I2}V2) → + ∧∧ lpx_sn R L1 L2 & R L1 V1 V2 & I1 = I2. +#R #I1 #I2 #L1 #L2 #V1 #V2 #H elim (lpx_sn_inv_pair1 … H) -H +#L0 #V0 #HL10 #HV10 #H destruct /2 width=1 by and3_intro/ +qed-. + +(* Basic forward lemmas *****************************************************) + +lemma lpx_sn_fwd_length: ∀R,L1,L2. lpx_sn R L1 L2 → |L1| = |L2|. +#R #L1 #L2 #H elim H -L1 -L2 normalize // +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lpx_sn_lpx_sn.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lpx_sn_lpx_sn.etc new file mode 100644 index 000000000..69c010a19 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lpx_sn_lpx_sn.etc @@ -0,0 +1,48 @@ +(**************************************************************************) +(* ___ *) +(* ||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/grammar/lpx_sn.ma". + +(* SN POINTWISE EXTENSION OF A CONTEXT-SENSITIVE REALTION FOR TERMS *********) + +definition lpx_sn_confluent: relation (lenv→relation term) ≝ λR1,R2. + ∀L0,T0,T1. R1 L0 T0 T1 → ∀T2. R2 L0 T0 T2 → + ∀L1. lpx_sn R1 L0 L1 → ∀L2. lpx_sn R2 L0 L2 → + ∃∃T. R2 L1 T1 T & R1 L2 T2 T. + +definition lpx_sn_transitive: relation (lenv→relation term) ≝ λR1,R2. + ∀L1,T1,T. R1 L1 T1 T → ∀L2. lpx_sn R1 L1 L2 → + ∀T2. R2 L2 T T2 → R1 L1 T1 T2. + +(* Main properties **********************************************************) + +theorem lpx_sn_trans: ∀R. lpx_sn_transitive R R → Transitive … (lpx_sn R). +#R #HR #L1 #L #H elim H -L1 -L // +#I #L1 #L #V1 #V #HL1 #HV1 #IHL1 #X #H +elim (lpx_sn_inv_pair1 … H) -H #L2 #V2 #HL2 #HV2 #H destruct /3 width=5/ +qed-. + +theorem lpx_sn_conf: ∀R1,R2. lpx_sn_confluent R1 R2 → + confluent2 … (lpx_sn R1) (lpx_sn R2). +#R1 #R2 #HR12 #L0 @(f_ind … length … L0) -L0 #n #IH * +[ #_ #X1 #H1 #X2 #H2 -n + >(lpx_sn_inv_atom1 … H1) -X1 + >(lpx_sn_inv_atom1 … H2) -X2 /2 width=3/ +| #L0 #I #V0 #Hn #X1 #H1 #X2 #H2 destruct + elim (lpx_sn_inv_pair1 … H1) -H1 #L1 #V1 #HL01 #HV01 #H destruct + elim (lpx_sn_inv_pair1 … H2) -H2 #L2 #V2 #HL02 #HV02 #H destruct + elim (IH … HL01 … HL02) -IH normalize // #L #HL1 #HL2 + elim (HR12 … HV01 … HV02 … HL01 … HL02) -L0 -V0 /3 width=5/ +] +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lpx_sn_tc.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lpx_sn_tc.etc new file mode 100644 index 000000000..2919d9d10 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lpx_sn_tc.etc @@ -0,0 +1,119 @@ +(**************************************************************************) +(* ___ *) +(* ||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/grammar/lpx_sn.ma". + +(* SN POINTWISE EXTENSION OF A CONTEXT-SENSITIVE REALTION FOR TERMS *********) + +(* Properties on transitive_closure *****************************************) + +lemma TC_lpx_sn_pair_refl: ∀R. (∀L. reflexive … (R L)) → + ∀L1,L2. TC … (lpx_sn R) L1 L2 → + ∀I,V. TC … (lpx_sn R) (L1. ⓑ{I} V) (L2. ⓑ{I} V). +#R #HR #L1 #L2 #H @(TC_star_ind … L2 H) -L2 +[ /2 width=1 by lpx_sn_refl/ +| /3 width=1 by TC_reflexive, lpx_sn_refl/ +| /3 width=5 by lpx_sn_pair, step/ +] +qed-. + +lemma TC_lpx_sn_pair: ∀R. (∀L. reflexive … (R L)) → + ∀I,L1,L2. TC … (lpx_sn R) L1 L2 → + ∀V1,V2. LTC … R L1 V1 V2 → + TC … (lpx_sn R) (L1. ⓑ{I} V1) (L2. ⓑ{I} V2). +#R #HR #I #L1 #L2 #HL12 #V1 #V2 #H @(TC_star_ind_dx … V1 H) -V1 // +[ /2 width=1 by TC_lpx_sn_pair_refl/ +| /4 width=3 by TC_strap, lpx_sn_pair, lpx_sn_refl/ +] +qed-. + +lemma lpx_sn_LTC_TC_lpx_sn: ∀R. (∀L. reflexive … (R L)) → + ∀L1,L2. lpx_sn (LTC … R) L1 L2 → + TC … (lpx_sn R) L1 L2. +#R #HR #L1 #L2 #H elim H -L1 -L2 +/2 width=1 by TC_lpx_sn_pair, lpx_sn_atom, inj/ +qed-. + +(* Inversion lemmas on transitive closure ***********************************) + +lemma TC_lpx_sn_inv_atom2: ∀R,L1. TC … (lpx_sn R) L1 (⋆) → L1 = ⋆. +#R #L1 #H @(TC_ind_dx … L1 H) -L1 +[ /2 width=2 by lpx_sn_inv_atom2/ +| #L1 #L #HL1 #_ #IHL2 destruct /2 width=2 by lpx_sn_inv_atom2/ +] +qed-. + +lemma TC_lpx_sn_inv_pair2: ∀R. s_rs_trans … R (lpx_sn R) → + ∀I,L1,K2,V2. TC … (lpx_sn R) L1 (K2.ⓑ{I}V2) → + ∃∃K1,V1. TC … (lpx_sn R) K1 K2 & LTC … R K1 V1 V2 & L1 = K1. ⓑ{I} V1. +#R #HR #I #L1 #K2 #V2 #H @(TC_ind_dx … L1 H) -L1 +[ #L1 #H elim (lpx_sn_inv_pair2 … H) -H /3 width=5 by inj, ex3_2_intro/ +| #L1 #L #HL1 #_ * #K #V #HK2 #HV2 #H destruct + elim (lpx_sn_inv_pair2 … HL1) -HL1 #K1 #V1 #HK1 #HV1 #H destruct + lapply (HR … HV2 … HK1) -HR -HV2 /3 width=5 by TC_strap, ex3_2_intro/ +] +qed-. + +lemma TC_lpx_sn_ind: ∀R. s_rs_trans … R (lpx_sn R) → + ∀S:relation lenv. + S (⋆) (⋆) → ( + ∀I,K1,K2,V1,V2. + TC … (lpx_sn R) K1 K2 → LTC … R K1 V1 V2 → + S K1 K2 → S (K1.ⓑ{I}V1) (K2.ⓑ{I}V2) + ) → + ∀L2,L1. TC … (lpx_sn R) L1 L2 → S L1 L2. +#R #HR #S #IH1 #IH2 #L2 elim L2 -L2 +[ #X #H >(TC_lpx_sn_inv_atom2 … H) -X // +| #L2 #I #V2 #IHL2 #X #H + elim (TC_lpx_sn_inv_pair2 … H) // -H -HR + #L1 #V1 #HL12 #HV12 #H destruct /3 width=1 by/ +] +qed-. + +lemma TC_lpx_sn_inv_atom1: ∀R,L2. TC … (lpx_sn R) (⋆) L2 → L2 = ⋆. +#R #L2 #H elim H -L2 +[ /2 width=2 by lpx_sn_inv_atom1/ +| #L #L2 #_ #HL2 #IHL1 destruct /2 width=2 by lpx_sn_inv_atom1/ +] +qed-. + +fact TC_lpx_sn_inv_pair1_aux: ∀R. s_rs_trans … R (lpx_sn R) → + ∀L1,L2. TC … (lpx_sn R) L1 L2 → + ∀I,K1,V1. L1 = K1.ⓑ{I}V1 → + ∃∃K2,V2. TC … (lpx_sn R) K1 K2 & LTC … R K1 V1 V2 & L2 = K2. ⓑ{I} V2. +#R #HR #L1 #L2 #H @(TC_lpx_sn_ind … H) // -HR -L1 -L2 +[ #J #K #W #H destruct +| #I #L1 #L2 #V1 #V2 #HL12 #HV12 #_ #J #K #W #H destruct /2 width=5 by ex3_2_intro/ +] +qed-. + +lemma TC_lpx_sn_inv_pair1: ∀R. s_rs_trans … R (lpx_sn R) → + ∀I,K1,L2,V1. TC … (lpx_sn R) (K1.ⓑ{I}V1) L2 → + ∃∃K2,V2. TC … (lpx_sn R) K1 K2 & LTC … R K1 V1 V2 & L2 = K2. ⓑ{I} V2. +/2 width=3 by TC_lpx_sn_inv_pair1_aux/ qed-. + +lemma TC_lpx_sn_inv_lpx_sn_LTC: ∀R. s_rs_trans … R (lpx_sn R) → + ∀L1,L2. TC … (lpx_sn R) L1 L2 → + lpx_sn (LTC … R) L1 L2. +/3 width=4 by TC_lpx_sn_ind, lpx_sn_pair/ qed-. + +(* Forward lemmas on transitive closure *************************************) + +lemma TC_lpx_sn_fwd_length: ∀R,L1,L2. TC … (lpx_sn R) L1 L2 → |L1| = |L2|. +#R #L1 #L2 #H elim H -L2 +[ #L2 #HL12 >(lpx_sn_fwd_length … HL12) -HL12 // +| #L #L2 #_ #HL2 #IHL1 + >IHL1 -L1 >(lpx_sn_fwd_length … HL2) -HL2 // +] +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/predsn_3.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/predsn_3.etc new file mode 100644 index 000000000..d06064a29 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/predsn_3.etc @@ -0,0 +1,19 @@ +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) + +(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) + +notation "hvbox( ⦃ term 46 G , break term 46 L1 ⦄ ⊢ ➡ break term 46 L2 )" + non associative with precedence 45 + for @{ 'PRedSn $G $L1 $L2 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/predsn_5.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/predsn_5.etc new file mode 100644 index 000000000..206566071 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/predsn_5.etc @@ -0,0 +1,19 @@ +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) + +(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) + +notation "hvbox( ⦃ term 46 G, break term 46 L1 ⦄ ⊢ ➡ break [ term 46 h , break term 46 g ] break term 46 L2 )" + non associative with precedence 45 + for @{ 'PRedSn $h $g $G $L1 $L2 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/predsnstar_3.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/predsnstar_3.etc new file mode 100644 index 000000000..2bcf32665 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/predsnstar_3.etc @@ -0,0 +1,19 @@ +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) + +(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) + +notation "hvbox( ⦃ term 46 G , break term 46 L1 ⦄ ⊢ ➡* break term 46 L2 )" + non associative with precedence 45 + for @{ 'PRedSnStar $G $L1 $L2 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/predsnstar_5.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/predsnstar_5.etc new file mode 100644 index 000000000..aef4f2707 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/predsnstar_5.etc @@ -0,0 +1,19 @@ +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) + +(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) + +notation "hvbox( ⦃ term 46 G, break term 46 L1 ⦄ ⊢ ➡ * break [ term 46 h , break term 46 g ] break term 46 L2 )" + non associative with precedence 45 + for @{ 'PRedSnStar $h $g $G $L1 $L2 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/predsnstaralt_3.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/predsnstaralt_3.etc new file mode 100644 index 000000000..45328fbaf --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/predsnstaralt_3.etc @@ -0,0 +1,19 @@ +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) + +(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) + +notation "hvbox( ⦃ term 46 G , break term 46 L1 ⦄ ⊢ ➡ ➡ * break term 46 L2 )" + non associative with precedence 45 + for @{ 'PRedSnStarAlt $G $L1 $L2 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/predsnstaralt_5.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/predsnstaralt_5.etc new file mode 100644 index 000000000..9682647cd --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/predsnstaralt_5.etc @@ -0,0 +1,19 @@ +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) + +(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) + +notation "hvbox( ⦃ term 46 G, break term 46 L1 ⦄ ⊢ ➡ ➡ * break [ term 46 h , break term 46 g ] break term 46 L2 )" + non associative with precedence 45 + for @{ 'PRedSnStarAlt $h $g $G $L1 $L2 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/grammar/lpx_sn.ma b/matita/matita/contribs/lambdadelta/basic_2/grammar/lpx_sn.ma deleted file mode 100644 index fddde2de5..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/grammar/lpx_sn.ma +++ /dev/null @@ -1,89 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||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/grammar/lenv_length.ma". - -(* SN POINTWISE EXTENSION OF A CONTEXT-SENSITIVE REALTION FOR TERMS *********) - -inductive lpx_sn (R:lenv→relation term): relation lenv ≝ -| lpx_sn_atom: lpx_sn R (⋆) (⋆) -| lpx_sn_pair: ∀I,K1,K2,V1,V2. - lpx_sn R K1 K2 → R K1 V1 V2 → - lpx_sn R (K1. ⓑ{I} V1) (K2. ⓑ{I} V2) -. - -(* Basic properties *********************************************************) - -lemma lpx_sn_refl: ∀R. (∀L. reflexive ? (R L)) → reflexive … (lpx_sn R). -#R #HR #L elim L -L /2 width=1 by lpx_sn_atom, lpx_sn_pair/ -qed-. - -(* Basic inversion lemmas ***************************************************) - -fact lpx_sn_inv_atom1_aux: ∀R,L1,L2. lpx_sn R L1 L2 → L1 = ⋆ → L2 = ⋆. -#R #L1 #L2 * -L1 -L2 -[ // -| #I #K1 #K2 #V1 #V2 #_ #_ #H destruct -] -qed-. - -lemma lpx_sn_inv_atom1: ∀R,L2. lpx_sn R (⋆) L2 → L2 = ⋆. -/2 width=4 by lpx_sn_inv_atom1_aux/ qed-. - -fact lpx_sn_inv_pair1_aux: ∀R,L1,L2. lpx_sn R L1 L2 → ∀I,K1,V1. L1 = K1. ⓑ{I} V1 → - ∃∃K2,V2. lpx_sn R K1 K2 & R K1 V1 V2 & L2 = K2. ⓑ{I} V2. -#R #L1 #L2 * -L1 -L2 -[ #J #K1 #V1 #H destruct -| #I #K1 #K2 #V1 #V2 #HK12 #HV12 #J #L #W #H destruct /2 width=5 by ex3_2_intro/ -] -qed-. - -lemma lpx_sn_inv_pair1: ∀R,I,K1,V1,L2. lpx_sn R (K1. ⓑ{I} V1) L2 → - ∃∃K2,V2. lpx_sn R K1 K2 & R K1 V1 V2 & L2 = K2. ⓑ{I} V2. -/2 width=3 by lpx_sn_inv_pair1_aux/ qed-. - -fact lpx_sn_inv_atom2_aux: ∀R,L1,L2. lpx_sn R L1 L2 → L2 = ⋆ → L1 = ⋆. -#R #L1 #L2 * -L1 -L2 -[ // -| #I #K1 #K2 #V1 #V2 #_ #_ #H destruct -] -qed-. - -lemma lpx_sn_inv_atom2: ∀R,L1. lpx_sn R L1 (⋆) → L1 = ⋆. -/2 width=4 by lpx_sn_inv_atom2_aux/ qed-. - -fact lpx_sn_inv_pair2_aux: ∀R,L1,L2. lpx_sn R L1 L2 → ∀I,K2,V2. L2 = K2. ⓑ{I} V2 → - ∃∃K1,V1. lpx_sn R K1 K2 & R K1 V1 V2 & L1 = K1. ⓑ{I} V1. -#R #L1 #L2 * -L1 -L2 -[ #J #K2 #V2 #H destruct -| #I #K1 #K2 #V1 #V2 #HK12 #HV12 #J #K #W #H destruct /2 width=5 by ex3_2_intro/ -] -qed-. - -lemma lpx_sn_inv_pair2: ∀R,I,L1,K2,V2. lpx_sn R L1 (K2. ⓑ{I} V2) → - ∃∃K1,V1. lpx_sn R K1 K2 & R K1 V1 V2 & L1 = K1. ⓑ{I} V1. -/2 width=3 by lpx_sn_inv_pair2_aux/ qed-. - -lemma lpx_sn_inv_pair: ∀R,I1,I2,L1,L2,V1,V2. - lpx_sn R (L1.ⓑ{I1}V1) (L2.ⓑ{I2}V2) → - ∧∧ lpx_sn R L1 L2 & R L1 V1 V2 & I1 = I2. -#R #I1 #I2 #L1 #L2 #V1 #V2 #H elim (lpx_sn_inv_pair1 … H) -H -#L0 #V0 #HL10 #HV10 #H destruct /2 width=1 by and3_intro/ -qed-. - -(* Basic forward lemmas *****************************************************) - -lemma lpx_sn_fwd_length: ∀R,L1,L2. lpx_sn R L1 L2 → |L1| = |L2|. -#R #L1 #L2 #H elim H -L1 -L2 normalize // -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/grammar/lpx_sn_lpx_sn.ma b/matita/matita/contribs/lambdadelta/basic_2/grammar/lpx_sn_lpx_sn.ma deleted file mode 100644 index 69c010a19..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/grammar/lpx_sn_lpx_sn.ma +++ /dev/null @@ -1,48 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||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/grammar/lpx_sn.ma". - -(* SN POINTWISE EXTENSION OF A CONTEXT-SENSITIVE REALTION FOR TERMS *********) - -definition lpx_sn_confluent: relation (lenv→relation term) ≝ λR1,R2. - ∀L0,T0,T1. R1 L0 T0 T1 → ∀T2. R2 L0 T0 T2 → - ∀L1. lpx_sn R1 L0 L1 → ∀L2. lpx_sn R2 L0 L2 → - ∃∃T. R2 L1 T1 T & R1 L2 T2 T. - -definition lpx_sn_transitive: relation (lenv→relation term) ≝ λR1,R2. - ∀L1,T1,T. R1 L1 T1 T → ∀L2. lpx_sn R1 L1 L2 → - ∀T2. R2 L2 T T2 → R1 L1 T1 T2. - -(* Main properties **********************************************************) - -theorem lpx_sn_trans: ∀R. lpx_sn_transitive R R → Transitive … (lpx_sn R). -#R #HR #L1 #L #H elim H -L1 -L // -#I #L1 #L #V1 #V #HL1 #HV1 #IHL1 #X #H -elim (lpx_sn_inv_pair1 … H) -H #L2 #V2 #HL2 #HV2 #H destruct /3 width=5/ -qed-. - -theorem lpx_sn_conf: ∀R1,R2. lpx_sn_confluent R1 R2 → - confluent2 … (lpx_sn R1) (lpx_sn R2). -#R1 #R2 #HR12 #L0 @(f_ind … length … L0) -L0 #n #IH * -[ #_ #X1 #H1 #X2 #H2 -n - >(lpx_sn_inv_atom1 … H1) -X1 - >(lpx_sn_inv_atom1 … H2) -X2 /2 width=3/ -| #L0 #I #V0 #Hn #X1 #H1 #X2 #H2 destruct - elim (lpx_sn_inv_pair1 … H1) -H1 #L1 #V1 #HL01 #HV01 #H destruct - elim (lpx_sn_inv_pair1 … H2) -H2 #L2 #V2 #HL02 #HV02 #H destruct - elim (IH … HL01 … HL02) -IH normalize // #L #HL1 #HL2 - elim (HR12 … HV01 … HV02 … HL01 … HL02) -L0 -V0 /3 width=5/ -] -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/grammar/lpx_sn_tc.ma b/matita/matita/contribs/lambdadelta/basic_2/grammar/lpx_sn_tc.ma deleted file mode 100644 index 2919d9d10..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/grammar/lpx_sn_tc.ma +++ /dev/null @@ -1,119 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||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/grammar/lpx_sn.ma". - -(* SN POINTWISE EXTENSION OF A CONTEXT-SENSITIVE REALTION FOR TERMS *********) - -(* Properties on transitive_closure *****************************************) - -lemma TC_lpx_sn_pair_refl: ∀R. (∀L. reflexive … (R L)) → - ∀L1,L2. TC … (lpx_sn R) L1 L2 → - ∀I,V. TC … (lpx_sn R) (L1. ⓑ{I} V) (L2. ⓑ{I} V). -#R #HR #L1 #L2 #H @(TC_star_ind … L2 H) -L2 -[ /2 width=1 by lpx_sn_refl/ -| /3 width=1 by TC_reflexive, lpx_sn_refl/ -| /3 width=5 by lpx_sn_pair, step/ -] -qed-. - -lemma TC_lpx_sn_pair: ∀R. (∀L. reflexive … (R L)) → - ∀I,L1,L2. TC … (lpx_sn R) L1 L2 → - ∀V1,V2. LTC … R L1 V1 V2 → - TC … (lpx_sn R) (L1. ⓑ{I} V1) (L2. ⓑ{I} V2). -#R #HR #I #L1 #L2 #HL12 #V1 #V2 #H @(TC_star_ind_dx … V1 H) -V1 // -[ /2 width=1 by TC_lpx_sn_pair_refl/ -| /4 width=3 by TC_strap, lpx_sn_pair, lpx_sn_refl/ -] -qed-. - -lemma lpx_sn_LTC_TC_lpx_sn: ∀R. (∀L. reflexive … (R L)) → - ∀L1,L2. lpx_sn (LTC … R) L1 L2 → - TC … (lpx_sn R) L1 L2. -#R #HR #L1 #L2 #H elim H -L1 -L2 -/2 width=1 by TC_lpx_sn_pair, lpx_sn_atom, inj/ -qed-. - -(* Inversion lemmas on transitive closure ***********************************) - -lemma TC_lpx_sn_inv_atom2: ∀R,L1. TC … (lpx_sn R) L1 (⋆) → L1 = ⋆. -#R #L1 #H @(TC_ind_dx … L1 H) -L1 -[ /2 width=2 by lpx_sn_inv_atom2/ -| #L1 #L #HL1 #_ #IHL2 destruct /2 width=2 by lpx_sn_inv_atom2/ -] -qed-. - -lemma TC_lpx_sn_inv_pair2: ∀R. s_rs_trans … R (lpx_sn R) → - ∀I,L1,K2,V2. TC … (lpx_sn R) L1 (K2.ⓑ{I}V2) → - ∃∃K1,V1. TC … (lpx_sn R) K1 K2 & LTC … R K1 V1 V2 & L1 = K1. ⓑ{I} V1. -#R #HR #I #L1 #K2 #V2 #H @(TC_ind_dx … L1 H) -L1 -[ #L1 #H elim (lpx_sn_inv_pair2 … H) -H /3 width=5 by inj, ex3_2_intro/ -| #L1 #L #HL1 #_ * #K #V #HK2 #HV2 #H destruct - elim (lpx_sn_inv_pair2 … HL1) -HL1 #K1 #V1 #HK1 #HV1 #H destruct - lapply (HR … HV2 … HK1) -HR -HV2 /3 width=5 by TC_strap, ex3_2_intro/ -] -qed-. - -lemma TC_lpx_sn_ind: ∀R. s_rs_trans … R (lpx_sn R) → - ∀S:relation lenv. - S (⋆) (⋆) → ( - ∀I,K1,K2,V1,V2. - TC … (lpx_sn R) K1 K2 → LTC … R K1 V1 V2 → - S K1 K2 → S (K1.ⓑ{I}V1) (K2.ⓑ{I}V2) - ) → - ∀L2,L1. TC … (lpx_sn R) L1 L2 → S L1 L2. -#R #HR #S #IH1 #IH2 #L2 elim L2 -L2 -[ #X #H >(TC_lpx_sn_inv_atom2 … H) -X // -| #L2 #I #V2 #IHL2 #X #H - elim (TC_lpx_sn_inv_pair2 … H) // -H -HR - #L1 #V1 #HL12 #HV12 #H destruct /3 width=1 by/ -] -qed-. - -lemma TC_lpx_sn_inv_atom1: ∀R,L2. TC … (lpx_sn R) (⋆) L2 → L2 = ⋆. -#R #L2 #H elim H -L2 -[ /2 width=2 by lpx_sn_inv_atom1/ -| #L #L2 #_ #HL2 #IHL1 destruct /2 width=2 by lpx_sn_inv_atom1/ -] -qed-. - -fact TC_lpx_sn_inv_pair1_aux: ∀R. s_rs_trans … R (lpx_sn R) → - ∀L1,L2. TC … (lpx_sn R) L1 L2 → - ∀I,K1,V1. L1 = K1.ⓑ{I}V1 → - ∃∃K2,V2. TC … (lpx_sn R) K1 K2 & LTC … R K1 V1 V2 & L2 = K2. ⓑ{I} V2. -#R #HR #L1 #L2 #H @(TC_lpx_sn_ind … H) // -HR -L1 -L2 -[ #J #K #W #H destruct -| #I #L1 #L2 #V1 #V2 #HL12 #HV12 #_ #J #K #W #H destruct /2 width=5 by ex3_2_intro/ -] -qed-. - -lemma TC_lpx_sn_inv_pair1: ∀R. s_rs_trans … R (lpx_sn R) → - ∀I,K1,L2,V1. TC … (lpx_sn R) (K1.ⓑ{I}V1) L2 → - ∃∃K2,V2. TC … (lpx_sn R) K1 K2 & LTC … R K1 V1 V2 & L2 = K2. ⓑ{I} V2. -/2 width=3 by TC_lpx_sn_inv_pair1_aux/ qed-. - -lemma TC_lpx_sn_inv_lpx_sn_LTC: ∀R. s_rs_trans … R (lpx_sn R) → - ∀L1,L2. TC … (lpx_sn R) L1 L2 → - lpx_sn (LTC … R) L1 L2. -/3 width=4 by TC_lpx_sn_ind, lpx_sn_pair/ qed-. - -(* Forward lemmas on transitive closure *************************************) - -lemma TC_lpx_sn_fwd_length: ∀R,L1,L2. TC … (lpx_sn R) L1 L2 → |L1| = |L2|. -#R #L1 #L2 #H elim H -L2 -[ #L2 #HL12 >(lpx_sn_fwd_length … HL12) -HL12 // -| #L #L2 #_ #HL2 #IHL1 - >IHL1 -L1 >(lpx_sn_fwd_length … HL2) -HL2 // -] -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazypredsnstar_5.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazypredsnstar_5.ma new file mode 100644 index 000000000..824933fba --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazypredsnstar_5.ma @@ -0,0 +1,19 @@ +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) + +(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) + +notation "hvbox( ⦃ term 46 G , break term 46 L1 ⦄ ⊢ ➡* break [ term 46 T , break term 46 d ] break term 46 L2 )" + non associative with precedence 45 + for @{ 'LazyPRedSnStar $G $L1 $L2 $T $d }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazypredsnstar_7.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazypredsnstar_7.ma new file mode 100644 index 000000000..f8209e2f8 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazypredsnstar_7.ma @@ -0,0 +1,19 @@ +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) + +(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) + +notation "hvbox( ⦃ term 46 G , break term 46 L1 ⦄ ⊢ ➡* break [ term 46 h , break term 46 g , break term 46 T , break term 46 d ] break term 46 L2 )" + non associative with precedence 45 + for @{ 'LazyPRedSnStar $G $L1 $L2 $h $g $T $d }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predsn_3.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predsn_3.ma deleted file mode 100644 index d06064a29..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predsn_3.ma +++ /dev/null @@ -1,19 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||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 *) -(* *) -(**************************************************************************) - -(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) - -notation "hvbox( ⦃ term 46 G , break term 46 L1 ⦄ ⊢ ➡ break term 46 L2 )" - non associative with precedence 45 - for @{ 'PRedSn $G $L1 $L2 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predsn_5.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predsn_5.ma deleted file mode 100644 index 206566071..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predsn_5.ma +++ /dev/null @@ -1,19 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||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 *) -(* *) -(**************************************************************************) - -(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) - -notation "hvbox( ⦃ term 46 G, break term 46 L1 ⦄ ⊢ ➡ break [ term 46 h , break term 46 g ] break term 46 L2 )" - non associative with precedence 45 - for @{ 'PRedSn $h $g $G $L1 $L2 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predsnstar_3.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predsnstar_3.ma deleted file mode 100644 index 2bcf32665..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predsnstar_3.ma +++ /dev/null @@ -1,19 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||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 *) -(* *) -(**************************************************************************) - -(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) - -notation "hvbox( ⦃ term 46 G , break term 46 L1 ⦄ ⊢ ➡* break term 46 L2 )" - non associative with precedence 45 - for @{ 'PRedSnStar $G $L1 $L2 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predsnstar_5.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predsnstar_5.ma deleted file mode 100644 index aef4f2707..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predsnstar_5.ma +++ /dev/null @@ -1,19 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||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 *) -(* *) -(**************************************************************************) - -(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) - -notation "hvbox( ⦃ term 46 G, break term 46 L1 ⦄ ⊢ ➡ * break [ term 46 h , break term 46 g ] break term 46 L2 )" - non associative with precedence 45 - for @{ 'PRedSnStar $h $g $G $L1 $L2 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predsnstaralt_3.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predsnstaralt_3.ma deleted file mode 100644 index 45328fbaf..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predsnstaralt_3.ma +++ /dev/null @@ -1,19 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||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 *) -(* *) -(**************************************************************************) - -(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) - -notation "hvbox( ⦃ term 46 G , break term 46 L1 ⦄ ⊢ ➡ ➡ * break term 46 L2 )" - non associative with precedence 45 - for @{ 'PRedSnStarAlt $G $L1 $L2 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predsnstaralt_5.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predsnstaralt_5.ma deleted file mode 100644 index 9682647cd..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predsnstaralt_5.ma +++ /dev/null @@ -1,19 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||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 *) -(* *) -(**************************************************************************) - -(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) - -notation "hvbox( ⦃ term 46 G, break term 46 L1 ⦄ ⊢ ➡ ➡ * break [ term 46 h , break term 46 g ] break term 46 L2 )" - non associative with precedence 45 - for @{ 'PRedSnStarAlt $h $g $G $L1 $L2 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cpr_llpx_sn.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/cpr_llpx_sn.ma new file mode 100644 index 000000000..ba2210f69 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/cpr_llpx_sn.ma @@ -0,0 +1,47 @@ +(**************************************************************************) +(* ___ *) +(* ||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/relocation/llpx_sn_ldrop.ma". +include "basic_2/reduction/cpr.ma". + +(* CONTEXT-SENSITIVE PARALLEL REDUCTION FOR TERMS ***************************) + +(* Properties on lazy sn pointwise extensions *******************************) + +lemma llpx_sn_cpr_conf: ∀R. (∀L. reflexive … (R L)) → l_liftable R → l_deliftable_sn R → + ∀G. s_r_confluent1 … (cpr G) (llpx_sn R 0). +#R #H1R #H2R #H3R #G #Ls #T1 #T2 #H elim H -G -Ls -T1 -T2 +[ // +| #G #Ls #Ks #V1s #V2s #W2s #i #HLKs #_ #HVW2s #IHV12s #Ld #H elim (llpx_sn_inv_lref_ge_sn … H … HLKs) // -H + #Kd #V1d #HLKd #HV1s #HV1sd + lapply (ldrop_fwd_drop2 … HLKs) -HLKs #HLKs + lapply (ldrop_fwd_drop2 … HLKd) -HLKd #HLKd + @(llpx_sn_lift_le … HLKs HLKd … HVW2s) -HLKs -HLKd -HVW2s /2 width=1 by/ (**) (* full auto too slow *) +| #a #I #G #Ls #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #Ld #H elim (llpx_sn_inv_bind_O … H) -H + /4 width=5 by llpx_sn_bind_repl_SO, llpx_sn_bind/ +| #I #G #Ls #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #Ld #H elim (llpx_sn_inv_flat … H) -H + /3 width=1 by llpx_sn_flat/ +| #G #Ls #V #T1 #T2 #T #_ #HT2 #IHT12 #Ld #H elim (llpx_sn_inv_bind_O … H) -H + /3 width=10 by llpx_sn_inv_lift_le, ldrop_drop/ +| #G #Ls #V #T1 #T2 #_ #IHT12 #Ld #H elim (llpx_sn_inv_flat … H) -H /2 width=1 by/ +| #a #G #Ls #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #IHV12 #IHW12 #IHT12 #Ld #H elim (llpx_sn_inv_flat … H) -H + #HV1 #H elim (llpx_sn_inv_bind_O … H) -H + /4 width=5 by llpx_sn_bind_repl_SO, llpx_sn_flat, llpx_sn_bind/ +| #a #G #Ls #V1 #V2 #V #W1 #W2 #T1 #T2 #_ #HV2 #_ #_ #IHV12 #IHW12 #IHT12 #Ld #H elim (llpx_sn_inv_flat … H) -H + #HV1 #H elim (llpx_sn_inv_bind_O … H) -H // + #HW1 #HT1 @llpx_sn_bind_O /2 width=1 by/ @llpx_sn_flat (**) (* full auto too slow *) + [ /3 width=10 by llpx_sn_lift_le, ldrop_drop/ + | /3 width=4 by llpx_sn_bind_repl_O/ +] +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_lleq.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_lleq.ma index d2703ad7c..77dce4631 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_lleq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_lleq.ma @@ -43,8 +43,7 @@ lemma lleq_cpx_trans: ∀h,g,G,L2,T1,T2. ⦃G, L2⦄ ⊢ T1 ➡[h, g] T2 → ] qed-. -lemma lleq_cpx_conf_sn: ∀h,g,G,L1,T1,T2. ⦃G, L1⦄ ⊢ T1 ➡[h, g] T2 → - ∀L2. L1 ⋕[T1, 0] L2 → L1 ⋕[T2, 0] L2. +lemma lleq_cpx_conf_sn: ∀h,g,G. s_r_confluent1 … (cpx h g G) (lleq 0). /3 width=6 by llpx_sn_cpx_conf, lift_mono, ex2_intro/ qed-. lemma lleq_cpx_conf_dx: ∀h,g,G,L2,T1,T2. ⦃G, L2⦄ ⊢ T1 ➡[h, g] T2 → diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_llpx_sn.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_llpx_sn.ma index 38a83a760..36a97fc62 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_llpx_sn.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_llpx_sn.ma @@ -21,8 +21,7 @@ include "basic_2/reduction/cpx.ma". (* Note: lemma 1000 *) lemma llpx_sn_cpx_conf: ∀R. (∀L. reflexive … (R L)) → l_liftable R → l_deliftable_sn R → - ∀h,g,G,Ls,T1,T2. ⦃G, Ls⦄ ⊢ T1 ➡[h, g] T2 → - ∀Ld. llpx_sn R 0 T1 Ls Ld → llpx_sn R 0 T2 Ls Ld. + ∀h,g,G. s_r_confluent1 … (cpx h g G) (llpx_sn R 0). #R #H1R #H2R #H3R #h #g #G #Ls #T1 #T2 #H elim H -G -Ls -T1 -T2 [ // | /3 width=4 by llpx_sn_fwd_length, llpx_sn_sort/ diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/fpb.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/fpb.ma index 94c114260..7c65dcfa9 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/reduction/fpb.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/fpb.ma @@ -13,15 +13,15 @@ (**************************************************************************) include "basic_2/notation/relations/btpred_8.ma". -include "basic_2/relocation/fquq_alt.ma". -include "basic_2/reduction/lpx.ma". +include "basic_2/relocation/fquq.ma". +include "basic_2/reduction/llpx.ma". (* "BIG TREE" PARALLEL REDUCTION FOR CLOSURES *******************************) inductive fpb (h) (g) (G1) (L1) (T1): relation3 genv lenv term ≝ | fpb_fquq: ∀G2,L2,T2. ⦃G1, L1, T1⦄ ⊃⸮ ⦃G2, L2, T2⦄ → fpb h g G1 L1 T1 G2 L2 T2 | fpb_cpx : ∀T2. ⦃G1, L1⦄ ⊢ T1 ➡[h, g] T2 → fpb h g G1 L1 T1 G1 L1 T2 -| fpb_lpx : ∀L2. ⦃G1, L1⦄ ⊢ ➡[h, g] L2 → fpb h g G1 L1 T1 G1 L2 T1 +| fpb_lpx : ∀L2. ⦃G1, L1⦄ ⊢ ➡[h, g, T1, 0] L2 → fpb h g G1 L1 T1 G1 L2 T1 . interpretation @@ -36,5 +36,5 @@ lemma fpb_refl: ∀h,g. tri_reflexive … (fpb h g). lemma cpr_fpb: ∀h,g,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡ T2 → ⦃G, L, T1⦄ ≽[h, g] ⦃G, L, T2⦄. /3 width=1 by fpb_cpx, cpr_cpx/ qed. -lemma lpr_fpb: ∀h,g,G,L1,L2,T. ⦃G, L1⦄ ⊢ ➡ L2 → ⦃G, L1, T⦄ ≽[h, g] ⦃G, L2, T⦄. -/3 width=1 by fpb_lpx, lpr_lpx/ qed. +lemma lpr_fpb: ∀h,g,G,L1,L2,T. ⦃G, L1⦄ ⊢ ➡[T, 0] L2 → ⦃G, L1, T⦄ ≽[h, g] ⦃G, L2, T⦄. +/3 width=1 by fpb_lpx, llpr_llpx/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/fpb_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/fpb_aaa.ma index d61a11ae0..158b6b1d6 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/reduction/fpb_aaa.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/fpb_aaa.ma @@ -13,7 +13,7 @@ (**************************************************************************) include "basic_2/static/aaa_fqus.ma". -include "basic_2/reduction/lpx_aaa.ma". +include "basic_2/reduction/llpx_aaa.ma". include "basic_2/reduction/fpb.ma". (* "BIG TREE" PARALLEL REDUCTION FOR CLOSURES *******************************) @@ -23,5 +23,5 @@ include "basic_2/reduction/fpb.ma". lemma aaa_fpb_conf: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ≽[h, g] ⦃G2, L2, T2⦄ → ∀A1. ⦃G1, L1⦄ ⊢ T1 ⁝ A1 → ∃A2. ⦃G2, L2⦄ ⊢ T2 ⁝ A2. #h #g #G1 #G2 #L1 #L2 #T1 #T2 * -G2 -L2 -T2 -/3 width=6 by aaa_lpx_conf, aaa_cpx_conf, aaa_fquq_conf, ex_intro/ +/3 width=6 by aaa_llpx_conf, aaa_cpx_conf, aaa_fquq_conf, ex_intro/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/llpr_ldrop.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/llpr_ldrop.ma index a19534b4a..0ca90bae4 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/reduction/llpr_ldrop.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/llpr_ldrop.ma @@ -12,9 +12,9 @@ (* *) (**************************************************************************) -include "basic_2/relocation/llpx_sn_ldrop.ma". include "basic_2/relocation/fquq_alt.ma". include "basic_2/reduction/cpr_lift.ma". +include "basic_2/reduction/cpr_llpx_sn.ma". include "basic_2/reduction/llpr.ma". (* LAZY SN PARALLEL REDUCTION FOR LOCAL ENVIRONMENTS ************************) @@ -47,6 +47,11 @@ lemma llpr_bind_repl_O: ∀I,G,L1,L2,V1,V2,T. ⦃G, L1.ⓑ{I}V1⦄ ⊢ ➡[T, 0] ∀J,W1,W2. ⦃G, L1⦄ ⊢ ➡[W1, 0] L2 → ⦃G, L1⦄ ⊢ W1 ➡ W2 → ⦃G, L1.ⓑ{J}W1⦄ ⊢ ➡[T, 0] L2.ⓑ{J}W2. /2 width=4 by llpx_sn_bind_repl_O/ qed-. +(* Advanced properties ******************************************************) + +lemma llpr_cpr_conf: ∀G. s_r_confluent1 … (cpr G) (llpr G 0). +/3 width=10 by llpx_sn_cpr_conf, cpr_inv_lift1, cpr_lift/ qed-. + (* Properties on context-sensitive parallel reduction for terms *************) lemma fqu_cpr_trans_dx: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃ ⦃G2, L2, T2⦄ → diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/llpr_llpr.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/llpr_llpr.ma index 925765be8..4e5b9e2be 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/reduction/llpr_llpr.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/llpr_llpr.ma @@ -300,7 +300,7 @@ lapply (cpr_lift … HV2 (L2.ⓓW2) … HVU2 … HVU) -HVU2 /2 width=2 by ldrop_ /4 width=7 by cpr_bind, cpr_flat, ex2_intro/ (**) (* full auto not tried *) qed-. -theorem cpr_conf_llpr: ∀G. llpx_sn_confluent (cpr G) (cpr G). +theorem cpr_conf_llpr: ∀G. llpx_sn_confluent2 (cpr G) (cpr G). #G #L0 #T0 @(fqup_wf_ind_eq … G L0 T0) -G -L0 -T0 #G #L #T #IH #G0 #L0 * [| * ] [ #I0 #HG #HL #HT #T1 #H1 #T2 #H2 #L1 #HL01 #L2 #HL02 destruct elim (cpr_inv_atom1 … H1) -H1 diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/llpx_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/llpx_aaa.ma new file mode 100644 index 000000000..7c0949133 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/llpx_aaa.ma @@ -0,0 +1,81 @@ +(**************************************************************************) +(* ___ *) +(* ||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/static/aaa_lift.ma". +include "basic_2/static/lsuba_aaa.ma". +include "basic_2/reduction/llpx_ldrop.ma". + +(* SN EXTENDED PARALLEL REDUCTION FOR LOCAL ENVIRONMENTS ********************) + +(* Properties on atomic arity assignment for terms **************************) + +(* Note: lemma 500 *) +lemma aaa_cpx_llpx_conf: ∀h,g,G,L1,T1,A. ⦃G, L1⦄ ⊢ T1 ⁝ A → + ∀T2. ⦃G, L1⦄ ⊢ T1 ➡[h, g] T2 → + ∀L2. ⦃G, L1⦄ ⊢ ➡[h, g, T1, 0] L2 → ⦃G, L2⦄ ⊢ T2 ⁝ A. +#h #g #G #L1 #T1 #A #H elim H -G -L1 -T1 -A +[ #g #L1 #k #X #H elim (cpx_inv_sort1 … H) -H // * // +| #I #G #L1 #K1 #V1 #B #i #HLK1 #_ #IHV1 #X #H #L2 #HL12 + elim (cpx_inv_lref1 … H) -H + [ #H destruct + elim (llpx_inv_lref_ge_sn … HL12 … HLK1) -L1 /3 width=6 by aaa_lref/ + | * #J #Y #Z #V2 #H #HV12 #HV2 + lapply (ldrop_mono … H … HLK1) -H #H destruct + elim (llpx_inv_lref_ge_sn … HL12 … HLK1) -L1 /3 width=8 by aaa_lift, ldrop_fwd_drop2/ + ] +| #a #G #L1 #V1 #T1 #B #A #_ #_ #IHV1 #IHT1 #X #H #L2 #HL12 + elim (llpx_inv_bind_O … HL12) -HL12 #HV1 #HT1 + elim (cpx_inv_abbr1 … H) -H * + [ #V2 #T2 #HV12 #HT12 #H destruct /4 width=4 by llpx_bind_repl_O, aaa_abbr/ + | #T2 #HT12 #HT2 #H destruct -IHV1 /3 width=8 by aaa_inv_lift, ldrop_drop/ + ] +| #a #G #L1 #V1 #T1 #B #A #_ #_ #IHV1 #IHT1 #X #H #L2 #HL12 + elim (llpx_inv_bind_O … HL12) -HL12 #HV1 #HT1 + elim (cpx_inv_abst1 … H) -H #V2 #T2 #HV12 #HT12 #H destruct + /4 width=4 by llpx_bind_repl_O, aaa_abst/ +| #G #L1 #V1 #T1 #B #A #_ #_ #IHV1 #IHT1 #X #H #L2 #HL12 + elim (llpx_inv_flat … HL12) -HL12 #HV1 #HT1 + elim (cpx_inv_appl1 … H) -H * + [ #V2 #T2 #HV12 #HT12 #H destruct /3 width=3 by aaa_appl/ + | #b #V2 #W1 #W2 #U1 #U2 #HV12 #HW12 #HU12 #H1 #H2 destruct + lapply (IHV1 … HV12 … HV1) -IHV1 -HV12 #HV2 + lapply (IHT1 (ⓛ{b}W2.U2) … HT1) -IHT1 /2 width=1 by cpx_bind/ -L1 #H + elim (aaa_inv_abst … H) -H #B0 #A0 #HW1 #HU2 #H destruct + /5 width=6 by lsuba_aaa_trans, lsuba_abbr, aaa_abbr, aaa_cast/ + | #b #V #V2 #W1 #W2 #U1 #U2 #HV1 #HV2 #HW12 #HU12 #H1 #H2 destruct + lapply (aaa_lift G L2 … B … (L2.ⓓW2) … HV2) -HV2 /2 width=2 by ldrop_drop/ #HV2 + lapply (IHT1 (ⓓ{b}W2.U2) … HT1) -IHT1 /2 width=1 by cpx_bind/ -L1 #H + elim (aaa_inv_abbr … H) -H /3 width=3 by aaa_abbr, aaa_appl/ + ] +| #G #L1 #V1 #T1 #A #_ #_ #IHV1 #IHT1 #X #H #L2 #HL12 + elim (llpx_inv_flat … HL12) -HL12 #HV1 #HT1 + elim (cpx_inv_cast1 … H) -H + [ * #V2 #T2 #HV12 #HT12 #H destruct /3 width=1 by aaa_cast/ + | -IHV1 /2 width=1 by/ + | -IHT1 /2 width=1 by/ + ] +] +qed-. + +lemma aaa_cpx_conf: ∀h,g,G,L,T1,A. ⦃G, L⦄ ⊢ T1 ⁝ A → ∀T2. ⦃G, L⦄ ⊢ T1 ➡[h, g] T2 → ⦃G, L⦄ ⊢ T2 ⁝ A. +/2 width=7 by aaa_cpx_llpx_conf/ qed-. + +lemma aaa_llpx_conf: ∀h,g,G,L1,T,A. ⦃G, L1⦄ ⊢ T ⁝ A → ∀L2. ⦃G, L1⦄ ⊢ ➡[h, g, T, 0] L2 → ⦃G, L2⦄ ⊢ T ⁝ A. +/2 width=7 by aaa_cpx_llpx_conf/ qed-. + +lemma aaa_cpr_conf: ∀G,L,T1,A. ⦃G, L⦄ ⊢ T1 ⁝ A → ∀T2. ⦃G, L⦄ ⊢ T1 ➡ T2 → ⦃G, L⦄ ⊢ T2 ⁝ A. +/3 width=5 by aaa_cpx_conf, cpr_cpx/ qed-. + +lemma aaa_llpr_conf: ∀G,L1,T,A. ⦃G, L1⦄ ⊢ T ⁝ A → ∀L2. ⦃G, L1⦄ ⊢ ➡[T, 0] L2 → ⦃G, L2⦄ ⊢ T ⁝ A. +/3 width=5 by aaa_llpx_conf, llpr_llpx/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/llpx_ldrop.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/llpx_ldrop.ma index 9b7d295d3..0b9d88b99 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/reduction/llpx_ldrop.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/llpx_ldrop.ma @@ -54,8 +54,7 @@ lemma llpx_fwd_bind_O_dx: ∀h,g,a,I,G,L1,L2,V,T. ⦃G, L1⦄ ⊢ ➡[h, g, ⓑ{ (* Advanced properties ******************************************************) -lemma llpx_cpx_conf: ∀h,g,G,L1,T1,T2. ⦃G, L1⦄ ⊢ T1 ➡[h, g] T2 → - ∀L2. ⦃G, L1⦄ ⊢ ➡[h, g, T1, 0] L2 → ⦃G, L1⦄ ⊢ ➡[h, g, T2, 0] L2. +lemma llpx_cpx_conf: ∀h,g,G. s_r_confluent1 … (cpx h g G) (llpx h g G 0). /3 width=10 by llpx_sn_cpx_conf, cpx_inv_lift1, cpx_lift/ qed-. (* Inversion lemmas on relocation *******************************************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/llpx_lleq.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/llpx_lleq.ma new file mode 100644 index 000000000..bc8619d66 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/llpx_lleq.ma @@ -0,0 +1,28 @@ +(**************************************************************************) +(* ___ *) +(* ||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/reduction/cpx_lleq.ma". +include "basic_2/reduction/llpx.ma". + +(* LAZY SN EXTENDED PARALLEL REDUCTION FOR LOCAL ENVIRONMENTS ***************) + +(* Properties on lazy equivalence for local environments ********************) + +lemma lleq_llpx_trans: ∀h,g,G,L1,L2,T,d. L1 ⋕[T, d] L2 → + ∀L.⦃G, L2⦄ ⊢ ➡[h, g, T, d] L → ⦃G, L1⦄ ⊢ ➡[h, g, T, d] L. +/3 width=3 by lleq_cpx_trans, lleq_llpx_sn_trans/ qed-. + +lemma lleq_llpx_conf: ∀h,g,G,L1,L2,T,d. L1 ⋕[T, d] L2 → + ∀L.⦃G, L1⦄ ⊢ ➡[h, g, T, d] L → ⦃G, L2⦄ ⊢ ➡[h, g, T, d] L. +/3 width=3 by lleq_cpx_trans, lleq_llpx_sn_conf/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/lpr.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/lpr.ma deleted file mode 100644 index 7636e38e6..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/reduction/lpr.ma +++ /dev/null @@ -1,61 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||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/notation/relations/predsn_3.ma". -include "basic_2/grammar/lpx_sn.ma". -include "basic_2/reduction/cpr.ma". - -(* SN PARALLEL REDUCTION FOR LOCAL ENVIRONMENTS *****************************) - -definition lpr: relation3 genv lenv lenv ≝ λG. lpx_sn (cpr G). - -interpretation "parallel reduction (local environment, sn variant)" - 'PRedSn G L1 L2 = (lpr G L1 L2). - -(* Basic inversion lemmas ***************************************************) - -(* Basic_1: includes: wcpr0_gen_sort *) -lemma lpr_inv_atom1: ∀G,L2. ⦃G, ⋆⦄ ⊢ ➡ L2 → L2 = ⋆. -/2 width=4 by lpx_sn_inv_atom1_aux/ qed-. - -(* Basic_1: includes: wcpr0_gen_head *) -lemma lpr_inv_pair1: ∀I,G,K1,V1,L2. ⦃G, K1.ⓑ{I}V1⦄ ⊢ ➡ L2 → - ∃∃K2,V2. ⦃G, K1⦄ ⊢ ➡ K2 & ⦃G, K1⦄ ⊢ V1 ➡ V2 & L2 = K2.ⓑ{I}V2. -/2 width=3 by lpx_sn_inv_pair1_aux/ qed-. - -lemma lpr_inv_atom2: ∀G,L1. ⦃G, L1⦄ ⊢ ➡ ⋆ → L1 = ⋆. -/2 width=4 by lpx_sn_inv_atom2_aux/ qed-. - -lemma lpr_inv_pair2: ∀I,G,L1,K2,V2. ⦃G, L1⦄ ⊢ ➡ K2.ⓑ{I}V2 → - ∃∃K1,V1. ⦃G, K1⦄ ⊢ ➡ K2 & ⦃G, K1⦄ ⊢ V1 ➡ V2 & L1 = K1. ⓑ{I} V1. -/2 width=3 by lpx_sn_inv_pair2_aux/ qed-. - -(* Basic properties *********************************************************) - -(* Note: lemma 250 *) -lemma lpr_refl: ∀G,L. ⦃G, L⦄ ⊢ ➡ L. -/2 width=1 by lpx_sn_refl/ qed. - -lemma lpr_pair: ∀I,G,K1,K2,V1,V2. ⦃G, K1⦄ ⊢ ➡ K2 → ⦃G, K1⦄ ⊢ V1 ➡ V2 → - ⦃G, K1.ⓑ{I}V1⦄ ⊢ ➡ K2.ⓑ{I}V2. -/2 width=1/ qed. - -(* Basic forward lemmas *****************************************************) - -lemma lpr_fwd_length: ∀G,L1,L2. ⦃G, L1⦄ ⊢ ➡ L2 → |L1| = |L2|. -/2 width=2 by lpx_sn_fwd_length/ qed-. - -(* Basic_1: removed theorems 3: wcpr0_getl wcpr0_getl_back - pr0_subst1_back -*) diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/lpr_ldrop.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/lpr_ldrop.ma deleted file mode 100644 index 4156df6ea..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/reduction/lpr_ldrop.ma +++ /dev/null @@ -1,96 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||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/relocation/fquq_alt.ma". -include "basic_2/relocation/ldrop_lpx_sn.ma". -include "basic_2/reduction/cpr_lift.ma". -include "basic_2/reduction/lpr.ma". - -(* SN PARALLEL REDUCTION FOR LOCAL ENVIRONMENTS *****************************) - -(* Properies on local environment slicing ***********************************) - -(* Basic_1: includes: wcpr0_drop *) -lemma lpr_ldrop_conf: ∀G. dropable_sn (lpr G). -/3 width=6 by lpx_sn_deliftable_dropable, cpr_inv_lift1/ qed-. - -(* Basic_1: includes: wcpr0_drop_back *) -lemma ldrop_lpr_trans: ∀G. dedropable_sn (lpr G). -/3 width=10 by lpx_sn_liftable_dedropable, cpr_lift/ qed-. - -lemma lpr_ldrop_trans_O1: ∀G. dropable_dx (lpr G). -/2 width=3 by lpx_sn_dropable/ qed-. - -(* Properties on context-sensitive parallel reduction for terms *************) - -lemma fqu_cpr_trans_dx: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃ ⦃G2, L2, T2⦄ → - ∀U2. ⦃G2, L2⦄ ⊢ T2 ➡ U2 → - ∃∃L,U1. ⦃G1, L1⦄ ⊢ ➡ L & ⦃G1, L⦄ ⊢ T1 ➡ U1 & ⦃G1, L, U1⦄ ⊃ ⦃G2, L2, U2⦄. -#G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2 -/3 width=5 by fqu_lref_O, fqu_pair_sn, fqu_bind_dx, fqu_flat_dx, lpr_pair, cpr_pair_sn, cpr_atom, cpr_bind, cpr_flat, ex3_2_intro/ -#G #L #K #U #T #e #HLK #HUT #U2 #HU2 -elim (lift_total U2 0 (e+1)) #T2 #HUT2 -lapply (cpr_lift … HU2 … HLK … HUT … HUT2) -HU2 -HUT /3 width=9 by fqu_drop, ex3_2_intro/ -qed-. - -lemma fquq_cpr_trans_dx: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃⸮ ⦃G2, L2, T2⦄ → - ∀U2. ⦃G2, L2⦄ ⊢ T2 ➡ U2 → - ∃∃L,U1. ⦃G1, L1⦄ ⊢ ➡ L & ⦃G1, L⦄ ⊢ T1 ➡ U1 & ⦃G1, L, U1⦄ ⊃⸮ ⦃G2, L2, U2⦄. -#G1 #G2 #L1 #L2 #T1 #T2 #H #U2 #HTU2 elim (fquq_inv_gen … H) -H -[ #HT12 elim (fqu_cpr_trans_dx … HT12 … HTU2) /3 width=5 by fqu_fquq, ex3_2_intro/ -| * #H1 #H2 #H3 destruct /2 width=5 by ex3_2_intro/ -] -qed-. - -lemma fqu_cpr_trans_sn: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃ ⦃G2, L2, T2⦄ → - ∀U2. ⦃G2, L2⦄ ⊢ T2 ➡ U2 → - ∃∃L,U1. ⦃G1, L1⦄ ⊢ ➡ L & ⦃G1, L1⦄ ⊢ T1 ➡ U1 & ⦃G1, L, U1⦄ ⊃ ⦃G2, L2, U2⦄. -#G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2 -/3 width=5 by fqu_lref_O, fqu_pair_sn, fqu_bind_dx, fqu_flat_dx, lpr_pair, cpr_pair_sn, cpr_atom, cpr_bind, cpr_flat, ex3_2_intro/ -#G #L #K #U #T #e #HLK #HUT #U2 #HU2 -elim (lift_total U2 0 (e+1)) #T2 #HUT2 -lapply (cpr_lift … HU2 … HLK … HUT … HUT2) -HU2 -HUT /3 width=9 by fqu_drop, ex3_2_intro/ -qed-. - -lemma fquq_cpr_trans_sn: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃⸮ ⦃G2, L2, T2⦄ → - ∀U2. ⦃G2, L2⦄ ⊢ T2 ➡ U2 → - ∃∃L,U1. ⦃G1, L1⦄ ⊢ ➡ L & ⦃G1, L1⦄ ⊢ T1 ➡ U1 & ⦃G1, L, U1⦄ ⊃⸮ ⦃G2, L2, U2⦄. -#G1 #G2 #L1 #L2 #T1 #T2 #H #U2 #HTU2 elim (fquq_inv_gen … H) -H -[ #HT12 elim (fqu_cpr_trans_sn … HT12 … HTU2) /3 width=5 by fqu_fquq, ex3_2_intro/ -| * #H1 #H2 #H3 destruct /2 width=5 by ex3_2_intro/ -] -qed-. - -lemma fqu_lpr_trans: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃ ⦃G2, L2, T2⦄ → - ∀K2. ⦃G2, L2⦄ ⊢ ➡ K2 → - ∃∃K1,T. ⦃G1, L1⦄ ⊢ ➡ K1 & ⦃G1, L1⦄ ⊢ T1 ➡ T & ⦃G1, K1, T⦄ ⊃ ⦃G2, K2, T2⦄. -#G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2 -/3 width=5 by fqu_lref_O, fqu_pair_sn, fqu_flat_dx, lpr_pair, ex3_2_intro/ -[ #a #I #G2 #L2 #V2 #T2 #X #H elim (lpr_inv_pair1 … H) -H - #K2 #W2 #HLK2 #HVW2 #H destruct - /3 width=5 by fqu_fquq, cpr_pair_sn, fqu_bind_dx, ex3_2_intro/ -| #G #L1 #K1 #T1 #U1 #e #HLK1 #HTU1 #K2 #HK12 - elim (ldrop_lpr_trans … HLK1 … HK12) -HK12 - /3 width=7 by fqu_drop, ex3_2_intro/ -] -qed-. - -lemma fquq_lpr_trans: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃⸮ ⦃G2, L2, T2⦄ → - ∀K2. ⦃G2, L2⦄ ⊢ ➡ K2 → - ∃∃K1,T. ⦃G1, L1⦄ ⊢ ➡ K1 & ⦃G1, L1⦄ ⊢ T1 ➡ T & ⦃G1, K1, T⦄ ⊃⸮ ⦃G2, K2, T2⦄. -#G1 #G2 #L1 #L2 #T1 #T2 #H #K2 #HLK2 elim (fquq_inv_gen … H) -H -[ #HT12 elim (fqu_lpr_trans … HT12 … HLK2) /3 width=5 by fqu_fquq, ex3_2_intro/ -| * #H1 #H2 #H3 destruct /2 width=5 by ex3_2_intro/ -] -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/lpr_lpr.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/lpr_lpr.ma deleted file mode 100644 index deaeff927..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/reduction/lpr_lpr.ma +++ /dev/null @@ -1,357 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||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/grammar/lpx_sn_lpx_sn.ma". -include "basic_2/substitution/fqup.ma". -include "basic_2/reduction/lpr_ldrop.ma". - -(* SN PARALLEL REDUCTION FOR LOCAL ENVIRONMENTS *****************************) - -(* Main properties on context-sensitive parallel reduction for terms ********) - -fact cpr_conf_lpr_atom_atom: - ∀I,G,L1,L2. ∃∃T. ⦃G, L1⦄ ⊢ ⓪{I} ➡ T & ⦃G, L2⦄ ⊢ ⓪{I} ➡ T. -/2 width=3 by cpr_atom, ex2_intro/ qed-. - -fact cpr_conf_lpr_atom_delta: - ∀G,L0,i. ( - ∀L,T. ⦃G, L0, #i⦄ ⊃+ ⦃G, L, T⦄ → - ∀T1. ⦃G, L⦄ ⊢ T ➡ T1 → ∀T2. ⦃G, L⦄ ⊢ T ➡ T2 → - ∀L1. ⦃G, L⦄ ⊢ ➡ L1 → ∀L2. ⦃G, L⦄ ⊢ ➡ L2 → - ∃∃T0. ⦃G, L1⦄ ⊢ T1 ➡ T0 & ⦃G, L2⦄ ⊢ T2 ➡ T0 - ) → - ∀K0,V0. ⇩[i] L0 ≡ K0.ⓓV0 → - ∀V2. ⦃G, K0⦄ ⊢ V0 ➡ V2 → ∀T2. ⇧[O, i + 1] V2 ≡ T2 → - ∀L1. ⦃G, L0⦄ ⊢ ➡ L1 → ∀L2. ⦃G, L0⦄ ⊢ ➡ L2 → - ∃∃T. ⦃G, L1⦄ ⊢ #i ➡ T & ⦃G, L2⦄ ⊢ T2 ➡ T. -#G #L0 #i #IH #K0 #V0 #HLK0 #V2 #HV02 #T2 #HVT2 #L1 #HL01 #L2 #HL02 -elim (lpr_ldrop_conf … HLK0 … HL01) -HL01 #X1 #H1 #HLK1 -elim (lpr_inv_pair1 … H1) -H1 #K1 #V1 #HK01 #HV01 #H destruct -elim (lpr_ldrop_conf … HLK0 … HL02) -HL02 #X2 #H2 #HLK2 -elim (lpr_inv_pair1 … H2) -H2 #K2 #W2 #HK02 #_ #H destruct -lapply (ldrop_fwd_drop2 … HLK2) -W2 #HLK2 -lapply (fqup_lref … G … HLK0) -HLK0 #HLK0 -elim (IH … HLK0 … HV01 … HV02 … HK01 … HK02) -L0 -K0 -V0 #V #HV1 #HV2 -elim (lift_total V 0 (i+1)) -/3 width=12 by cpr_lift, cpr_delta, ex2_intro/ -qed-. - -(* Basic_1: includes: pr0_delta_delta pr2_delta_delta *) -fact cpr_conf_lpr_delta_delta: - ∀G,L0,i. ( - ∀L,T. ⦃G, L0, #i⦄ ⊃+ ⦃G, L, T⦄ → - ∀T1. ⦃G, L⦄ ⊢ T ➡ T1 → ∀T2. ⦃G, L⦄ ⊢ T ➡ T2 → - ∀L1. ⦃G, L⦄ ⊢ ➡ L1 → ∀L2. ⦃G, L⦄ ⊢ ➡ L2 → - ∃∃T0. ⦃G, L1⦄ ⊢ T1 ➡ T0 & ⦃G, L2⦄ ⊢ T2 ➡ T0 - ) → - ∀K0,V0. ⇩[i] L0 ≡ K0.ⓓV0 → - ∀V1. ⦃G, K0⦄ ⊢ V0 ➡ V1 → ∀T1. ⇧[O, i + 1] V1 ≡ T1 → - ∀KX,VX. ⇩[i] L0 ≡ KX.ⓓVX → - ∀V2. ⦃G, KX⦄ ⊢ VX ➡ V2 → ∀T2. ⇧[O, i + 1] V2 ≡ T2 → - ∀L1. ⦃G, L0⦄ ⊢ ➡ L1 → ∀L2. ⦃G, L0⦄ ⊢ ➡ L2 → - ∃∃T. ⦃G, L1⦄ ⊢ T1 ➡ T & ⦃G, L2⦄ ⊢ T2 ➡ T. -#G #L0 #i #IH #K0 #V0 #HLK0 #V1 #HV01 #T1 #HVT1 -#KX #VX #H #V2 #HV02 #T2 #HVT2 #L1 #HL01 #L2 #HL02 -lapply (ldrop_mono … H … HLK0) -H #H destruct -elim (lpr_ldrop_conf … HLK0 … HL01) -HL01 #X1 #H1 #HLK1 -elim (lpr_inv_pair1 … H1) -H1 #K1 #W1 #HK01 #_ #H destruct -lapply (ldrop_fwd_drop2 … HLK1) -W1 #HLK1 -elim (lpr_ldrop_conf … HLK0 … HL02) -HL02 #X2 #H2 #HLK2 -elim (lpr_inv_pair1 … H2) -H2 #K2 #W2 #HK02 #_ #H destruct -lapply (ldrop_fwd_drop2 … HLK2) -W2 #HLK2 -lapply (fqup_lref … G … HLK0) -HLK0 #HLK0 -elim (IH … HLK0 … HV01 … HV02 … HK01 … HK02) -L0 -K0 -V0 #V #HV1 #HV2 -elim (lift_total V 0 (i+1)) /3 width=12 by cpr_lift, ex2_intro/ -qed-. - -fact cpr_conf_lpr_bind_bind: - ∀a,I,G,L0,V0,T0. ( - ∀L,T. ⦃G, L0, ⓑ{a,I}V0.T0⦄ ⊃+ ⦃G, L, T⦄ → - ∀T1. ⦃G, L⦄ ⊢ T ➡ T1 → ∀T2. ⦃G, L⦄ ⊢ T ➡ T2 → - ∀L1. ⦃G, L⦄ ⊢ ➡ L1 → ∀L2. ⦃G, L⦄ ⊢ ➡ L2 → - ∃∃T0. ⦃G, L1⦄ ⊢ T1 ➡ T0 & ⦃G, L2⦄ ⊢ T2 ➡ T0 - ) → - ∀V1. ⦃G, L0⦄ ⊢ V0 ➡ V1 → ∀T1. ⦃G, L0.ⓑ{I}V0⦄ ⊢ T0 ➡ T1 → - ∀V2. ⦃G, L0⦄ ⊢ V0 ➡ V2 → ∀T2. ⦃G, L0.ⓑ{I}V0⦄ ⊢ T0 ➡ T2 → - ∀L1. ⦃G, L0⦄ ⊢ ➡ L1 → ∀L2. ⦃G, L0⦄ ⊢ ➡ L2 → - ∃∃T. ⦃G, L1⦄ ⊢ ⓑ{a,I}V1.T1 ➡ T & ⦃G, L2⦄ ⊢ ⓑ{a,I}V2.T2 ➡ T. -#a #I #G #L0 #V0 #T0 #IH #V1 #HV01 #T1 #HT01 -#V2 #HV02 #T2 #HT02 #L1 #HL01 #L2 #HL02 -elim (IH … HV01 … HV02 … HL01 … HL02) // -elim (IH … HT01 … HT02 (L1.ⓑ{I}V1) … (L2.ⓑ{I}V2)) -IH -/3 width=5 by lpr_pair, cpr_bind, ex2_intro/ -qed-. - -fact cpr_conf_lpr_bind_zeta: - ∀G,L0,V0,T0. ( - ∀L,T. ⦃G, L0, +ⓓV0.T0⦄ ⊃+ ⦃G, L, T⦄ → - ∀T1. ⦃G, L⦄ ⊢ T ➡ T1 → ∀T2. ⦃G, L⦄ ⊢ T ➡ T2 → - ∀L1. ⦃G, L⦄ ⊢ ➡ L1 → ∀L2. ⦃G, L⦄ ⊢ ➡ L2 → - ∃∃T0. ⦃G, L1⦄ ⊢ T1 ➡ T0 & ⦃G, L2⦄ ⊢ T2 ➡ T0 - ) → - ∀V1. ⦃G, L0⦄ ⊢ V0 ➡ V1 → ∀T1. ⦃G, L0.ⓓV0⦄ ⊢ T0 ➡ T1 → - ∀T2. ⦃G, L0.ⓓV0⦄ ⊢ T0 ➡ T2 → ∀X2. ⇧[O, 1] X2 ≡ T2 → - ∀L1. ⦃G, L0⦄ ⊢ ➡ L1 → ∀L2. ⦃G, L0⦄ ⊢ ➡ L2 → - ∃∃T. ⦃G, L1⦄ ⊢ +ⓓV1.T1 ➡ T & ⦃G, L2⦄ ⊢ X2 ➡ T. -#G #L0 #V0 #T0 #IH #V1 #HV01 #T1 #HT01 -#T2 #HT02 #X2 #HXT2 #L1 #HL01 #L2 #HL02 -elim (IH … HT01 … HT02 (L1.ⓓV1) … (L2.ⓓV1)) -IH -HT01 -HT02 /2 width=1 by lpr_pair/ -L0 -V0 -T0 #T #HT1 #HT2 -elim (cpr_inv_lift1 … HT2 L2 … HXT2) -T2 /3 width=3 by cpr_zeta, ldrop_drop, ex2_intro/ -qed-. - -fact cpr_conf_lpr_zeta_zeta: - ∀G,L0,V0,T0. ( - ∀L,T. ⦃G, L0, +ⓓV0.T0⦄ ⊃+ ⦃G, L, T⦄ → - ∀T1. ⦃G, L⦄ ⊢ T ➡ T1 → ∀T2. ⦃G, L⦄ ⊢ T ➡ T2 → - ∀L1. ⦃G, L⦄ ⊢ ➡ L1 → ∀L2. ⦃G, L⦄ ⊢ ➡ L2 → - ∃∃T0. ⦃G, L1⦄ ⊢ T1 ➡ T0 & ⦃G, L2⦄ ⊢ T2 ➡ T0 - ) → - ∀T1. ⦃G, L0.ⓓV0⦄ ⊢ T0 ➡ T1 → ∀X1. ⇧[O, 1] X1 ≡ T1 → - ∀T2. ⦃G, L0.ⓓV0⦄ ⊢ T0 ➡ T2 → ∀X2. ⇧[O, 1] X2 ≡ T2 → - ∀L1. ⦃G, L0⦄ ⊢ ➡ L1 → ∀L2. ⦃G, L0⦄ ⊢ ➡ L2 → - ∃∃T. ⦃G, L1⦄ ⊢ X1 ➡ T & ⦃G, L2⦄ ⊢ X2 ➡ T. -#G #L0 #V0 #T0 #IH #T1 #HT01 #X1 #HXT1 -#T2 #HT02 #X2 #HXT2 #L1 #HL01 #L2 #HL02 -elim (IH … HT01 … HT02 (L1.ⓓV0) … (L2.ⓓV0)) -IH -HT01 -HT02 /2 width=1 by lpr_pair/ -L0 -T0 #T #HT1 #HT2 -elim (cpr_inv_lift1 … HT1 L1 … HXT1) -T1 /2 width=2 by ldrop_drop/ #T1 #HT1 #HXT1 -elim (cpr_inv_lift1 … HT2 L2 … HXT2) -T2 /2 width=2 by ldrop_drop/ #T2 #HT2 #HXT2 -lapply (lift_inj … HT2 … HT1) -T #H destruct /2 width=3 by ex2_intro/ -qed-. - -fact cpr_conf_lpr_flat_flat: - ∀I,G,L0,V0,T0. ( - ∀L,T. ⦃G, L0, ⓕ{I}V0.T0⦄ ⊃+ ⦃G, L, T⦄ → - ∀T1. ⦃G, L⦄ ⊢ T ➡ T1 → ∀T2. ⦃G, L⦄ ⊢ T ➡ T2 → - ∀L1. ⦃G, L⦄ ⊢ ➡ L1 → ∀L2. ⦃G, L⦄ ⊢ ➡ L2 → - ∃∃T0. ⦃G, L1⦄ ⊢ T1 ➡ T0 & ⦃G, L2⦄ ⊢ T2 ➡ T0 - ) → - ∀V1. ⦃G, L0⦄ ⊢ V0 ➡ V1 → ∀T1. ⦃G, L0⦄ ⊢ T0 ➡ T1 → - ∀V2. ⦃G, L0⦄ ⊢ V0 ➡ V2 → ∀T2. ⦃G, L0⦄ ⊢ T0 ➡ T2 → - ∀L1. ⦃G, L0⦄ ⊢ ➡ L1 → ∀L2. ⦃G, L0⦄ ⊢ ➡ L2 → - ∃∃T. ⦃G, L1⦄ ⊢ ⓕ{I}V1.T1 ➡ T & ⦃G, L2⦄ ⊢ ⓕ{I}V2.T2 ➡ T. -#I #G #L0 #V0 #T0 #IH #V1 #HV01 #T1 #HT01 -#V2 #HV02 #T2 #HT02 #L1 #HL01 #L2 #HL02 -elim (IH … HV01 … HV02 … HL01 … HL02) // -elim (IH … HT01 … HT02 … HL01 … HL02) /3 width=5 by cpr_flat, ex2_intro/ -qed-. - -fact cpr_conf_lpr_flat_tau: - ∀G,L0,V0,T0. ( - ∀L,T. ⦃G, L0, ⓝV0.T0⦄ ⊃+ ⦃G, L, T⦄ → - ∀T1. ⦃G, L⦄ ⊢ T ➡ T1 → ∀T2. ⦃G, L⦄ ⊢ T ➡ T2 → - ∀L1. ⦃G, L⦄ ⊢ ➡ L1 → ∀L2. ⦃G, L⦄ ⊢ ➡ L2 → - ∃∃T0. ⦃G, L1⦄ ⊢ T1 ➡ T0 & ⦃G, L2⦄ ⊢ T2 ➡ T0 - ) → - ∀V1,T1. ⦃G, L0⦄ ⊢ T0 ➡ T1 → ∀T2. ⦃G, L0⦄ ⊢ T0 ➡ T2 → - ∀L1. ⦃G, L0⦄ ⊢ ➡ L1 → ∀L2. ⦃G, L0⦄ ⊢ ➡ L2 → - ∃∃T. ⦃G, L1⦄ ⊢ ⓝV1.T1 ➡ T & ⦃G, L2⦄ ⊢ T2 ➡ T. -#G #L0 #V0 #T0 #IH #V1 #T1 #HT01 -#T2 #HT02 #L1 #HL01 #L2 #HL02 -elim (IH … HT01 … HT02 … HL01 … HL02) // -L0 -V0 -T0 /3 width=3 by cpr_tau, ex2_intro/ -qed-. - -fact cpr_conf_lpr_tau_tau: - ∀G,L0,V0,T0. ( - ∀L,T. ⦃G, L0, ⓝV0.T0⦄ ⊃+ ⦃G, L, T⦄ → - ∀T1. ⦃G, L⦄ ⊢ T ➡ T1 → ∀T2. ⦃G, L⦄ ⊢ T ➡ T2 → - ∀L1. ⦃G, L⦄ ⊢ ➡ L1 → ∀L2. ⦃G, L⦄ ⊢ ➡ L2 → - ∃∃T0. ⦃G, L1⦄ ⊢ T1 ➡ T0 & ⦃G, L2⦄ ⊢ T2 ➡ T0 - ) → - ∀T1. ⦃G, L0⦄ ⊢ T0 ➡ T1 → ∀T2. ⦃G, L0⦄ ⊢ T0 ➡ T2 → - ∀L1. ⦃G, L0⦄ ⊢ ➡ L1 → ∀L2. ⦃G, L0⦄ ⊢ ➡ L2 → - ∃∃T. ⦃G, L1⦄ ⊢ T1 ➡ T & ⦃G, L2⦄ ⊢ T2 ➡ T. -#G #L0 #V0 #T0 #IH #T1 #HT01 -#T2 #HT02 #L1 #HL01 #L2 #HL02 -elim (IH … HT01 … HT02 … HL01 … HL02) // -L0 -V0 -T0 /2 width=3 by ex2_intro/ -qed-. - -fact cpr_conf_lpr_flat_beta: - ∀a,G,L0,V0,W0,T0. ( - ∀L,T. ⦃G, L0, ⓐV0.ⓛ{a}W0.T0⦄ ⊃+ ⦃G, L, T⦄ → - ∀T1. ⦃G, L⦄ ⊢ T ➡ T1 → ∀T2. ⦃G, L⦄ ⊢ T ➡ T2 → - ∀L1. ⦃G, L⦄ ⊢ ➡ L1 → ∀L2. ⦃G, L⦄ ⊢ ➡ L2 → - ∃∃T0. ⦃G, L1⦄ ⊢ T1 ➡ T0 & ⦃G, L2⦄ ⊢ T2 ➡ T0 - ) → - ∀V1. ⦃G, L0⦄ ⊢ V0 ➡ V1 → ∀T1. ⦃G, L0⦄ ⊢ ⓛ{a}W0.T0 ➡ T1 → - ∀V2. ⦃G, L0⦄ ⊢ V0 ➡ V2 → ∀W2. ⦃G, L0⦄ ⊢ W0 ➡ W2 → ∀T2. ⦃G, L0.ⓛW0⦄ ⊢ T0 ➡ T2 → - ∀L1. ⦃G, L0⦄ ⊢ ➡ L1 → ∀L2. ⦃G, L0⦄ ⊢ ➡ L2 → - ∃∃T. ⦃G, L1⦄ ⊢ ⓐV1.T1 ➡ T & ⦃G, L2⦄ ⊢ ⓓ{a}ⓝW2.V2.T2 ➡ T. -#a #G #L0 #V0 #W0 #T0 #IH #V1 #HV01 #X #H -#V2 #HV02 #W2 #HW02 #T2 #HT02 #L1 #HL01 #L2 #HL02 -elim (cpr_inv_abst1 … H) -H #W1 #T1 #HW01 #HT01 #H destruct -elim (IH … HV01 … HV02 … HL01 … HL02) -HV01 -HV02 /2 width=1 by/ #V #HV1 #HV2 -elim (IH … HW01 … HW02 … HL01 … HL02) /2 width=1 by/ #W #HW1 #HW2 -elim (IH … HT01 … HT02 (L1.ⓛW1) … (L2.ⓛW2)) /2 width=1 by lpr_pair/ -L0 -V0 -W0 -T0 #T #HT1 #HT2 -lapply (lsubr_cpr_trans … HT2 (L2.ⓓⓝW2.V2) ?) -HT2 /2 width=1 by lsubr_abst/ (**) (* full auto not tried *) -/4 width=5 by cpr_bind, cpr_flat, cpr_beta, ex2_intro/ -qed-. - -(* Basic-1: includes: - pr0_cong_upsilon_refl pr0_cong_upsilon_zeta - pr0_cong_upsilon_cong pr0_cong_upsilon_delta -*) -fact cpr_conf_lpr_flat_theta: - ∀a,G,L0,V0,W0,T0. ( - ∀L,T. ⦃G, L0, ⓐV0.ⓓ{a}W0.T0⦄ ⊃+ ⦃G, L, T⦄ → - ∀T1. ⦃G, L⦄ ⊢ T ➡ T1 → ∀T2. ⦃G, L⦄ ⊢ T ➡ T2 → - ∀L1. ⦃G, L⦄ ⊢ ➡ L1 → ∀L2. ⦃G, L⦄ ⊢ ➡ L2 → - ∃∃T0. ⦃G, L1⦄ ⊢ T1 ➡ T0 & ⦃G, L2⦄ ⊢ T2 ➡ T0 - ) → - ∀V1. ⦃G, L0⦄ ⊢ V0 ➡ V1 → ∀T1. ⦃G, L0⦄ ⊢ ⓓ{a}W0.T0 ➡ T1 → - ∀V2. ⦃G, L0⦄ ⊢ V0 ➡ V2 → ∀U2. ⇧[O, 1] V2 ≡ U2 → - ∀W2. ⦃G, L0⦄ ⊢ W0 ➡ W2 → ∀T2. ⦃G, L0.ⓓW0⦄ ⊢ T0 ➡ T2 → - ∀L1. ⦃G, L0⦄ ⊢ ➡ L1 → ∀L2. ⦃G, L0⦄ ⊢ ➡ L2 → - ∃∃T. ⦃G, L1⦄ ⊢ ⓐV1.T1 ➡ T & ⦃G, L2⦄ ⊢ ⓓ{a}W2.ⓐU2.T2 ➡ T. -#a #G #L0 #V0 #W0 #T0 #IH #V1 #HV01 #X #H -#V2 #HV02 #U2 #HVU2 #W2 #HW02 #T2 #HT02 #L1 #HL01 #L2 #HL02 -elim (IH … HV01 … HV02 … HL01 … HL02) -HV01 -HV02 /2 width=1 by/ #V #HV1 #HV2 -elim (lift_total V 0 1) #U #HVU -lapply (cpr_lift … HV2 (L2.ⓓW2) … HVU2 … HVU) -HVU2 /2 width=2 by ldrop_drop/ #HU2 -elim (cpr_inv_abbr1 … H) -H * -[ #W1 #T1 #HW01 #HT01 #H destruct - elim (IH … HW01 … HW02 … HL01 … HL02) /2 width=1 by/ - elim (IH … HT01 … HT02 (L1.ⓓW1) … (L2.ⓓW2)) /2 width=1 by lpr_pair/ -L0 -V0 -W0 -T0 - /4 width=7 by cpr_bind, cpr_flat, cpr_theta, ex2_intro/ -| #T1 #HT01 #HXT1 #H destruct - elim (IH … HT01 … HT02 (L1.ⓓW2) … (L2.ⓓW2)) /2 width=1 by lpr_pair/ -L0 -V0 -W0 -T0 #T #HT1 #HT2 - elim (cpr_inv_lift1 … HT1 L1 … HXT1) -HXT1 - /4 width=9 by cpr_flat, cpr_zeta, ldrop_drop, lift_flat, ex2_intro/ -] -qed-. - -fact cpr_conf_lpr_beta_beta: - ∀a,G,L0,V0,W0,T0. ( - ∀L,T. ⦃G, L0, ⓐV0.ⓛ{a}W0.T0⦄ ⊃+ ⦃G, L, T⦄ → - ∀T1. ⦃G, L⦄ ⊢ T ➡ T1 → ∀T2. ⦃G, L⦄ ⊢ T ➡ T2 → - ∀L1. ⦃G, L⦄ ⊢ ➡ L1 → ∀L2. ⦃G, L⦄ ⊢ ➡ L2 → - ∃∃T0. ⦃G, L1⦄ ⊢ T1 ➡ T0 & ⦃G, L2⦄ ⊢ T2 ➡ T0 - ) → - ∀V1. ⦃G, L0⦄ ⊢ V0 ➡ V1 → ∀W1. ⦃G, L0⦄ ⊢ W0 ➡ W1 → ∀T1. ⦃G, L0.ⓛW0⦄ ⊢ T0 ➡ T1 → - ∀V2. ⦃G, L0⦄ ⊢ V0 ➡ V2 → ∀W2. ⦃G, L0⦄ ⊢ W0 ➡ W2 → ∀T2. ⦃G, L0.ⓛW0⦄ ⊢ T0 ➡ T2 → - ∀L1. ⦃G, L0⦄ ⊢ ➡ L1 → ∀L2. ⦃G, L0⦄ ⊢ ➡ L2 → - ∃∃T. ⦃G, L1⦄ ⊢ ⓓ{a}ⓝW1.V1.T1 ➡ T & ⦃G, L2⦄ ⊢ ⓓ{a}ⓝW2.V2.T2 ➡ T. -#a #G #L0 #V0 #W0 #T0 #IH #V1 #HV01 #W1 #HW01 #T1 #HT01 -#V2 #HV02 #W2 #HW02 #T2 #HT02 #L1 #HL01 #L2 #HL02 -elim (IH … HV01 … HV02 … HL01 … HL02) -HV01 -HV02 /2 width=1 by/ #V #HV1 #HV2 -elim (IH … HW01 … HW02 … HL01 … HL02) /2 width=1/ #W #HW1 #HW2 -elim (IH … HT01 … HT02 (L1.ⓛW1) … (L2.ⓛW2)) /2 width=1 by lpr_pair/ -L0 -V0 -W0 -T0 #T #HT1 #HT2 -lapply (lsubr_cpr_trans … HT1 (L1.ⓓⓝW1.V1) ?) -HT1 /2 width=1 by lsubr_abst/ -lapply (lsubr_cpr_trans … HT2 (L2.ⓓⓝW2.V2) ?) -HT2 /2 width=1 by lsubr_abst/ -/4 width=5 by cpr_bind, cpr_flat, ex2_intro/ (**) (* full auto not tried *) -qed-. - -(* Basic_1: was: pr0_upsilon_upsilon *) -fact cpr_conf_lpr_theta_theta: - ∀a,G,L0,V0,W0,T0. ( - ∀L,T. ⦃G, L0, ⓐV0.ⓓ{a}W0.T0⦄ ⊃+ ⦃G, L, T⦄ → - ∀T1. ⦃G, L⦄ ⊢ T ➡ T1 → ∀T2. ⦃G, L⦄ ⊢ T ➡ T2 → - ∀L1. ⦃G, L⦄ ⊢ ➡ L1 → ∀L2. ⦃G, L⦄ ⊢ ➡ L2 → - ∃∃T0. ⦃G, L1⦄ ⊢ T1 ➡ T0 & ⦃G, L2⦄ ⊢ T2 ➡ T0 - ) → - ∀V1. ⦃G, L0⦄ ⊢ V0 ➡ V1 → ∀U1. ⇧[O, 1] V1 ≡ U1 → - ∀W1. ⦃G, L0⦄ ⊢ W0 ➡ W1 → ∀T1. ⦃G, L0.ⓓW0⦄ ⊢ T0 ➡ T1 → - ∀V2. ⦃G, L0⦄ ⊢ V0 ➡ V2 → ∀U2. ⇧[O, 1] V2 ≡ U2 → - ∀W2. ⦃G, L0⦄ ⊢ W0 ➡ W2 → ∀T2. ⦃G, L0.ⓓW0⦄ ⊢ T0 ➡ T2 → - ∀L1. ⦃G, L0⦄ ⊢ ➡ L1 → ∀L2. ⦃G, L0⦄ ⊢ ➡ L2 → - ∃∃T. ⦃G, L1⦄ ⊢ ⓓ{a}W1.ⓐU1.T1 ➡ T & ⦃G, L2⦄ ⊢ ⓓ{a}W2.ⓐU2.T2 ➡ T. -#a #G #L0 #V0 #W0 #T0 #IH #V1 #HV01 #U1 #HVU1 #W1 #HW01 #T1 #HT01 -#V2 #HV02 #U2 #HVU2 #W2 #HW02 #T2 #HT02 #L1 #HL01 #L2 #HL02 -elim (IH … HV01 … HV02 … HL01 … HL02) -HV01 -HV02 /2 width=1 by/ #V #HV1 #HV2 -elim (IH … HW01 … HW02 … HL01 … HL02) /2 width=1 by/ -elim (IH … HT01 … HT02 (L1.ⓓW1) … (L2.ⓓW2)) /2 width=1 by lpr_pair/ -L0 -V0 -W0 -T0 -elim (lift_total V 0 1) #U #HVU -lapply (cpr_lift … HV1 (L1.ⓓW1) … HVU1 … HVU) -HVU1 /2 width=2 by ldrop_drop/ -lapply (cpr_lift … HV2 (L2.ⓓW2) … HVU2 … HVU) -HVU2 /2 width=2 by ldrop_drop/ -/4 width=7 by cpr_bind, cpr_flat, ex2_intro/ (**) (* full auto not tried *) -qed-. - -theorem cpr_conf_lpr: ∀G. lpx_sn_confluent (cpr G) (cpr G). -#G #L0 #T0 @(fqup_wf_ind_eq … G L0 T0) -G -L0 -T0 #G #L #T #IH #G0 #L0 * [| * ] -[ #I0 #HG #HL #HT #T1 #H1 #T2 #H2 #L1 #HL01 #L2 #HL02 destruct - elim (cpr_inv_atom1 … H1) -H1 - elim (cpr_inv_atom1 … H2) -H2 - [ #H2 #H1 destruct - /2 width=1 by cpr_conf_lpr_atom_atom/ - | * #K0 #V0 #V2 #i2 #HLK0 #HV02 #HVT2 #H2 #H1 destruct - /3 width=10 by cpr_conf_lpr_atom_delta/ - | #H2 * #K0 #V0 #V1 #i1 #HLK0 #HV01 #HVT1 #H1 destruct - /4 width=10 by ex2_commute, cpr_conf_lpr_atom_delta/ - | * #X #Y #V2 #z #H #HV02 #HVT2 #H2 - * #K0 #V0 #V1 #i #HLK0 #HV01 #HVT1 #H1 destruct - /3 width=17 by cpr_conf_lpr_delta_delta/ - ] -| #a #I #V0 #T0 #HG #HL #HT #X1 #H1 #X2 #H2 #L1 #HL01 #L2 #HL02 destruct - elim (cpr_inv_bind1 … H1) -H1 * - [ #V1 #T1 #HV01 #HT01 #H1 - | #T1 #HT01 #HXT1 #H11 #H12 - ] - elim (cpr_inv_bind1 … H2) -H2 * - [1,3: #V2 #T2 #HV02 #HT02 #H2 - |2,4: #T2 #HT02 #HXT2 #H21 #H22 - ] destruct - [ /3 width=10 by cpr_conf_lpr_bind_bind/ - | /4 width=11 by ex2_commute, cpr_conf_lpr_bind_zeta/ - | /3 width=11 by cpr_conf_lpr_bind_zeta/ - | /3 width=12 by cpr_conf_lpr_zeta_zeta/ - ] -| #I #V0 #T0 #HG #HL #HT #X1 #H1 #X2 #H2 #L1 #HL01 #L2 #HL02 destruct - elim (cpr_inv_flat1 … H1) -H1 * - [ #V1 #T1 #HV01 #HT01 #H1 - | #HX1 #H1 - | #a1 #V1 #Y1 #W1 #Z1 #T1 #HV01 #HYW1 #HZT1 #H11 #H12 #H13 - | #a1 #V1 #U1 #Y1 #W1 #Z1 #T1 #HV01 #HVU1 #HYW1 #HZT1 #H11 #H12 #H13 - ] - elim (cpr_inv_flat1 … H2) -H2 * - [1,5,9,13: #V2 #T2 #HV02 #HT02 #H2 - |2,6,10,14: #HX2 #H2 - |3,7,11,15: #a2 #V2 #Y2 #W2 #Z2 #T2 #HV02 #HYW2 #HZT2 #H21 #H22 #H23 - |4,8,12,16: #a2 #V2 #U2 #Y2 #W2 #Z2 #T2 #HV02 #HVU2 #HYW2 #HZT2 #H21 #H22 #H23 - ] destruct - [ /3 width=10 by cpr_conf_lpr_flat_flat/ - | /4 width=8 by ex2_commute, cpr_conf_lpr_flat_tau/ - | /4 width=12 by ex2_commute, cpr_conf_lpr_flat_beta/ - | /4 width=14 by ex2_commute, cpr_conf_lpr_flat_theta/ - | /3 width=8 by cpr_conf_lpr_flat_tau/ - | /3 width=7 by cpr_conf_lpr_tau_tau/ - | /3 width=12 by cpr_conf_lpr_flat_beta/ - | /3 width=13 by cpr_conf_lpr_beta_beta/ - | /3 width=14 by cpr_conf_lpr_flat_theta/ - | /3 width=17 by cpr_conf_lpr_theta_theta/ - ] -] -qed-. - -(* Basic_1: includes: pr0_confluence pr2_confluence *) -theorem cpr_conf: ∀G,L. confluent … (cpr G L). -/2 width=6 by cpr_conf_lpr/ qed-. - -(* Properties on context-sensitive parallel reduction for terms *************) - -lemma lpr_cpr_conf_dx: ∀G,L0,T0,T1. ⦃G, L0⦄ ⊢ T0 ➡ T1 → ∀L1. ⦃G, L0⦄ ⊢ ➡ L1 → - ∃∃T. ⦃G, L1⦄ ⊢ T0 ➡ T & ⦃G, L1⦄ ⊢ T1 ➡ T. -#G #L0 #T0 #T1 #HT01 #L1 #HL01 -elim (cpr_conf_lpr … HT01 T0 … HL01 … HL01) // -L0 /2 width=3 by ex2_intro/ -qed-. - -lemma lpr_cpr_conf_sn: ∀G,L0,T0,T1. ⦃G, L0⦄ ⊢ T0 ➡ T1 → ∀L1. ⦃G, L0⦄ ⊢ ➡ L1 → - ∃∃T. ⦃G, L1⦄ ⊢ T0 ➡ T & ⦃G, L0⦄ ⊢ T1 ➡ T. -#G #L0 #T0 #T1 #HT01 #L1 #HL01 -elim (cpr_conf_lpr … HT01 T0 … L0 … HL01) // -HT01 -HL01 /2 width=3 by ex2_intro/ -qed-. - -(* Main properties **********************************************************) - -theorem lpr_conf: ∀G. confluent … (lpr G). -/3 width=6 by lpx_sn_conf, cpr_conf_lpr/ -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/lpx.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/lpx.ma deleted file mode 100644 index b10b13a28..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/reduction/lpx.ma +++ /dev/null @@ -1,65 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||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/notation/relations/predsn_5.ma". -include "basic_2/reduction/lpr.ma". -include "basic_2/reduction/cpx.ma". - -(* SN EXTENDED PARALLEL REDUCTION FOR LOCAL ENVIRONMENTS ********************) - -definition lpx: ∀h. sd h → relation3 genv lenv lenv ≝ - λh,g,G. lpx_sn (cpx h g G). - -interpretation "extended parallel reduction (local environment, sn variant)" - 'PRedSn h g G L1 L2 = (lpx h g G L1 L2). - -(* Basic inversion lemmas ***************************************************) - -lemma lpx_inv_atom1: ∀h,g,G,L2. ⦃G, ⋆⦄ ⊢ ➡[h, g] L2 → L2 = ⋆. -/2 width=4 by lpx_sn_inv_atom1_aux/ qed-. - -lemma lpx_inv_pair1: ∀h,g,I,G,K1,V1,L2. ⦃G, K1.ⓑ{I}V1⦄ ⊢ ➡[h, g] L2 → - ∃∃K2,V2. ⦃G, K1⦄ ⊢ ➡[h, g] K2 & ⦃G, K1⦄ ⊢ V1 ➡[h, g] V2 & - L2 = K2. ⓑ{I} V2. -/2 width=3 by lpx_sn_inv_pair1_aux/ qed-. - -lemma lpx_inv_atom2: ∀h,g,G,L1. ⦃G, L1⦄ ⊢ ➡[h, g] ⋆ → L1 = ⋆. -/2 width=4 by lpx_sn_inv_atom2_aux/ qed-. - -lemma lpx_inv_pair2: ∀h,g,I,G,L1,K2,V2. ⦃G, L1⦄ ⊢ ➡[h, g] K2.ⓑ{I}V2 → - ∃∃K1,V1. ⦃G, K1⦄ ⊢ ➡[h, g] K2 & ⦃G, K1⦄ ⊢ V1 ➡[h, g] V2 & - L1 = K1. ⓑ{I} V1. -/2 width=3 by lpx_sn_inv_pair2_aux/ qed-. - -lemma lpx_inv_pair: ∀h,g,I1,I2,G,L1,L2,V1,V2. ⦃G, L1.ⓑ{I1}V1⦄ ⊢ ➡[h, g] L2.ⓑ{I2}V2 → - ∧∧ ⦃G, L1⦄ ⊢ ➡[h, g] L2 & ⦃G, L1⦄ ⊢ V1 ➡[h, g] V2 & I1 = I2. -/2 width=1 by lpx_sn_inv_pair/ qed-. - -(* Basic properties *********************************************************) - -lemma lpx_refl: ∀h,g,G,L. ⦃G, L⦄ ⊢ ➡[h, g] L. -/2 width=1 by lpx_sn_refl/ qed. - -lemma lpx_pair: ∀h,g,I,G,K1,K2,V1,V2. ⦃G, K1⦄ ⊢ ➡[h, g] K2 → ⦃G, K1⦄ ⊢ V1 ➡[h, g] V2 → - ⦃G, K1.ⓑ{I}V1⦄ ⊢ ➡[h, g] K2.ⓑ{I}V2. -/2 width=1 by lpx_sn_pair/ qed. - -lemma lpr_lpx: ∀h,g,G,L1,L2. ⦃G, L1⦄ ⊢ ➡ L2 → ⦃G, L1⦄ ⊢ ➡[h, g] L2. -#h #g #G #L1 #L2 #H elim H -L1 -L2 /3 width=1 by lpx_pair, cpr_cpx/ -qed. - -(* Basic forward lemmas *****************************************************) - -lemma lpx_fwd_length: ∀h,g,G,L1,L2. ⦃G, L1⦄ ⊢ ➡[h, g] L2 → |L1| = |L2|. -/2 width=2 by lpx_sn_fwd_length/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/lpx_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/lpx_aaa.ma deleted file mode 100644 index f9c2374c2..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/reduction/lpx_aaa.ma +++ /dev/null @@ -1,83 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||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/static/aaa_lift.ma". -include "basic_2/static/lsuba_aaa.ma". -include "basic_2/reduction/lpx_ldrop.ma". - -(* SN EXTENDED PARALLEL REDUCTION FOR LOCAL ENVIRONMENTS ********************) - -(* Properties on atomic arity assignment for terms **************************) - -(* Note: lemma 500 *) -lemma aaa_cpx_lpx_conf: ∀h,g,G,L1,T1,A. ⦃G, L1⦄ ⊢ T1 ⁝ A → - ∀T2. ⦃G, L1⦄ ⊢ T1 ➡[h, g] T2 → - ∀L2. ⦃G, L1⦄ ⊢ ➡[h, g] L2 → ⦃G, L2⦄ ⊢ T2 ⁝ A. -#h #g #G #L1 #T1 #A #H elim H -G -L1 -T1 -A -[ #g #L1 #k #X #H - elim (cpx_inv_sort1 … H) -H // * // -| #I #G #L1 #K1 #V1 #B #i #HLK1 #_ #IHV1 #X #H #L2 #HL12 - elim (cpx_inv_lref1 … H) -H - [ #H destruct - elim (lpx_ldrop_conf … HLK1 … HL12) -L1 #X #H #HLK2 - elim (lpx_inv_pair1 … H) -H - #K2 #V2 #HK12 #HV12 #H destruct /3 width=6 by aaa_lref/ - | * #J #Y #Z #V2 #H #HV12 #HV2 - lapply (ldrop_mono … H … HLK1) -H #H destruct - elim (lpx_ldrop_conf … HLK1 … HL12) -L1 #Z #H #HLK2 - elim (lpx_inv_pair1 … H) -H #K2 #V0 #HK12 #_ #H destruct - /3 width=8 by aaa_lift, ldrop_fwd_drop2/ - ] -| #a #G #L1 #V1 #T1 #B #A #_ #_ #IHV1 #IHT1 #X #H #L2 #HL12 - elim (cpx_inv_abbr1 … H) -H * - [ #V2 #T2 #HV12 #HT12 #H destruct /4 width=2 by lpx_pair, aaa_abbr/ - | #T2 #HT12 #HT2 #H destruct -IHV1 - /4 width=8 by lpx_pair, aaa_inv_lift, ldrop_drop/ - ] -| #a #G #L1 #V1 #T1 #B #A #_ #_ #IHV1 #IHT1 #X #H #L2 #HL12 - elim (cpx_inv_abst1 … H) -H #V2 #T2 #HV12 #HT12 #H destruct - /4 width=1 by lpx_pair, aaa_abst/ -| #G #L1 #V1 #T1 #B #A #_ #_ #IHV1 #IHT1 #X #H #L2 #HL12 - elim (cpx_inv_appl1 … H) -H * - [ #V2 #T2 #HV12 #HT12 #H destruct /3 width=3 by aaa_appl/ - | #b #V2 #W1 #W2 #U1 #U2 #HV12 #HW12 #HU12 #H1 #H2 destruct - lapply (IHV1 … HV12 … HL12) -IHV1 -HV12 #HV2 - lapply (IHT1 (ⓛ{b}W2.U2) … HL12) -IHT1 /2 width=1 by cpx_bind/ -L1 #H - elim (aaa_inv_abst … H) -H #B0 #A0 #HW1 #HU2 #H destruct - /5 width=6 by lsuba_aaa_trans, lsuba_abbr, aaa_abbr, aaa_cast/ - | #b #V #V2 #W1 #W2 #U1 #U2 #HV1 #HV2 #HW12 #HU12 #H1 #H2 destruct - lapply (aaa_lift G L2 … B … (L2.ⓓW2) … HV2) -HV2 /2 width=2 by ldrop_drop/ #HV2 - lapply (IHT1 (ⓓ{b}W2.U2) … HL12) -IHT1 /2 width=1 by cpx_bind/ -L1 #H - elim (aaa_inv_abbr … H) -H /3 width=3 by aaa_abbr, aaa_appl/ - ] -| #G #L1 #V1 #T1 #A #_ #_ #IHV1 #IHT1 #X #H #L2 #HL12 - elim (cpx_inv_cast1 … H) -H - [ * #V2 #T2 #HV12 #HT12 #H destruct /3 width=1 by aaa_cast/ - | -IHV1 /2 width=1 by/ - | -IHT1 /2 width=1 by/ - ] -] -qed-. - -lemma aaa_cpx_conf: ∀h,g,G,L,T1,A. ⦃G, L⦄ ⊢ T1 ⁝ A → ∀T2. ⦃G, L⦄ ⊢ T1 ➡[h, g] T2 → ⦃G, L⦄ ⊢ T2 ⁝ A. -/2 width=7 by aaa_cpx_lpx_conf/ qed-. - -lemma aaa_lpx_conf: ∀h,g,G,L1,T,A. ⦃G, L1⦄ ⊢ T ⁝ A → ∀L2. ⦃G, L1⦄ ⊢ ➡[h, g] L2 → ⦃G, L2⦄ ⊢ T ⁝ A. -/2 width=7 by aaa_cpx_lpx_conf/ qed-. - -lemma aaa_cpr_conf: ∀G,L,T1,A. ⦃G, L⦄ ⊢ T1 ⁝ A → ∀T2. ⦃G, L⦄ ⊢ T1 ➡ T2 → ⦃G, L⦄ ⊢ T2 ⁝ A. -/3 width=5 by aaa_cpx_conf, cpr_cpx/ qed-. - -lemma aaa_lpr_conf: ∀G,L1,T,A. ⦃G, L1⦄ ⊢ T ⁝ A → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 → ⦃G, L2⦄ ⊢ T ⁝ A. -/3 width=5 by aaa_lpx_conf, lpr_lpx/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/lpx_ldrop.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/lpx_ldrop.ma deleted file mode 100644 index 188e8d11b..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/reduction/lpx_ldrop.ma +++ /dev/null @@ -1,78 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||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/relocation/ldrop_lpx_sn.ma". -include "basic_2/reduction/cpx_lift.ma". -include "basic_2/reduction/lpx.ma". - -(* SN EXTENDED PARALLEL REDUCTION FOR LOCAL ENVIRONMENTS ********************) - -(* Properies on local environment slicing ***********************************) - -lemma lpx_ldrop_conf: ∀h,g,G. dropable_sn (lpx h g G). -/3 width=6 by lpx_sn_deliftable_dropable, cpx_inv_lift1/ qed-. - -lemma ldrop_lpx_trans: ∀h,g,G. dedropable_sn (lpx h g G). -/3 width=10 by lpx_sn_liftable_dedropable, cpx_lift/ qed-. - -lemma lpx_ldrop_trans_O1: ∀h,g,G. dropable_dx (lpx h g G). -/2 width=3 by lpx_sn_dropable/ qed-. - -(* Properties on supclosure *************************************************) - -lemma fqu_lpx_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃ ⦃G2, L2, T2⦄ → - ∀K2. ⦃G2, L2⦄ ⊢ ➡[h, g] K2 → - ∃∃K1,T. ⦃G1, L1⦄ ⊢ ➡[h, g] K1 & ⦃G1, L1⦄ ⊢ T1 ➡[h, g] T & ⦃G1, K1, T⦄ ⊃ ⦃G2, K2, T2⦄. -#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2 -/3 width=5 by fqu_lref_O, fqu_pair_sn, fqu_flat_dx, lpx_pair, ex3_2_intro/ -[ #a #I #G2 #L2 #V2 #T2 #X #H elim (lpx_inv_pair1 … H) -H - #K2 #W2 #HLK2 #HVW2 #H destruct - /3 width=5 by fqu_fquq, cpx_pair_sn, fqu_bind_dx, ex3_2_intro/ -| #G #L1 #K1 #T1 #U1 #e #HLK1 #HTU1 #K2 #HK12 - elim (ldrop_lpx_trans … HLK1 … HK12) -HK12 - /3 width=7 by fqu_drop, ex3_2_intro/ -] -qed-. - -lemma fquq_lpx_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃⸮ ⦃G2, L2, T2⦄ → - ∀K2. ⦃G2, L2⦄ ⊢ ➡[h, g] K2 → - ∃∃K1,T. ⦃G1, L1⦄ ⊢ ➡[h, g] K1 & ⦃G1, L1⦄ ⊢ T1 ➡[h, g] T & ⦃G1, K1, T⦄ ⊃⸮ ⦃G2, K2, T2⦄. -#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H #K2 #HLK2 elim (fquq_inv_gen … H) -H -[ #HT12 elim (fqu_lpx_trans … HT12 … HLK2) /3 width=5 by fqu_fquq, ex3_2_intro/ -| * #H1 #H2 #H3 destruct /2 width=5 by ex3_2_intro/ -] -qed-. - -lemma lpx_fqu_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃ ⦃G2, L2, T2⦄ → - ∀K1. ⦃G1, K1⦄ ⊢ ➡[h, g] L1 → - ∃∃K2,T. ⦃G1, K1⦄ ⊢ T1 ➡[h, g] T & ⦃G1, K1, T⦄ ⊃ ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡[h, g] L2. -#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2 -/3 width=7 by fqu_pair_sn, fqu_bind_dx, fqu_flat_dx, lpx_pair, ex3_2_intro/ -[ #I #G1 #L1 #V1 #X #H elim (lpx_inv_pair2 … H) -H - #K1 #W1 #HKL1 #HWV1 #H destruct elim (lift_total V1 0 1) - /4 width=7 by cpx_delta, fqu_drop, ldrop_drop, ex3_2_intro/ -| #G #L1 #K1 #T1 #U1 #e #HLK1 #HTU1 #L0 #HL01 - elim (lpx_ldrop_trans_O1 … HL01 … HLK1) -L1 - /3 width=5 by fqu_drop, ex3_2_intro/ -] -qed-. - -lemma lpx_fquq_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃⸮ ⦃G2, L2, T2⦄ → - ∀K1. ⦃G1, K1⦄ ⊢ ➡[h, g] L1 → - ∃∃K2,T. ⦃G1, K1⦄ ⊢ T1 ➡[h, g] T & ⦃G1, K1, T⦄ ⊃⸮ ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡[h, g] L2. -#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H #K1 #HKL1 elim (fquq_inv_gen … H) -H -[ #HT12 elim (lpx_fqu_trans … HT12 … HKL1) /3 width=5 by fqu_fquq, ex3_2_intro/ -| * #H1 #H2 #H3 destruct /2 width=5 by ex3_2_intro/ -] -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/lpx_lleq.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/lpx_lleq.ma deleted file mode 100644 index 353f810c3..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/reduction/lpx_lleq.ma +++ /dev/null @@ -1,108 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||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/relocation/lleq_ldrop.ma". -include "basic_2/reduction/lpx_ldrop.ma". - -(* SN EXTENDED PARALLEL REDUCTION FOR LOCAL ENVIRONMENTS ********************) - -(* Properties on lazy equivalence for local environments ********************) -(* -lamma pippo: ∀h,g,G,L2,K2. ⦃G, L2⦄ ⊢ ➡[h, g] K2 → ∀L1. |L1| = |L2| → - ∃∃K1. ⦃G, L1⦄ ⊢ ➡[h, g] K1 & |K1| = |K2| & - (∀T,d. L1 ⋕[T, d] L2 ↔ K1 ⋕[T, d] K2). -#h #g #G #L2 #K2 #H elim H -L2 -K2 -[ #L1 #H >(length_inv_zero_dx … H) -L1 /3 width=5 by ex3_intro, conj/ -| #I2 #L2 #K2 #V2 #W2 #_ #HVW2 #IHLK2 #Y #H - elim (length_inv_pos_dx … H) -H #I #L1 #V1 #HL12 #H destruct - elim (IHLK2 … HL12) -IHLK2 #K1 #HLK1 #HK12 #IH - elim (eq_term_dec V1 V2) #H destruct - [ @(ex3_intro … (K1.ⓑ{I}W2)) normalize /2 width=1 by / -*) -axiom lleq_lpx_trans: ∀h,g,G,L2,K2. ⦃G, L2⦄ ⊢ ➡[h, g] K2 → - ∀L1,T,d. L1 ⋕[T, d] L2 → - ∃∃K1. ⦃G, L1⦄ ⊢ ➡[h, g] K1 & K1 ⋕[T, d] K2. -(* -#h #g #G #L2 #K2 #H elim H -L2 -K2 -[ #L1 #T #d #H lapply (lleq_fwd_length … H) -H - #H >(length_inv_zero_dx … H) -L1 /2 width=3 by ex2_intro/ -| #I2 #L2 #K2 #V2 #W2 #HLK2 #HVW2 #IHLK2 #Y #T #d #HT - lapply (lleq_fwd_length … HT) #H - elim (length_inv_pos_dx … H) -H #I1 #L1 #V1 #HL12 #H destruct - elim (eq_term_dec V1 V2) #H destruct - [ @ex2_intro … -*) - -lemma lpx_lleq_fqu_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃ ⦃G2, L2, T2⦄ → - ∀K1. ⦃G1, K1⦄ ⊢ ➡[h, g] L1 → K1 ⋕[T1, 0] L1 → - ∃∃K2. ⦃G1, K1, T1⦄ ⊃ ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡[h, g] L2 & K2 ⋕[T2, 0] L2. -#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2 -[ #I #G1 #L1 #V1 #X #H1 #H2 elim (lpx_inv_pair2 … H1) -H1 - #K0 #V0 #H1KL1 #_ #H destruct - elim (lleq_inv_lref_ge_dx … H2 ? I L1 V1) -H2 // - #K1 #H #H2KL1 lapply (ldrop_inv_O2 … H) -H #H destruct - /2 width=4 by fqu_lref_O, ex3_intro/ -| * [ #a ] #I #G1 #L1 #V1 #T1 #K1 #HLK1 #H - [ elim (lleq_inv_bind … H) - | elim (lleq_inv_flat … H) - ] -H /2 width=4 by fqu_pair_sn, ex3_intro/ -| #a #I #G1 #L1 #V1 #T1 #K1 #HLK1 #H elim (lleq_inv_bind_O … H) -H - /3 width=4 by lpx_pair, fqu_bind_dx, ex3_intro/ -| #I #G1 #L1 #V1 #T1 #K1 #HLK1 #H elim (lleq_inv_flat … H) -H - /2 width=4 by fqu_flat_dx, ex3_intro/ -| #G1 #L1 #L #T1 #U1 #e #HL1 #HTU1 #K1 #H1KL1 #H2KL1 - elim (ldrop_O1_le (e+1) K1) - [ #K #HK1 lapply (lleq_inv_lift_le … H2KL1 … HK1 HL1 … HTU1 ?) -H2KL1 // - #H2KL elim (lpx_ldrop_trans_O1 … H1KL1 … HL1) -L1 - #K0 #HK10 #H1KL lapply (ldrop_mono … HK10 … HK1) -HK10 #H destruct - /3 width=4 by fqu_drop, ex3_intro/ - | lapply (ldrop_fwd_length_le2 … HL1) -L -T1 -g - lapply (lleq_fwd_length … H2KL1) // - ] -] -qed-. - -lemma lpx_lleq_fquq_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃⸮ ⦃G2, L2, T2⦄ → - ∀K1. ⦃G1, K1⦄ ⊢ ➡[h, g] L1 → K1 ⋕[T1, 0] L1 → - ∃∃K2. ⦃G1, K1, T1⦄ ⊃⸮ ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡[h, g] L2 & K2 ⋕[T2, 0] L2. -#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H #K1 #H1KL1 #H2KL1 -elim (fquq_inv_gen … H) -H -[ #H elim (lpx_lleq_fqu_trans … H … H1KL1 H2KL1) -L1 - /3 width=4 by fqu_fquq, ex3_intro/ -| * #HG #HL #HT destruct /2 width=4 by ex3_intro/ -] -qed-. - -lemma lpx_lleq_fqup_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃+ ⦃G2, L2, T2⦄ → - ∀K1. ⦃G1, K1⦄ ⊢ ➡[h, g] L1 → K1 ⋕[T1, 0] L1 → - ∃∃K2. ⦃G1, K1, T1⦄ ⊃+ ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡[h, g] L2 & K2 ⋕[T2, 0] L2. -#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H @(fqup_ind … H) -G2 -L2 -T2 -[ #G2 #L2 #T2 #H #K1 #H1KL1 #H2KL1 elim (lpx_lleq_fqu_trans … H … H1KL1 H2KL1) -L1 - /3 width=4 by fqu_fqup, ex3_intro/ -| #G #G2 #L #L2 #T #T2 #_ #HT2 #IHT1 #K1 #H1KL1 #H2KL1 elim (IHT1 … H2KL1) // -L1 - #K #HT1 #H1KL #H2KL elim (lpx_lleq_fqu_trans … HT2 … H1KL H2KL) -L - /3 width=5 by fqup_strap1, ex3_intro/ -] -qed-. - -lemma lpx_lleq_fqus_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃* ⦃G2, L2, T2⦄ → - ∀K1. ⦃G1, K1⦄ ⊢ ➡[h, g] L1 → K1 ⋕[T1, 0] L1 → - ∃∃K2. ⦃G1, K1, T1⦄ ⊃* ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡[h, g] L2 & K2 ⋕[T2, 0] L2. -#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H #K1 #H1KL1 #H2KL1 -elim (fqus_inv_gen … H) -H -[ #H elim (lpx_lleq_fqup_trans … H … H1KL1 H2KL1) -L1 - /3 width=4 by fqup_fqus, ex3_intro/ -| * #HG #HL #HT destruct /2 width=4 by ex3_intro/ -] -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop_leq.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop_leq.ma index cdca16bb5..91b20e720 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop_leq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop_leq.ma @@ -59,6 +59,17 @@ elim (leq_ldrop_trans_be … (leq_sym … HL12) … HLK1) // -L1 -Hdi -Hide /3 width=3 by leq_sym, ex2_intro/ qed-. +lemma ldrop_O1_ex: ∀K2,i,L1. |L1| = |K2| + i → + ∃∃L2. L1 ≃[0, i] L2 & ⇩[i] L2 ≡ K2. +#K2 #i @(nat_ind_plus … i) -i +[ /3 width=3 by leq_O2, ex2_intro/ +| #i #IHi #Y #Hi elim (ldrop_O1_lt Y 0) // + #I #L1 #V #H lapply (ldrop_inv_O2 … H) -H #H destruct + normalize in Hi; elim (IHi L1) -IHi + /3 width=5 by ldrop_drop, leq_pair, injective_plus_l, ex2_intro/ +] +qed-. + lemma dedropable_sn_TC: ∀R. dedropable_sn R → dedropable_sn (TC … R). #R #HR #L1 #K1 #s #d #e #HLK1 #K2 #H elim H -K2 [ #K2 #HK12 elim (HR … HLK1 … HK12) -HR -K1 @@ -70,7 +81,7 @@ qed-. (* Inversion lemmas on equivalence ******************************************) -lemma ldrop_O_inj: ∀i,L1,L2,K. ⇩[i] L1 ≡ K → ⇩[i] L2 ≡ K → L1 ≃[i, ∞] L2. +lemma ldrop_O1_inj: ∀i,L1,L2,K. ⇩[i] L1 ≡ K → ⇩[i] L2 ≡ K → L1 ≃[i, ∞] L2. #i @(nat_ind_plus … i) -i [ #L1 #L2 #K #H <(ldrop_inv_O2 … H) -K #H <(ldrop_inv_O2 … H) -L1 // | #i #IHi * [2: #L1 #I1 #V1 ] * [2,4: #L2 #I2 #V2 ] #K #HLK1 #HLK2 // diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop_lpx_sn.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop_lpx_sn.ma deleted file mode 100644 index 3dc3b2f79..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop_lpx_sn.ma +++ /dev/null @@ -1,78 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||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/grammar/lpx_sn.ma". -include "basic_2/relocation/ldrop_leq.ma". - -(* DROPPING *****************************************************************) - -(* Properties on sn pointwise extension *************************************) - -lemma lpx_sn_deliftable_dropable: ∀R. l_deliftable_sn R → dropable_sn (lpx_sn R). -#R #HR #L1 #K1 #s #d #e #H elim H -L1 -K1 -d -e -[ #d #e #He #X #H >(lpx_sn_inv_atom1 … H) -H - /4 width=3 by ldrop_atom, lpx_sn_atom, ex2_intro/ -| #I #K1 #V1 #X #H elim (lpx_sn_inv_pair1 … H) -H - #L2 #V2 #HL12 #HV12 #H destruct - /3 width=5 by ldrop_pair, lpx_sn_pair, ex2_intro/ -| #I #L1 #K1 #V1 #e #_ #IHLK1 #X #H elim (lpx_sn_inv_pair1 … H) -H - #L2 #V2 #HL12 #HV12 #H destruct - elim (IHLK1 … HL12) -L1 /3 width=3 by ldrop_drop, ex2_intro/ -| #I #L1 #K1 #V1 #W1 #d #e #HLK1 #HWV1 #IHLK1 #X #H - elim (lpx_sn_inv_pair1 … H) -H #L2 #V2 #HL12 #HV12 #H destruct - elim (HR … HV12 … HLK1 … HWV1) -V1 - elim (IHLK1 … HL12) -L1 /3 width=5 by ldrop_skip, lpx_sn_pair, ex2_intro/ -] -qed-. - -lemma lpx_sn_liftable_dedropable: ∀R. (∀L. reflexive ? (R L)) → - l_liftable R → dedropable_sn (lpx_sn R). -#R #H1R #H2R #L1 #K1 #s #d #e #H elim H -L1 -K1 -d -e -[ #d #e #He #X #H >(lpx_sn_inv_atom1 … H) -H - /4 width=4 by ldrop_atom, lpx_sn_atom, ex3_intro/ -| #I #K1 #V1 #X #H elim (lpx_sn_inv_pair1 … H) -H - #K2 #V2 #HK12 #HV12 #H destruct - lapply (lpx_sn_fwd_length … HK12) - #H @(ex3_intro … (K2.ⓑ{I}V2)) (**) (* explicit constructor *) - /3 width=1 by lpx_sn_pair, monotonic_le_plus_l/ - @leq_O2 normalize // -| #I #L1 #K1 #V1 #e #_ #IHLK1 #K2 #HK12 elim (IHLK1 … HK12) -K1 - /3 width=5 by ldrop_drop, leq_pair, lpx_sn_pair, ex3_intro/ -| #I #L1 #K1 #V1 #W1 #d #e #HLK1 #HWV1 #IHLK1 #X #H - elim (lpx_sn_inv_pair1 … H) -H #K2 #W2 #HK12 #HW12 #H destruct - elim (lift_total W2 d e) #V2 #HWV2 - lapply (H2R … HW12 … HLK1 … HWV1 … HWV2) -W1 - elim (IHLK1 … HK12) -K1 - /3 width=6 by ldrop_skip, leq_succ, lpx_sn_pair, ex3_intro/ -] -qed-. - -fact lpx_sn_dropable_aux: ∀R,L2,K2,s,d,e. ⇩[s, d, e] L2 ≡ K2 → ∀L1. lpx_sn R L1 L2 → - d = 0 → ∃∃K1. ⇩[s, 0, e] L1 ≡ K1 & lpx_sn R K1 K2. -#R #L2 #K2 #s #d #e #H elim H -L2 -K2 -d -e -[ #d #e #He #X #H >(lpx_sn_inv_atom2 … H) -H - /4 width=3 by ldrop_atom, lpx_sn_atom, ex2_intro/ -| #I #K2 #V2 #X #H elim (lpx_sn_inv_pair2 … H) -H - #K1 #V1 #HK12 #HV12 #H destruct - /3 width=5 by ldrop_pair, lpx_sn_pair, ex2_intro/ -| #I #L2 #K2 #V2 #e #_ #IHLK2 #X #H #_ elim (lpx_sn_inv_pair2 … H) -H - #L1 #V1 #HL12 #HV12 #H destruct - elim (IHLK2 … HL12) -L2 /3 width=3 by ldrop_drop, ex2_intro/ -| #I #L2 #K2 #V2 #W2 #d #e #_ #_ #_ #L1 #_ -