From: Ferruccio Guidi Date: Fri, 17 Jan 2014 19:31:58 +0000 (+0000) Subject: commit of the "unfold" component ... X-Git-Tag: make_still_working~995 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=3d953276edded0659cc73489290da43fb3ebb94c;p=helm.git commit of the "unfold" component ... --- diff --git a/matita/matita/contribs/lambdadelta/basic_2/unfold/lsstas_alt.ma b/matita/matita/contribs/lambdadelta/basic_2/unfold/lsstas_alt.ma index 6fab6dec6..849579fa8 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/unfold/lsstas_alt.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/unfold/lsstas_alt.ma @@ -21,9 +21,9 @@ include "basic_2/unfold/lsstas_lift.ma". inductive lsstasa (h) (g): genv → relation4 lenv nat term term ≝ | lsstasa_O : ∀G,L,T. lsstasa h g G L 0 T T | lsstasa_sort: ∀G,L,l,k. lsstasa h g G L l (⋆k) (⋆((next h)^l k)) -| lsstasa_ldef: ∀G,L,K,V,W,U,i,l. ⇩[0, i] L ≡ K.ⓓV → lsstasa h g G K (l+1) V W → +| lsstasa_ldef: ∀G,L,K,V,W,U,i,l. ⇩[i] L ≡ K.ⓓV → lsstasa h g G K (l+1) V W → ⇧[0, i+1] W ≡ U → lsstasa h g G L (l+1) (#i) U -| lsstasa_ldec: ∀G,L,K,W,V,U,i,l,l0. ⇩[0, i] L ≡ K.ⓛW → ⦃G, K⦄ ⊢ W ▪[h, g] l0 → +| lsstasa_ldec: ∀G,L,K,W,V,U,i,l,l0. ⇩[i] L ≡ K.ⓛW → ⦃G, K⦄ ⊢ W ▪[h, g] l0 → lsstasa h g G K l W V → ⇧[0, i+1] V ≡ U → lsstasa h g G L (l+1) (#i) U | lsstasa_bind: ∀a,I,G,L,V,T,U,l. lsstasa h g G (L.ⓑ{I}V) l T U → lsstasa h g G L l (ⓑ{a,I}V.T) (ⓑ{a,I}V.U) @@ -38,7 +38,7 @@ interpretation "nat-iterated stratified static type assignment (term) alternativ lemma ssta_lsstasa: ∀h,g,G,L,T,U. ⦃G, L⦄ ⊢ T •[h, g] U → ⦃G, L⦄ ⊢ T ••*[h, g, 1] U. #h #g #G #L #T #U #H elim H -G -L -T -U -// /2 width=1/ /2 width=6/ /2 width=8/ +/2 width=8 by lsstasa_O, lsstasa_sort, lsstasa_ldef, lsstasa_ldec, lsstasa_bind, lsstasa_appl, lsstasa_cast/ qed. lemma lsstasa_step_dx: ∀h,g,G,L,T1,T,l. ⦃G, L⦄ ⊢ T1 ••*[h, g, l] T → @@ -48,29 +48,29 @@ lemma lsstasa_step_dx: ∀h,g,G,L,T1,T,l. ⦃G, L⦄ ⊢ T1 ••*[h, g, l] T | #G #L #l #k #X #H >(ssta_inv_sort1 … H) -X >commutative_plus // | #G #L #K #V #W #U #i #l #HLK #_ #HWU #IHVW #U2 #HU2 lapply (ldrop_fwd_drop2 … HLK) #H - elim (ssta_inv_lift1 … HU2 … H … HWU) -H -U /3 width=6/ + elim (ssta_inv_lift1 … HU2 … H … HWU) -H -U /3 width=6 by lsstasa_ldef/ | #G #L #K #W #V #U #i #l #l0 #HLK #HWl0 #_ #HVU #IHWV #U2 #HU2 lapply (ldrop_fwd_drop2 … HLK) #H - elim (ssta_inv_lift1 … HU2 … H … HVU) -H -U /3 width=8/ + elim (ssta_inv_lift1 … HU2 … H … HVU) -H -U /3 width=8 by lsstasa_ldec/ | #a #I #G #L #V #T1 #U1 #l #_ #IHTU1 #X #H - elim (ssta_inv_bind1 … H) -H #U #HU1 #H destruct /3 width=1/ + elim (ssta_inv_bind1 … H) -H #U #HU1 #H destruct /3 width=1 by lsstasa_bind/ | #G #L #V #T1 #U1 #l #_ #IHTU1 #X #H - elim (ssta_inv_appl1 … H) -H #U #HU1 #H destruct /3 width=1/ -| /3 width=1/ + elim (ssta_inv_appl1 … H) -H #U #HU1 #H destruct /3 width=1 by lsstasa_appl/ +| /3 width=1 by lsstasa_cast/ ] qed. (* Main properties **********************************************************) theorem lsstas_lsstasa: ∀h,g,G,L,T,U,l. ⦃G, L⦄ ⊢ T •*[h, g, l] U → ⦃G, L⦄ ⊢ T ••*[h, g, l] U. -#h #g #G #L #T #U #l #H @(lsstas_ind_dx … H) -U -l // /2 width=3/ +#h #g #G #L #T #U #l #H @(lsstas_ind_dx … H) -U -l /2 width=3 by lsstasa_step_dx, lsstasa_O/ qed. (* Main inversion lemmas ****************************************************) theorem lsstasa_inv_lsstas: ∀h,g,G,L,T,U,l. ⦃G, L⦄ ⊢ T ••*[h, g, l] U → ⦃G, L⦄ ⊢ T •*[h, g, l] U. #h #g #G #L #T #U #l #H elim H -G -L -T -U -l -// /2 width=1/ /2 width=6/ /3 width=8 by lsstas_ldec, lsstas_inv_SO/ +/2 width=8 by lsstas_inv_SO, lsstas_ldec, lsstas_ldef, lsstas_cast, lsstas_appl, lsstas_bind/ qed-. (* Advanced eliminators *****************************************************) @@ -79,11 +79,11 @@ lemma lsstas_ind_alt: ∀h,g. ∀R:genv→relation4 lenv nat term term. (∀G,L,T. R G L O T T) → (∀G,L,l,k. R G L l (⋆k) (⋆((next h)^l k))) → ( ∀G,L,K,V,W,U,i,l. - ⇩[O, i] L ≡ K.ⓓV → ⦃G, K⦄ ⊢ V •*[h, g, l+1] W → ⇧[O, i+1] W ≡ U → + ⇩[i] L ≡ K.ⓓV → ⦃G, K⦄ ⊢ V •*[h, g, l+1] W → ⇧[O, i+1] W ≡ U → R G K (l+1) V W → R G L (l+1) (#i) U ) → ( ∀G,L,K,W,V,U,i,l,l0. - ⇩[O, i] L ≡ K.ⓛW → ⦃G, K⦄ ⊢ W ▪[h, g] l0 → + ⇩[i] L ≡ K.ⓛW → ⦃G, K⦄ ⊢ W ▪[h, g] l0 → ⦃G, K⦄ ⊢ W •*[h, g, l]V → ⇧[O, i+1] V ≡ U → R G K l W V → R G L (l+1) (#i) U ) → ( diff --git a/matita/matita/contribs/lambdadelta/basic_2/unfold/lsstas_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/unfold/lsstas_lift.ma index 76c9c27f3..2a7cc800e 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/unfold/lsstas_lift.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/unfold/lsstas_lift.ma @@ -20,27 +20,28 @@ include "basic_2/unfold/lsstas.ma". (* Properties on relocation *************************************************) lemma lsstas_lift: ∀h,g,G,l. l_liftable (llstar … (ssta h g G) l). -/2 width=1/ qed. +/3 width=10 by l_liftable_llstar, ssta_lift/ qed. (* Inversion lemmas on relocation *******************************************) lemma lsstas_inv_lift1: ∀h,g,G,l. l_deliftable_sn (llstar … (ssta h g G) l). -/3 width=5 by l_deliftable_sn_llstar, ssta_inv_lift1/ qed-. +/3 width=6 by l_deliftable_sn_llstar, ssta_inv_lift1/ qed-. (* Advanced inversion lemmas ************************************************) lemma lsstas_inv_lref1: ∀h,g,G,L,U,i,l. ⦃G, L⦄ ⊢ #i •*[h, g, l+1] U → - (∃∃K,V,W. ⇩[0, i] L ≡ K.ⓓV & ⦃G, K⦄ ⊢ V •*[h, g, l+1] W & + (∃∃K,V,W. ⇩[i] L ≡ K.ⓓV & ⦃G, K⦄ ⊢ V •*[h, g, l+1] W & ⇧[0, i + 1] W ≡ U ) ∨ - (∃∃K,W,V,l0. ⇩[0, i] L ≡ K.ⓛW & ⦃G, K⦄ ⊢ W ▪[h, g] l0 & + (∃∃K,W,V,l0. ⇩[i] L ≡ K.ⓛW & ⦃G, K⦄ ⊢ W ▪[h, g] l0 & ⦃G, K⦄ ⊢ W •*[h, g, l] V & ⇧[0, i + 1] V ≡ U ). #h #g #G #L #U #i #l #H elim (lsstas_inv_step_sn … H) -H #X #H #HXU elim (ssta_inv_lref1 … H) -H * #K [ #V #W | #W #l0 ] #HLK [ #HVW | #HWl0 ] #HWX lapply (ldrop_fwd_drop2 … HLK) #H0LK -elim (lsstas_inv_lift1 … HXU … H0LK … HWX) -H0LK -X /3 width=8/ /4 width=6/ +elim (lsstas_inv_lift1 … HXU … H0LK … HWX) -H0LK -X +/4 width=8 by lsstas_step_sn, ex4_4_intro, ex3_3_intro, or_introl, or_intror/ qed-. (* Advanced forward lemmas **************************************************) @@ -48,35 +49,35 @@ qed-. lemma lsstas_fwd_correct: ∀h,g,G,L,T1,U1. ⦃G, L⦄ ⊢ T1 •[h, g] U1 → ∀T2,l. ⦃G, L⦄ ⊢ T1 •*[h, g, l] T2 → ∃U2. ⦃G, L⦄ ⊢ T2 •[h, g] U2. -#h #g #G #L #T1 #U1 #HTU1 #T2 #l #H @(lsstas_ind_dx … H) -l -T2 [ /2 width=3/ ] -HTU1 +#h #g #G #L #T1 #U1 #HTU1 #T2 #l #H @(lsstas_ind_dx … H) -l -T2 [ /2 width=3 by ex_intro/ ] -HTU1 #l #T #T2 #_ #HT2 #_ -T1 -U1 -l -elim (ssta_fwd_correct … HT2) -T /2 width=2/ +elim (ssta_fwd_correct … HT2) -T /2 width=2 by ex_intro/ qed-. (* Advanced properties ******************************************************) lemma lsstas_total: ∀h,g,G,L,T,U. ⦃G, L⦄ ⊢ T •[h, g] U → ∀l. ∃U0. ⦃G, L⦄ ⊢ T •*[h, g, l] U0. -#h #g #G #L #T #U #HTU #l @(nat_ind_plus … l) -l [ /2 width=2/ ] +#h #g #G #L #T #U #HTU #l @(nat_ind_plus … l) -l [ /2 width=2 by lstar_O, ex_intro/ ] #l * #U0 #HTU0 -elim (lsstas_fwd_correct … HTU … HTU0) -U /3 width=4/ +elim (lsstas_fwd_correct … HTU … HTU0) -U /3 width=4 by lsstas_step_dx, ex_intro/ qed-. -lemma lsstas_ldef: ∀h,g,G,L,K,V,i. ⇩[0, i] L ≡ K.ⓓV → +lemma lsstas_ldef: ∀h,g,G,L,K,V,i. ⇩[i] L ≡ K.ⓓV → ∀W,l. ⦃G, K⦄ ⊢ V •*[h, g, l+1] W → ∀U. ⇧[0, i+1] W ≡ U → ⦃G, L⦄ ⊢ #i •*[h, g, l+1] U. #h #g #G #L #K #V #i #HLK #W #l #HVW #U #HWU lapply (ldrop_fwd_drop2 … HLK) elim (lsstas_inv_step_sn … HVW) -HVW #W0 -elim (lift_total W0 0 (i+1)) /3 width=11/ +elim (lift_total W0 0 (i+1)) /3 width=12 by lsstas_step_sn, ssta_ldef, lsstas_lift/ qed. -lemma lsstas_ldec: ∀h,g,G,L,K,W,i. ⇩[0, i] L ≡ K.ⓛW → ∀l0. ⦃G, K⦄ ⊢ W ▪[h, g] l0 → +lemma lsstas_ldec: ∀h,g,G,L,K,W,i. ⇩[i] L ≡ K.ⓛW → ∀l0. ⦃G, K⦄ ⊢ W ▪[h, g] l0 → ∀V,l. ⦃G, K⦄ ⊢ W •*[h, g, l] V → ∀U. ⇧[0, i+1] V ≡ U → ⦃G, L⦄ ⊢ #i •*[h, g, l+1] U. #h #g #G #L #K #W #i #HLK #T #HWT #V #l #HWV #U #HVU lapply (ldrop_fwd_drop2 … HLK) #H -elim (lift_total W 0 (i+1)) /3 width=11/ +elim (lift_total W 0 (i+1)) /3 width=12 by lsstas_step_sn, ssta_ldec, lsstas_lift/ qed. (* Properties on degree assignment for terms ********************************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/unfold/unfold.ma b/matita/matita/contribs/lambdadelta/basic_2/unfold/unfold.ma index 160c6da76..4599cf038 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/unfold/unfold.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/unfold/unfold.ma @@ -22,8 +22,8 @@ include "basic_2/relocation/ldrop.ma". (* activate genv *) inductive unfold: relation4 genv lenv term lenv ≝ | unfold_sort: ∀G,L,k. unfold G L (⋆k) L -| unfold_lref: ∀I,G,L1,L2,K1,K2,V,i. ⇩[0, i] L1 ≡ K1. ⓑ{I}V → - unfold G K1 V K2 → ⇩[|L2|, i] L2 ≡ K2 → +| unfold_lref: ∀I,G,L1,L2,K1,K2,V,i. ⇩[i] L1 ≡ K1. ⓑ{I}V → + unfold G K1 V K2 → ⇩[Ⓣ, |L2|, i] L2 ≡ K2 → unfold G L1 (#i) (L1@@L2) | unfold_bind: ∀a,I,G,L1,L2,V,T. unfold G (L1.ⓑ{I}V) T L2 → unfold G L1 (ⓑ{a,I}V.T) L2