From: Ferruccio Guidi Date: Wed, 25 Mar 2015 21:44:57 +0000 (+0000) Subject: - revision of ground_2 and basic_2 X-Git-Tag: make_still_working~724 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=658c000ee2ea2da04cf29efc0acdaf16364fbf5e;p=helm.git - revision of ground_2 and basic_2 lift and drop now accept infinity as first parameter - Makefile: updated for matitac that now takes directories --- diff --git a/matita/matita/contribs/lambdadelta/Makefile b/matita/matita/contribs/lambdadelta/Makefile index cdd4f35b6..064c24db9 100644 --- a/matita/matita/contribs/lambdadelta/Makefile +++ b/matita/matita/contribs/lambdadelta/Makefile @@ -40,6 +40,10 @@ XPACKAGES := ground_2 basic_2 LDWS := $(shell find -name "*.ldw.xml") TBLS := $(shell find -name "*.tbl") +all: + @echo " MATITAC $(PACKAGES)" + $(H)../../matitac.opt $(PACKAGES) + # MAS ######################################################################## define MAS_TEMPLATE @@ -57,10 +61,6 @@ endef $(foreach PKG, $(PACKAGES), $(eval $(call MAS_TEMPLATE,$(PKG)))) -all: - @echo " MATITAC $(PACKAGES)" - $(H)../../matitac.opt $(MAS) - # XMAS ####################################################################### define XMAS_TEMPLATE diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_cpxs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_cpxs.ma index c02d0cd06..e6f9c381f 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_cpxs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_cpxs.ma @@ -133,7 +133,8 @@ lemma fqu_cpxs_trans_neq: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐ ⦃G2, [ #I #G #L #V1 #V2 #HV12 #_ elim (lift_total V2 0 1) #U2 #HVU2 @(ex3_intro … U2) [1,3: /3 width=7 by fqu_drop, cpxs_delta, drop_pair, drop_drop/ - | #H destruct /2 width=7 by lift_inv_lref2_be/ + | #H destruct + lapply (lift_inv_lref2_be … HVU2 ? ?) -HVU2 // ] | #I #G #L #V1 #T #V2 #HV12 #H @(ex3_intro … (②{I}V2.T)) [1,3: /2 width=4 by fqu_pair_sn, cpxs_pair_sn/ diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/lcosx.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/lcosx.ma index 8997c6ec9..b19af4067 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/lcosx.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/lcosx.ma @@ -58,7 +58,7 @@ fact lcosx_inv_succ_aux: ∀h,g,G,L,x. G ⊢ ~⬊*[h, g, x] L → ∀l. x = ⫯l G ⊢ ⬊*[h, g, V, l] K. #h #g #G #L #l * -L -l /2 width=1 by or_introl/ [ #I #L #T #_ #x #H elim (ysucc_inv_O_sn … H) -| #I #L #T #l #HT #HL #x #H <(ysucc_inj … H) -x +| #I #L #T #l #HT #HL #x #H <(ysucc_inv_inj … H) -x /3 width=6 by ex3_3_intro, or_intror/ ] qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/lcosx_cpx.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/lcosx_cpx.ma index 12b9a05d2..eaa8649d4 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/lcosx_cpx.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/lcosx_cpx.ma @@ -28,7 +28,7 @@ lemma lsx_cpx_trans_lcosx: ∀h,g,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡[h, g] T2 → #h #g #G #L #T1 #T2 #H elim H -G -L -T1 -T2 // [ #I #G #L #K #V1 #V2 #W2 #i #HLK #_ #HVW2 #IHV12 #l #HL #H elim (ylt_split i l) #Hli [ -H | -HL ] - [ <(ymax_pre_sn l (⫯i)) /2 width=1 by ylt_fwd_le_succ/ + [ <(ymax_pre_sn l (⫯i)) /2 width=1 by ylt_fwd_le_succ1/ elim (lcosx_drop_trans_lt … HL … HLK) // -HL -Hli lapply (drop_fwd_drop2 … HLK) -HLK /3 width=7 by lsx_lift_ge/ | lapply (lsx_fwd_lref_be … H … HLK) // -H -Hli @@ -42,8 +42,9 @@ lemma lsx_cpx_trans_lcosx: ∀h,g,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡[h, g] T2 → | #I #G #L #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #l #HL #H elim (lsx_inv_flat … H) -H /3 width=1 by lsx_flat/ | #G #L #V #U1 #U2 #T2 #_ #HTU2 #IHU12 #l #HL #H - elim (lsx_inv_bind … H) -H - /4 width=9 by lcosx_pair, lsx_inv_lift_ge, drop_drop/ + elim (lsx_inv_bind … H) -H #HV #HU1 + <(ypred_succ l) (lift_inv_sort1 … H) -X -K -l -m // | #I #G #K #K0 #V #i #HK0 #_ #IHV #L #s #l #m #HLK #X #H elim (lift_inv_lref1 … H) * #Hil #H destruct - [ elim (drop_trans_le … HLK … HK0) -K /2 width=2 by lt_to_le/ #X #HL0 #H - elim (drop_inv_skip2 … H) -H /2 width=1 by lt_plus_to_minus_r/ -Hil #L0 #W #HLK0 #HVW #H destruct + [ elim (drop_trans_le … HLK … HK0) -K /2 width=2 by ylt_fwd_le/ #X #HL0 #H + elim (drop_inv_skip2 … H) -H /2 width=1 by ylt_to_minus/ -Hil #L0 #W #HLK0 #HVW #H destruct /3 width=9 by snv_lref/ | lapply (drop_trans_ge … HLK … HK0 ?) -K /3 width=9 by snv_lref, drop_inv_gen/ @@ -55,8 +55,8 @@ lemma snv_inv_lift: ∀h,g,G,L,U. ⦃G, L⦄ ⊢ U ¡[h, g] → ∀K,s,l,m. ⬇[ >(lift_inv_sort2 … H) -X -L -l -m // | #I #G #L #L0 #W #i #HL0 #_ #IHW #K #s #l #m #HLK #X #H elim (lift_inv_lref2 … H) * #Hil #H destruct - [ elim (drop_conf_le … HLK … HL0) -L /2 width=2 by lt_to_le/ #X #HK0 #H - elim (drop_inv_skip1 … H) -H /2 width=1 by lt_plus_to_minus_r/ -Hil #K0 #V #HLK0 #HVW #H destruct + [ elim (drop_conf_le … HLK … HL0) -L /2 width=2 by ylt_fwd_le/ #X #HK0 #H + elim (drop_inv_skip1 … H) -H /2 width=1 by ylt_to_minus/ -Hil #K0 #V #HLK0 #HVW #H destruct /3 width=12 by snv_lref/ | lapply (drop_conf_ge … HLK … HL0 ?) -L /3 width=9 by snv_lref/ ] diff --git a/matita/matita/contribs/lambdadelta/basic_2/multiple/cpys.ma b/matita/matita/contribs/lambdadelta/basic_2/multiple/cpys.ma index 2ca575e2a..7da756f97 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/multiple/cpys.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/multiple/cpys.ma @@ -159,8 +159,8 @@ lemma cpys_inv_refl_O2: ∀G,L,T1,T2,l. ⦃G, L⦄ ⊢ T1 ▶*[l, 0] T2 → T1 = #T #T2 #_ #HT2 #IHT1 <(cpy_inv_refl_O2 … HT2) -HT2 // qed-. -lemma cpys_inv_lift1_eq: ∀G,L,U1,U2. ∀l,m:nat. - ⦃G, L⦄ ⊢ U1 ▶*[l, m] U2 → ∀T1. ⬆[l, m] T1 ≡ U1 → U1 = U2. +lemma cpys_inv_lift1_eq: ∀G,L,U1,U2,l,m. + ⦃G, L⦄ ⊢ U1 ▶*[l, yinj m] U2 → ∀T1. ⬆[l, m] T1 ≡ U1 → U1 = U2. #G #L #U1 #U2 #l #m #H #T1 #HTU1 @(cpys_ind … H) -U2 /2 width=7 by cpy_inv_lift1_eq/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/multiple/cpys_alt.ma b/matita/matita/contribs/lambdadelta/basic_2/multiple/cpys_alt.ma index d868ef407..d6b6c3096 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/multiple/cpys_alt.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/multiple/cpys_alt.ma @@ -61,7 +61,7 @@ lemma cpysa_cpy_trans: ∀G,L,T1,T,l,m. ⦃G, L⦄ ⊢ T1 ▶▶*[l, m] T → lapply (drop_fwd_drop2 … HLK) #H0LK lapply (cpy_weak … H 0 (l+m) ? ?) -H // #H elim (cpy_inv_lift1_be … H … H0LK … HVW2) -H -H0LK -HVW2 - /3 width=7 by cpysa_subst, ylt_fwd_le_succ/ + /3 width=7 by cpysa_subst, ylt_fwd_le_succ1/ | #a #I #G #L #V1 #V #T1 #T #l #m #_ #_ #IHV1 #IHT1 #X #H elim (cpy_inv_bind1 … H) -H #V2 #T2 #HV2 #HT2 #H destruct /5 width=5 by cpysa_bind, lsuby_cpy_trans, lsuby_succ/ diff --git a/matita/matita/contribs/lambdadelta/basic_2/multiple/cpys_cpys.ma b/matita/matita/contribs/lambdadelta/basic_2/multiple/cpys_cpys.ma index 60557d094..7df95948e 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/multiple/cpys_cpys.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/multiple/cpys_cpys.ma @@ -60,8 +60,8 @@ qed-. lemma cpys_inv_lift1_up: ∀G,L,U1,U2,lt,mt. ⦃G, L⦄ ⊢ U1 ▶*[lt, mt] U2 → ∀K,s,l,m. ⬇[s, l, m] L ≡ K → ∀T1. ⬆[l, m] T1 ≡ U1 → - l ≤ lt → lt ≤ yinj l + m → yinj l + m ≤ lt + mt → - ∃∃T2. ⦃G, K⦄ ⊢ T1 ▶*[l, lt + mt - (yinj l + m)] T2 & + l ≤ lt → lt ≤ l + m → l + m ≤ lt + mt → + ∃∃T2. ⦃G, K⦄ ⊢ T1 ▶*[l, lt + mt - (l + m)] T2 & ⬆[l, m] T2 ≡ U2. #G #L #U1 #U2 #lt #mt #HU12 #K #s #l #m #HLK #T1 #HTU1 #Hllt #Hltlm #Hlmlmt elim (cpys_split_up … HU12 (l + m)) -HU12 // -Hlmlmt #U #HU1 #HU2 @@ -105,8 +105,8 @@ theorem cpys_antisym_eq: ∀G,L1,T1,T2,l,m. ⦃G, L1⦄ ⊢ T1 ▶*[l, m] T2 → #HW2 >(cpys_inv_lift1_eq … HW2) -HW2 // | elim (drop_O1_le (Ⓕ) … Hi) -Hi #K2 #HLK2 elim (cpys_inv_lift1_ge_up … HW2 … HLK2 … HVW2 ? ? ?) -HW2 -HLK2 -HVW2 - /2 width=1 by ylt_fwd_le_succ, yle_succ_dx/ -Hli -Hilm - #X #_ #H elim (lift_inv_lref2_be … H) -H // + /2 width=1 by ylt_fwd_le_succ1, yle_succ_dx/ -Hli -Hilm + #X #_ #H elim (lift_inv_lref2_be … H) -H /2 width=1 by ylt_inj/ ] | #a #I #G #L1 #V1 #V2 #T1 #T2 #l #m #_ #_ #IHV12 #IHT12 #L2 #H elim (cpys_inv_bind1 … H) -H #V #T #HV2 #HT2 #H destruct diff --git a/matita/matita/contribs/lambdadelta/basic_2/multiple/cpys_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/multiple/cpys_lift.ma index 848284a25..59cddfbc9 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/multiple/cpys_lift.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/multiple/cpys_lift.ma @@ -32,7 +32,7 @@ lemma cpys_subst: ∀I,G,L,K,V,U1,i,l,m. lapply (cpy_lift_ge … HU1 … HLK HU0 HU12 ?) -HU1 -HLK -HU0 -HU12 // #HU02 lapply (cpy_weak … HU02 l m ? ?) -HU02 [2,3: /2 width=3 by cpys_strap1, yle_succ_dx/ ] - >yplus_O1 ymax_pre_sn_comm /2 width=1 by ylt_fwd_le_succ/ + >yplus_O1 ymax_pre_sn_comm /2 width=1 by ylt_fwd_le_succ1/ ] qed. @@ -61,7 +61,7 @@ lemma cpys_inv_atom1: ∀I,G,L,T2,l,m. ⦃G, L⦄ ⊢ ⓪{I} ▶*[l, m] T2 → | * #J #K #V1 #V #i #Hli #Hilm #HLK #HV1 #HVT #HI lapply (drop_fwd_drop2 … HLK) #H elim (cpy_inv_lift1_ge_up … HT2 … H … HVT) -HT2 -H -HVT - [2,3,4: /2 width=1 by ylt_fwd_le_succ, yle_succ_dx/ ] + [2,3,4: /2 width=1 by ylt_fwd_le_succ1, yle_succ_dx/ ] /4 width=11 by cpys_strap1, ex6_5_intro, or_intror/ ] ] @@ -92,7 +92,7 @@ lemma cpys_inv_lref1_drop: ∀G,L,T2,i,l,m. ⦃G, L⦄ ⊢ #i ▶*[l, m] T2 → & l ≤ i & i < l + m. #G #L #T2 #i #l #m #H #I #K #V1 #HLK #V2 #HVT2 elim (cpys_inv_lref1 … H) -H -[ #H destruct elim (lift_inv_lref2_be … HVT2) -HVT2 -HLK // +[ #H destruct elim (lift_inv_lref2_be … HVT2) -HVT2 -HLK /2 width=1 by ylt_inj/ | * #Z #Y #X1 #X2 #Hli #Hilm #HLY #HX12 #HXT2 lapply (lift_inj … HXT2 … HVT2) -T2 #H destruct lapply (drop_mono … HLY … HLK) -L #H destruct @@ -103,7 +103,7 @@ qed-. (* Properties on relocation *************************************************) lemma cpys_lift_le: ∀G,K,T1,T2,lt,mt. ⦃G, K⦄ ⊢ T1 ▶*[lt, mt] T2 → - ∀L,U1,s,l,m. lt + mt ≤ yinj l → ⬇[s, l, m] L ≡ K → + ∀L,U1,s,l,m. lt + mt ≤ l → ⬇[s, l, m] L ≡ K → ⬆[l, m] T1 ≡ U1 → ∀U2. ⬆[l, m] T2 ≡ U2 → ⦃G, L⦄ ⊢ U1 ▶*[lt, mt] U2. #G #K #T1 #T2 #lt #mt #H #L #U1 #s #l #m #Hlmtl #HLK #HTU1 @(cpys_ind … H) -T2 @@ -116,7 +116,7 @@ lemma cpys_lift_le: ∀G,K,T1,T2,lt,mt. ⦃G, K⦄ ⊢ T1 ▶*[lt, mt] T2 → qed-. lemma cpys_lift_be: ∀G,K,T1,T2,lt,mt. ⦃G, K⦄ ⊢ T1 ▶*[lt, mt] T2 → - ∀L,U1,s,l,m. lt ≤ yinj l → l ≤ lt + mt → + ∀L,U1,s,l,m. lt ≤ l → l ≤ lt + mt → ⬇[s, l, m] L ≡ K → ⬆[l, m] T1 ≡ U1 → ∀U2. ⬆[l, m] T2 ≡ U2 → ⦃G, L⦄ ⊢ U1 ▶*[lt, mt + m] U2. #G #K #T1 #T2 #lt #mt #H #L #U1 #s #l #m #Hltl #Hllmt #HLK #HTU1 @(cpys_ind … H) -T2 @@ -129,7 +129,7 @@ lemma cpys_lift_be: ∀G,K,T1,T2,lt,mt. ⦃G, K⦄ ⊢ T1 ▶*[lt, mt] T2 → qed-. lemma cpys_lift_ge: ∀G,K,T1,T2,lt,mt. ⦃G, K⦄ ⊢ T1 ▶*[lt, mt] T2 → - ∀L,U1,s,l,m. yinj l ≤ lt → ⬇[s, l, m] L ≡ K → + ∀L,U1,s,l,m. l ≤ lt → ⬇[s, l, m] L ≡ K → ⬆[l, m] T1 ≡ U1 → ∀U2. ⬆[l, m] T2 ≡ U2 → ⦃G, L⦄ ⊢ U1 ▶*[lt+m, mt] U2. #G #K #T1 #T2 #lt #mt #H #L #U1 #s #l #m #Hllt #HLK #HTU1 @(cpys_ind … H) -T2 @@ -156,7 +156,7 @@ qed-. lemma cpys_inv_lift1_be: ∀G,L,U1,U2,lt,mt. ⦃G, L⦄ ⊢ U1 ▶*[lt, mt] U2 → ∀K,s,l,m. ⬇[s, l, m] L ≡ K → ∀T1. ⬆[l, m] T1 ≡ U1 → - lt ≤ l → yinj l + m ≤ lt + mt → + lt ≤ l → l + m ≤ lt + mt → ∃∃T2. ⦃G, K⦄ ⊢ T1 ▶*[lt, mt - m] T2 & ⬆[l, m] T2 ≡ U2. #G #L #U1 #U2 #lt #mt #H #K #s #l #m #HLK #T1 #HTU1 #Hltl #Hlmlmt @(cpys_ind … H) -U2 [ /2 width=3 by ex2_intro/ @@ -167,7 +167,7 @@ qed-. lemma cpys_inv_lift1_ge: ∀G,L,U1,U2,lt,mt. ⦃G, L⦄ ⊢ U1 ▶*[lt, mt] U2 → ∀K,s,l,m. ⬇[s, l, m] L ≡ K → ∀T1. ⬆[l, m] T1 ≡ U1 → - yinj l + m ≤ lt → + l + m ≤ lt → ∃∃T2. ⦃G, K⦄ ⊢ T1 ▶*[lt - m, mt] T2 & ⬆[l, m] T2 ≡ U2. #G #L #U1 #U2 #lt #mt #H #K #s #l #m #HLK #T1 #HTU1 #Hlmlt @(cpys_ind … H) -U2 [ /2 width=3 by ex2_intro/ @@ -180,8 +180,8 @@ qed-. lemma cpys_inv_lift1_ge_up: ∀G,L,U1,U2,lt,mt. ⦃G, L⦄ ⊢ U1 ▶*[lt, mt] U2 → ∀K,s,l,m. ⬇[s, l, m] L ≡ K → ∀T1. ⬆[l, m] T1 ≡ U1 → - l ≤ lt → lt ≤ yinj l + m → yinj l + m ≤ lt + mt → - ∃∃T2. ⦃G, K⦄ ⊢ T1 ▶*[l, lt + mt - (yinj l + m)] T2 & + l ≤ lt → lt ≤ l + m → l + m ≤ lt + mt → + ∃∃T2. ⦃G, K⦄ ⊢ T1 ▶*[l, lt + mt - (l + m)] T2 & ⬆[l, m] T2 ≡ U2. #G #L #U1 #U2 #lt #mt #H #K #s #l #m #HLK #T1 #HTU1 #Hllt #Hltlm #Hlmlmt @(cpys_ind … H) -U2 [ /2 width=3 by ex2_intro/ @@ -192,7 +192,7 @@ qed-. lemma cpys_inv_lift1_be_up: ∀G,L,U1,U2,lt,mt. ⦃G, L⦄ ⊢ U1 ▶*[lt, mt] U2 → ∀K,s,l,m. ⬇[s, l, m] L ≡ K → ∀T1. ⬆[l, m] T1 ≡ U1 → - lt ≤ l → lt + mt ≤ yinj l + m → + lt ≤ l → lt + mt ≤ l + m → ∃∃T2. ⦃G, K⦄ ⊢ T1 ▶*[lt, l - lt] T2 & ⬆[l, m] T2 ≡ U2. #G #L #U1 #U2 #lt #mt #H #K #s #l #m #HLK #T1 #HTU1 #Hltl #Hlmtlm @(cpys_ind … H) -U2 [ /2 width=3 by ex2_intro/ @@ -203,7 +203,7 @@ qed-. lemma cpys_inv_lift1_le_up: ∀G,L,U1,U2,lt,mt. ⦃G, L⦄ ⊢ U1 ▶*[lt, mt] U2 → ∀K,s,l,m. ⬇[s, l, m] L ≡ K → ∀T1. ⬆[l, m] T1 ≡ U1 → - lt ≤ l → l ≤ lt + mt → lt + mt ≤ yinj l + m → + lt ≤ l → l ≤ lt + mt → lt + mt ≤ l + m → ∃∃T2. ⦃G, K⦄ ⊢ T1 ▶*[lt, l - lt] T2 & ⬆[l, m] T2 ≡ U2. #G #L #U1 #U2 #lt #mt #H #K #s #l #m #HLK #T1 #HTU1 #Hltl #Hllmt #Hlmtlm @(cpys_ind … H) -U2 [ /2 width=3 by ex2_intro/ @@ -213,7 +213,7 @@ lemma cpys_inv_lift1_le_up: ∀G,L,U1,U2,lt,mt. ⦃G, L⦄ ⊢ U1 ▶*[lt, mt] U qed-. lemma cpys_inv_lift1_subst: ∀G,L,W1,W2,l,m. ⦃G, L⦄ ⊢ W1 ▶*[l, m] W2 → - ∀K,V1,i. ⬇[i+1] L ≡ K → ⬆[O, i+1] V1 ≡ W1 → + ∀K,V1,i. ⬇[i+1] L ≡ K → ⬆[O, i+1] V1 ≡ W1 → l ≤ yinj i → i < l + m → ∃∃V2. ⦃G, K⦄ ⊢ V1 ▶*[O, ⫰(l+m-i)] V2 & ⬆[O, i+1] V2 ≡ W2. #G #L #W1 #W2 #l #m #HW12 #K #V1 #i #HLK #HVW1 #Hli #Hilm diff --git a/matita/matita/contribs/lambdadelta/basic_2/multiple/drops.ma b/matita/matita/contribs/lambdadelta/basic_2/multiple/drops.ma index 53253e55e..065135c9a 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/multiple/drops.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/multiple/drops.ma @@ -20,7 +20,7 @@ include "basic_2/multiple/lifts_vector.ma". (* ITERATED LOCAL ENVIRONMENT SLICING ***************************************) -inductive drops (s:bool): list2 nat nat → relation lenv ≝ +inductive drops (s:bool): list2 ynat nat → relation lenv ≝ | drops_nil : ∀L. drops s (◊) L L | drops_cons: ∀L1,L,L2,cs,l,m. drops s cs L1 L → ⬇[s, l, m] L ≡ L2 → drops s ({l, m} @ cs) L1 L2 @@ -83,13 +83,15 @@ lemma drops_inv_skip2: ∀I,s,cs,cs2,i. cs ▭ i ≡ cs2 → >(drops_inv_nil … H) -L1 /2 width=7 by lifts_nil, minuss_nil, ex4_3_intro, drops_nil/ | #cs #cs2 #l #m #i #Hil #_ #IHcs2 #L1 #K2 #V2 #H elim (drops_inv_cons … H) -H #L #HL1 #H - elim (drop_inv_skip2 … H) -H /2 width=1 by lt_plus_to_minus_r/ #K #V >minus_plus #HK2 #HV2 #H destruct + elim (drop_inv_skip2 … H) -H /2 width=1 by ylt_to_minus/ #K #V plus_minus /3 width=1 by minuss_lt, lt_minus_to_plus/ (**) (* explicit constructors *) + >pluss_SO2 >pluss_SO2 + >yminus_succ2 >ylt_inv_O1 /2 width=1 by ylt_to_minus/ commutative_plus (**) (* (nlift_inv_lref_be_SO … Hnx) -x /3 width=5 by ex4_3_intro, or_intror/ + lapply (nlift_inv_lref_be_SO … Hnx) -Hnx #H + lapply (yinj_inj … H) -H #H destruct + /3 width=5 by ex4_3_intro, or_intror/ ] qed-. -lemma frees_inv_lref_free: ∀L,l,j,i. L ⊢ i ϵ 𝐅*[l]⦃#j⦄ → |L| ≤ j → j = i. +lemma frees_inv_lref_free: ∀L,l,j,i. L ⊢ i ϵ 𝐅*[l]⦃#j⦄ → |L| ≤ j → yinj j = i. #L #l #j #i #H #Hj elim (frees_inv_lref … H) -H // * #I #K #W #_ #_ #HLK lapply (drop_fwd_length_lt2 … HLK) -I #H elim (lt_refl_false j) /2 width=3 by lt_to_le_to_lt/ qed-. -lemma frees_inv_lref_skip: ∀L,l,j,i. L ⊢ i ϵ 𝐅*[l]⦃#j⦄ → yinj j < l → j = i. +lemma frees_inv_lref_skip: ∀L,l,j,i. L ⊢ i ϵ 𝐅*[l]⦃#j⦄ → yinj j < l → yinj j = i. #L #l #j #i #H #Hjl elim (frees_inv_lref … H) -H // * #I #K #W #Hlj elim (ylt_yle_false … Hlj) -Hlj // qed-. -lemma frees_inv_lref_ge: ∀L,l,j,i. L ⊢ i ϵ 𝐅*[l]⦃#j⦄ → i ≤ j → j = i. +lemma frees_inv_lref_ge: ∀L,l,j,i. L ⊢ i ϵ 𝐅*[l]⦃#j⦄ → i ≤ j → yinj j = i. #L #l #j #i #H #Hij elim (frees_inv_lref … H) -H // -* #I #K #W #_ #Hji elim (lt_refl_false j) -I -L -K -W -l /2 width=3 by lt_to_le_to_lt/ +* #I #K #W #_ #Hji elim (ylt_yle_false … Hji Hij) qed-. lemma frees_inv_lref_lt: ∀L,l,j,i.L ⊢ i ϵ 𝐅*[l]⦃#j⦄ → j < i → - ∃∃I,K,W. l ≤ yinj j & ⬇[j] L ≡ K.ⓑ{I}W & K ⊢ (i-j-1) ϵ 𝐅*[yinj 0]⦃W⦄. + ∃∃I,K,W. l ≤ yinj j & ⬇[j] L ≡ K.ⓑ{I}W & K ⊢ ⫰(i-j) ϵ 𝐅*[yinj 0]⦃W⦄. #L #l #j #i #H #Hji elim (frees_inv_lref … H) -H -[ #H elim (lt_refl_false j) // +[ #H elim (ylt_yle_false … Hji) // | * /2 width=5 by ex3_3_intro/ ] qed-. lemma frees_inv_bind: ∀a,I,L,W,U,l,i. L ⊢ i ϵ 𝐅*[l]⦃ⓑ{a,I}W.U⦄ → - L ⊢ i ϵ 𝐅*[l]⦃W⦄ ∨ L.ⓑ{I}W ⊢ i+1 ϵ 𝐅*[⫯l]⦃U⦄ . + L ⊢ i ϵ 𝐅*[l]⦃W⦄ ∨ L.ⓑ{I}W ⊢ ⫯i ϵ 𝐅*[⫯l]⦃U⦄ . #a #J #L #V #U #l #i #H elim (frees_inv … H) -H [ #HnX elim (nlift_inv_bind … HnX) -HnX /4 width=2 by frees_eq, or_intror, or_introl/ | * #I #K #W #j #Hlj #Hji #HnX #HLK #HW elim (nlift_inv_bind … HnX) -HnX [ /4 width=9 by frees_be, or_introl/ | #HnT @or_intror @(frees_be … HnT) -HnT - [4,5,6: /2 width=1 by drop_drop, yle_succ, lt_minus_to_plus/ - |7: >minus_plus_plus_l // + [4: lapply (yle_succ … Hlj) // (**) + |5: lapply (ylt_succ … Hji) // (**) + |6: /2 width=4 by drop_drop/ + |7: (plus_minus_m_m j 1) in HnU; // yminus_succ + lapply (ylt_O … Hj) -Hj #Hj #H + lapply (ylt_inv_succ … H) -H #Hji #HnU #HLK #HW + @(frees_be … Hlj Hji … HW) -HW -Hlj -Hji (**) (* explicit constructor *) + [2: #X #H lapply (nlift_bind_dx … H) /2 width=2 by/ (**) + |3: lapply (drop_inv_drop1_lt … HLK ?) -HLK // + |*: skip ] qed. @@ -157,7 +164,7 @@ qed-. (* Advanced inversion lemmas ************************************************) lemma frees_inv_bind_O: ∀a,I,L,W,U,i. L ⊢ i ϵ 𝐅*[0]⦃ⓑ{a,I}W.U⦄ → - L ⊢ i ϵ 𝐅*[0]⦃W⦄ ∨ L.ⓑ{I}W ⊢ i+1 ϵ 𝐅*[0]⦃U⦄ . + L ⊢ i ϵ 𝐅*[0]⦃W⦄ ∨ L.ⓑ{I}W ⊢ ⫯i ϵ 𝐅*[0]⦃U⦄ . #a #I #L #W #U #i #H elim (frees_inv_bind … H) -H /3 width=3 by frees_weak, or_intror, or_introl/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/multiple/frees_append.ma b/matita/matita/contribs/lambdadelta/basic_2/multiple/frees_append.ma index 8f6835955..ee8324cc9 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/multiple/frees_append.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/multiple/frees_append.ma @@ -25,9 +25,10 @@ lemma frees_append: ∀L2,U,l,i. L2 ⊢ i ϵ 𝐅*[l]⦃U⦄ → i ≤ |L2| → #I #L2 #K2 #U #W #l #i #j #Hlj #Hji #HnU #HLK2 #_ #IHW #Hi #L1 lapply (drop_fwd_length_minus2 … HLK2) normalize #H0 lapply (drop_O1_append_sn_le … HLK2 … L1) -HLK2 -[ -I -L1 -K2 -U -W -l /3 width=3 by lt_to_le, lt_to_le_to_lt/ +[ -I -L1 -K2 -U -W -l /4 width=3 by ylt_yle_trans, ylt_inv_inj, lt_to_le/ | #HLK2 @(frees_be … HnU HLK2) // -HnU -HLK2 @IHW -IHW - >(minus_plus_m_m (|K2|) 1) >H0 -H0 /2 width=1 by monotonic_le_minus_l2/ + >(minus_plus_m_m (|K2|) 1) >H0 -H0 yminus_SO2 + /3 width=1 by monotonic_yle_minus_dx, yle_pred/ ] qed. @@ -37,13 +38,14 @@ fact frees_inv_append_aux: ∀L,U,l,i. L ⊢ i ϵ 𝐅*[l]⦃U⦄ → ∀L1,L2. i ≤ |L2| → L2 ⊢ i ϵ 𝐅*[l]⦃U⦄. #L #U #l #i #H elim H -L -U -l -i /3 width=2 by frees_eq/ #Z #L #Y #U #X #l #i #j #Hlj #Hji #HnU #HLY #_ #IHW #L1 #L2 #H #Hi destruct -elim (drop_O1_lt (Ⓕ) L2 j) [2: -Z -Y -L1 -X -U -l /2 width=3 by lt_to_le_to_lt/ ] +elim (drop_O1_lt (Ⓕ) L2 j) [2: -Z -Y -L1 -X -U -l /3 width=3 by ylt_yle_trans, ylt_inv_inj/ ] #I #K2 #W #HLK2 lapply (drop_fwd_length_minus2 … HLK2) normalize #H0 lapply (drop_O1_inv_append1_le … HLY … HLK2) -HLY -[ -Z -I -Y -K2 -L1 -X -U -W -l /3 width=3 by lt_to_le, lt_to_le_to_lt/ +[ -Z -I -Y -K2 -L1 -X -U -W -l /4 width=3 by ylt_yle_trans, ylt_inv_inj, lt_to_le/ | normalize #H destruct @(frees_be … HnU HLK2) -HnU -HLK2 // @IHW -IHW // - >(minus_plus_m_m (|K2|) 1) >H0 -H0 /2 width=1 by monotonic_le_minus_l2/ + >(minus_plus_m_m (|K2|) 1) >H0 -H0 yminus_SO2 + /3 width=1 by monotonic_yle_minus_dx, yle_pred/ ] qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/multiple/frees_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/multiple/frees_lift.ma index a95f1ac3f..65b629206 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/multiple/frees_lift.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/multiple/frees_lift.ma @@ -12,6 +12,7 @@ (* *) (**************************************************************************) +include "ground_2/ynat/ynat_max.ma". include "basic_2/substitution/drop_drop.ma". include "basic_2/multiple/frees.ma". @@ -23,19 +24,19 @@ lemma frees_dec: ∀L,U,l,i. Decidable (frees l L U i). #L #U @(f2_ind … rfw … L U) -L -U #x #IH #L * * [ -IH /3 width=5 by frees_inv_sort, or_intror/ -| #j #Hx #l #i elim (lt_or_eq_or_gt i j) #Hji - [ -x @or_intror #H elim (lt_refl_false i) - lapply (frees_inv_lref_ge … H ?) -L -l /2 width=1 by lt_to_le/ +| #j #Hx #l #i elim (ylt_split_eq i j) #Hji + [ -x @or_intror #H elim (ylt_yle_false … Hji) + lapply (frees_inv_lref_ge … H ?) -L -l /2 width=1 by ylt_fwd_le/ | -x /2 width=1 by or_introl/ | elim (ylt_split j l) #Hli - [ -x @or_intror #H elim (lt_refl_false i) + [ -x @or_intror #H elim (ylt_yle_false … Hji) lapply (frees_inv_lref_skip … H ?) -L // | elim (lt_or_ge j (|L|)) #Hj [ elim (drop_O1_lt (Ⓕ) L j) // -Hj #I #K #W #HLK destruct elim (IH K W … 0 (i-j-1)) -IH [1,3: /3 width=5 by frees_lref_be, drop_fwd_rfw, or_introl/ ] #HnW @or_intror #H elim (frees_inv_lref_lt … H) // #Z #Y #X #_ #HLY -l lapply (drop_mono … HLY … HLK) -L #H destruct /2 width=1 by/ - | -x @or_intror #H elim (lt_refl_false i) + | -x @or_intror #H elim (ylt_yle_false … Hji) lapply (frees_inv_lref_free … H ?) -l // ] ] @@ -53,7 +54,7 @@ lemma frees_dec: ∀L,U,l,i. Decidable (frees l L U i). qed-. lemma frees_S: ∀L,U,l,i. L ⊢ i ϵ 𝐅*[yinj l]⦃U⦄ → ∀I,K,W. ⬇[l] L ≡ K.ⓑ{I}W → - (K ⊢ i-l-1 ϵ 𝐅*[0]⦃W⦄ → ⊥) → L ⊢ i ϵ 𝐅*[⫯l]⦃U⦄. + (K ⊢ ⫰(i-l) ϵ 𝐅*[0]⦃W⦄ → ⊥) → L ⊢ i ϵ 𝐅*[⫯l]⦃U⦄. #L #U #l #i #H elim (frees_inv … H) -H /3 width=2 by frees_eq/ * #I #K #W #j #Hlj #Hji #HnU #HLK #HW #I0 #K0 #W0 #HLK0 #HnW0 lapply (yle_inv_inj … Hlj) -Hlj #Hlj @@ -66,7 +67,7 @@ elim (le_to_or_lt_eq … Hlj) -Hlj qed. (* Note: lemma 1250 *) -lemma frees_bind_dx_O: ∀a,I,L,W,U,i. L.ⓑ{I}W ⊢ i+1 ϵ 𝐅*[0]⦃U⦄ → +lemma frees_bind_dx_O: ∀a,I,L,W,U,i. L.ⓑ{I}W ⊢ ⫯i ϵ 𝐅*[0]⦃U⦄ → L ⊢ i ϵ 𝐅*[0]⦃ⓑ{a,I}W.U⦄. #a #I #L #W #U #i #HU elim (frees_dec L W 0 i) /4 width=5 by frees_S, frees_bind_dx, frees_bind_sn/ @@ -82,20 +83,23 @@ lemma frees_lift_ge: ∀K,T,l,i. K ⊢ i ϵ𝐅*[l]⦃T⦄ → [ #K #T #l #i #HnT #L #s #l0 #m0 #_ #U #HTU #Hl0i -K -s @frees_eq #X #HXU elim (lift_div_le … HTU … HXU) -U /2 width=2 by/ | #I #K #K0 #T #V #l #i #j #Hlj #Hji #HnT #HK0 #HV #IHV #L #s #l0 #m0 #HLK #U #HTU #Hl0i - elim (lt_or_ge j l0) #H1 - [ elim (drop_trans_lt … HLK … HK0) // -K #L0 #W #HL0 #HLK0 #HVW - @(frees_be … HL0) -HL0 -HV - /3 width=3 by lt_plus_to_minus_r, lt_to_le_to_lt/ - [ #X #HXU >(plus_minus_m_m l0 1) in HTU; /2 width=2 by ltn_to_ltO/ #HTU - elim (lift_div_le … HXU … HTU ?) -U /2 width=2 by monotonic_pred/ - | >minus_plus yminus_SO2 #HLK0 #HVW + @(frees_be … HL0) -HL0 -HV /3 width=3 by ylt_plus_dx2_trans/ + [ lapply (ylt_fwd_lt_O1 … H0) #H1 + #X #HXU <(ymax_pre_sn l0 1) in HTU; /2 width=1 by ylt_fwd_le_succ1/ #HTU + <(ylt_inv_O1 l0) in H0; // -H1 #H0 + elim (lift_div_le … HXU … HTU ?) -U /2 width=2 by ylt_fwd_succ2/ + | >yplus_minus_comm_inj /2 width=1 by ylt_fwd_le/ + commutative_plus -HLK0 #HLK0 @(frees_be … HLK0) -HLK0 -IHV - /2 width=1 by yle_plus_dx1_trans, lt_minus_to_plus/ - #X #HXU elim (lift_div_le … HTU … HXU) -U /2 width=2 by/ + /2 width=1 by monotonic_ylt_plus_dx, yle_plus_dx1_trans/ + [ #X minus_plus >minus_plus >plus_minus /2 width=1 by monotonic_le_minus_l/ + [ /3 width=1 by monotonic_yle_minus_dx, yle_pred/ + | >yplus_pred1 /2 width=1 by ylt_to_minus/ + ymax_pre_sn /2 width=2 by/ | #I #L #K0 #U #W #l #i #j #Hli #Hij #HnU #HLK0 #_ #IHW #K #s #l0 #m0 #HLK #T #HTU #Hlm0i - elim (lt_or_ge j l0) #H1 + elim (ylt_split j l0) #H1 [ elim (drop_conf_lt … HLK … HLK0) -L // #L0 #V #H #HKL0 #HVW - elim (le_inv_plus_l … Hlm0i) #H0 #Hm0i + elim (yle_inv_plus_inj2 … Hlm0i) #H0 #Hm0i @(frees_be … H) -H [ /3 width=1 by yle_plus_dx1_trans, monotonic_yle_minus_dx/ - | /2 width=3 by lt_to_le_to_lt/ - | #X #HXT elim (lift_trans_ge … HXT … HTU) -T /2 width=2 by/ + | /2 width=3 by ylt_yle_trans/ + | #X #HXT elim (lift_trans_ge … HXT … HTU) -T /2 width=2 by ylt_fwd_le_succ1/ | lapply (IHW … HKL0 … HVW ?) // -I -K -K0 -L0 -V -W -T -U -s - >minus_plus >minus_plus >plus_minus /2 width=1 by monotonic_le_minus_l/ + >yplus_pred1 /2 width=1 by ylt_to_minus/ + commutative_plus |] #H2 - [ -L -I -W lapply (lt_plus_to_minus ???? H2) // -H2 #H2 - elim (lift_split … HTU j (m0-1)) -HTU // - [ >minus_minus_associative /2 width=2 by ltn_to_ltO/ commutative_plus /3 width=1 by le_minus_to_plus, monotonic_pred/ + | elim (ylt_split j (l0+m0)) #H2 + [ -L -I -W elim (yle_inv_inj2 … H1) -H1 #x #H1 #H destruct + lapply (ylt_plus2_to_minus_inj1 … H2) /2 width=1 by yle_inj/ #H3 + lapply (ylt_fwd_lt_O1 … H3) -H3 #H3 + elim (lift_split … HTU j (m0-1)) -HTU /2 width=1 by yle_inj/ + [ >minus_minus_associative /2 width=1 by ylt_inv_inj/ yminus_SO2 >yplus_pred2 /2 width=1 by ylt_fwd_le_pred2/ ] | lapply (drop_conf_ge … HLK … HLK0 ?) // -L #HK0 - elim (le_inv_plus_l … H2) -H2 #H2 #Hm0j + elim ( yle_inv_plus_inj2 … H2) -H2 #H2 #Hm0j @(frees_be … HK0) [ /2 width=1 by monotonic_yle_minus_dx/ - | /2 width=1 by monotonic_lt_minus_l/ - | #X #HXT elim (lift_trans_le … HXT … HTU) -T // arith_b1 /2 width=5 by/ + | /2 width=1 by monotonic_ylt_minus_dx/ + | #X #HXT elim (lift_trans_le … HXT … HTU) -T // + ymax_pre_sn /2 width=2 by/ + | yplus_minus_assoc_comm_inj // + >ymax_pre_sn /3 width=5 by yle_trans, ylt_fwd_le/ ] ] ] diff --git a/matita/matita/contribs/lambdadelta/basic_2/multiple/lifts.ma b/matita/matita/contribs/lambdadelta/basic_2/multiple/lifts.ma index be2d50f1e..7a091abce 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/multiple/lifts.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/multiple/lifts.ma @@ -18,7 +18,7 @@ include "basic_2/multiple/mr2_plus.ma". (* GENERIC TERM RELOCATION **************************************************) -inductive lifts: list2 nat nat → relation term ≝ +inductive lifts: list2 ynat nat → relation term ≝ | lifts_nil : ∀T. lifts (◊) T T | lifts_cons: ∀T1,T,T2,cs,l,m. ⬆[l,m] T1 ≡ T → lifts cs T T2 → lifts ({l, m} @ cs) T1 T2 diff --git a/matita/matita/contribs/lambdadelta/basic_2/multiple/lifts_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/multiple/lifts_lift.ma index 102ed0ceb..2c693baaa 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/multiple/lifts_lift.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/multiple/lifts_lift.ma @@ -12,6 +12,7 @@ (* *) (**************************************************************************) +include "ground_2/ynat/ynat_max.ma". include "basic_2/substitution/lift_lift.ma". include "basic_2/multiple/mr2_minus.ma". include "basic_2/multiple/lifts.ma". @@ -37,7 +38,7 @@ lemma lifts_lift_trans: ∀cs,i,i0. @⦃i, cs⦄ ≡ i0 → ∀T1,T0. ⬆*[cs0] T1 ≡ T0 → ∀T2. ⬆[O, i0 + 1] T0 ≡ T2 → ∃∃T. ⬆[0, i + 1] T1 ≡ T & ⬆*[cs] T ≡ T2. -#cs elim cs -cs normalize +#cs elim cs -cs [ #i #x #H1 #cs0 #H2 #T1 #T0 #HT10 #T2 <(at_inv_nil … H1) -x #HT02 lapply (minuss_inv_nil1 … H2) -H2 #H @@ -45,15 +46,18 @@ lemma lifts_lift_trans: ∀cs,i,i0. @⦃i, cs⦄ ≡ i0 → >(lifts_inv_nil … H) -T1 /2 width=3 by lifts_nil, ex2_intro/ | #l #m #cs #IHcs #i #i0 #H1 #cs0 #H2 #T1 #T0 #HT10 #T2 #HT02 elim (at_inv_cons … H1) -H1 * #Hil #Hi0 - [ elim (minuss_inv_cons1_lt … H2) -H2 [2: /2 width=1 by lt_minus_to_plus/ ] #cs1 #Hcs1 yplus_SO2 >yplus_SO2 >yminus_succ #H elim (pluss_inv_cons2 … H) -H #cs2 #H1 #H2 destruct - elim (lifts_inv_cons … HT10) -HT10 #T >minus_plus #HT1 #HT0 + elim (lifts_inv_cons … HT10) -HT10 #T #HT1 #HT0 elim (IHcs … Hi0 … Hcs1 … HT0 … HT02) -IHcs -Hi0 -Hcs1 -T0 #T0 #HT0 #HT02 - elim (lift_trans_le … HT1 … HT0) -T /2 width=1 by/ #T #HT1 yplus_SO2 >ymax_pre_sn + /3 width=5 by lifts_cons, ex2_intro, ylt_fwd_le_succ1/ | >commutative_plus in Hi0; #Hi0 - lapply (minuss_inv_cons1_ge … H2 ?) -H2 [ /2 width=1 by le_S_S/ ] (lift_inv_gref2 … H) -H /2 width=1 by llpx_sn_gref/ | #a #I #L1 #L2 #W #U #lt #_ #_ #IHV #IHT #X #l #m #H #Hltlm destruct - elim (lift_inv_bind2 … H) -H #V #T #HVW >commutative_plus #HTU #H destruct + elim (lift_inv_bind2 … H) -H #V #T #HVW #HTU #H destruct @(llpx_sn_bind) /2 width=4 by/ (**) (* full auto fails *) @(IHT … HTU) /2 width=1 by yle_succ/ | #I #L1 #L2 #W #U #lt #_ #_ #IHV #IHT #X #l #m #H #Hltlm destruct diff --git a/matita/matita/contribs/lambdadelta/basic_2/multiple/llpx_sn_alt.ma b/matita/matita/contribs/lambdadelta/basic_2/multiple/llpx_sn_alt.ma index a849ade55..f40046c5f 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/multiple/llpx_sn_alt.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/multiple/llpx_sn_alt.ma @@ -33,14 +33,14 @@ theorem llpx_sn_llpx_sn_alt: ∀R,T,L1,L2,l. llpx_sn R l T L1 L2 → llpx_sn_alt #HL12 #IHU @conj // #I1 #I2 #K1 #K2 #V1 #V2 #i #Hli #H #HLK1 #HLK2 elim (frees_inv … H) -H [ -x #HnU elim (IHU … HnU HLK1 HLK2) -IHU -HnU -HLK1 -HLK2 /2 width=1 by conj/ -| * #J1 #K10 #W10 #j #Hlj #Hji #HnU #HLK10 #HnW10 destruct +| * #J1 #K10 #W10 #j #Hlj #Hji #HnU #HLK10 yminus_inj >yminus_inj #HnW10 destruct lapply (drop_fwd_drop2 … HLK10) #H - lapply (drop_conf_ge … H … HLK1 ?) -H /2 width=1 by lt_to_le/ (minus_plus_m_m j (i+1)) in ⊢ (%→?); >commutative_plus yminus_SO2 #HnV1 #HKY1 #HKY2 (**) (* full auto too slow *) lapply (drop_trans_ge … H1 … HKY1 ?) -H1 -HKY1 // #HLY1 lapply (drop_trans_ge … H2 … HKY2 ?) -H2 -HKY2 // #HLY2 -/4 width=14 by frees_be, yle_plus_dx2_trans, yle_succ_dx/ +/4 width=9 by frees_be, yle_plus_dx2_trans, yle_succ_dx, ylt_inj/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/multiple/llpx_sn_alt_rec.ma b/matita/matita/contribs/lambdadelta/basic_2/multiple/llpx_sn_alt_rec.ma index 6cd1b9bd9..870a4bbef 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/multiple/llpx_sn_alt_rec.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/multiple/llpx_sn_alt_rec.ma @@ -83,11 +83,10 @@ lemma llpx_sn_alt_r_inv_bind: ∀R,a,I,L1,L2,V,T,l. llpx_sn_alt_r R l (ⓑ{a,I}V #I1 #I2 #K1 #K2 #V1 #V2 #i #Hli #H #HLK1 #HLK2 [ elim (IH … HLK1 HLK2) -IH -HLK1 -HLK2 /3 width=9 by nlift_bind_sn, and3_intro/ -| lapply (yle_inv_succ1 … Hli) -Hli * #Hli #Hi +| lapply (yle_inv_succ1 … Hli) -Hli * #Hli #Hi (lift_inv_sort2 … H) -X lapply (drop_fwd_length_eq1 … HLK1 HLK2 HL12) -L1 -L2 -l0 -m @@ -317,7 +317,7 @@ lemma llpx_sn_inv_lift_be: ∀R,L1,L2,U,l0. llpx_sn R l0 U L1 L2 → /3 width=3 by ylt_yle_trans, ylt_inj/ | lapply (drop_conf_ge … HLK1 … HLK11 ?) // -L1 lapply (drop_conf_ge … HLK2 … HLK22 ?) // -L2 -Hil0 -Hl0 -Hl0m - elim (le_inv_plus_l … Hil) -Hil /3 width=9 by llpx_sn_lref, yle_inj/ + elim (yle_inv_plus_inj2 … Hil) -Hil /3 width=9 by llpx_sn_lref, yle_inj/ ] | #L1 #L2 #l0 #i #HL1 #HL2 #HL12 #K1 #K2 #l #m #HLK1 #HLK2 #X #H #Hl0 #Hl0m elim (lift_inv_lref2 … H) -H * #_ #H destruct @@ -333,7 +333,7 @@ lemma llpx_sn_inv_lift_be: ∀R,L1,L2,U,l0. llpx_sn R l0 U L1 L2 → lapply (drop_fwd_length_eq1 … HLK1 HLK2 HL12) -L1 -L2 -l0 -m /2 width=1 by llpx_sn_gref/ | #a #I #L1 #L2 #W #U #l0 #_ #_ #IHW #IHU #K1 #K2 #l #m #HLK1 #HLK2 #X #H #Hl0 #Hl0m elim (lift_inv_bind2 … H) -H - >commutative_plus #V #T #HVW #HTU #H destruct + #V #T #HVW #HTU #H destruct @llpx_sn_bind [ /2 width=5 by/ ] -IHW (**) (* explicit constructor *) @(IHU … HTU) -IHU -HTU /2 width=1 by drop_skip, yle_succ/ | #I #L1 #L2 #W #U #l0 #_ #_ #IHW #IHU #K1 #K2 #l #m #HLK1 #HLK2 #X #H #Hl0 #Hl0m elim (lift_inv_flat2 … H) -H @@ -343,7 +343,7 @@ qed-. lemma llpx_sn_inv_lift_ge: ∀R,L1,L2,U,l0. llpx_sn R l0 U L1 L2 → ∀K1,K2,l,m. ⬇[Ⓕ, l, m] L1 ≡ K1 → ⬇[Ⓕ, l, m] L2 ≡ K2 → - ∀T. ⬆[l, m] T ≡ U → yinj l + m ≤ l0 → llpx_sn R (l0-m) T K1 K2. + ∀T. ⬆[l, m] T ≡ U → l + m ≤ l0 → llpx_sn R (l0-m) T K1 K2. #R #L1 #L2 #U #l0 #H elim H -L1 -L2 -U -l0 [ #L1 #L2 #l0 #k #HL12 #K1 #K2 #l #m #HLK1 #HLK2 #X #H #_ >(lift_inv_sort2 … H) -X lapply (drop_fwd_length_eq1 … HLK1 HLK2 HL12) -L1 -L2 -l @@ -352,8 +352,8 @@ lemma llpx_sn_inv_lift_ge: ∀R,L1,L2,U,l0. llpx_sn R l0 U L1 L2 → * #Hil #H destruct [ -Hil0 | -Hlml0 ] lapply (drop_fwd_length_eq1 … HLK1 HLK2 HL12) -L1 -L2 [ /4 width=3 by llpx_sn_skip, yle_plus1_to_minus_inj2, ylt_yle_trans, ylt_inj/ - | elim (le_inv_plus_l … Hil) -Hil #_ - /4 width=1 by llpx_sn_skip, monotonic_ylt_minus_dx, yle_inj/ + | elim (yle_inv_plus_inj2 … Hil) -Hil + /3 width=1 by llpx_sn_skip, monotonic_ylt_minus_dx/ ] | #I #L1 #L2 #K11 #K22 #W1 #W2 #l0 #i #Hil0 #HLK11 #HLK22 #HK12 #HW12 #_ #K1 #K2 #l #m #HLK1 #HLK2 #X #H #Hlml0 elim (lift_inv_lref2 … H) -H * #Hil #H destruct diff --git a/matita/matita/contribs/lambdadelta/basic_2/multiple/mr2.ma b/matita/matita/contribs/lambdadelta/basic_2/multiple/mr2.ma index 6b5684072..71869b02b 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/multiple/mr2.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/multiple/mr2.ma @@ -12,16 +12,17 @@ (* *) (**************************************************************************) +include "ground_2/ynat/ynat_lt.ma". include "basic_2/notation/relations/rat_3.ma". include "basic_2/grammar/term_vector.ma". (* MULTIPLE RELOCATION WITH PAIRS *******************************************) -inductive at: list2 nat nat → relation nat ≝ +inductive at: list2 ynat nat → relation nat ≝ | at_nil: ∀i. at (◊) i i -| at_lt : ∀cs,l,m,i1,i2. i1 < l → +| at_lt : ∀cs,l,m,i1,i2. yinj i1 < l → at cs i1 i2 → at ({l, m} @ cs) i1 i2 -| at_ge : ∀cs,l,m,i1,i2. l ≤ i1 → +| at_ge : ∀cs,l,m,i1,i2. l ≤ yinj i1 → at cs (i1 + m) i2 → at ({l, m} @ cs) i1 i2 . @@ -61,14 +62,12 @@ lemma at_inv_cons_lt: ∀cs,l,m,i1,i2. @⦃i1, {l, m} @ cs⦄ ≡ i2 → i1 < l → @⦃i1, cs⦄ ≡ i2. #cs #l #m #i1 #m2 #H elim (at_inv_cons … H) -H * // #Hli1 #_ #Hi1l -lapply (le_to_lt_to_lt … Hli1 Hi1l) -Hli1 -Hi1l #Hl -elim (lt_refl_false … Hl) +elim (ylt_yle_false … Hi1l Hli1) qed-. lemma at_inv_cons_ge: ∀cs,l,m,i1,i2. @⦃i1, {l, m} @ cs⦄ ≡ i2 → l ≤ i1 → @⦃i1 + m, cs⦄ ≡ i2. #cs #l #m #i1 #m2 #H elim (at_inv_cons … H) -H * // #Hi1l #_ #Hli1 -lapply (le_to_lt_to_lt … Hli1 Hi1l) -Hli1 -Hi1l #Hl -elim (lt_refl_false … Hl) +elim (ylt_yle_false … Hi1l Hli1) qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/multiple/mr2_minus.ma b/matita/matita/contribs/lambdadelta/basic_2/multiple/mr2_minus.ma index ac00f87b3..3c5f8da5c 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/multiple/mr2_minus.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/multiple/mr2_minus.ma @@ -12,16 +12,17 @@ (* *) (**************************************************************************) +include "ground_2/ynat/ynat_minus.ma". include "basic_2/notation/relations/rminus_3.ma". include "basic_2/multiple/mr2.ma". (* MULTIPLE RELOCATION WITH PAIRS *******************************************) -inductive minuss: nat → relation (list2 nat nat) ≝ +inductive minuss: nat → relation (list2 ynat nat) ≝ | minuss_nil: ∀i. minuss i (◊) (◊) -| minuss_lt : ∀cs1,cs2,l,m,i. i < l → minuss i cs1 cs2 → +| minuss_lt : ∀cs1,cs2,l,m,i. yinj i < l → minuss i cs1 cs2 → minuss i ({l, m} @ cs1) ({l - i, m} @ cs2) -| minuss_ge : ∀cs1,cs2,l,m,i. l ≤ i → minuss (m + i) cs1 cs2 → +| minuss_ge : ∀cs1,cs2,l,m,i. l ≤ yinj i → minuss (m + i) cs1 cs2 → minuss i ({l, m} @ cs1) cs2 . @@ -63,14 +64,12 @@ lemma minuss_inv_cons1_ge: ∀cs1,cs2,l,m,i. {l, m} @ cs1 ▭ i ≡ cs2 → l ≤ i → cs1 ▭ m + i ≡ cs2. #cs1 #cs2 #l #m #i #H elim (minuss_inv_cons1 … H) -H * // #cs #Hil #_ #_ #Hli -lapply (lt_to_le_to_lt … Hil Hli) -Hil -Hli #Hi -elim (lt_refl_false … Hi) +elim (ylt_yle_false … Hil Hli) qed-. lemma minuss_inv_cons1_lt: ∀cs1,cs2,l,m,i. {l, m} @ cs1 ▭ i ≡ cs2 → i < l → ∃∃cs. cs1 ▭ i ≡ cs & cs2 = {l - i, m} @ cs. #cs1 #cs2 #l #m #i #H elim (minuss_inv_cons1 … H) -H * /2 width=3 by ex2_intro/ -#Hli #_ #Hil lapply (lt_to_le_to_lt … Hil Hli) -Hil -Hli -#Hi elim (lt_refl_false … Hi) +#Hli #_ #Hil elim (ylt_yle_false … Hil Hli) qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/multiple/mr2_plus.ma b/matita/matita/contribs/lambdadelta/basic_2/multiple/mr2_plus.ma index 99b2d4b17..455b669be 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/multiple/mr2_plus.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/multiple/mr2_plus.ma @@ -12,11 +12,12 @@ (* *) (**************************************************************************) +include "ground_2/ynat/ynat_plus.ma". include "basic_2/multiple/mr2.ma". (* MULTIPLE RELOCATION WITH PAIRS *******************************************) -let rec pluss (cs:list2 nat nat) (i:nat) on cs ≝ match cs with +let rec pluss (cs:list2 ynat nat) (i:nat) on cs ≝ match cs with [ nil2 ⇒ ◊ | cons2 l m cs ⇒ {l + i, m} @ pluss cs i ]. @@ -24,6 +25,11 @@ let rec pluss (cs:list2 nat nat) (i:nat) on cs ≝ match cs with interpretation "plus (multiple relocation with pairs)" 'plus x y = (pluss x y). +(* Basic properties *********************************************************) + +lemma pluss_SO2: ∀l,m,cs. ({l, m} @ cs) + 1 = {⫯l, m} @ cs + 1. +// qed. + (* Basic inversion lemmas ***************************************************) lemma pluss_inv_nil2: ∀i,cs. cs + i = ◊ → cs = ◊. @@ -33,8 +39,9 @@ qed. lemma pluss_inv_cons2: ∀i,l,m,cs2,cs. cs + i = {l, m} @ cs2 → ∃∃cs1. cs1 + i = cs2 & cs = {l - i, m} @ cs1. -#i #l #m #cs2 * normalize -[ #H destruct -| #l1 #m1 #cs1 #H destruct /2 width=3 by ex2_intro/ +#i #l #m #cs2 * +[ normalize #H destruct +| #l1 #m1 #cs1 whd in ⊢ (??%?→?); #H destruct + >yplus_minus_inj /2 width=3 by ex2_intro/ ] qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cnr.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/cnr.ma index c70640808..11b911c78 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/reduction/cnr.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/cnr.ma @@ -29,7 +29,7 @@ lemma cnr_inv_delta: ∀G,L,K,V,i. ⬇[i] L ≡ K.ⓓV → ⦃G, L⦄ ⊢ ➡ #G #L #K #V #i #HLK #H elim (lift_total V 0 (i+1)) #W #HVW lapply (H W ?) -H [ /3 width=6 by cpr_delta/ ] -HLK #H destruct -elim (lift_inv_lref2_be … HVW) -HVW // +elim (lift_inv_lref2_be … HVW) -HVW /2 width=1 by ylt_inj/ qed-. lemma cnr_inv_abst: ∀a,G,L,V,T. ⦃G, L⦄ ⊢ ➡ 𝐍⦃ⓛ{a}V.T⦄ → ⦃G, L⦄ ⊢ ➡ 𝐍⦃V⦄ ∧ ⦃G, L.ⓛV⦄ ⊢ ➡ 𝐍⦃T⦄. diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cnx.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/cnx.ma index e6d1fcf4b..942ccc285 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/reduction/cnx.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/cnx.ma @@ -40,7 +40,7 @@ lemma cnx_inv_delta: ∀h,g,I,G,L,K,V,i. ⬇[i] L ≡ K.ⓑ{I}V → ⦃G, L⦄ #h #g #I #G #L #K #V #i #HLK #H elim (lift_total V 0 (i+1)) #W #HVW lapply (H W ?) -H [ /3 width=7 by cpx_delta/ ] -HLK #H destruct -elim (lift_inv_lref2_be … HVW) -HVW // +elim (lift_inv_lref2_be … HVW) -HVW /2 width=1 by ylt_inj/ qed-. lemma cnx_inv_abst: ∀h,g,a,G,L,V,T. ⦃G, L⦄ ⊢ ➡[h, g] 𝐍⦃ⓛ{a}V.T⦄ → diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cpr.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/cpr.ma index 6dafc6d8c..27682aa74 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/reduction/cpr.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/cpr.ma @@ -81,7 +81,7 @@ lemma cpr_delift: ∀G,K,V,T1,L,l. ⬇[l] L ≡ (K.ⓓV) → #G #K #V #T1 elim T1 -T1 [ * /2 width=4 by cpr_atom, lift_sort, lift_gref, ex2_2_intro/ #i #L #l #HLK elim (lt_or_eq_or_gt i l) - #Hil [1,3: /3 width=4 by cpr_atom, lift_lref_ge_minus, lift_lref_lt, ex2_2_intro/ ] + #Hil [1,3: /4 width=4 by lift_lref_ge_minus, lift_lref_lt, ylt_inj, yle_inj, ex2_2_intro/ ] destruct elim (lift_total V 0 (i+1)) #W #HVW elim (lift_split … HVW i i) /3 width=6 by cpr_delta, ex2_2_intro/ @@ -97,8 +97,7 @@ fact lstas_cpr_aux: ∀h,G,L,T1,T2,d. ⦃G, L⦄ ⊢ T1 •*[h, d] T2 → d = 0 → ⦃G, L⦄ ⊢ T1 ➡ T2. #h #G #L #T1 #T2 #d #H elim H -G -L -T1 -T2 -d /3 width=1 by cpr_eps, cpr_flat, cpr_bind/ -[ #G #L #d #k #H0 destruct normalize // -| #G #L #K #V1 #V2 #W2 #i #d #HLK #_ #HVW2 #IHV12 #H destruct +[ #G #L #K #V1 #V2 #W2 #i #d #HLK #_ #HVW2 #IHV12 #H destruct /3 width=6 by cpr_delta/ | #G #L #K #V1 #V2 #W2 #i #d #_ #_ #_ #_ (lift_mono … H1 … H2) -H1 -H2 // | #G #K #KV #V #V2 #W2 #i #HKV #HV2 #HVW2 #IHV2 #L #s #l #m #HLK #U1 #H #U2 #HWU2 elim (lift_inv_lref1 … H) * #Hil #H destruct - [ elim (lift_trans_ge … HVW2 … HWU2) -W2 // plus_plus_comm_23 #HVU2 + | lapply (lift_trans_be … HVW2 … HWU2 ? ?) -W2 /2 width=1 by yle_succ_dx/ >plus_plus_comm_23 #HVU2 lapply (drop_trans_ge_comm … HLK … HKV ?) -K // -Hil /3 width=6 by cpr_delta, drop_inv_gen/ ] | #a #I #G #K #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #L #s #l #m #HLK #U1 #H1 #U2 #H2 @@ -70,10 +71,11 @@ lemma cpr_inv_lift1: ∀G. d_deliftable_sn (cpr G). elim (lift_inv_lref2 … H) -H * #Hil #H destruct [ elim (drop_conf_lt … HLK … HLV) -L // #L #U #HKL #HLV #HUV elim (IHV2 … HLV … HUV) -V #U2 #HUV2 #HU2 - elim (lift_trans_le … HUV2 … HVW2) -V2 // >minus_plus yplus_SO2 >ymax_pre_sn /3 width=8 by cpr_delta, ylt_fwd_le_succ1, ex2_intro/ + | elim (yle_inv_plus_inj2 … Hil) #Hlim #Hmi + lapply (yle_inv_inj … Hmi) -Hmi #Hmi lapply (drop_conf_ge … HLK … HLV ?) -L // #HKLV - elim (lift_split … HVW2 l (i - m + 1)) -HVW2 [2,3,4: /2 width=1 by le_S_S, le_S/ ] -Hil -Hlim + elim (lift_split … HVW2 l (i - m + 1)) -HVW2 [2,3,4: /2 width=1 by yle_succ_dx, le_S_S/ ] -Hil -Hlim #V1 #HV1 >plus_minus // (lift_inv_sort1 … H2) -U2 /2 width=2 by cpx_st/ | #I #G #K #KV #V #V2 #W2 #i #HKV #HV2 #HVW2 #IHV2 #L #s #l #m #HLK #U1 #H #U2 #HWU2 elim (lift_inv_lref1 … H) * #Hil #H destruct - [ elim (lift_trans_ge … HVW2 … HWU2) -W2 // plus_plus_comm_23 #HVU2 + | lapply (lift_trans_be … HVW2 … HWU2 ? ?) -W2 /2 width=1 by yle_succ_dx/ >plus_plus_comm_23 #HVU2 lapply (drop_trans_ge_comm … HLK … HKV ?) -K /3 width=7 by cpx_delta, drop_inv_gen/ ] | #a #I #G #K #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #L #s #l #m #HLK #U1 #H1 #U2 #H2 @@ -103,10 +104,11 @@ lemma cpx_inv_lift1: ∀h,g,G. d_deliftable_sn (cpx h g G). elim (lift_inv_lref2 … H) -H * #Hil #H destruct [ elim (drop_conf_lt … HLK … HLV) -L // #L #U #HKL #HLV #HUV elim (IHV2 … HLV … HUV) -V #U2 #HUV2 #HU2 - elim (lift_trans_le … HUV2 … HVW2) -V2 // >minus_plus yplus_SO2 >ymax_pre_sn /3 width=9 by cpx_delta, ylt_fwd_le_succ1, ex2_intro/ + | elim (yle_inv_plus_inj2 … Hil) #Hlim #Hmi + lapply (yle_inv_inj … Hmi) -Hmi #Hmi lapply (drop_conf_ge … HLK … HLV ?) -L // #HKLV - elim (lift_split … HVW2 l (i - m + 1)) -HVW2 /3 width=1 by le_S, le_S_S/ -Hil -Hlim + elim (lift_split … HVW2 l (i - m + 1)) -HVW2 /3 width=1 by yle_succ, yle_pred_sn, le_S_S/ -Hil -Hlim #V1 #HV1 >plus_minus // yplus_SO2 #Hji + [ -IH elim (frees_inv_lift_be … H2 … HLK2 … HW0U2) /2 width=1 by ylt_fwd_succ2/ + | lapply (frees_inv_lift_ge … H2 … HLK2 … HW0U2 ?) -L2 -U2 // destruct + /4 width=11 by frees_lref_be, fqup_lref, yle_succ1_inj/ ] ] | -IH #p #HG #HL #HU #U2 #H1 >(cpx_inv_gref1 … H1) -H1 destruct diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/aaa_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/static/aaa_lift.ma index 91723374f..e83255951 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/static/aaa_lift.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/static/aaa_lift.ma @@ -26,8 +26,8 @@ lemma aaa_lift: ∀G,L1,T1,A. ⦃G, L1⦄ ⊢ T1 ⁝ A → ∀L2,s,l,m. ⬇[s, l >(lift_inv_sort1 … H) -H // | #I #G #L1 #K1 #V1 #B #i #HLK1 #_ #IHB #L2 #s #l #m #HL21 #T2 #H elim (lift_inv_lref1 … H) -H * #Hil #H destruct - [ elim (drop_trans_le … HL21 … HLK1) -L1 /2 width=2 by lt_to_le/ #X #HLK2 #H - elim (drop_inv_skip2 … H) -H /2 width=1 by lt_plus_to_minus_r/ -Hil #K2 #V2 #HK21 #HV12 #H destruct + [ elim (drop_trans_le … HL21 … HLK1) -L1 /2 width=2 by ylt_fwd_le/ #X #HLK2 #H + elim (drop_inv_skip2 … H) -H /2 width=1 by ylt_to_minus/ -Hil #K2 #V2 #HK21 #HV12 #H destruct /3 width=9 by aaa_lref/ | lapply (drop_trans_ge … HL21 … HLK1 ?) -L1 /3 width=9 by aaa_lref, drop_inv_gen/ diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/da_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/static/da_lift.ma index 3f3926c17..25cde075b 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/static/da_lift.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/static/da_lift.ma @@ -27,16 +27,16 @@ lemma da_lift: ∀h,g,G,L1,T1,d. ⦃G, L1⦄ ⊢ T1 ▪[h, g] d → >(lift_inv_sort1 … H) -X /2 width=1 by da_sort/ | #G #L1 #K1 #V1 #i #d #HLK1 #_ #IHV1 #L2 #s #l #m #HL21 #X #H elim (lift_inv_lref1 … H) * #Hil #H destruct - [ elim (drop_trans_le … HL21 … HLK1) -L1 /2 width=2 by lt_to_le/ #X #HLK2 #H - elim (drop_inv_skip2 … H) -H /2 width=1 by lt_plus_to_minus_r/ -Hil #K2 #V2 #HK21 #HV12 #H destruct + [ elim (drop_trans_le … HL21 … HLK1) -L1 /2 width=2 by ylt_fwd_le/ #X #HLK2 #H + elim (drop_inv_skip2 … H) -H /2 width=1 by ylt_to_minus/ -Hil #K2 #V2 #HK21 #HV12 #H destruct /3 width=9 by da_ldef/ | lapply (drop_trans_ge … HL21 … HLK1 ?) -L1 /3 width=8 by da_ldef, drop_inv_gen/ ] | #G #L1 #K1 #W1 #i #d #HLK1 #_ #IHW1 #L2 #s #l #m #HL21 #X #H elim (lift_inv_lref1 … H) * #Hil #H destruct - [ elim (drop_trans_le … HL21 … HLK1) -L1 /2 width=2 by lt_to_le/ #X #HLK2 #H - elim (drop_inv_skip2 … H) -H /2 width=1 by lt_plus_to_minus_r/ -Hil #K2 #W2 #HK21 #HW12 #H destruct + [ elim (drop_trans_le … HL21 … HLK1) -L1 /2 width=2 by ylt_fwd_le/ #X #HLK2 #H + elim (drop_inv_skip2 … H) -H /2 width=1 by ylt_to_minus/ -Hil #K2 #W2 #HK21 #HW12 #H destruct /3 width=8 by da_ldec/ | lapply (drop_trans_ge … HL21 … HLK1 ?) -L1 /3 width=8 by da_ldec, drop_inv_gen/ diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/cpy.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/cpy.ma index 8fe2e8d26..cd16f5042 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/substitution/cpy.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/cpy.ma @@ -58,7 +58,7 @@ lemma cpy_full: ∀I,G,K,V,T1,L,l. ⬇[l] L ≡ K.ⓑ{I}V → [ * #i #L #l #HLK /2 width=4 by lift_sort, lift_gref, ex2_2_intro/ elim (lt_or_eq_or_gt i l) #Hil - /3 width=4 by lift_lref_ge_minus, lift_lref_lt, ex2_2_intro/ + /4 width=4 by lift_lref_ge_minus, lift_lref_lt, ex2_2_intro, ylt_inj, yle_inj/ (**) (* was /3 width=4/ without inj *) destruct elim (lift_total V 0 (i+1)) #W #HVW elim (lift_split … HVW i i) @@ -90,6 +90,7 @@ lemma cpy_weak_top: ∀G,L,T1,T2,l,m. lapply (drop_fwd_length_lt2 … HLK) /4 width=5 by cpy_subst, ylt_yle_trans, ylt_inj/ | #a #I #G #L #V1 #V2 normalize in match (|L.ⓑ{I}V2|); (**) (* |?| does not work *) + yplus_SO2 >yminus_succ /2 width=1 by cpy_bind/ | /2 width=1 by cpy_flat/ ] @@ -155,9 +156,9 @@ lemma cpy_fwd_up: ∀G,L,U1,U2,lt,mt. ⦃G, L⦄ ⊢ U1 ▶[lt, mt] U2 → | #I #G #L #K #V #W #i #lt #mt #Hlti #Hilmt #HLK #HVW #T1 #l #m #H #Hllt #Hlmlmt elim (lift_inv_lref2 … H) -H * #Hil #H destruct [ -V -Hilmt -Hlmlmt | -Hlti -Hllt ] [ elim (ylt_yle_false … Hllt) -Hllt /3 width=3 by yle_ylt_trans, ylt_inj/ - | elim (le_inv_plus_l … Hil) #Hlim #Hmi - elim (lift_split … HVW l (i-m+1) ? ? ?) [2,3,4: /2 width=1 by le_S_S, le_S/ ] -Hlim - #T2 #_ >plus_minus // plus_minus /2 width=1 by yle_inv_inj/ ymax_pre_sn_comm // (**) (* explicit constructor *) ] | #a #I #G #L #W1 #W2 #U1 #U2 #lt #mt #_ #_ #IHW12 #IHU12 #X #l #m #H #Hllt #Hlmlmt diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/cpy_cpy.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/cpy_cpy.ma index ef48b05af..7a65a2db5 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/substitution/cpy_cpy.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/cpy_cpy.ma @@ -85,7 +85,8 @@ theorem cpy_trans_ge: ∀G,L,T1,T0,l,m. ⦃G, L⦄ ⊢ T1 ▶[l, m] T0 → elim (cpy_inv_atom1 … H) -H [ #H destruct // | * #J #K #V #i #Hl2i #Hilm2 #HLK #HVT2 #H destruct - lapply (ylt_yle_trans … (l+m) … Hilm2) /2 width=5 by cpy_subst, monotonic_yle_plus_dx/ + lapply (ylt_yle_trans … (l+m) … Hilm2) + /2 width=5 by cpy_subst, monotonic_yle_plus_sn/ ] | #I #G #L #K #V #V2 #i #l #m #Hli #Hilm #HLK #HVW #T2 #HVT2 #Hm lapply (cpy_weak … HVT2 0 (i+1) ? ?) -HVT2 /3 width=1 by yle_plus_dx2_trans, yle_succ/ diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/cpy_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/cpy_lift.ma index 1d42acd6f..44a7f3d76 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/substitution/cpy_lift.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/cpy_lift.ma @@ -29,11 +29,11 @@ lemma cpy_lift_le: ∀G,K,T1,T2,lt,mt. ⦃G, K⦄ ⊢ T1 ▶[lt, mt] T2 → >(lift_mono … H1 … H2) -H1 -H2 // | #I #G #K #KV #V #W #i #lt #mt #Hlti #Hilmt #HKV #HVW #L #U1 #U2 #s #l #m #HLK #H #HWU2 #Hlmtl lapply (ylt_yle_trans … Hlmtl … Hilmt) -Hlmtl #Hil - lapply (ylt_inv_inj … Hil) -Hil #Hil lapply (lift_inv_lref1_lt … H … Hil) -H #H destruct - elim (lift_trans_ge … HVW … HWU2) -W // yplus_SO2 >yminus_succ2 #W #HVW #HWU2 + elim (drop_trans_le … HLK … HKV) -K /2 width=2 by ylt_fwd_le/ #X #HLK #H + elim (drop_inv_skip2 … H) -H /2 width=1 by ylt_to_minus/ -Hil #K #Y #_ #HVY >(lift_mono … HVY … HVW) -Y -HVW #H destruct /2 width=5 by cpy_subst/ | #a #I #G #K #V1 #V2 #T1 #T2 #lt #mt #_ #_ #IHV12 #IHT12 #L #U1 #U2 #s #l #m #HLK #H1 #H2 #Hlmtl elim (lift_inv_bind1 … H1) -H1 #VV1 #TT1 #HVV1 #HTT1 #H1 @@ -57,16 +57,16 @@ lemma cpy_lift_be: ∀G,K,T1,T2,lt,mt. ⦃G, K⦄ ⊢ T1 ▶[lt, mt] T2 → elim (lift_inv_lref1 … H) -H * #Hil #H destruct [ -Hltl lapply (ylt_yle_trans … (lt+mt+m) … Hilmt) // -Hilmt #Hilmtm - elim (lift_trans_ge … HVW … HWU2) -W // yplus_SO2 + [2: >yplus_O1 /2 width=1 by ylt_fwd_le_succ1/ ] >yminus_succ2 #W #HVW #HWU2 + elim (drop_trans_le … HLK … HKV) -K /2 width=1 by ylt_fwd_le/ #X #HLK #H + elim (drop_inv_skip2 … H) -H /2 width=1 by ylt_to_minus/ -Hil #K #Y #_ #HVY >(lift_mono … HVY … HVW) -V #H destruct /2 width=5 by cpy_subst/ | -Hlti - elim (yle_inv_inj2 … Hltl) -Hltl #ltt #Hltl #H destruct - lapply (transitive_le … Hltl Hil) -Hltl #Hlti - lapply (lift_trans_be … HVW … HWU2 ? ?) -W /2 width=1 by le_S/ >plus_plus_comm_23 #HVU2 + lapply (yle_trans … Hltl … Hil) -Hltl #Hlti + lapply (lift_trans_be … HVW … HWU2 ? ?) -W /2 width=1 by yle_succ_dx/ >plus_plus_comm_23 #HVU2 lapply (drop_trans_ge_comm … HLK … HKV ?) -K // -Hil - /4 width=5 by cpy_subst, drop_inv_gen, monotonic_ylt_plus_dx, yle_plus_dx1_trans, yle_inj/ + /3 width=5 by cpy_subst, drop_inv_gen, monotonic_ylt_plus_dx, yle_plus_dx1_trans/ ] | #a #I #G #K #V1 #V2 #T1 #T2 #lt #mt #_ #_ #IHV12 #IHT12 #L #U1 #U2 #s #l #m #HLK #H1 #H2 #Hltl #Hllmt elim (lift_inv_bind1 … H1) -H1 #VV1 #TT1 #HVV1 #HTT1 #H1 @@ -89,10 +89,9 @@ lemma cpy_lift_ge: ∀G,K,T1,T2,lt,mt. ⦃G, K⦄ ⊢ T1 ▶[lt, mt] T2 → >(lift_mono … H1 … H2) -H1 -H2 // | #I #G #K #KV #V #W #i #lt #mt #Hlti #Hilmt #HKV #HVW #L #U1 #U2 #s #l #m #HLK #H #HWU2 #Hllt lapply (yle_trans … Hllt … Hlti) -Hllt #Hil - elim (yle_inv_inj2 … Hil) -Hil #ll #Hlli #H0 destruct - lapply (lift_inv_lref1_ge … H … Hlli) -H #H destruct - lapply (lift_trans_be … HVW … HWU2 ? ?) -W /2 width=1 by le_S/ >plus_plus_comm_23 #HVU2 - lapply (drop_trans_ge_comm … HLK … HKV ?) -K // -Hlli + lapply (lift_inv_lref1_ge … H … Hil) -H #H destruct + lapply (lift_trans_be … HVW … HWU2 ? ?) -W /2 width=1 by yle_succ_dx/ >plus_plus_comm_23 #HVU2 + lapply (drop_trans_ge_comm … HLK … HKV ?) -K // -Hil /3 width=5 by cpy_subst, drop_inv_gen, monotonic_ylt_plus_dx, monotonic_yle_plus_dx/ | #a #I #G #K #V1 #V2 #T1 #T2 #lt #mt #_ #_ #IHV12 #IHT12 #L #U1 #U2 #s #l #m #HLK #H1 #H2 #Hllt elim (lift_inv_bind1 … H1) -H1 #VV1 #TT1 #HVV1 #HTT1 #H1 @@ -120,10 +119,11 @@ lemma cpy_inv_lift1_le: ∀G,L,U1,U2,lt,mt. ⦃G, L⦄ ⊢ U1 ▶[lt, mt] U2 → ] | #I #G #L #KV #V #W #i #lt #mt #Hlti #Hilmt #HLKV #HVW #K #s #l #m #HLK #T1 #H #Hlmtl lapply (ylt_yle_trans … Hlmtl … Hilmt) -Hlmtl #Hil - lapply (ylt_inv_inj … Hil) -Hil #Hil lapply (lift_inv_lref2_lt … H … Hil) -H #H destruct elim (drop_conf_lt … HLK … HLKV) -L // #L #U #HKL #_ #HUV - elim (lift_trans_le … HUV … HVW) -V // >minus_plus minus_plus yplus_SO2 >ymax_pre_sn /2 width=1 by ylt_fwd_le_succ1/ -Hil + /3 width=5 by cpy_subst, ex2_intro/ | #a #I #G #L #W1 #W2 #U1 #U2 #lt #mt #_ #_ #IHW12 #IHU12 #K #s #l #m #HLK #X #H #Hlmtl elim (lift_inv_bind2 … H) -H #V1 #T1 #HVW1 #HTU1 #H destruct elim (IHW12 … HLK … HVW1) -IHW12 // #V2 #HV12 #HVW2 @@ -139,7 +139,7 @@ qed-. lemma cpy_inv_lift1_be: ∀G,L,U1,U2,lt,mt. ⦃G, L⦄ ⊢ U1 ▶[lt, mt] U2 → ∀K,s,l,m. ⬇[s, l, m] L ≡ K → ∀T1. ⬆[l, m] T1 ≡ U1 → - lt ≤ l → yinj l + m ≤ lt + mt → + lt ≤ l → l + m ≤ lt + mt → ∃∃T2. ⦃G, K⦄ ⊢ T1 ▶[lt, mt-m] T2 & ⬆[l, m] T2 ≡ U2. #G #L #U1 #U2 #lt #mt #H elim H -G -L -U1 -U2 -lt -mt [ * #i #G #L #lt #mt #K #s #l #m #_ #T1 #H #_ #_ @@ -147,18 +147,21 @@ lemma cpy_inv_lift1_be: ∀G,L,U1,U2,lt,mt. ⦃G, L⦄ ⊢ U1 ▶[lt, mt] U2 → | elim (lift_inv_lref2 … H) -H * #Hil #H destruct /3 width=3 by lift_lref_ge_minus, lift_lref_lt, ex2_intro/ | lapply (lift_inv_gref2 … H) -H #H destruct /2 width=3 by ex2_intro/ ] -| #I #G #L #KV #V #W #i #lt #mt #Hlti #Hilmt #HLKV #HVW #K #s #l #m #HLK #T1 #H #Hltl #Hlmlmt - lapply (yle_fwd_plus_ge_inj … Hltl Hlmlmt) #Hmmt +| #I #G #L #KV #V #W #i #x #mt #Hlti #Hilmt #HLKV #HVW #K #s #l #m #HLK #T1 #H #Hltl #Hlmlmt + elim (yle_inv_inj2 … Hlti) -Hlti #lt #Hlti #H destruct + lapply (yle_fwd_plus_yge … Hltl Hlmlmt) #Hmmt elim (lift_inv_lref2 … H) -H * #Hil #H destruct [ -Hltl -Hilmt | -Hlti -Hlmlmt ] - [ lapply (ylt_yle_trans i l (lt+(mt-m)) ? ?) /2 width=1 by ylt_inj/ + [ lapply (ylt_yle_trans i l (lt+(mt-m)) ? ?) // [ >yplus_minus_assoc_inj /2 width=1 by yle_plus1_to_minus_inj2/ ] -Hlmlmt #Hilmtm elim (drop_conf_lt … HLK … HLKV) -L // #L #U #HKL #_ #HUV - elim (lift_trans_le … HUV … HVW) -V // >minus_plus yplus_SO2 >ymax_pre_sn /2 width=1 by ylt_fwd_le_succ1/ -Hil + /4 width=5 by cpy_subst, ex2_intro, yle_inj/ + | elim (yle_inv_plus_inj2 … Hil) #Hlim #Hmi + lapply (yle_inv_inj … Hmi) -Hmi #Hmi + lapply (yle_trans … Hltl (i-m) ?) // -Hltl #Hltim lapply (drop_conf_ge … HLK … HLKV ?) -L // #HKV - elim (lift_split … HVW l (i-m+1)) -HVW [2,3,4: /2 width=1 by le_S_S, le_S/ ] -Hil -Hlim + elim (lift_split … HVW l (i-m+1)) -HVW [2,3,4: /2 width=1 by yle_succ_dx, le_S_S/ ] -Hil -Hlim #V1 #HV1 >plus_minus // yplus_minus_assoc_inj /3 width=1 by monotonic_ylt_minus_dx, yle_inj/ @@ -179,7 +182,7 @@ qed-. (* Basic_1: was: subst1_gen_lift_ge *) lemma cpy_inv_lift1_ge: ∀G,L,U1,U2,lt,mt. ⦃G, L⦄ ⊢ U1 ▶[lt, mt] U2 → ∀K,s,l,m. ⬇[s, l, m] L ≡ K → ∀T1. ⬆[l, m] T1 ≡ U1 → - yinj l + m ≤ lt → + l + m ≤ lt → ∃∃T2. ⦃G, K⦄ ⊢ T1 ▶[lt-m, mt] T2 & ⬆[l, m] T2 ≡ U2. #G #L #U1 #U2 #lt #mt #H elim H -G -L -U1 -U2 -lt -mt [ * #i #G #L #lt #mt #K #s #l #m #_ #T1 #H #_ @@ -191,13 +194,14 @@ lemma cpy_inv_lift1_ge: ∀G,L,U1,U2,lt,mt. ⦃G, L⦄ ⊢ U1 ▶[lt, mt] U2 → lapply (yle_trans … Hlmlt … Hlti) #Hlmi elim (yle_inv_plus_inj2 … Hlmlt) -Hlmlt #_ #Hmlt elim (yle_inv_plus_inj2 … Hlmi) #Hlim #Hmi - lapply (lift_inv_lref2_ge … H ?) -H /2 width=1 by yle_inv_inj/ #H destruct - lapply (drop_conf_ge … HLK … HLKV ?) -L /2 width=1 by yle_inv_inj/ #HKV - elim (lift_split … HVW l (i-m+1)) -HVW [2,3,4: /3 width=1 by yle_inv_inj, le_S_S, le_S/ ] -Hlmi -Hlim - #V0 #HV10 >plus_minus /2 width=1 by yle_inv_inj/ plus_minus // ymax_pre_sn_comm // ] -Hllt -Hltlm #HU1 @@ -227,7 +231,7 @@ qed-. lemma cpy_inv_lift1_be_up: ∀G,L,U1,U2,lt,mt. ⦃G, L⦄ ⊢ U1 ▶[lt, mt] U2 → ∀K,s,l,m. ⬇[s, l, m] L ≡ K → ∀T1. ⬆[l, m] T1 ≡ U1 → - lt ≤ l → lt + mt ≤ yinj l + m → + lt ≤ l → lt + mt ≤ l + m → ∃∃T2. ⦃G, K⦄ ⊢ T1 ▶[lt, l-lt] T2 & ⬆[l, m] T2 ≡ U2. #G #L #U1 #U2 #lt #mt #HU12 #K #s #l #m #HLK #T1 #HTU1 #Hltl #Hlmtlm lapply (cpy_weak … HU12 lt (l+m-lt) ? ?) -HU12 // @@ -237,7 +241,7 @@ qed-. lemma cpy_inv_lift1_le_up: ∀G,L,U1,U2,lt,mt. ⦃G, L⦄ ⊢ U1 ▶[lt, mt] U2 → ∀K,s,l,m. ⬇[s, l, m] L ≡ K → ∀T1. ⬆[l, m] T1 ≡ U1 → - lt ≤ l → l ≤ lt + mt → lt + mt ≤ yinj l + m → + lt ≤ l → l ≤ lt + mt → lt + mt ≤ l + m → ∃∃T2. ⦃G, K⦄ ⊢ T1 ▶[lt, l - lt] T2 & ⬆[l, m] T2 ≡ U2. #G #L #U1 #U2 #lt #mt #HU12 #K #s #l #m #HLK #T1 #HTU1 #Hltl #Hllmt #Hlmtlm elim (cpy_split_up … HU12 l) -HU12 // #U #HU1 #HU2 diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/cpy_nlift.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/cpy_nlift.ma index bcf52015d..3a6450724 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/substitution/cpy_nlift.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/cpy_nlift.ma @@ -21,18 +21,18 @@ include "basic_2/substitution/cpy.ma". (* Inversion lemmas on negated relocation ***********************************) lemma cpy_fwd_nlift2_ge: ∀G,L,U1,U2,l,m. ⦃G, L⦄ ⊢ U1 ▶[l, m] U2 → - ∀i. l ≤ yinj i → (∀T2. ⬆[i, 1] T2 ≡ U2 → ⊥) → + ∀i. l ≤ i → (∀T2. ⬆[i, 1] T2 ≡ U2 → ⊥) → (∀T1. ⬆[i, 1] T1 ≡ U1 → ⊥) ∨ ∃∃I,K,W,j. l ≤ yinj j & j < i & ⬇[j]L ≡ K.ⓑ{I}W & - (∀V. ⬆[i-j-1, 1] V ≡ W → ⊥) & (∀T1. ⬆[j, 1] T1 ≡ U1 → ⊥). + (∀V. ⬆[⫰(i-j), 1] V ≡ W → ⊥) & (∀T1. ⬆[j, 1] T1 ≡ U1 → ⊥). #G #L #U1 #U2 #l #m #H elim H -G -L -U1 -U2 -l -m [ /3 width=2 by or_introl/ | #I #G #L #K #V #W #j #l #m #Hlj #Hjlm #HLK #HVW #i #Hli #HnW - elim (lt_or_ge j i) #Hij + elim (ylt_split j i) #Hij [ @or_intror @(ex5_4_intro … HLK) // -HLK - [ #X #HXV elim (lift_trans_le … HXV … HVW ?) -V // - #Y #HXY >minus_plus yplus_SO2 >ymax_pre_sn /2 width=2 by ylt_fwd_le_succ1/ + | -HnW /3 width=7 by lift_inv_lref2_be, ylt_inj/ ] | elim (lift_split … HVW i j) -HVW // #X #_ #H elim HnW -HnW // @@ -44,13 +44,12 @@ lemma cpy_fwd_nlift2_ge: ∀G,L,U1,U2,l,m. ⦃G, L⦄ ⊢ U1 ▶[l, m] U2 → ] | #HnU2 elim (IHU12 … HnU2) -IHU12 -HnU2 -IHW12 /2 width=1 by yle_succ/ [ /4 width=9 by nlift_bind_dx, or_introl/ - | * #J #K #W #j #Hlj #Hji #HLK #HnW - elim (yle_inv_succ1 … Hlj) -Hlj #Hlj #Hj - lapply (ylt_O … Hj) -Hj #Hj - lapply (drop_inv_drop1_lt … HLK ?) // -HLK #HLK - >(plus_minus_m_m j 1) in ⊢ (%→?); [2: /3 width=3 by yle_trans, yle_inv_inj/ ] - #HnU1 yminus_succ #Hji #HLK #HnW + lapply (drop_inv_drop1_lt … HLK ?) /2 width=1 by ylt_O/ -HLK #HLK + commutative_plus normalize #H destruct +| #I #L1 #L2 #V1 #V2 #l #m #_ #_ #H elim (ysucc_inv_O_dx … H) ] qed-. -lemma drop_inv_O1_pair1: ∀I,K,L2,V,s,m. ⬇[s, 0, m] K. ⓑ{I} V ≡ L2 → +lemma drop_inv_O1_pair1: ∀I,K,L2,V,s,m. ⬇[s, yinj 0, m] K. ⓑ{I} V ≡ L2 → (m = 0 ∧ L2 = K.ⓑ{I}V) ∨ - (0 < m ∧ ⬇[s, 0, m-1] K ≡ L2). + (0 < m ∧ ⬇[s, yinj 0, m-1] K ≡ L2). /2 width=3 by drop_inv_O1_pair1_aux/ qed-. lemma drop_inv_pair1: ∀I,K,L2,V,s. ⬇[s, 0, 0] K.ⓑ{I}V ≡ L2 → L2 = K.ⓑ{I}V. @@ -102,7 +102,7 @@ qed-. (* Basic_1: was: drop_gen_drop *) lemma drop_inv_drop1_lt: ∀I,K,L2,V,s,m. - ⬇[s, 0, m] K.ⓑ{I}V ≡ L2 → 0 < m → ⬇[s, 0, m-1] K ≡ L2. + ⬇[s, yinj 0, m] K.ⓑ{I}V ≡ L2 → 0 < m → ⬇[s, yinj 0, m-1] K ≡ L2. #I #K #L2 #V #s #m #H #Hm elim (drop_inv_O1_pair1 … H) -H * // #H destruct elim (lt_refl_false … Hm) @@ -115,27 +115,27 @@ qed-. fact drop_inv_skip1_aux: ∀L1,L2,s,l,m. ⬇[s, l, m] L1 ≡ L2 → 0 < l → ∀I,K1,V1. L1 = K1.ⓑ{I}V1 → - ∃∃K2,V2. ⬇[s, l-1, m] K1 ≡ K2 & - ⬆[l-1, m] V2 ≡ V1 & + ∃∃K2,V2. ⬇[s, ⫰l, m] K1 ≡ K2 & + ⬆[⫰l, m] V2 ≡ V1 & L2 = K2.ⓑ{I}V2. #L1 #L2 #s #l #m * -L1 -L2 -l -m [ #l #m #_ #_ #J #K1 #W1 #H destruct -| #I #L #V #H elim (lt_refl_false … H) -| #I #L1 #L2 #V #m #_ #H elim (lt_refl_false … H) +| #I #L #V #H elim (ylt_yle_false … H) -H // +| #I #L1 #L2 #V #m #_ #H elim (ylt_yle_false … H) -H // | #I #L1 #L2 #V1 #V2 #l #m #HL12 #HV21 #_ #J #K1 #W1 #H destruct /2 width=5 by ex3_2_intro/ ] qed-. (* Basic_1: was: drop_gen_skip_l *) lemma drop_inv_skip1: ∀I,K1,V1,L2,s,l,m. ⬇[s, l, m] K1.ⓑ{I}V1 ≡ L2 → 0 < l → - ∃∃K2,V2. ⬇[s, l-1, m] K1 ≡ K2 & - ⬆[l-1, m] V2 ≡ V1 & + ∃∃K2,V2. ⬇[s, ⫰l, m] K1 ≡ K2 & + ⬆[⫰l, m] V2 ≡ V1 & L2 = K2.ⓑ{I}V2. /2 width=3 by drop_inv_skip1_aux/ qed-. -lemma drop_inv_O1_pair2: ∀I,K,V,s,m,L1. ⬇[s, 0, m] L1 ≡ K.ⓑ{I}V → +lemma drop_inv_O1_pair2: ∀I,K,V,s,m,L1. ⬇[s, yinj 0, m] L1 ≡ K.ⓑ{I}V → (m = 0 ∧ L1 = K.ⓑ{I}V) ∨ - ∃∃I1,K1,V1. ⬇[s, 0, m-1] K1 ≡ K.ⓑ{I}V & L1 = K1.ⓑ{I1}V1 & 0 < m. + ∃∃I1,K1,V1. ⬇[s, yinj 0, m-1] K1 ≡ K.ⓑ{I}V & L1 = K1.ⓑ{I1}V1 & 0 < m. #I #K #V #s #m * [ #H elim (drop_inv_atom1 … H) -H #H destruct | #L1 #I1 #V1 #H @@ -148,24 +148,24 @@ qed-. fact drop_inv_skip2_aux: ∀L1,L2,s,l,m. ⬇[s, l, m] L1 ≡ L2 → 0 < l → ∀I,K2,V2. L2 = K2.ⓑ{I}V2 → - ∃∃K1,V1. ⬇[s, l-1, m] K1 ≡ K2 & - ⬆[l-1, m] V2 ≡ V1 & + ∃∃K1,V1. ⬇[s, ⫰l, m] K1 ≡ K2 & + ⬆[⫰l, m] V2 ≡ V1 & L1 = K1.ⓑ{I}V1. #L1 #L2 #s #l #m * -L1 -L2 -l -m [ #l #m #_ #_ #J #K2 #W2 #H destruct -| #I #L #V #H elim (lt_refl_false … H) -| #I #L1 #L2 #V #m #_ #H elim (lt_refl_false … H) +| #I #L #V #H elim (ylt_yle_false … H) -H // +| #I #L1 #L2 #V #m #_ #H elim (ylt_yle_false … H) -H // | #I #L1 #L2 #V1 #V2 #l #m #HL12 #HV21 #_ #J #K2 #W2 #H destruct /2 width=5 by ex3_2_intro/ ] qed-. (* Basic_1: was: drop_gen_skip_r *) lemma drop_inv_skip2: ∀I,L1,K2,V2,s,l,m. ⬇[s, l, m] L1 ≡ K2.ⓑ{I}V2 → 0 < l → - ∃∃K1,V1. ⬇[s, l-1, m] K1 ≡ K2 & ⬆[l-1, m] V2 ≡ V1 & + ∃∃K1,V1. ⬇[s, ⫰l, m] K1 ≡ K2 & ⬆[⫰l, m] V2 ≡ V1 & L1 = K1.ⓑ{I}V1. /2 width=3 by drop_inv_skip2_aux/ qed-. -lemma drop_inv_O1_gt: ∀L,K,m,s. ⬇[s, 0, m] L ≡ K → |L| < m → +lemma drop_inv_O1_gt: ∀L,K,m,s. ⬇[s, yinj 0, m] L ≡ K → |L| < m → s = Ⓣ ∧ K = ⋆. #L elim L -L [| #L #Z #X #IHL ] #K #m #s #H normalize in ⊢ (?%?→?); #H1m [ elim (drop_inv_atom1 … H) -H elim s -s /2 width=1 by conj/ @@ -177,26 +177,45 @@ lemma drop_inv_O1_gt: ∀L,K,m,s. ⬇[s, 0, m] L ≡ K → |L| < m → ] qed-. +lemma drop_inv_Y1: ∀L,K,m,s. ⬇[s, ∞, m] L ≡ K → + L = K ∧ (s = Ⓕ → m = 0). +#L elim L -L +[ #Y #m #s #H elim (drop_inv_atom1 … H) -H /3 width=1 by conj/ +| #L #I #V #IHL #Y #m #s #H elim (drop_inv_skip1 … H) -H // + #K #W #HLK #HWV #H destruct + lapply (lift_inv_Y1 … HWV) -HWV #H destruct + elim (IHL … HLK) -IHL -HLK /3 width=1 by conj/ +] +qed-. + (* Basic properties *********************************************************) lemma drop_refl_atom_O2: ∀s,l. ⬇[s, l, O] ⋆ ≡ ⋆. /2 width=1 by drop_atom/ qed. +lemma drop_Y1: ∀m,s. (s = Ⓕ → m = 0) → ∀L. ⬇[s, ∞, m] L ≡ L. +#m #s #H #L elim L -L /3 width=3 by drop_atom, drop_skip/ +qed. + (* Basic_1: was by definition: drop_refl *) lemma drop_refl: ∀L,l,s. ⬇[s, l, 0] L ≡ L. #L elim L -L // -#L #I #V #IHL #l #s @(nat_ind_plus … l) -l /2 width=1 by drop_pair, drop_skip/ +#L #I #V #IHL #x #s elim (ynat_cases x) +[ #H destruct // +| * #l #H destruct /2 width=1 by drop_skip/ +] qed. lemma drop_drop_lt: ∀I,L1,L2,V,s,m. - ⬇[s, 0, m-1] L1 ≡ L2 → 0 < m → ⬇[s, 0, m] L1.ⓑ{I}V ≡ L2. + ⬇[s, yinj 0, m-1] L1 ≡ L2 → 0 < m → ⬇[s, yinj 0, m] L1.ⓑ{I}V ≡ L2. #I #L1 #L2 #V #s #m #HL12 #Hm >(plus_minus_m_m m 1) /2 width=1 by drop_drop/ qed. lemma drop_skip_lt: ∀I,L1,L2,V1,V2,s,l,m. - ⬇[s, l-1, m] L1 ≡ L2 → ⬆[l-1, m] V2 ≡ V1 → 0 < l → + ⬇[s, ⫰l, m] L1 ≡ L2 → ⬆[⫰l, m] V2 ≡ V1 → 0 < l → ⬇[s, l, m] L1. ⓑ{I} V1 ≡ L2.ⓑ{I}V2. -#I #L1 #L2 #V1 #V2 #s #l #m #HL12 #HV21 #Hl >(plus_minus_m_m l 1) /2 width=1 by drop_skip/ +#I #L1 #L2 #V1 #V2 #s #l #m #HL12 #HV21 #Hl <(ylt_inv_O1 … Hl) -Hl +/2 width=1 by drop_skip/ qed. lemma drop_O1_le: ∀s,m,L. m ≤ |L| → ∃K. ⬇[s, 0, m] L ≡ K. @@ -215,8 +234,8 @@ lemma drop_O1_lt: ∀s,L,m. m < |L| → ∃∃I,K,V. ⬇[s, 0, m] L ≡ K.ⓑ{I} ] qed-. -lemma drop_O1_pair: ∀L,K,m,s. ⬇[s, 0, m] L ≡ K → m ≤ |L| → ∀I,V. - ∃∃J,W. ⬇[s, 0, m] L.ⓑ{I}V ≡ K.ⓑ{J}W. +lemma drop_O1_pair: ∀L,K,m,s. ⬇[s, yinj 0, m] L ≡ K → m ≤ |L| → ∀I,V. + ∃∃J,W. ⬇[s, yinj 0, m] L.ⓑ{I}V ≡ K.ⓑ{J}W. #L elim L -L [| #L #Z #X #IHL ] #K #m #s #H normalize #Hm #I #V [ elim (drop_inv_atom1 … H) -H #H <(le_n_O_to_eq … Hm) -m #Hs destruct /2 width=3 by ex1_2_intro/ @@ -336,27 +355,32 @@ lemma drop_fwd_drop2: ∀L1,I2,K2,V2,s,m. ⬇[s, O, m] L1 ≡ K2. ⓑ{I2} V2 → qed-. lemma drop_fwd_length_ge: ∀L1,L2,l,m,s. ⬇[s, l, m] L1 ≡ L2 → |L1| ≤ l → |L2| = |L1|. -#L1 #L2 #l #m #s #H elim H -L1 -L2 -l -m // normalize -[ #I #L1 #L2 #V #m #_ #_ #H elim (le_plus_xSy_O_false … H) -| /4 width=2 by le_plus_to_le_r, eq_f/ +#L1 #L2 #l #m #s #H elim H -L1 -L2 -l -m // +[ #I #L1 #L2 #V #m #_ #_ #H elim (ylt_yle_false … H) -H normalize // +| #I #L1 #L2 #V1 #V2 #l #m #_ #_ #IH yplus_SO2 #H + lapply (yle_inv_succ … H) -H #H normalize /3 width=1 by eq_f2/ ] qed-. lemma drop_fwd_length_le_le: ∀L1,L2,l,m,s. ⬇[s, l, m] L1 ≡ L2 → l ≤ |L1| → m ≤ |L1| - l → |L2| = |L1| - m. -#L1 #L2 #l #m #s #H elim H -L1 -L2 -l -m // normalize -[ /3 width=2 by le_plus_to_le_r/ -| #I #L1 #L2 #V1 #V2 #l #m #_ #_ #IHL12 >minus_plus_plus_l - #Hl #Hm lapply (le_plus_to_le_r … Hl) -Hl - #Hl >IHL12 // -L2 >plus_minus /2 width=3 by transitive_le/ +#L1 #L2 #l #m #s #H elim H -L1 -L2 -l -m // +[ #I #L1 #L2 #V #m #_ minus_plus_plus_l yplus_SO2 /3 width=1 by yle_inv_succ/ +| #I #L1 #L2 #V1 #V2 #l #m #_ #_ #IHL12 yplus_SO2 #H + lapply (yle_inv_succ … H) -H #Hl1 >yminus_succ #Hml1 normalize + yminus_inj >yminus_inj yplus_SO2 >yplus_SO2 >yminus_succ + /4 width=1 by yle_inv_succ, eq_f/ ] qed-. @@ -461,8 +485,8 @@ fact drop_inv_FT_aux: ∀L1,L2,s,l,m. ⬇[s, l, m] L1 ≡ L2 → | #I #L #V #J #K #W #H destruct // | #I #L1 #L2 #V #m #_ #IHL12 #J #K #W #H1 #H2 destruct /3 width=1 by drop_drop/ -| #I #L1 #L2 #V1 #V2 #l #m #_ #_ #_ #J #K #W #_ #_ - commutative_plus normalize #H destruct +[ lapply (le_n_O_to_eq … H1m) -H1m -IHL2 minus_minus_comm /3 width=1 by monotonic_pred/ ] qed-. -lemma drop_O1_inv_append1_le: ∀K,L1,L2,s,m. ⬇[s, 0, m] L1 @@ L2 ≡ K → m ≤ |L2| → - ∀K2. ⬇[s, 0, m] L2 ≡ K2 → K = L1 @@ K2. +lemma drop_O1_inv_append1_le: ∀K,L1,L2,s,m. ⬇[s, yinj 0, m] L1 @@ L2 ≡ K → m ≤ |L2| → + ∀K2. ⬇[s, yinj 0, m] L2 ≡ K2 → K = L1 @@ K2. #K #L1 #L2 elim L2 -L2 normalize [ #s #m #H1 #H2 #K2 #H3 lapply (le_n_O_to_eq … H2) -H2 #H2 elim (drop_inv_atom1 … H3) -H3 #H3 #_ destruct diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/drop_drop.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/drop_drop.ma index 83b347d39..ea8cadb13 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/substitution/drop_drop.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/drop_drop.ma @@ -28,7 +28,7 @@ theorem drop_mono: ∀L,L1,s1,l,m. ⬇[s1, l, m] L ≡ L1 → | #I #L #K #V #m #_ #IHLK #L2 #s2 #H lapply (drop_inv_drop1 … H) -H /2 width=2 by/ | #I #L #K1 #T #V1 #l #m #_ #HVT1 #IHLK1 #X #s2 #H - elim (drop_inv_skip1 … H) -H // ypred_succ #K2 #V2 #HLK2 #HVT2 #H destruct >(lift_inj … HVT1 … HVT2) -HVT1 -HVT2 >(IHLK1 … HLK2) -IHLK1 -HLK2 // ] @@ -42,21 +42,25 @@ theorem drop_conf_ge: ∀L,L1,s1,l1,m1. ⬇[s1, l1, m1] L ≡ L1 → [ #l #m #_ #L2 #s2 #m2 #H #_ elim (drop_inv_atom1 … H) -H #H #Hm destruct @drop_atom #H >Hm // (**) (* explicit constructor *) -| #I #L #K #V #m #_ #IHLK #L2 #s2 #m2 #H #Hm2 - lapply (drop_inv_drop1_lt … H ?) -H /2 width=2 by ltn_to_ltO/ #HL2 - minus_minus_comm /3 width=1 by monotonic_pred/ +| #I #L #K #V #m #_ #IHLK #L2 #s2 #m2 #H >yplus_O1 minus_minus_comm @IHLK // | #I #L #K #V1 #V2 #l #m #_ #_ #IHLK #L2 #s2 #m2 #H #Hlmm2 - lapply (transitive_le 1 … Hlmm2) // #Hm2 - lapply (drop_inv_drop1_lt … H ?) -H // -Hm2 #HL2 - lapply (transitive_le (1+m) … Hlmm2) // #Hmm2 - @drop_drop_lt >minus_minus_comm /3 width=1 by lt_minus_to_plus_r, monotonic_le_minus_r, monotonic_pred/ (**) (* explicit constructor *) + lapply (yle_plus1_to_minus_inj2 … Hlmm2) #Hlm2m + lapply (ylt_yle_trans 0 … Hlm2m ?) // -Hlm2m #Hm2m + >yplus_succ1 in Hlmm2; #Hlmm2 + elim (yle_inv_succ1 … Hlmm2) -Hlmm2 #Hlmm2 #Hm2 + lapply (drop_inv_drop1_lt … H ?) -H /2 width=1 by ylt_inv_inj/ -Hm2 #HL2 + @drop_drop_lt /2 width=1 by ylt_inv_inj/ >minus_minus_comm + (Hm2 ?) in Hl1; // -Hm2 #Hl1 <(le_n_O_to_eq … Hl1) -l1 @@ -77,7 +81,7 @@ theorem drop_conf_be: ∀L0,L1,s1,l1,m1. ⬇[s1, l1, m1] L0 ≡ L1 → elim (IHLK0 … HL02) -L0 /3 width=3 by drop_drop, monotonic_pred, ex2_intro/ ] qed-. - +*) (* Note: apparently this was missing in basic_1 *) theorem drop_conf_le: ∀L0,L1,s1,l1,m1. ⬇[s1, l1, m1] L0 ≡ L1 → ∀L2,s2,m2. ⬇[s2, 0, m2] L0 ≡ L2 → m2 ≤ l1 → @@ -86,17 +90,19 @@ theorem drop_conf_le: ∀L0,L1,s1,l1,m1. ⬇[s1, l1, m1] L0 ≡ L1 → [ #l1 #m1 #Hm1 #L2 #s2 #m2 #H elim (drop_inv_atom1 … H) -H #H #Hm2 #_ destruct /4 width=3 by drop_atom, ex2_intro/ | #I #K0 #V0 #L2 #s2 #m2 #H1 #H2 - lapply (le_n_O_to_eq … H2) -H2 #H destruct + lapply (yle_inv_O2 … H2) -H2 #H destruct lapply (drop_inv_pair1 … H1) -H1 #H destruct /2 width=3 by drop_pair, ex2_intro/ | #I #K0 #K1 #V0 #m1 #HK01 #_ #L2 #s2 #m2 #H1 #H2 - lapply (le_n_O_to_eq … H2) -H2 #H destruct + lapply (yle_inv_O2 … H2) -H2 #H destruct lapply (drop_inv_pair1 … H1) -H1 #H destruct /3 width=3 by drop_drop, ex2_intro/ | #I #K0 #K1 #V0 #V1 #l1 #m1 #HK01 #HV10 #IHK01 #L2 #s2 #m2 #H #Hm2l1 elim (drop_inv_O1_pair1 … H) -H * [ -IHK01 -Hm2l1 #H1 #H2 destruct /3 width=5 by drop_pair, drop_skip, ex2_intro/ | -HK01 -HV10 #Hm2 #HK0L2 - elim (IHK01 … HK0L2) -IHK01 -HK0L2 /2 width=1 by monotonic_pred/ - >minus_le_minus_minus_comm /3 width=3 by drop_drop_lt, ex2_intro/ + lapply (yle_inv_succ2 … Hm2l1) -Hm2l1 yplus_minus_assoc_comm_inj /2 width=1 by yle_inj/ + >yplus_SO2 /3 width=3 by drop_drop_lt, ex2_intro/ ] ] qed-. @@ -111,10 +117,11 @@ theorem drop_trans_ge: ∀L1,L,s1,l1,m1. ⬇[s1, l1, m1] L1 ≡ L → | /2 width=1 by drop_gen/ | /3 width=1 by drop_drop/ | #I #L1 #L2 #V1 #V2 #l #m #_ #_ #IHL12 #L #m2 #H #Hlm2 - lapply (lt_to_le_to_lt 0 … Hlm2) // #Hm2 + elim (yle_inv_succ1 … Hlm2) -Hlm2 #Hlm2 #Hm2 + lapply (ylt_O … Hm2) -Hm2 #Hm2 lapply (lt_to_le_to_lt … (m + m2) Hm2 ?) // #Hmm2 lapply (drop_inv_drop1_lt … H ?) -H // #HL2 - @drop_drop_lt // >le_plus_minus /3 width=1 by monotonic_pred/ + @drop_drop_lt // >le_plus_minus minus_le_minus_minus_comm // /3 width=3 by drop_drop_lt, ex2_intro/ | /2 width=1 by monotonic_pred/ ] + lapply (yle_inv_succ2 … Hm2l) -Hm2l yplus_minus_assoc_comm_inj /3 width=3 by drop_drop_lt, yle_inj, ex2_intro/ ] ] qed-. @@ -154,12 +163,12 @@ qed-. (* Basic_1: was: drop_conf_lt *) lemma drop_conf_lt: ∀L,L1,s1,l1,m1. ⬇[s1, l1, m1] L ≡ L1 → ∀I,K2,V2,s2,m2. ⬇[s2, 0, m2] L ≡ K2.ⓑ{I}V2 → - m2 < l1 → let l ≝ l1 - m2 - 1 in + m2 < l1 → let l ≝ ⫰(l1 - m2) in ∃∃K1,V1. ⬇[s2, 0, m2] L1 ≡ K1.ⓑ{I}V1 & ⬇[s1, l, m1] K2 ≡ K1 & ⬆[l, m1] V1 ≡ V2. #L #L1 #s1 #l1 #m1 #H1 #I #K2 #V2 #s2 #m2 #H2 #Hm2l1 -elim (drop_conf_le … H1 … H2) -L /2 width=2 by lt_to_le/ #K #HL1K #HK2 -elim (drop_inv_skip1 … HK2) -HK2 /2 width=1 by lt_plus_to_minus_r/ +elim (drop_conf_le … H1 … H2) -L /2 width=2 by ylt_fwd_le/ #K #HL1K #HK2 +elim (drop_inv_skip1 … HK2) -HK2 /2 width=1 by ylt_to_minus/ #K1 #V1 #HK21 #HV12 #H destruct /2 width=5 by ex3_2_intro/ qed-. @@ -170,8 +179,9 @@ lemma drop_trans_lt: ∀L1,L,s1,l1,m1. ⬇[s1, l1, m1] L1 ≡ L → ∃∃L0,V0. ⬇[s2, 0, m2] L1 ≡ L0.ⓑ{I}V0 & ⬇[s1, l, m1] L0 ≡ L2 & ⬆[l, m1] V2 ≡ V0. #L1 #L #s1 #l1 #m1 #HL1 #I #L2 #V2 #s2 #m2 #HL2 #Hl21 -elim (drop_trans_le … HL1 … HL2) -L /2 width=1 by lt_to_le/ #L0 #HL10 #HL02 -elim (drop_inv_skip2 … HL02) -HL02 /2 width=1 by lt_plus_to_minus_r/ #L #V1 #HL2 #HV21 #H destruct /2 width=5 by ex3_2_intro/ +elim (drop_trans_le … HL1 … HL2) -L /2 width=1 by ylt_fwd_le/ #L0 #HL10 #HL02 +elim (drop_inv_skip2 … HL02) -HL02 /2 width=1 by ylt_to_minus/ +#L #V1 #HL2 #HV21 #H destruct /2 width=5 by ex3_2_intro/ qed-. lemma drop_trans_ge_comm: ∀L1,L,L2,s1,l1,m1,m2. @@ -188,7 +198,7 @@ lemma drop_conf_div: ∀I1,L,K,V1,m1. ⬇[m1] L ≡ K.ⓑ{I1}V1 → elim (le_or_ge m1 m2) #Hm [ lapply (drop_conf_ge … HLK1 … HLK2 ?) | lapply (drop_conf_ge … HLK2 … HLK1 ?) -] -HLK1 -HLK2 // #HK +] -HLK1 -HLK2 /2 width=1 by yle_inj/ #HK lapply (drop_fwd_length_minus2 … HK) #H elim (discr_minus_x_xy … H) -H [1,3: normalize ypred_succ /2 width=3 by drop_pair, ex2_intro/ | lapply (ylt_inv_O1 i ?) /2 width=1 by ylt_inj/ - #H yminus_succ (plus_minus_m_m i m) in ⊢ (? ? ? ? %); /3 width=2 by lift_lref_ge, le_plus_to_minus_r, le_plus_b/ +lemma lift_lref_ge_minus: ∀l,m,i. l + yinj m ≤ yinj i → ⬆[l, m] #(i - m) ≡ #i. +#l #m #i #H >(plus_minus_m_m i m) in ⊢ (? ? ? ? %); +elim (yle_inv_plus_inj2 … H) -H #Hlim #H +lapply (yle_inv_inj … H) -H /2 width=1 by lift_lref_ge/ qed. -lemma lift_lref_ge_minus_eq: ∀l,m,i,j. l + m ≤ i → j = i - m → ⬆[l, m] #j ≡ #i. +lemma lift_lref_ge_minus_eq: ∀l,m,i,j. l + yinj m ≤ yinj i → j = i - m → ⬆[l, m] #j ≡ #i. /2 width=1 by lift_lref_ge_minus/ qed-. (* Basic_1: was: lift_r *) lemma lift_refl: ∀T,l. ⬆[l, 0] T ≡ T. #T elim T -T -[ * #i // #l elim (lt_or_ge i l) /2 width=1 by lift_lref_lt, lift_lref_ge/ +[ * #i // #l elim (ylt_split i l) /2 width=1 by lift_lref_lt, lift_lref_ge/ | * /2 width=1 by lift_bind, lift_flat/ ] qed. -lemma lift_total: ∀T1,l,m. ∃T2. ⬆[l,m] T1 ≡ T2. +(* Basic_2b: first lemma *) +lemma lift_Y1: ∀T,m. ⬆[∞, m] T ≡ T. +#T elim T -T * /2 width=1 by lift_lref_lt, lift_bind, lift_flat/ +qed. + +lemma lift_total: ∀T1,l,m. ∃T2. ⬆[l, m] T1 ≡ T2. #T1 elim T1 -T1 [ * #i /2 width=2 by lift_sort, lift_gref, ex_intro/ - #l #m elim (lt_or_ge i l) /3 width=2 by lift_lref_lt, lift_lref_ge, ex_intro/ + #l #m elim (ylt_split i l) /3 width=2 by lift_lref_lt, lift_lref_ge, ex_intro/ | * [ #a ] #I #V1 #T1 #IHV1 #IHT1 #l #m elim (IHV1 l m) -IHV1 #V2 #HV12 - [ elim (IHT1 (l+1) m) -IHT1 /3 width=2 by lift_bind, ex_intro/ + [ elim (IHT1 (⫯l) m) -IHT1 /3 width=2 by lift_bind, ex_intro/ | elim (IHT1 l m) -IHT1 /3 width=2 by lift_flat, ex_intro/ ] ] @@ -333,19 +348,19 @@ qed. (* Basic_1: was: lift_free (right to left) *) lemma lift_split: ∀l1,m2,T1,T2. ⬆[l1, m2] T1 ≡ T2 → - ∀l2,m1. l1 ≤ l2 → l2 ≤ l1 + m1 → m1 ≤ m2 → + ∀l2,m1. l1 ≤ l2 → l2 ≤ l1 + yinj m1 → m1 ≤ m2 → ∃∃T. ⬆[l1, m1] T1 ≡ T & ⬆[l2, m2 - m1] T ≡ T2. #l1 #m2 #T1 #T2 #H elim H -l1 -m2 -T1 -T2 [ /3 width=3 by lift_sort, ex2_intro/ | #i #l1 #m2 #Hil1 #l2 #m1 #Hl12 #_ #_ - lapply (lt_to_le_to_lt … Hil1 Hl12) -Hl12 #Hil2 /4 width=3 by lift_lref_lt, ex2_intro/ + lapply (ylt_yle_trans … Hl12 Hil1) -Hl12 #Hil2 /4 width=3 by lift_lref_lt, ex2_intro/ | #i #l1 #m2 #Hil1 #l2 #m1 #_ #Hl21 #Hm12 - lapply (transitive_le … (i+m1) Hl21 ?) /2 width=1 by monotonic_le_plus_l/ -Hl21 #Hl21 + lapply (yle_trans … Hl21 (i+m1) ?) /2 width=1 by monotonic_yle_plus_dx/ -Hl21 #Hl21 >(plus_minus_m_m m2 m1 ?) /3 width=3 by lift_lref_ge, ex2_intro/ | /3 width=3 by lift_gref, ex2_intro/ | #a #I #V1 #V2 #T1 #T2 #l1 #m2 #_ #_ #IHV #IHT #l2 #m1 #Hl12 #Hl21 #Hm12 elim (IHV … Hl12 Hl21 Hm12) -IHV #V0 #HV0a #HV0b - elim (IHT (l2+1) … ? ? Hm12) /3 width=5 by lift_bind, le_S_S, ex2_intro/ + elim (IHT (⫯l2) … ? ? Hm12) /3 width=5 by lift_bind, yle_succ, ex2_intro/ | #I #V1 #V2 #T1 #T2 #l1 #m2 #_ #_ #IHV #IHT #l2 #m1 #Hl12 #Hl21 #Hm12 elim (IHV … Hl12 Hl21 Hm12) -IHV #V0 #HV0a #HV0b elim (IHT l2 … ? ? Hm12) /3 width=5 by lift_flat, ex2_intro/ @@ -353,19 +368,19 @@ lemma lift_split: ∀l1,m2,T1,T2. ⬆[l1, m2] T1 ≡ T2 → qed. (* Basic_1: was only: dnf_dec2 dnf_dec *) -lemma is_lift_dec: ∀T2,l,m. Decidable (∃T1. ⬆[l,m] T1 ≡ T2). +lemma is_lift_dec: ∀T2,l,m. Decidable (∃T1. ⬆[l, m] T1 ≡ T2). #T1 elim T1 -T1 [ * [1,3: /3 width=2 by lift_sort, lift_gref, ex_intro, or_introl/ ] #i #l #m - elim (lt_or_ge i l) #Hli + elim (ylt_split i l) #Hli [ /4 width=3 by lift_lref_lt, ex_intro, or_introl/ - | elim (lt_or_ge i (l + m)) #Hilm + | elim (ylt_split i (l + m)) #Hilm [ @or_intror * #T1 #H elim (lift_inv_lref2_be … H Hli Hilm) | -Hli /4 width=2 by lift_lref_ge_minus, ex_intro, or_introl/ ] ] | * [ #a ] #I #V2 #T2 #IHV2 #IHT2 #l #m [ elim (IHV2 l m) -IHV2 - [ * #V1 #HV12 elim (IHT2 (l+1) m) -IHT2 + [ * #V1 #HV12 elim (IHT2 (⫯l) m) -IHT2 [ * #T1 #HT12 @or_introl /3 width=2 by lift_bind, ex_intro/ | -V1 #HT2 @or_intror * #X #H elim (lift_inv_bind2 … H) -H /3 width=2 by ex_intro/ diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/lift_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/lift_lift.ma index 9ab57806f..70ec68826 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/substitution/lift_lift.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/lift_lift.ma @@ -19,14 +19,14 @@ include "basic_2/substitution/lift.ma". (* Main properties ***********************************************************) (* Basic_1: was: lift_inj *) -theorem lift_inj: ∀l,m,T1,U. ⬆[l,m] T1 ≡ U → ∀T2. ⬆[l,m] T2 ≡ U → T1 = T2. +theorem lift_inj: ∀l,m,T1,U. ⬆[l, m] T1 ≡ U → ∀T2. ⬆[l, m] T2 ≡ U → T1 = T2. #l #m #T1 #U #H elim H -l -m -T1 -U [ #k #l #m #X #HX lapply (lift_inv_sort2 … HX) -HX // | #i #l #m #Hil #X #HX lapply (lift_inv_lref2_lt … HX ?) -HX // | #i #l #m #Hli #X #HX - lapply (lift_inv_lref2_ge … HX ?) -HX /2 width=1 by monotonic_le_plus_l/ + lapply (lift_inv_lref2_ge … HX ?) -HX /2 width=1 by monotonic_yle_plus_dx/ | #p #l #m #X #HX lapply (lift_inv_gref2 … HX) -HX // | #a #I #V1 #V2 #T1 #T2 #l #m #_ #_ #IHV12 #IHT12 #X #HX @@ -45,23 +45,24 @@ theorem lift_div_le: ∀l1,m1,T1,T. ⬆[l1, m1] T1 ≡ T → [ #k #l1 #m1 #l2 #m2 #T2 #Hk #Hl12 lapply (lift_inv_sort2 … Hk) -Hk #Hk destruct /3 width=3 by lift_sort, ex2_intro/ | #i #l1 #m1 #Hil1 #l2 #m2 #T2 #Hi #Hl12 - lapply (lt_to_le_to_lt … Hil1 Hl12) -Hl12 #Hil2 - lapply (lift_inv_lref2_lt … Hi ?) -Hi /3 width=3 by lift_lref_lt, lt_plus_to_minus_r, lt_to_le_to_lt, ex2_intro/ + lapply (ylt_yle_trans … Hl12 Hil1) -Hl12 #Hil2 + lapply (lift_inv_lref2_lt … Hi ?) -Hi /3 width=3 by lift_lref_lt, ylt_plus_dx1_trans, ex2_intro/ | #i #l1 #m1 #Hil1 #l2 #m2 #T2 #Hi #Hl12 - elim (lift_inv_lref2 … Hi) -Hi * #Hil2 #H destruct - [ -Hl12 lapply (lt_plus_to_lt_l … Hil2) -Hil2 #Hil2 /3 width=3 by lift_lref_lt, lift_lref_ge, ex2_intro/ - | -Hil1 >plus_plus_comm_23 in Hil2; #H lapply (le_plus_to_le_r … H) -H #H - elim (le_inv_plus_l … H) -H #Hilm2 #Hm2i - lapply (transitive_le … Hl12 Hilm2) -Hl12 #Hl12 + elim (lift_inv_lref2 … Hi) -Hi * yplus_comm_23 in Hil2; #H lapply ( yle_inv_monotonic_plus_dx … H) -H #H + elim (yle_inv_plus_inj2 … H) -H >yminus_inj #Hl2im2 #H + lapply (yle_inv_inj … H) -H #Hm2i + lapply (yle_trans … Hl12 … Hl2im2) -Hl12 #Hl1im2 >le_plus_minus_comm // >(plus_minus_m_m i m2) in ⊢ (? ? ? %); - /4 width=3 by lift_lref_ge, ex2_intro/ + /3 width=3 by lift_lref_ge, ex2_intro/ ] | #p #l1 #m1 #l2 #m2 #T2 #Hk #Hl12 lapply (lift_inv_gref2 … Hk) -Hk #Hk destruct /3 width=3 by lift_gref, ex2_intro/ | #a #I #W1 #W #U1 #U #l1 #m1 #_ #_ #IHW #IHU #l2 #m2 #T2 #H #Hl12 lapply (lift_inv_bind2 … H) -H * #W2 #U2 #HW2 #HU2 #H destruct elim (IHW … HW2) // -IHW -HW2 #W0 #HW2 #HW1 - >plus_plus_comm_23 in HU2; #HU2 elim (IHU … HU2) /3 width=5 by lift_bind, le_S_S, ex2_intro/ + (lift_inv_sort2 … H) -H /2 width=3 by lift_sort, ex2_intro/ | #i #l1 #m1 #Hil1 #m #m2 #T2 #H #Hm1 #Hm1m2 - >(lift_inv_lref2_lt … H) -H /3 width=3 by lift_lref_lt, lt_plus_to_minus_r, lt_to_le_to_lt, ex2_intro/ + >(lift_inv_lref2_lt … H) -H /3 width=3 by ylt_plus_dx1_trans, lift_lref_lt, ex2_intro/ | #i #l1 #m1 #Hil1 #m #m2 #T2 #H #Hm1 #Hm1m2 - elim (lt_or_ge (i+m1) (l1+m+m2)) #Him1l1m2 - [ elim (lift_inv_lref2_be … H) -H /2 width=1 by le_plus/ + elim (ylt_split (i+m1) (l1+m+m2)) #H0 + [ elim (lift_inv_lref2_be … H) -H /3 width=2 by monotonic_yle_plus, yle_inj/ | >(lift_inv_lref2_ge … H ?) -H // - lapply (le_plus_to_minus … Him1l1m2) #Hl1m21i - elim (le_inv_plus_l … Him1l1m2) -Him1l1m2 #Hl1m12 #Hm2im1 - @ex2_intro [2: /2 width=1 by lift_lref_ge_minus/ | skip ] -Hl1m12 - @lift_lref_ge_minus_eq [ >plus_minus_associative // | /2 width=1 by minus_le_minus_minus_comm/ ] + lapply (yle_plus2_to_minus_inj2 … H0) #Hl1m21i + elim (yle_inv_plus_inj2 … H0) -H0 #Hl1m12 #Hm2im1 + @ex2_intro [2: /2 width=1 by lift_lref_ge_minus/ | skip ] + @lift_lref_ge_minus_eq + [ yplus_minus_assoc_inj /2 width=1 by yle_inj/ + | /2 width=1 by minus_le_minus_minus_comm/ + ] ] | #p #l1 #m1 #m #m2 #T2 #H >(lift_inv_gref2 … H) -H /2 width=3 by lift_gref, ex2_intro/ | #a #I #V1 #V #T1 #T #l1 #m1 #_ #_ #IHV1 #IHT1 #m #m2 #X #H #Hm1 #Hm1m2 - elim (lift_inv_bind2 … H) -H #V2 #T2 #HV2 #HT2 #H destruct - elim (IHV1 … HV2) -V // >plus_plus_comm_23 in HT2; #HT2 + elim (lift_inv_bind2 … H) -H #V2 #T2 #HV2 (lift_inv_sort1 … HT2) -HT2 // | #i #l1 #m1 #Hil1 #l2 #m2 #T2 #HT2 #Hl12 #_ - lapply (lt_to_le_to_lt … Hil1 Hl12) -Hl12 #Hil2 + lapply (ylt_yle_trans … Hl12 Hil1) -Hl12 #Hil2 lapply (lift_inv_lref1_lt … HT2 Hil2) /2 width=1 by lift_lref_lt/ | #i #l1 #m1 #Hil1 #l2 #m2 #T2 #HT2 #_ #Hl21 lapply (lift_inv_lref1_ge … HT2 ?) -HT2 - [ @(transitive_le … Hl21 ?) -Hl21 /2 width=1 by monotonic_le_plus_l/ + [ @(yle_trans … Hl21) -Hl21 /2 width=1 by monotonic_yle_plus_dx/ | -Hl21 /2 width=1 by lift_lref_ge/ ] | #p #l1 #m1 #l2 #m2 #T2 #HT2 #_ #_ >(lift_inv_gref1 … HT2) -HT2 // | #a #I #V1 #V2 #T1 #T2 #l1 #m1 #_ #_ #IHV12 #IHT12 #l2 #m2 #X #HX #Hl12 #Hl21 - elim (lift_inv_bind1 … HX) -HX #V0 #T0 #HV20 #HT20 #HX destruct + elim (lift_inv_bind1 … HX) -HX #V0 #T0 #HV20 #HT20 #HX destruct lapply (IHV12 … HV20 ? ?) // -IHV12 -HV20 #HV10 - lapply (IHT12 … HT20 ? ?) /2 width=1 by lift_bind, le_S_S/ (**) (* full auto a bit slow *) + lapply (IHT12 … HT20 ? ?) /2 width=1 by lift_bind, yle_succ/ (**) (* full auto a bit slow *) | #I #V1 #V2 #T1 #T2 #l1 #m1 #_ #_ #IHV12 #IHT12 #l2 #m2 #X #HX #Hl12 #Hl21 elim (lift_inv_flat1 … HX) -HX #V0 #T0 #HV20 #HT20 #HX destruct lapply (IHV12 … HV20 ? ?) // -IHV12 -HV20 #HV10 @@ -152,18 +156,19 @@ theorem lift_trans_le: ∀l1,m1,T1,T. ⬆[l1, m1] T1 ≡ T → [ #k #l1 #m1 #l2 #m2 #X #HX #_ >(lift_inv_sort1 … HX) -HX /2 width=3 by lift_sort, ex2_intro/ | #i #l1 #m1 #Hil1 #l2 #m2 #X #HX #_ - lapply (lt_to_le_to_lt … (l1+m2) Hil1 ?) // #Him2 - elim (lift_inv_lref1 … HX) -HX * #Hil2 #HX destruct /4 width=3 by lift_lref_ge_minus, lift_lref_lt, lt_minus_to_plus, monotonic_le_plus_l, ex2_intro/ + lapply (ylt_yle_trans … (l1+m2) ? Hil1) // #Him2 + elim (lift_inv_lref1 … HX) -HX * #Hil2 #HX destruct + /4 width=3 by monotonic_ylt_plus_dx, monotonic_yle_plus_dx, lift_lref_ge_minus, lift_lref_lt, ex2_intro/ | #i #l1 #m1 #Hil1 #l2 #m2 #X #HX #Hl21 - lapply (transitive_le … Hl21 Hil1) -Hl21 #Hil2 - lapply (lift_inv_lref1_ge … HX ?) -HX /2 width=3 by transitive_le/ #HX destruct - >plus_plus_comm_23 /4 width=3 by lift_lref_ge_minus, lift_lref_ge, monotonic_le_plus_l, ex2_intro/ + lapply (yle_trans … Hl21 … Hil1) -Hl21 #Hil2 + lapply (lift_inv_lref1_ge … HX ?) -HX /2 width=3 by yle_plus_dx1_trans/ #HX destruct + >plus_plus_comm_23 /4 width=3 by monotonic_yle_plus_dx, lift_lref_ge_minus, lift_lref_ge, ex2_intro/ | #p #l1 #m1 #l2 #m2 #X #HX #_ >(lift_inv_gref1 … HX) -HX /2 width=3 by lift_gref, ex2_intro/ | #a #I #V1 #V2 #T1 #T2 #l1 #m1 #_ #_ #IHV12 #IHT12 #l2 #m2 #X #HX #Hl21 elim (lift_inv_bind1 … HX) -HX #V0 #T0 #HV20 #HT20 #HX destruct elim (IHV12 … HV20) -IHV12 -HV20 // - elim (IHT12 … HT20) -IHT12 -HT20 /3 width=5 by lift_bind, le_S_S, ex2_intro/ + elim (IHT12 … HT20) -IHT12 -HT20 /3 width=5 by lift_bind, yle_succ, ex2_intro/ | #I #V1 #V2 #T1 #T2 #l1 #m1 #_ #_ #IHV12 #IHT12 #l2 #m2 #X #HX #Hl21 elim (lift_inv_flat1 … HX) -HX #V0 #T0 #HV20 #HT20 #HX destruct elim (IHV12 … HV20) -IHV12 -HV20 // @@ -179,19 +184,23 @@ theorem lift_trans_ge: ∀l1,m1,T1,T. ⬆[l1, m1] T1 ≡ T → [ #k #l1 #m1 #l2 #m2 #X #HX #_ >(lift_inv_sort1 … HX) -HX /2 width=3 by lift_sort, ex2_intro/ | #i #l1 #m1 #Hil1 #l2 #m2 #X #HX #Hlml - lapply (lt_to_le_to_lt … (l1+m1) Hil1 ?) // #Hil1m - lapply (lt_to_le_to_lt … (l2-m1) Hil1 ?) /2 width=1 by le_plus_to_minus_r/ #Hil2m - lapply (lt_to_le_to_lt … Hil1m Hlml) -Hil1m -Hlml #Hil2 + lapply (ylt_yle_trans … (l1+m1) ? Hil1) // #Hil1m + lapply (ylt_yle_trans … (l2-m1) ? Hil1) /2 width=1 by yle_plus1_to_minus_inj2/ #Hil2m + lapply (ylt_yle_trans … Hlml Hil1m) -Hil1m -Hlml #Hil2 lapply (lift_inv_lref1_lt … HX ?) -HX // #HX destruct /3 width=3 by lift_lref_lt, ex2_intro/ | #i #l1 #m1 #Hil1 #l2 #m2 #X #HX #_ - elim (lift_inv_lref1 … HX) -HX * #Himl #HX destruct /4 width=3 by lift_lref_lt, lift_lref_ge, monotonic_le_minus_l, lt_plus_to_minus_r, transitive_le, ex2_intro/ + elim (lift_inv_lref1 … HX) -HX * (lift_inv_gref1 … HX) -HX /2 width=3 by lift_gref, ex2_intro/ | #a #I #V1 #V2 #T1 #T2 #l1 #m1 #_ #_ #IHV12 #IHT12 #l2 #m2 #X #HX #Hlml + elim (yle_inv_plus_inj2 … Hlml) #Hlm #Hml elim (lift_inv_bind1 … HX) -HX #V0 #T0 #HV20 #HT20 #HX destruct elim (IHV12 … HV20) -IHV12 -HV20 // - elim (IHT12 … HT20) -IHT12 -HT20 /2 width=1 by le_S_S/ #T - yminus_succ1_inj /3 width=5 by lift_bind, ex2_intro/ | #I #V1 #V2 #T1 #T2 #l1 #m1 #_ #_ #IHV12 #IHT12 #l2 #m2 #X #HX #Hlml elim (lift_inv_flat1 … HX) -HX #V0 #T0 #HV20 #HT20 #HX destruct elim (IHV12 … HV20) -IHV12 -HV20 // @@ -210,7 +219,7 @@ lapply (lift_mono … HTX … HT2) -T #H destruct /2 width=3 by ex2_intro/ qed. lemma lift_conf_be: ∀T,T1,l,m1. ⬆[l, m1] T ≡ T1 → ∀T2,m2. ⬆[l, m2] T ≡ T2 → - m1 ≤ m2 → ⬆[l + m1, m2 - m1] T1 ≡ T2. + m1 ≤ m2 → ⬆[l + yinj m1, m2 - m1] T1 ≡ T2. #T #T1 #l #m1 #HT1 #T2 #m2 #HT2 #Hm12 elim (lift_split … HT2 (l+m1) m1) -HT2 // #X #H >(lift_mono … H … HT1) -T // diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/lift_neg.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/lift_neg.ma index 434ad02e4..6c797befb 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/substitution/lift_neg.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/lift_neg.ma @@ -18,15 +18,15 @@ include "basic_2/substitution/lift.ma". (* Properties on negated basic relocation ***********************************) -lemma nlift_lref_be_SO: ∀X,i. ⬆[i, 1] X ≡ #i → ⊥. -/2 width=7 by lift_inv_lref2_be/ qed-. +lemma nlift_lref_be_SO: ∀X,i. ⬆[yinj i, 1] X ≡ #i → ⊥. +/3 width=7 by lift_inv_lref2_be, ylt_inj/ qed-. lemma nlift_bind_sn: ∀W,l,m. (∀V. ⬆[l, m] V ≡ W → ⊥) → ∀a,I,U. (∀X. ⬆[l, m] X ≡ ⓑ{a,I}W.U → ⊥). #W #l #m #HW #a #I #U #X #H elim (lift_inv_bind2 … H) -H /2 width=2 by/ qed-. -lemma nlift_bind_dx: ∀U,l,m. (∀T. ⬆[l+1, m] T ≡ U → ⊥) → +lemma nlift_bind_dx: ∀U,l,m. (∀T. ⬆[⫯l, m] T ≡ U → ⊥) → ∀a,I,W. (∀X. ⬆[l, m] X ≡ ⓑ{a,I}W.U → ⊥). #U #l #m #HU #a #I #W #X #H elim (lift_inv_bind2 … H) -H /2 width=2 by/ qed-. @@ -43,15 +43,16 @@ qed-. (* Inversion lemmas on negated basic relocation *****************************) -lemma nlift_inv_lref_be_SO: ∀i,j. (∀X. ⬆[i, 1] X ≡ #j → ⊥) → j = i. +lemma nlift_inv_lref_be_SO: ∀i,j. (∀X. ⬆[i, 1] X ≡ #j → ⊥) → yinj j = i. +* [2: #j #H elim H -H // ] #i #j elim (lt_or_eq_or_gt i j) // #Hij #H -[ elim (H (#(j-1))) -H /2 width=1 by lift_lref_ge_minus/ -| elim (H (#j)) -H /2 width=1 by lift_lref_lt/ +[ elim (H (#(j-1))) -H /3 width=1 by lift_lref_ge_minus, yle_inj/ +| elim (H (#j)) -H /3 width=1 by lift_lref_lt, ylt_inj/ ] qed-. lemma nlift_inv_bind: ∀a,I,W,U,l,m. (∀X. ⬆[l, m] X ≡ ⓑ{a,I}W.U → ⊥) → - (∀V. ⬆[l, m] V ≡ W → ⊥) ∨ (∀T. ⬆[l+1, m] T ≡ U → ⊥). + (∀V. ⬆[l, m] V ≡ W → ⊥) ∨ (∀T. ⬆[⫯l, m] T ≡ U → ⊥). #a #I #W #U #l #m #H elim (is_lift_dec W l m) [ * /4 width=2 by lift_bind, or_intror/ | /4 width=2 by ex_intro, or_introl/ diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/lift_vector.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/lift_vector.ma index 42cef005b..6876229e4 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/substitution/lift_vector.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/lift_vector.ma @@ -17,7 +17,7 @@ include "basic_2/substitution/lift.ma". (* BASIC TERM VECTOR RELOCATION *********************************************) -inductive liftv (l,m:nat) : relation (list term) ≝ +inductive liftv (l) (m): relation (list term) ≝ | liftv_nil : liftv l m (◊) (◊) | liftv_cons: ∀T1s,T2s,T1,T2. ⬆[l, m] T1 ≡ T2 → liftv l m T1s T2s → diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/lpx_sn_drop.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/lpx_sn_drop.ma index 3b7b6ebab..6eb2dd8b2 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/substitution/lpx_sn_drop.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/lpx_sn_drop.ma @@ -87,7 +87,7 @@ qed-. fact lpx_sn_dropable_aux: ∀R,L2,K2,s,l,m. ⬇[s, l, m] L2 ≡ K2 → ∀L1. lpx_sn R L1 L2 → l = 0 → ∃∃K1. ⬇[s, 0, m] L1 ≡ K1 & lpx_sn R K1 K2. #R #L2 #K2 #s #l #m #H elim H -L2 -K2 -l -m -[ #l #m #Hm #X #H >(lpx_sn_inv_atom2 … H) -H +[ #l #m #Hm #X #H >(lpx_sn_inv_atom2 … H) -H /4 width=3 by drop_atom, lpx_sn_atom, ex2_intro/ | #I #K2 #V2 #X #H elim (lpx_sn_inv_pair2 … H) -H #K1 #V1 #HK12 #HV12 #H destruct @@ -95,8 +95,7 @@ fact lpx_sn_dropable_aux: ∀R,L2,K2,s,l,m. ⬇[s, l, m] L2 ≡ K2 → ∀L1. lp | #I #L2 #K2 #V2 #m #_ #IHLK2 #X #H #_ elim (lpx_sn_inv_pair2 … H) -H #L1 #V1 #HL12 #HV12 #H destruct elim (IHLK2 … HL12) -L2 /3 width=3 by drop_drop, ex2_intro/ -| #I #L2 #K2 #V2 #W2 #l #m #_ #_ #_ #L1 #_ - yminus_succ (lift_inv_sort1 … H2) -X2 // | #G #L1 #K1 #V1 #W1 #W #i #d #HLK1 #_ #HW1 #IHVW1 #L2 #s #l #m #HL21 #X #H #U2 #HWU2 elim (lift_inv_lref1 … H) * #Hil #H destruct - [ elim (lift_trans_ge … HW1 … HWU2) -W // #W2 #HW12 #HWU2 - elim (drop_trans_le … HL21 … HLK1) -L1 /2 width=2 by lt_to_le/ #X #HLK2 #H - elim (drop_inv_skip2 … H) -H /2 width=1 by lt_plus_to_minus_r/ -Hil #K2 #V2 #HK21 #HV12 #H destruct + [ elim (lift_trans_ge … HW1 … HWU2) -W /2 width=1 by ylt_fwd_le_succ1/ #W2 #HW12 #HWU2 + elim (drop_trans_le … HL21 … HLK1) -L1 /2 width=2 by ylt_fwd_le/ #X #HLK2 #H + elim (drop_inv_skip2 … H) -H /2 width=1 by ylt_to_minus/ -Hil #K2 #V2 #HK21 #HV12 #H destruct /3 width=9 by lstas_ldef/ - | lapply (lift_trans_be … HW1 … HWU2 ? ?) -W /2 width=1 by le_S/ #HW1U2 + | lapply (lift_trans_be … HW1 … HWU2 ? ?) -W /2 width=1 by yle_succ_dx/ #HW1U2 lapply (drop_trans_ge … HL21 … HLK1 ?) -L1 /3 width=9 by lstas_ldef, drop_inv_gen/ ] | #G #L1 #K1 #V1 #W1 #i #HLK1 #_ #IHVW1 #L2 #s #l #m #HL21 #X #H #U2 #HWU2 >(lift_mono … HWU2 … H) -U2 elim (lift_inv_lref1 … H) * #Hil #H destruct [ elim (lift_total W1 (l-i-1) m) #W2 #HW12 - elim (drop_trans_le … HL21 … HLK1) -L1 /2 width=2 by lt_to_le/ #X #HLK2 #H - elim (drop_inv_skip2 … H) -H /2 width=1 by lt_plus_to_minus_r/ -Hil #K2 #V2 #HK21 #HV12 #H destruct + elim (drop_trans_le … HL21 … HLK1) -L1 /2 width=2 by ylt_fwd_le/ #X #HLK2 #H + elim (drop_inv_skip2 … H) -H /2 width=1 by ylt_to_minus/ -Hil #K2 #V2 #HK21 #HV12 #H destruct /3 width=10 by lstas_zero/ | lapply (drop_trans_ge … HL21 … HLK1 ?) -L1 /3 width=10 by lstas_zero, drop_inv_gen/ ] | #G #L1 #K1 #W1 #V1 #W #i #d #HLK1 #_ #HW1 #IHWV1 #L2 #s #l #m #HL21 #X #H #U2 #HWU2 elim (lift_inv_lref1 … H) * #Hil #H destruct - [ elim (lift_trans_ge … HW1 … HWU2) -W // minus_plus yplus_SO2 >ymax_pre_sn /3 width=8 by lstas_ldef, ylt_fwd_le_succ1, ex2_intro/ | lapply (drop_conf_ge … HL21 … HLK2 ?) -L2 // #HL1K2 - elim (le_inv_plus_l … Hil) -Hil #Hlim #mi - elim (lift_split … HW2 l (i-m+1)) -HW2 /2 width=1 by le_S_S, le_S/ - #W0 #HW20 minus_minus_m_m /3 width=8 by lstas_ldef, le_S, ex2_intro/ + elim (yle_inv_plus_inj2 … Hil) -Hil #Hlim #mi + elim (lift_split … HW2 l (i-m+1)) -HW2 /2 width=1 by yle_succ_dx, le_S_S/ + #W0 #HW20 minus_minus_m_m /3 width=8 by lstas_ldef, yle_inv_inj, le_S, ex2_intro/ ] | #G #L2 #K2 #W2 #V2 #i #HLK2 #HWV2 #IHWV2 #L1 #s #l #m #HL21 #X #H elim (lift_inv_lref2 … H) * #Hil #H destruct [ -HWV2 | -IHWV2 ] @@ -95,11 +96,11 @@ lemma lstas_inv_lift1: ∀h,G,d. d_deliftable_sn (lstas h G d). elim (lift_inv_lref2 … H) * #Hil #H destruct [ -HWV2 | -IHWV2 ] [ elim (drop_conf_lt … HL21 … HLK2) -L2 // #K1 #W1 #HLK1 #HK21 #HW12 elim (IHWV2 … HK21 … HW12) -K2 #V1 #HV12 #HWV1 - elim (lift_trans_le … HV12 … HW2) -W2 // >minus_plus yplus_SO2 >ymax_pre_sn /3 width=8 by lstas_succ, ylt_fwd_le_succ1, ex2_intro/ | lapply (drop_conf_ge … HL21 … HLK2 ?) -L2 // #HL1K2 - elim (le_inv_plus_l … Hil) -Hil #Hlim #mi - elim (lift_split … HW2 l (i-m+1)) -HW2 /2 width=1 by le_S_S, le_S/ - #W0 #HW20 minus_minus_m_m /3 width=8 by lstas_succ, le_S, ex2_intro/ + elim (yle_inv_plus_inj2 … Hil) -Hil #Hlim #mi + elim (lift_split … HW2 l (i-m+1)) -HW2 /2 width=1 by yle_succ_dx, le_S_S/ + #W0 #HW20 minus_minus_m_m /3 width=8 by lstas_succ, yle_inv_inj, le_S, ex2_intro/ ] | #a #I #G #L2 #V2 #T2 #U2 #d #_ #IHTU2 #L1 #s #l #m #HL21 #X #H elim (lift_inv_bind2 … H) -H #V1 #T1 #HV12 #HT12 #H destruct diff --git a/matita/matita/contribs/lambdadelta/ground_2/lib/arith.ma b/matita/matita/contribs/lambdadelta/ground_2/lib/arith.ma index 93fb86d42..b23fb9de8 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/lib/arith.ma +++ b/matita/matita/contribs/lambdadelta/ground_2/lib/arith.ma @@ -17,6 +17,14 @@ include "ground_2/lib/star.ma". (* ARITHMETICAL PROPERTIES **************************************************) +(* Iota equations ***********************************************************) + +lemma pred_O: pred 0 = 0. +normalize // qed. + +lemma pred_S: ∀m. pred (S m) = m. +// qed. + (* Equations ****************************************************************) lemma minus_plus_m_m_commutative: ∀n,m:nat. n = m + n - m. @@ -168,6 +176,12 @@ let rec iter (n:nat) (B:Type[0]) (op: B → B) (nil: B) ≝ interpretation "iterated function" 'exp op n = (iter n ? op). +lemma iter_O: ∀B:Type[0]. ∀f:B→B.∀b. f^0 b = b. +// qed. + +lemma iter_S: ∀B:Type[0]. ∀f:B→B.∀b,l. f^(S l) b = f (f^l b). +// qed. + lemma iter_SO: ∀B:Type[0]. ∀f:B→B. ∀b,l. f^(l+1) b = f (f^l b). #B #f #b #l >commutative_plus // qed. diff --git a/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_le.ma b/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_le.ma index 1f0195f15..b7b57d764 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_le.ma +++ b/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_le.ma @@ -60,6 +60,22 @@ qed-. lemma yle_inv_Y1: ∀n. ∞ ≤ n → n = ∞. /2 width=3 by yle_inv_Y1_aux/ qed-. +(* Basic properties *********************************************************) + +lemma le_O1: ∀n:ynat. 0 ≤ n. +* /2 width=1 by yle_inj/ +qed. + +lemma yle_refl: reflexive … yle. +* /2 width=1 by le_n, yle_inj/ +qed. + +lemma yle_split: ∀x,y:ynat. x ≤ y ∨ y ≤ x. +* /2 width=1 by or_intror/ +#x * /2 width=1 by or_introl/ +#y elim (le_or_ge x y) /3 width=1 by yle_inj, or_introl, or_intror/ +qed-. + (* Inversion lemmas on successor ********************************************) fact yle_inv_succ1_aux: ∀x,y. x ≤ y → ∀m. x = ⫯m → m ≤ ⫰y ∧ ⫯⫰y = y. @@ -78,20 +94,11 @@ lemma yle_inv_succ: ∀m,n. ⫯m ≤ ⫯n → m ≤ n. #m #n #H elim (yle_inv_succ1 … H) -H // qed-. -(* Basic properties *********************************************************) - -lemma le_O1: ∀n:ynat. 0 ≤ n. -* /2 width=1 by yle_inj/ -qed. - -lemma yle_refl: reflexive … yle. -* /2 width=1 by le_n, yle_inj/ -qed. - -lemma yle_split: ∀x,y:ynat. x ≤ y ∨ y ≤ x. -* /2 width=1 by or_intror/ -#x * /2 width=1 by or_introl/ -#y elim (le_or_ge x y) /3 width=1 by yle_inj, or_introl, or_intror/ +lemma yle_inv_succ2: ∀x,y. x ≤ ⫯y → ⫰x ≤ y. +#x #y #Hxy elim (ynat_cases x) +[ #H destruct // +| * #m #H destruct /2 width=1 by yle_inv_succ/ +] qed-. (* Properties on predecessor ************************************************) @@ -122,7 +129,14 @@ lemma yle_refl_S_dx: ∀x. x ≤ ⫯x. lemma yle_refl_SP_dx: ∀x. x ≤ ⫯⫰x. * // * // -qed. +qed. + +lemma yle_succ2: ∀x,y. ⫰x ≤ y → x ≤ ⫯y. +#x #y #Hxy elim (ynat_cases x) +[ #H destruct // +| * #m #H destruct /2 width=1 by yle_succ/ +] +qed-. (* Main properties **********************************************************) 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 26135550e..3e496e185 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_lt.ma +++ b/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_lt.ma @@ -30,8 +30,8 @@ lemma ylt_fwd_gen: ∀x,y. x < y → ∃m. x = yinj m. #x #y * -x -y /2 width=2 by ex_intro/ qed-. -lemma ylt_fwd_le_succ: ∀x,y. x < y → ⫯x ≤ y. -#x #y * -x -y /2 width=1 by yle_inj/ +lemma ylt_fwd_lt_O1: ∀x,y:ynat. x < y → 0 < y. +#x #y #H elim H -x -y /3 width=2 by ylt_inj, ltn_to_ltO/ qed-. (* Basic inversion lemmas ***************************************************) @@ -102,6 +102,10 @@ lemma ylt_fwd_le_succ1: ∀m,n. m < n → ⫯m ≤ n. #m #n * -m -n /2 width=1 by yle_inj/ qed-. +lemma ylt_fwd_le_pred2: ∀x,y:ynat. x < y → x ≤ ⫰y. +#x #y #H elim H -x -y /3 width=1 by yle_inj, monotonic_pred/ +qed-. + lemma ylt_fwd_le: ∀m:ynat. ∀n:ynat. m < n → m ≤ n. #m #n * -m -n /3 width=1 by lt_to_le, yle_inj/ qed-. @@ -139,9 +143,13 @@ lemma ylt_succ: ∀m,n. m < n → ⫯m < ⫯n. #m #n #H elim H -m -n /3 width=1 by ylt_inj, le_S_S/ qed. +lemma yle_succ1_inj: ∀x,y. ⫯yinj x ≤ y → x < y. +#x * /3 width=1 by yle_inv_inj, ylt_inj/ +qed. + (* Properties on order ******************************************************) -lemma yle_split_eq: ∀m:ynat. ∀n:ynat. m ≤ n → m < n ∨ m = n. +lemma yle_split_eq: ∀m,n:ynat. m ≤ n → m < n ∨ m = n. #m #n * -m -n [ #m #n #Hmn elim (le_to_or_lt_eq … Hmn) -Hmn /3 width=1 by or_introl, ylt_inj/ @@ -149,10 +157,15 @@ lemma yle_split_eq: ∀m:ynat. ∀n:ynat. m ≤ n → m < n ∨ m = n. ] qed-. -lemma ylt_split: ∀m,n:ynat. m < n ∨ n ≤ m.. +lemma ylt_split: ∀m,n:ynat. m < n ∨ n ≤ m. #m #n elim (yle_split m n) /2 width=1 by or_intror/ #H elim (yle_split_eq … H) -H /2 width=1 by or_introl, or_intror/ -qed-. +qed-. + +lemma ylt_split_eq: ∀m,n:ynat. ∨∨ m < n | n = m | n < m. +#m #n elim (ylt_split m n) /2 width=1 by or3_intro0/ +#H elim (yle_split_eq … H) -H /2 width=1 by or3_intro1, or3_intro2/ +qed-. lemma ylt_yle_trans: ∀x:ynat. ∀y:ynat. ∀z:ynat. y ≤ z → x < y → x < z. #x #y #z * -y -z 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 81b9cb015..0c80f8370 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_minus.ma +++ b/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_minus.ma @@ -24,15 +24,24 @@ definition yminus: ynat → ynat → ynat ≝ λx,y. match y with interpretation "ynat minus" 'minus x y = (yminus x y). +lemma yminus_O2: ∀m:ynat. m - 0 = m. +// qed. + +lemma yminus_S2: ∀m:ynat. ∀n:nat. m - S n = ⫰(m - n). +// qed. + +lemma yminus_Y2: ∀m. m - (∞) = 0. +// qed. + (* Basic properties *********************************************************) -lemma yminus_inj: ∀n,m. yinj m - yinj n = yinj (m - n). -#n elim n -n /2 width=3 by trans_eq/ +lemma yminus_inj: ∀m,n. yinj m - yinj n = yinj (m - n). +#m #n elim n -n // +#n #IH >yminus_S2 >IH -IH >eq_minus_S_pred // qed. lemma yminus_Y_inj: ∀n. ∞ - yinj n = ∞. -#n elim n -n // normalize -#n #IHn >IHn // +#n elim n -n // qed. lemma yminus_O1: ∀x:ynat. 0 - x = 0. @@ -51,6 +60,10 @@ lemma yminus_SO2: ∀m. m - 1 = ⫰m. * // qed. +lemma yminus_pred1: ∀x,y. ⫰x - y = ⫰(x-y). +#x * // #y elim y -y // +qed. + lemma yminus_pred: ∀n,m. 0 < m → 0 < n → ⫰m - ⫰n = m - n. * // #n * [ #m #Hm #Hn >yminus_inj >yminus_inj @@ -62,9 +75,7 @@ qed-. (* Properties on successor **************************************************) lemma yminus_succ: ∀n,m. ⫯m - ⫯n = m - n. -* // #n * [2: >yminus_Y_inj // ] -#m >yminus_inj // -qed. +* // qed. lemma yminus_succ1_inj: ∀n:nat. ∀m:ynat. n ≤ m → ⫯m - n = ⫯(m - n). #n * @@ -103,6 +114,15 @@ qed. (* Properties on strict order ***********************************************) +lemma ylt_to_minus: ∀x,y:ynat. x < y → 0 < y - x. +#x #y #H elim H -x -y /3 width=1 by ylt_inj, lt_plus_to_minus_r/ +qed. + +lemma yminus_to_lt: ∀x,y:ynat. 0 < y - x → x < y. +* [2: #y #H elim (ylt_yle_false … H) // ] +#m * /4 width=1 by ylt_inv_inj, ylt_inj, lt_minus_to_plus_r/ +qed-. + lemma monotonic_ylt_minus_dx: ∀x,y:ynat. x < y → ∀z:nat. z ≤ x → x - z < y - z. #x #y * -x -y /4 width=1 by ylt_inj, yle_inv_inj, monotonic_lt_minus_l/ diff --git a/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_plus.ma b/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_plus.ma index e8390c8dd..f7a15c310 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_plus.ma +++ b/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_plus.ma @@ -24,6 +24,15 @@ definition yplus: ynat → ynat → ynat ≝ λx,y. match y with interpretation "ynat plus" 'plus x y = (yplus x y). +lemma yplus_O2: ∀m:ynat. m + 0 = m. +// qed. + +lemma yplus_S2: ∀m:ynat. ∀n. m + S n = ⫯(m + n). +// qed. + +lemma yplus_Y2: ∀m:ynat. m + (∞) = ∞. +// qed. + (* Properties on successor **************************************************) lemma yplus_succ2: ∀m,n. m + ⫯n = ⫯(m + n). @@ -31,7 +40,7 @@ lemma yplus_succ2: ∀m,n. m + ⫯n = ⫯(m + n). qed. lemma yplus_succ1: ∀m,n. ⫯m + n = ⫯(m + n). -#m * normalize // +#m * // #n elim n -n // qed. lemma yplus_succ_swap: ∀m,n. m + ⫯n = ⫯m + n. @@ -44,18 +53,17 @@ qed. (* Basic properties *********************************************************) lemma yplus_inj: ∀n,m. yinj m + yinj n = yinj (m + n). -#n elim n -n [ normalize // ] +#n elim n -n // #n #IHn #m >(yplus_succ2 ? n) >IHn -IHn ysucc_iter_Y // qed. lemma yplus_assoc: associative … yplus. @@ -68,6 +76,10 @@ qed. lemma yplus_O1: ∀n:ynat. 0 + n = n. #n >yplus_comm // qed. +lemma yplus_comm_23: ∀x,y,z. x + z + y = x + y + z. +#x #y #z >yplus_assoc // +qed. + (* Basic inversion lemmas ***************************************************) lemma yplus_inv_inj: ∀z,y,x. x + y = yinj z → @@ -104,7 +116,7 @@ lemma monotonic_yle_plus_sn: ∀x,y. x ≤ y → ∀z. z + x ≤ z + y. lemma monotonic_yle_plus: ∀x1,y1. x1 ≤ y1 → ∀x2,y2. x2 ≤ y2 → x1 + x2 ≤ y1 + y2. -/3 width=3 by monotonic_yle_plus_dx, yle_trans/ qed. +/3 width=3 by monotonic_yle_plus_dx, monotonic_yle_plus_sn, yle_trans/ qed. (* Forward lemmas on order **************************************************) @@ -132,6 +144,10 @@ lemma yle_fwd_plus_ge_inj: ∀m1:nat. ∀m2,n1,n2:ynat. m2 ≤ m1 → m1 + n1 #x #H0 #H destruct /3 width=4 by yle_fwd_plus_ge, yle_inj/ qed-. +lemma yle_fwd_plus_yge: ∀n2,m1:ynat. ∀n1,m2:nat. m2 ≤ m1 → m1 + n1 ≤ m2 + n2 → n1 ≤ n2. +* // #n2 * /2 width=4 by yle_fwd_plus_ge_inj/ +qed-. + (* Forward lemmas on strict order *******************************************) lemma ylt_inv_monotonic_plus_dx: ∀x,y,z. x + z < y + z → x < y. @@ -155,6 +171,17 @@ qed. lemma monotonic_ylt_plus_sn: ∀x,y. x < y → ∀z:nat. yinj z + x < yinj z + y. /2 width=1 by monotonic_ylt_plus_dx/ qed. +(* Properties on predeccessor ***********************************************) + +lemma yplus_pred1: ∀x,y:ynat. 0 < x → ⫰x + y = ⫰(x+y). +#x * // #y elim y -y // #y #IH #Hx +>yplus_S2 >yplus_S2 >IH -IH // >ylt_inv_O1 +/2 width=1 by ylt_plus_dx1_trans/ +qed-. + +lemma yplus_pred2: ∀x,y:ynat. 0 < y → x + ⫰y = ⫰(x+y). +/2 width=1 by yplus_pred1/ qed-. + (* Properties on minus ******************************************************) lemma yplus_minus_inj: ∀m:ynat. ∀n:nat. m + n - n = m. @@ -166,10 +193,18 @@ lemma yplus_minus: ∀m,n. m + n - n ≤ m. #m * // qed. +lemma yminus_plus2: ∀z,y,x:ynat. x - (y + z) = x - y - z. +* // #z * [2: >yplus_Y1 >yminus_O1 // ] #y * +[ #x >yplus_inj >yminus_inj >yminus_inj >yminus_inj /2 width=1 by eq_f/ +| >yplus_inj >yminus_Y_inj // +] +qed. + (* Forward lemmas on minus **************************************************) lemma yle_plus1_to_minus_inj2: ∀x,z:ynat. ∀y:nat. x + y ≤ z → x ≤ z - y. -/2 width=1 by monotonic_yle_minus_dx/ qed-. +#x #z #y #H lapply (monotonic_yle_minus_dx … H y) -H // +qed-. lemma yle_plus1_to_minus_inj1: ∀x,z:ynat. ∀y:nat. y + x ≤ z → x ≤ z - y. /2 width=1 by yle_plus1_to_minus_inj2/ qed-. @@ -188,12 +223,36 @@ lemma yplus_minus_assoc_inj: ∀x:nat. ∀y,z:ynat. x ≤ y → z + (y - x) = z ] qed-. +lemma yplus_minus_assoc_comm_inj: ∀x:nat. ∀y,z:ynat. x ≤ y → z - (y - x) = z + x - y. +#x * +[ #y * + [ #z >yminus_inj >yminus_inj >yplus_inj >yminus_inj + /4 width=1 by yle_inv_inj, minus_le_minus_minus_comm, eq_f/ + | >yminus_inj >yminus_Y_inj // + ] +| >yminus_Y_inj // +] +qed-. + lemma yplus_minus_comm_inj: ∀y:nat. ∀x,z:ynat. y ≤ x → x + z - y = x - y + z. #y * // #x * // #z #Hxy >yplus_inj >yminus_inj