From: Ferruccio Guidi Date: Fri, 21 Feb 2014 16:36:20 +0000 (+0000) Subject: - main proposition on lsx finally proved! X-Git-Tag: make_still_working~975 X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=376fd7774ef0fa2f30a4afb25aab6158e3cd04b7 - main proposition on lsx finally proved! - long awaited equivalence for local environments is now set up (coequivalence is in etc in case of need) - unused results on append parked in etc - some additions to ynat --- diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/fsb_csx.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fsb_csx.ma index a460855c3..62eb01ba2 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/fsb_csx.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/fsb_csx.ma @@ -16,7 +16,7 @@ include "basic_2/computation/lsx_csx.ma". include "basic_2/computation/fsb_alt.ma". axiom lsx_fqup_conf: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃+ ⦃G2, L2, T2⦄ → - G1 ⊢ ⋕⬊*[h, g, T1] L1 → G2 ⊢ ⋕⬊*[h, g, T2] L2. + G1 ⊢ ⋕⬊*[h, g, T1, 0] L1 → G2 ⊢ ⋕⬊*[h, g, T2, 0] L2. axiom fqup_lpxs_trans_nlleq: ∀h,g,G1,G2,K1,K2,T1,T2. ⦃G1, K1, T1⦄ ⊃+ ⦃G2, K2, T2⦄ → ∀L2. ⦃G2, K2⦄ ⊢ ➡*[h, g] L2 → (K2 ⋕[T2, 0] L2 →⊥) → @@ -29,7 +29,7 @@ axiom fqup_lpxs_trans_nlleq: ∀h,g,G1,G2,K1,K2,T1,T2. ⦃G1, K1, T1⦄ ⊃+ ⦃ lemma csx_fsb: ∀h,g,G,L,T. ⦃G, L⦄ ⊢ ⬊*[h, g] T → ⦃G, L⦄ ⊢ ⦥[h, g] T. #h #g #G1 #L1 #T1 #H @(csx_ind_alt … H) -T1 -#T1 #HT1 @(lsx_ind h g T1 G1 … L1) /2 width=1 by csx_lsx/ -L1 +#T1 #HT1 @(lsx_ind h g G1 T1 0 … L1) /2 width=1 by csx_lsx/ -L1 #L1 @(fqup_wf_ind … G1 L1 T1) -G1 -L1 -T1 #G1 #L1 #T1 #IHu #H1 #IHl #IHc @fsb_intro #G2 #L2 #T2 * -G2 -L2 -T2 diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/lcosx.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/lcosx.ma new file mode 100644 index 000000000..f29f9837b --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/lcosx.ma @@ -0,0 +1,77 @@ +(**************************************************************************) +(* ___ *) +(* ||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/lazycosn_5.ma". +include "basic_2/computation/lsx.ma". + +(* SN EXTENDED STRONGLY CONORMALIZING LOCAL ENVIRONMENTS ********************) + +inductive lcosx (h) (g) (G): relation2 ynat lenv ≝ +| lcosx_sort: ∀d. lcosx h g G d (⋆) +| lcosx_skip: ∀I,L,T. lcosx h g G 0 L → lcosx h g G 0 (L.ⓑ{I}T) +| lcosx_pair: ∀I,L,T,d. G ⊢ ⋕⬊*[h, g, T, d] L → + lcosx h g G d L → lcosx h g G (⫯d) (L.ⓑ{I}T) +. + +interpretation + "sn extended strong conormalization (local environment)" + 'LazyCoSN h g d G L = (lcosx h g G d L). + +(* Basic properties *********************************************************) + +lemma lcosx_O: ∀h,g,G,L. G ⊢ ⧤⬊*[h, g, 0] L. +#h #g #G #L elim L /2 width=1 by lcosx_skip/ +qed. + +lemma lcosx_ldrop_trans_lt: ∀h,g,G,L,d. G ⊢ ⧤⬊*[h, g, d] L → + ∀I,K,V,i. ⇩[i] L ≡ K.ⓑ{I}V → i < d → + G ⊢ ⧤⬊*[h, g, ⫰(d-i)] K ∧ G ⊢ ⋕⬊*[h, g, V, ⫰(d-i)] K. +#h #g #G #L #d #H elim H -L -d +[ #d #J #K #V #i #H elim (ldrop_inv_atom1 … H) -H #H destruct +| #I #L #T #_ #_ #J #K #V #i #_ #H elim (ylt_yle_false … H) -H // +| #I #L #T #d #HT #HL #IHL #J #K #V #i #H #Hid + elim (ldrop_inv_O1_pair1 … H) -H * #Hi #HLK destruct + [ >ypred_succ /2 width=1 by conj/ + | lapply (ylt_pred … Hid ?) -Hid /2 width=1 by ylt_inj/ >ypred_succ #Hid + elim (IHL … HLK ?) -IHL -HLK yminus_SO2 // + <(ypred_succ d) in ⊢ (%→%→?); >yminus_pred /2 width=1 by ylt_inj, conj/ + ] +] +qed-. + +(* Basic inversion lemmas ***************************************************) + +fact lcosx_inv_succ_aux: ∀h,g,G,L,x. G ⊢ ⧤⬊*[h, g, x] L → ∀d. x = ⫯d → + L = ⋆ ∨ + ∃∃I,K,V. L = K.ⓑ{I}V & G ⊢ ⧤⬊*[h, g, d] K & + G ⊢ ⋕⬊*[h, g, V, d] K. +#h #g #G #L #d * -L -d /2 width=1 by or_introl/ +[ #I #L #T #_ #x #H elim (ysucc_inv_O_sn … H) +| #I #L #T #d #HT #HL #x #H <(ysucc_inj … H) -x + /3 width=6 by ex3_3_intro, or_intror/ +] +qed-. + +lemma lcosx_inv_succ: ∀h,g,G,L,d. G ⊢ ⧤⬊*[h, g, ⫯d] L → L = ⋆ ∨ + ∃∃I,K,V. L = K.ⓑ{I}V & G ⊢ ⧤⬊*[h, g, d] K & + G ⊢ ⋕⬊*[h, g, V, d] K. +/2 width=3 by lcosx_inv_succ_aux/ qed-. + +lemma lcosx_inv_pair: ∀h,g,I,G,L,T,d. G ⊢ ⧤⬊*[h, g, ⫯d] L.ⓑ{I}T → + G ⊢ ⧤⬊*[h, g, d] L ∧ G ⊢ ⋕⬊*[h, g, T, d] L. +#h #g #I #G #L #T #d #H elim (lcosx_inv_succ … H) -H +[ #H destruct +| * #Z #Y #X #H destruct /2 width=1 by conj/ +] +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/lcosx_cpxs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/lcosx_cpxs.ma new file mode 100644 index 000000000..3ed17d258 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/lcosx_cpxs.ma @@ -0,0 +1,71 @@ +(**************************************************************************) +(* ___ *) +(* ||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/lsx_ldrop.ma". +include "basic_2/computation/lsx_lpxs.ma". +include "basic_2/computation/lcosx.ma". + +(* SN EXTENDED STRONGLY CONORMALIZING LOCAL ENVIRONMENTS ********************) + +(* Properties on extended context-sensitive parallel computation for term ***) + +lemma lsx_cpx_trans_lcosx: ∀h,g,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡[h, g] T2 → + ∀d. G ⊢ ⧤⬊*[h, g, d] L → + G ⊢ ⋕⬊*[h, g, T1, d] L → G ⊢ ⋕⬊*[h, g, T2, d] L. +#h #g #G #L #T1 #T2 #H elim H -G -L -T1 -T2 // +[ #I #G #L #K #V1 #V2 #W2 #i #HLK #_ #HVW2 #IHV12 #d #HL #H + elim (ylt_split i d) #Hdi [ -H | -HL ] + [ <(ymax_pre_sn d (⫯i)) /2 width=1 by ylt_fwd_le_succ/ + elim (lcosx_ldrop_trans_lt … HL … HLK) // -HL -Hdi + lapply (ldrop_fwd_drop2 … HLK) -HLK /3 width=7 by lsx_lift_ge/ + | lapply (lsx_fwd_lref_be … H … HLK) // -H -Hdi + lapply (ldrop_fwd_drop2 … HLK) -HLK + /4 width=10 by lsx_ge, lsx_lift_le/ + ] +| #a #I #G #L #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #d #HL #H + elim (lsx_inv_bind … H) -H #HV1 #HT1 + @lsx_bind /2 width=2 by/ (**) (* explicit constructor *) + @(lsx_leqy_conf … (L.ⓑ{I}V1)) /3 width=1 by lcosx_pair, lsuby_succ/ +| #I #G #L #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #d #HL #H + elim (lsx_inv_flat … H) -H /3 width=1 by lsx_flat/ +| #G #L #V #U1 #U2 #T2 #_ #HTU2 #IHU12 #d #HL #H + elim (lsx_inv_bind … H) -H + /4 width=9 by lcosx_pair, lsx_inv_lift_ge, ldrop_drop/ +| #G #L #V #T1 #T2 #_ #IHT12 #d #HL #H + elim (lsx_inv_flat … H) -H /2 width=1 by/ +| #G #L #V1 #V2 #T #_ #IHV12 #d #HL #H + elim (lsx_inv_flat … H) -H /2 width=1 by/ +| #a #G #L #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #IHV12 #IHW12 #IHT12 #d #HL #H + elim (lsx_inv_flat … H) -H #HV1 #H + elim (lsx_inv_bind … H) -H #HW1 #HT1 + @lsx_bind /3 width=1 by lsx_flat/ (**) (* explicit constructor *) + @(lsx_leqy_conf … (L.ⓛW1)) /3 width=1 by lcosx_pair, lsuby_succ/ +| #a #G #L #V1 #V2 #U2 #W1 #W2 #T1 #T2 #_ #HVU2 #_ #_ #IHV12 #IHW12 #IHT12 #d #HL #H + elim (lsx_inv_flat … H) -H #HV1 #H + elim (lsx_inv_bind … H) -H #HW1 #HT1 + @lsx_bind /2 width=1 by/ (**) (* explicit constructor *) + @lsx_flat [ /3 width=7 by lsx_lift_ge, ldrop_drop/ ] + @(lsx_leqy_conf … (L.ⓓW1)) /3 width=1 by lcosx_pair, lsuby_succ/ +] +qed-. + +lemma lsx_cpx_trans_O: ∀h,g,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡[h, g] T2 → + G ⊢ ⋕⬊*[h, g, T1, 0] L → G ⊢ ⋕⬊*[h, g, T2, 0] L. +/2 width=3 by lsx_cpx_trans_lcosx/ qed-. + +lemma lsx_cpxs_trans_O: ∀h,g,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡*[h, g] T2 → + G ⊢ ⋕⬊*[h, g, T1, 0] L → G ⊢ ⋕⬊*[h, g, T2, 0] L. +#h #g #G #L #T1 #T2 #H @(cpxs_ind … H) -T2 +/3 width=3 by lsx_cpx_trans_O, cpxs_strap1/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/lprs_ldrop.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/lprs_ldrop.ma index a728ad0ab..f03d3f0e8 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/lprs_ldrop.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/lprs_ldrop.ma @@ -12,7 +12,6 @@ (* *) (**************************************************************************) -include "basic_2/relocation/ldrop_lsuby.ma". include "basic_2/reduction/lpr_ldrop.ma". include "basic_2/computation/lprs.ma". diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_ldrop.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_ldrop.ma index 95afc7c3b..d8c489017 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_ldrop.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_ldrop.ma @@ -12,7 +12,6 @@ (* *) (**************************************************************************) -include "basic_2/relocation/ldrop_lsuby.ma". include "basic_2/reduction/lpx_ldrop.ma". include "basic_2/computation/lpxs.ma". diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/lsx.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/lsx.ma index 9661a8839..5307af43e 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/lsx.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/lsx.ma @@ -62,6 +62,12 @@ lemma lsx_gref: ∀h,g,G,L,d,p. G ⊢ ⋕⬊*[h, g, §p, d] L. /3 width=4 by lpxs_fwd_length, lleq_gref/ qed. +lemma lsx_be: ∀h,g,G,L,T,U,dt,d,e. yinj d ≤ dt → dt ≤ d + e → + ⇧[d, e] T ≡ U → G ⊢ ⋕⬊*[h, g, U, dt] L → G ⊢ ⋕⬊*[h, g, U, d] L. +#h #g #G #L #T #U #dt #d #e #Hddt #Hdtde #HTU #H @(lsx_ind … H) -L +/5 width=7 by lsx_intro, lleq_be/ +qed-. + (* Basic forward lemmas *****************************************************) lemma lsx_fwd_bind_sn: ∀h,g,a,I,G,L,V,T,d. G ⊢ ⋕⬊*[h, g, ⓑ{a,I}V.T, d] L → diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/lsx_csx.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/lsx_csx.ma index edde17495..a213bfa60 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/lsx_csx.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/lsx_csx.ma @@ -12,76 +12,50 @@ (* *) (**************************************************************************) -include "basic_2/reduction/cpx_cpys.ma". -include "basic_2/computation/lpxs_llneq.ma". include "basic_2/computation/csx_alt.ma". -include "basic_2/computation/lsx_lpxs.ma". +include "basic_2/computation/csx_lift.ma". +include "basic_2/computation/lcosx_cpxs.ma". (* SN EXTENDED STRONGLY NORMALIZING LOCAL ENVIRONMENTS **********************) (* Advanced properties ******************************************************) -lemma lpxs_cpys_csx_lsx: ∀h,g,G,L1,U. ⦃G, L1⦄ ⊢ ⬊*[h, g] U → - ∀T. ⦃G, L1⦄ ⊢ T ▶*[0, ∞] U → - G ⊢ ⋕⬊*[h, g, T] L1. -#h #g #G #L1 #U #H @(csx_ind_alt … H) -U -#U #_ #IHU #T #HTU @lsx_intro -#L2 #HL02 #HnT elim (lpxs_nlleq_fwd_cpxs … HL02 HnT) -HnT -#U0 #U2 #H0 #H2 #HU02 #HnU02 elim (cpys_conf_eq … HTU … H0) -#X #HUX #H0X elim (eq_term_dec U X) #HnUX destruct -[ -HUX -| -HnU02 @(lsx_lpxs_trans … HL02) @(IHU … HnUX) - [ /3 width=3 by cpys_cpx, cpx_cpxs/ - | /2 width=3 by cpys_trans_eq/ - ] -] - -lemma lpxs_cpys_csx_lsx: ∀h,g,G,L1,U. ⦃G, L1⦄ ⊢ ⬊*[h, g] U → - ∀L2. ⦃G, L1⦄ ⊢ ➡*[h, g] L2 → ∀T. ⦃G, L2⦄ ⊢ T ▶*[0, ∞] U → - G ⊢ ⋕⬊*[h, g, T] L2. -#h #g #G #L1 #U #H @(csx_ind_alt … H) -U -#U #_ #IHU #L0 #HL10 #T #HTU @lsx_intro -#L2 #HL02 #HnT elim (lpxs_nlleq_fwd_cpxs … HL02 HnT) -HnT -#U0 #U2 #H0 #H2 #HU02 #HnU02 elim (cpys_conf_eq … HTU … H0) -#X #HUX #H0X elim (eq_term_dec U X) #HnUX destruct -[ -HUX -| -HnU02 @(IHU … HnUX) - - --HnT /4 width=9 by lpxs_trans, lpxs_cpxs_trans, cpx_cpye_fwd_lpxs/ +lemma lsx_lref_be_lpxs: ∀h,g,I,G,K1,V,i,d. d ≤ yinj i → ⦃G, K1⦄ ⊢ ⬊*[h, g] V → + ∀K2. G ⊢ ⋕⬊*[h, g, V, 0] K2 → ⦃G, K1⦄ ⊢ ➡*[h, g] K2 → + ∀L2. ⇩[i] L2 ≡ K2.ⓑ{I}V → G ⊢ ⋕⬊*[h, g, #i, d] L2. +#h #g #I #G #K1 #V #i #d #Hdi #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 (lpxs_ldrop_conf … HLK0 … HL02) -HL02 +#Y #H #HLK2 elim (lpxs_inv_pair1 … H) -H +#K2 #V2 #HK02 #HV02 #H destruct +lapply (lpxs_trans … HK10 … HK02) #HK12 +elim (eq_term_dec V0 V2) #HnV02 destruct [ -IHV0 -HV02 -HK0 -HK10 | -IHK0 -HnL02 -HLK0 ] +[ /4 width=8 by lleq_lref/ +| @(IHV0 … HnV02 … HK12 … HLK2) -IHV0 -HnV02 -HK12 -HLK2 + /3 width=4 by lsx_cpxs_trans_O, lsx_lpxs_trans, lpxs_cpxs_trans/ (**) (* full auto too slow *) ] - - - - - - - -include "basic_2/reduction/cpx_cpys.ma". -include "basic_2/computation/lpxs_cpye.ma". -include "basic_2/computation/csx_alt.ma". -include "basic_2/computation/lsx_lpxs.ma". - -(* SN EXTENDED STRONGLY NORMALIZING LOCAL ENVIRONMENTS **********************) +qed. -(* Advanced properties ******************************************************) +lemma lsx_lref_be: ∀h,g,I,G,K,V,i,d. d ≤ yinj i → ⦃G, K⦄ ⊢ ⬊*[h, g] V → + G ⊢ ⋕⬊*[h, g, V, 0] K → + ∀L. ⇩[i] L ≡ K.ⓑ{I}V → G ⊢ ⋕⬊*[h, g, #i, d] L. +/2 width=8 by lsx_lref_be_lpxs/ qed. -axiom lpxs_cpye_csx_lsx: ∀h,g,G,L1,U. ⦃G, L1⦄ ⊢ ⬊*[h, g] U → - ∀L2. ⦃G, L1⦄ ⊢ ➡*[h, g] L2 → ∀T. ⦃G, L2⦄ ⊢ T ▶*[0, ∞] 𝐍⦃U⦄ → - G ⊢ ⋕⬊*[h, g, T] L2. -(* -#h #g #G #L1 #U #H @(csx_ind_alt … H) -U -#U0 #_ #IHU0 #L0 #HL10 #T #H0 @lsx_intro -#L2 #HL02 #HnT elim (cpye_total G L2 T 0 (∞)) -#U2 #H2 elim (eq_term_dec U0 U2) #H destruct -[ -IHU0 -| -HnT /4 width=9 by lpxs_trans, lpxs_cpxs_trans, cpx_cpye_fwd_lpxs/ -] -*) (* Main properties **********************************************************) -lemma csx_lsx: ∀h,g,G,L,T. ⦃G, L⦄ ⊢ ⬊*[h, g] T → G ⊢ ⋕⬊*[h, g, T] L. -#h #g #G #L #T #HT elim (cpye_total G L T 0 (∞)) -#U #HTU elim HTU -/4 width=5 by lpxs_cpye_csx_lsx, csx_cpx_trans, cpys_cpx/ +theorem csx_lsx: ∀h,g,G,L,T. ⦃G, L⦄ ⊢ ⬊*[h, g] T → ∀d. G ⊢ ⋕⬊*[h, g, T, d] L. +#h #g #G #L #T @(fqup_wf_ind_eq … G L T) -G -L -T +#Z #Y #X #IH #G #L * * // +[ #i #HG #HL #HT #H #d destruct + elim (lt_or_ge i (|L|)) /2 width=1 by lsx_lref_free/ + elim (ylt_split i d) /2 width=1 by lsx_lref_skip/ + #Hdi #Hi elim (ldrop_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 #d destruct + elim (csx_fwd_bind … H) -H /3 width=1 by lsx_bind/ +| #I #V #T #HG #HL #HT #H #d destruct + elim (csx_fwd_flat … H) -H /3 width=1 by lsx_flat/ +] qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/lsx_ldrop.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/lsx_ldrop.ma index 261168b92..cdb3f2fbc 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/lsx_ldrop.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/lsx_ldrop.ma @@ -13,6 +13,7 @@ (**************************************************************************) include "basic_2/substitution/lleq_ldrop.ma". +include "basic_2/computation/lpxs_ldrop.ma". include "basic_2/computation/lsx.ma". (* SN EXTENDED STRONGLY NORMALIZING LOCAL ENVIRONMENTS **********************) @@ -30,3 +31,52 @@ lemma lsx_lref_skip: ∀h,g,G,L,d,i. yinj i < d → G ⊢ ⋕⬊*[h, g, #i, d] L #L2 #HL12 #H elim H -H /3 width=4 by lpxs_fwd_length, lleq_skip/ qed. + +(* Properties on relocation *************************************************) + +lemma lsx_lift_le: ∀h,g,G,K,T,U,dt,d,e. dt ≤ yinj d → + ⇧[d, e] T ≡ U → G ⊢ ⋕⬊*[h, g, T, dt] K → + ∀L. ⇩[Ⓕ, d, e] L ≡ K → G ⊢ ⋕⬊*[h, g, U, dt] L. +#h #g #G #K #T #U #dt #d #e #Hdtd #HTU #H @(lsx_ind … H) -K +#K1 #_ #IHK1 #L1 #HLK1 @lsx_intro +#L2 #HL12 #HnU elim (lpxs_ldrop_conf … HLK1 … HL12) -HL12 +/4 width=10 by lleq_lift_le/ +qed-. + +lemma lsx_lift_ge: ∀h,g,G,K,T,U,dt,d,e. yinj d ≤ dt → + ⇧[d, e] T ≡ U → G ⊢ ⋕⬊*[h, g, T, dt] K → + ∀L. ⇩[Ⓕ, d, e] L ≡ K → G ⊢ ⋕⬊*[h, g, U, dt + e] L. +#h #g #G #K #T #U #dt #d #e #Hddt #HTU #H @(lsx_ind … H) -K +#K1 #_ #IHK1 #L1 #HLK1 @lsx_intro +#L2 #HL12 #HnU elim (lpxs_ldrop_conf … HLK1 … HL12) -HL12 +/4 width=9 by lleq_lift_ge/ +qed-. + +(* Inversion lemmas on relocation *******************************************) + +lemma lsx_inv_lift_le: ∀h,g,G,L,T,U,dt,d,e. dt ≤ yinj d → + ⇧[d, e] T ≡ U → G ⊢ ⋕⬊*[h, g, U, dt] L → + ∀K. ⇩[Ⓕ, d, e] L ≡ K → G ⊢ ⋕⬊*[h, g, T, dt] K. +#h #g #G #L #T #U #dt #d #e #Hdtd #HTU #H @(lsx_ind … H) -L +#L1 #_ #IHL1 #K1 #HLK1 @lsx_intro +#K2 #HK12 #HnT elim (ldrop_lpxs_trans … HLK1 … HK12) -HK12 +/4 width=10 by lleq_inv_lift_le/ +qed-. + +lemma lsx_inv_lift_be: ∀h,g,G,L,T,U,dt,d,e. yinj d ≤ dt → dt ≤ d + e → + ⇧[d, e] T ≡ U → G ⊢ ⋕⬊*[h, g, U, dt] L → + ∀K. ⇩[Ⓕ, d, e] L ≡ K → G ⊢ ⋕⬊*[h, g, T, d] K. +#h #g #G #L #T #U #dt #d #e #Hddt #Hdtde #HTU #H @(lsx_ind … H) -L +#L1 #_ #IHL1 #K1 #HLK1 @lsx_intro +#K2 #HK12 #HnT elim (ldrop_lpxs_trans … HLK1 … HK12) -HK12 +/4 width=11 by lleq_inv_lift_be/ +qed-. + +lemma lsx_inv_lift_ge: ∀h,g,G,L,T,U,dt,d,e. yinj d + yinj e ≤ dt → + ⇧[d, e] T ≡ U → G ⊢ ⋕⬊*[h, g, U, dt] L → + ∀K. ⇩[Ⓕ, d, e] L ≡ K → G ⊢ ⋕⬊*[h, g, T, dt-e] K. +#h #g #G #L #T #U #dt #d #e #Hdedt #HTU #H @(lsx_ind … H) -L +#L1 #_ #IHL1 #K1 #HLK1 @lsx_intro +#K2 #HK12 #HnT elim (ldrop_lpxs_trans … HLK1 … HK12) -HK12 +/4 width=9 by lleq_inv_lift_ge/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/lsx_lpxs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/lsx_lpxs.ma index 8f2603102..b3cb36781 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/lsx_lpxs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/lsx_lpxs.ma @@ -31,6 +31,12 @@ lemma lsx_leqy_conf: ∀h,g,G,L1,T,d. G ⊢ ⋕⬊*[h, g, T, d] L1 → #_ #H @(IHL1 … H1L10) -IHL1 -H1L10 /3 width=1 by/ qed-. +lemma lsx_ge: ∀h,g,G,L,T,d1,d2. d1 ≤ d2 → + G ⊢ ⋕⬊*[h, g, T, d1] L → G ⊢ ⋕⬊*[h, g, T, d2] L. +#h #g #G #L #T #d1 #d2 #Hd12 #H @(lsx_ind … H) -L +/5 width=7 by lsx_intro, lleq_ge/ +qed-. + lemma lsx_lleq_trans: ∀h,g,T,G,L1,d. G ⊢ ⋕⬊*[h, g, T, d] L1 → ∀L2. L1 ⋕[T, d] L2 → G ⊢ ⋕⬊*[h, g, T, d] L2. #h #g #T #G #L1 #d #H @(lsx_ind … H) -L1 @@ -95,12 +101,9 @@ lemma lsx_fwd_lref_be: ∀h,g,I,G,L,d,i. d ≤ yinj i → G ⊢ ⋕⬊*[h, g, #i #L1 #_ #IHL1 #K1 #V #HLK1 @lsx_intro #K2 #HK12 #HnK12 lapply (ldrop_fwd_drop2 … HLK1) #H2LK1 elim (ldrop_lpxs_trans … H2LK1 … HK12) -H2LK1 -HK12 -#L2 #HL12 #H2LK2 #HL21 elim (lsuby_ldrop_trans_be … HL21 … HLK1) -HL21 /2 width=1 by ylt_inj/ -#J #Y #_ #HLK2 lapply (ldrop_fwd_drop2 … HLK2) +#L2 #HL12 #H2LK2 #H elim (leq_ldrop_conf_be … H … HLK1) -H /2 width=1 by ylt_inj/ +#Y #_ #HLK2 lapply (ldrop_fwd_drop2 … HLK2) #HY lapply (ldrop_mono … HY … H2LK2) -HY -H2LK2 #H destruct -elim (lpxs_ldrop_conf … HLK1 … HL12) #Y #H #HY -elim (lpxs_inv_pair1 … H) -H #Z #X #_ #_ #H destruct -lapply (ldrop_mono … HY … HLK2) -HY #H destruct /4 width=10 by lleq_inv_lref_ge/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/append/cir_append.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/append/cir_append.etc new file mode 100644 index 000000000..efd097f84 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/append/cir_append.etc @@ -0,0 +1,34 @@ +(**************************************************************************) +(* ___ *) +(* ||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/crr_append.ma". +include "basic_2/reduction/cir.ma". + +(* IRREDUCIBLE TERMS FOR CONTEXT-SENSITIVE REDUCTION ************************) + +(* Advanved properties ******************************************************) + +lemma cir_labst_last: ∀G,L,T,W. ⦃G, L⦄ ⊢ ➡ 𝐈⦃T⦄ → ⦃G, ⋆.ⓛW @@ L⦄ ⊢ ➡ 𝐈⦃T⦄. +/3 width=2 by crr_inv_labst_last/ qed. + +lemma cir_tif: ∀G,T,W. ⦃G, ⋆⦄ ⊢ ➡ 𝐈⦃T⦄ → ⦃G, ⋆.ⓛW⦄ ⊢ ➡ 𝐈⦃T⦄. +/3 width=2 by crr_inv_trr/ qed. + +(* Advanced inversion lemmas ************************************************) + +lemma cir_inv_append_sn: ∀G,L,K,T. ⦃G, K @@ L⦄ ⊢ ➡ 𝐈⦃T⦄ → ⦃G, L⦄ ⊢ ➡ 𝐈⦃T⦄. +/3 width=1/ qed-. + +lemma cir_inv_tir: ∀G,T,W. ⦃G, ⋆.ⓛW⦄ ⊢ ➡ 𝐈⦃T⦄ → ⦃G, ⋆⦄ ⊢ ➡ 𝐈⦃T⦄. +/3 width=1/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/append/cix_append.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/append/cix_append.etc new file mode 100644 index 000000000..7b5522ebd --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/append/cix_append.etc @@ -0,0 +1,26 @@ +(**************************************************************************) +(* ___ *) +(* ||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/crx_append.ma". +include "basic_2/reduction/cix.ma". + +(* IRREDUCIBLE TERMS FOR CONTEXT-SENSITIVE EXTENDED REDUCTION ***************) + +(* Advanced inversion lemmas ************************************************) + +lemma cix_inv_append_sn: ∀h,g,G,L,K,T. ⦃G, K @@ L⦄ ⊢ ➡[h, g] 𝐈⦃T⦄ → ⦃G, L⦄ ⊢ ➡[h, g] 𝐈⦃T⦄. +/3 width=1 by crx_append_sn/ qed-. + +lemma cix_inv_tix: ∀h,g,G,L,T. ⦃G, L⦄ ⊢ ➡[h, g] 𝐈⦃T⦄ → ⦃G, ⋆⦄ ⊢ ➡[h, g] 𝐈⦃T⦄. +/3 width=1 by trx_crx/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/append/cl_shift.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/append/cl_shift.etc new file mode 100644 index 000000000..5fdab7148 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/append/cl_shift.etc @@ -0,0 +1,45 @@ +(**************************************************************************) +(* ___ *) +(* ||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_append.ma". + +(* SHIFT OF A CLOSURE *******************************************************) + +let rec shift L T on L ≝ match L with +[ LAtom ⇒ T +| LPair L I V ⇒ shift L (-ⓑ{I} V. T) +]. + +interpretation "shift (closure)" 'Append L T = (shift L T). + +(* Basic properties *********************************************************) + +lemma shift_append_assoc: ∀L,K. ∀T:term. (L @@ K) @@ T = L @@ K @@ T. +#L #K elim K -K // normalize // +qed. + +(* Basic inversion lemmas ***************************************************) + +lemma shift_inj: ∀L1,L2. ∀T1,T2:term. L1 @@ T1 = L2 @@ T2 → |L1| = |L2| → + L1 = L2 ∧ T1 = T2. +#L1 elim L1 -L1 +[ * normalize /2 width=1/ + #L2 #I2 #V2 #T1 #T2 #_ shift_append_assoc normalize #H + elim (cpr_inv_bind1 … H) -H * + [ #V0 #T0 #_ #HT10 #H destruct + elim (IH … HT10) -IH -HT10 #L2 #T2 #HL12 #H destruct + >append_length >HL12 -HL12 + @(ex2_2_intro … (⋆.ⓑ{I}V0@@L2) T2) [ >append_length ] /2 width=3 by trans_eq/ (**) (* explicit constructor *) + | #T #_ #_ #H destruct + ] +] +qed-. + diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/append/cpx.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/append/cpx.etc new file mode 100644 index 000000000..5f8bf520c --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/append/cpx.etc @@ -0,0 +1,25 @@ +lemma cpx_append: ∀h,g,G. l_appendable_sn … (cpx h g G). +#h #g #G #K #T1 #T2 #H elim H -G -K -T1 -T2 +/2 width=3 by cpx_sort, cpx_bind, cpx_flat, cpx_zeta, cpx_tau, cpx_ti, cpx_beta, cpx_theta/ +#I #G #K #K0 #V1 #V2 #W2 #i #HK0 #_ #HVW2 #IHV12 #L +lapply (ldrop_fwd_length_lt2 … HK0) #H +@(cpx_delta … I … (L@@K0) V1 … HVW2) // +@(ldrop_O1_append_sn_le … HK0) /2 width=2 by lt_to_le/ (**) (* /3/ does not work *) +qed. + +lemma cpx_fwd_shift1: ∀h,g,G,L1,L,T1,T. ⦃G, L⦄ ⊢ L1 @@ T1 ➡[h, g] T → + ∃∃L2,T2. |L1| = |L2| & T = L2 @@ T2. +#h #g #G #L1 @(lenv_ind_dx … L1) -L1 normalize +[ #L #T1 #T #HT1 + @(ex2_2_intro … (⋆)) // (**) (* explicit constructor *) +| #I #L1 #V1 #IH #L #T1 #X + >shift_append_assoc normalize #H + elim (cpx_inv_bind1 … H) -H * + [ #V0 #T0 #_ #HT10 #H destruct + elim (IH … HT10) -IH -HT10 #L2 #T2 #HL12 #H destruct + >append_length >HL12 -HL12 + @(ex2_2_intro … (⋆.ⓑ{I}V0@@L2) T2) [ >append_length ] /2 width=3 by refl, trans_eq/ (**) (* explicit constructor *) + | #T #_ #_ #H destruct + ] +] +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/append/crr_append.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/append/crr_append.etc new file mode 100644 index 000000000..dbf794d99 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/append/crr_append.etc @@ -0,0 +1,56 @@ +(**************************************************************************) +(* ___ *) +(* ||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_append.ma". +include "basic_2/reduction/crr.ma". + +(* REDUCIBLE TERMS FOR CONTEXT-SENSITIVE REDUCTION **************************) + +(* Advanved properties ******************************************************) + +lemma crr_append_sn: ∀G,L,K,T. ⦃G, L⦄ ⊢ ➡ 𝐑⦃T⦄ → ⦃G, K @@ L⦄ ⊢ ➡ 𝐑⦃T⦄. +#G #L #K0 #T #H elim H -L -T /2 width=1/ +#L #K #V #i #HLK +lapply (ldrop_fwd_length_lt2 … HLK) #Hi +lapply (ldrop_O1_append_sn_le … HLK … K0) -HLK /2 width=2/ -Hi /2 width=3/ +qed. + +lemma trr_crr: ∀G,L,T. ⦃G, ⋆⦄ ⊢ ➡ 𝐑⦃T⦄ → ⦃G, L⦄ ⊢ ➡ 𝐑⦃T⦄. +#G #L #T #H lapply (crr_append_sn … H) // +qed. + +(* Advanced inversion lemmas ************************************************) + +fact crr_inv_labst_last_aux: ∀G,L1,T,W. ⦃G, L1⦄ ⊢ ➡ 𝐑⦃T⦄ → + ∀L2. L1 = ⋆.ⓛW @@ L2 → ⦃G, L2⦄ ⊢ ➡ 𝐑⦃T⦄. +#G #L1 #T #W #H elim H -L1 -T /2 width=1/ /3 width=1/ +[ #L1 #K1 #V1 #i #HLK1 #L2 #H destruct + lapply (ldrop_fwd_length_lt2 … HLK1) + >append_length >commutative_plus normalize in ⊢ (??% → ?); #H + elim (le_to_or_lt_eq i (|L2|)) /2 width=1/ -H #Hi destruct + [ elim (ldrop_O1_lt … Hi) #I2 #K2 #V2 #HLK2 + lapply (ldrop_O1_inv_append1_le … HLK1 … HLK2) -HLK1 /2 width=2/ -Hi + normalize #H destruct /2 width=3/ + | lapply (ldrop_O1_inv_append1_ge … HLK1 ?) -HLK1 // commutative_plus normalize #H destruct +| minus_minus_comm /3 width=1 by monotonic_pred/ +] +qed-. + +lemma ldrop_O1_inv_append1_le: ∀K,L1,L2,s,e. ⇩[s, 0, e] L1 @@ L2 ≡ K → e ≤ |L2| → + ∀K2. ⇩[s, 0, e] L2 ≡ K2 → K = L1 @@ K2. +#K #L1 #L2 elim L2 -L2 normalize +[ #s #e #H1 #H2 #K2 #H3 lapply (le_n_O_to_eq … H2) -H2 + #H2 elim (ldrop_inv_atom1 … H3) -H3 #H3 #_ destruct + >(ldrop_inv_O2 … H1) -H1 // +| #L2 #I #V #IHL2 #s #e @(nat_ind_plus … e) -e [ -IHL2 ] + [ #H1 #_ #K2 #H2 + lapply (ldrop_inv_O2 … H1) -H1 #H1 + lapply (ldrop_inv_O2 … H2) -H2 #H2 destruct // + | /4 width=7 by ldrop_inv_drop1, le_plus_to_le_r/ + ] +] +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/append/lpr.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/append/lpr.etc new file mode 100644 index 000000000..5b550111d --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/append/lpr.etc @@ -0,0 +1,13 @@ +lemma lpr_append: ∀G,K1,K2. ⦃G, K1⦄ ⊢ ➡ K2 → ∀L1,L2. ⦃G, L1⦄ ⊢ ➡ L2 → + ⦃G, L1 @@ K1⦄ ⊢ ➡ L2 @@ K2. +/3 width=1 by lpx_sn_append, cpr_append/ qed. + +(* Advanced forward lemmas **************************************************) + +lemma lpr_fwd_append1: ∀G,K1,L1,L. ⦃G, K1 @@ L1⦄ ⊢ ➡ L → + ∃∃K2,L2. ⦃G, K1⦄ ⊢ ➡ K2 & L = K2 @@ L2. +/2 width=2 by lpx_sn_fwd_append1/ qed-. + +lemma lpr_fwd_append2: ∀G,L,K2,L2. ⦃G, L⦄ ⊢ ➡ K2 @@ L2 → + ∃∃K1,L1. ⦃G, K1⦄ ⊢ ➡ K2 & L = K1 @@ L1. +/2 width=2 by lpx_sn_fwd_append2/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/append/lpx.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/append/lpx.etc new file mode 100644 index 000000000..a1976d5d1 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/append/lpx.etc @@ -0,0 +1,13 @@ +lemma lpx_append: ∀h,g,G,K1,K2. ⦃G, K1⦄ ⊢ ➡[h, g] K2 → ∀L1,L2. ⦃G, L1⦄ ⊢ ➡[h, g] L2 → + ⦃G, L1 @@ K1⦄ ⊢ ➡[h, g] L2 @@ K2. +/3 width=1 by lpx_sn_append, cpx_append/ qed. + +(* Advanced forward lemmas **************************************************) + +lemma lpx_fwd_append1: ∀h,g,G,K1,L1,L. ⦃G, K1 @@ L1⦄ ⊢ ➡[h, g] L → + ∃∃K2,L2. ⦃G, K1⦄ ⊢ ➡[h, g] K2 & L = K2 @@ L2. +/2 width=2 by lpx_sn_fwd_append1/ qed-. + +lemma lpx_fwd_append2: ∀h,g,G,L,K2,L2. ⦃G, L⦄ ⊢ ➡[h, g] K2 @@ L2 → + ∃∃K1,L1. ⦃G, K1⦄ ⊢ ➡[h, g] K2 & L = K1 @@ L1. +/2 width=2 by lpx_sn_fwd_append2/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/append/lpx_sn.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/append/lpx_sn.etc new file mode 100644 index 000000000..d399e0a3b --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/append/lpx_sn.etc @@ -0,0 +1,31 @@ +lemma lpx_sn_append: ∀R. l_appendable_sn R → + ∀K1,K2. lpx_sn R K1 K2 → ∀L1,L2. lpx_sn R L1 L2 → + lpx_sn R (L1 @@ K1) (L2 @@ K2). +#R #HR #K1 #K2 #H elim H -K1 -K2 /3 width=1 by lpx_sn_pair/ +qed-. + +(* Advanced forward lemmas **************************************************) + +lemma lpx_sn_fwd_append1: ∀R,L1,K1,L. lpx_sn R (K1 @@ L1) L → + ∃∃K2,L2. lpx_sn R K1 K2 & L = K2 @@ L2. +#R #L1 elim L1 -L1 +[ #K1 #K2 #HK12 + @(ex2_2_intro … K2 (⋆)) // (* explicit constructor, /2 width=4/ does not work *) +| #L1 #I #V1 #IH #K1 #X #H + elim (lpx_sn_inv_pair1 … H) -H #L #V2 #H1 #HV12 #H destruct + elim (IH … H1) -IH -H1 #K2 #L2 #HK12 #H destruct + @(ex2_2_intro … (L2.ⓑ{I}V2) HK12) // (* explicit constructor, /2 width=4/ does not work *) +] +qed-. + +lemma lpx_sn_fwd_append2: ∀R,L2,K2,L. lpx_sn R L (K2 @@ L2) → + ∃∃K1,L1. lpx_sn R K1 K2 & L = K1 @@ L1. +#R #L2 elim L2 -L2 +[ #K2 #K1 #HK12 + @(ex2_2_intro … K1 (⋆)) // (**) (* explicit constructor, /2 width=4/ does not work *) +| #L2 #I #V2 #IH #K2 #X #H + elim (lpx_sn_inv_pair2 … H) -H #L #V1 #H1 #HV12 #H destruct + elim (IH … H1) -IH -H1 #K1 #L1 #HK12 #H destruct + @(ex2_2_intro … (L1.ⓑ{I}V1) HK12) // (* explicit constructor, /2 width=4/ does not work *) +] +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/lcoeq/coeq_4.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/lcoeq/coeq_4.etc new file mode 100644 index 000000000..8abd1ee30 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/lcoeq/coeq_4.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( L1 ≅ break [ term 46 d , break term 46 e ] break term 46 L2 )" + non associative with precedence 45 + for @{ 'CoEq $d $e $L1 $L2 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/lcoeq/lcoeq.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/lcoeq/lcoeq.etc new file mode 100644 index 000000000..5338c2aeb --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/lcoeq/lcoeq.etc @@ -0,0 +1,165 @@ +(**************************************************************************) +(* ___ *) +(* ||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 "ground_2/ynat/ynat_lt.ma". +include "basic_2/notation/relations/coeq_4.ma". +include "basic_2/grammar/lenv_length.ma". + +(* COEQUIVALENCE FOR LOCAL ENVIRONMENTS *************************************) + +inductive lcoeq: relation4 ynat ynat lenv lenv ≝ +| lcoeq_atom: ∀d,e. lcoeq d e (⋆) (⋆) +| lcoeq_zero: ∀I,L1,L2,V. + lcoeq 0 0 L1 L2 → lcoeq 0 0 (L1.ⓑ{I}V) (L2.ⓑ{I}V) +| lcoeq_pair: ∀I1,I2,L1,L2,V1,V2,e. lcoeq 0 e L1 L2 → + lcoeq 0 (⫯e) (L1.ⓑ{I1}V1) (L2.ⓑ{I2}V2) +| lcoeq_succ: ∀I,L1,L2,V,d,e. + lcoeq d e L1 L2 → lcoeq (⫯d) e (L1.ⓑ{I}V) (L2.ⓑ{I}V) +. + +interpretation + "coequivalence (local environment)" + 'CoEq d e L1 L2 = (lcoeq d e L1 L2). + +(* Basic properties *********************************************************) + +lemma lcoeq_pair_lt: ∀I1,I2,L1,L2,V1,V2,e. L1 ≅[0, ⫰e] L2 → 0 < e → + L1.ⓑ{I1}V1 ≅[0, e] L2.ⓑ{I2}V2. +#I1 #I2 #L1 #L2 #V1 #V2 #e #HL12 #He <(ylt_inv_O1 … He) /2 width=1 by lcoeq_pair/ +qed. + +lemma lcoeq_succ_lt: ∀I,L1,L2,V,d,e. L1 ≅[⫰d, e] L2 → 0 < d → + L1.ⓑ{I}V ≅[d, e] L2. ⓑ{I}V. +#I #L1 #L2 #V #d #e #HL12 #Hd <(ylt_inv_O1 … Hd) /2 width=1 by lcoeq_succ/ +qed. + +lemma lcoeq_pair_O_Y: ∀L1,L2. L1 ≅[0, ∞] L2 → + ∀I1,I2,V1,V2. L1.ⓑ{I1}V1 ≅[0,∞] L2.ⓑ{I2}V2. +#L1 #L2 #HL12 #I1 #I2 #V1 #V2 lapply (lcoeq_pair I1 I2 … V1 V2 … HL12) -HL12 // +qed. + +lemma lcoeq_refl: ∀L,d,e. L ≅[d, e] L. +#L elim L -L // +#L #I #V #IHL #d elim (ynat_cases … d) [| * #x ] +#Hd destruct /2 width=1 by lcoeq_succ/ +#e elim (ynat_cases … e) [| * #x ] +#He destruct /2 width=1 by lcoeq_zero, lcoeq_pair/ +qed. + +lemma lcoeq_O_Y: ∀L1,L2. |L1| = |L2| → L1 ≅[0, ∞] L2. +#L1 elim L1 -L1 [| #L1 #I1 #V1 #IHL1 ] +* [2,4: #L2 #I2 #V1 ] normalize /3 width=2 by lcoeq_pair_O_Y/ +(lcoeq_inv_O2 … HL1) -HL1 // +| #I1 #I #L1 #L #V1 #V #e #_ #IHL1 #X #H elim (lcoeq_inv_pair1 … H) -H // + #I2 #L2 #V2 #HL2 #H destruct /3 width=1 by lcoeq_pair/ +| #I #L1 #L #V #d #e #_ #IHL1 #X #H elim (lcoeq_inv_succ1 … H) -H // + #L2 #HL2 #H destruct /3 width=1 by lcoeq_succ/ +] +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/lcoeq/ldrop_lcoeq.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/lcoeq/ldrop_lcoeq.etc new file mode 100644 index 000000000..4891949c2 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/lcoeq/ldrop_lcoeq.etc @@ -0,0 +1,51 @@ +(**************************************************************************) +(* ___ *) +(* ||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 "ground_2/ynat/ynat_minus.ma". +include "basic_2/grammar/lcoeq.ma". +include "basic_2/relocation/ldrop.ma". + +(* BASIC SLICING FOR LOCAL ENVIRONMENTS *************************************) + +(* Properties on coequivalence **********************************************) + +lemma lcoeq_ldrop_trans_lt: ∀L1,L2,d,e. L1 ≅[d, e] L2 → + ∀I,K2,W,s,i. ⇩[s, 0, i] L2 ≡ K2.ⓑ{I}W → i < d → + ∃∃K1. K1 ≅[⫰(d-i), e] K2 & ⇩[s, 0, i] L1 ≡ K1.ⓑ{I}W. +#L1 #L2 #d #e #H elim H -L1 -L2 -d -e +[ #d #e #J #K2 #W #s #i #H + elim (ldrop_inv_atom1 … H) -H #H destruct +| #I #L1 #L2 #V #_ #_ #J #K2 #W #s #i #_ #H + elim (ylt_yle_false … H) // +| #I1 #I2 #L1 #L2 #V1 #V2 #e #_ #_ #J #K2 #W #s #i #_ #H + elim (ylt_yle_false … H) // +| #I #L1 #L2 #V #d #e #HL12 #IHL12 #J #K2 #W #s #i #H + elim (ldrop_inv_O1_pair1 … H) -H * #Hi #HLK1 [ -IHL12 | -HL12 ] + [ #_ destruct >ypred_succ + /2 width=3 by ldrop_pair, ex2_intro/ + | lapply (ylt_inv_O1 i ?) /2 width=1 by ylt_inj/ + #H yminus_succ yminus_Y_inj #J #Y #X #HK12 #H lapply (ldrop_mono … H … HLK2) -L2 - #H destruct /3 width=7 by cpx_delta/ - | #J #K1 #V #HLK1 #_ #HV1 #Hid elim (ldrop_leq_conf_lt … HL12 … HLK1) -HL12 /2 width=1 by ylt_inj/ - yminus_inj #Y #HK12 #H lapply (ldrop_mono … H … HLK2) -L2 - #H destruct /3 width=7 by cpx_delta/ - ] -| #a #I #G #L2 #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #L1 #d #H elim (lleq_inv_bind … H) -H - /4 width=3 by cpx_bind, leq_succ/ -| #I #G #L2 #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #L1 #d #H elim (lleq_inv_flat … H) -H - /3 width=3 by cpx_flat/ -| #G #L2 #V2 #T1 #T #T2 #_ #HT2 #IHT1 #L1 #d #H elim (lleq_inv_bind … H) -H - /4 width=3 by cpx_zeta, leq_succ/ -| #G #L2 #W1 #T1 #T2 #_ #IHT12 #L1 #d #H elim (lleq_inv_flat … H) -H - /3 width=3 by cpx_tau/ -| #G #L2 #W1 #W2 #T1 #_ #IHW12 #L1 #d #H elim (lleq_inv_flat … H) -H - /3 width=3 by cpx_ti/ -| #a #G #L1 #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #IHV12 #IHW12 #IHT12 #L1 #d #H elim (lleq_inv_flat … H) -H - #HV1 #H elim (lleq_inv_bind … H) -H /4 width=3 by cpx_beta, leq_succ/ -| #a #G #L1 #V1 #V #V2 #W1 #W2 #T1 #T2 #_ #HV2 #_ #_ #IHV1 #IHW12 #IHT12 #L1 #d #H elim (lleq_inv_flat … H) -H - #HV1 #H elim (lleq_inv_bind … H) -H /4 width=3 by cpx_theta, leq_succ/ -] -qed-. - -(* Note: this can be proved directly *) -lemma lleq_cpx_trans: ∀h,g,G,L2,T1,T2. ⦃G, L2⦄ ⊢ T1 ➡[h, g] T2 → - ∀L1. L1 ⋕[0, T1] L2 → ⦃G, L1⦄ ⊢ T1 ➡[h, g] T2. -/4 width=6 by lleq_cpx_trans_leq, lleq_fwd_length, leq_O_Y/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/leq/iso_4.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/leq/iso_4.etc deleted file mode 100644 index 8a3617c1b..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/etc/leq/iso_4.etc +++ /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( L1 ≃ break [ term 46 d , break term 46 e ] break term 46 L2 )" - non associative with precedence 45 - for @{ 'Iso $d $e $L1 $L2 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/leq/ldrop_leq.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/leq/ldrop_leq.etc deleted file mode 100644 index 179bb5f05..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/etc/leq/ldrop_leq.etc +++ /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 "ground_2/ynat/ynat_plus.ma". -include "basic_2/grammar/leq.ma". -include "basic_2/relocation/ldrop.ma". - -(* BASIC SLICING FOR LOCAL ENVIRONMENTS *************************************) - -lemma ldrop_leq_conf_ge: ∀L1,L2,d,e. L1 ≃[d, e] L2 → - ∀I,K,V,i. ⇩[O, i]L1 ≡ K.ⓑ{I}V → d + e ≤ i → - ⇩[O, i]L2 ≡ K.ⓑ{I}V. -#L1 #L2 #d #e #H elim H -L1 -L2 -d -e -[ #d #e #J #K #W #i #H elim (ldrop_inv_atom1 … H) -H - #H destruct -| #I #L1 #L2 #V #HL12 #IHL12 #J #K #W #i #H #_ elim (ldrop_inv_O1_pair1 … H) -H - * #H1 #H2 - [ -IHL12 lapply (leq_inv_O2 … HL12) -HL12 - #H3 destruct // - | -HL12 /4 width=1 by ldrop_ldrop_lt, yle_inj/ - ] -| #I1 #I2 #L1 #L2 #V1 #V2 #e #_ #IHL12 #J #K #W #i #H1 >yplus_succ_swap - #Hei elim (yle_inv_inj2 … Hei) -Hei - #x #Hei #H elim (yplus_inv_inj … H) -H normalize - #y #z >commutative_plus - #H1 #H2 #H3 destruct elim (le_inv_plus_l … Hei) -Hei - #Hzi #Hi lapply (ldrop_inv_ldrop1_lt … H1 ?) -H1 - /4 width=1 by ldrop_ldrop_lt, yle_inj/ -| #I #L1 #L2 #V #d #e #_ #IHL12 #J #K #W #i #H0 #Hdei elim (yle_inv_inj2 … Hdei) -Hdei - #x #Hdei #H elim (yplus_inv_inj … H) -H - #y #z >commutative_plus - #H1 #H2 #H3 destruct elim (ysucc_inv_inj_dx … H2) -H2 - #x #H1 #H2 destruct elim (le_inv_plus_l … Hdei) - #_ #Hi lapply (ldrop_inv_ldrop1_lt … H0 ?) -H0 - [2: #H0 @ldrop_ldrop_lt ] [2,3: /2 width=3 by lt_to_le_to_lt/ ] - /4 width=3 by yle_inj, monotonic_pred/ -] -qed-. - -lemma ldrop_leq_conf_be: ∀L1,L2,d,e. L1 ≃[d, e] L2 → - ∀I1,K1,V1,i. ⇩[O, i]L1 ≡ K1.ⓑ{I1}V1 → d ≤ i → i < d + e → - ∃∃I2,K2,V2. K1 ≃[0, ⫰(d+e-i)] K2 & ⇩[O, i]L2 ≡ K2.ⓑ{I2}V2. -#L1 #L2 #d #e #H elim H -L1 -L2 -d -e -[ #d #e #J1 #K1 #W1 #i #H elim (ldrop_inv_atom1 … H) -H - #H destruct -| #I #L1 #L2 #V #HL12 #IHL12 #J1 #K1 #W1 #i #_ #_ #H elim (ylt_yle_false … H) // -| #I1 #I2 #L1 #L2 #V1 #V2 #e #HL12 >yplus_O1 >yplus_O1 - #IHL12 #J1 #K1 #W1 #i #H #_ elim (eq_or_gt i) #Hi destruct [ -IHL12 | -HL12 ] - [ #_ lapply (ldrop_inv_O2 … H) -H - #H destruct >ypred_succ /2 width=5 by ldrop_pair, ex2_3_intro/ - | lapply (ldrop_inv_ldrop1_lt … H ?) -H // - #H <(ylt_inv_O1 i) /2 width=1 by ylt_inj/ - #Hie lapply (ylt_inv_succ … Hie) -Hie - #Hie elim (IHL12 … H) -IHL12 -H // - >yminus_succ /3 width=5 by ldrop_ldrop_lt, ex2_3_intro/ - ] -| #I #L1 #L2 #V #d #e #_ #IHL12 #J1 #K1 #W1 #i #H #Hdi lapply (ylt_yle_trans 0 … Hdi ?) // - #Hi <(ylt_inv_O1 … Hi) >yplus_succ1 >yminus_succ elim (yle_inv_succ1 … Hdi) -Hdi - #Hdi #_ #Hide lapply (ylt_inv_succ … Hide) - #Hide lapply (ylt_inv_inj … Hi) -Hi - #Hi lapply (ldrop_inv_ldrop1_lt … H ?) -H // - #H elim (IHL12 … H) -IHL12 -H - /3 width=5 by ldrop_ldrop_lt, ex2_3_intro/ -] -qed-. - -lemma ldrop_leq_conf_lt: ∀L1,L2,d,e. L1 ≃[d, e] L2 → - ∀I,K1,V,i. ⇩[O, i]L1 ≡ K1.ⓑ{I}V → i < d → - ∃∃K2. K1 ≃[⫰(d-i), e] K2 & ⇩[O, i]L2 ≡ K2.ⓑ{I}V. -#L1 #L2 #d #e #H elim H -L1 -L2 -d -e -[ #d #e #J #K1 #W #i #H elim (ldrop_inv_atom1 … H) -H - #H destruct -| #I #L1 #L2 #V #_ #_ #J #K1 #W #i #_ #H elim (ylt_yle_false … H) // -| #I1 #I2 #L1 #L2 #V1 #V2 #e #_ #_ #J #K1 #W #i #_ #H elim (ylt_yle_false … H) // -| #I #L1 #L2 #V #d #e #HL12 #IHL12 #J #K1 #W #i #H elim (eq_or_gt i) #Hi destruct [ -IHL12 | -HL12 ] - [ #_ lapply (ldrop_inv_O2 … H) -H - #H destruct >ypred_succ /2 width=5 by ldrop_pair, ex2_intro/ - | lapply (ldrop_inv_ldrop1_lt … H ?) -H // - #H <(ylt_inv_O1 i) /2 width=1 by ylt_inj/ - #Hie lapply (ylt_inv_succ … Hie) -Hie - #Hie elim (IHL12 … H) -IHL12 -H - >yminus_succ /3 width=5 by ldrop_ldrop_lt, ex2_intro/ - ] -] -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/leq/leq.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/leq/leq.etc deleted file mode 100644 index 095e1ced3..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/etc/leq/leq.etc +++ /dev/null @@ -1,81 +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 "ground_2/ynat/ynat_succ.ma". -include "basic_2/notation/relations/iso_4.ma". -include "basic_2/grammar/lenv_length.ma". - -(* EQUIVALENCE FOR LOCAL ENVIRONMENTS ***************************************) - -inductive leq: ynat → ynat → relation lenv ≝ -| leq_atom: ∀d,e. leq d e (⋆) (⋆) -| leq_zero: ∀I,L1,L2,V. leq 0 0 L1 L2 → leq 0 0 (L1.ⓑ{I}V) (L2.ⓑ{I}V) -| leq_pair: ∀I1,I2,L1,L2,V1,V2,e. - leq 0 e L1 L2 → leq 0 (⫯e) (L1.ⓑ{I1}V1) (L2.ⓑ{I2}V2) -| leq_succ: ∀I,L1,L2,V,d,e. leq d e L1 L2 → leq (⫯d) e (L1.ⓑ{I}V) (L2.ⓑ{I}V) -. - -interpretation - "equivalence (local environment)" - 'Iso d e L1 L2 = (leq d e L1 L2). - -(* Basic properties *********************************************************) - -lemma leq_refl: ∀L,d,e. L ≃[d, e] L. -#L elim L -L /2 width=1 by/ -#L #I #V #IHL #d #e elim (ynat_cases … d) [ | * /2 width=1 by leq_succ/ ] -elim (ynat_cases … e) [ | * ] -/2 width=1 by leq_zero, leq_pair/ -qed. - -lemma leq_sym: ∀L1,L2,d,e. L1 ≃[d, e] L2 → L2 ≃[d, e] L1. -#L1 #L2 #d #e #H elim H -L1 -L2 -d -e -/2 width=1 by leq_atom, leq_zero, leq_pair, leq_succ/ -qed-. - -lemma leq_O_Y: ∀L1,L2. |L1| = |L2| → L1 ≃[0, ∞] L2. -#L1 elim L1 -L1 -[ #X #H lapply (length_inv_zero_sn … H) -H // -| #L1 #I1 #V1 #IHL1 #X #H elim (length_inv_pos_sn … H) -H - #L2 #I2 #V2 #HL12 #H destruct - @(leq_pair … (∞)) /2 width=1 by/ (**) (* explicit constructor *) -] -qed. - -(* Basic forward lemmas *****************************************************) - -lemma leq_fwd_length: ∀L1,L2,d,e. L1 ≃[d, e] L2 → |L1| = |L2|. -#L1 #L2 #d #e #H elim H -L1 -L2 -d -e normalize // -qed-. - -(* Basic inversion lemmas ***************************************************) - -fact leq_inv_O2_aux: ∀L1,L2,d,e. L1 ≃[d, e] L2 → e = 0 → L1 = L2. -#L1 #L2 #d #e #H elim H -L1 -L2 -d -e /3 width=1 by eq_f3/ -#I1 #I2 #L1 #L2 #V1 #V2 #e #_ #_ #H elim (ysucc_inv_O_dx … H) -qed-. - -lemma leq_inv_O2: ∀L1,L2,d. L1 ≃[d, 0] L2 → L1 = L2. -/2 width=4 by leq_inv_O2_aux/ qed-. - -fact leq_inv_Y1_aux: ∀L1,L2,d,e. L1 ≃[d, e] L2 → d = ∞ → L1 = L2. -#L1 #L2 #d #e #H elim H -L1 -L2 -d -e /3 width=1 by eq_f3/ -[ #I1 #I2 #L1 #L2 #V1 #V2 #e #_ #_ #H destruct -| #I #L1 #L2 #V #d #e #_ #IHL12 #H lapply (ysucc_inv_Y_dx … H) -H - /3 width=1 by eq_f3/ -] -qed-. - -lemma leq_inv_Y1: ∀L1,L2,e. L1 ≃[∞, e] L2 → L1 = L2. -/2 width=4 by leq_inv_Y1_aux/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/leq/leq_nat.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/leq/leq_nat.etc deleted file mode 100644 index a21457b4e..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/etc/leq/leq_nat.etc +++ /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/grammar/lenv_length.ma". - -(* LOCAL ENVIRONMENT EQUALITY ***********************************************) - -notation "hvbox( T1 break [ d , break e ] ≈ break T2 )" - non associative with precedence 45 - for @{ 'Eq $T1 $d $e $T2 }. - -inductive leq: nat → nat → relation lenv ≝ -| leq_sort: ∀d,e. leq d e (⋆) (⋆) -| leq_OO: ∀L1,L2. leq 0 0 L1 L2 -| leq_eq: ∀L1,L2,I,V,e. leq 0 e L1 L2 → - leq 0 (e + 1) (L1. 𝕓{I} V) (L2.𝕓{I} V) -| leq_skip: ∀L1,L2,I1,I2,V1,V2,d,e. - leq d e L1 L2 → leq (d + 1) e (L1. 𝕓{I1} V1) (L2. 𝕓{I2} V2) -. - -interpretation "local environment equality" 'Eq L1 d e L2 = (leq d e L1 L2). - -definition leq_repl_dx: ∀S. (lenv → relation S) → Prop ≝ λS,R. - ∀L1,s1,s2. R L1 s1 s2 → - ∀L2,d,e. L1 [d, e]≈ L2 → R L2 s1 s2. - -(* Basic properties *********************************************************) - -lemma TC_leq_repl_dx: ∀S,R. leq_repl_dx S R → leq_repl_dx S (λL. (TC … (R L))). -#S #R #HR #L1 #s1 #s2 #H elim H -H s2 -[ /3 width=5/ -| #s #s2 #_ #Hs2 #IHs1 #L2 #d #e #HL12 - lapply (HR … Hs2 … HL12) -HR Hs2 HL12 /3/ -] -qed. - -lemma leq_refl: ∀d,e,L. L [d, e] ≈ L. -#d elim d -d -[ #e elim e -e // #e #IHe #L elim L -L /2/ -| #d #IHd #e #L elim L -L /2/ -] -qed. - -lemma leq_sym: ∀L1,L2,d,e. L1 [d, e] ≈ L2 → L2 [d, e] ≈ L1. -#L1 #L2 #d #e #H elim H -H L1 L2 d e /2/ -qed. - -lemma leq_skip_lt: ∀L1,L2,d,e. L1 [d - 1, e] ≈ L2 → 0 < d → - ∀I1,I2,V1,V2. L1. 𝕓{I1} V1 [d, e] ≈ L2. 𝕓{I2} V2. - -#L1 #L2 #d #e #HL12 #Hd >(plus_minus_m_m d 1) /2/ -qed. - -(* Basic inversion lemmas ***************************************************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/leq/leq_old.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/leq/leq_old.etc deleted file mode 100644 index 52b458ce4..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/etc/leq/leq_old.etc +++ /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 *) -(* *) -(**************************************************************************) - -axiom- lleq_inv_lref_lt_bi: ∀L1,L2,i,d. L1 ⋕[d, #i] L2 → i < d → - ∀I1,I2,K1,K2,V1,V2. ⇩[0, i] L1 ≡ K1.ⓑ{I1}V1 → ⇩[0, i] L2 ≡ K2.ⓑ{I2}V2 → - K1 ⋕[d-i-1, V1] K2 ∧ K1 ⋕[d-i-1, V2] K2. - -include "Basic-2/grammar/lenv_length.ma". - -(* LOCAL ENVIRONMENT EQUALITY ***********************************************) - -interpretation "local environment equality" 'Eq L1 d e L2 = (leq L1 d e L2). - -(* Basic properties *********************************************************) - -| leq_comp: ∀L1,L2,I1,I2,V1,V2. - leq L1 0 0 L2 → leq (L1. 𝕓{I1} V1) 0 0 (L2. 𝕓{I2} V2) - -lemma leq_fwd_length: ∀L1,L2,d,e. L1 [d, e] ≈ L2 → |L1| = |L2|. -#L1 #L2 #d #e #H elim H -H L1 L2 d e; normalize // -qed. - -(* Basic inversion lemmas ***************************************************) - -lemma leq_inv_sort1_aux: ∀L1,L2,d,e. L1 [d, e] ≈ L2 → L1 = ⋆ → L2 = ⋆. -#L1 #L2 #d #e #H elim H -H L1 L2 d e -[ // -| #L1 #L2 #I1 #I2 #V1 #V2 #_ #_ #H destruct -| #L1 #L2 #I #V #e #_ #_ #H destruct -| #L1 #L2 #I1 #I2 #V1 #V2 #d #e #_ #_ #H destruct -qed. - -lemma leq_inv_sort1: ∀L2,d,e. ⋆ [d, e] ≈ L2 → L2 = ⋆. -/2 width=5/ qed. - -lemma leq_inv_sort2: ∀L1,d,e. L1 [d, e] ≈ ⋆ → L1 = ⋆. -/3/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/leq/leqdx.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/leq/leqdx.etc deleted file mode 100644 index 63b43d876..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/etc/leq/leqdx.etc +++ /dev/null @@ -1,58 +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/leqdx_3.ma". -include "basic_2/grammar/lenv_length.ma". - -(* DX GUARDED EQUIVALENCE FOR LOCAL ENVIRONMENTS ****************************) - -inductive leqdx: nat → relation lenv ≝ -| leqdx_atom: ∀d. leqdx d (⋆) (⋆) -| leqdx_zero: ∀I1,I2,L1,L2,V1,V2. - leqdx 0 L1 L2 → leqdx 0 (L1.ⓑ{I1}V1) (L2.ⓑ{I2}V2) -| leqdx_succ: ∀I,L1,L2,V,d. - leqdx d L1 L2 → leqdx (d+1) (L1.ⓑ{I}V) (L2.ⓑ{I}V) -. - -interpretation - "guarded equivalence (local environment, dx variant)" - 'LEqDx d L1 L2 = (leqdx d L1 L2). - -(* Basic properties *********************************************************) - -lemma leqdx_O: ∀L1,L2. |L1| = |L2| → L1 ≚[0] L2. -#L1 elim L1 -L1 -[ #L2 #H >(length_inv_zero_sn … H) -L2 // -| #L1 #I1 #V1 #IHL1 #X #H elim (length_inv_pos_sn … H) -H - #I2 #L2 #V2 #HL12 #H destruct /3 width=1 by leqdx_zero/ -] -qed. - -(* Basic inversion lemmas ***************************************************) - -fact leqdx_inv_succ2_aux: ∀L1,L2,d. L1 ≚[d] L2 → - ∀I,K2,V,e. L2 = K2.ⓑ{I}V → d = e + 1 → - ∃∃K1. K1 ≚[e] K2 & L1 = K1.ⓑ{I}V. -#L1 #L2 #d * -L1 -L2 -d -[ #d #J #K2 #W #e #H destruct -| #I1 #I2 #L1 #L2 #V1 #V2 #_ #J #K2 #W #e #_ - >commutative_plus normalize #H destruct -| #I #L1 #L2 #V #d #HL12 #J #K2 #W #e #H1 #H2 destruct - /2 width=3 by ex2_intro/ -] -qed-. - -lemma leqdx_inv_succ2: ∀I,L1,K2,V,d. L1 ≚[d+1] K2.ⓑ{I}V → - ∃∃K1. K1 ≚[d] K2 & L1 = K1.ⓑ{I}V. -/2 width=5 by leqdx_inv_succ2_aux/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/leq/leqdx_3.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/leq/leqdx_3.etc deleted file mode 100644 index 54a9c5f50..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/etc/leq/leqdx_3.etc +++ /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( L1 ≚ break [ term 46 d ] break term 46 L2 )" - non associative with precedence 45 - for @{ 'LEqDx $d $L1 $L2 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/leq/lpx_leq.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/leq/lpx_leq.etc deleted file mode 100644 index b2b5324a6..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/etc/leq/lpx_leq.etc +++ /dev/null @@ -1,125 +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/reduction/cpx_leq.ma". -include "basic_2/reduction/lpx_ldrop.ma". - -(**) (* to be proved later *) -axiom- lleq_beta: ∀L2s,L2d,V2,W2,T2,d. - L2s.ⓛW2 ⋕[d+1, T2] L2d.ⓛW2 → - L2s.ⓓⓝW2.V2 ⋕[d+1, T2] L2d.ⓓⓝW2.V2. - -(* SN EXTENDED PARALLEL REDUCTION FOR LOCAL ENVIRONMENTS ********************) - -(* Properties using equivalences for local environments *********************) - -lemma lleq_cpx_conf_leq_dx: ∀h,g,G,L1s,L1d,T1,d. L1s ⋕[d, T1] L1d → L1s ≃[d, ∞] L1d → - ∀T2. ⦃G, L1d⦄ ⊢ T1 ➡[h, g] T2 → - ∀L2s. ⦃G, L1s⦄ ⊢ ➡[h, g] L2s → L1s ≃[0, d] L2s → - ∀L2d. ⦃G, L1d⦄ ⊢ ➡[h, g] L2d → L1d ≃[0, d] L2d → - L2s ≃[d, ∞] L2d → L2s ⋕[d, T2] L2d. -#h #g #G #L1s #L1d #T1 #d #H elim H -L1s -L1d -T1 -d -[ #L1s #L1d #d #k #_ #_ #X #H2 #L2s #_ #_ #L2d #_ #_ #H3 - lapply (leq_fwd_length … H3) -H3 #HL2sd - elim (cpx_inv_sort1 … H2) -H2 [| * #l #_ ] - #H destruct /2 width=1 by lleq_sort/ -| #Is #Id #L1s #L1d #K1s #K1d #V1s #V1d #d #i #Hid #HLK1s #HLK1d #_ #_ #_ #IHV1d #H1 #X #H2 #L2s #H1s #H2s #L2d #H1d #H2d #H3 - elim (ldrop_leq_conf_lt … H1 … HLK1s) -H1 /2 width=1 by ylt_inj/ - yminus_inj #Y #H1 #HY - lapply (ldrop_mono … HY … HLK1d) -HY #H destruct - elim (lpx_ldrop_conf … HLK1s … H1s) -H1s #Y #H #HLK2s - elim (lpx_inv_pair1 … H) -H #K2s #V2s #H1s #HV12s #H destruct - elim (lpx_ldrop_conf … HLK1d … H1d) -H1d #Y #H #HLK2d - elim (lpx_inv_pair1 … H) -H #K2d #V2d #H1d #HV12d #H destruct - elim (ldrop_leq_conf_be … H2s … HLK1s) -H2s /2 width=1 by ylt_inj/ - >yplus_O1 yminus_inj #Z #Y #X #HK12s #H - lapply (ldrop_mono … H … HLK2s) -H #H destruct - elim (ldrop_leq_conf_be … H2d … HLK1d) -H2d /2 width=1 by ylt_inj/ - >yplus_O1 yminus_inj #Z #Y #X #HK12d #H - lapply (ldrop_mono … H … HLK2d) -H #H destruct - elim (ldrop_leq_conf_lt … H3 … HLK2s) -H3 /2 width=1 by ylt_inj/ - yminus_inj #Y #H3 #HY - lapply (ldrop_mono … HY … HLK2d) -HY #H destruct - elim (cpx_inv_lref1 … H2) -H2 -L1s - [ -L1d #H destruct /3 width=15 by lleq_skip/ - | * #Z #Y #X1 #X2 #H #HX12 #HX2 lapply (ldrop_mono … H … HLK1d) -L1d - #H destruct >(plus_minus_m_m d (i+1)) // - lapply (ldrop_fwd_ldrop2 … HLK2s) -HLK2s - lapply (ldrop_fwd_ldrop2 … HLK2d) -HLK2d - /3 width=9 by lleq_lift_ge/ - ] -| #I #L1s #L1d #K1s #K1d #V1 #d #i #Hdi #HLK1s #HLK1d #_ #IHV1 #H1 #X #H2 #L2s #H1s #H2s #L2d #H1d #H2d #H3 - elim (ldrop_leq_conf_be … H1 … HLK1s) -H1 /2 width=1 by ylt_Y, yle_inj/ #Z #Y #X #H1 #HY - lapply (ldrop_mono … HY … HLK1d) -HY #H destruct - elim (lpx_ldrop_conf … HLK1s … H1s) -H1s #Y #H #HLK2s - elim (lpx_inv_pair1 … H) -H #K2s #V2s #H1s #HV12s #H destruct - elim (lpx_ldrop_conf … HLK1d … H1d) -H1d #Y #H #HLK2d - elim (lpx_inv_pair1 … H) -H #K2d #V2d #H1d #HV12d #H destruct - lapply (ldrop_leq_conf_ge … H2s … HLK1s ?) /2 width=1 by yle_inj/ #H - lapply (ldrop_mono … H … HLK2s) -H #H destruct - lapply (ldrop_leq_conf_ge … H2d … HLK1d ?) /2 width=1 by yle_inj/ #H - lapply (ldrop_mono … H … HLK2d) -H #H destruct - elim (ldrop_leq_conf_be … H3 … HLK2s) -H3 /2 width=1 by ylt_Y, yle_inj/ - >yminus_Y_inj #Z #Y #X #H3 #HY - lapply (ldrop_mono … HY … HLK2d) -HY #H destruct - elim (cpx_inv_lref1 … H2) -H2 -L1s - [ -L1d #H destruct /3 width=12 by lleq_lref/ - | * #Z #Y #X1 #X2 #H #HX12 #HX2 lapply (ldrop_mono … H … HLK1d) -L1d - #H destruct - lapply (ldrop_fwd_ldrop2 … HLK2s) -HLK2s #HLK2s - lapply (ldrop_fwd_ldrop2 … HLK2d) -HLK2d #HLK2d - @(lleq_ge … 0) /3 width=10 by lleq_lift_le/ (**) (* full auto too slow *) - ] -| #L1s #L1d #d #i #HL1s #HL1d #_ #_ #X #H2 #L2s #_ #_ #L2s #_ #H2d #H3 - lapply (leq_fwd_length … H2d) -H2d - lapply (leq_fwd_length … H3) -H3 - elim (cpx_inv_lref1 … H2) -H2 - [ #H destruct /2 width=1 by lleq_free/ - | -L1s * #I #K1d #V1 #V2 #HLK1d - lapply (ldrop_fwd_length_lt2 … HLK1d) -HLK1d #H - elim (lt_refl_false … i) /2 width=3 by lt_to_le_to_lt/ (**) (* full auto too slow *) - ] -| #L1s #L1d #d #k #_ #_ #X #H2 #L2s #_ #_ #L2d #_ #_ #H3 - lapply (leq_fwd_length … H3) -H3 #HL2sd - lapply (cpx_inv_gref1 … H2) -H2 - #H destruct /2 width=1 by lleq_gref/ -| #a #I #L1s #L1d #V1 #T1 #d #HV1 #_ #IHV1 #IHT1 #H1 #X #H2 #L2s #H1s #H2s #L2d #H1d #H2d #H3 - elim (cpx_inv_bind1 … H2) -H2 * - [ #V2 #T2 #HV12 #HT12 #H destruct - /5 width=5 by lpx_pair, lleq_cpx_trans_leq, lleq_bind, leq_pair, leq_succ/ - | #T2 #HT12 #HT2X #H1 #H2 destruct >(minus_plus_m_m d 1) - /4 width=9 by lpx_pair, lleq_inv_lift_ge, ldrop_ldrop, leq_pair, leq_succ/ - ] -| #I #L1s #L1d #V1 #T1 #d #HV1 #_ #IHV1 #IHT1 #H1 #X #H2 #L2s #H1s #H2s #L2d #H1d #H2d #H3 - elim (cpx_inv_flat1 … H2) -H2 * - [ #V2 #T2 #HV12 #HT12 #H destruct /3 width=1 by lleq_flat/ - | #HT1X #H destruct /2 width=1 by/ - | #HV1X #H destruct /2 width=1 by/ - | #a #V2 #W1 #W2 #T0 #T2 #HV12 #HW12 #HT02 #H1 #H2 #H3 destruct - lapply (IHT1 … (ⓛ{a}W2.T2) … L2s … L2d ? ? ?) -IHT1 /2 width=1 by cpx_bind/ #H - elim (lleq_inv_bind … H) -H -HW12 -HT02 #HW2 #HT2 - /4 width=1 by lleq_beta, lleq_flat, lleq_bind/ - | #a #V0 #V2 #W1 #W2 #T0 #T2 #HV10 #HV02 #HW12 #HT02 #H1 #H2 #H3 destruct - lapply (IHT1 … (ⓓ{a}W2.T2) … L2s … L2d ? ? ?) -IHT1 /2 width=1 by cpx_bind/ #H - elim (lleq_inv_bind … H) -H -HW12 -HT02 - /5 width=9 by lleq_lift_ge, lleq_flat, lleq_bind, ldrop_ldrop/ - ] -] -qed-. - -lemma lleq_cpx_conf_dx: ∀h,g,G,L2,T1,T2. ⦃G, L2⦄ ⊢ T1 ➡[h, g] T2 → - ∀L1. L1 ⋕[0, T1] L2 → L1 ⋕[0, T2] L2. -#h #g #G #L2 #T1 #T2 #HT12 #L1 #HT1 lapply (lleq_fwd_length … HT1) -/3 width=13 by lleq_cpx_conf_leq_dx, leq_O_Y/ -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/grammar/cl_shift.ma b/matita/matita/contribs/lambdadelta/basic_2/grammar/cl_shift.ma deleted file mode 100644 index 5fdab7148..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/grammar/cl_shift.ma +++ /dev/null @@ -1,45 +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_append.ma". - -(* SHIFT OF A CLOSURE *******************************************************) - -let rec shift L T on L ≝ match L with -[ LAtom ⇒ T -| LPair L I V ⇒ shift L (-ⓑ{I} V. T) -]. - -interpretation "shift (closure)" 'Append L T = (shift L T). - -(* Basic properties *********************************************************) - -lemma shift_append_assoc: ∀L,K. ∀T:term. (L @@ K) @@ T = L @@ K @@ T. -#L #K elim K -K // normalize // -qed. - -(* Basic inversion lemmas ***************************************************) - -lemma shift_inj: ∀L1,L2. ∀T1,T2:term. L1 @@ T1 = L2 @@ T2 → |L1| = |L2| → - L1 = L2 ∧ T1 = T2. -#L1 elim L1 -L1 -[ * normalize /2 width=1/ - #L2 #I2 #V2 #T1 #T2 #_ shift_append_assoc normalize #H - elim (cpr_inv_bind1 … H) -H * - [ #V0 #T0 #_ #HT10 #H destruct - elim (IH … HT10) -IH -HT10 #L2 #T2 #HL12 #H destruct - >append_length >HL12 -HL12 - @(ex2_2_intro … (⋆.ⓑ{I}V0@@L2) T2) [ >append_length ] /2 width=3 by trans_eq/ (**) (* explicit constructor *) - | #T #_ #_ #H destruct - ] -] -qed-. - (* Basic_1: removed theorems 11: pr0_subst0_back pr0_subst0_fwd pr0_subst0 pr2_head_2 pr2_cflat clear_pr2_trans diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx.ma index 7b99bd8de..9fd1ccf48 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx.ma @@ -94,15 +94,6 @@ lemma cpx_delift: ∀h,g,I,G,K,V,T1,L,d. ⇩[d] L ≡ (K.ⓑ{I}V) → ] qed-. -lemma cpx_append: ∀h,g,G. l_appendable_sn … (cpx h g G). -#h #g #G #K #T1 #T2 #H elim H -G -K -T1 -T2 -/2 width=3 by cpx_sort, cpx_bind, cpx_flat, cpx_zeta, cpx_tau, cpx_ti, cpx_beta, cpx_theta/ -#I #G #K #K0 #V1 #V2 #W2 #i #HK0 #_ #HVW2 #IHV12 #L -lapply (ldrop_fwd_length_lt2 … HK0) #H -@(cpx_delta … I … (L@@K0) V1 … HVW2) // -@(ldrop_O1_append_sn_le … HK0) /2 width=2 by lt_to_le/ (**) (* /3/ does not work *) -qed. - (* Basic inversion lemmas ***************************************************) fact cpx_inv_atom1_aux: ∀h,g,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡[h, g] T2 → ∀J. T1 = ⓪{J} → @@ -311,20 +302,3 @@ elim (cpx_inv_bind1 … H) -H * | #T2 #_ #_ #H destruct ] qed-. - -lemma cpx_fwd_shift1: ∀h,g,G,L1,L,T1,T. ⦃G, L⦄ ⊢ L1 @@ T1 ➡[h, g] T → - ∃∃L2,T2. |L1| = |L2| & T = L2 @@ T2. -#h #g #G #L1 @(lenv_ind_dx … L1) -L1 normalize -[ #L #T1 #T #HT1 - @(ex2_2_intro … (⋆)) // (**) (* explicit constructor *) -| #I #L1 #V1 #IH #L #T1 #X - >shift_append_assoc normalize #H - elim (cpx_inv_bind1 … H) -H * - [ #V0 #T0 #_ #HT10 #H destruct - elim (IH … HT10) -IH -HT10 #L2 #T2 #HL12 #H destruct - >append_length >HL12 -HL12 - @(ex2_2_intro … (⋆.ⓑ{I}V0@@L2) T2) [ >append_length ] /2 width=3 by refl, trans_eq/ (**) (* explicit constructor *) - | #T #_ #_ #H destruct - ] -] -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/crr_append.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/crr_append.ma deleted file mode 100644 index dbf794d99..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/reduction/crr_append.ma +++ /dev/null @@ -1,56 +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_append.ma". -include "basic_2/reduction/crr.ma". - -(* REDUCIBLE TERMS FOR CONTEXT-SENSITIVE REDUCTION **************************) - -(* Advanved properties ******************************************************) - -lemma crr_append_sn: ∀G,L,K,T. ⦃G, L⦄ ⊢ ➡ 𝐑⦃T⦄ → ⦃G, K @@ L⦄ ⊢ ➡ 𝐑⦃T⦄. -#G #L #K0 #T #H elim H -L -T /2 width=1/ -#L #K #V #i #HLK -lapply (ldrop_fwd_length_lt2 … HLK) #Hi -lapply (ldrop_O1_append_sn_le … HLK … K0) -HLK /2 width=2/ -Hi /2 width=3/ -qed. - -lemma trr_crr: ∀G,L,T. ⦃G, ⋆⦄ ⊢ ➡ 𝐑⦃T⦄ → ⦃G, L⦄ ⊢ ➡ 𝐑⦃T⦄. -#G #L #T #H lapply (crr_append_sn … H) // -qed. - -(* Advanced inversion lemmas ************************************************) - -fact crr_inv_labst_last_aux: ∀G,L1,T,W. ⦃G, L1⦄ ⊢ ➡ 𝐑⦃T⦄ → - ∀L2. L1 = ⋆.ⓛW @@ L2 → ⦃G, L2⦄ ⊢ ➡ 𝐑⦃T⦄. -#G #L1 #T #W #H elim H -L1 -T /2 width=1/ /3 width=1/ -[ #L1 #K1 #V1 #i #HLK1 #L2 #H destruct - lapply (ldrop_fwd_length_lt2 … HLK1) - >append_length >commutative_plus normalize in ⊢ (??% → ?); #H - elim (le_to_or_lt_eq i (|L2|)) /2 width=1/ -H #Hi destruct - [ elim (ldrop_O1_lt … Hi) #I2 #K2 #V2 #HLK2 - lapply (ldrop_O1_inv_append1_le … HLK1 … HLK2) -HLK1 /2 width=2/ -Hi - normalize #H destruct /2 width=3/ - | lapply (ldrop_O1_inv_append1_ge … HLK1 ?) -HLK1 // yplus_O1 - elim (ldrop_inv_O1_pair1 … H) -H * #Hi #HLK1 [ -IHL12 | -HL12 ] - [ #_ destruct -I2 >ypred_succ - /2 width=4 by ldrop_pair, ex2_2_intro/ - | lapply (ylt_inv_O1 i ?) /2 width=1 by ylt_inj/ - #H yminus_succ yplus_succ1 #H lapply (ylt_inv_succ … H) -H - #Hide lapply (ldrop_inv_drop1_lt … HLK2 ?) -HLK2 /2 width=1 by ylt_O/ - #HLK1 elim (IHL12 … HLK1) -IHL12 -HLK1 yminus_SO2 - /4 width=4 by ylt_O, ldrop_drop_lt, ex2_2_intro/ -] -qed-. - (* Basic forvard lemmas *****************************************************) (* Basic_1: was: drop_S *) diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop_append.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop_append.ma deleted file mode 100644 index 1fa09a012..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop_append.ma +++ /dev/null @@ -1,60 +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_append.ma". -include "basic_2/relocation/ldrop.ma". - -(* DROPPING *****************************************************************) - -(* Properties on append for local environments ******************************) - -fact ldrop_O1_append_sn_le_aux: ∀L1,L2,s,d,e. ⇩[s, d, e] L1 ≡ L2 → - d = 0 → e ≤ |L1| → - ∀L. ⇩[s, 0, e] L @@ L1 ≡ L @@ L2. -#L1 #L2 #s #d #e #H elim H -L1 -L2 -d -e normalize -[2,3,4: /4 width=1 by ldrop_skip_lt, ldrop_drop, arith_b1, lt_minus_to_plus_r, monotonic_pred/ ] -#d #e #_ #_ #H <(le_n_O_to_eq … H) -H // -qed-. - -lemma ldrop_O1_append_sn_le: ∀L1,L2,s,e. ⇩[s, 0, e] L1 ≡ L2 → e ≤ |L1| → - ∀L. ⇩[s, 0, e] L @@ L1 ≡ L @@ L2. -/2 width=3 by ldrop_O1_append_sn_le_aux/ qed. - -(* Inversion lemmas on append for local environments ************************) - -lemma ldrop_O1_inv_append1_ge: ∀K,L1,L2,s,e. ⇩[s, 0, e] L1 @@ L2 ≡ K → - |L2| ≤ e → ⇩[s, 0, e - |L2|] L1 ≡ K. -#K #L1 #L2 elim L2 -L2 normalize // -#L2 #I #V #IHL2 #s #e #H #H1e -elim (ldrop_inv_O1_pair1 … H) -H * #H2e #HL12 destruct -[ lapply (le_n_O_to_eq … H1e) -H1e -IHL2 - >commutative_plus normalize #H destruct -| minus_minus_comm /3 width=1 by monotonic_pred/ -] -qed-. - -lemma ldrop_O1_inv_append1_le: ∀K,L1,L2,s,e. ⇩[s, 0, e] L1 @@ L2 ≡ K → e ≤ |L2| → - ∀K2. ⇩[s, 0, e] L2 ≡ K2 → K = L1 @@ K2. -#K #L1 #L2 elim L2 -L2 normalize -[ #s #e #H1 #H2 #K2 #H3 lapply (le_n_O_to_eq … H2) -H2 - #H2 elim (ldrop_inv_atom1 … H3) -H3 #H3 #_ destruct - >(ldrop_inv_O2 … H1) -H1 // -| #L2 #I #V #IHL2 #s #e @(nat_ind_plus … e) -e [ -IHL2 ] - [ #H1 #_ #K2 #H2 - lapply (ldrop_inv_O2 … H1) -H1 #H1 - lapply (ldrop_inv_O2 … H2) -H2 #H2 destruct // - | /4 width=7 by ldrop_inv_drop1, le_plus_to_le_r/ - ] -] -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 new file mode 100644 index 000000000..e5a755531 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop_leq.ma @@ -0,0 +1,70 @@ +(**************************************************************************) +(* ___ *) +(* ||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 "ground_2/ynat/ynat_plus.ma". +include "basic_2/grammar/leq_leq.ma". +include "basic_2/relocation/ldrop.ma". + +(* BASIC SLICING FOR LOCAL ENVIRONMENTS *************************************) + +definition dedropable_sn: predicate (relation lenv) ≝ + λR. ∀L1,K1,s,d,e. ⇩[s, d, e] L1 ≡ K1 → ∀K2. R K1 K2 → + ∃∃L2. R L1 L2 & ⇩[s, d, e] L2 ≡ K2 & L1 ≃[d, e] L2. + +(* Properties on equivalence ************************************************) + +lemma leq_ldrop_trans_be: ∀L1,L2,d,e. L1 ≃[d, e] L2 → + ∀I,K2,W,s,i. ⇩[s, 0, i] L2 ≡ K2.ⓑ{I}W → + d ≤ i → i < d + e → + ∃∃K1. K1 ≃[0, ⫰(d+e-i)] K2 & ⇩[s, 0, i] L1 ≡ K1.ⓑ{I}W. +#L1 #L2 #d #e #H elim H -L1 -L2 -d -e +[ #d #e #J #K2 #W #s #i #H + elim (ldrop_inv_atom1 … H) -H #H destruct +| #I1 #I2 #L1 #L2 #V1 #V2 #_ #_ #J #K2 #W #s #i #_ #_ #H + elim (ylt_yle_false … H) // +| #I #L1 #L2 #V #e #HL12 #IHL12 #J #K2 #W #s #i #H #_ >yplus_O1 + elim (ldrop_inv_O1_pair1 … H) -H * #Hi #HLK1 [ -IHL12 | -HL12 ] + [ #_ destruct >ypred_succ + /2 width=3 by ldrop_pair, ex2_intro/ + | lapply (ylt_inv_O1 i ?) /2 width=1 by ylt_inj/ + #H yminus_succ yplus_succ1 #H lapply (ylt_inv_succ … H) -H + #Hide lapply (ldrop_inv_drop1_lt … HLK2 ?) -HLK2 /2 width=1 by ylt_O/ + #HLK1 elim (IHL12 … HLK1) -IHL12 -HLK1 yminus_SO2 + /4 width=3 by ylt_O, ldrop_drop_lt, ex2_intro/ +] +qed-. + +lemma leq_ldrop_conf_be: ∀L1,L2,d,e. L1 ≃[d, e] L2 → + ∀I,K1,W,s,i. ⇩[s, 0, i] L1 ≡ K1.ⓑ{I}W → + d ≤ i → i < d + e → + ∃∃K2. K1 ≃[0, ⫰(d+e-i)] K2 & ⇩[s, 0, i] L2 ≡ K2.ⓑ{I}W. +#L1 #L2 #d #e #HL12 #I #K1 #W #s #i #HLK1 #Hdi #Hide +elim (leq_ldrop_trans_be … (leq_sym … HL12) … HLK1) // -L1 -Hdi -Hide +/3 width=3 by leq_sym, 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 + /3 width=4 by inj, ex3_intro/ +| #K #K2 #_ #HK2 * #L #H1L1 #HLK #H2L1 elim (HR … HLK … HK2) -HR -K + /3 width=6 by leq_trans, step, ex3_intro/ +] +qed-. 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 index 127f92cc0..3dc3b2f79 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop_lpx_sn.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop_lpx_sn.ma @@ -13,7 +13,7 @@ (**************************************************************************) include "basic_2/grammar/lpx_sn.ma". -include "basic_2/relocation/ldrop.ma". +include "basic_2/relocation/ldrop_leq.ma". (* DROPPING *****************************************************************) @@ -44,16 +44,17 @@ lemma lpx_sn_liftable_dedropable: ∀R. (∀L. reflexive ? (R L)) → | #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 lsuby_O1, lpx_sn_pair, monotonic_le_plus_l/ + #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, lsuby_pair, lpx_sn_pair, ex3_intro/ + /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, lsuby_succ, lpx_sn_pair, ex3_intro/ + /3 width=6 by ldrop_skip, leq_succ, lpx_sn_pair, ex3_intro/ ] qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop_lsuby.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop_lsuby.ma deleted file mode 100644 index fdcca5a3d..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop_lsuby.ma +++ /dev/null @@ -1,29 +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/lsuby_lsuby.ma". -include "basic_2/relocation/ldrop.ma". - -(* BASIC SLICING FOR LOCAL ENVIRONMENTS *************************************) - -(* Properties on local environment refinement for extended substitution *****) - -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 - /3 width=4 by inj, ex3_intro/ -| #K #K2 #_ #HK2 * #L #H1L1 #HLK #H2L1 elim (HR … HLK … HK2) -HR -K - /3 width=6 by lsuby_trans, step, ex3_intro/ -] -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/lsuby.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/lsuby.ma index 34212a6c7..6c90b202b 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/lsuby.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/lsuby.ma @@ -14,7 +14,7 @@ include "ground_2/ynat/ynat_plus.ma". include "basic_2/notation/relations/extlrsubeq_4.ma". -include "basic_2/grammar/lenv_length.ma". +include "basic_2/relocation/ldrop.ma". (* LOCAL ENVIRONMENT REFINEMENT FOR EXTENDED SUBSTITUTION *******************) @@ -57,7 +57,7 @@ lemma lsuby_refl: ∀L,d,e. L ⊑×[d, e] L. #He destruct /2 width=1 by lsuby_zero, lsuby_pair/ qed. -lemma lsuby_O1: ∀L2,L1,d. |L2| ≤ |L1| → L1 ⊑×[d, yinj 0] L2. +lemma lsuby_O2: ∀L2,L1,d. |L2| ≤ |L1| → L1 ⊑×[d, yinj 0] L2. #L2 elim L2 -L2 // #L2 #I2 #V2 #IHL2 * normalize [ #d #H lapply (le_n_O_to_eq … H) -H (length_inv_zero_dx … H) -L1 // -| /2 width=1 by lsuby_O1/ +| /2 width=1 by lsuby_O2/ | #I1 #I2 #L1 #L2 #V #e #_ #IHL12 #H lapply (injective_plus_l … H) /3 width=1 by lsuby_pair/ | #I1 #I2 #L1 #L2 #V1 #V2 #d #e #_ #IHL12 #H lapply (injective_plus_l … H) @@ -206,3 +206,32 @@ lemma lsuby_inv_succ2: ∀I2,K2,L1,V2,d,e. L1 ⊑×[d, e] K2.ⓑ{I2}V2 → 0 < d lemma lsuby_fwd_length: ∀L1,L2,d,e. L1 ⊑×[d, e] L2 → |L2| ≤ |L1|. #L1 #L2 #d #e #H elim H -L1 -L2 -d -e normalize /2 width=1 by le_S_S/ qed-. + +(* Properties on basic slicing **********************************************) + +lemma lsuby_ldrop_trans_be: ∀L1,L2,d,e. L1 ⊑×[d, e] L2 → + ∀I2,K2,W,s,i. ⇩[s, 0, i] L2 ≡ K2.ⓑ{I2}W → + d ≤ i → i < d + e → + ∃∃I1,K1. K1 ⊑×[0, ⫰(d+e-i)] K2 & ⇩[s, 0, i] L1 ≡ K1.ⓑ{I1}W. +#L1 #L2 #d #e #H elim H -L1 -L2 -d -e +[ #L1 #d #e #J2 #K2 #W #s #i #H + elim (ldrop_inv_atom1 … H) -H #H destruct +| #I1 #I2 #L1 #L2 #V1 #V2 #_ #_ #J2 #K2 #W #s #i #_ #_ #H + elim (ylt_yle_false … H) // +| #I1 #I2 #L1 #L2 #V #e #HL12 #IHL12 #J2 #K2 #W #s #i #H #_ >yplus_O1 + elim (ldrop_inv_O1_pair1 … H) -H * #Hi #HLK1 [ -IHL12 | -HL12 ] + [ #_ destruct -I2 >ypred_succ + /2 width=4 by ldrop_pair, ex2_2_intro/ + | lapply (ylt_inv_O1 i ?) /2 width=1 by ylt_inj/ + #H yminus_succ yplus_succ1 #H lapply (ylt_inv_succ … H) -H + #Hide lapply (ldrop_inv_drop1_lt … HLK2 ?) -HLK2 /2 width=1 by ylt_O/ + #HLK1 elim (IHL12 … HLK1) -IHL12 -HLK1 yminus_SO2 + /4 width=4 by ylt_O, ldrop_drop_lt, ex2_2_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 bb8ab1587..78b3b6b3b 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 @@ -84,7 +84,8 @@ table { } ] [ { "strongly normalizing extended computation" * } { - [ "lsx ( ? ⊢ ⬊*[?,?,?,?] ? )" "lsx_ldrop" + "lsx_cpxs" + "lsx_csx" * ] + [ "lcosx ( ? ⊢ ⧤⬊*[?,?,?] ? )" "lcosx_cpxs" * ] + [ "lsx ( ? ⊢ ⋕⬊*[?,?,?,?] ? )" "lsx_ldrop" + "lsx_cpxs" + "lsx_csx" * ] [ "csx_vector ( ⦃?,?⦄ ⊢ ⬊*[?,?] ? )" "csx_tstc_vector" + "csx_aaa" * ] [ "csx ( ⦃?,?⦄ ⊢ ⬊*[?,?] ? )" "csx_alt ( ⦃?,?⦄ ⊢ ⬊⬊*[?,?] ? )" "csx_lift" + "csx_lpx" + "csx_fpbs" * ] } @@ -140,11 +141,11 @@ table { } ] [ { "irreducible forms for context-sensitive extended reduction" * } { - [ "cix ( ⦃?,?⦄ ⊢ ➡[?,?] 𝐈⦃?⦄ )" "cix_append" + "cix_lift" * ] + [ "cix ( ⦃?,?⦄ ⊢ ➡[?,?] 𝐈⦃?⦄ )" "cix_lift" * ] } ] [ { "reducible forms for context-sensitive extended reduction" * } { - [ "crx ( ⦃?,?⦄ ⊢ ➡[?,?] 𝐑⦃?⦄ )" "crx_append" + "crx_lift" * ] + [ "crx ( ⦃?,?⦄ ⊢ ➡[?,?] 𝐑⦃?⦄ )" "crx_lift" * ] } ] [ { "normal forms for context-sensitive reduction" * } { @@ -157,11 +158,11 @@ table { } ] [ { "irreducible forms for context-sensitive reduction" * } { - [ "cir ( ⦃?,?⦄ ⊢ ➡ 𝐈⦃?⦄ )" "cir_append" + "cir_lift" * ] + [ "cir ( ⦃?,?⦄ ⊢ ➡ 𝐈⦃?⦄ )" "cir_lift" * ] } ] [ { "reducible forms for context-sensitive reduction" * } { - [ "crr ( ⦃?,?⦄ ⊢ ➡ 𝐑⦃?⦄ )" "crr_append" + "crr_lift" * ] + [ "crr ( ⦃?,?⦄ ⊢ ➡ 𝐑⦃?⦄ )" "crr_lift" * ] } ] } @@ -246,6 +247,10 @@ table { [ "lsubr ( ? ⊑ ? )" "lsubr_lsubr" * ] } ] + [ { "local env. ref. for extended substitution" * } { + [ "lsuby ( ? ⊑×[?,?] ? )" "lsuby_lsuby" * ] + } + ] [ { "structural successor for closures" * } { [ "fquq ( ⦃?,?,?⦄ ⊃⸮ ⦃?,?,?⦄ )" "fquq_alt ( ⦃?,?,?⦄ ⊃⊃⸮ ⦃?,?,?⦄ )" * ] [ "fqu ( ⦃?,?,?⦄ ⊃ ⦃?,?,?⦄ )" * ] @@ -256,11 +261,7 @@ table { } ] [ { "basic local env. slicing" * } { - [ "ldrop ( ⇩[?,?,?] ? ≡ ? )" "ldrop_append" + "ldrop_lpx_sn" + "ldrop_lsuby" + "ldrop_ldrop" * ] - } - ] - [ { "local env. ref. for extended substitution" * } { - [ "lsuby ( ? ⊑×[?,?] ? )" "lsuby_lsuby" * ] + [ "ldrop ( ⇩[?,?,?] ? ≡ ? )" "ldrop_lpx_sn" + "ldrop_leq" + "ldrop_ldrop" * ] } ] [ { "basic term relocation" * } { @@ -272,6 +273,10 @@ table { ] class "red" [ { "grammar" * } { + [ { "equivalence for local environments" * } { + [ "leq ( ? ≃[?,?] ? )" "leq_leq" * ] + } + ] [ { "pointwise extension of a relation" * } { [ "lpx_sn" "lpx_sn_tc" + "lpx_sn_lpx_sn" * ] } @@ -281,7 +286,7 @@ table { } ] [ { "closures" * } { - [ "cl_shift ( ? @@ ? )" "cl_weight ( ♯{?,?,?} )" * ] + [ "cl_weight ( ♯{?,?,?} )" "cl_restricted_weight ( ♯{?,?} )" * ] } ] [ { "internal syntax" * } { diff --git a/matita/matita/contribs/lambdadelta/ground_2/lib/arith.ma b/matita/matita/contribs/lambdadelta/ground_2/lib/arith.ma index 832195fe9..555a340d8 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/lib/arith.ma +++ b/matita/matita/contribs/lambdadelta/ground_2/lib/arith.ma @@ -58,6 +58,12 @@ fact le_repl_sn_aux: ∀x,y,z:nat. x ≤ z → x = y → y ≤ z. lemma monotonic_le_minus_l2: ∀x1,x2,y,z. x1 ≤ x2 → x1 - y - z ≤ x2 - y - z. /3 width=1 by monotonic_le_minus_l/ qed. +(* Note: this might interfere with nat.ma *) +lemma monotonic_lt_pred: ∀m,n. m < n → O < m → pred m < pred n. +#m #n #Hmn #Hm whd >(S_pred … Hm) +@le_S_S_to_le >S_pred /2 width=3 by transitive_lt/ +qed. + lemma arith_j: ∀x,y,z. x-y-1 ≤ x-(y-z)-1. /3 width=1 by monotonic_le_minus_l, monotonic_le_minus_r/ qed. diff --git a/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_lt.ma b/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_lt.ma index a306b5756..26135550e 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_lt.ma +++ b/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_lt.ma @@ -122,6 +122,13 @@ lemma ylt_O: ∀x. ⫯⫰(yinj x) = yinj x → 0 < x. #H destruct qed. +(* Properties on predecessor ************************************************) + +lemma ylt_pred: ∀m,n. m < n → 0 < m → ⫰m < ⫰n. +#m #n * -m -n +/4 width=1 by ylt_inv_inj, ylt_inj, monotonic_lt_pred/ +qed. + (* Properties on successor **************************************************) lemma ylt_O_succ: ∀n. 0 < ⫯n. diff --git a/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_minus.ma b/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_minus.ma index 596885cf0..81b9cb015 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_minus.ma +++ b/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_minus.ma @@ -51,6 +51,14 @@ lemma yminus_SO2: ∀m. m - 1 = ⫰m. * // qed. +lemma yminus_pred: ∀n,m. 0 < m → 0 < n → ⫰m - ⫰n = m - n. +* // #n * +[ #m #Hm #Hn >yminus_inj >yminus_inj + /4 width=1 by ylt_inv_inj, minus_pred_pred, eq_f/ +| >yminus_Y_inj // +] +qed-. + (* Properties on successor **************************************************) lemma yminus_succ: ∀n,m. ⫯m - ⫯n = m - n. diff --git a/matita/matita/predefined_virtuals.ml b/matita/matita/predefined_virtuals.ml index 42a14c179..3ad4d33ae 100644 --- a/matita/matita/predefined_virtuals.ml +++ b/matita/matita/predefined_virtuals.ml @@ -1508,9 +1508,9 @@ let predefined_classes = [ ["?"; "¿"; "⸮"; ]; [":"; "⁝"; ]; ["."; "•"; "◦"; ]; - ["#"; "♯"; "⋕"; "⌘"; ]; + ["#"; "♯"; "⋕"; "⧤"; "⌘"; ]; ["-"; "÷"; "⊢"; "⊩"; ]; - ["="; "≃"; "≈"; "≝"; "≡"; "≅"; "≐"; "≑"; "≚"; "≙"; "⌆"; ]; + ["="; "≝"; "⊜"; "≡"; "≃"; "≈"; "≅"; "≐"; "≑"; "≚"; "≙"; "⌆"; ]; ["→"; "↦"; "⇝"; "⤞"; "⇾"; "⤍"; "⤏"; "⤳"; ] ; ["⇒"; "⤇"; "➾"; "⇨"; "➡"; "➤"; "➸"; "⇉"; "⥰"; ] ; ["^"; "↑"; ] ;