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=0e1ae0e21c115e56f95f077c4c707164e7da37c3;hb=222044da28742b24584549ba86b1805a87def070;hpb=21827c7db90ddb4fd30adec6becd94e201898f9c 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 0e1ae0e21..fe24eadf5 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/static/frees_drops.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/static/frees_drops.ma @@ -20,8 +20,8 @@ include "basic_2/static/frees_fqup.ma". (* Advanced properties ******************************************************) -lemma frees_atom_drops: âb,L,i. â¬*[b, ðâ´iâµ] L â¡ â â - âf. ðâ¦f⦠â L ⢠ð *â¦#i⦠⡠â*[i]⫯f. +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 @@ -29,16 +29,16 @@ lemma frees_atom_drops: âb,L,i. â¬*[b, ðâ´iâµ] L â¡ â â ] qed. -lemma frees_pair_drops: â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_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. +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 @@ -46,16 +46,16 @@ lemma frees_unit_drops: âf. ðâ¦f⦠â âI,K,i,L. â¬*[i] L â¡ K.â¤{I ] qed. (* -lemma frees_sort_pushs: âf,K,s. K ⢠ð *â¦âs⦠⡠f â - âi,L. â¬*[i] L â¡ K â L ⢠ð *â¦âs⦠⡠â*[i] f. +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. +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 @@ -63,8 +63,8 @@ lemma frees_lref_pushs: âf,K,j. K ⢠ð *â¦#j⦠⡠f â ] qed. (* -lemma frees_gref_pushs: âf,K,l. K ⢠ð *â¦Â§l⦠⡠f â - âi,L. â¬*[i] L â¡ K â L ⢠ð *â¦Â§l⦠⡠â*[i] f. +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/ @@ -73,11 +73,11 @@ qed. *) (* Advanced inversion lemmas ************************************************) -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. +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 @@ -97,9 +97,9 @@ 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. +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 @@ -154,41 +154,48 @@ lemma frees_lifts: âb,f1,K,T. K ⢠ð *â¦T⦠⡠f1 â ] 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. +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_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. +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. +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. +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-. -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. +(* 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