From: Ferruccio Guidi Date: Thu, 9 Nov 2017 16:07:21 +0000 (+0000) Subject: lfsx_drops completed X-Git-Tag: make_still_working~413 X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=c879284b576409cec07e96c1f08510d9d9ac14f3 lfsx_drops completed --- diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/drops.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/drops.ma index 7702a5a94..d469f0ac1 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/drops.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/drops.ma @@ -42,10 +42,18 @@ definition d_liftable1: predicate (relation2 lenv term) ≝ λR. ∀K,T. R K T → ∀b,f,L. ⬇*[b, f] L ≡ K → ∀U. ⬆*[f] T ≡ U → R L U. +definition d_liftable1_isuni: predicate (relation2 lenv term) ≝ + λR. ∀K,T. R K T → ∀b,f,L. ⬇*[b, f] L ≡ K → 𝐔⦃f⦄ → + ∀U. ⬆*[f] T ≡ U → R L U. + definition d_deliftable1: predicate (relation2 lenv term) ≝ λR. ∀L,U. R L U → ∀b,f,K. ⬇*[b, f] L ≡ K → ∀T. ⬆*[f] T ≡ U → R K T. +definition d_deliftable1_isuni: predicate (relation2 lenv term) ≝ + λR. ∀L,U. R L U → ∀b,f,K. ⬇*[b, f] L ≡ K → 𝐔⦃f⦄ → + ∀T. ⬆*[f] T ≡ U → R K T. + definition d_liftable2_sn: ∀C:Type[0]. ∀S:rtmap → relation C. predicate (lenv → relation C) ≝ λC,S,R. ∀K,T1,T2. R K T1 T2 → ∀b,f,L. ⬇*[b, f] L ≡ K → @@ -235,7 +243,6 @@ lemma drops_fwd_isid: ∀b,f,L1,L2. ⬇*[b, f] L1 ≡ L2 → 𝐈⦃f⦄ → L1 ] qed-. - lemma drops_after_fwd_drop2: ∀b,f2,I,X,K. ⬇*[b, f2] X ≡ K.ⓘ{I} → ∀f1,f. 𝐈⦃f1⦄ → f2 ⊚ ⫯f1 ≡ f → ⬇*[b, f] X ≡ K. #b #f2 #I #X #K #H #f1 #f #Hf1 #Hf elim (drops_fwd_drop2 … H) -H diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/drops_lexs.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/drops_lexs.ma index 2bdf99d9e..7cfbf82c0 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/drops_lexs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/drops_lexs.ma @@ -12,6 +12,7 @@ (* *) (**************************************************************************) +include "basic_2/relocation/lifts_lifts_bind.ma". include "basic_2/relocation/drops.ma". (* GENERIC SLICING FOR LOCAL ENVIRONMENTS ***********************************) @@ -40,9 +41,37 @@ lemma lexs_co_dropable_sn: ∀RN,RP. co_dropable_sn (lexs RN RP). ] qed-. +lemma lexs_liftable_co_dedropable_bi: ∀RN,RP. d_liftable2_sn … liftsb RN → d_liftable2_sn … liftsb RP → + ∀f2,L1,L2. L1 ⪤*[cfull, RP, f2] L2 → ∀f1,K1,K2. K1 ⪤*[RN, RP, f1] K2 → + ∀b,f. ⬇*[b, f] L1 ≡ K1 → ⬇*[b, f] L2 ≡ K2 → + f ~⊚ f1 ≡ f2 → L1 ⪤*[RN, RP, f2] L2. +#RN #RP #HRN #HRP #f2 #L1 #L2 #H elim H -f2 -L1 -L2 // +#g2 #I1 #I2 #L1 #L2 #HL12 #HI12 #IH #f1 #Y1 #Y2 #HK12 #b #f #HY1 #HY2 #H +[ elim (coafter_inv_xxn … H) [ |*: // ] -H #g #g1 #Hg2 #H1 #H2 destruct + elim (drops_inv_skip1 … HY1) -HY1 #J1 #K1 #HLK1 #HJI1 #H destruct + elim (drops_inv_skip1 … HY2) -HY2 #J2 #K2 #HLK2 #HJI2 #H destruct + elim (lexs_inv_next … HK12) -HK12 #HK12 #HJ12 + elim (HRN … HJ12 … HLK1 … HJI1) -HJ12 -HJI1 #Z #Hz + >(liftsb_mono … Hz … HJI2) -Z /3 width=9 by lexs_next/ +| elim (coafter_inv_xxp … H) [1,2: |*: // ] -H * + [ #g #g1 #Hg2 #H1 #H2 destruct + elim (drops_inv_skip1 … HY1) -HY1 #J1 #K1 #HLK1 #HJI1 #H destruct + elim (drops_inv_skip1 … HY2) -HY2 #J2 #K2 #HLK2 #HJI2 #H destruct + elim (lexs_inv_push … HK12) -HK12 #HK12 #HJ12 + elim (HRP … HJ12 … HLK1 … HJI1) -HJ12 -HJI1 #Z #Hz + >(liftsb_mono … Hz … HJI2) -Z /3 width=9 by lexs_push/ + | #g #Hg2 #H destruct + lapply (drops_inv_drop1 … HY1) -HY1 #HLK1 + lapply (drops_inv_drop1 … HY2) -HY2 #HLK2 + /3 width=9 by lexs_push/ + ] +] +qed-. + (* Basic_2A1: includes: lpx_sn_liftable_dedropable *) lemma lexs_liftable_co_dedropable_sn: ∀RN,RP. (∀L. reflexive … (RN L)) → (∀L. reflexive … (RP L)) → - d_liftable2_sn … liftsb RN → d_liftable2_sn … liftsb RP → co_dedropable_sn (lexs RN RP). + d_liftable2_sn … liftsb RN → d_liftable2_sn … liftsb RP → + co_dedropable_sn (lexs RN RP). #RN #RP #H1RN #H1RP #H2RN #H2RP #b #f #L1 #K1 #H elim H -f -L1 -K1 [ #f #Hf #X #f1 #H #f2 #Hf2 >(lexs_inv_atom1 … H) -X /4 width=4 by drops_atom, lexs_atom, ex3_intro/ diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/lexs_length.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/lexs_length.ma index 812a75eea..2ceec510b 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/lexs_length.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/lexs_length.ma @@ -19,8 +19,19 @@ include "basic_2/relocation/lexs.ma". (* Forward lemmas with length for local environments ************************) -(* Basic_2A1: includes: lpx_sn_fwd_length *) +(* Basic_2A1: uses: lpx_sn_fwd_length *) lemma lexs_fwd_length: ∀RN,RP,f,L1,L2. L1 ⪤*[RN, RP, f] L2 → |L1| = |L2|. #RM #RP #f #L1 #L2 #H elim H -f -L1 -L2 // #f #I1 #I2 #L1 #L2 >length_bind >length_bind // qed-. + +(* Properties with length for local environments ****************************) + +lemma lexs_length_cfull: ∀L1,L2. |L1| = |L2| → ∀f. L1 ⪤*[cfull, cfull, f] L2. +#L1 elim L1 -L1 +[ #Y2 #H >(length_inv_zero_sn … H) -Y2 // +| #L1 #I1 #IH #Y2 #H #f + elim (length_inv_succ_sn … H) -H #I2 #L2 #HL12 #H destruct + elim (pn_split f) * #g #H destruct /3 width=1 by lexs_next, lexs_push/ +] +qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/lifts_lifts_bind.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/lifts_lifts_bind.ma index 10ad3cc52..7054d1ff4 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/lifts_lifts_bind.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/lifts_lifts_bind.ma @@ -32,3 +32,22 @@ theorem liftsb_trans: ∀f1,I1,I. ⬆*[f1] I1 ≡ I → ∀f2,I2. ⬆*[f2] I ≡ [ elim (liftsb_inv_pair_sn … H) | lapply (liftsb_inv_unit_sn … H) ] -H /3 width=6 by lifts_trans, ext2_pair, ext2_unit/ qed-. + +theorem liftsb_conf: ∀f1,I,I1. ⬆*[f1] I ≡ I1 → ∀f,I2. ⬆*[f] I ≡ I2 → + ∀f2. f2 ⊚ f1 ≡ f → ⬆*[f2] I1 ≡ I2. +#f1 #I #I1 * -I -I1 #I [2: #V #V1 #HV1 ] #f2 #I2 #H +[ elim (liftsb_inv_pair_sn … H) | lapply (liftsb_inv_unit_sn … H) ] -H +/3 width=6 by lifts_conf, ext2_pair, ext2_unit/ +qed-. + +(* Advanced proprerties *****************************************************) + +lemma liftsb_inj: ∀f. is_inj2 … (liftsb f). +#f #T1 #U #H1 #T2 #H2 lapply (after_isid_dx 𝐈𝐝 … f) +/3 width=6 by liftsb_div3, liftsb_fwd_isid/ +qed-. + +lemma liftsb_mono: ∀f,T. is_mono … (liftsb f T). +#f #T #U1 #H1 #U2 #H2 lapply (after_isid_sn 𝐈𝐝 … f) +/3 width=6 by liftsb_conf, liftsb_fwd_isid/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_csx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_csx.ma index a0f48f828..69ca48513 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_csx.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_csx.ma @@ -73,3 +73,11 @@ lemma csx_inv_lref_pair: ∀h,o,I,G,L,K,V,i. ⬇*[i] L ≡ K.ⓑ{I}V → elim (lifts_total V (𝐔❴⫯i❵)) /4 width=9 by csx_inv_lifts, csx_cpx_trans, cpx_delta_drops, drops_isuni_fwd_drop2/ qed-. + +lemma csx_inv_lref: ∀h,o,G,L,i. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃#i⦄ → + ∨∨ ⬇*[Ⓕ, 𝐔❴i❵] L ≡ ⋆ + | ∃∃I,K. ⬇*[i] L ≡ K.ⓤ{I} + | ∃∃I,K,V. ⬇*[i] L ≡ K.ⓑ{I}V & ⦃G, K⦄ ⊢ ⬈*[h, o] 𝐒⦃V⦄. +#h #o #G #L #i #H elim (drops_F_uni L i) /2 width=1 by or3_intro0/ +* * /4 width=9 by csx_inv_lref_pair, ex2_3_intro, ex1_2_intro, or3_intro2, or3_intro1/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_lsubr.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_lsubr.ma index 00683b0fc..694ce6b3c 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_lsubr.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_lsubr.ma @@ -44,3 +44,21 @@ qed-. (* Basic_1: was just: sn3_beta *) lemma csx_appl_beta: ∀h,o,p,G,L,V,W,T. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃ⓓ{p}ⓝW.V.T⦄ → ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃ⓐV.ⓛ{p}W.T⦄. /2 width=3 by csx_appl_beta_aux/ qed. + +(* Advanced forward lemmas **************************************************) + +fact csx_fwd_bind_dx_unit_aux: ∀h,o,G,L,U. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃U⦄ → + ∀p,I,J,V,T. U = ⓑ{p,I}V.T → ⦃G, L.ⓤ{J}⦄ ⊢ ⬈*[h, o] 𝐒⦃T⦄. +#h #o #G #L #U #H elim H -H #U0 #_ #IH #p #I #J #V #T #H destruct +@csx_intro #T2 #HLT2 #HT2 +@(IH (ⓑ{p,I}V.T2)) -IH /2 width=4 by cpx_bind_unit/ -HLT2 +#H elim (tdeq_inv_pair … H) -H /2 width=1 by/ +qed-. + +lemma csx_fwd_bind_dx_unit: ∀h,o,p,I,G,L,V,T. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃ⓑ{p,I}V.T⦄ → + ∀J. ⦃G, L.ⓤ{J}⦄ ⊢ ⬈*[h, o] 𝐒⦃T⦄. +/2 width=6 by csx_fwd_bind_dx_unit_aux/ qed-. + +lemma csx_fwd_bind_unit: ∀h,o,p,I,G,L,V,T. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃ⓑ{p,I}V.T⦄ → + ∀J. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃V⦄ ∧ ⦃G, L.ⓤ{J}⦄ ⊢ ⬈*[h, o] 𝐒⦃T⦄. +/3 width=4 by csx_fwd_pair_sn, csx_fwd_bind_dx_unit, conj/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_fqup.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_fqup.ma index 52159d8cd..0f90e90e2 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_fqup.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_fqup.ma @@ -29,6 +29,10 @@ lemma lfpxs_fwd_bind_dx: ∀h,p,I,G,L1,L2,V,T. ⦃G, L1⦄ ⊢ ⬈*[h, ⓑ{p,I}V ⦃G, L1.ⓑ{I}V⦄ ⊢ ⬈*[h, T] L2.ⓑ{I}V. /2 width=2 by tc_lfxs_fwd_bind_dx/ qed-. +lemma lfpxs_fwd_bind_dx_void: ∀h,p,I,G,L1,L2,V,T. ⦃G, L1⦄ ⊢ ⬈*[h, ⓑ{p,I}V.T] L2 → + ⦃G, L1.ⓧ⦄ ⊢ ⬈*[h, T] L2.ⓧ. +/2 width=4 by tc_lfxs_fwd_bind_dx_void/ qed-. + (* Advanced eliminators *****************************************************) (* Basic_2A1: uses: lpxs_ind *) diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfsx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfsx.ma index 14c939fac..74181a037 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfsx.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfsx.ma @@ -66,6 +66,24 @@ lemma lfsx_gref: ∀h,o,G,L,p. G ⊢ ⬈*[h, o, §p] 𝐒⦃L⦄. ] qed. +lemma lfsx_unit: ∀h,o,I,G,L. G ⊢ ⬈*[h, o, #0] 𝐒⦃L.ⓤ{I}⦄. +#h #o #I #G #L1 @lfsx_intro +#Y #HY #HnY elim HnY -HnY /2 width=2 by lfxs_unit_sn/ +qed. + +(* Basic forward lemmas *****************************************************) + +fact lfsx_fwd_pair_aux: ∀h,o,G,L. G ⊢ ⬈*[h, o, #0] 𝐒⦃L⦄ → + ∀I,K,V. L = K.ⓑ{I}V → G ⊢ ⬈*[h, o, V] 𝐒⦃K⦄. +#h #o #G #L #H +@(lfsx_ind … H) -L #L1 #_ #IH #I #K1 #V #H destruct +/5 width=5 by lfpx_pair, lfsx_intro, lfdeq_fwd_zero_pair/ +qed-. + +lemma lfsx_fwd_pair: ∀h,o,I,G,K,V. + G ⊢ ⬈*[h, o, #0] 𝐒⦃K.ⓑ{I}V⦄ → G ⊢ ⬈*[h, o, V] 𝐒⦃K⦄. +/2 width=4 by lfsx_fwd_pair_aux/ qed-. + (* Basic_2A1: removed theorems 9: lsx_ge_up lsx_ge lsxa_ind lsxa_intro lsxa_lleq_trans lsxa_lpxs_trans lsxa_intro_lpx lsx_lsxa lsxa_inv_lsx diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfsx_csx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfsx_csx.ma new file mode 100644 index 000000000..ff005164f --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfsx_csx.ma @@ -0,0 +1,66 @@ +(**************************************************************************) +(* ___ *) +(* ||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/rt_computation/csx_lsubr.ma". +include "basic_2/rt_computation/lfsx_lfpxs.ma". + +(* STRONGLY NORMALIZING LOCAL ENV.S FOR UNCOUNTED PARALLEL RT-TRANSITION ****) +(* +(* Advanced properties ******************************************************) + +lemma lsx_lref_be_lpxs: ∀h,o,I,G,K1,V,i,l. l ≤ yinj i → ⦃G, K1⦄ ⊢ ⬊*[h, o] V → + ∀K2. G ⊢ ⬊*[h, o, V, 0] K2 → ⦃G, K1⦄ ⊢ ➡*[h, o] K2 → + ∀L2. ⬇[i] L2 ≡ K2.ⓑ{I}V → G ⊢ ⬊*[h, o, #i, l] L2. +#h #o #I #G #K1 #V #i #l #Hli #H @(csx_ind_alt … H) -V +#V0 #_ #IHV0 #K2 #H @(lsx_ind … H) -K2 +#K0 #HK0 #IHK0 #HK10 #L0 #HLK0 @lsx_intro +#L2 #HL02 #HnL02 elim (lpx_drop_conf … HLK0 … HL02) -HL02 +#Y #H #HLK2 elim (lpx_inv_pair1 … H) -H +#K2 #V2 #HK02 #HV02 #H destruct +elim (eq_term_dec V0 V2) #HnV02 destruct [ -IHV0 -HV02 -HK0 | -IHK0 -HnL02 -HLK0 ] +[ /4 width=8 by lpxs_strap1, lleq_lref/ +| @(IHV0 … HnV02 … HLK2) -IHV0 -HnV02 -HLK2 + /3 width=4 by lsx_cpx_trans_O, lsx_lpx_trans, lpxs_cpx_trans, lpxs_strap1/ (**) (* full auto too slow *) +] +qed. + +lemma lsx_lref_be: ∀h,o,I,G,K,V,i,l. l ≤ yinj i → ⦃G, K⦄ ⊢ ⬊*[h, o] V → + G ⊢ ⬊*[h, o, V, 0] K → + ∀L. ⬇[i] L ≡ K.ⓑ{I}V → G ⊢ ⬊*[h, o, #i, l] L. +/2 width=8 by lsx_lref_be_lpxs/ qed. +*) +(* Main properties **********************************************************) + +theorem csx_lsx: ∀h,o,G,L,T. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃T⦄ → G ⊢ ⬈*[h, o, T] 𝐒⦃L⦄. +#h #o #G #L #T @(fqup_wf_ind_eq (Ⓕ) … G L T) -G -L -T +#Z #Y #X #IH #G #L * * // +[ #i #HG #HL #HT #H destruct + elim (csx_inv_lref … H) -H [ |*: * ] + [ #HL + | #I #K #HLK + | #I #K #V #HLK #HV + ] +(* + elim (lt_or_ge i (|L|)) /2 width=1 by lsx_lref_free/ + elim (ylt_split i l) /2 width=1 by lsx_lref_skip/ + #Hli #Hi elim (drop_O1_lt (Ⓕ) … Hi) -Hi + #I #K #V #HLK lapply (csx_inv_lref_bind … HLK … H) -H + /4 width=6 by lsx_lref_be, fqup_lref/ +*) +| #a #I #V #T #HG #HL #HT #H destruct + elim (csx_fwd_bind_unit … H Void) -H /3 width=1 by lfsx_bind_void/ +| #I #V #T #HG #HL #HT #H destruct + elim (csx_fwd_flat … H) -H /3 width=1 by lfsx_flat/ +] +qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfsx_drops.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfsx_drops.ma new file mode 100644 index 000000000..e4679904f --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfsx_drops.ma @@ -0,0 +1,66 @@ +(**************************************************************************) +(* ___ *) +(* ||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/lfdeq_length.ma". +include "basic_2/static/lfdeq_drops.ma". +include "basic_2/rt_transition/lfpx_length.ma". +include "basic_2/rt_transition/lfpx_drops.ma". +include "basic_2/rt_computation/lfsx_fqup.ma". + +(* STRONGLY NORMALIZING LOCAL ENV.S FOR UNCOUNTED PARALLEL RT-TRANSITION ****) + +(* Properties with generic relocation ***************************************) + +(* Note: this uses length *) +(* Basic_2A1: uses: lsx_lift_le lsx_lift_ge *) +lemma lfsx_lifts: ∀h,o,G. d_liftable1_isuni … (λL,T. G ⊢ ⬈*[h, o, T] 𝐒⦃L⦄). +#h #o #G #K #T #H @(lfsx_ind … H) -K +#K1 #_ #IH #b #f #L1 #HLK1 #Hf #U #HTU @lfsx_intro +#L2 #HL12 #HnL12 elim (lfpx_drops_conf … HLK1 … HL12 … HTU) +/5 width=9 by lfdeq_lifts_bi, lfpx_fwd_length/ +qed-. + +(* Inversion lemmas on relocation *******************************************) + +(* Basic_2A1: uses: lsx_inv_lift_le lsx_inv_lift_be lsx_inv_lift_ge *) +lemma lfsx_inv_lifts: ∀h,o,G. d_deliftable1_isuni … (λL,T. G ⊢ ⬈*[h, o, T] 𝐒⦃L⦄). +#h #o #G #L #U #H @(lfsx_ind … H) -L +#L1 #_ #IH #b #f #K1 #HLK1 #Hf #T #HTU @lfsx_intro +#K2 #HK12 #HnK12 elim (drops_lfpx_trans … HLK1 … HK12 … HTU) -HK12 +/4 width=10 by lfdeq_inv_lifts_bi/ +qed-. + +(* Advanced properties ******************************************************) + +(* Basic_2A1: uses: lsx_lref_free *) +lemma lfsx_lref_atom: ∀h,o,G,L,i. ⬇*[Ⓕ, 𝐔❴i❵] L ≡ ⋆ → G ⊢ ⬈*[h, o, #i] 𝐒⦃L⦄. +#h #o #G #L1 #i #HL1 +@(lfsx_lifts … (#0) … HL1) -HL1 // +qed. + +(* Basic_2A1: uses: lsx_lref_skip *) +lemma lfsx_lref_unit: ∀h,o,I,G,L,K,i. ⬇*[i] L ≡ K.ⓤ{I} → G ⊢ ⬈*[h, o, #i] 𝐒⦃L⦄. +#h #o #I #G #L1 #K1 #i #HL1 +@(lfsx_lifts … (#0) … HL1) -HL1 // +qed. + +(* Advanced forward lemmas **************************************************) + +(* Basic_2A1: uses: lsx_fwd_lref_be *) +lemma lfsx_fwd_lref_pair: ∀h,o,G,L,i. G ⊢ ⬈*[h, o, #i] 𝐒⦃L⦄ → + ∀I,K,V. ⬇*[i] L ≡ K.ⓑ{I}V → G ⊢ ⬈*[h, o, V] 𝐒⦃K⦄. +#h #o #G #L #i #HL #I #K #V #HLK +lapply (lfsx_inv_lifts … HL … HLK … (#0) ?) -L +/2 width=2 by lfsx_fwd_pair/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfsx_lfpxs.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfsx_lfpxs.ma index 31a027834..ff5ddc304 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfsx_lfpxs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfsx_lfpxs.ma @@ -120,3 +120,27 @@ qed-. lemma lfsx_flat: ∀h,o,I,G,L,V. G ⊢ ⬈*[h, o, V] 𝐒⦃L⦄ → ∀T. G ⊢ ⬈*[h, o, T] 𝐒⦃L⦄ → G ⊢ ⬈*[h, o, ⓕ{I}V.T] 𝐒⦃L⦄. /2 width=3 by lfsx_flat_lfpxs/ qed. + +fact lfsx_bind_lfpxs_void_aux: ∀h,o,p,I,G,L1,V. G ⊢ ⬈*[h, o, V] 𝐒⦃L1⦄ → + ∀Y,T. G ⊢ ⬈*[h, o, T] 𝐒⦃Y⦄ → + ∀L2. Y = L2.ⓧ → ⦃G, L1⦄ ⊢ ⬈*[h, ⓑ{p,I}V.T] L2 → + G ⊢ ⬈*[h, o, ⓑ{p,I}V.T] 𝐒⦃L2⦄. +#h #o #p #I #G #L1 #V #H @(lfsx_ind_lfpxs … H) -L1 +#L1 #_ #IHL1 #Y #T #H @(lfsx_ind_lfpxs … H) -Y +#Y #HY #IHY #L2 #H #HL12 destruct +@lfsx_intro_lfpxs #L0 #HL20 +lapply (lfpxs_trans … HL12 … HL20) #HL10 #H +elim (lfdneq_inv_bind_void … H) -H [ -IHY | -HY -IHL1 -HL12 ] +[ #HnV elim (lfdeq_dec h o L1 L2 V) + [ #HV @(IHL1 … L0) -IHL1 -HL12 + /3 width=6 by lfsx_lfpxs_trans, lfpxs_fwd_bind_dx_void, lfpxs_fwd_pair_sn, lfdeq_canc_sn/ (**) (* full auto too slow *) + | -HnV -HL10 /4 width=4 by lfsx_lfpxs_trans, lfpxs_fwd_pair_sn/ + ] +| /3 width=4 by lfpxs_fwd_bind_dx_void/ +] +qed-. + +lemma lfsx_bind_void: ∀h,o,p,I,G,L,V. G ⊢ ⬈*[h, o, V] 𝐒⦃L⦄ → + ∀T. G ⊢ ⬈*[h, o, T] 𝐒⦃L.ⓧ⦄ → + G ⊢ ⬈*[h, o, ⓑ{p,I}V.T] 𝐒⦃L⦄. +/2 width=3 by lfsx_bind_lfpxs_void_aux/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lsx_csx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lsx_csx.ma deleted file mode 100644 index fa00a907d..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lsx_csx.ma +++ /dev/null @@ -1,59 +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/computation/csx_lpxs.ma". -include "basic_2/computation/lcosx_cpx.ma". - -(* SN EXTENDED STRONGLY NORMALIZING LOCAL ENVIRONMENTS **********************) - -(* Advanced properties ******************************************************) - -lemma lsx_lref_be_lpxs: ∀h,o,I,G,K1,V,i,l. l ≤ yinj i → ⦃G, K1⦄ ⊢ ⬊*[h, o] V → - ∀K2. G ⊢ ⬊*[h, o, V, 0] K2 → ⦃G, K1⦄ ⊢ ➡*[h, o] K2 → - ∀L2. ⬇[i] L2 ≡ K2.ⓑ{I}V → G ⊢ ⬊*[h, o, #i, l] L2. -#h #o #I #G #K1 #V #i #l #Hli #H @(csx_ind_alt … H) -V -#V0 #_ #IHV0 #K2 #H @(lsx_ind … H) -K2 -#K0 #HK0 #IHK0 #HK10 #L0 #HLK0 @lsx_intro -#L2 #HL02 #HnL02 elim (lpx_drop_conf … HLK0 … HL02) -HL02 -#Y #H #HLK2 elim (lpx_inv_pair1 … H) -H -#K2 #V2 #HK02 #HV02 #H destruct -elim (eq_term_dec V0 V2) #HnV02 destruct [ -IHV0 -HV02 -HK0 | -IHK0 -HnL02 -HLK0 ] -[ /4 width=8 by lpxs_strap1, lleq_lref/ -| @(IHV0 … HnV02 … HLK2) -IHV0 -HnV02 -HLK2 - /3 width=4 by lsx_cpx_trans_O, lsx_lpx_trans, lpxs_cpx_trans, lpxs_strap1/ (**) (* full auto too slow *) -] -qed. - -lemma lsx_lref_be: ∀h,o,I,G,K,V,i,l. l ≤ yinj i → ⦃G, K⦄ ⊢ ⬊*[h, o] V → - G ⊢ ⬊*[h, o, V, 0] K → - ∀L. ⬇[i] L ≡ K.ⓑ{I}V → G ⊢ ⬊*[h, o, #i, l] L. -/2 width=8 by lsx_lref_be_lpxs/ qed. - -(* Main properties **********************************************************) - -theorem csx_lsx: ∀h,o,G,L,T. ⦃G, L⦄ ⊢ ⬊*[h, o] T → ∀l. G ⊢ ⬊*[h, o, T, l] L. -#h #o #G #L #T @(fqup_wf_ind_eq … G L T) -G -L -T -#Z #Y #X #IH #G #L * * // -[ #i #HG #HL #HT #H #l destruct - elim (lt_or_ge i (|L|)) /2 width=1 by lsx_lref_free/ - elim (ylt_split i l) /2 width=1 by lsx_lref_skip/ - #Hli #Hi elim (drop_O1_lt (Ⓕ) … Hi) -Hi - #I #K #V #HLK lapply (csx_inv_lref_bind … HLK … H) -H - /4 width=6 by lsx_lref_be, fqup_lref/ -| #a #I #V #T #HG #HL #HT #H #l destruct - elim (csx_fwd_bind … H) -H /3 width=1 by lsx_bind/ -| #I #V #T #HG #HL #HT #H #l destruct - elim (csx_fwd_flat … H) -H /3 width=1 by lsx_flat/ -] -qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lsx_drop.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lsx_drop.ma deleted file mode 100644 index c70d6fbc5..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lsx_drop.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/multiple/lleq_drop.ma". -include "basic_2/reduction/lpx_drop.ma". -include "basic_2/computation/lsx.ma". - -(* SN EXTENDED STRONGLY NORMALIZING LOCAL ENVIRONMENTS **********************) - -(* Advanced properties ******************************************************) - -lemma lsx_lref_free: ∀h,o,G,L,l,i. |L| ≤ i → G ⊢ ⬊*[h, o, #i, l] L. -#h #o #G #L1 #l #i #HL1 @lsx_intro -#L2 #HL12 #H elim H -H -/4 width=6 by lpx_fwd_length, lleq_free, le_repl_sn_conf_aux/ -qed. - -lemma lsx_lref_skip: ∀h,o,G,L,l,i. yinj i < l → G ⊢ ⬊*[h, o, #i, l] L. -#h #o #G #L1 #l #i #HL1 @lsx_intro -#L2 #HL12 #H elim H -H -/3 width=4 by lpx_fwd_length, lleq_skip/ -qed. - -(* Advanced forward lemmas **************************************************) - -lemma lsx_fwd_lref_be: ∀h,o,I,G,L,l,i. l ≤ yinj i → G ⊢ ⬊*[h, o, #i, l] L → - ∀K,V. ⬇[i] L ≡ K.ⓑ{I}V → G ⊢ ⬊*[h, o, V, 0] K. -#h #o #I #G #L #l #i #Hli #H @(lsx_ind … H) -L -#L1 #_ #IHL1 #K1 #V #HLK1 @lsx_intro -#K2 #HK12 #HnK12 lapply (drop_fwd_drop2 … HLK1) -#H2LK1 elim (drop_lpx_trans … H2LK1 … HK12) -H2LK1 -HK12 -#L2 #HL12 #H2LK2 #H elim (lreq_drop_conf_be … H … HLK1) -H /2 width=1 by ylt_inj/ -#Y #_ #HLK2 lapply (drop_fwd_drop2 … HLK2) -#HY lapply (drop_mono … HY … H2LK2) -HY -H2LK2 #H destruct -/4 width=10 by lleq_inv_lref_ge/ -qed-. - -(* Properties on relocation *************************************************) - -lemma lsx_lift_le: ∀h,o,G,K,T,U,lt,l,k. lt ≤ yinj l → - ⬆[l, k] T ≡ U → G ⊢ ⬊*[h, o, T, lt] K → - ∀L. ⬇[Ⓕ, l, k] L ≡ K → G ⊢ ⬊*[h, o, U, lt] L. -#h #o #G #K #T #U #lt #l #k #Hltl #HTU #H @(lsx_ind … H) -K -#K1 #_ #IHK1 #L1 #HLK1 @lsx_intro -#L2 #HL12 #HnU elim (lpx_drop_conf … HLK1 … HL12) -HL12 -/4 width=10 by lleq_lift_le/ -qed-. - -lemma lsx_lift_ge: ∀h,o,G,K,T,U,lt,l,k. yinj l ≤ lt → - ⬆[l, k] T ≡ U → G ⊢ ⬊*[h, o, T, lt] K → - ∀L. ⬇[Ⓕ, l, k] L ≡ K → G ⊢ ⬊*[h, o, U, lt + k] L. -#h #o #G #K #T #U #lt #l #k #Hllt #HTU #H @(lsx_ind … H) -K -#K1 #_ #IHK1 #L1 #HLK1 @lsx_intro -#L2 #HL12 #HnU elim (lpx_drop_conf … HLK1 … HL12) -HL12 -/4 width=9 by lleq_lift_ge/ -qed-. - -(* Inversion lemmas on relocation *******************************************) - -lemma lsx_inv_lift_le: ∀h,o,G,L,T,U,lt,l,k. lt ≤ yinj l → - ⬆[l, k] T ≡ U → G ⊢ ⬊*[h, o, U, lt] L → - ∀K. ⬇[Ⓕ, l, k] L ≡ K → G ⊢ ⬊*[h, o, T, lt] K. -#h #o #G #L #T #U #lt #l #k #Hltl #HTU #H @(lsx_ind … H) -L -#L1 #_ #IHL1 #K1 #HLK1 @lsx_intro -#K2 #HK12 #HnT elim (drop_lpx_trans … HLK1 … HK12) -HK12 -/4 width=10 by lleq_inv_lift_le/ -qed-. - -lemma lsx_inv_lift_be: ∀h,o,G,L,T,U,lt,l,k. yinj l ≤ lt → lt ≤ l + k → - ⬆[l, k] T ≡ U → G ⊢ ⬊*[h, o, U, lt] L → - ∀K. ⬇[Ⓕ, l, k] L ≡ K → G ⊢ ⬊*[h, o, T, l] K. -#h #o #G #L #T #U #lt #l #k #Hllt #Hltlm #HTU #H @(lsx_ind … H) -L -#L1 #_ #IHL1 #K1 #HLK1 @lsx_intro -#K2 #HK12 #HnT elim (drop_lpx_trans … HLK1 … HK12) -HK12 -/4 width=11 by lleq_inv_lift_be/ -qed-. - -lemma lsx_inv_lift_ge: ∀h,o,G,L,T,U,lt,l,k. yinj l + yinj k ≤ lt → - ⬆[l, k] T ≡ U → G ⊢ ⬊*[h, o, U, lt] L → - ∀K. ⬇[Ⓕ, l, k] L ≡ K → G ⊢ ⬊*[h, o, T, lt-k] K. -#h #o #G #L #T #U #lt #l #k #Hlmlt #HTU #H @(lsx_ind … H) -L -#L1 #_ #IHL1 #K1 #HLK1 @lsx_intro -#K2 #HK12 #HnT elim (drop_lpx_trans … HLK1 … HK12) -HK12 -/4 width=9 by lleq_inv_lift_ge/ -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/partial.txt b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/partial.txt index 598bfebb4..079fa87e0 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/partial.txt +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/partial.txt @@ -2,4 +2,4 @@ cpxs.ma cpxs_tdeq.ma cpxs_theq.ma cpxs_theq_vector.ma cpxs_drops.ma cpxs_fqus.ma lfpxs.ma lfpxs_length.ma lfpxs_drops.ma lfpxs_fqup.ma lfpxs_lfdeq.ma lfpxs_aaa.ma lfpxs_cpxs.ma lfpxs_lfpxs.ma csx.ma csx_simple.ma csx_simple_theq.ma csx_drops.ma csx_lsubr.ma csx_lfdeq.ma csx_aaa.ma csx_gcp.ma csx_gcr.ma csx_lfpx.ma csx_cnx.ma csx_cpxs.ma csx_lfpxs.ma csx_csx.ma csx_vector.ma csx_cnx_vector.ma csx_csx_vector.ma -lfsx.ma lfsx_fqup.ma lfsx_lfpxs.ma lfsx_lfsx.ma +lfsx.ma lfsx_drops.ma lfsx_fqup.ma lfsx_lfpxs.ma lfsx_lfsx.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_lsubr.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_lsubr.ma index cabba2b41..58350fb86 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_lsubr.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_lsubr.ma @@ -22,3 +22,9 @@ include "basic_2/rt_transition/cpx.ma". lemma lsubr_cpx_trans: ∀h,G. lsub_trans … (cpx h G) lsubr. #h #G #L1 #T1 #T2 * /3 width=4 by lsubr_cpg_trans, ex_intro/ qed-. + +lemma cpx_bind_unit: ∀h,L,G,V1,V2. ⦃G, L⦄ ⊢ V1 ⬈[h] V2 → + ∀J,T1,T2. ⦃G, L.ⓤ{J}⦄ ⊢ T1 ⬈[h] T2 → + ∀p,I. ⦃G, L⦄ ⊢ ⓑ{p,I}V1.T1 ⬈[h] ⓑ{p,I}V2.T2. +/4 width=4 by lsubr_cpx_trans, cpx_bind, lsubr_unit/ qed. + diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lfdeq.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lfdeq.ma index 2d86a95a6..9123e9121 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/static/lfdeq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/static/lfdeq.ma @@ -175,6 +175,10 @@ lemma lfdeq_inv_lref_bind_dx: ∀h,o,I2,Y1,L2,i. Y1 ≡[h, o, #⫯i] L2.ⓘ{I2} (* Basic forward lemmas *****************************************************) +lemma lfdeq_fwd_zero_pair: ∀h,o,I,K1,K2,V1,V2. + K1.ⓑ{I}V1 ≡[h, o, #0] K2.ⓑ{I}V2 → K1 ≡[h, o, V1] K2. +/2 width=3 by lfxs_fwd_zero_pair/ qed-. + (* Basic_2A1: uses: lleq_fwd_bind_sn lleq_fwd_flat_sn *) lemma lfdeq_fwd_pair_sn: ∀h,o,I,L1,L2,V,T. L1 ≡[h, o, ②{I}V.T] L2 → L1 ≡[h, o, V] L2. /2 width=3 by lfxs_fwd_pair_sn/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lfdeq_drops.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lfdeq_drops.ma index 70950458f..4b8f2f92b 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/static/lfdeq_drops.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/static/lfdeq_drops.ma @@ -20,13 +20,11 @@ include "basic_2/static/lfdeq.ma". (* Properties with generic slicing for local environments *******************) -(* Basic_2A1: includes: lleq_lift_le lleq_lift_ge *) lemma lfdeq_lifts_sn: ∀h,o. dedropable_sn (cdeq h o). /3 width=5 by lfxs_liftable_dedropable_sn, tdeq_lifts_sn/ qed-. (* Inversion lemmas with generic slicing for local environments *************) -(* Basic_2A1: restricts: lleq_inv_lift_le lleq_inv_lift_be lleq_inv_lift_ge *) lemma lfdeq_inv_lifts_sn: ∀h,o. dropable_sn (cdeq h o). /2 width=5 by lfxs_dropable_sn/ qed-. @@ -34,11 +32,11 @@ lemma lfdeq_inv_lifts_sn: ∀h,o. dropable_sn (cdeq h o). lemma lfdeq_inv_lifts_dx: ∀h,o. dropable_dx (cdeq h o). /2 width=5 by lfxs_dropable_dx/ qed-. -(* Note: missing in basic_2A1 *) -lemma lfdeq_inv_lifts_bi: ∀h,o,L1,L2,U. L1 ≡[h, o, U] L2 → - ∀K1,K2,i. ⬇*[i] L1 ≡ K1 → ⬇*[i] L2 ≡ K2 → - ∀T. ⬆*[i] T ≡ U → K1 ≡[h, o, T] K2. -/2 width=8 by lfxs_inv_lifts_bi/ qed-. +(* Basic_2A1: uses: lleq_inv_lift_le lleq_inv_lift_be lleq_inv_lift_ge *) +lemma lfdeq_inv_lifts_bi: ∀h,o,L1,L2,U. L1 ≡[h, o, U] L2 → ∀b,f. 𝐔⦃f⦄ → + ∀K1,K2. ⬇*[b, f] L1 ≡ K1 → ⬇*[b, f] L2 ≡ K2 → + ∀T. ⬆*[f] T ≡ U → K1 ≡[h, o, T] K2. +/2 width=10 by lfxs_inv_lifts_bi/ qed-. lemma lfdeq_inv_lref_pair_sn: ∀h,o,L1,L2,i. L1 ≡[h, o, #i] L2 → ∀I,K1,V1. ⬇*[i] L1 ≡ K1.ⓑ{I}V1 → ∃∃K2,V2. ⬇*[i] L2 ≡ K2.ⓑ{I}V2 & K1 ≡[h, o, V1] K2 & V1 ≡[h, o] V2. diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lfdeq_fqus.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lfdeq_fqus.ma index ab52a9150..78345ad1e 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/static/lfdeq_fqus.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/static/lfdeq_fqus.ma @@ -74,7 +74,7 @@ lemma lfdeq_fqu_trans: ∀h,o,b,G1,G2,L2,K2,T,U. ⦃G1, L2, T⦄ ⊐[b] ⦃G2, K /2 width=5 by fqu_flat_dx, ex3_2_intro/ | #I #G #L2 #T #U #HTU #Y #HU elim (lfdeq_fwd_dx … HU) #L1 #V1 #H destruct - /5 width=12 by lfdeq_inv_lifts_bi, fqu_drop, drops_refl, drops_drop, ex3_2_intro/ + /5 width=14 by lfdeq_inv_lifts_bi, fqu_drop, drops_refl, drops_drop, ex3_2_intro/ ] qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lfdeq_length.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lfdeq_length.ma index aafc79221..8221e2ed8 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/static/lfdeq_length.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/static/lfdeq_length.ma @@ -12,6 +12,7 @@ (* *) (**************************************************************************) +include "basic_2/relocation/lifts_tdeq.ma". include "basic_2/static/lfxs_length.ma". include "basic_2/static/lfdeq.ma". @@ -22,3 +23,11 @@ include "basic_2/static/lfdeq.ma". (* Basic_2A1: lleq_fwd_length *) lemma lfdeq_fwd_length: ∀h,o,L1,L2. ∀T:term. L1 ≡[h, o, T] L2 → |L1| = |L2|. /2 width=3 by lfxs_fwd_length/ qed-. + +(* Properties with length for local environments ****************************) + +(* Basic_2A1: uses: lleq_lift_le lleq_lift_ge *) +lemma lfdeq_lifts_bi: ∀L1,L2. |L1| = |L2| → ∀h,o,K1,K2,T. K1 ≡[h, o, T] K2 → + ∀b,f. ⬇*[b, f] L1 ≡ K1 → ⬇*[b, f] L2 ≡ K2 → + ∀U. ⬆*[f] T ≡ U → L1 ≡[h, o, U] L2. +/3 width=9 by lfxs_lifts_bi, tdeq_lifts_sn/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lfxs.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lfxs.ma index 747d508a8..8fddc5896 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/static/lfxs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/static/lfxs.ma @@ -44,72 +44,6 @@ definition R_confluent2_lfxs: relation4 (relation3 lenv term term) ∀L1. L0 ⪤*[RP1, T0] L1 → ∀L2. L0 ⪤*[RP2, T0] L2 → ∃∃T. R2 L1 T1 T & R1 L2 T2 T. -(* Basic properties *********************************************************) - -lemma lfxs_atom: ∀R,I. ⋆ ⪤*[R, ⓪{I}] ⋆. -#R * /3 width=3 by frees_sort, frees_atom, frees_gref, lexs_atom, ex2_intro/ -qed. - -(* Basic_2A1: uses: llpx_sn_sort *) -lemma lfxs_sort: ∀R,I1,I2,L1,L2,s. - L1 ⪤*[R, ⋆s] L2 → L1.ⓘ{I1} ⪤*[R, ⋆s] L2.ⓘ{I2}. -#R #I1 #I2 #L1 #L2 #s * #f #Hf #H12 -lapply (frees_inv_sort … Hf) -Hf -/4 width=3 by frees_sort, lexs_push, isid_push, ex2_intro/ -qed. - -lemma lfxs_pair: ∀R,I,L1,L2,V1,V2. L1 ⪤*[R, V1] L2 → - R L1 V1 V2 → L1.ⓑ{I}V1 ⪤*[R, #0] L2.ⓑ{I}V2. -#R #I1 #I2 #L1 #L2 #V1 * -/4 width=3 by ext2_pair, frees_pair, lexs_next, ex2_intro/ -qed. - -lemma lfxs_unit: ∀R,f,I,L1,L2. 𝐈⦃f⦄ → L1 ⪤*[cext2 R, cfull, f] L2 → - L1.ⓤ{I} ⪤*[R, #0] L2.ⓤ{I}. -/4 width=3 by frees_unit, lexs_next, ext2_unit, ex2_intro/ qed. - -lemma lfxs_lref: ∀R,I1,I2,L1,L2,i. - L1 ⪤*[R, #i] L2 → L1.ⓘ{I1} ⪤*[R, #⫯i] L2.ⓘ{I2}. -#R #I1 #I2 #L1 #L2 #i * /3 width=3 by lexs_push, frees_lref, ex2_intro/ -qed. - -(* Basic_2A1: uses: llpx_sn_gref *) -lemma lfxs_gref: ∀R,I1,I2,L1,L2,l. - L1 ⪤*[R, §l] L2 → L1.ⓘ{I1} ⪤*[R, §l] L2.ⓘ{I2}. -#R #I1 #I2 #L1 #L2 #l * #f #Hf #H12 -lapply (frees_inv_gref … Hf) -Hf -/4 width=3 by frees_gref, lexs_push, isid_push, ex2_intro/ -qed. - -lemma lfxs_bind_repl_dx: ∀R,I,I1,L1,L2,T. - L1.ⓘ{I} ⪤*[R, T] L2.ⓘ{I1} → - ∀I2. cext2 R L1 I I2 → - L1.ⓘ{I} ⪤*[R, T] L2.ⓘ{I2}. -#R #I #I1 #L1 #L2 #T * #f #Hf #HL12 #I2 #HR -/3 width=5 by lexs_pair_repl, ex2_intro/ -qed-. - -lemma lfxs_sym: ∀R. lexs_frees_confluent (cext2 R) cfull → - (∀L1,L2,T1,T2. R L1 T1 T2 → R L2 T2 T1) → - ∀T. symmetric … (lfxs R T). -#R #H1R #H2R #T #L1 #L2 * #f1 #Hf1 #HL12 elim (H1R … Hf1 … HL12) -Hf1 -/5 width=5 by sle_lexs_trans, lexs_sym, cext2_sym, ex2_intro/ -qed-. - -(* Basic_2A1: uses: llpx_sn_co *) -lemma lfxs_co: ∀R1,R2. (∀L,T1,T2. R1 L T1 T2 → R2 L T1 T2) → - ∀L1,L2,T. L1 ⪤*[R1, T] L2 → L1 ⪤*[R2, T] L2. -#R1 #R2 #HR #L1 #L2 #T * /5 width=7 by lexs_co, cext2_co, ex2_intro/ -qed-. - -lemma lfxs_isid: ∀R1,R2,L1,L2,T1,T2. - (∀f. L1 ⊢ 𝐅*⦃T1⦄ ≡ f → 𝐈⦃f⦄) → - (∀f. 𝐈⦃f⦄ → L1 ⊢ 𝐅*⦃T2⦄ ≡ f) → - L1 ⪤*[R1, T1] L2 → L1 ⪤*[R2, T2] L2. -#R1 #R2 #L1 #L2 #T1 #T2 #H1 #H2 * -/4 width=7 by lexs_co_isid, ex2_intro/ -qed-. - (* Basic inversion lemmas ***************************************************) lemma lfxs_inv_atom_sn: ∀R,Y2,T. ⋆ ⪤*[R, T] Y2 → Y2 = ⋆. @@ -284,6 +218,12 @@ qed-. (* Basic forward lemmas *****************************************************) +lemma lfxs_fwd_zero_pair: ∀R,I,K1,K2,V1,V2. + K1.ⓑ{I}V1 ⪤*[R, #0] K2.ⓑ{I}V2 → K1 ⪤*[R, V1] K2. +#R #I #K1 #K2 #V1 #V2 #H +elim (lfxs_inv_zero_pair_sn … H) -H #Y #X #HK12 #_ #H destruct // +qed-. + (* Basic_2A1: uses: llpx_sn_fwd_pair_sn llpx_sn_fwd_bind_sn llpx_sn_fwd_flat_sn *) lemma lfxs_fwd_pair_sn: ∀R,I,L1,L2,V,T. L1 ⪤*[R, ②{I}V.T] L2 → L1 ⪤*[R, V] L2. #R * [ #p ] #I #L1 #L2 #V #T * #f #Hf #HL @@ -309,6 +249,79 @@ lemma lfxs_fwd_dx: ∀R,I2,L1,K2,T. L1 ⪤*[R, T] K2.ⓘ{I2} → /2 width=3 by ex1_2_intro/ qed-. +(* Basic properties *********************************************************) + +lemma lfxs_atom: ∀R,I. ⋆ ⪤*[R, ⓪{I}] ⋆. +#R * /3 width=3 by frees_sort, frees_atom, frees_gref, lexs_atom, ex2_intro/ +qed. + +(* Basic_2A1: uses: llpx_sn_sort *) +lemma lfxs_sort: ∀R,I1,I2,L1,L2,s. + L1 ⪤*[R, ⋆s] L2 → L1.ⓘ{I1} ⪤*[R, ⋆s] L2.ⓘ{I2}. +#R #I1 #I2 #L1 #L2 #s * #f #Hf #H12 +lapply (frees_inv_sort … Hf) -Hf +/4 width=3 by frees_sort, lexs_push, isid_push, ex2_intro/ +qed. + +lemma lfxs_pair: ∀R,I,L1,L2,V1,V2. L1 ⪤*[R, V1] L2 → + R L1 V1 V2 → L1.ⓑ{I}V1 ⪤*[R, #0] L2.ⓑ{I}V2. +#R #I1 #I2 #L1 #L2 #V1 * +/4 width=3 by ext2_pair, frees_pair, lexs_next, ex2_intro/ +qed. + +lemma lfxs_unit: ∀R,f,I,L1,L2. 𝐈⦃f⦄ → L1 ⪤*[cext2 R, cfull, f] L2 → + L1.ⓤ{I} ⪤*[R, #0] L2.ⓤ{I}. +/4 width=3 by frees_unit, lexs_next, ext2_unit, ex2_intro/ qed. + +lemma lfxs_lref: ∀R,I1,I2,L1,L2,i. + L1 ⪤*[R, #i] L2 → L1.ⓘ{I1} ⪤*[R, #⫯i] L2.ⓘ{I2}. +#R #I1 #I2 #L1 #L2 #i * /3 width=3 by lexs_push, frees_lref, ex2_intro/ +qed. + +(* Basic_2A1: uses: llpx_sn_gref *) +lemma lfxs_gref: ∀R,I1,I2,L1,L2,l. + L1 ⪤*[R, §l] L2 → L1.ⓘ{I1} ⪤*[R, §l] L2.ⓘ{I2}. +#R #I1 #I2 #L1 #L2 #l * #f #Hf #H12 +lapply (frees_inv_gref … Hf) -Hf +/4 width=3 by frees_gref, lexs_push, isid_push, ex2_intro/ +qed. + +lemma lfxs_bind_repl_dx: ∀R,I,I1,L1,L2,T. + L1.ⓘ{I} ⪤*[R, T] L2.ⓘ{I1} → + ∀I2. cext2 R L1 I I2 → + L1.ⓘ{I} ⪤*[R, T] L2.ⓘ{I2}. +#R #I #I1 #L1 #L2 #T * #f #Hf #HL12 #I2 #HR +/3 width=5 by lexs_pair_repl, ex2_intro/ +qed-. + +lemma lfxs_sym: ∀R. lexs_frees_confluent (cext2 R) cfull → + (∀L1,L2,T1,T2. R L1 T1 T2 → R L2 T2 T1) → + ∀T. symmetric … (lfxs R T). +#R #H1R #H2R #T #L1 #L2 * #f1 #Hf1 #HL12 elim (H1R … Hf1 … HL12) -Hf1 +/5 width=5 by sle_lexs_trans, lexs_sym, cext2_sym, ex2_intro/ +qed-. + +(* Basic_2A1: uses: llpx_sn_co *) +lemma lfxs_co: ∀R1,R2. (∀L,T1,T2. R1 L T1 T2 → R2 L T1 T2) → + ∀L1,L2,T. L1 ⪤*[R1, T] L2 → L1 ⪤*[R2, T] L2. +#R1 #R2 #HR #L1 #L2 #T * /5 width=7 by lexs_co, cext2_co, ex2_intro/ +qed-. + +lemma lfxs_isid: ∀R1,R2,L1,L2,T1,T2. + (∀f. L1 ⊢ 𝐅*⦃T1⦄ ≡ f → 𝐈⦃f⦄) → + (∀f. 𝐈⦃f⦄ → L1 ⊢ 𝐅*⦃T2⦄ ≡ f) → + L1 ⪤*[R1, T1] L2 → L1 ⪤*[R2, T2] L2. +#R1 #R2 #L1 #L2 #T1 #T2 #H1 #H2 * +/4 width=7 by lexs_co_isid, ex2_intro/ +qed-. + +lemma lfxs_unit_sn: ∀R1,R2,I,K1,L2. + K1.ⓤ{I} ⪤*[R1, #0] L2 → K1.ⓤ{I} ⪤*[R2, #0] L2. +#R1 #R2 #I #K1 #L2 #H +elim (lfxs_inv_zero_unit_sn … H) -H #f #K2 #Hf #HK12 #H destruct +/3 width=7 by lfxs_unit, lexs_co_isid/ +qed-. + (* Basic_2A1: removed theorems 9: llpx_sn_skip llpx_sn_lref llpx_sn_free llpx_sn_fwd_lref diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lfxs_drops.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lfxs_drops.ma index 8edb37e99..0eec7d41e 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/static/lfxs_drops.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/static/lfxs_drops.ma @@ -36,7 +36,6 @@ definition dropable_dx: predicate (relation3 lenv term term) ≝ (* Properties with generic slicing for local environments *******************) -(* Basic_2A1: includes: llpx_sn_lift_le llpx_sn_lift_ge *) lemma lfxs_liftable_dedropable_sn: ∀R. (∀L. reflexive ? (R L)) → d_liftable2_sn … lifts R → dedropable_sn R. #R #H1R #H2R #b #f #L1 #K1 #HLK1 #K2 #T * #f1 #Hf1 #HK12 #U #HTU @@ -48,7 +47,7 @@ qed-. (* Inversion lemmas with generic slicing for local environments *************) -(* Basic_2A1: restricts: llpx_sn_inv_lift_le llpx_sn_inv_lift_be llpx_sn_inv_lift_ge *) +(* Basic_2A1: uses: llpx_sn_inv_lift_le llpx_sn_inv_lift_be llpx_sn_inv_lift_ge *) (* Basic_2A1: was: llpx_sn_drop_conf_O *) lemma lfxs_dropable_sn: ∀R. dropable_sn R. #R #b #f #L1 #K1 #HLK1 #H1f #L2 #U * #f2 #Hf2 #HL12 #T #HTU @@ -69,13 +68,13 @@ elim (lexs_co_dropable_dx … HL12 … HLK2 … H2f) -L2 /4 width=9 by frees_inv_lifts, ex2_intro/ qed-. -(* Basic_2A1: was: llpx_sn_inv_lift_O *) -lemma lfxs_inv_lifts_bi: ∀R,L1,L2,U. L1 ⪤*[R, U] L2 → - ∀K1,K2,i. ⬇*[i] L1 ≡ K1 → ⬇*[i] L2 ≡ K2 → - ∀T. ⬆*[i] T ≡ U → K1 ⪤*[R, T] K2. -#R #L1 #L2 #U #HL12 #K1 #K2 #i #HLK1 #HLK2 #T #HTU +(* Basic_2A1: uses: llpx_sn_inv_lift_O *) +lemma lfxs_inv_lifts_bi: ∀R,L1,L2,U. L1 ⪤*[R, U] L2 → ∀b,f. 𝐔⦃f⦄ → + ∀K1,K2. ⬇*[b, f] L1 ≡ K1 → ⬇*[b, f] L2 ≡ K2 → + ∀T. ⬆*[f] T ≡ U → K1 ⪤*[R, T] K2. +#R #L1 #L2 #U #HL12 #b #f #Hf #K1 #K2 #HLK1 #HLK2 #T #HTU elim (lfxs_dropable_sn … HLK1 … HL12 … HTU) -L1 -U // #Y #HK12 #HY -lapply (drops_mono … HY … HLK2) -L2 -i #H destruct // +lapply (drops_mono … HY … HLK2) -b -f -L2 #H destruct // qed-. lemma lfxs_inv_lref_pair_sn: ∀R,L1,L2,i. L1 ⪤*[R, #i] L2 → ∀I,K1,V1. ⬇*[i] L1 ≡ K1.ⓑ{I}V1 → diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lfxs_length.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lfxs_length.ma index 3b8208e4a..2a090e642 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/static/lfxs_length.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/static/lfxs_length.ma @@ -13,7 +13,7 @@ (**************************************************************************) include "basic_2/relocation/lexs_length.ma". -include "basic_2/static/lfxs.ma". +include "basic_2/static/lfxs_drops.ma". (* GENERIC EXTENSION ON REFERRED ENTRIES OF A CONTEXT-SENSITIVE REALTION ****) @@ -23,3 +23,16 @@ include "basic_2/static/lfxs.ma". lemma lfxs_fwd_length: ∀R,L1,L2,T. L1 ⪤*[R, T] L2 → |L1| = |L2|. #R #L1 #L2 #T * /2 width=4 by lexs_fwd_length/ qed-. + +(* Properties with length for local environments ****************************) + +(* Basic_2A1: uses: llpx_sn_lift_le llpx_sn_lift_ge *) +lemma lfxs_lifts_bi: ∀R.d_liftable2_sn … lifts R → + ∀L1,L2. |L1| = |L2| → ∀K1,K2,T. K1 ⪤*[R, T] K2 → + ∀b,f. ⬇*[b, f] L1 ≡ K1 → ⬇*[b, f] L2 ≡ K2 → + ∀U. ⬆*[f] T ≡ U → L1 ⪤*[R, U] L2. +#R #HR #L1 #L2 #HL12 #K1 #K2 #T * #f1 #Hf1 #HK12 #b #f #HLK1 #HLK2 #U #HTU +elim (frees_total L1 U) #f2 #Hf2 +lapply (frees_fwd_coafter … Hf2 … HLK1 … HTU … Hf1) -HTU #Hf +/4 width=12 by lexs_length_cfull, lexs_liftable_co_dedropable_bi, cext2_d_liftable2_sn, cfull_lift_sn, ex2_intro/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl index 7310545d7..8ff7a521f 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl +++ b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl @@ -88,7 +88,7 @@ table { ] [ { "strongly normalizing rt-computation" * } { [ "lcosx ( ? ⊢ ~⬊*[?,?,?] ? )" "lcosx_cpx" * ] - [ "lsx_drop" + "lsx_lpx" + "lsx_lpxs" + "llsx_csx" * ] + [ "llsx_csx" * ] [ "csx_fpbs" * ] } ] @@ -108,7 +108,7 @@ table { ] *) [ { "uncounted context-sensitive rt-computation" * } { - [ "lfsx ( ? ⊢ ⬈*[?,?,?] 𝐒⦃?⦄ )" "lfsx_fqup" + "lfsx_lfpxs" + "lfsx_lfsx" * ] + [ "lfsx ( ? ⊢ ⬈*[?,?,?] 𝐒⦃?⦄ )" "lfsx_drops" + "lfsx_fqup" + "lfsx_lfpxs" + "lfsx_lfsx" * ] [ "csx_vector ( ⦃?,?⦄ ⊢ ⬈*[?,?] 𝐒⦃?⦄ )" "csx_cnx_vector" + "csx_csx_vector" * ] [ "csx ( ⦃?,?⦄ ⊢ ⬈*[?,?] 𝐒⦃?⦄ )" "csx_simple" + "csx_simple_theq" + "csx_drops" + "csx_lsubr" + "csx_lfdeq" + "csx_aaa" + "csx_gcp" + "csx_gcr" + "csx_lfpx" + "csx_cnx" + "csx_cpxs" + "csx_lfpxs" + "csx_csx" * ] [ "lfpxs ( ⦃?,?⦄ ⊢ ⬈*[?,?] ? )" "lfpxs_length" + "lfpxs_drops" + "lfpxs_fqup" + "lfpxs_lfdeq" + "lfpxs_aaa" + "lfpxs_cpxs" + "lfpxs_lfpxs" * ] @@ -121,7 +121,7 @@ table { [ { "rt-transition" * } { [ { "uncounted rst-transition" * } { [ "fpbq ( ⦃?,?,?⦄ ≽[?] ⦃?,?,?⦄ )" "fpbq_aaa" * ] - [ "fpb ( ⦃?,?,?⦄ ≻[?,?] ⦃?,?,?⦄ )" "fpb_lfdeq" * ] + [ "fpb ( ⦃?,?,?⦄ ≻[?] ⦃?,?,?⦄ )" "fpb_lfdeq" * ] } ] [ { "t-bound context-sensitive rt-transition" * } {