X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fstatic_2%2Fstatic%2Ffrees_fqup.ma;h=6868962e64f6782e5a0dacd64b41f796a7408610;hb=98e786e1a6bd7b621e37ba7cd4098d4a0a6f8278;hp=feb74eb263f4fc3d49639e1d98d91c8c9b114005;hpb=a454837a256907d2f83d42ced7be847e10361ea9;p=helm.git diff --git a/matita/matita/contribs/lambdadelta/static_2/static/frees_fqup.ma b/matita/matita/contribs/lambdadelta/static_2/static/frees_fqup.ma index feb74eb26..6868962e6 100644 --- a/matita/matita/contribs/lambdadelta/static_2/static/frees_fqup.ma +++ b/matita/matita/contribs/lambdadelta/static_2/static/frees_fqup.ma @@ -20,7 +20,7 @@ include "static_2/static/lsubf_lsubr.ma". (* Advanced properties ******************************************************) (* Note: this replaces lemma 1400 concluding the "big tree" theorem *) -lemma frees_total: ∀L,T. ∃f. L ⊢ 𝐅+⦃T⦄ ≘ f. +lemma frees_total: ∀L,T. ∃f. L ⊢ 𝐅+❪T❫ ≘ f. #L #T @(fqup_wf_ind_eq (Ⓣ) … (⋆) L T) -L -T #G0 #L0 #T0 #IH #G #L * * [ /3 width=2 by frees_sort, ex_intro/ @@ -38,13 +38,13 @@ lemma frees_total: ∀L,T. ∃f. L ⊢ 𝐅+⦃T⦄ ≘ f. | /3 width=2 by frees_gref, ex_intro/ | #p #I #V #T #HG #HL #HT destruct elim (IH G L V) // #f1 #HV - elim (IH G (L.ⓑ{I}V) T) -IH // #f2 #HT - elim (sor_isfin_ex f1 (⫱f2)) - /3 width=6 by frees_fwd_isfin, frees_bind, isfin_tl, ex_intro/ + elim (IH G (L.ⓑ[I]V) T) -IH // #f2 #HT + elim (pr_sor_isf_bi f1 (⫰f2)) + /3 width=6 by frees_fwd_isfin, frees_bind, pr_isf_tl, ex_intro/ | #I #V #T #HG #HL #HT destruct elim (IH G L V) // #f1 #HV elim (IH G L T) -IH // #f2 #HT - elim (sor_isfin_ex f1 f2) + elim (pr_sor_isf_bi f1 f2) /3 width=6 by frees_fwd_isfin, frees_flat, ex_intro/ ] qed-. @@ -52,81 +52,81 @@ qed-. (* Advanced main properties *************************************************) theorem frees_bind_void: - ∀f1,L,V. L ⊢ 𝐅+⦃V⦄ ≘ f1 → ∀f2,T. L.ⓧ ⊢ 𝐅+⦃T⦄ ≘ f2 → - ∀f. f1 ⋓ ⫱f2 ≘ f → ∀p,I. L ⊢ 𝐅+⦃ⓑ{p,I}V.T⦄ ≘ f. + ∀f1,L,V. L ⊢ 𝐅+❪V❫ ≘ f1 → ∀f2,T. L.ⓧ ⊢ 𝐅+❪T❫ ≘ f2 → + ∀f. f1 ⋓ ⫰f2 ≘ f → ∀p,I. L ⊢ 𝐅+❪ⓑ[p,I]V.T❫ ≘ f. #f1 #L #V #Hf1 #f2 #T #Hf2 #f #Hf #p #I -elim (frees_total (L.ⓑ{I}V) T) #f0 #Hf0 +elim (frees_total (L.ⓑ[I]V) T) #f0 #Hf0 lapply (lsubr_lsubf … Hf2 … Hf0) -Hf2 /2 width=5 by lsubr_unit/ #H02 -elim (pn_split f2) * #g2 #H destruct +elim (pr_map_split_tl f2) * #g2 #H destruct [ elim (lsubf_inv_push2 … H02) -H02 #g0 #Z #Y #H02 #H0 #H destruct lapply (lsubf_inv_refl … H02) -H02 #H02 - lapply (sor_eq_repl_fwd2 … Hf … H02) -g2 #Hf + lapply (pr_sor_eq_repl_fwd_dx … Hf … H02) -g2 #Hf /2 width=5 by frees_bind/ | elim (lsubf_inv_unit2 … H02) -H02 * [ #g0 #Y #_ #_ #H destruct ] #z1 #g0 #z #Z #Y #X #H02 #Hz1 #Hz #H0 #H destruct lapply (lsubf_inv_refl … H02) -H02 #H02 lapply (frees_mono … Hz1 … Hf1) -Hz1 #H1 - lapply (sor_eq_repl_back1 … Hz … H02) -g0 #Hz - lapply (sor_eq_repl_back2 … Hz … H1) -z1 #Hz - lapply (sor_comm … Hz) -Hz #Hz - lapply (sor_mono … f Hz ?) // -Hz #H - lapply (sor_inv_sle_sn … Hf) -Hf #Hf - lapply (frees_eq_repl_back … Hf0 (↑f) ?) /2 width=5 by eq_next/ -z #Hf0 + lapply (pr_sor_eq_repl_back_sn … Hz … H02) -g0 #Hz + lapply (pr_sor_eq_repl_back_dx … Hz … H1) -z1 #Hz + lapply (pr_sor_comm … Hz) -Hz #Hz + lapply (pr_sor_mono … f Hz ?) // -Hz #H + lapply (pr_sor_inv_sle_sn … Hf) -Hf #Hf + lapply (frees_eq_repl_back … Hf0 (↑f) ?) /2 width=5 by pr_eq_next/ -z #Hf0 @(frees_bind … Hf1 Hf0) -Hf1 -Hf0 (**) (* constructor needed *) - /2 width=1 by sor_sle_dx/ + /2 width=1 by pr_sor_sle_dx/ ] qed-. (* Advanced inversion lemmas ************************************************) lemma frees_inv_bind_void: - ∀f,p,I,L,V,T. L ⊢ 𝐅+⦃ⓑ{p,I}V.T⦄ ≘ f → - ∃∃f1,f2. L ⊢ 𝐅+⦃V⦄ ≘ f1 & L.ⓧ ⊢ 𝐅+⦃T⦄ ≘ f2 & f1 ⋓ ⫱f2 ≘ f. + ∀f,p,I,L,V,T. L ⊢ 𝐅+❪ⓑ[p,I]V.T❫ ≘ f → + ∃∃f1,f2. L ⊢ 𝐅+❪V❫ ≘ f1 & L.ⓧ ⊢ 𝐅+❪T❫ ≘ f2 & f1 ⋓ ⫰f2 ≘ f. #f #p #I #L #V #T #H elim (frees_inv_bind … H) -H #f1 #f2 #Hf1 #Hf2 #Hf elim (frees_total (L.ⓧ) T) #f0 #Hf0 lapply (lsubr_lsubf … Hf0 … Hf2) -Hf2 /2 width=5 by lsubr_unit/ #H20 -elim (pn_split f0) * #g0 #H destruct +elim (pr_map_split_tl f0) * #g0 #H destruct [ elim (lsubf_inv_push2 … H20) -H20 #g2 #I #Y #H20 #H2 #H destruct lapply (lsubf_inv_refl … H20) -H20 #H20 - lapply (sor_eq_repl_back2 … Hf … H20) -g2 #Hf + lapply (pr_sor_eq_repl_back_dx … Hf … H20) -g2 #Hf /2 width=5 by ex3_2_intro/ | elim (lsubf_inv_unit2 … H20) -H20 * [ #g2 #Y #_ #_ #H destruct ] #z1 #z0 #g2 #Z #Y #X #H20 #Hz1 #Hg2 #H2 #H destruct lapply (lsubf_inv_refl … H20) -H20 #H0 lapply (frees_mono … Hz1 … Hf1) -Hz1 #H1 - lapply (sor_eq_repl_back1 … Hg2 … H0) -z0 #Hg2 - lapply (sor_eq_repl_back2 … Hg2 … H1) -z1 #Hg2 + lapply (pr_sor_eq_repl_back_sn … Hg2 … H0) -z0 #Hg2 + lapply (pr_sor_eq_repl_back_dx … Hg2 … H1) -z1 #Hg2 @(ex3_2_intro … Hf1 Hf0) -Hf1 -Hf0 (**) (* constructor needed *) - /2 width=3 by sor_comm_23_idem/ + /2 width=3 by pr_sor_comm_23_idem/ ] qed-. lemma frees_ind_void (Q:relation3 …): ( - ∀f,L,s. 𝐈⦃f⦄ → Q L (⋆s) f + ∀f,L,s. 𝐈❪f❫ → Q L (⋆s) f ) → ( - ∀f,i. 𝐈⦃f⦄ → Q (⋆) (#i) (⫯*[i]↑f) + ∀f,i. 𝐈❪f❫ → Q (⋆) (#i) (⫯*[i]↑f) ) → ( ∀f,I,L,V. - L ⊢ 𝐅+⦃V⦄ ≘ f → Q L V f→ Q (L.ⓑ{I}V) (#O) (↑f) + L ⊢ 𝐅+❪V❫ ≘ f → Q L V f→ Q (L.ⓑ[I]V) (#O) (↑f) ) → ( - ∀f,I,L. 𝐈⦃f⦄ → Q (L.ⓤ{I}) (#O) (↑f) + ∀f,I,L. 𝐈❪f❫ → Q (L.ⓤ[I]) (#O) (↑f) ) → ( ∀f,I,L,i. - L ⊢ 𝐅+⦃#i⦄ ≘ f → Q L (#i) f → Q (L.ⓘ{I}) (#(↑i)) (⫯f) + L ⊢ 𝐅+❪#i❫ ≘ f → Q L (#i) f → Q (L.ⓘ[I]) (#(↑i)) (⫯f) ) → ( - ∀f,L,l. 𝐈⦃f⦄ → Q L (§l) f + ∀f,L,l. 𝐈❪f❫ → Q L (§l) f ) → ( ∀f1,f2,f,p,I,L,V,T. - L ⊢ 𝐅+⦃V⦄ ≘ f1 → L.ⓧ ⊢𝐅+⦃T⦄≘ f2 → f1 ⋓ ⫱f2 ≘ f → - Q L V f1 → Q (L.ⓧ) T f2 → Q L (ⓑ{p,I}V.T) f + L ⊢ 𝐅+❪V❫ ≘ f1 → L.ⓧ ⊢𝐅+❪T❫≘ f2 → f1 ⋓ ⫰f2 ≘ f → + Q L V f1 → Q (L.ⓧ) T f2 → Q L (ⓑ[p,I]V.T) f ) → ( ∀f1,f2,f,I,L,V,T. - L ⊢ 𝐅+⦃V⦄ ≘ f1 → L ⊢𝐅+⦃T⦄ ≘ f2 → f1 ⋓ f2 ≘ f → - Q L V f1 → Q L T f2 → Q L (ⓕ{I}V.T) f + L ⊢ 𝐅+❪V❫ ≘ f1 → L ⊢𝐅+❪T❫ ≘ f2 → f1 ⋓ f2 ≘ f → + Q L V f1 → Q L T f2 → Q L (ⓕ[I]V.T) f ) → - ∀L,T,f. L ⊢ 𝐅+⦃T⦄ ≘ f → Q L T f. + ∀L,T,f. L ⊢ 𝐅+❪T❫ ≘ f → Q L T f. #Q #IH1 #IH2 #IH3 #IH4 #IH5 #IH6 #IH7 #IH8 #L #T @(fqup_wf_ind_eq (Ⓕ) … (⋆) L T) -L -T #G0 #L0 #T0 #IH #G #L * * [ #s #HG #HL #HT #f #H destruct -IH