X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fstatic%2Ffrees_drops.ma;h=fe24eadf5d0496b0dce3a9145e2e441f55e4174b;hp=fd4ec0ce18854cdcac109112a786ab1ddd8db7d0;hb=222044da28742b24584549ba86b1805a87def070;hpb=d64b4238ec803353f0a06f2aad25c173852b0526 diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/frees_drops.ma b/matita/matita/contribs/lambdadelta/basic_2/static/frees_drops.ma index fd4ec0ce1..fe24eadf5 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/static/frees_drops.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/static/frees_drops.ma @@ -12,108 +12,234 @@ (* *) (**************************************************************************) -include "ground_2/relocation/rtmap_pushs.ma". -include "ground_2/relocation/rtmap_coafter.ma". -include "basic_2/relocation/lifts_lifts.ma". -include "basic_2/relocation/drops.ma". -include "basic_2/static/frees.ma". +include "ground_2/relocation/nstream_coafter.ma". +include "basic_2/relocation/drops_drops.ma". +include "basic_2/static/frees_fqup.ma". (* CONTEXT-SENSITIVE FREE VARIABLES *****************************************) (* Advanced properties ******************************************************) -lemma frees_lref_atom: âL,i. â¬*[â», ðâ´iâµ] L â¡ â â L ⢠ð *â¦#i⦠⡠ðð. -#L elim L -L /2 width=1 by frees_atom/ -#L #I #V #IH * +lemma frees_atom_drops: âb,L,i. â¬*[b, ðâ´iâµ] L â â â + âf. ðâ¦f⦠â L ⢠ð *â¦#i⦠â ⫯*[i]âf. +#b #L elim L -L /2 width=1 by frees_atom/ +#L #I #IH * [ #H lapply (drops_fwd_isid ⦠H ?) -H // #H destruct | /4 width=3 by frees_lref, drops_inv_drop1/ ] qed. -lemma frees_lref_pair: âf,K,V. K ⢠ð *â¦V⦠⡠f â - âi,I,L. â¬*[i] L â¡ K.â{I}V â L ⢠ð *â¦#i⦠⡠â*[i] ⫯f. +lemma frees_pair_drops: âf,K,V. K ⢠ð *â¦V⦠â f â + âi,I,L. â¬*[i] L â K.â{I}V â L ⢠ð *â¦#i⦠â ⫯*[i] âf. #f #K #V #Hf #i elim i -i -[ #I #L #H lapply (drops_fwd_isid ⦠H ?) -H /2 width=1 by frees_zero/ +[ #I #L #H lapply (drops_fwd_isid ⦠H ?) -H /2 width=1 by frees_pair/ | #i #IH #I #L #H elim (drops_inv_succ ⦠H) -H /3 width=2 by frees_lref/ ] qed. +lemma frees_unit_drops: âf. ðâ¦f⦠â âI,K,i,L. â¬*[i] L â K.â¤{I} â + L ⢠ð *â¦#i⦠â ⫯*[i] âf. +#f #Hf #I #K #i elim i -i +[ #L #H lapply (drops_fwd_isid ⦠H ?) -H /2 width=1 by frees_unit/ +| #i #IH #Y #H elim (drops_inv_succ ⦠H) -H + #J #L #HLK #H destruct /3 width=1 by frees_lref/ +] +qed. +(* +lemma frees_sort_pushs: âf,K,s. K ⢠ð *â¦âs⦠â f â + âi,L. â¬*[i] L â K â L ⢠ð *â¦âs⦠â ⫯*[i] f. +#f #K #s #Hf #i elim i -i +[ #L #H lapply (drops_fwd_isid ⦠H ?) -H // +| #i #IH #L #H elim (drops_inv_succ ⦠H) -H /3 width=1 by frees_sort/ +] +qed. +*) +lemma frees_lref_pushs: âf,K,j. K ⢠ð *â¦#j⦠â f â + âi,L. â¬*[i] L â K â L ⢠ð *â¦#(i+j)⦠â ⫯*[i] f. +#f #K #j #Hf #i elim i -i +[ #L #H lapply (drops_fwd_isid ⦠H ?) -H // +| #i #IH #L #H elim (drops_inv_succ ⦠H) -H + #I #Y #HYK #H destruct /3 width=1 by frees_lref/ +] +qed. +(* +lemma frees_gref_pushs: âf,K,l. K ⢠ð *â¦Â§l⦠â f â + âi,L. â¬*[i] L â K â L ⢠ð *â¦Â§l⦠â ⫯*[i] f. +#f #K #l #Hf #i elim i -i +[ #L #H lapply (drops_fwd_isid ⦠H ?) -H // +| #i #IH #L #H elim (drops_inv_succ ⦠H) -H /3 width=1 by frees_gref/ +] +qed. +*) (* Advanced inversion lemmas ************************************************) -lemma frees_inv_lref_drops: âi,f,L. L ⢠ð *â¦#i⦠⡠f â - (â¬*[â», ðâ´iâµ] L â¡ â ⧠ðâ¦fâ¦) ⨠- ââg,I,K,V. K ⢠ð *â¦V⦠⡠g & - â¬*[i] L â¡ K.â{I}V & f = â*[i] ⫯g. -#i elim i -i -[ #f #L #H elim (frees_inv_zero ⦠H) -H * - /4 width=7 by ex3_4_intro, or_introl, or_intror, conj, drops_refl/ -| #i #IH #f #L #H elim (frees_inv_lref ⦠H) -H * /3 width=1 by or_introl, conj/ - #g #I #K #V #Hg #H1 #H2 destruct - elim (IH ⦠Hg) -IH -Hg * - [ /4 width=3 by or_introl, conj, isid_push, drops_drop/ - | /4 width=7 by drops_drop, ex3_4_intro, or_intror/ +lemma frees_inv_lref_drops: âL,i,f. L ⢠ð *â¦#i⦠â f â + â¨â¨ ââg. â¬*[â», ðâ´iâµ] L â â & ðâ¦g⦠& f = ⫯*[i] âg + | ââg,I,K,V. K ⢠ð *â¦V⦠â g & + â¬*[i] L â K.â{I}V & f = ⫯*[i] âg + | ââg,I,K. â¬*[i] L â K.â¤{I} & ðâ¦g⦠& f = ⫯*[i] âg. +#L elim L -L +[ #i #g | #L #I #IH * [ #g cases I -I [ #I | #I #V ] -IH | #i #g ] ] #H +[ elim (frees_inv_atom ⦠H) -H #f #Hf #H destruct + /3 width=3 by or3_intro0, ex3_intro/ +| elim (frees_inv_unit ⦠H) -H #f #Hf #H destruct + /4 width=3 by drops_refl, or3_intro2, ex3_3_intro/ +| elim (frees_inv_pair ⦠H) -H #f #Hf #H destruct + /4 width=7 by drops_refl, or3_intro1, ex3_4_intro/ +| elim (frees_inv_lref ⦠H) -H #f #Hf #H destruct + elim (IH ⦠Hf) -IH -Hf * + [ /4 width=3 by drops_drop, or3_intro0, ex3_intro/ + | /4 width=7 by drops_drop, or3_intro1, ex3_4_intro/ + | /4 width=3 by drops_drop, or3_intro2, ex3_3_intro/ ] ] qed-. (* Properties with generic slicing for local environments *******************) +lemma frees_lifts: âb,f1,K,T. K ⢠ð *â¦T⦠â f1 â + âf,L. â¬*[b, f] L â K â âU. â¬*[f] T â U â + âf2. f ~â f1 â f2 â L ⢠ð *â¦U⦠â f2. +#b #f1 #K #T #H lapply (frees_fwd_isfin ⦠H) elim H -f1 -K -T +[ #f1 #K #s #Hf1 #_ #f #L #HLK #U #H2 #f2 #H3 + lapply (coafter_isid_inv_dx ⦠H3 ⦠Hf1) -f1 #Hf2 + >(lifts_inv_sort1 ⦠H2) -U /2 width=1 by frees_sort/ +| #f1 #i #Hf1 #_ #f #L #H1 #U #H2 #f2 #H3 + elim (lifts_inv_lref1 ⦠H2) -H2 #j #Hij #H destruct + elim (coafter_fwd_xnx_pushs ⦠Hij H3) -H3 #g2 #Hg2 #H2 destruct + lapply (coafter_isid_inv_dx ⦠Hg2 ⦠Hf1) -f1 #Hf2 + elim (drops_inv_atom2 ⦠H1) -H1 #n #g #H1 #Hf + elim (after_at_fwd ⦠Hij ⦠Hf) -f #x #_ #Hj -g -i + lapply (at_inv_uni ⦠Hj) -Hj #H destruct + /3 width=8 by frees_atom_drops, drops_trans/ +| #f1 #I #K #V #_ #IH #Hf1 #f #L #H1 #U #H2 #f2 #H3 + lapply (isfin_inv_next ⦠Hf1 ??) -Hf1 [3: |*: // ] #Hf1 + lapply (lifts_inv_lref1 ⦠H2) -H2 * #j #Hf #H destruct + elim (drops_split_trans_bind2 ⦠H1) -H1 [ |*: // ] #Z #Y #HLY #HYK #H + elim (liftsb_inv_pair_sn ⦠H) -H #W #HVW #H destruct + elim (coafter_fwd_xnx_pushs ⦠Hf H3) -H3 #g2 #H3 #H2 destruct + lapply (IH ⦠HYK ⦠HVW ⦠H3) -IH -H3 -HYK -HVW // + /2 width=5 by frees_pair_drops/ +| #f1 #I #K #Hf1 #_ #f #L #H1 #U #H2 #f2 #H3 + lapply (lifts_inv_lref1 ⦠H2) -H2 * #j #Hf #H destruct + elim (coafter_fwd_xnx_pushs ⦠Hf H3) -H3 #g2 #H3 #H2 destruct + lapply (coafter_isid_inv_dx ⦠H3 ⦠Hf1) -f1 #Hg2 + elim (drops_split_trans_bind2 ⦠H1 ⦠Hf) -H1 -Hf #Z #Y #HLY #_ #H + lapply (liftsb_inv_unit_sn ⦠H) -H #H destruct + /2 width=3 by frees_unit_drops/ +| #f1 #I #K #i #_ #IH #Hf1 #f #L #H1 #U #H2 #f2 #H3 + lapply (isfin_inv_push ⦠Hf1 ??) -Hf1 [3: |*: // ] #Hf1 + lapply (lifts_inv_lref1 ⦠H2) -H2 * #x #Hf #H destruct + elim (at_inv_nxx ⦠Hf) -Hf [ |*: // ] #j #Hf #H destruct + elim (drops_split_trans_bind2 ⦠H1) -H1 [ |*: // ] #Z #Y #HLY #HYK #_ + elim (coafter_fwd_xpx_pushs ⦠0 ⦠H3) [ |*: // ] #g2 #H3 #H2 destruct + lapply (drops_isuni_fwd_drop2 ⦠HLY) -HLY // #HLY + lapply (IH ⦠HYK ⦠H3) -IH -H3 -HYK [4: |*: /2 width=2 by lifts_lref/ ] + >plus_S1 /2 width=3 by frees_lref_pushs/ (**) (* full auto fails *) +| #f1 #K #l #Hf1 #_ #f #L #HLK #U #H2 #f2 #H3 + lapply (coafter_isid_inv_dx ⦠H3 ⦠Hf1) -f1 #Hf2 + >(lifts_inv_gref1 ⦠H2) -U /2 width=1 by frees_gref/ +| #f1V #f1T #f1 #p #I #K #V #T #_ #_ #H1f1 #IHV #IHT #H2f1 #f #L #H1 #Y #H2 #f2 #H3 + elim (sor_inv_isfin3 ⦠H1f1) // #Hf1V #H + lapply (isfin_inv_tl ⦠H) -H + elim (lifts_inv_bind1 ⦠H2) -H2 #W #U #HVW #HTU #H destruct + elim (coafter_sor ⦠H3 ⦠H1f1) /2 width=5 by coafter_isfin2_fwd/ -H3 -H1f1 #f2V #f2T #Hf2V #H + elim (coafter_inv_tl1 ⦠H) -H + /5 width=5 by frees_bind, drops_skip, ext2_pair/ +| #f1V #f1T #f1 #I #K #V #T #_ #_ #H1f1 #IHV #IHT #H2f1 #f #L #H1 #Y #H2 #f2 #H3 + elim (sor_inv_isfin3 ⦠H1f1) // + elim (lifts_inv_flat1 ⦠H2) -H2 #W #U #HVW #HTU #H destruct + elim (coafter_sor ⦠H3 ⦠H1f1) + /3 width=5 by coafter_isfin2_fwd, frees_flat/ +] +qed-. + +lemma frees_lifts_SO: âb,L,K. â¬*[b, ðâ´1âµ] L â K â âT,U. â¬*[1] T â U â + âf. K ⢠ð *â¦T⦠â f â L ⢠ð *â¦U⦠â ⫯f. +#b #L #K #HLK #T #U #HTU #f #Hf +@(frees_lifts b ⦠Hf ⦠HTU) // (**) (* auto fails *) +qed. + +(* Forward lemmas with generic slicing for local environments ***************) + +lemma frees_fwd_coafter: âb,f2,L,U. L ⢠ð *â¦U⦠â f2 â + âf,K. â¬*[b, f] L â K â âT. â¬*[f] T â U â + âf1. K ⢠ð *â¦T⦠â f1 â f ~â f1 â f2. +/4 width=11 by frees_lifts, frees_mono, coafter_eq_repl_back0/ qed-. + (* Inversion lemmas with generic slicing for local environments *************) -lemma frees_inv_lifts: âb,f2,L,U. L ⢠ð *â¦U⦠⡠f2 â - âf,K. â¬*[b, f] L â¡ K â âT. â¬*[f] T â¡ U â - âf1. f ~â f1 â¡ f2 â K ⢠ð *â¦T⦠⡠f1. -#b #f2 #L #U #H lapply (frees_fwd_isfin ⦠H) elim H -f2 -L -U -[ #f2 #I #Hf2 #_ #f #K #H1 #T #H2 #f1 #H3 - lapply (coafter_fwd_isid2 ⦠H3 ⦠Hf2) -H3 // -Hf2 #Hf1 - elim (drops_inv_atom1 ⦠H1) -H1 #H #_ destruct - elim (lifts_fwd_atom2 ⦠H2) -H2 - /2 width=3 by frees_atom/ -| #f2 #I #L #W #s #_ #IH #Hf2 #f #Y #H1 #T #H2 #f1 #H3 - lapply (isfin_fwd_push ⦠Hf2 ??) -Hf2 [3: |*: // ] #Hf2 - lapply (lifts_inv_sort2 ⦠H2) -H2 #H destruct - elim (coafter_inv_xxp ⦠H3) -H3 [1,3: * |*: // ] - [ #g #g1 #Hf2 #H #H0 destruct - elim (drops_inv_skip1 ⦠H1) -H1 #K #V #HLK #_ #H destruct - | #g #Hf2 #H destruct - lapply (drops_inv_drop1 ⦠H1) -H1 - ] /3 width=4 by frees_sort/ -| #f2 #I #L #W #_ #IH #Hf2 #f #Y #H1 #T #H2 #f1 #H3 - lapply (isfin_inv_next ⦠Hf2 ??) -Hf2 [3: |*: // ] #Hf2 - elim (lifts_inv_lref2 ⦠H2) -H2 #i #H2 #H destruct - lapply (at_inv_xxp ⦠H2 ?) -H2 // * #g #H #H0 destruct - elim (drops_inv_skip1 ⦠H1) -H1 #K #V #HLK #HVW #H destruct - elim (coafter_inv_pxn ⦠H3) -H3 [ |*: // ] #g1 #Hf2 #H destruct - /3 width=4 by frees_zero/ -| #f2 #I #L #W #j #_ #IH #Hf2 #f #Y #H1 #T #H2 #f1 #H3 - lapply (isfin_fwd_push ⦠Hf2 ??) -Hf2 [3: |*: // ] #Hf2 - elim (lifts_inv_lref2 ⦠H2) -H2 #x #H2 #H destruct - elim (coafter_inv_xxp ⦠H3) -H3 [1,3: * |*: // ] - [ #g #g1 #Hf2 #H #H0 destruct - elim (drops_inv_skip1 ⦠H1) -H1 #K #V #HLK #HVW #H destruct - elim (at_inv_xpn ⦠H2) -H2 [ |*: // ] #j #Hg #H destruct - | #g #Hf2 #H destruct - lapply (drops_inv_drop1 ⦠H1) -H1 - lapply (at_inv_xnn ⦠H2 ????) -H2 [5: |*: // ] - ] /4 width=4 by lifts_lref, frees_lref/ -| #f2 #I #L #W #l #_ #IH #Hf2 #f #Y #H1 #T #H2 #f1 #H3 - lapply (isfin_fwd_push ⦠Hf2 ??) -Hf2 [3: |*: // ] #Hf2 - lapply (lifts_inv_gref2 ⦠H2) -H2 #H destruct - elim (coafter_inv_xxp ⦠H3) -H3 [1,3: * |*: // ] - [ #g #g1 #Hf2 #H #H0 destruct - elim (drops_inv_skip1 ⦠H1) -H1 #K #V #HLK #_ #H destruct - | #g #Hf2 #H destruct - lapply (drops_inv_drop1 ⦠H1) -H1 - ] /3 width=4 by frees_gref/ -| #f2W #f2U #f2 #p #I #L #W #U #_ #_ #H1f2 #IHW #IHU #H2f2 #f #K #H1 #X #H2 #f1 #H3 - elim (sor_inv_isfin3 ⦠H1f2) // #H1f2W #H - lapply (isfin_inv_tl ⦠H) -H - elim (lifts_inv_bind2 ⦠H2) -H2 #V #T #HVW #HTU #H destruct - elim (coafter_inv_sor ⦠H3 ⦠H1f2) -H3 -H1f2 // #f1W #f1U #H2f2W #H - elim (coafter_inv_tl0 ⦠H) -H /4 width=5 by frees_bind, drops_skip/ -| #f2W #f2U #f2 #I #L #W #U #_ #_ #H1f2 #IHW #IHU #H2f2 #f #K #H1 #X #H2 #f1 #H3 - elim (sor_inv_isfin3 ⦠H1f2) // - elim (lifts_inv_flat2 ⦠H2) -H2 #V #T #HVW #HTU #H destruct - elim (coafter_inv_sor ⦠H3 ⦠H1f2) -H3 -H1f2 /3 width=5 by frees_flat/ +lemma frees_inv_lifts_ex: âb,f2,L,U. L ⢠ð *â¦U⦠â f2 â + âf,K. â¬*[b, f] L â K â âT. â¬*[f] T â U â + ââf1. f ~â f1 â f2 & K ⢠ð *â¦T⦠â f1. +#b #f2 #L #U #Hf2 #f #K #HLK #T elim (frees_total K T) +/3 width=9 by frees_fwd_coafter, ex2_intro/ +qed-. + +lemma frees_inv_lifts_SO: âb,f,L,U. L ⢠ð *â¦U⦠â f â + âK. â¬*[b, ðâ´1âµ] L â K â âT. â¬*[1] T â U â + K ⢠ð *â¦T⦠â ⫱f. +#b #f #L #U #H #K #HLK #T #HTU elim(frees_inv_lifts_ex ⦠H ⦠HLK ⦠HTU) -b -L -U +#f1 #Hf #Hf1 elim (coafter_inv_nxx ⦠Hf) -Hf +/3 width=5 by frees_eq_repl_back, coafter_isid_inv_sn/ +qed-. + +lemma frees_inv_lifts: âb,f2,L,U. L ⢠ð *â¦U⦠â f2 â + âf,K. â¬*[b, f] L â K â âT. â¬*[f] T â U â + âf1. f ~â f1 â f2 â K ⢠ð *â¦T⦠â f1. +#b #f2 #L #U #H #f #K #HLK #T #HTU #f1 #Hf2 elim (frees_inv_lifts_ex ⦠H ⦠HLK ⦠HTU) -b -L -U +/3 width=7 by frees_eq_repl_back, coafter_inj/ +qed-. + +(* Note: this is used by rex_conf and might be modified *) +lemma frees_inv_drops_next: âf1,L1,T1. L1 ⢠ð *â¦T1⦠â f1 â + âI2,L2,V2,n. â¬*[n] L1 â L2.â{I2}V2 â + âg1. âg1 = ⫱*[n] f1 â + ââg2. L2 ⢠ð *â¦V2⦠â g2 & g2 â g1. +#f1 #L1 #T1 #H elim H -f1 -L1 -T1 +[ #f1 #L1 #s #Hf1 #I2 #L2 #V2 #n #_ #g1 #H1 -I2 -L1 -s + lapply (isid_tls n ⦠Hf1) -Hf1