X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fstatic_2%2Fstatic%2Ffrees_drops.ma;h=67e3e9992b4a1add09474f7de86323a6002dd3b3;hb=eba13527cf74de399b7e5b958901962666d4cd25;hp=215ba6e1aab18d91fed4eba2a6c3dc8f5d3ab263;hpb=98e786e1a6bd7b621e37ba7cd4098d4a0a6f8278;p=helm.git diff --git a/matita/matita/contribs/lambdadelta/static_2/static/frees_drops.ma b/matita/matita/contribs/lambdadelta/static_2/static/frees_drops.ma index 215ba6e1a..67e3e9992 100644 --- a/matita/matita/contribs/lambdadelta/static_2/static/frees_drops.ma +++ b/matita/matita/contribs/lambdadelta/static_2/static/frees_drops.ma @@ -22,7 +22,7 @@ include "static_2/static/frees_fqup.ma". lemma frees_atom_drops: âb,L,i. â©*[b,ðâ¨iâ©] L â â â - âf. ðâªfâ« â L ⢠ð +âª#iâ« â ⫯*[i]âf. + â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 @@ -31,8 +31,8 @@ lemma frees_atom_drops: qed. 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. 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/ @@ -40,8 +40,8 @@ lemma frees_pair_drops: qed. lemma frees_unit_drops: - âf. ðâªfâ« â âI,K,i,L. â©[i] L â K.â¤[I] â - L ⢠ð +âª#iâ« â ⫯*[i] âf. + â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 @@ -50,8 +50,8 @@ lemma frees_unit_drops: qed. lemma frees_lref_pushs: - âf,K,j. K ⢠ð +âª#jâ« â f â - âi,L. â©[i] L â K â L ⢠ð +âª#(i+j)â« â ⫯*[i] f. + â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 @@ -62,10 +62,10 @@ 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. + â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 @@ -86,9 +86,9 @@ qed-. (* Properties with generic slicing for local environments *******************) lemma frees_lifts: - âb,f1,K,T. K ⢠ð +âªTâ« â f1 â + âb,f1,K,T. K ⢠ð +â¨Tâ© â f1 â âf,L. â©*[b,f] L â K â âU. â§*[f] T â U â - âf2. f ~â f1 â f2 â L ⢠ð +âªUâ« â f2. + â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 (pr_coafter_isi_inv_dx ⦠H3 ⦠Hf1) -f1 #Hf2 @@ -145,7 +145,7 @@ qed-. lemma frees_lifts_SO: âb,L,K. â©*[b,ðâ¨1â©] L â K â âT,U. â§[1] T â U â - âf. K ⢠ð +âªTâ« â f â L ⢠ð +âªUâ« â ⫯f. + âf. K ⢠ð +â¨Tâ© â f â L ⢠ð +â¨Uâ© â ⫯f. #b #L #K #HLK #T #U #HTU #f #Hf @(frees_lifts b ⦠Hf ⦠HTU) // (**) (* auto fails *) qed. @@ -153,44 +153,44 @@ qed. (* Forward lemmas with generic slicing for local environments ***************) lemma frees_fwd_coafter: - âb,f2,L,U. L ⢠ð +âªUâ« â f2 â + âb,f2,L,U. L ⢠ð +â¨Uâ© â f2 â âf,K. â©*[b,f] L â K â âT. â§*[f] T â U â - âf1. K ⢠ð +âªTâ« â f1 â f ~â f1 â f2. + âf1. K ⢠ð +â¨Tâ© â f1 â f ~â f1 â f2. /4 width=11 by frees_lifts, frees_mono, pr_coafter_eq_repl_back/ qed-. (* Inversion lemmas with generic slicing for local environments *************) lemma frees_inv_lifts_ex: - âb,f2,L,U. L ⢠ð +âªUâ« â f2 â + âb,f2,L,U. L ⢠ð +â¨Uâ© â f2 â âf,K. â©*[b,f] L â K â âT. â§*[f] T â U â - ââf1. f ~â f1 â f2 & K ⢠ð +âªTâ« â f1. + ââ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 â + âb,f,L,U. L ⢠ð +â¨Uâ© â f â âK. â©*[b,ðâ¨1â©] L â K â âT. â§[1] T â U â - K ⢠ð +âªTâ« â â«°f. + 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 (pr_coafter_inv_next_sn ⦠Hf) -Hf /3 width=5 by frees_eq_repl_back, pr_coafter_isi_inv_sn/ qed-. lemma frees_inv_lifts: - âb,f2,L,U. L ⢠ð +âªUâ« â f2 â + âb,f2,L,U. L ⢠ð +â¨Uâ© â f2 â âf,K. â©*[b,f] L â K â âT. â§*[f] T â U â - âf1. f ~â f1 â f2 â K ⢠ð +âªTâ« â f1. + â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, pr_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 â + âf1,L1,T1. L1 ⢠ð +â¨T1â© â f1 â âI2,L2,V2,i. â©[i] L1 â L2.â[I2]V2 â âg1. âg1 = â«°*[i] f1 â - ââg2. L2 ⢠ð +âªV2â« â g2 & g2 â g1. + ââg2. L2 ⢠ð +â¨V2â© â g2 & g2 â g1. #f1 #L1 #T1 #H elim H -f1 -L1 -T1 [ #f1 #L1 #s #Hf1 #I2 #L2 #V2 #j #_ #g1 #H1 -I2 -L1 -s lapply (pr_isi_tls j ⦠Hf1) -Hf1