X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fstatic_2%2Fstatic%2Ffrees_drops.ma;h=215ba6e1aab18d91fed4eba2a6c3dc8f5d3ab263;hb=98e786e1a6bd7b621e37ba7cd4098d4a0a6f8278;hp=7b4f04950b5d65b11741a5212f9432edeaf49191;hpb=68b4f2490c12139c03760b39895619e63b0f38c9;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 7b4f04950..215ba6e1a 100644 --- a/matita/matita/contribs/lambdadelta/static_2/static/frees_drops.ma +++ b/matita/matita/contribs/lambdadelta/static_2/static/frees_drops.ma @@ -91,18 +91,18 @@ lemma frees_lifts: â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 + lapply (pr_coafter_isi_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 + lapply (pr_coafter_isi_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 + elim (pr_after_pat_des ⦠Hij ⦠Hf) -f #x #_ #Hj -g -i + lapply (pr_pat_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 (pr_isf_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 @@ -112,34 +112,34 @@ lemma frees_lifts: | #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 + lapply (pr_coafter_isi_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 (pr_isf_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 (pr_pat_inv_succ_sn ⦠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 *) + >nplus_succ_sn /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 + lapply (pr_coafter_isi_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 (pr_sor_inv_isf ⦠H1f1) // #Hf1V #H + lapply (pr_isf_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 + elim (pr_sor_coafter_dx_tans ⦠H3 ⦠H1f1) /2 width=5 by pr_coafter_des_ist_isf/ -H3 -H1f1 #f2V #f2T #Hf2V #H + elim (pr_coafter_inv_tl_dx ⦠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 (pr_sor_inv_isf ⦠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/ + elim (pr_sor_coafter_dx_tans ⦠H3 ⦠H1f1) + /3 width=5 by pr_coafter_des_ist_isf, frees_flat/ ] qed-. @@ -156,7 +156,7 @@ 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-. +/4 width=11 by frees_lifts, frees_mono, pr_coafter_eq_repl_back/ qed-. (* Inversion lemmas with generic slicing for local environments *************) @@ -171,10 +171,10 @@ 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. + 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/ +#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: @@ -182,59 +182,59 @@ lemma frees_inv_lifts: â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/ +/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 â âI2,L2,V2,i. â©[i] L1 â L2.â[I2]V2 â - âg1. âg1 = ⫱*[i] f1 â + âg1. âg1 = â«°*[i] f1 â ââ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 (isid_tls j ⦠Hf1) -Hf1