From: Ferruccio Guidi Date: Tue, 5 Oct 2021 22:51:38 +0000 (+0200) Subject: partial commit in static_2 X-Git-Tag: make_still_working~136 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=98e786e1a6bd7b621e37ba7cd4098d4a0a6f8278;p=helm.git partial commit in static_2 propagating the new ground library to static_2 begins --- diff --git a/matita/matita/contribs/lambdadelta/static_2/i_static/rexs_fqup.ma b/matita/matita/contribs/lambdadelta/static_2/i_static/rexs_fqup.ma index 705338db3..1adadac59 100644 --- a/matita/matita/contribs/lambdadelta/static_2/i_static/rexs_fqup.ma +++ b/matita/matita/contribs/lambdadelta/static_2/i_static/rexs_fqup.ma @@ -34,7 +34,7 @@ lemma rexs_tc: ∀R,L1,L2,T,f. 𝐈❪f❫ → TC … (sex cfull (cext2 R) f) L1 L1 ⪤*[R,T] L2. #R #L1 #L2 #T #f #Hf #H elim H -L2 [ elim (frees_total L1 T) | #L elim (frees_total L T) ] -/5 width=7 by sex_sdj, rexs_step_dx, sdj_isid_sn, inj, ex2_intro/ +/5 width=7 by sex_sdj, rexs_step_dx, pr_sdj_isi_sn, inj, ex2_intro/ qed. (* Advanced eliminators *****************************************************) diff --git a/matita/matita/contribs/lambdadelta/static_2/i_static/rexs_lex.ma b/matita/matita/contribs/lambdadelta/static_2/i_static/rexs_lex.ma index fd50b7a6d..39059adfc 100644 --- a/matita/matita/contribs/lambdadelta/static_2/i_static/rexs_lex.ma +++ b/matita/matita/contribs/lambdadelta/static_2/i_static/rexs_lex.ma @@ -48,8 +48,8 @@ lapply (s_rs_transitive_lex_inv_isid … H3R) -H3R #H3R | #L0 #L2 #_ #HL02 * #L * #f0 #Hf0 #HL1 #HL0 lapply (req_rex_trans … HL0 … HL02) -L0 // * #f1 #Hf1 #HL2 elim (sex_sdj_split_sn … ceq_ext … HL2 f0 ?) -HL2 - [ #L0 #HL0 #HL02 |*: /2 width=1 by ext2_refl, sdj_isid_dx/ ] - lapply (sex_sdj … HL0 f1 ?) /2 width=1 by sdj_isid_sn/ #H + [ #L0 #HL0 #HL02 |*: /2 width=1 by ext2_refl, pr_sdj_isi_dx/ ] + lapply (sex_sdj … HL0 f1 ?) /2 width=1 by pr_sdj_isi_sn/ #H elim (frees_sex_conf_fsge … Hf1 … H) // -H2R -H #f2 #Hf2 #Hf21 lapply (sle_sex_trans … HL02 … Hf21) -f1 // #HL02 lapply (sex_co ?? cfull (CTC … (cext2 R)) … HL1) -HL1 /2 width=1 by ext2_inv_tc/ #HL1 diff --git a/matita/matita/contribs/lambdadelta/static_2/notation/functions/uparrow_1_0.ma b/matita/matita/contribs/lambdadelta/static_2/notation/functions/uparrow_1_0.ma new file mode 100644 index 000000000..e4bb638ac --- /dev/null +++ b/matita/matita/contribs/lambdadelta/static_2/notation/functions/uparrow_1_0.ma @@ -0,0 +1,19 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) + +notation "hvbox( ⇡[ term 46 h ] )" + non associative with precedence 46 + for @{ 'UpArrow_1_0 $h }. diff --git a/matita/matita/contribs/lambdadelta/static_2/notation/functions/uparrowstar_2_0.ma b/matita/matita/contribs/lambdadelta/static_2/notation/functions/uparrowstar_2_0.ma new file mode 100644 index 000000000..a4ca8f209 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/static_2/notation/functions/uparrowstar_2_0.ma @@ -0,0 +1,19 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) + +notation "hvbox( ⇡*[ term 46 h, term 46 n ] )" + non associative with precedence 46 + for @{ 'UpArrowStar_2_0 $h $n }. diff --git a/matita/matita/contribs/lambdadelta/static_2/notation/functions/upspoon_2.ma b/matita/matita/contribs/lambdadelta/static_2/notation/functions/upspoon_2.ma deleted file mode 100644 index c04bf2278..000000000 --- a/matita/matita/contribs/lambdadelta/static_2/notation/functions/upspoon_2.ma +++ /dev/null @@ -1,19 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) - -notation "hvbox( ⫯[ term 46 h ] break term 46 s )" - non associative with precedence 46 - for @{ 'UpSpoon $h $s }. diff --git a/matita/matita/contribs/lambdadelta/static_2/relocation/drops.ma b/matita/matita/contribs/lambdadelta/static_2/relocation/drops.ma index 407f8cc4f..b459df118 100644 --- a/matita/matita/contribs/lambdadelta/static_2/relocation/drops.ma +++ b/matita/matita/contribs/lambdadelta/static_2/relocation/drops.ma @@ -26,7 +26,7 @@ include "static_2/relocation/lifts_bind.ma". (* Basic_2A1: includes: drop_atom drop_pair drop_drop drop_skip drop_refl_atom_O2 drop_drop_lt drop_skip_lt *) -inductive drops (b:bool): rtmap → relation lenv ≝ +inductive drops (b:bool): pr_map → relation lenv ≝ | drops_atom: ∀f. (b = Ⓣ → 𝐈❪f❫) → drops b (f) (⋆) (⋆) | drops_drop: ∀f,I,L1,L2. drops b f L1 L2 → drops b (↑f) (L1.ⓘ[I]) L2 | drops_skip: ∀f,I1,I2,L1,L2. @@ -38,7 +38,7 @@ interpretation "generic slicing (local environment)" 'RDropStar b f L1 L2 = (drops b f L1 L2). interpretation "uniform slicing (local environment)" - 'RDrop i L1 L2 = (drops true (uni i) L1 L2). + 'RDrop i L1 L2 = (drops true (pr_uni i) L1 L2). definition d_liftable1: predicate (relation2 lenv term) ≝ λR. ∀K,T. R K T → ∀b,f,L. ⇩*[b,f] L ≘ K → @@ -102,9 +102,9 @@ lemma drops_atom_F: ∀f. ⇩*[Ⓕ,f] ⋆ ≘ ⋆. #f @drops_atom #H destruct qed. -lemma drops_eq_repl_back: ∀b,L1,L2. eq_repl_back … (λf. ⇩*[b,f] L1 ≘ L2). +lemma drops_eq_repl_back: ∀b,L1,L2. pr_eq_repl_back … (λf. ⇩*[b,f] L1 ≘ L2). #b #L1 #L2 #f1 #H elim H -f1 -L1 -L2 -[ /4 width=3 by drops_atom, isid_eq_repl_back/ +[ /4 width=3 by drops_atom, pr_isi_eq_repl_back/ | #f1 #I #L1 #L2 #_ #IH #f2 #H elim (eq_inv_nx … H) -H /3 width=3 by drops_drop/ | #f1 #I1 #I2 #L1 #L2 #_ #HI #IH #f2 #H elim (eq_inv_px … H) -H @@ -112,8 +112,8 @@ lemma drops_eq_repl_back: ∀b,L1,L2. eq_repl_back … (λf. ⇩*[b,f] L1 ≘ L2 ] qed-. -lemma drops_eq_repl_fwd: ∀b,L1,L2. eq_repl_fwd … (λf. ⇩*[b,f] L1 ≘ L2). -#b #L1 #L2 @eq_repl_sym /2 width=3 by drops_eq_repl_back/ (**) (* full auto fails *) +lemma drops_eq_repl_fwd: ∀b,L1,L2. pr_eq_repl_fwd … (λf. ⇩*[b,f] L1 ≘ L2). +#b #L1 #L2 @pr_eq_repl_sym /2 width=3 by drops_eq_repl_back/ (**) (* full auto fails *) qed-. (* Basic_2A1: includes: drop_FT *) @@ -166,8 +166,8 @@ fact drops_inv_drop1_aux: ∀b,f,X,Y. ⇩*[b,f] X ≘ Y → ∀g,I,K. X = K.ⓘ[ ⇩*[b,g] K ≘ Y. #b #f #X #Y * -f -X -Y [ #f #Hf #g #J #K #H destruct -| #f #I #L1 #L2 #HL #g #J #K #H1 #H2 <(injective_next … H2) -g destruct // -| #f #I1 #I2 #L1 #L2 #_ #_ #g #J #K #_ #H2 elim (discr_push_next … H2) +| #f #I #L1 #L2 #HL #g #J #K #H1 #H2 <(eq_inv_pr_next_bi … H2) -g destruct // +| #f #I1 #I2 #L1 #L2 #_ #_ #g #J #K #_ #H2 elim (eq_inv_pr_push_next … H2) ] qed-. @@ -180,8 +180,8 @@ fact drops_inv_skip1_aux: ∀b,f,X,Y. ⇩*[b,f] X ≘ Y → ∀g,I1,K1. X = K1. ∃∃I2,K2. ⇩*[b,g] K1 ≘ K2 & ⇧*[g] I2 ≘ I1 & Y = K2.ⓘ[I2]. #b #f #X #Y * -f -X -Y [ #f #Hf #g #J1 #K1 #H destruct -| #f #I #L1 #L2 #_ #g #J1 #K1 #_ #H2 elim (discr_next_push … H2) -| #f #I1 #I2 #L1 #L2 #HL #HI #g #J1 #K1 #H1 #H2 <(injective_push … H2) -g destruct +| #f #I #L1 #L2 #_ #g #J1 #K1 #_ #H2 elim (eq_inv_pr_next_push … H2) +| #f #I1 #I2 #L1 #L2 #HL #HI #g #J1 #K1 #H1 #H2 <(eq_inv_pr_push_bi … H2) -g destruct /2 width=5 by ex3_2_intro/ ] qed-. @@ -196,8 +196,8 @@ fact drops_inv_skip2_aux: ∀b,f,X,Y. ⇩*[b,f] X ≘ Y → ∀g,I2,K2. Y = K2. ∃∃I1,K1. ⇩*[b,g] K1 ≘ K2 & ⇧*[g] I2 ≘ I1 & X = K1.ⓘ[I1]. #b #f #X #Y * -f -X -Y [ #f #Hf #g #J2 #K2 #H destruct -| #f #I #L1 #L2 #_ #g #J2 #K2 #_ #H2 elim (discr_next_push … H2) -| #f #I1 #I2 #L1 #L2 #HL #HV #g #J2 #K2 #H1 #H2 <(injective_push … H2) -g destruct +| #f #I #L1 #L2 #_ #g #J2 #K2 #_ #H2 elim (eq_inv_pr_next_push … H2) +| #f #I1 #I2 #L1 #L2 #HL #HV #g #J2 #K2 #H1 #H2 <(eq_inv_pr_push_bi … H2) -g destruct /2 width=5 by ex3_2_intro/ ] qed-. @@ -215,9 +215,9 @@ fact drops_fwd_drop2_aux: ∀b,f2,X,Y. ⇩*[b,f2] X ≘ Y → ∀I,K. Y = K.ⓘ[ #b #f2 #X #Y #H elim H -f2 -X -Y [ #f2 #Hf2 #J #K #H destruct | #f2 #I #L1 #L2 #_ #IHL #J #K #H elim (IHL … H) -IHL - /3 width=7 by after_next, ex3_2_intro, drops_drop/ + /3 width=7 by pr_after_next, ex3_2_intro, drops_drop/ | #f2 #I1 #I2 #L1 #L2 #HL #_ #_ #J #K #H destruct - lapply (after_isid_dx 𝐢 … f2) /3 width=9 by after_push, ex3_2_intro, drops_drop/ + lapply (pr_after_isi_dx 𝐢 … f2) /3 width=9 by pr_after_push, ex3_2_intro, drops_drop/ ] qed-. @@ -230,7 +230,7 @@ lemma drops_fwd_drop2: ∀b,f2,I,X,K. ⇩*[b,f2] X ≘ K.ⓘ[I] → (* Basic_2A1: includes: drop_refl *) lemma drops_refl: ∀b,L,f. 𝐈❪f❫ → ⇩*[b,f] L ≘ L. #b #L elim L -L /2 width=1 by drops_atom/ -#L #I #IHL #f #Hf elim (isid_inv_gen … Hf) -Hf +#L #I #IHL #f #Hf elim (pr_isi_inv_gen … Hf) -Hf /3 width=1 by drops_skip, liftsb_refl/ qed. @@ -240,23 +240,23 @@ qed. (* Basic_2A1: includes: drop_inv_O2 *) lemma drops_fwd_isid: ∀b,f,L1,L2. ⇩*[b,f] L1 ≘ L2 → 𝐈❪f❫ → L1 = L2. #b #f #L1 #L2 #H elim H -f -L1 -L2 // -[ #f #I #L1 #L2 #_ #_ #H elim (isid_inv_next … H) // -| /5 width=5 by isid_inv_push, liftsb_fwd_isid, eq_f2, sym_eq/ +[ #f #I #L1 #L2 #_ #_ #H elim (pr_isi_inv_next … H) // +| /5 width=5 by pr_isi_inv_push, liftsb_fwd_isid, eq_f2, sym_eq/ ] qed-. lemma drops_after_fwd_drop2: ∀b,f2,I,X,K. ⇩*[b,f2] X ≘ K.ⓘ[I] → ∀f1,f. 𝐈❪f1❫ → f2 ⊚ ↑f1 ≘ f → ⇩*[b,f] X ≘ K. #b #f2 #I #X #K #H #f1 #f #Hf1 #Hf elim (drops_fwd_drop2 … H) -H -#g1 #g #Hg1 #Hg #HK lapply (after_mono_eq … Hg … Hf ??) -Hg -Hf -/3 width=5 by drops_eq_repl_back, isid_inv_eq_repl, eq_next/ +#g1 #g #Hg1 #Hg #HK lapply (pr_after_mono_eq … Hg … Hf ??) -Hg -Hf +/3 width=5 by drops_eq_repl_back, pr_isi_inv_eq_repl, pr_eq_next/ qed-. (* Forward lemmas with test for finite colength *****************************) lemma drops_fwd_isfin: ∀f,L1,L2. ⇩*[Ⓣ,f] L1 ≘ L2 → 𝐅❪f❫. #f #L1 #L2 #H elim H -f -L1 -L2 -/3 width=1 by isfin_next, isfin_push, isfin_isid/ +/3 width=1 by pr_isf_next, pr_isf_push, pr_isf_isi/ qed-. (* Properties with test for uniformity **************************************) @@ -274,8 +274,8 @@ lemma drops_inv_isuni: ∀f,L1,L2. ⇩*[Ⓣ,f] L1 ≘ L2 → 𝐔❪f❫ → ∃∃g,I,K. ⇩*[Ⓣ,g] K ≘ L2 & 𝐔❪g❫ & L1 = K.ⓘ[I] & f = ↑g. #f #L1 #L2 * -f -L1 -L2 [ /4 width=1 by or_introl, conj/ -| /4 width=7 by isuni_inv_next, ex4_3_intro, or_intror/ -| /7 width=6 by drops_fwd_isid, liftsb_fwd_isid, isuni_inv_push, isid_push, or_introl, conj, eq_f2, sym_eq/ +| /4 width=7 by pr_isu_inv_next, ex4_3_intro, or_intror/ +| /7 width=6 by drops_fwd_isid, liftsb_fwd_isid, pr_isu_inv_push, pr_isi_push, or_introl, conj, eq_f2, sym_eq/ ] qed-. @@ -283,10 +283,10 @@ qed-. lemma drops_inv_bind1_isuni: ∀b,f,I,K,L2. 𝐔❪f❫ → ⇩*[b,f] K.ⓘ[I] ≘ L2 → (𝐈❪f❫ ∧ L2 = K.ⓘ[I]) ∨ ∃∃g. 𝐔❪g❫ & ⇩*[b,g] K ≘ L2 & f = ↑g. -#b #f #I #K #L2 #Hf #H elim (isuni_split … Hf) -Hf * #g #Hg #H0 destruct +#b #f #I #K #L2 #Hf #H elim (pr_isu_split … Hf) -Hf * #g #Hg #H0 destruct [ lapply (drops_inv_skip1 … H) -H * #Z #Y #HY #HZ #H destruct <(drops_fwd_isid … HY Hg) -Y >(liftsb_fwd_isid … HZ Hg) -Z - /4 width=3 by isid_push, or_introl, conj/ + /4 width=3 by pr_isi_push, or_introl, conj/ | lapply (drops_inv_drop1 … H) -H /3 width=4 by ex3_intro, or_intror/ ] qed-. @@ -306,8 +306,8 @@ qed-. lemma drops_inv_bind2_isuni_next: ∀b,f,I,K,L1. 𝐔❪f❫ → ⇩*[b,↑f] L1 ≘ K.ⓘ[I] → ∃∃I1,K1. ⇩*[b,f] K1 ≘ K.ⓘ[I] & L1 = K1.ⓘ[I1]. -#b #f #I #K #L1 #Hf #H elim (drops_inv_bind2_isuni … H) -H /2 width=3 by isuni_next/ -Hf * -[ #H elim (isid_inv_next … H) -H // +#b #f #I #K #L1 #Hf #H elim (drops_inv_bind2_isuni … H) -H /2 width=3 by pr_isu_next/ -Hf * +[ #H elim (pr_isi_inv_next … H) -H // | /2 width=4 by ex2_2_intro/ ] qed-. @@ -317,11 +317,11 @@ fact drops_inv_TF_aux: ∀f,L1,L2. ⇩*[Ⓕ,f] L1 ≘ L2 → 𝐔❪f❫ → #f #L1 #L2 #H elim H -f -L1 -L2 [ #f #_ #_ #J #K #H destruct | #f #I #L1 #L2 #_ #IH #Hf #J #K #H destruct - /4 width=3 by drops_drop, isuni_inv_next/ + /4 width=3 by drops_drop, pr_isu_inv_next/ | #f #I1 #I2 #L1 #L2 #HL12 #HI21 #_ #Hf #J #K #H destruct - lapply (isuni_inv_push … Hf ??) -Hf [1,2: // ] #Hf + lapply (pr_isu_inv_push … Hf ??) -Hf [1,2: // ] #Hf <(drops_fwd_isid … HL12) -K // <(liftsb_fwd_isid … HI21) -I1 - /3 width=3 by drops_refl, isid_push/ + /3 width=3 by drops_refl, pr_isi_push/ ] qed-. @@ -344,18 +344,18 @@ qed-. (* Basic_1: was: drop_S *) (* Basic_2A1: was: drop_fwd_drop2 *) lemma drops_isuni_fwd_drop2: ∀b,f,I,X,K. 𝐔❪f❫ → ⇩*[b,f] X ≘ K.ⓘ[I] → ⇩*[b,↑f] X ≘ K. -/3 width=7 by drops_after_fwd_drop2, after_isid_isuni/ qed-. +/3 width=7 by drops_after_fwd_drop2, pr_after_isu_isi_next/ qed-. (* Inversion lemmas with uniform relocations ********************************) lemma drops_inv_atom2: ∀b,L,f. ⇩*[b,f] L ≘ ⋆ → ∃∃n,f1. ⇩*[b,𝐔❨n❩] L ≘ ⋆ & 𝐔❨n❩ ⊚ f1 ≘ f. #b #L elim L -L -[ /3 width=4 by drops_atom, after_isid_sn, ex2_2_intro/ -| #L #I #IH #f #H elim (pn_split f) * #g #H0 destruct +[ /3 width=4 by drops_atom, pr_after_isi_sn, ex2_2_intro/ +| #L #I #IH #f #H elim (pr_map_split_tl f) * #g #H0 destruct [ elim (drops_inv_skip1 … H) -H #J #K #_ #_ #H destruct | lapply (drops_inv_drop1 … H) -H #HL - elim (IH … HL) -IH -HL /3 width=8 by drops_drop, after_next, ex2_2_intro/ + elim (IH … HL) -IH -HL /3 width=8 by drops_drop, pr_after_next, ex2_2_intro/ ] ] qed-. @@ -363,7 +363,7 @@ qed-. lemma drops_inv_succ: ∀L1,L2,i. ⇩[↑i] L1 ≘ L2 → ∃∃I,K. ⇩[i] K ≘ L2 & L1 = K.ⓘ[I]. #L1 #L2 #i #H elim (drops_inv_isuni … H) -H // * -[ #H elim (isid_inv_next … H) -H // +[ #H elim (pr_isi_inv_next … H) -H // | /2 width=4 by ex2_2_intro/ ] qed-. @@ -383,18 +383,18 @@ lemma drops_split_trans: ∀b,f,L1,L2. ⇩*[b,f] L1 ≘ L2 → ∀f1,f2. f1 ⊚ #b #f #L1 #L2 #H elim H -f -L1 -L2 [ #f #H0f #f1 #f2 #Hf #Hf1 @(ex2_intro … (⋆)) @drops_atom #H lapply (H0f H) -b - #H elim (after_inv_isid3 … Hf H) -f // -| #f #I #L1 #L2 #HL12 #IHL12 #f1 #f2 #Hf #Hf1 elim (after_inv_xxn … Hf) -Hf [1,3: * |*: // ] + #H elim (pr_after_inv_isi … Hf H) -f // +| #f #I #L1 #L2 #HL12 #IHL12 #f1 #f2 #Hf #Hf1 elim (pr_after_inv_next … Hf) -Hf [1,3: * |*: // ] [ #g1 #g2 #Hf #H1 #H2 destruct - lapply (isuni_inv_push … Hf1 ??) -Hf1 [1,2: // ] #Hg1 + lapply (pr_isu_inv_push … Hf1 ??) -Hf1 [1,2: // ] #Hg1 elim (IHL12 … Hf) -f - /4 width=5 by drops_drop, drops_skip, liftsb_refl, isuni_isid, ex2_intro/ + /4 width=5 by drops_drop, drops_skip, liftsb_refl, pr_isu_isi, ex2_intro/ | #g1 #Hf #H destruct elim (IHL12 … Hf) -f - /3 width=5 by ex2_intro, drops_drop, isuni_inv_next/ + /3 width=5 by ex2_intro, drops_drop, pr_isu_inv_next/ ] -| #f #I1 #I2 #L1 #L2 #_ #HI21 #IHL12 #f1 #f2 #Hf #Hf1 elim (after_inv_xxp … Hf) -Hf [2,3: // ] +| #f #I1 #I2 #L1 #L2 #_ #HI21 #IHL12 #f1 #f2 #Hf #Hf1 elim (pr_after_inv_push … Hf) -Hf [2,3: // ] #g1 #g2 #Hf #H1 #H2 destruct elim (liftsb_split_trans … HI21 … Hf) -HI21 - elim (IHL12 … Hf) -f /3 width=5 by ex2_intro, drops_skip, isuni_fwd_push/ + elim (IHL12 … Hf) -f /3 width=5 by ex2_intro, drops_skip, pr_isu_fwd_push/ ] qed-. @@ -402,15 +402,15 @@ lemma drops_split_div: ∀b,f1,L1,L. ⇩*[b,f1] L1 ≘ L → ∀f2,f. f1 ⊚ f2 ∃∃L2. ⇩*[Ⓕ,f2] L ≘ L2 & ⇩*[Ⓕ,f] L1 ≘ L2. #b #f1 #L1 #L #H elim H -f1 -L1 -L [ #f1 #Hf1 #f2 #f #Hf #Hf2 @(ex2_intro … (⋆)) @drops_atom #H destruct -| #f1 #I #L1 #L #HL1 #IH #f2 #f #Hf #Hf2 elim (after_inv_nxx … Hf) -Hf [2,3: // ] +| #f1 #I #L1 #L #HL1 #IH #f2 #f #Hf #Hf2 elim (pr_after_inv_next_sn … Hf) -Hf [2,3: // ] #g #Hg #H destruct elim (IH … Hg) -IH -Hg /3 width=5 by drops_drop, ex2_intro/ | #f1 #I1 #I #L1 #L #HL1 #HI1 #IH #f2 #f #Hf #Hf2 - elim (after_inv_pxx … Hf) -Hf [1,3: * |*: // ] + elim (pr_after_inv_push_sn … Hf) -Hf [1,3: * |*: // ] #g2 #g #Hg #H2 #H0 destruct - [ lapply (isuni_inv_push … Hf2 ??) -Hf2 [1,2: // ] #Hg2 -IH - lapply (after_isid_inv_dx … Hg … Hg2) -Hg #Hg - /5 width=7 by drops_eq_repl_back, drops_F, drops_refl, drops_skip, liftsb_eq_repl_back, isid_push, ex2_intro/ - | lapply (isuni_inv_next … Hf2 ??) -Hf2 [1,2: // ] #Hg2 -HL1 -HI1 + [ lapply (pr_isu_inv_push … Hf2 ??) -Hf2 [1,2: // ] #Hg2 -IH + lapply (pr_after_isi_inv_dx … Hg … Hg2) -Hg #Hg + /5 width=7 by drops_eq_repl_back, drops_F, drops_refl, drops_skip, liftsb_eq_repl_back, pr_isi_push, ex2_intro/ + | lapply (pr_isu_inv_next … Hf2 ??) -Hf2 [1,2: // ] #Hg2 -HL1 -HI1 elim (IH … Hg) -f1 /3 width=3 by drops_drop, ex2_intro/ ] ] @@ -421,12 +421,12 @@ qed-. lemma drops_tls_at: ∀f,i1,i2. @❪i1,f❫ ≘ i2 → ∀b,L1,L2. ⇩*[b,⫰*[i2]f] L1 ≘ L2 → ⇩*[b,⫯⫰*[↑i2]f] L1 ≘ L2. -/3 width=3 by drops_eq_repl_fwd, at_inv_tls/ qed-. +/3 width=3 by drops_eq_repl_fwd, pr_pat_inv_succ_dx_tls/ qed-. lemma drops_split_trans_bind2: ∀b,f,I,L,K0. ⇩*[b,f] L ≘ K0.ⓘ[I] → ∀i. @❪O,f❫ ≘ i → ∃∃J,K. ⇩[i]L ≘ K.ⓘ[J] & ⇩*[b,⫰*[↑i]f] K ≘ K0 & ⇧*[⫰*[↑i]f] I ≘ J. #b #f #I #L #K0 #H #i #Hf -elim (drops_split_trans … H) -H [ |5: @(after_uni_dx … Hf) |2,3: skip ] /2 width=1 by after_isid_dx/ #Y #HLY #H +elim (drops_split_trans … H) -H [ |5: @(pr_after_nat_uni … Hf) |2,3: skip ] /2 width=1 by pr_after_isi_dx/ #Y #HLY #H lapply (drops_tls_at … Hf … H) -H #H elim (drops_inv_skip2 … H) -H #J #K #HK0 #HIJ #H destruct /3 width=5 by drops_inv_gen, ex3_2_intro/ diff --git a/matita/matita/contribs/lambdadelta/static_2/relocation/drops_drops.ma b/matita/matita/contribs/lambdadelta/static_2/relocation/drops_drops.ma index ab924e9b8..7b8bebb69 100644 --- a/matita/matita/contribs/lambdadelta/static_2/relocation/drops_drops.ma +++ b/matita/matita/contribs/lambdadelta/static_2/relocation/drops_drops.ma @@ -26,10 +26,10 @@ theorem drops_conf: ∀b1,f1,L1,L. ⇩*[b1,f1] L1 ≘ L → #b1 #f1 #L1 #L #H elim H -f1 -L1 -L [ #f1 #_ #b2 #f #L2 #HL2 #f2 #Hf12 elim (drops_inv_atom1 … HL2) -b1 -HL2 #H #Hf destruct @drops_atom - #H elim (after_inv_isid3 … Hf12) -Hf12 /2 width=1 by/ -| #f1 #I1 #K1 #K #_ #IH #b2 #f #L2 #HL2 #f2 #Hf elim (after_inv_nxx … Hf) -Hf [2,3: // ] + #H elim (pr_after_inv_isi … Hf12) -Hf12 /2 width=1 by/ +| #f1 #I1 #K1 #K #_ #IH #b2 #f #L2 #HL2 #f2 #Hf elim (pr_after_inv_next_sn … Hf) -Hf [2,3: // ] #g #Hg #H destruct /3 width=3 by drops_inv_drop1/ -| #f1 #I1 #I #K1 #K #_ #HI1 #IH #b2 #f #L2 #HL2 #f2 #Hf elim (after_inv_pxx … Hf) -Hf [1,3: * |*:// ] +| #f1 #I1 #I #K1 #K #_ #HI1 #IH #b2 #f #L2 #HL2 #f2 #Hf elim (pr_after_inv_push_sn … Hf) -Hf [1,3: * |*:// ] #g2 #g #Hf #H1 #H2 destruct [ elim (drops_inv_skip1 … HL2) -HL2 /3 width=6 by drops_skip, liftsb_div3/ | /4 width=3 by drops_inv_drop1, drops_drop/ @@ -47,11 +47,11 @@ theorem drops_trans: ∀b1,f1,L1,L. ⇩*[b1,f1] L1 ≘ L → #b1 #f1 #L1 #L #H elim H -f1 -L1 -L [ #f1 #Hf1 #b2 #f2 #L2 #HL2 #f #Hf elim (drops_inv_atom1 … HL2) -HL2 #H #Hf2 destruct @drops_atom #H elim (andb_inv_true_dx … H) -H - #H1 #H2 lapply (after_isid_inv_sn … Hf ?) -Hf - /3 width=3 by isid_eq_repl_back/ -| #f1 #I1 #K1 #K #_ #IH #b2 #f2 #L2 #HL2 #f #Hf elim (after_inv_nxx … Hf) -Hf + #H1 #H2 lapply (pr_after_isi_inv_sn … Hf ?) -Hf + /3 width=3 by pr_isi_eq_repl_back/ +| #f1 #I1 #K1 #K #_ #IH #b2 #f2 #L2 #HL2 #f #Hf elim (pr_after_inv_next_sn … Hf) -Hf /3 width=3 by drops_drop/ -| #f1 #I1 #I #K1 #K #_ #HI1 #IH #b2 #f2 #L2 #HL2 #f #Hf elim (after_inv_pxx … Hf) -Hf [1,3: * |*: // ] +| #f1 #I1 #I #K1 #K #_ #HI1 #IH #b2 #f2 #L2 #HL2 #f #Hf elim (pr_after_inv_push_sn … Hf) -Hf [1,3: * |*: // ] #g2 #g #Hg #H1 #H2 destruct [ elim (drops_inv_skip1 … HL2) -HL2 /3 width=6 by drops_skip, liftsb_trans/ | /4 width=3 by drops_inv_drop1, drops_drop/ @@ -64,20 +64,20 @@ theorem drops_conf_div_isuni: 𝐔❪f1❫ → 𝐔❪f2❫ → f1 ≡ f2. #f1 #L #K #H elim H -f1 -L -K [ #f1 #Hf1 #f2 #Hf2 elim (drops_inv_atom1 … Hf2) -Hf2 - /3 width=1 by isid_inv_eq_repl/ -| #f1 #I #L #K #Hf1 #IH #f2 elim (pn_split f2) * + /3 width=1 by pr_isi_inv_eq_repl/ +| #f1 #I #L #K #Hf1 #IH #f2 elim (pr_map_split_tl f2) * #g2 #H2 #Hf2 #HU1 #HU2 destruct [ elim (drops_inv_skip1 … Hf2) -IH -HU1 -Hf2 #Y2 #X2 #HY2 #_ #H destruct - lapply (drops_fwd_isid … HY2 ?) -HY2 /2 width=3 by isuni_inv_push/ -HU2 + lapply (drops_fwd_isid … HY2 ?) -HY2 /2 width=3 by pr_isu_inv_push/ -HU2 #H destruct elim (drops_inv_x_bind_xy … Hf1) - | /4 width=5 by drops_inv_drop1, isuni_inv_next, eq_next/ + | /4 width=5 by drops_inv_drop1, pr_isu_inv_next, pr_eq_next/ ] -| #f1 #I1 #I2 #L #K #Hf1 #_ #IH #f2 elim (pn_split f2) * +| #f1 #I1 #I2 #L #K #Hf1 #_ #IH #f2 elim (pr_map_split_tl f2) * #g2 #H2 #Hf2 #HU1 #HU2 destruct [ elim (drops_inv_skip1 … Hf2) -Hf2 #Y2 #X2 #HY2 #_ #H destruct -Hf1 - /4 width=5 by isuni_fwd_push, eq_push/ + /4 width=5 by pr_isu_fwd_push, pr_eq_push/ | lapply (drops_inv_drop1 … Hf2) -Hf2 -IH -HU2 #Hg2 - lapply (drops_fwd_isid … Hf1 ?) -Hf1 /2 width=3 by isuni_inv_push/ -HU1 + lapply (drops_fwd_isid … Hf1 ?) -Hf1 /2 width=3 by pr_isu_inv_push/ -HU1 #H destruct elim (drops_inv_x_bind_xy … Hg2) ] ] @@ -88,7 +88,7 @@ qed-. (* Basic_2A1: includes: drop_mono *) lemma drops_mono: ∀b1,f,L,L1. ⇩*[b1,f] L ≘ L1 → ∀b2,L2. ⇩*[b2,f] L ≘ L2 → L1 = L2. -#b1 #f #L #L1 lapply (after_isid_dx 𝐢 … f) +#b1 #f #L #L1 lapply (pr_after_isi_dx 𝐢 … f) /3 width=8 by drops_conf, drops_fwd_isid/ qed-. @@ -135,7 +135,7 @@ lemma drops_conf_div_bind_isuni: #f1 #f2 #I1 #I2 #L #K #Hf1 #Hf2 #HU1 #HU2 lapply (drops_isuni_fwd_drop2 … Hf1) // #H1 lapply (drops_isuni_fwd_drop2 … Hf2) // #H2 -lapply (drops_conf_div_isuni … H1 … H2 ??) /2 width=3 by isuni_next/ -H1 -H2 -HU1 -HU2 #H +lapply (drops_conf_div_isuni … H1 … H2 ??) /2 width=3 by pr_isu_next/ -H1 -H2 -HU1 -HU2 #H lapply (eq_inv_nn … H ????) -H [5: |*: // ] #H12 lapply (drops_eq_repl_back … Hf1 … H12) -Hf1 #H0 lapply (drops_mono … H0 … Hf2) -L #H diff --git a/matita/matita/contribs/lambdadelta/static_2/relocation/drops_length.ma b/matita/matita/contribs/lambdadelta/static_2/relocation/drops_length.ma index fe6b2ade8..49c4f0206 100644 --- a/matita/matita/contribs/lambdadelta/static_2/relocation/drops_length.ma +++ b/matita/matita/contribs/lambdadelta/static_2/relocation/drops_length.ma @@ -21,7 +21,7 @@ include "static_2/relocation/drops.ma". (* Basic_2A1: includes: drop_fwd_length_le4 *) lemma drops_fwd_length_le4: ∀b,f,L1,L2. ⇩*[b,f] L1 ≘ L2 → |L2| ≤ |L1|. -#b #f #L1 #L2 #H elim H -f -L1 -L2 /2 width=1 by le_S, le_S_S/ +#b #f #L1 #L2 #H elim H -f -L1 -L2 /2 width=1 by nle_succ_dx, nle_succ_bi/ qed-. (* Basic_2A1: includes: drop_fwd_length_eq1 *) @@ -46,9 +46,9 @@ qed-. lemma drops_fwd_fcla: ∀f,L1,L2. ⇩*[Ⓣ,f] L1 ≘ L2 → ∃∃n. 𝐂❪f❫ ≘ n & |L1| = |L2| + n. #f #L1 #L2 #H elim H -f -L1 -L2 -[ /4 width=3 by fcla_isid, ex2_intro/ -| #f #I #L1 #L2 #_ * >length_bind /3 width=3 by fcla_next, ex2_intro, eq_f/ -| #f #I1 #I2 #L1 #L2 #_ #_ * >length_bind >length_bind /3 width=3 by fcla_push, ex2_intro/ +[ /4 width=3 by pr_fcla_isi, ex2_intro/ +| #f #I #L1 #L2 #_ * >length_bind /3 width=3 by pr_fcla_next, ex2_intro, eq_f/ +| #f #I1 #I2 #L1 #L2 #_ #_ * >length_bind >length_bind /3 width=3 by pr_fcla_push, ex2_intro/ ] qed-. @@ -56,7 +56,7 @@ qed-. lemma drops_fcla_fwd: ∀f,L1,L2,n. ⇩*[Ⓣ,f] L1 ≘ L2 → 𝐂❪f❫ ≘ n → |L1| = |L2| + n. #f #l1 #l2 #n #Hf #Hn elim (drops_fwd_fcla … Hf) -Hf -#k #Hm #H <(fcla_mono … Hm … Hn) -f // +#k #Hm #H <(pr_fcla_mono … Hm … Hn) -f // qed-. lemma drops_fwd_fcla_le2: ∀f,L1,L2. ⇩*[Ⓣ,f] L1 ≘ L2 → @@ -68,13 +68,13 @@ qed-. lemma drops_fcla_fwd_le2: ∀f,L1,L2,n. ⇩*[Ⓣ,f] L1 ≘ L2 → 𝐂❪f❫ ≘ n → n ≤ |L1|. #f #L1 #L2 #n #H #Hn elim (drops_fwd_fcla_le2 … H) -H -#k #Hm #H <(fcla_mono … Hm … Hn) -f // +#k #Hm #H <(pr_fcla_mono … Hm … Hn) -f // qed-. lemma drops_fwd_fcla_lt2: ∀f,L1,I2,K2. ⇩*[Ⓣ,f] L1 ≘ K2.ⓘ[I2] → ∃∃n. 𝐂❪f❫ ≘ n & n < |L1|. #f #L1 #I2 #K2 #H elim (drops_fwd_fcla … H) -H -#n #Hf #H >H -L1 /3 width=3 by le_S_S, ex2_intro/ +#n #Hf #H >H -L1 /3 width=3 by nle_succ_bi, ex2_intro/ qed-. (* Basic_2A1: includes: drop_fwd_length_lt2 *) @@ -82,20 +82,20 @@ lemma drops_fcla_fwd_lt2: ∀f,L1,I2,K2,n. ⇩*[Ⓣ,f] L1 ≘ K2.ⓘ[I2] → 𝐂❪f❫ ≘ n → n < |L1|. #f #L1 #I2 #K2 #n #H #Hn elim (drops_fwd_fcla_lt2 … H) -H -#k #Hm #H <(fcla_mono … Hm … Hn) -f // +#k #Hm #H <(pr_fcla_mono … Hm … Hn) -f // qed-. (* Basic_2A1: includes: drop_fwd_length_lt4 *) lemma drops_fcla_fwd_lt4: ∀f,L1,L2,n. ⇩*[Ⓣ,f] L1 ≘ L2 → 𝐂❪f❫ ≘ n → 0 < n → |L2| < |L1|. #f #L1 #L2 #n #H #Hf #Hn lapply (drops_fcla_fwd … H Hf) -f -/2 width=1 by lt_minus_to_plus_r/ qed-. +/2 width=1 by nlt_inv_minus_dx/ qed-. (* Basic_2A1: includes: drop_inv_length_eq *) lemma drops_inv_length_eq: ∀f,L1,L2. ⇩*[Ⓣ,f] L1 ≘ L2 → |L1| = |L2| → 𝐈❪f❫. #f #L1 #L2 #H #HL12 elim (drops_fwd_fcla … H) -H -#n #Hn H1 -L1 elim (drops_fwd_fcla … HLK2) -HLK2 #n2 #Hn2 #H2 >H2 -L2 -<(fcla_mono … Hn2 … Hn1) -f // +<(pr_fcla_mono … Hn2 … Hn1) -f // qed-. theorem drops_conf_div: ∀f1,f2,L1,L2. ⇩*[Ⓣ,f1] L1 ≘ L2 → ⇩*[Ⓣ,f2] L1 ≘ L2 → @@ -112,7 +112,7 @@ theorem drops_conf_div: ∀f1,f2,L1,L2. ⇩*[Ⓣ,f1] L1 ≘ L2 → ⇩*[Ⓣ,f2] #f1 #f2 #L1 #L2 #H1 #H2 elim (drops_fwd_fcla … H1) -H1 #n1 #Hf1 #H1 elim (drops_fwd_fcla … H2) -H2 #n2 #Hf2 >H1 -L1 #H -lapply (injective_plus_r … H) -L2 #H destruct /2 width=3 by ex2_intro/ +lapply (eq_inv_nplus_bi_sn … H) -L2 #H destruct /2 width=3 by ex2_intro/ qed-. theorem drops_conf_div_fcla: ∀f1,f2,L1,L2,n1,n2. @@ -121,5 +121,5 @@ theorem drops_conf_div_fcla: ∀f1,f2,L1,L2,n1,n2. #f1 #f2 #L1 #L2 #n1 #n2 #Hf1 #Hf2 #Hn1 #Hn2 lapply (drops_fcla_fwd … Hf1 Hn1) -f1 #H1 lapply (drops_fcla_fwd … Hf2 Hn2) -f2 >H1 -L1 -/2 width=1 by injective_plus_r/ +/2 width=1 by eq_inv_nplus_bi_sn/ qed-. diff --git a/matita/matita/contribs/lambdadelta/static_2/relocation/drops_lex.ma b/matita/matita/contribs/lambdadelta/static_2/relocation/drops_lex.ma index 1201b75fa..4e261897d 100644 --- a/matita/matita/contribs/lambdadelta/static_2/relocation/drops_lex.ma +++ b/matita/matita/contribs/lambdadelta/static_2/relocation/drops_lex.ma @@ -37,7 +37,7 @@ lemma lex_liftable_dedropable_sn (R): c_reflexive … R → d_liftable2_sn … lifts R → dedropable_sn R. #R #H1R #H2R #b #f #L1 #K1 #HLK1 #K2 * #f1 #Hf1 #HK12 elim (sex_liftable_co_dedropable_sn … HLK1 … HK12) -K1 -/3 width=6 by cext2_d_liftable2_sn, cfull_lift_sn, ext2_refl, coafter_isid_dx, ex3_intro, ex2_intro/ +/3 width=6 by cext2_d_liftable2_sn, cfull_lift_sn, ext2_refl, pr_coafter_isi_dx, ex3_intro, ex2_intro/ qed-. (* Inversion lemmas with generic extension **********************************) @@ -46,14 +46,14 @@ qed-. lemma lex_dropable_sn (R): dropable_sn R. #R #b #f #L1 #K1 #HLK1 #H1f #L2 * #f2 #Hf2 #HL12 elim (sex_co_dropable_sn … HLK1 … HL12) -L1 -/3 width=3 by coafter_isid_dx, ex2_intro/ +/3 width=3 by pr_coafter_isi_dx, ex2_intro/ qed-. (* Basic_2A1: was: lpx_sn_dropable *) lemma lex_dropable_dx (R): dropable_dx R. #R #L1 #L2 * #f2 #Hf2 #HL12 #b #f #K2 #HLK2 #Hf elim (sex_co_dropable_dx … HL12 … HLK2) -L2 -/3 width=5 by coafter_isid_dx, ex2_intro/ +/3 width=5 by pr_coafter_isi_dx, ex2_intro/ qed-. (* Basic_2A1: includes: lpx_sn_drop_conf *) @@ -65,7 +65,7 @@ elim (sex_drops_conf_push … HL12 … HLK1 Hf f2) -L1 -Hf [ #Z2 #K2 #HLK2 #HK12 #H elim (ext2_inv_pair_sn … H) -H #V2 #HV12 #H destruct /3 width=5 by ex3_2_intro, ex2_intro/ -| /3 width=3 by coafter_isid_dx, isid_push/ +| /3 width=3 by pr_coafter_isi_dx, pr_isi_push/ ] qed-. @@ -78,6 +78,6 @@ elim (sex_drops_trans_push … HL12 … HLK2 Hf f2) -L2 -Hf [ #Z1 #K1 #HLK1 #HK12 #H elim (ext2_inv_pair_dx … H) -H #V1 #HV12 #H destruct /3 width=5 by ex3_2_intro, ex2_intro/ -| /3 width=3 by coafter_isid_dx, isid_push/ +| /3 width=3 by pr_coafter_isi_dx, pr_isi_push/ ] qed-. diff --git a/matita/matita/contribs/lambdadelta/static_2/relocation/drops_sex.ma b/matita/matita/contribs/lambdadelta/static_2/relocation/drops_sex.ma index aeff28cee..18017d88a 100644 --- a/matita/matita/contribs/lambdadelta/static_2/relocation/drops_sex.ma +++ b/matita/matita/contribs/lambdadelta/static_2/relocation/drops_sex.ma @@ -26,19 +26,19 @@ lemma sex_co_dropable_sn (RN) (RP): [ #f #Hf #_ #f2 #X #H #f1 #Hf2 >(sex_inv_atom1 … H) -X /4 width=3 by sex_atom, drops_atom, ex2_intro/ | #f #I1 #L1 #K1 #_ #IH #Hf #f2 #X #H #f1 #Hf2 - elim (coafter_inv_nxx … Hf2) -Hf2 [2,3: // ] #g2 #Hg2 #H2 destruct + elim (pr_coafter_inv_next_sn … Hf2) -Hf2 [2,3: // ] #g2 #Hg2 #H2 destruct elim (sex_inv_push1 … H) -H #I2 #L2 #HL12 #HI12 #H destruct elim (IH … HL12 … Hg2) -g2 - /3 width=3 by isuni_inv_next, drops_drop, ex2_intro/ + /3 width=3 by pr_isu_inv_next, drops_drop, ex2_intro/ | #f #I1 #J1 #L1 #K1 #HLK #HJI1 #IH #Hf #f2 #X #H #f1 #Hf2 - lapply (isuni_inv_push … Hf ??) -Hf [3: |*: // ] #Hf + lapply (pr_isu_inv_push … Hf ??) -Hf [3: |*: // ] #Hf lapply (drops_fwd_isid … HLK … Hf) -HLK #H0 destruct lapply (liftsb_fwd_isid … HJI1 … Hf) -HJI1 #H0 destruct - elim (coafter_inv_pxx … Hf2) -Hf2 [1,3:* |*: // ] #g1 #g2 #Hg2 #H1 #H2 destruct + elim (pr_coafter_inv_push_sn … Hf2) -Hf2 [1,3:* |*: // ] #g1 #g2 #Hg2 #H1 #H2 destruct [ elim (sex_inv_push1 … H) | elim (sex_inv_next1 … H) ] -H #I2 #L2 #HL12 #HI12 #H destruct - elim (IH … HL12 … Hg2) -g2 -IH /2 width=1 by isuni_isid/ #K2 #HK12 #HLK2 + elim (IH … HL12 … Hg2) -g2 -IH /2 width=1 by pr_isu_isi/ #K2 #HK12 #HLK2 lapply (drops_fwd_isid … HLK2 … Hf) -HLK2 #H0 destruct - /4 width=3 by drops_refl, sex_next, sex_push, isid_push, ex2_intro/ + /4 width=3 by drops_refl, sex_next, sex_push, pr_isi_push, ex2_intro/ ] qed-. @@ -49,13 +49,13 @@ lemma sex_liftable_co_dedropable_bi (RN) (RP): f ~⊚ f1 ≘ f2 → L1 ⪤[RN,RP,f2] L2. #RN #RP #HRN #HRP #f2 #L1 #L2 #H elim H -f2 -L1 -L2 // #g2 #I1 #I2 #L1 #L2 #HL12 #HI12 #IH #f1 #Y1 #Y2 #HK12 #b #f #HY1 #HY2 #H -[ elim (coafter_inv_xxn … H) [ |*: // ] -H #g #g1 #Hg2 #H1 #H2 destruct +[ elim (pr_coafter_inv_next … H) [ |*: // ] -H #g #g1 #Hg2 #H1 #H2 destruct elim (drops_inv_skip1 … HY1) -HY1 #J1 #K1 #HLK1 #HJI1 #H destruct elim (drops_inv_skip1 … HY2) -HY2 #J2 #K2 #HLK2 #HJI2 #H destruct elim (sex_inv_next … HK12) -HK12 #HK12 #HJ12 elim (HRN … HJ12 … HLK1 … HJI1) -HJ12 -HJI1 #Z #Hz >(liftsb_mono … Hz … HJI2) -Z /3 width=9 by sex_next/ -| elim (coafter_inv_xxp … H) [1,2: |*: // ] -H * +| elim (pr_coafter_inv_push … H) [1,2: |*: // ] -H * [ #g #g1 #Hg2 #H1 #H2 destruct elim (drops_inv_skip1 … HY1) -HY1 #J1 #K1 #HLK1 #HJI1 #H destruct elim (drops_inv_skip1 … HY2) -HY2 #J2 #K2 #HLK2 #HJI2 #H destruct @@ -78,11 +78,11 @@ lemma sex_liftable_co_dedropable_sn (RN) (RP): [ #f #Hf #X #f1 #H #f2 #Hf2 >(sex_inv_atom1 … H) -X /4 width=4 by drops_atom, sex_atom, ex3_intro/ | #f #I1 #L1 #K1 #_ #IHLK1 #K2 #f1 #HK12 #f2 #Hf2 - elim (coafter_inv_nxx … Hf2) -Hf2 [2,3: // ] #g2 #Hg2 #H destruct + elim (pr_coafter_inv_next_sn … Hf2) -Hf2 [2,3: // ] #g2 #Hg2 #H destruct elim (IHLK1 … HK12 … Hg2) -K1 /3 width=6 by drops_drop, sex_next, sex_push, ex3_intro/ | #f #I1 #J1 #L1 #K1 #HLK1 #HJI1 #IHLK1 #X #f1 #H #f2 #Hf2 - elim (coafter_inv_pxx … Hf2) -Hf2 [1,3: * |*: // ] #g1 #g2 #Hg2 #H1 #H2 destruct + elim (pr_coafter_inv_push_sn … Hf2) -Hf2 [1,3: * |*: // ] #g1 #g2 #Hg2 #H1 #H2 destruct [ elim (sex_inv_push1 … H) | elim (sex_inv_next1 … H) ] -H #J2 #K2 #HK12 #HJ12 #H destruct [ elim (H2RP … HJ12 … HLK1 … HJI1) | elim (H2RN … HJ12 … HLK1 … HJI1) ] -J1 elim (IHLK1 … HK12 … Hg2) -K1 @@ -98,18 +98,18 @@ fact sex_dropable_dx_aux (RN) (RP): [ #f #Hf #_ #f2 #X #H #f1 #Hf2 lapply (sex_inv_atom2 … H) -H #H destruct /4 width=3 by sex_atom, drops_atom, ex2_intro/ | #f #I2 #L2 #K2 #_ #IH #Hf #f2 #X #HX #f1 #Hf2 - elim (coafter_inv_nxx … Hf2) -Hf2 [2,3: // ] #g2 #Hg2 #H destruct + elim (pr_coafter_inv_next_sn … Hf2) -Hf2 [2,3: // ] #g2 #Hg2 #H destruct elim (sex_inv_push2 … HX) -HX #I1 #L1 #HL12 #HI12 #H destruct elim (IH … HL12 … Hg2) -L2 -I2 -g2 - /3 width=3 by drops_drop, isuni_inv_next, ex2_intro/ + /3 width=3 by drops_drop, pr_isu_inv_next, ex2_intro/ | #f #I2 #J2 #L2 #K2 #_ #HJI2 #IH #Hf #f2 #X #HX #f1 #Hf2 - elim (coafter_inv_pxx … Hf2) -Hf2 [1,3: * |*: // ] #g1 #g2 #Hg2 #H1 #H2 destruct + elim (pr_coafter_inv_push_sn … Hf2) -Hf2 [1,3: * |*: // ] #g1 #g2 #Hg2 #H1 #H2 destruct [ elim (sex_inv_push2 … HX) | elim (sex_inv_next2 … HX) ] -HX #I1 #L1 #HL12 #HI12 #H destruct - elim (IH … HL12 … Hg2) -L2 -g2 /2 width=3 by isuni_fwd_push/ #K1 #HLK1 #HK12 - lapply (isuni_inv_push … Hf ??) -Hf [3,6: |*: // ] #Hf + elim (IH … HL12 … Hg2) -L2 -g2 /2 width=3 by pr_isu_fwd_push/ #K1 #HLK1 #HK12 + lapply (pr_isu_inv_push … Hf ??) -Hf [3,6: |*: // ] #Hf lapply (liftsb_fwd_isid … HJI2 … Hf) #H destruct -HJI2 lapply (drops_fwd_isid … HLK1 … Hf) #H destruct -HLK1 - /4 width=5 by sex_next, sex_push, drops_refl, isid_push, ex2_intro/ + /4 width=5 by sex_next, sex_push, drops_refl, pr_isi_push, ex2_intro/ ] qed-. @@ -205,16 +205,16 @@ lemma sex_sdj_split_dx (R1) (R2) (RP): [ #f1 #_ #L2 #H #f2 #_ lapply (sex_inv_atom1 … H) -H #H destruct /2 width=3 by sex_atom, ex2_intro/ -| #K1 #I1 #IH #f1 elim (pn_split f1) * #g1 #H destruct +| #K1 #I1 #IH #f1 elim (pr_map_split_tl f1) * #g1 #H destruct #HR #L2 #H #f2 #Hf [ elim (sex_inv_push1 … H) -H #I2 #K2 #HK12 #HI12 #H destruct - elim (sdj_inv_px … Hf ??) -Hf [1,3: * |*: // ] #g2 #Hg #H destruct + elim (pr_sdj_inv_push_sn … Hf ??) -Hf [1,3: * |*: // ] #g2 #Hg #H destruct elim (IH … HK12 … Hg) -IH -HK12 -Hg [1,3: /3 width=5 by sex_next, sex_push, ex2_intro/ |2,4: /3 width=3 by drops_drop/ ] | elim (sex_inv_next1 … H) -H #I2 #K2 #HK12 #HI12 #H destruct - elim (sdj_inv_nx … Hf ??) -Hf [|*: // ] #g2 #Hg #H destruct + elim (pr_sdj_inv_next_sn … Hf ??) -Hf [|*: // ] #g2 #Hg #H destruct elim (IH … HK12 … Hg) -IH -HK12 -Hg [ /5 width=11 by sex_next, sex_push, drops_refl, ex2_intro/ | /3 width=3 by drops_drop/ diff --git a/matita/matita/contribs/lambdadelta/static_2/relocation/drops_weight.ma b/matita/matita/contribs/lambdadelta/static_2/relocation/drops_weight.ma index 975b01523..97b730cc8 100644 --- a/matita/matita/contribs/lambdadelta/static_2/relocation/drops_weight.ma +++ b/matita/matita/contribs/lambdadelta/static_2/relocation/drops_weight.ma @@ -23,9 +23,9 @@ include "static_2/relocation/drops.ma". (* Basic_2A1: includes: drop_fwd_lw *) lemma drops_fwd_lw: ∀b,f,L1,L2. ⇩*[b,f] L1 ≘ L2 → ♯❨L2❩ ≤ ♯❨L1❩. #b #f #L1 #L2 #H elim H -f -L1 -L2 // -[ /2 width=3 by transitive_le/ +[ /2 width=3 by nle_trans/ | #f #I1 #I2 #L1 #L2 #_ #HI21 #IHL12 normalize - >(liftsb_fwd_bw … HI21) -HI21 /2 width=1 by monotonic_le_plus_l/ + >(liftsb_fwd_bw … HI21) -HI21 /2 width=1 by nle_plus_bi_dx/ ] qed-. @@ -34,9 +34,9 @@ lemma drops_fwd_lw_lt: ∀f,L1,L2. ⇩*[Ⓣ,f] L1 ≘ L2 → (𝐈❪f❫ → ⊥) → ♯❨L2❩ < ♯❨L1❩. #f #L1 #L2 #H elim H -f -L1 -L2 [ #f #Hf #Hnf elim Hnf -Hnf /2 width=1 by/ -| /3 width=3 by drops_fwd_lw, le_to_lt_to_lt/ +| /3 width=3 by drops_fwd_lw, nle_nlt_trans/ | #f #I1 #I2 #L1 #L2 #_ #HI21 #IHL12 #H normalize in ⊢ (?%%); - >(liftsb_fwd_bw … HI21) -I2 /5 width=3 by isid_push, monotonic_lt_plus_l/ + >(liftsb_fwd_bw … HI21) -I2 /5 width=3 by pr_isi_push, nlt_plus_bi_dx/ ] qed-. @@ -45,12 +45,12 @@ qed-. (* Basic_2A1: includes: drop_fwd_rfw *) lemma drops_bind2_fwd_rfw: ∀b,f,I,L,K,V. ⇩*[b,f] L ≘ K.ⓑ[I]V → ∀T. ♯❨K,V❩ < ♯❨L,T❩. #b #f #I #L #K #V #HLK lapply (drops_fwd_lw … HLK) -HLK -normalize in ⊢ (%→?→?%%); /3 width=3 by le_to_lt_to_lt, monotonic_lt_plus_r/ +normalize in ⊢ (%→?→?%%); /3 width=3 by nle_nlt_trans, nlt_plus_bi_sn/ qed-. (* Advanced inversion lemma *************************************************) lemma drops_inv_x_bind_xy: ∀b,f,I,L. ⇩*[b,f] L ≘ L.ⓘ[I] → ⊥. #b #f #I #L #H lapply (drops_fwd_lw … H) -b -f -/2 width=4 by lt_le_false/ (**) (* full auto is a bit slow: 19s *) +/2 width=4 by nlt_ge_false/ (**) (* full auto is a bit slow: 19s *) qed-. diff --git a/matita/matita/contribs/lambdadelta/static_2/relocation/lex.ma b/matita/matita/contribs/lambdadelta/static_2/relocation/lex.ma index 2c3e5548c..02ba4bedc 100644 --- a/matita/matita/contribs/lambdadelta/static_2/relocation/lex.ma +++ b/matita/matita/contribs/lambdadelta/static_2/relocation/lex.ma @@ -44,7 +44,7 @@ lemma lex_atom (R): ⋆ ⪤[R] ⋆. lemma lex_bind (R): ∀I1,I2,K1,K2. K1 ⪤[R] K2 → cext2 R K1 I1 I2 → K1.ⓘ[I1] ⪤[R] K2.ⓘ[I2]. #R #I1 #I2 #K1 #K2 * #f #Hf #HK12 #HI12 -/3 width=3 by sex_push, isid_push, ex2_intro/ +/3 width=3 by sex_push, pr_isi_push, ex2_intro/ qed. (* Basic_2A1: was: lpx_sn_refl *) @@ -80,7 +80,7 @@ qed-. lemma lex_inv_bind_sn (R): ∀I1,L2,K1. K1.ⓘ[I1] ⪤[R] L2 → ∃∃I2,K2. K1 ⪤[R] K2 & cext2 R K1 I1 I2 & L2 = K2.ⓘ[I2]. #R #I1 #L2 #K1 * #f #Hf #H -lapply (sex_eq_repl_fwd … H (⫯f) ?) -H /2 width=1 by eq_push_inv_isid/ #H +lapply (sex_eq_repl_fwd … H (⫯f) ?) -H /2 width=1 by pr_isi_inv_eq_push/ #H elim (sex_inv_push1 … H) -H #I2 #K2 #HK12 #HI12 #H destruct /3 width=5 by ex2_intro, ex3_2_intro/ qed-. @@ -93,7 +93,7 @@ qed-. lemma lex_inv_bind_dx (R): ∀I2,L1,K2. L1 ⪤[R] K2.ⓘ[I2] → ∃∃I1,K1. K1 ⪤[R] K2 & cext2 R K1 I1 I2 & L1 = K1.ⓘ[I1]. #R #I2 #L1 #K2 * #f #Hf #H -lapply (sex_eq_repl_fwd … H (⫯f) ?) -H /2 width=1 by eq_push_inv_isid/ #H +lapply (sex_eq_repl_fwd … H (⫯f) ?) -H /2 width=1 by pr_isi_inv_eq_push/ #H elim (sex_inv_push2 … H) -H #I1 #K1 #HK12 #HI12 #H destruct /3 width=5 by ex3_2_intro, ex2_intro/ qed-. @@ -154,8 +154,8 @@ lemma lex_ind (R) (Q:relation2 …): ∀L1,L2. L1 ⪤[R] L2 → Q L1 L2. #R #Q #IH1 #IH2 #IH3 #L1 #L2 * #f @pull_2 #H elim H -f -L1 -L2 // #f #I1 #I2 #K1 #K2 @pull_4 #H -[ elim (isid_inv_next … H) -| lapply (isid_inv_push … H ??) +[ elim (pr_isi_inv_next … H) +| lapply (pr_isi_inv_push … H ??) ] -H [5:|*: // ] #Hf @pull_2 #H elim H -H /3 width=3 by ex2_intro/ qed-. diff --git a/matita/matita/contribs/lambdadelta/static_2/relocation/lex_tc.ma b/matita/matita/contribs/lambdadelta/static_2/relocation/lex_tc.ma index 2f86bf51c..51039cd8d 100644 --- a/matita/matita/contribs/lambdadelta/static_2/relocation/lex_tc.ma +++ b/matita/matita/contribs/lambdadelta/static_2/relocation/lex_tc.ma @@ -47,7 +47,7 @@ lemma lex_CTC (R): s_rs_transitive … R (λ_. lex R) → TC … (lex R) ⊆ lex (CTC … R). #R #HR #L1 #L2 #HL12 lapply (monotonic_TC … (sex cfull (cext2 R) 𝐢) … HL12) -HL12 -[ #L1 #L2 * /3 width=3 by sex_eq_repl_fwd, eq_id_inv_isid/ +[ #L1 #L2 * /3 width=3 by sex_eq_repl_fwd, pr_isi_inv_eq_id/ | /5 width=9 by s_rs_transitive_lex_inv_isid, sex_tc_dx, sex_co, ext2_tc, ex2_intro/ ] qed-. diff --git a/matita/matita/contribs/lambdadelta/static_2/relocation/lifts.ma b/matita/matita/contribs/lambdadelta/static_2/relocation/lifts.ma index 2dceb17d0..f019c66d6 100644 --- a/matita/matita/contribs/lambdadelta/static_2/relocation/lifts.ma +++ b/matita/matita/contribs/lambdadelta/static_2/relocation/lifts.ma @@ -23,7 +23,7 @@ include "static_2/syntax/term.ma". lift_sort lift_lref_lt lift_lref_ge lift_bind lift_flat lifts_nil lifts_cons *) -inductive lifts: rtmap → relation term ≝ +inductive lifts: pr_map → relation term ≝ | lifts_sort: ∀f,s. lifts f (⋆s) (⋆s) | lifts_lref: ∀f,i1,i2. @❪i1,f❫ ≘ i2 → lifts f (#i1) (#i2) | lifts_gref: ∀f,l. lifts f (§l) (§l) @@ -39,7 +39,7 @@ interpretation "generic relocation (term)" 'RLiftStar f T1 T2 = (lifts f T1 T2). interpretation "uniform relocation (term)" - 'RLift i T1 T2 = (lifts (uni i) T1 T2). + 'RLift i T1 T2 = (lifts (pr_uni i) T1 T2). definition liftable2_sn: predicate (relation term) ≝ λR. ∀T1,T2. R T1 T2 → ∀f,U1. ⇧*[f] T1 ≘ U1 → @@ -292,7 +292,7 @@ lemma lifts_inv_push_zero_sn (f): ∀X. ⇧*[⫯f]#0 ≘ X → #0 = X. #f #X #H elim (lifts_inv_lref1 … H) -H #i #Hi #H destruct -lapply (at_inv_ppx … Hi ???) -Hi // +lapply (pr_pat_inv_unit_push … Hi ???) -Hi // qed-. lemma lifts_inv_push_succ_sn (f) (i1): @@ -300,30 +300,30 @@ lemma lifts_inv_push_succ_sn (f) (i1): ∃∃i2. ⇧*[f]#i1 ≘ #i2 & #(↑i2) = X. #f #i1 #X #H elim (lifts_inv_lref1 … H) -H #j #Hij #H destruct -elim (at_inv_npx … Hij) -Hij [|*: // ] #i2 #Hi12 #H destruct +elim (pr_pat_inv_succ_push … Hij) -Hij [|*: // ] #i2 #Hi12 #H destruct /3 width=3 by lifts_lref, ex2_intro/ qed-. (* Inversion lemmas with uniform relocations ********************************) lemma lifts_inv_lref1_uni: ∀l,Y,i. ⇧[l] #i ≘ Y → Y = #(l+i). -#l #Y #i1 #H elim (lifts_inv_lref1 … H) -H /4 width=4 by at_mono, eq_f/ +#l #Y #i1 #H elim (lifts_inv_lref1 … H) -H /4 width=4 by fr2_nat_mono, eq_f/ qed-. lemma lifts_inv_lref2_uni: ∀l,X,i2. ⇧[l] X ≘ #i2 → ∃∃i1. X = #i1 & i2 = l + i1. #l #X #i2 #H elim (lifts_inv_lref2 … H) -H -/3 width=3 by at_inv_uni, ex2_intro/ +/3 width=3 by pr_pat_inv_uni, ex2_intro/ qed-. lemma lifts_inv_lref2_uni_ge: ∀l,X,i. ⇧[l] X ≘ #(l + i) → X = #i. #l #X #i2 #H elim (lifts_inv_lref2_uni … H) -H -#i1 #H1 #H2 destruct /4 width=2 by injective_plus_r, eq_f, sym_eq/ +#i1 #H1 #H2 destruct /4 width=2 by eq_inv_nplus_bi_sn, eq_f, sym_eq/ qed-. lemma lifts_inv_lref2_uni_lt: ∀l,X,i. ⇧[l] X ≘ #i → i < l → ⊥. #l #X #i2 #H elim (lifts_inv_lref2_uni … H) -H -#i1 #_ #H1 #H2 destruct /2 width=4 by lt_le_false/ +#i1 #_ #H1 #H2 destruct /2 width=4 by nlt_ge_false/ qed-. (* Basic forward lemmas *****************************************************) @@ -331,7 +331,7 @@ qed-. (* Basic_2A1: includes: lift_inv_O2 *) lemma lifts_fwd_isid: ∀f,T1,T2. ⇧*[f] T1 ≘ T2 → 𝐈❪f❫ → T1 = T2. #f #T1 #T2 #H elim H -f -T1 -T2 -/4 width=3 by isid_inv_at_mono, isid_push, eq_f2, eq_f/ +/4 width=3 by pr_isi_pat_des, pr_isi_push, eq_f2, eq_f/ qed-. (* Basic_2A1: includes: lift_fwd_pair1 *) @@ -364,20 +364,20 @@ lemma deliftable2_sn_dx (R): symmetric … R → deliftable2_sn R → deliftable elim (H1R … U1 … HTU2) -H1R /3 width=3 by ex2_intro/ qed-. -lemma lifts_eq_repl_back: ∀T1,T2. eq_repl_back … (λf. ⇧*[f] T1 ≘ T2). +lemma lifts_eq_repl_back: ∀T1,T2. pr_eq_repl_back … (λf. ⇧*[f] T1 ≘ T2). #T1 #T2 #f1 #H elim H -T1 -T2 -f1 -/4 width=5 by lifts_flat, lifts_bind, lifts_lref, at_eq_repl_back, eq_push/ +/4 width=5 by lifts_flat, lifts_bind, lifts_lref, pr_pat_eq_repl_back, pr_eq_push/ qed-. -lemma lifts_eq_repl_fwd: ∀T1,T2. eq_repl_fwd … (λf. ⇧*[f] T1 ≘ T2). -#T1 #T2 @eq_repl_sym /2 width=3 by lifts_eq_repl_back/ (**) (* full auto fails *) +lemma lifts_eq_repl_fwd: ∀T1,T2. pr_eq_repl_fwd … (λf. ⇧*[f] T1 ≘ T2). +#T1 #T2 @pr_eq_repl_sym /2 width=3 by lifts_eq_repl_back/ (**) (* full auto fails *) qed-. (* Basic_1: includes: lift_r *) (* Basic_2A1: includes: lift_refl *) lemma lifts_refl: ∀T,f. 𝐈❪f❫ → ⇧*[f] T ≘ T. #T elim T -T * -/4 width=3 by lifts_flat, lifts_bind, lifts_lref, isid_inv_at, isid_push/ +/4 width=3 by lifts_flat, lifts_bind, lifts_lref, pr_isi_inv_pat, pr_isi_push/ qed. (* Basic_2A1: includes: lift_total *) @@ -397,7 +397,7 @@ lemma lifts_push_zero (f): ⇧*[⫯f]#0 ≘ #0. lemma lifts_push_lref (f) (i1) (i2): ⇧*[f]#i1 ≘ #i2 → ⇧*[⫯f]#(↑i1) ≘ #(↑i2). #f1 #i1 #i2 #H elim (lifts_inv_lref1 … H) -H #j #Hij #H destruct -/3 width=7 by lifts_lref, at_push/ +/3 width=7 by lifts_lref, pr_pat_push/ qed. lemma lifts_lref_uni: ∀l,i. ⇧[l] #i ≘ #(l+i). @@ -411,7 +411,7 @@ lemma lifts_split_trans: ∀f,T1,T2. ⇧*[f] T1 ≘ T2 → ∃∃T. ⇧*[f1] T1 ≘ T & ⇧*[f2] T ≘ T2. #f #T1 #T2 #H elim H -f -T1 -T2 [ /3 width=3 by lifts_sort, ex2_intro/ -| #f #i1 #i2 #Hi #f1 #f2 #Ht elim (after_at_fwd … Hi … Ht) -Hi -Ht +| #f #i1 #i2 #Hi #f1 #f2 #Ht elim (pr_after_pat_des … Hi … Ht) -Hi -Ht /3 width=3 by lifts_lref, ex2_intro/ | /3 width=3 by lifts_gref, ex2_intro/ | #f #p #I #V1 #V2 #T1 #T2 #_ #_ #IHV #IHT #f1 #f2 #Ht @@ -429,7 +429,7 @@ lemma lifts_split_div: ∀f1,T1,T2. ⇧*[f1] T1 ≘ T2 → ∃∃T. ⇧*[f2] T2 ≘ T & ⇧*[f] T1 ≘ T. #f1 #T1 #T2 #H elim H -f1 -T1 -T2 [ /3 width=3 by lifts_sort, ex2_intro/ -| #f1 #i1 #i2 #Hi #f2 #f #Ht elim (after_at1_fwd … Hi … Ht) -Hi -Ht +| #f1 #i1 #i2 #Hi #f2 #f #Ht elim (pr_after_des_ist_pat … Hi … Ht) -Hi -Ht /3 width=3 by lifts_lref, ex2_intro/ | /3 width=3 by lifts_gref, ex2_intro/ | #f1 #p #I #V1 #V2 #T1 #T2 #_ #_ #IHV #IHT #f2 #f #Ht @@ -446,7 +446,7 @@ qed-. lemma is_lifts_dec: ∀T2,f. Decidable (∃T1. ⇧*[f] T1 ≘ T2). #T1 elim T1 -T1 [ * [1,3: /3 width=2 by lifts_sort, lifts_gref, ex_intro, or_introl/ ] - #i2 #f elim (is_at_dec f i2) // + #i2 #f elim (is_pr_pat_dec f i2) // [ * /4 width=3 by lifts_lref, ex_intro, or_introl/ | #H @or_intror * #X #HX elim (lifts_inv_lref2 … HX) -HX diff --git a/matita/matita/contribs/lambdadelta/static_2/relocation/lifts_basic.ma b/matita/matita/contribs/lambdadelta/static_2/relocation/lifts_basic.ma index d6dc490e0..2eefef1fc 100644 --- a/matita/matita/contribs/lambdadelta/static_2/relocation/lifts_basic.ma +++ b/matita/matita/contribs/lambdadelta/static_2/relocation/lifts_basic.ma @@ -24,13 +24,13 @@ interpretation "basic relocation (term)" (* Properties with basic relocation *****************************************) lemma lifts_lref_lt (m,n,i): i < m → ⇧[m,n] #i ≘ #i. -/3 width=1 by lifts_lref, at_basic_lt/ qed. +/3 width=1 by lifts_lref, pr_pat_basic_lt/ qed. lemma lifts_lref_ge (m,n,i): m ≤ i → ⇧[m,n] #i ≘ #(n+i). -/3 width=1 by lifts_lref, at_basic_ge/ qed. +/3 width=1 by lifts_lref, pr_pat_basic_ge/ qed. lemma lifts_lref_ge_minus (m,n,i): n+m ≤ i → ⇧[m,n] #(i-n) ≘ #i. #m #n #i #Hi ->(plus_minus_m_m i n) in ⊢ (???%); -/3 width=2 by lifts_lref_ge, le_plus_to_minus_l, le_plus_b/ +>(nplus_minus_sn_refl_sn i n) in ⊢ (???%); +/3 width=2 by lifts_lref_ge, nle_minus_dx_dx, nle_inv_plus_sn_dx/ qed. diff --git a/matita/matita/contribs/lambdadelta/static_2/relocation/lifts_bind.ma b/matita/matita/contribs/lambdadelta/static_2/relocation/lifts_bind.ma index 925baceae..3b45f26c3 100644 --- a/matita/matita/contribs/lambdadelta/static_2/relocation/lifts_bind.ma +++ b/matita/matita/contribs/lambdadelta/static_2/relocation/lifts_bind.ma @@ -17,14 +17,14 @@ include "static_2/relocation/lifts.ma". (* GENERIC RELOCATION FOR BINDERS *******************************************) -definition liftsb: rtmap → relation bind ≝ +definition liftsb: pr_map → relation bind ≝ λf. ext2 (lifts f). interpretation "generic relocation (binder for local environments)" 'RLiftStar f I1 I2 = (liftsb f I1 I2). interpretation "uniform relocation (binder for local environments)" - 'RLift i I1 I2 = (liftsb (uni i) I1 I2). + 'RLift i I1 I2 = (liftsb (pr_uni i) I1 I2). (* Basic_inversion lemmas **************************************************) @@ -48,7 +48,7 @@ lemma liftsb_inv_pair_dx (f): (* Basic properties *********************************************************) -lemma liftsb_eq_repl_back: ∀I1,I2. eq_repl_back … (λf. ⇧*[f] I1 ≘ I2). +lemma liftsb_eq_repl_back: ∀I1,I2. pr_eq_repl_back … (λf. ⇧*[f] I1 ≘ I2). #I1 #I2 #f1 * -I1 -I2 /3 width=3 by lifts_eq_repl_back, ext2_pair/ qed-. diff --git a/matita/matita/contribs/lambdadelta/static_2/relocation/lifts_lifts.ma b/matita/matita/contribs/lambdadelta/static_2/relocation/lifts_lifts.ma index 3f78beb36..406436b9f 100644 --- a/matita/matita/contribs/lambdadelta/static_2/relocation/lifts_lifts.ma +++ b/matita/matita/contribs/lambdadelta/static_2/relocation/lifts_lifts.ma @@ -21,7 +21,7 @@ include "static_2/relocation/lifts.ma". (* Basic_1: includes: lift_gen_lift *) (* Basic_2A1: includes: lift_div_le lift_div_be *) theorem lifts_div4: ∀f2,Tf,T. ⇧*[f2] Tf ≘ T → ∀g2,Tg. ⇧*[g2] Tg ≘ T → - ∀f1,g1. H_at_div f2 g2 f1 g1 → + ∀f1,g1. H_pr_pat_div f2 g2 f1 g1 → ∃∃T0. ⇧*[f1] T0 ≘ Tf & ⇧*[g1] T0 ≘ Tg. #f2 #Tf #T #H elim H -f2 -Tf -T [ #f2 #s #g2 #Tg #H #f1 #g1 #_ @@ -36,7 +36,7 @@ theorem lifts_div4: ∀f2,Tf,T. ⇧*[f2] Tf ≘ T → ∀g2,Tg. ⇧*[g2] Tg ≘ | #f2 #p #I #Vf #V #Tf #T #_ #_ #IHV #IHT #g2 #X #H #f1 #g1 #H0 elim (lifts_inv_bind2 … H) -H #Vg #Tg #HVg #HTg #H destruct elim (IHV … HVg … H0) -IHV -HVg - elim (IHT … HTg) -IHT -HTg [ |*: /2 width=8 by at_div_pp/ ] + elim (IHT … HTg) -IHT -HTg [ |*: /2 width=8 by pr_pat_div_push_bi/ ] /3 width=5 by lifts_bind, ex2_intro/ | #f2 #I #Vf #V #Tf #T #_ #_ #IHV #IHT #g2 #X #H #f1 #g1 #H0 elim (lifts_inv_flat2 … H) -H #Vg #Tg #HVg #HTg #H destruct @@ -49,14 +49,14 @@ qed-. lemma lifts_div4_one: ∀f,Tf,T. ⇧*[⫯f] Tf ≘ T → ∀T1. ⇧[1] T1 ≘ T → ∃∃T0. ⇧[1] T0 ≘ Tf & ⇧*[f] T0 ≘ T1. -/4 width=6 by lifts_div4, at_div_id_dx, at_div_pn/ qed-. +/4 width=6 by lifts_div4, pr_pat_div_id_dx, pr_pat_div_push_next/ qed-. theorem lifts_div3: ∀f2,T,T2. ⇧*[f2] T2 ≘ T → ∀f,T1. ⇧*[f] T1 ≘ T → ∀f1. f2 ⊚ f1 ≘ f → ⇧*[f1] T1 ≘ T2. #f2 #T #T2 #H elim H -f2 -T -T2 [ #f2 #s #f #T1 #H >(lifts_inv_sort2 … H) -T1 // | #f2 #i2 #i #Hi2 #f #T1 #H #f1 #Ht21 elim (lifts_inv_lref2 … H) -H - #i1 #Hi1 #H destruct /3 width=6 by lifts_lref, after_fwd_at1/ + #i1 #Hi1 #H destruct /3 width=6 by lifts_lref, pr_after_des_pat_dx/ | #f2 #l #f #T1 #H >(lifts_inv_gref2 … H) -T1 // | #f2 #p #I #W2 #W #U2 #U #_ #_ #IHW #IHU #f #T1 #H elim (lifts_inv_bind2 … H) -H #W1 #U1 #HW1 #HU1 #H destruct @@ -75,7 +75,7 @@ theorem lifts_trans: ∀f1,T1,T. ⇧*[f1] T1 ≘ T → ∀f2,T2. ⇧*[f2] T ≘ #f1 #T1 #T #H elim H -f1 -T1 -T [ #f1 #s #f2 #T2 #H >(lifts_inv_sort1 … H) -T2 // | #f1 #i1 #i #Hi1 #f2 #T2 #H #f #Ht21 elim (lifts_inv_lref1 … H) -H - #i2 #Hi2 #H destruct /3 width=6 by lifts_lref, after_fwd_at/ + #i2 #Hi2 #H destruct /3 width=6 by lifts_lref, pr_after_des_pat/ | #f1 #l #f2 #T2 #H >(lifts_inv_gref1 … H) -T2 // | #f1 #p #I #W1 #W #U1 #U #_ #_ #IHW #IHU #f2 #T2 #H elim (lifts_inv_bind1 … H) -H #W2 #U2 #HW2 #HU2 #H destruct @@ -89,7 +89,7 @@ qed-. lemma lifts_trans4_one (f) (T1) (T2): ∀T. ⇧[1]T1 ≘ T → ⇧*[⫯f]T ≘ T2 → ∃∃T0. ⇧*[f]T1 ≘ T0 & ⇧[1]T0 ≘ T2. -/4 width=6 by lifts_trans, lifts_split_trans, after_uni_one_dx/ qed-. +/4 width=6 by lifts_trans, lifts_split_trans, pr_after_push_unit/ qed-. (* Basic_2A1: includes: lift_conf_O1 lift_conf_be *) theorem lifts_conf: ∀f1,T,T1. ⇧*[f1] T ≘ T1 → ∀f,T2. ⇧*[f] T ≘ T2 → @@ -97,7 +97,7 @@ theorem lifts_conf: ∀f1,T,T1. ⇧*[f1] T ≘ T1 → ∀f,T2. ⇧*[f] T ≘ T2 #f1 #T #T1 #H elim H -f1 -T -T1 [ #f1 #s #f #T2 #H >(lifts_inv_sort1 … H) -T2 // | #f1 #i #i1 #Hi1 #f #T2 #H #f2 #Ht21 elim (lifts_inv_lref1 … H) -H - #i2 #Hi2 #H destruct /3 width=6 by lifts_lref, after_fwd_at2/ + #i2 #Hi2 #H destruct /3 width=6 by lifts_lref, pr_after_des_pat_sn/ | #f1 #l #f #T2 #H >(lifts_inv_gref1 … H) -T2 // | #f1 #p #I #W #W1 #U #U1 #_ #_ #IHW #IHU #f #T2 #H elim (lifts_inv_bind1 … H) -H #W2 #U2 #HW2 #HU2 #H destruct @@ -112,13 +112,13 @@ qed-. (* Basic_2A1: includes: lift_inj *) lemma lifts_inj: ∀f. is_inj2 … (lifts f). -#f #T1 #U #H1 #T2 #H2 lapply (after_isid_dx 𝐢 … f) +#f #T1 #U #H1 #T2 #H2 lapply (pr_after_isi_dx 𝐢 … f) /3 width=6 by lifts_div3, lifts_fwd_isid/ qed-. (* Basic_2A1: includes: lift_mono *) lemma lifts_mono: ∀f,T. is_mono … (lifts f T). -#f #T #U1 #H1 #U2 #H2 lapply (after_isid_sn 𝐢 … f) +#f #T #U1 #H1 #U2 #H2 lapply (pr_after_isi_sn 𝐢 … f) /3 width=6 by lifts_conf, lifts_fwd_isid/ qed-. diff --git a/matita/matita/contribs/lambdadelta/static_2/relocation/lifts_lifts_bind.ma b/matita/matita/contribs/lambdadelta/static_2/relocation/lifts_lifts_bind.ma index 0e18b44fd..c1c66d978 100644 --- a/matita/matita/contribs/lambdadelta/static_2/relocation/lifts_lifts_bind.ma +++ b/matita/matita/contribs/lambdadelta/static_2/relocation/lifts_lifts_bind.ma @@ -43,11 +43,11 @@ qed-. (* Advanced proprerties *****************************************************) lemma liftsb_inj: ∀f. is_inj2 … (liftsb f). -#f #T1 #U #H1 #T2 #H2 lapply (after_isid_dx 𝐢 … f) +#f #T1 #U #H1 #T2 #H2 lapply (pr_after_isi_dx 𝐢 … f) /3 width=6 by liftsb_div3, liftsb_fwd_isid/ qed-. lemma liftsb_mono: ∀f,T. is_mono … (liftsb f T). -#f #T #U1 #H1 #U2 #H2 lapply (after_isid_sn 𝐢 … f) +#f #T #U1 #H1 #U2 #H2 lapply (pr_after_isi_sn 𝐢 … f) /3 width=6 by liftsb_conf, liftsb_fwd_isid/ qed-. diff --git a/matita/matita/contribs/lambdadelta/static_2/relocation/lifts_teqo.ma b/matita/matita/contribs/lambdadelta/static_2/relocation/lifts_teqo.ma index 0a6831c72..b45a9e7e8 100644 --- a/matita/matita/contribs/lambdadelta/static_2/relocation/lifts_teqo.ma +++ b/matita/matita/contribs/lambdadelta/static_2/relocation/lifts_teqo.ma @@ -59,7 +59,7 @@ lemma teqo_inv_lifts_bi: deliftable2_bi teqo. | #j #f #X1 #H1 #X2 #H2 elim (lifts_inv_lref2 … H1) -H1 #i1 #Hj1 #H destruct elim (lifts_inv_lref2 … H2) -H2 #i2 #Hj2 #H destruct - <(at_inj … Hj2 … Hj1) -j -f -i1 + <(pr_pat_inj … Hj2 … Hj1) -j -f -i1 /1 width=1 by teqo_lref/ | #l #f #X1 #H1 #X2 #H2 >(lifts_inv_gref2 … H1) -H1 >(lifts_inv_gref2 … H2) -H2 diff --git a/matita/matita/contribs/lambdadelta/static_2/relocation/lifts_teqw.ma b/matita/matita/contribs/lambdadelta/static_2/relocation/lifts_teqw.ma index 532d0b236..d03e0ab40 100644 --- a/matita/matita/contribs/lambdadelta/static_2/relocation/lifts_teqw.ma +++ b/matita/matita/contribs/lambdadelta/static_2/relocation/lifts_teqw.ma @@ -69,7 +69,7 @@ lemma teqw_inv_lifts_bi: deliftable2_bi teqw. | #j #f #X1 #H1 #X2 #H2 elim (lifts_inv_lref2 … H1) -H1 #i1 #Hj1 #H destruct elim (lifts_inv_lref2 … H2) -H2 #i2 #Hj2 #H destruct - <(at_inj … Hj2 … Hj1) -j -f -i1 + <(pr_pat_inj … Hj2 … Hj1) -j -f -i1 /1 width=1 by teqw_lref/ | #l #f #X1 #H1 #X2 #H2 >(lifts_inv_gref2 … H1) -H1 >(lifts_inv_gref2 … H2) -H2 @@ -98,7 +98,7 @@ qed-. lemma teqw_inv_abbr_pos_x_lifts_y_y (T) (f): ∀V,U. +ⓓV.U ≃ T → ⇧*[f]T ≘ U → ⊥. -@(f_ind … tw) #n #IH #T #Hn #f #V #U #H1 #H2 destruct +@(wf1_ind_nlt … tw) #n #IH #T #Hn #f #V #U #H1 #H2 destruct elim (teqw_inv_abbr_pos_sn … H1) -H1 #X1 #X2 #HX2 #H destruct -V elim (lifts_inv_bind1 … H2) -H2 #Y1 #Y2 #_ #HXY2 #H destruct /2 width=7 by/ diff --git a/matita/matita/contribs/lambdadelta/static_2/relocation/lifts_vector.ma b/matita/matita/contribs/lambdadelta/static_2/relocation/lifts_vector.ma index a5310b63d..d0cd506bc 100644 --- a/matita/matita/contribs/lambdadelta/static_2/relocation/lifts_vector.ma +++ b/matita/matita/contribs/lambdadelta/static_2/relocation/lifts_vector.ma @@ -29,7 +29,7 @@ interpretation "generic relocation (term vector)" 'RLiftStar f T1s T2s = (liftsv f T1s T2s). interpretation "uniform relocation (term vector)" - 'RLift i T1s T2s = (liftsv (uni i) T1s T2s). + 'RLift i T1s T2s = (liftsv (pr_uni i) T1s T2s). (* Basic inversion lemmas ***************************************************) diff --git a/matita/matita/contribs/lambdadelta/static_2/relocation/seq.ma b/matita/matita/contribs/lambdadelta/static_2/relocation/seq.ma index 128cd2974..224102f01 100644 --- a/matita/matita/contribs/lambdadelta/static_2/relocation/seq.ma +++ b/matita/matita/contribs/lambdadelta/static_2/relocation/seq.ma @@ -19,7 +19,7 @@ include "static_2/relocation/sex.ma". (* SYNTACTIC EQUIVALENCE FOR SELECTED LOCAL ENVIRONMENTS ********************) (* Basic_2A1: includes: lreq_atom lreq_zero lreq_pair lreq_succ *) -definition seq: relation3 rtmap lenv lenv ≝ +definition seq: relation3 pr_map lenv lenv ≝ sex ceq_ext cfull. interpretation @@ -29,11 +29,11 @@ interpretation (* Basic properties *********************************************************) lemma seq_eq_repl_back: - ∀L1,L2. eq_repl_back … (λf. L1 ≡[f] L2). + ∀L1,L2. pr_eq_repl_back … (λf. L1 ≡[f] L2). /2 width=3 by sex_eq_repl_back/ qed-. lemma seq_eq_repl_fwd: - ∀L1,L2. eq_repl_fwd … (λf. L1 ≡[f] L2). + ∀L1,L2. pr_eq_repl_fwd … (λf. L1 ≡[f] L2). /2 width=3 by sex_eq_repl_fwd/ qed-. lemma sle_seq_trans: diff --git a/matita/matita/contribs/lambdadelta/static_2/relocation/sex.ma b/matita/matita/contribs/lambdadelta/static_2/relocation/sex.ma index 2a6946fca..47912ace0 100644 --- a/matita/matita/contribs/lambdadelta/static_2/relocation/sex.ma +++ b/matita/matita/contribs/lambdadelta/static_2/relocation/sex.ma @@ -19,7 +19,7 @@ include "static_2/syntax/lenv.ma". (* GENERIC ENTRYWISE EXTENSION OF CONTEXT-SENSITIVE REALTIONS FOR TERMS *****) -inductive sex (RN,RP:relation3 lenv bind bind): rtmap → relation lenv ≝ +inductive sex (RN,RP:relation3 lenv bind bind): pr_map → relation lenv ≝ | sex_atom: ∀f. sex RN RP f (⋆) (⋆) | sex_next: ∀f,I1,I2,L1,L2. sex RN RP f L1 L2 → RN L1 I1 I2 → @@ -37,7 +37,7 @@ definition R_pw_transitive_sex: relation3 lenv bind bind → relation3 lenv bind bind → relation3 lenv bind bind → relation3 lenv bind bind → relation3 lenv bind bind → - relation3 rtmap lenv bind ≝ + relation3 pr_map lenv bind ≝ λR1,R2,R3,RN,RP,f,L1,I1. ∀I. R1 L1 I1 I → ∀L2. L1 ⪤[RN,RP,f] L2 → ∀I2. R2 L2 I I2 → R3 L1 I1 I2. @@ -45,7 +45,7 @@ definition R_pw_transitive_sex: definition R_pw_confluent1_sex: relation3 lenv bind bind → relation3 lenv bind bind → relation3 lenv bind bind → relation3 lenv bind bind → - relation3 rtmap lenv bind ≝ + relation3 pr_map lenv bind ≝ λR1,R2,RN,RP,f,L1,I1. ∀I2. R1 L1 I1 I2 → ∀L2. L1 ⪤[RN,RP,f] L2 → R2 L2 I1 I2. @@ -53,7 +53,7 @@ definition R_pw_confluent2_sex: relation3 lenv bind bind → relation3 lenv bind bind → relation3 lenv bind bind → relation3 lenv bind bind → relation3 lenv bind bind → relation3 lenv bind bind → - relation3 rtmap lenv bind ≝ + relation3 pr_map lenv bind ≝ λR1,R2,RN1,RP1,RN2,RP2,f,L0,I0. ∀I1. R1 L0 I0 I1 → ∀I2. R2 L0 I0 I2 → ∀L1. L0 ⪤[RN1,RP1,f] L1 → ∀L2. L0 ⪤[RN2,RP2,f] L2 → @@ -63,7 +63,7 @@ definition R_pw_replace3_sex: relation3 lenv bind bind → relation3 lenv bind bind → relation3 lenv bind bind → relation3 lenv bind bind → relation3 lenv bind bind → relation3 lenv bind bind → - relation3 rtmap lenv bind ≝ + relation3 pr_map lenv bind ≝ λR1,R2,RN1,RP1,RN2,RP2,f,L0,I0. ∀I1. R1 L0 I0 I1 → ∀I2. R2 L0 I0 I2 → ∀L1. L0 ⪤[RN1,RP1,f] L1 → ∀L2. L0 ⪤[RN2,RP2,f] L2 → @@ -87,9 +87,9 @@ fact sex_inv_next1_aux (RN) (RP): ∃∃J2,K2. K1 ⪤[RN,RP,g] K2 & RN K1 J1 J2 & Y = K2.ⓘ[J2]. #RN #RP #f #X #Y * -f -X -Y [ #f #g #J1 #K1 #H destruct -| #f #I1 #I2 #L1 #L2 #HL #HI #g #J1 #K1 #H1 #H2 <(injective_next … H2) -g destruct +| #f #I1 #I2 #L1 #L2 #HL #HI #g #J1 #K1 #H1 #H2 <(eq_inv_pr_next_bi … H2) -g destruct /2 width=5 by ex3_2_intro/ -| #f #I1 #I2 #L1 #L2 #_ #_ #g #J1 #K1 #_ #H elim (discr_push_next … H) +| #f #I1 #I2 #L1 #L2 #_ #_ #g #J1 #K1 #_ #H elim (eq_inv_pr_push_next … H) ] qed-. @@ -104,8 +104,8 @@ fact sex_inv_push1_aux (RN) (RP): ∃∃J2,K2. K1 ⪤[RN,RP,g] K2 & RP K1 J1 J2 & Y = K2.ⓘ[J2]. #RN #RP #f #X #Y * -f -X -Y [ #f #g #J1 #K1 #H destruct -| #f #I1 #I2 #L1 #L2 #_ #_ #g #J1 #K1 #_ #H elim (discr_next_push … H) -| #f #I1 #I2 #L1 #L2 #HL #HI #g #J1 #K1 #H1 #H2 <(injective_push … H2) -g destruct +| #f #I1 #I2 #L1 #L2 #_ #_ #g #J1 #K1 #_ #H elim (eq_inv_pr_next_push … H) +| #f #I1 #I2 #L1 #L2 #HL #HI #g #J1 #K1 #H1 #H2 <(eq_inv_pr_push_bi … H2) -g destruct /2 width=5 by ex3_2_intro/ ] qed-. @@ -131,9 +131,9 @@ fact sex_inv_next2_aux (RN) (RP): ∃∃J1,K1. K1 ⪤[RN,RP,g] K2 & RN K1 J1 J2 & X = K1.ⓘ[J1]. #RN #RP #f #X #Y * -f -X -Y [ #f #g #J2 #K2 #H destruct -| #f #I1 #I2 #L1 #L2 #HL #HI #g #J2 #K2 #H1 #H2 <(injective_next … H2) -g destruct +| #f #I1 #I2 #L1 #L2 #HL #HI #g #J2 #K2 #H1 #H2 <(eq_inv_pr_next_bi … H2) -g destruct /2 width=5 by ex3_2_intro/ -| #f #I1 #I2 #L1 #L2 #_ #_ #g #J2 #K2 #_ #H elim (discr_push_next … H) +| #f #I1 #I2 #L1 #L2 #_ #_ #g #J2 #K2 #_ #H elim (eq_inv_pr_push_next … H) ] qed-. @@ -148,8 +148,8 @@ fact sex_inv_push2_aux (RN) (RP): ∃∃J1,K1. K1 ⪤[RN,RP,g] K2 & RP K1 J1 J2 & X = K1.ⓘ[J1]. #RN #RP #f #X #Y * -f -X -Y [ #f #J2 #K2 #g #H destruct -| #f #I1 #I2 #L1 #L2 #_ #_ #g #J2 #K2 #_ #H elim (discr_next_push … H) -| #f #I1 #I2 #L1 #L2 #HL #HI #g #J2 #K2 #H1 #H2 <(injective_push … H2) -g destruct +| #f #I1 #I2 #L1 #L2 #_ #_ #g #J2 #K2 #_ #H elim (eq_inv_pr_next_push … H) +| #f #I1 #I2 #L1 #L2 #HL #HI #g #J2 #K2 #H1 #H2 <(eq_inv_pr_push_bi … H2) -g destruct /2 width=5 by ex3_2_intro/ ] qed-. @@ -180,7 +180,7 @@ lemma sex_inv_tl (RN) (RP): ∀f,I1,I2,L1,L2. L1 ⪤[RN,RP,⫰f] L2 → RN L1 I1 I2 → RP L1 I1 I2 → L1.ⓘ[I1] ⪤[RN,RP,f] L2.ⓘ[I2]. -#RN #RP #f #I1 #I2 #L2 #L2 elim (pn_split f) * +#RN #RP #f #I1 #I2 #L2 #L2 elim (pr_map_split_tl f) * /2 width=1 by sex_next, sex_push/ qed-. @@ -190,14 +190,14 @@ lemma sex_fwd_bind (RN) (RP): ∀f,I1,I2,L1,L2. L1.ⓘ[I1] ⪤[RN,RP,f] L2.ⓘ[I2] → L1 ⪤[RN,RP,⫰f] L2. #RN #RP #f #I1 #I2 #L1 #L2 #Hf -elim (pn_split f) * #g #H destruct +elim (pr_map_split_tl f) * #g #H destruct [ elim (sex_inv_push … Hf) | elim (sex_inv_next … Hf) ] -Hf // qed-. (* Basic properties *********************************************************) lemma sex_eq_repl_back (RN) (RP): - ∀L1,L2. eq_repl_back … (λf. L1 ⪤[RN,RP,f] L2). + ∀L1,L2. pr_eq_repl_back … (λf. L1 ⪤[RN,RP,f] L2). #RN #RP #L1 #L2 #f1 #H elim H -f1 -L1 -L2 // #f1 #I1 #I2 #L1 #L2 #_ #HI #IH #f2 #H [ elim (eq_inv_nx … H) -H /3 width=3 by sex_next/ @@ -206,15 +206,15 @@ lemma sex_eq_repl_back (RN) (RP): qed-. lemma sex_eq_repl_fwd (RN) (RP): - ∀L1,L2. eq_repl_fwd … (λf. L1 ⪤[RN,RP,f] L2). -#RN #RP #L1 #L2 @eq_repl_sym /2 width=3 by sex_eq_repl_back/ (**) (* full auto fails *) + ∀L1,L2. pr_eq_repl_fwd … (λf. L1 ⪤[RN,RP,f] L2). +#RN #RP #L1 #L2 @pr_eq_repl_sym /2 width=3 by sex_eq_repl_back/ (**) (* full auto fails *) qed-. lemma sex_refl (RN) (RP): c_reflexive … RN → c_reflexive … RP → ∀f.reflexive … (sex RN RP f). #RN #RP #HRN #HRP #f #L generalize in match f; -f elim L -L // -#L #I #IH #f elim (pn_split f) * +#L #I #IH #f elim (pr_map_split_tl f) * #g #H destruct /2 width=1 by sex_next, sex_push/ qed. @@ -246,8 +246,8 @@ lemma sex_co_isid (RN1) (RP1) (RN2) (RP2): L1 ⪤[RN2,RP2,f] L2. #RN1 #RP1 #RN2 #RP2 #HR #f #L1 #L2 #H elim H -f -L1 -L2 // #f #I1 #I2 #K1 #K2 #_ #HI12 #IH #H -[ elim (isid_inv_next … H) -H // -| /4 width=3 by sex_push, isid_inv_push/ +[ elim (pr_isi_inv_next … H) -H // +| /4 width=3 by sex_push, pr_isi_inv_push/ ] qed-. @@ -257,9 +257,9 @@ lemma sex_sdj (RN) (RP): ∀f2. f1 ∥ f2 → L1 ⪤[RP,RN,f2] L2. #RN #RP #HR #f1 #L1 #L2 #H elim H -f1 -L1 -L2 // #f1 #I1 #I2 #L1 #L2 #_ #HI12 #IH #f2 #H12 -[ elim (sdj_inv_nx … H12) -H12 [2,3: // ] +[ elim (pr_sdj_inv_next_sn … H12) -H12 [2,3: // ] #g2 #H #H2 destruct /3 width=1 by sex_push/ -| elim (sdj_inv_px … H12) -H12 [2,4: // ] * +| elim (pr_sdj_inv_push_sn … H12) -H12 [2,4: // ] * #g2 #H #H2 destruct /3 width=1 by sex_next, sex_push/ ] qed-. @@ -270,10 +270,10 @@ lemma sle_sex_trans (RN) (RP): ∀f1. f1 ⊆ f2 → L1 ⪤[RN,RP,f1] L2. #RN #RP #HR #f2 #L1 #L2 #H elim H -f2 -L1 -L2 // #f2 #I1 #I2 #L1 #L2 #_ #HI12 #IH #f1 #H12 -[ elim (pn_split f1) * ] -[ /4 width=5 by sex_push, sle_inv_pn/ -| /4 width=5 by sex_next, sle_inv_nn/ -| elim (sle_inv_xp … H12) -H12 [2,3: // ] +[ elim (pr_map_split_tl f1) * ] +[ /4 width=5 by sex_push, pr_sle_inv_push_next/ +| /4 width=5 by sex_next, pr_sle_inv_next_bi/ +| elim (pr_sle_inv_push_dx … H12) -H12 [2,3: // ] #g1 #H #H1 destruct /3 width=5 by sex_push/ ] qed-. @@ -284,10 +284,10 @@ lemma sle_sex_conf (RN) (RP): ∀f2. f1 ⊆ f2 → L1 ⪤[RN,RP,f2] L2. #RN #RP #HR #f1 #L1 #L2 #H elim H -f1 -L1 -L2 // #f1 #I1 #I2 #L1 #L2 #_ #HI12 #IH #f2 #H12 -[2: elim (pn_split f2) * ] -[ /4 width=5 by sex_push, sle_inv_pp/ -| /4 width=5 by sex_next, sle_inv_pn/ -| elim (sle_inv_nx … H12) -H12 [2,3: // ] +[2: elim (pr_map_split_tl f2) * ] +[ /4 width=5 by sex_push, pr_sle_inv_push_bi/ +| /4 width=5 by sex_next, pr_sle_inv_push_next/ +| elim (pr_sle_inv_next_sn … H12) -H12 [2,3: // ] #g2 #H #H2 destruct /3 width=5 by sex_next/ ] qed-. @@ -299,9 +299,9 @@ lemma sex_sle_split_sn (R1) (R2) (RP): #R1 #R2 #RP #HR1 #HR2 #f #L1 #L2 #H elim H -f -L1 -L2 [ /2 width=3 by sex_atom, ex2_intro/ ] #f #I1 #I2 #L1 #L2 #_ #HI12 #IH #y #H -[ elim (sle_inv_nx … H ??) -H [ |*: // ] #g #Hfg #H destruct +[ elim (pr_sle_inv_next_sn … H ??) -H [ |*: // ] #g #Hfg #H destruct elim (IH … Hfg) -IH -Hfg /3 width=5 by sex_next, ex2_intro/ -| elim (sle_inv_px … H ??) -H [1,3: * |*: // ] #g #Hfg #H destruct +| elim (pr_sle_inv_push_sn … H ??) -H [1,3: * |*: // ] #g #Hfg #H destruct elim (IH … Hfg) -IH -Hfg /3 width=5 by sex_next, sex_push, ex2_intro/ ] qed-. @@ -313,9 +313,9 @@ lemma sex_sdj_split_sn (R1) (R2) (RP): #R1 #R2 #RP #HR1 #HR2 #f #L1 #L2 #H elim H -f -L1 -L2 [ /2 width=3 by sex_atom, ex2_intro/ ] #f #I1 #I2 #L1 #L2 #_ #HI12 #IH #y #H -[ elim (sdj_inv_nx … H ??) -H [ |*: // ] #g #Hfg #H destruct +[ elim (pr_sdj_inv_next_sn … H ??) -H [ |*: // ] #g #Hfg #H destruct elim (IH … Hfg) -IH -Hfg /3 width=5 by sex_next, sex_push, ex2_intro/ -| elim (sdj_inv_px … H ??) -H [1,3: * |*: // ] #g #Hfg #H destruct +| elim (pr_sdj_inv_push_sn … H ??) -H [1,3: * |*: // ] #g #Hfg #H destruct elim (IH … Hfg) -IH -Hfg /3 width=5 by sex_next, sex_push, ex2_intro/ ] qed-. @@ -332,7 +332,7 @@ lemma sex_dec (RN) (RP): lapply (sex_inv_atom2 … H) -H #H destruct | #L2 #I2 #f elim (IH L2 (⫰f)) -IH #HL12 [2: /4 width=3 by sex_fwd_bind, or_intror/ ] - elim (pn_split f) * #g #H destruct + elim (pr_map_split_tl f) * #g #H destruct [ elim (HRP L1 I1 I2) | elim (HRN L1 I1 I2) ] -HRP -HRN #HV12 [1,3: /3 width=1 by sex_push, sex_next, or_introl/ ] @or_intror #H diff --git a/matita/matita/contribs/lambdadelta/static_2/relocation/sex_length.ma b/matita/matita/contribs/lambdadelta/static_2/relocation/sex_length.ma index 4f2157be2..c99c786c6 100644 --- a/matita/matita/contribs/lambdadelta/static_2/relocation/sex_length.ma +++ b/matita/matita/contribs/lambdadelta/static_2/relocation/sex_length.ma @@ -31,7 +31,7 @@ lemma sex_length_cfull: ∀L1,L2. |L1| = |L2| → ∀f. L1 ⪤[cfull,cfull,f] L2 [ #Y2 #H >(length_inv_zero_sn … H) -Y2 // | #L1 #I1 #IH #Y2 #H #f elim (length_inv_succ_sn … H) -H #I2 #L2 #HL12 #H destruct - elim (pn_split f) * #g #H destruct /3 width=1 by sex_next, sex_push/ + elim (pr_map_split_tl f) * #g #H destruct /3 width=1 by sex_next, sex_push/ ] qed. @@ -41,6 +41,6 @@ lemma sex_length_isid: ∀R,L1,L2. |L1| = |L2| → [ #Y2 #H >(length_inv_zero_sn … H) -Y2 // | #L1 #I1 #IH #Y2 #H #f #Hf elim (length_inv_succ_sn … H) -H #I2 #L2 #HL12 #H destruct - elim (isid_inv_gen … Hf) -Hf #g #Hg #H destruct /3 width=1 by sex_push/ + elim (pr_isi_inv_gen … Hf) -Hf #g #Hg #H destruct /3 width=1 by sex_push/ ] qed. diff --git a/matita/matita/contribs/lambdadelta/static_2/relocation/sex_sex.ma b/matita/matita/contribs/lambdadelta/static_2/relocation/sex_sex.ma index a92cf28c1..19078cfbe 100644 --- a/matita/matita/contribs/lambdadelta/static_2/relocation/sex_sex.ma +++ b/matita/matita/contribs/lambdadelta/static_2/relocation/sex_sex.ma @@ -31,7 +31,7 @@ theorem sex_trans_gen (RN1) (RP1) (RN2) (RP2) (RN) (RP): lapply (sex_inv_atom1 … H1) -H1 #H destruct lapply (sex_inv_atom1 … H2) -H2 #H destruct /2 width=1 by sex_atom/ -| #K1 #I1 #IH #f elim (pn_split f) * #g #H destruct +| #K1 #I1 #IH #f elim (pr_map_split_tl f) * #g #H destruct #HN #HP #L0 #H1 #L2 #H2 [ elim (sex_inv_push1 … H1) -H1 #I0 #K0 #HK10 #HI10 #H destruct elim (sex_inv_push1 … H2) -H2 #I2 #K2 #HK02 #HI02 #H destruct @@ -57,7 +57,7 @@ theorem sex_trans_id_cfull (R1) (R2) (R3): #R1 #R2 #R3 #L1 #L #f #H elim H -L1 -L -f [ #f #Hf #L2 #H >(sex_inv_atom1 … H) -L2 // ] #f #I1 #I #K1 #K #HK1 #_ #IH #Hf #L2 #H -[ elim (isid_inv_next … Hf) | lapply (isid_inv_push … Hf ??) ] -Hf [5: |*: // ] #Hf +[ elim (pr_isi_inv_next … Hf) | lapply (pr_isi_inv_push … Hf ??) ] -Hf [5: |*: // ] #Hf elim (sex_inv_push1 … H) -H #I2 #K2 #HK2 #_ #H destruct /3 width=1 by sex_push/ qed-. @@ -70,7 +70,7 @@ theorem sex_conf (RN1) (RP1) (RN2) (RP2): #RN1 #RP1 #RN2 #RP2 #L elim L -L [ #f #_ #_ #L1 #H1 #L2 #H2 >(sex_inv_atom1 … H1) >(sex_inv_atom1 … H2) -H2 -H1 /2 width=3 by sex_atom, ex2_intro/ -| #L #I0 #IH #f elim (pn_split f) * #g #H destruct +| #L #I0 #IH #f elim (pr_map_split_tl f) * #g #H destruct #HN #HP #Y1 #H1 #Y2 #H2 [ elim (sex_inv_push1 … H1) -H1 #I1 #L1 #HL1 #HI01 #H destruct elim (sex_inv_push1 … H2) -H2 #I2 #L2 #HL2 #HI02 #H destruct @@ -94,7 +94,7 @@ lemma sex_repl (RN) (RP) (SN) (SP) (L1) (f): lapply (sex_inv_atom1 … HY) -HY #H destruct lapply (sex_inv_atom1 … HY1) -HY1 #H destruct lapply (sex_inv_atom1 … HY2) -HY2 #H destruct // -| #L1 #I1 #IH #f elim (pn_split f) * #g #H destruct +| #L1 #I1 #IH #f elim (pr_map_split_tl f) * #g #H destruct #HN #HP #Y #HY #Y1 #HY1 #Y2 #HY2 [ elim (sex_inv_push1 … HY) -HY #I2 #L2 #HL12 #HI12 #H destruct elim (sex_inv_push1 … HY1) -HY1 #J1 #K1 #HLK1 #HIJ1 #H destruct @@ -124,10 +124,10 @@ lemma sex_meet (RN) (RP) (L1) (L2): ∀f. f1 ⋒ f2 ≘ f → L1 ⪤[RN,RP,f] L2. #RN #RP #L1 #L2 #f1 #H elim H -f1 -L1 -L2 // #f1 #I1 #I2 #L1 #L2 #_ #HI12 #IH #f2 #H #f #Hf -elim (pn_split f2) * #g2 #H2 destruct +elim (pr_map_split_tl f2) * #g2 #H2 destruct try elim (sex_inv_push … H) try elim (sex_inv_next … H) -H -[ elim (sand_inv_npx … Hf) | elim (sand_inv_nnx … Hf) -| elim (sand_inv_ppx … Hf) | elim (sand_inv_pnx … Hf) +[ elim (pr_sand_inv_next_push … Hf) | elim (pr_sand_inv_next_bi … Hf) +| elim (pr_sand_inv_push_bi … Hf) | elim (pr_sand_inv_push_next … Hf) ] -Hf /3 width=5 by sex_next, sex_push/ qed-. @@ -137,9 +137,9 @@ lemma sex_join (RN) (RP) (L1) (L2): ∀f. f1 ⋓ f2 ≘ f → L1 ⪤[RN,RP,f] L2. #RN #RP #L1 #L2 #f1 #H elim H -f1 -L1 -L2 // #f1 #I1 #I2 #L1 #L2 #_ #HI12 #IH #f2 #H #f #Hf -elim (pn_split f2) * #g2 #H2 destruct +elim (pr_map_split_tl f2) * #g2 #H2 destruct try elim (sex_inv_push … H) try elim (sex_inv_next … H) -H -[ elim (sor_inv_npx … Hf) | elim (sor_inv_nnx … Hf) -| elim (sor_inv_ppx … Hf) | elim (sor_inv_pnx … Hf) +[ elim (pr_sor_inv_next_push … Hf) | elim (pr_sor_inv_next_bi … Hf) +| elim (pr_sor_inv_push_bi … Hf) | elim (pr_sor_inv_push_next … Hf) ] -Hf /3 width=5 by sex_next, sex_push/ qed-. diff --git a/matita/matita/contribs/lambdadelta/static_2/relocation/sex_tc.ma b/matita/matita/contribs/lambdadelta/static_2/relocation/sex_tc.ma index f372e4067..0a95ed3b0 100644 --- a/matita/matita/contribs/lambdadelta/static_2/relocation/sex_tc.ma +++ b/matita/matita/contribs/lambdadelta/static_2/relocation/sex_tc.ma @@ -87,8 +87,8 @@ theorem sex_tc_step_dx: ∀RN,RP. s_rs_transitive_isid RN RP → #RN #RP #HRP #f #L1 #L #H elim H -f -L1 -L [ #f #_ #Y #H -HRP >(sex_inv_atom1 … H) -Y // ] #f #I1 #I #L1 #L #HL1 #HI1 #IH #Hf #Y #H -[ elim (isid_inv_next … Hf) -Hf // -| lapply (isid_inv_push … Hf ??) -Hf [3: |*: // ] #Hf +[ elim (pr_isi_inv_next … Hf) -Hf // +| lapply (pr_isi_inv_push … Hf ??) -Hf [3: |*: // ] #Hf elim (sex_inv_push1 … H) -H #I2 #L2 #HL2 #HI2 #H destruct @sex_push [ /2 width=1 by/ ] -L2 -IH @(TC_strap … HI1) -HI1 diff --git a/matita/matita/contribs/lambdadelta/static_2/s_computation/fqup_weight.ma b/matita/matita/contribs/lambdadelta/static_2/s_computation/fqup_weight.ma index 94642d014..ed22b9e12 100644 --- a/matita/matita/contribs/lambdadelta/static_2/s_computation/fqup_weight.ma +++ b/matita/matita/contribs/lambdadelta/static_2/s_computation/fqup_weight.ma @@ -22,7 +22,7 @@ include "static_2/s_computation/fqup.ma". lemma fqup_fwd_fw: ∀b,G1,G2,L1,L2,T1,T2. ❪G1,L1,T1❫ ⬂+[b] ❪G2,L2,T2❫ → ♯❨G2,L2,T2❩ < ♯❨G1,L1,T1❩. #b #G1 #G2 #L1 #L2 #T1 #T2 #H @(fqup_ind … H) -G2 -L2 -T2 -/3 width=3 by fqu_fwd_fw, transitive_lt/ +/3 width=3 by fqu_fwd_fw, nlt_trans/ qed-. (* Advanced eliminators *****************************************************) @@ -31,7 +31,7 @@ lemma fqup_wf_ind: ∀b. ∀Q:relation3 …. ( ∀G1,L1,T1. (∀G2,L2,T2. ❪G1,L1,T1❫ ⬂+[b] ❪G2,L2,T2❫ → Q G2 L2 T2) → Q G1 L1 T1 ) → ∀G1,L1,T1. Q G1 L1 T1. -#b #Q #HQ @(f3_ind … fw) #x #IHx #G1 #L1 #T1 #H destruct +#b #Q #HQ @(wf3_ind_nlt … fw) #x #IHx #G1 #L1 #T1 #H destruct /4 width=2 by fqup_fwd_fw/ qed-. @@ -39,6 +39,6 @@ lemma fqup_wf_ind_eq: ∀b. ∀Q:relation3 …. ( ∀G1,L1,T1. (∀G2,L2,T2. ❪G1,L1,T1❫ ⬂+[b] ❪G2,L2,T2❫ → Q G2 L2 T2) → ∀G2,L2,T2. G1 = G2 → L1 = L2 → T1 = T2 → Q G2 L2 T2 ) → ∀G1,L1,T1. Q G1 L1 T1. -#b #Q #HQ @(f3_ind … fw) #x #IHx #G1 #L1 #T1 #H destruct +#b #Q #HQ @(wf3_ind_nlt … fw) #x #IHx #G1 #L1 #T1 #H destruct /4 width=7 by fqup_fwd_fw/ qed-. diff --git a/matita/matita/contribs/lambdadelta/static_2/s_computation/fqus_weight.ma b/matita/matita/contribs/lambdadelta/static_2/s_computation/fqus_weight.ma index 4c0406cf5..b76988981 100644 --- a/matita/matita/contribs/lambdadelta/static_2/s_computation/fqus_weight.ma +++ b/matita/matita/contribs/lambdadelta/static_2/s_computation/fqus_weight.ma @@ -22,7 +22,7 @@ include "static_2/s_computation/fqus.ma". lemma fqus_fwd_fw: ∀b,G1,G2,L1,L2,T1,T2. ❪G1,L1,T1❫ ⬂*[b] ❪G2,L2,T2❫ → ♯❨G2,L2,T2❩ ≤ ♯❨G1,L1,T1❩. #b #G1 #G2 #L1 #L2 #T1 #T2 #H @(fqus_ind … H) -L2 -T2 -/3 width=3 by fquq_fwd_fw, transitive_le/ +/3 width=3 by fquq_fwd_fw, nle_trans/ qed-. (* Advanced inversion lemmas ************************************************) @@ -30,6 +30,6 @@ qed-. lemma fqus_inv_refl_atom3: ∀b,I,G,L,X. ❪G,L,⓪[I]❫ ⬂*[b] ❪G,L,X❫ → ⓪[I] = X. #b #I #G #L #X #H elim (fqus_inv_fqu_sn … H) -H * // #G0 #L0 #T0 #H1 #H2 lapply (fqu_fwd_fw … H1) lapply (fqus_fwd_fw … H2) -H2 -H1 -#H2 #H1 lapply (le_to_lt_to_lt … H2 H1) -G0 -L0 -T0 -#H elim (lt_le_false … H) -H /2 width=1 by monotonic_le_plus_r/ +#H2 #H1 lapply (nle_nlt_trans … H2 H1) -G0 -L0 -T0 +#H elim (nlt_ge_false … H) -H /2 width=1 by nle_plus_bi_sn/ qed-. diff --git a/matita/matita/contribs/lambdadelta/static_2/s_transition/fqu_teqg.ma b/matita/matita/contribs/lambdadelta/static_2/s_transition/fqu_teqg.ma index bd420fd38..366fad94a 100644 --- a/matita/matita/contribs/lambdadelta/static_2/s_transition/fqu_teqg.ma +++ b/matita/matita/contribs/lambdadelta/static_2/s_transition/fqu_teqg.ma @@ -23,8 +23,8 @@ fact fqu_inv_teqg_aux (S) (b): ∀G1,G2,L1,L2,T1,T2. ❪G1,L1,T1❫ ⬂[b] ❪G2,L2,T2❫ → G1 = G2 → |L1| = |L2| → T1 ≛[S] T2 → ⊥. #S #b #G1 #G2 #L1 #L2 #T1 #T2 * -G1 -G2 -L1 -L2 -T1 -T2 -[1: #I #G #L #V #_ #H elim (succ_inv_refl_sn … H) -|6: #I #G #L #T #U #_ #_ #H elim (succ_inv_refl_sn … H) +[1: #I #G #L #V #_ #H elim (nsucc_inv_refl … H) +|6: #I #G #L #T #U #_ #_ #H elim (nsucc_inv_refl … H) ] /2 width=6 by teqg_inv_pair_xy_y, teqg_inv_pair_xy_x/ qed-. diff --git a/matita/matita/contribs/lambdadelta/static_2/s_transition/fqu_weight.ma b/matita/matita/contribs/lambdadelta/static_2/s_transition/fqu_weight.ma index 51d3b957f..f34260369 100644 --- a/matita/matita/contribs/lambdadelta/static_2/s_transition/fqu_weight.ma +++ b/matita/matita/contribs/lambdadelta/static_2/s_transition/fqu_weight.ma @@ -24,7 +24,7 @@ lemma fqu_fwd_fw: ∀b,G1,G2,L1,L2,T1,T2. ❪G1,L1,T1❫ ⬂[b] ❪G2,L2,T2❫ ♯❨G2,L2,T2❩ < ♯❨G1,L1,T1❩. #b #G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2 // #I #I1 #I2 #G #L #HI12 normalize in ⊢ (?%%); -I1 -<(lifts_fwd_tw … HI12) /3 width=1 by monotonic_lt_plus_r, monotonic_lt_plus_l/ +<(lifts_fwd_tw … HI12) /3 width=1 by nlt_plus_bi_sn, nlt_plus_bi_dx/ qed-. (* Advanced eliminators *****************************************************) @@ -33,5 +33,5 @@ lemma fqu_wf_ind: ∀b. ∀Q:relation3 …. ( ∀G1,L1,T1. (∀G2,L2,T2. ❪G1,L1,T1❫ ⬂[b] ❪G2,L2,T2❫ → Q G2 L2 T2) → Q G1 L1 T1 ) → ∀G1,L1,T1. Q G1 L1 T1. -#b #Q #HQ @(f3_ind … fw) #x #IHx #G1 #L1 #T1 #H destruct /4 width=2 by fqu_fwd_fw/ +#b #Q #HQ @(wf3_ind_nlt … fw) #x #IHx #G1 #L1 #T1 #H destruct /4 width=2 by fqu_fwd_fw/ qed-. diff --git a/matita/matita/contribs/lambdadelta/static_2/s_transition/fquq_length.ma b/matita/matita/contribs/lambdadelta/static_2/s_transition/fquq_length.ma index 20bc7f0bd..ed038771f 100644 --- a/matita/matita/contribs/lambdadelta/static_2/s_transition/fquq_length.ma +++ b/matita/matita/contribs/lambdadelta/static_2/s_transition/fquq_length.ma @@ -22,5 +22,5 @@ include "static_2/s_transition/fquq.ma". lemma fquq_fwd_length_lref1: ∀b,G1,G2,L1,L2,T2,i. ❪G1,L1,#i❫ ⬂⸮[b] ❪G2,L2,T2❫ → |L2| ≤ |L1|. #b #G1 #G2 #L1 #L2 #T2 #i #H elim H -H [2: * ] -/3 width=6 by fqu_fwd_length_lref1, lt_to_le/ +/3 width=6 by fqu_fwd_length_lref1, nlt_des_le/ qed-. diff --git a/matita/matita/contribs/lambdadelta/static_2/s_transition/fquq_weight.ma b/matita/matita/contribs/lambdadelta/static_2/s_transition/fquq_weight.ma index 605a53905..69f303e93 100644 --- a/matita/matita/contribs/lambdadelta/static_2/s_transition/fquq_weight.ma +++ b/matita/matita/contribs/lambdadelta/static_2/s_transition/fquq_weight.ma @@ -22,5 +22,5 @@ include "static_2/s_transition/fquq.ma". lemma fquq_fwd_fw: ∀b,G1,G2,L1,L2,T1,T2. ❪G1,L1,T1❫ ⬂⸮[b] ❪G2,L2,T2❫ → ♯❨G2,L2,T2❩ ≤ ♯❨G1,L1,T1❩. #b #G1 #G2 #L1 #L2 #T1 #T2 #H elim H -H [2: * ] -/3 width=2 by fqu_fwd_fw, lt_to_le/ +/3 width=2 by fqu_fwd_fw, nlt_des_le/ qed-. diff --git a/matita/matita/contribs/lambdadelta/static_2/static/aaa_drops.ma b/matita/matita/contribs/lambdadelta/static_2/static/aaa_drops.ma index bb54a3367..b501bd3a6 100644 --- a/matita/matita/contribs/lambdadelta/static_2/static/aaa_drops.ma +++ b/matita/matita/contribs/lambdadelta/static_2/static/aaa_drops.ma @@ -26,7 +26,7 @@ lemma aaa_lref_drops: ∀I,G,K,V,B,i,L. ⇩[i] L ≘ K.ⓑ[I]V → ❪G,K❫ ⊢ #I #G #K #V #B #i elim i -i [ #L #H lapply (drops_fwd_isid … H ?) -H // #H destruct /2 width=1 by aaa_zero/ -| #i #IH #L (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 *************) @@ -173,8 +173,8 @@ lemma frees_inv_lifts_SO: ∀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/ +#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,7 +182,7 @@ 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 *) @@ -193,48 +193,48 @@ lemma frees_inv_drops_next: ∃∃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

(injective_next … Hgf1) -g1 + #H destruct #g1 #Hgf1 >(eq_inv_pr_next_bi … Hgf1) -g1 /2 width=3 by ex2_intro/ | -Hf1 #j #HL12 lapply (drops_inv_drop1 … HL12) -HL12 - #HL12 #g1 tls_xn #H2 elim (IHT1 … H2) -IHT1 -H2 - /3 width=6 by drops_drop, sor_inv_sle_dx_trans, ex2_intro/ + /3 width=6 by pr_sor_inv_sle_sn_trans, ex2_intro/ + | -IHV1 #_ >pr_tls_swap #H2 elim (IHT1 … H2) -IHT1 -H2 + /3 width=6 by drops_drop, pr_sor_inv_sle_dx_trans, ex2_intro/ ] | #fV1 #fT1 #f1 #I1 #L1 #V1 #T1 #_ #_ #Hf1 #IHV1 #IHT1 #I2 #L2 #V2 #j #HL12 #g1 #Hgf1 - lapply (sor_tls … Hf1 j) -Hf1 (liftsv_mono … HV12s … HV10s) -V1s // | @(acr_lifts … H1RP … HB … HV120) /3 width=2 by drops_refl, drops_drop/ ] diff --git a/matita/matita/contribs/lambdadelta/static_2/static/lsubf.ma b/matita/matita/contribs/lambdadelta/static_2/static/lsubf.ma index 8e63f58d2..be342a26b 100644 --- a/matita/matita/contribs/lambdadelta/static_2/static/lsubf.ma +++ b/matita/matita/contribs/lambdadelta/static_2/static/lsubf.ma @@ -24,7 +24,7 @@ include "static_2/static/frees.ma". (* RESTRICTED REFINEMENT FOR CONTEXT-SENSITIVE FREE VARIABLES ***************) -inductive lsubf: relation4 lenv rtmap lenv rtmap ≝ +inductive lsubf: relation4 lenv pr_map lenv pr_map ≝ | lsubf_atom: ∀f1,f2. f1 ≡ f2 → lsubf (⋆) f1 (⋆) f2 | lsubf_push: ∀f1,f2,I1,I2,L1,L2. lsubf L1 (f1) L2 (f2) → lsubf (L1.ⓘ[I1]) (⫯f1) (L2.ⓘ[I2]) (⫯f2) @@ -64,10 +64,10 @@ fact lsubf_inv_push1_aux: #f1 #f2 #L1 #L2 * -f1 -f2 -L1 -L2 [ #f1 #f2 #_ #g1 #J1 #K1 #_ #H destruct | #f1 #f2 #I1 #I2 #L1 #L2 #H12 #g1 #J1 #K1 #H1 #H2 destruct - <(injective_push … H1) -g1 /2 width=6 by ex3_3_intro/ -| #f1 #f2 #I #L1 #L2 #_ #g1 #J1 #K1 #H elim (discr_next_push … H) -| #f #f0 #f1 #f2 #L1 #L2 #W #V #_ #_ #_ #g1 #J1 #K1 #H elim (discr_next_push … H) -| #f #f0 #f1 #f2 #I1 #I2 #L1 #L2 #V #_ #_ #_ #g1 #J1 #K1 #H elim (discr_next_push … H) + <(eq_inv_pr_push_bi … H1) -g1 /2 width=6 by ex3_3_intro/ +| #f1 #f2 #I #L1 #L2 #_ #g1 #J1 #K1 #H elim (eq_inv_pr_next_push … H) +| #f #f0 #f1 #f2 #L1 #L2 #W #V #_ #_ #_ #g1 #J1 #K1 #H elim (eq_inv_pr_next_push … H) +| #f #f0 #f1 #f2 #I1 #I2 #L1 #L2 #V #_ #_ #_ #g1 #J1 #K1 #H elim (eq_inv_pr_next_push … H) ] qed-. @@ -87,13 +87,13 @@ fact lsubf_inv_pair1_aux: K1 ⊢ 𝐅+❪X❫ ≘ g & g0 ⋓ g ≘ g1 & f2 = ↑g2 & L2 = K2.ⓤ[J]. #f1 #f2 #L1 #L2 * -f1 -f2 -L1 -L2 [ #f1 #f2 #_ #g1 #J #K1 #X #_ #H destruct -| #f1 #f2 #I1 #I2 #L1 #L2 #H12 #g1 #J #K1 #X #H elim (discr_push_next … H) +| #f1 #f2 #I1 #I2 #L1 #L2 #H12 #g1 #J #K1 #X #H elim (eq_inv_pr_push_next … H) | #f1 #f2 #I #L1 #L2 #H12 #g1 #J #K1 #X #H1 #H2 destruct - <(injective_next … H1) -g1 /3 width=5 by or3_intro0, ex3_2_intro/ + <(eq_inv_pr_next_bi … H1) -g1 /3 width=5 by or3_intro0, ex3_2_intro/ | #f #f0 #f1 #f2 #L1 #L2 #W #V #Hf #Hf1 #H12 #g1 #J #K1 #X #H1 #H2 destruct - <(injective_next … H1) -g1 /3 width=12 by or3_intro1, ex7_6_intro/ + <(eq_inv_pr_next_bi … H1) -g1 /3 width=12 by or3_intro1, ex7_6_intro/ | #f #f0 #f1 #f2 #I1 #I2 #L1 #L2 #V #Hf #Hf1 #H12 #g1 #J #K1 #X #H1 #H2 destruct - <(injective_next … H1) -g1 /3 width=10 by or3_intro2, ex5_5_intro/ + <(eq_inv_pr_next_bi … H1) -g1 /3 width=10 by or3_intro2, ex5_5_intro/ ] qed-. @@ -113,9 +113,9 @@ fact lsubf_inv_unit1_aux: ∃∃g2,K2. ❪K1,g1❫ ⫃𝐅+ ❪K2,g2❫ & f2 = ↑g2 & L2 = K2.ⓤ[I]. #f1 #f2 #L1 #L2 * -f1 -f2 -L1 -L2 [ #f1 #f2 #_ #g1 #J #K1 #_ #H destruct -| #f1 #f2 #I1 #I2 #L1 #L2 #H12 #g1 #J #K1 #H elim (discr_push_next … H) +| #f1 #f2 #I1 #I2 #L1 #L2 #H12 #g1 #J #K1 #H elim (eq_inv_pr_push_next … H) | #f1 #f2 #I #L1 #L2 #H12 #g1 #J #K1 #H1 #H2 destruct - <(injective_next … H1) -g1 /2 width=5 by ex3_2_intro/ + <(eq_inv_pr_next_bi … H1) -g1 /2 width=5 by ex3_2_intro/ | #f #f0 #f1 #f2 #L1 #L2 #W #V #_ #_ #_ #g1 #J #K1 #_ #H destruct | #f #f0 #f1 #f2 #I1 #I2 #L1 #L2 #V #_ #_ #_ #g1 #J #K1 #_ #H destruct ] @@ -148,10 +148,10 @@ fact lsubf_inv_push2_aux: #f1 #f2 #L1 #L2 * -f1 -f2 -L1 -L2 [ #f1 #f2 #_ #g2 #J2 #K2 #_ #H destruct | #f1 #f2 #I1 #I2 #L1 #L2 #H12 #g2 #J2 #K2 #H1 #H2 destruct - <(injective_push … H1) -g2 /2 width=6 by ex3_3_intro/ -| #f1 #f2 #I #L1 #L2 #_ #g2 #J2 #K2 #H elim (discr_next_push … H) -| #f #f0 #f1 #f2 #L1 #L2 #W #V #_ #_ #_ #g2 #J2 #K2 #H elim (discr_next_push … H) -| #f #f0 #f1 #f2 #I1 #I2 #L1 #L2 #V #_ #_ #_ #g2 #J2 #K2 #H elim (discr_next_push … H) + <(eq_inv_pr_push_bi … H1) -g2 /2 width=6 by ex3_3_intro/ +| #f1 #f2 #I #L1 #L2 #_ #g2 #J2 #K2 #H elim (eq_inv_pr_next_push … H) +| #f #f0 #f1 #f2 #L1 #L2 #W #V #_ #_ #_ #g2 #J2 #K2 #H elim (eq_inv_pr_next_push … H) +| #f #f0 #f1 #f2 #I1 #I2 #L1 #L2 #V #_ #_ #_ #g2 #J2 #K2 #H elim (eq_inv_pr_next_push … H) ] qed-. @@ -169,11 +169,11 @@ fact lsubf_inv_pair2_aux: I = Abst & L1 = K1.ⓓⓝW.V. #f1 #f2 #L1 #L2 * -f1 -f2 -L1 -L2 [ #f1 #f2 #_ #g2 #J #K2 #X #_ #H destruct -| #f1 #f2 #I1 #I2 #L1 #L2 #H12 #g2 #J #K2 #X #H elim (discr_push_next … H) +| #f1 #f2 #I1 #I2 #L1 #L2 #H12 #g2 #J #K2 #X #H elim (eq_inv_pr_push_next … H) | #f1 #f2 #I #L1 #L2 #H12 #g2 #J #K2 #X #H1 #H2 destruct - <(injective_next … H1) -g2 /3 width=5 by ex3_2_intro, or_introl/ + <(eq_inv_pr_next_bi … H1) -g2 /3 width=5 by ex3_2_intro, or_introl/ | #f #f0 #f1 #f2 #L1 #L2 #W #V #Hf #Hf1 #H12 #g2 #J #K2 #X #H1 #H2 destruct - <(injective_next … H1) -g2 /3 width=10 by ex6_5_intro, or_intror/ + <(eq_inv_pr_next_bi … H1) -g2 /3 width=10 by ex6_5_intro, or_intror/ | #f #f0 #f1 #f2 #I1 #I2 #L1 #L2 #V #_ #_ #_ #g2 #J #K2 #X #_ #H destruct ] qed-. @@ -194,12 +194,12 @@ fact lsubf_inv_unit2_aux: K1 ⊢ 𝐅+❪V❫ ≘ g & g0 ⋓ g ≘ g1 & f1 = ↑g1 & L1 = K1.ⓑ[J]V. #f1 #f2 #L1 #L2 * -f1 -f2 -L1 -L2 [ #f1 #f2 #_ #g2 #J #K2 #_ #H destruct -| #f1 #f2 #I1 #I2 #L1 #L2 #H12 #g2 #J #K2 #H elim (discr_push_next … H) +| #f1 #f2 #I1 #I2 #L1 #L2 #H12 #g2 #J #K2 #H elim (eq_inv_pr_push_next … H) | #f1 #f2 #I #L1 #L2 #H12 #g2 #J #K2 #H1 #H2 destruct - <(injective_next … H1) -g2 /3 width=5 by ex3_2_intro, or_introl/ + <(eq_inv_pr_next_bi … H1) -g2 /3 width=5 by ex3_2_intro, or_introl/ | #f #f0 #f1 #f2 #L1 #L2 #W #V #_ #_ #_ #g2 #J #K2 #_ #H destruct | #f #f0 #f1 #f2 #I1 #I2 #L1 #L2 #V #Hf #Hf1 #H12 #g2 #J #K2 #H1 #H2 destruct - <(injective_next … H1) -g2 /3 width=11 by ex5_6_intro, or_intror/ + <(eq_inv_pr_next_bi … H1) -g2 /3 width=11 by ex5_6_intro, or_intror/ ] qed-. @@ -262,9 +262,9 @@ qed-. lemma lsubf_inv_refl: ∀L,f1,f2. ❪L,f1❫ ⫃𝐅+ ❪L,f2❫ → f1 ≡ f2. #L elim L -L /2 width=1 by lsubf_inv_atom/ #L #I #IH #f1 #f2 #H12 -elim (pn_split f1) * #g1 #H destruct +elim (pr_map_split_tl f1) * #g1 #H destruct [ elim (lsubf_inv_push_sn … H12) | elim (lsubf_inv_bind_sn … H12) ] -H12 -#g2 #H12 #H destruct /3 width=5 by eq_next, eq_push/ +#g2 #H12 #H destruct /3 width=5 by pr_eq_next, pr_eq_push/ qed-. (* Basic forward lemmas *****************************************************) @@ -272,42 +272,42 @@ qed-. lemma lsubf_fwd_bind_tl: ∀f1,f2,I,L1,L2. ❪L1.ⓘ[I],f1❫ ⫃𝐅+ ❪L2.ⓘ[I],f2❫ → ❪L1,⫰f1❫ ⫃𝐅+ ❪L2,⫰f2❫. #f1 #f2 #I #L1 #L2 #H -elim (pn_split f1) * #g1 #H0 destruct +elim (pr_map_split_tl f1) * #g1 #H0 destruct [ elim (lsubf_inv_push_sn … H) | elim (lsubf_inv_bind_sn … H) ] -H #g2 #H12 #H destruct // qed-. lemma lsubf_fwd_isid_dx: ∀f1,f2,L1,L2. ❪L1,f1❫ ⫃𝐅+ ❪L2,f2❫ → 𝐈❪f2❫ → 𝐈❪f1❫. #f1 #f2 #L1 #L2 #H elim H -f1 -f2 -L1 -L2 -[ /2 width=3 by isid_eq_repl_fwd/ -| /4 width=3 by isid_inv_push, isid_push/ -| #f1 #f2 #I #L1 #L2 #_ #_ #H elim (isid_inv_next … H) -H // -| #f #f0 #f1 #f2 #L1 #L2 #W #V #_ #_ #_ #_ #H elim (isid_inv_next … H) -H // -| #f #f0 #f1 #f2 #I1 #I2 #L1 #L2 #V #_ #_ #_ #_ #H elim (isid_inv_next … H) -H // +[ /2 width=3 by pr_isi_eq_repl_fwd/ +| /4 width=3 by pr_isi_inv_push, pr_isi_push/ +| #f1 #f2 #I #L1 #L2 #_ #_ #H elim (pr_isi_inv_next … H) -H // +| #f #f0 #f1 #f2 #L1 #L2 #W #V #_ #_ #_ #_ #H elim (pr_isi_inv_next … H) -H // +| #f #f0 #f1 #f2 #I1 #I2 #L1 #L2 #V #_ #_ #_ #_ #H elim (pr_isi_inv_next … H) -H // ] qed-. lemma lsubf_fwd_isid_sn: ∀f1,f2,L1,L2. ❪L1,f1❫ ⫃𝐅+ ❪L2,f2❫ → 𝐈❪f1❫ → 𝐈❪f2❫. #f1 #f2 #L1 #L2 #H elim H -f1 -f2 -L1 -L2 -[ /2 width=3 by isid_eq_repl_back/ -| /4 width=3 by isid_inv_push, isid_push/ -| #f1 #f2 #I #L1 #L2 #_ #_ #H elim (isid_inv_next … H) -H // -| #f #f0 #f1 #f2 #L1 #L2 #W #V #_ #_ #_ #_ #H elim (isid_inv_next … H) -H // -| #f #f0 #f1 #f2 #I1 #I2 #L1 #L2 #V #_ #_ #_ #_ #H elim (isid_inv_next … H) -H // +[ /2 width=3 by pr_isi_eq_repl_back/ +| /4 width=3 by pr_isi_inv_push, pr_isi_push/ +| #f1 #f2 #I #L1 #L2 #_ #_ #H elim (pr_isi_inv_next … H) -H // +| #f #f0 #f1 #f2 #L1 #L2 #W #V #_ #_ #_ #_ #H elim (pr_isi_inv_next … H) -H // +| #f #f0 #f1 #f2 #I1 #I2 #L1 #L2 #V #_ #_ #_ #_ #H elim (pr_isi_inv_next … H) -H // ] qed-. lemma lsubf_fwd_sle: ∀f1,f2,L1,L2. ❪L1,f1❫ ⫃𝐅+ ❪L2,f2❫ → f2 ⊆ f1. #f1 #f2 #L1 #L2 #H elim H -f1 -f2 -L1 -L2 -/3 width=5 by sor_inv_sle_sn_trans, sle_next, sle_push, sle_refl_eq, eq_sym/ +/3 width=5 by pr_sor_inv_sle_sn_trans, pr_sle_next, pr_sle_push, pr_sle_refl_eq, pr_eq_sym/ qed-. (* Basic properties *********************************************************) -lemma lsubf_eq_repl_back1: ∀f2,L1,L2. eq_repl_back … (λf1. ❪L1,f1❫ ⫃𝐅+ ❪L2,f2❫). +lemma lsubf_eq_repl_back1: ∀f2,L1,L2. pr_eq_repl_back … (λf1. ❪L1,f1❫ ⫃𝐅+ ❪L2,f2❫). #f2 #L1 #L2 #f #H elim H -f -f2 -L1 -L2 [ #f1 #f2 #Hf12 #g1 #Hfg1 - /3 width=3 by lsubf_atom, eq_canc_sn/ + /3 width=3 by lsubf_atom, pr_eq_canc_sn/ | #f1 #f2 #I1 #I2 #K1 #K2 #_ #IH #g #H elim (eq_inv_px … H) -H [|*: // ] #g1 #Hfg1 #H destruct /3 width=1 by lsubf_push/ @@ -316,21 +316,21 @@ lemma lsubf_eq_repl_back1: ∀f2,L1,L2. eq_repl_back … (λf1. ❪L1,f1❫ ⫃ /3 width=1 by lsubf_bind/ | #f #f0 #f1 #f2 #K1 #L2 #W #V #Hf #Hf1 #_ #IH #g #H elim (eq_inv_nx … H) -H [|*: // ] #g1 #Hfg1 #H destruct - /3 width=5 by lsubf_beta, sor_eq_repl_back3/ + /3 width=5 by lsubf_beta, pr_sor_eq_repl_back/ | #f #f0 #f1 #f2 #I1 #I2 #K1 #K2 #V #Hf #Hf1 #_ #IH #g #H elim (eq_inv_nx … H) -H [|*: // ] #g1 #Hfg1 #H destruct - /3 width=5 by lsubf_unit, sor_eq_repl_back3/ + /3 width=5 by lsubf_unit, pr_sor_eq_repl_back/ ] qed-. -lemma lsubf_eq_repl_fwd1: ∀f2,L1,L2. eq_repl_fwd … (λf1. ❪L1,f1❫ ⫃𝐅+ ❪L2,f2❫). -#f2 #L1 #L2 @eq_repl_sym /2 width=3 by lsubf_eq_repl_back1/ +lemma lsubf_eq_repl_fwd1: ∀f2,L1,L2. pr_eq_repl_fwd … (λf1. ❪L1,f1❫ ⫃𝐅+ ❪L2,f2❫). +#f2 #L1 #L2 @pr_eq_repl_sym /2 width=3 by lsubf_eq_repl_back1/ qed-. -lemma lsubf_eq_repl_back2: ∀f1,L1,L2. eq_repl_back … (λf2. ❪L1,f1❫ ⫃𝐅+ ❪L2,f2❫). +lemma lsubf_eq_repl_back2: ∀f1,L1,L2. pr_eq_repl_back … (λf2. ❪L1,f1❫ ⫃𝐅+ ❪L2,f2❫). #f1 #L1 #L2 #f #H elim H -f1 -f -L1 -L2 [ #f1 #f2 #Hf12 #g2 #Hfg2 - /3 width=3 by lsubf_atom, eq_trans/ + /3 width=3 by lsubf_atom, pr_eq_trans/ | #f1 #f2 #I1 #I2 #K1 #K2 #_ #IH #g #H elim (eq_inv_px … H) -H [|*: // ] #g2 #Hfg2 #H destruct /3 width=1 by lsubf_push/ @@ -346,13 +346,13 @@ lemma lsubf_eq_repl_back2: ∀f1,L1,L2. eq_repl_back … (λf2. ❪L1,f1❫ ⫃ ] qed-. -lemma lsubf_eq_repl_fwd2: ∀f1,L1,L2. eq_repl_fwd … (λf2. ❪L1,f1❫ ⫃𝐅+ ❪L2,f2❫). -#f1 #L1 #L2 @eq_repl_sym /2 width=3 by lsubf_eq_repl_back2/ +lemma lsubf_eq_repl_fwd2: ∀f1,L1,L2. pr_eq_repl_fwd … (λf2. ❪L1,f1❫ ⫃𝐅+ ❪L2,f2❫). +#f1 #L1 #L2 @pr_eq_repl_sym /2 width=3 by lsubf_eq_repl_back2/ qed-. lemma lsubf_refl: bi_reflexive … lsubf. -#L elim L -L /2 width=1 by lsubf_atom, eq_refl/ -#L #I #IH #f elim (pn_split f) * #g #H destruct +#L elim L -L /2 width=1 by lsubf_atom, pr_eq_refl/ +#L #I #IH #f elim (pr_map_split_tl f) * #g #H destruct /2 width=1 by lsubf_push, lsubf_bind/ qed. @@ -363,7 +363,7 @@ lemma lsubf_bind_tl_dx: ∀g1,f2,I,L1,L2. ❪L1,g1❫ ⫃𝐅+ ❪L2,⫰f2❫ → ∃∃f1. ❪L1.ⓘ[I],f1❫ ⫃𝐅+ ❪L2.ⓘ[I],f2❫ & g1 = ⫰f1. #g1 #f2 #I #L1 #L2 #H -elim (pn_split f2) * #g2 #H2 destruct +elim (pr_map_split_tl f2) * #g2 #H2 destruct @ex2_intro [1,2,4,5: /2 width=2 by lsubf_push, lsubf_bind/ ] // (**) (* constructor needed *) qed-. @@ -372,8 +372,8 @@ lemma lsubf_beta_tl_dx: ∀f2,L2,W. ❪L1,f0❫ ⫃𝐅+ ❪L2,⫰f2❫ → ∃∃f1. ❪L1.ⓓⓝW.V,f1❫ ⫃𝐅+ ❪L2.ⓛW,f2❫ & ⫰f1 ⊆ g1. #f #f0 #g1 #L1 #V #Hf #Hg1 #f2 -elim (pn_split f2) * #x2 #H2 #L2 #W #HL12 destruct -[ /3 width=4 by lsubf_push, sor_inv_sle_sn, ex2_intro/ +elim (pr_map_split_tl f2) * #x2 #H2 #L2 #W #HL12 destruct +[ /3 width=4 by lsubf_push, pr_sor_inv_sle_sn, ex2_intro/ | @(ex2_intro … (↑g1)) /2 width=5 by lsubf_beta/ (**) (* full auto fails *) ] qed-. @@ -384,32 +384,32 @@ lemma lsubf_inv_sor_dx: ∀f2l,f2r. f2l⋓f2r ≘ f2 → ∃∃f1l,f1r. ❪L1,f1l❫ ⫃𝐅+ ❪L2,f2l❫ & ❪L1,f1r❫ ⫃𝐅+ ❪L2,f2r❫ & f1l⋓f1r ≘ f1. #f1 #f2 #L1 #L2 #H elim H -f1 -f2 -L1 -L2 -[ /3 width=7 by sor_eq_repl_fwd3, ex3_2_intro/ +[ /3 width=7 by pr_sor_eq_repl_fwd, ex3_2_intro/ | #g1 #g2 #I1 #I2 #L1 #L2 #_ #IH #f2l #f2r #H - elim (sor_inv_xxp … H) -H [|*: // ] #g2l #g2r #Hg2 #Hl #Hr destruct - elim (IH … Hg2) -g2 /3 width=11 by lsubf_push, sor_pp, ex3_2_intro/ + elim (pr_sor_inv_push … H) -H [|*: // ] #g2l #g2r #Hg2 #Hl #Hr destruct + elim (IH … Hg2) -g2 /3 width=11 by lsubf_push, pr_sor_push_bi, ex3_2_intro/ | #g1 #g2 #I #L1 #L2 #_ #IH #f2l #f2r #H - elim (sor_inv_xxn … H) -H [1,3,4: * |*: // ] #g2l #g2r #Hg2 #Hl #Hr destruct - elim (IH … Hg2) -g2 /3 width=11 by lsubf_push, lsubf_bind, sor_np, sor_pn, sor_nn, ex3_2_intro/ + elim (pr_sor_inv_next … H) -H [1,3,4: * |*: // ] #g2l #g2r #Hg2 #Hl #Hr destruct + elim (IH … Hg2) -g2 /3 width=11 by lsubf_push, lsubf_bind, pr_sor_next_push, pr_sor_push_next, pr_sor_next_bi, ex3_2_intro/ | #g #g0 #g1 #g2 #L1 #L2 #W #V #Hg #Hg1 #_ #IH #f2l #f2r #H - elim (sor_inv_xxn … H) -H [1,3,4: * |*: // ] #g2l #g2r #Hg2 #Hl #Hr destruct + elim (pr_sor_inv_next … H) -H [1,3,4: * |*: // ] #g2l #g2r #Hg2 #Hl #Hr destruct elim (IH … Hg2) -g2 #g1l #g1r #Hl #Hr #Hg0 - [ lapply (sor_comm_23 … Hg0 Hg1 ?) -g0 [3: |*: // ] #Hg1 - /3 width=11 by lsubf_push, lsubf_beta, sor_np, ex3_2_intro/ - | lapply (sor_assoc_dx … Hg1 … Hg0 ??) -g0 [3: |*: // ] #Hg1 - /3 width=11 by lsubf_push, lsubf_beta, sor_pn, ex3_2_intro/ - | lapply (sor_distr_dx … Hg0 … Hg1) -g0 [5: |*: // ] #Hg1 - /3 width=11 by lsubf_beta, sor_nn, ex3_2_intro/ + [ lapply (pr_sor_comm_23 … Hg0 Hg1 ?) -g0 [3: |*: // ] #Hg1 + /3 width=11 by lsubf_push, lsubf_beta, pr_sor_next_push, ex3_2_intro/ + | lapply (pr_sor_assoc_dx … Hg1 … Hg0 ??) -g0 [3: |*: // ] #Hg1 + /3 width=11 by lsubf_push, lsubf_beta, pr_sor_push_next, ex3_2_intro/ + | lapply (pr_sor_distr_dx … Hg0 … Hg1) -g0 [5: |*: // ] #Hg1 + /3 width=11 by lsubf_beta, pr_sor_next_bi, ex3_2_intro/ ] | #g #g0 #g1 #g2 #I1 #I2 #L1 #L2 #V #Hg #Hg1 #_ #IH #f2l #f2r #H - elim (sor_inv_xxn … H) -H [1,3,4: * |*: // ] #g2l #g2r #Hg2 #Hl #Hr destruct + elim (pr_sor_inv_next … H) -H [1,3,4: * |*: // ] #g2l #g2r #Hg2 #Hl #Hr destruct elim (IH … Hg2) -g2 #g1l #g1r #Hl #Hr #Hg0 - [ lapply (sor_comm_23 … Hg0 Hg1 ?) -g0 [3: |*: // ] #Hg1 - /3 width=11 by lsubf_push, lsubf_unit, sor_np, ex3_2_intro/ - | lapply (sor_assoc_dx … Hg1 … Hg0 ??) -g0 [3: |*: // ] #Hg1 - /3 width=11 by lsubf_push, lsubf_unit, sor_pn, ex3_2_intro/ - | lapply (sor_distr_dx … Hg0 … Hg1) -g0 [5: |*: // ] #Hg1 - /3 width=11 by lsubf_unit, sor_nn, ex3_2_intro/ + [ lapply (pr_sor_comm_23 … Hg0 Hg1 ?) -g0 [3: |*: // ] #Hg1 + /3 width=11 by lsubf_push, lsubf_unit, pr_sor_next_push, ex3_2_intro/ + | lapply (pr_sor_assoc_dx … Hg1 … Hg0 ??) -g0 [3: |*: // ] #Hg1 + /3 width=11 by lsubf_push, lsubf_unit, pr_sor_push_next, ex3_2_intro/ + | lapply (pr_sor_distr_dx … Hg0 … Hg1) -g0 [5: |*: // ] #Hg1 + /3 width=11 by lsubf_unit, pr_sor_next_bi, ex3_2_intro/ ] ] qed-. diff --git a/matita/matita/contribs/lambdadelta/static_2/static/lsubf_frees.ma b/matita/matita/contribs/lambdadelta/static_2/static/lsubf_frees.ma index de32a2f00..e36bc6729 100644 --- a/matita/matita/contribs/lambdadelta/static_2/static/lsubf_frees.ma +++ b/matita/matita/contribs/lambdadelta/static_2/static/lsubf_frees.ma @@ -25,9 +25,9 @@ lemma lsubf_frees_trans: [ /3 width=5 by lsubf_fwd_isid_dx, frees_sort/ | #f2 #i #Hf2 #g1 #Y1 #H elim (lsubf_inv_atom2 … H) -H #Hg1 #H destruct - elim (eq_inv_pushs_dx … Hg1) -Hg1 #g #Hg #H destruct + elim (pr_eq_inv_pushs_dx … Hg1) -Hg1 #g #Hg #H destruct elim (eq_inv_xn … Hg) -Hg - /3 width=3 by frees_atom, isid_eq_repl_fwd/ + /3 width=3 by frees_atom, pr_isi_eq_repl_fwd/ | #f2 #I #K2 #W #_ #IH #g1 #Y1 #H elim (lsubf_inv_pair2 … H) -H * [ #f1 #K1 #H12 #H1 #H2 destruct /3 width=1 by frees_pair/ | #f #f0 #f1 #K1 #V #H12 #Hf #Hf1 #H1 #H2 #H3 destruct @@ -37,7 +37,7 @@ lemma lsubf_frees_trans: [ #f1 #L1 #H12 #H1 #H2 destruct /3 width=5 by lsubf_fwd_isid_dx, frees_unit/ | #f #f0 #f1 #J #L1 #V #H12 #Hf #Hf1 #H1 #H2 destruct - /5 width=9 by lsubf_fwd_isid_dx, frees_eq_repl_back, frees_pair, sor_isid_inv_sn/ + /5 width=9 by lsubf_fwd_isid_dx, frees_eq_repl_back, frees_pair, pr_sor_inv_isi_sn/ ] | #f2 #I #L2 #i #_ #IH #g1 #L1 #H elim (lsubf_inv_push2 … H) -H /3 width=1 by frees_lref/ diff --git a/matita/matita/contribs/lambdadelta/static_2/static/lsubf_lsubf.ma b/matita/matita/contribs/lambdadelta/static_2/static/lsubf_lsubf.ma index 7d162a58e..8ad9f517d 100644 --- a/matita/matita/contribs/lambdadelta/static_2/static/lsubf_lsubf.ma +++ b/matita/matita/contribs/lambdadelta/static_2/static/lsubf_lsubf.ma @@ -27,16 +27,16 @@ theorem lsubf_sor: [ #L #g1 #f1 #H1 #g2 #f2 #H2 #g #Hg #f #Hf elim (lsubf_inv_atom1 … H1) -H1 #H1 #H destruct lapply (lsubf_inv_atom … H2) -H2 #H2 - /5 width=4 by lsubf_atom, sor_mono, sor_eq_repl_back2, sor_eq_repl_back1/ + /5 width=4 by lsubf_atom, pr_sor_mono, pr_sor_eq_repl_back_dx, pr_sor_eq_repl_back_sn/ | #K #J #IH #L #g1 #f1 #H1 #g2 #f2 #H2 #g #Hg #f #Hf - elim (pn_split g1) * #y1 #H destruct - elim (pn_split g2) * #y2 #H destruct - [ elim (sor_inv_ppx … Hg) -Hg [|*: // ] #y #Hy #H destruct + elim (pr_map_split_tl g1) * #y1 #H destruct + elim (pr_map_split_tl g2) * #y2 #H destruct + [ elim (pr_sor_inv_push_bi … Hg) -Hg [|*: // ] #y #Hy #H destruct elim (lsubf_inv_push1 … H1) -H1 #x1 #Z1 #Y1 #H1 #H #H0 destruct elim (lsubf_inv_push_sn … H2) -H2 #x2 #H2 #H destruct - elim (sor_inv_ppx … Hf) -Hf [|*: // ] #x #Hx #H destruct + elim (pr_sor_inv_push_bi … Hf) -Hf [|*: // ] #x #Hx #H destruct /3 width=8 by lsubf_push/ - | elim (sor_inv_pnx … Hg) -Hg [|*: // ] #y #Hy #H destruct + | elim (pr_sor_inv_push_next … Hg) -Hg [|*: // ] #y #Hy #H destruct elim (lsubf_inv_push1 … H1) -H1 #x1 #Z1 #Y1 #H1 #H #H0 destruct generalize in match H2; -H2 cases J -J #J [| #V ] #H2 [ elim (lsubf_inv_unit1 … H2) -H2 #x2 #Y2 #H2 #H #H0 destruct @@ -46,9 +46,9 @@ theorem lsubf_sor: | #y3 #y4 #x2 #Z2 #Y2 #H2 #Hy3 #Hy2 #H #H0 destruct ] ] - elim (sor_inv_pnx … Hf) -Hf [1,6,11,16:|*: // ] #x #Hx #H destruct - /3 width=12 by lsubf_unit, lsubf_beta, lsubf_bind, sor_assoc_sn/ - | elim (sor_inv_npx … Hg) -Hg [|*: // ] #y #Hy #H destruct + elim (pr_sor_inv_push_next … Hf) -Hf [1,6,11,16:|*: // ] #x #Hx #H destruct + /3 width=12 by lsubf_unit, lsubf_beta, lsubf_bind, pr_sor_assoc_sn/ + | elim (pr_sor_inv_next_push … Hg) -Hg [|*: // ] #y #Hy #H destruct elim (lsubf_inv_push1 … H2) -H2 #x2 #Z2 #Y2 #H2 #H #H0 destruct generalize in match H1; -H1 cases J -J #J [| #V ] #H1 [ elim (lsubf_inv_unit1 … H1) -H1 #x1 #Y1 #H1 #H #H0 destruct @@ -58,9 +58,9 @@ theorem lsubf_sor: | #y3 #y4 #x1 #Z1 #Y1 #H1 #Hy3 #Hy1 #H #H0 destruct ] ] - elim (sor_inv_npx … Hf) -Hf [1,6,11,16:|*: // ] #x #Hx #H destruct - /3 width=12 by lsubf_unit, lsubf_beta, lsubf_bind, sor_comm_23/ - | elim (sor_inv_nnx … Hg) -Hg [|*: // ] #y #Hy #H destruct + elim (pr_sor_inv_next_push … Hf) -Hf [1,6,11,16:|*: // ] #x #Hx #H destruct + /3 width=12 by lsubf_unit, lsubf_beta, lsubf_bind, pr_sor_comm_23/ + | elim (pr_sor_inv_next_bi … Hg) -Hg [|*: // ] #y #Hy #H destruct generalize in match H2; generalize in match H1; -H1 -H2 cases J -J #J [| #V ] #H1 #H2 [ elim (lsubf_inv_unit1 … H1) -H1 #x1 #Y1 #H1 #H #H0 destruct elim (lsubf_inv_bind_sn … H2) -H2 #x2 #H2 #H destruct @@ -70,15 +70,15 @@ theorem lsubf_sor: | #y3 #y4 #x1 #Y1 #W #U #H1 #Hy3 #Hy1 #H #H0 #H3 #H4 destruct elim (lsubf_inv_beta_sn … H2) -H2 #z3 #z4 #x2 #H2 #Hz3 #Hy2 #H destruct lapply (frees_mono … Hz3 … Hy3) -Hz3 #H3 - lapply (sor_eq_repl_back2 … Hy2 … H3) -z3 #Hy2 + lapply (pr_sor_eq_repl_back_dx … Hy2 … H3) -z3 #Hy2 | #y3 #y4 #x1 #Z1 #Y1 #H1 #Hy3 #Hy1 #H #H0 destruct elim (lsubf_inv_unit_sn … H2) -H2 #z3 #z4 #x2 #H2 #Hz3 #Hy2 #H destruct lapply (frees_mono … Hz3 … Hy3) -Hz3 #H3 - lapply (sor_eq_repl_back2 … Hy2 … H3) -z3 #Hy2 + lapply (pr_sor_eq_repl_back_dx … Hy2 … H3) -z3 #Hy2 ] ] - elim (sor_inv_nnx … Hf) -Hf [1,6,11,16:|*: // ] #x #Hx #H destruct - /3 width=12 by lsubf_unit, lsubf_beta, lsubf_bind, sor_coll_dx/ + elim (pr_sor_inv_next_bi … Hf) -Hf [1,6,11,16:|*: // ] #x #Hx #H destruct + /3 width=12 by lsubf_unit, lsubf_beta, lsubf_bind, pr_sor_coll_dx/ ] ] qed-. diff --git a/matita/matita/contribs/lambdadelta/static_2/static/lsubf_lsubr.ma b/matita/matita/contribs/lambdadelta/static_2/static/lsubf_lsubr.ma index 3e0ce90ba..3d4448a68 100644 --- a/matita/matita/contribs/lambdadelta/static_2/static/lsubf_lsubr.ma +++ b/matita/matita/contribs/lambdadelta/static_2/static/lsubf_lsubr.ma @@ -22,11 +22,11 @@ include "static_2/static/lsubf_lsubf.ma". lemma lsubf_fwd_lsubr_isdiv: ∀f1,f2,L1,L2. ❪L1,f1❫ ⫃𝐅+ ❪L2,f2❫ → 𝛀❪f1❫ → 𝛀❪f2❫ → L1 ⫃ L2. #f1 #f2 #L1 #L2 #H elim H -f1 -f2 -L1 -L2 -/4 width=3 by lsubr_bind, isdiv_inv_next/ +/4 width=3 by lsubr_bind, pr_isd_inv_next/ [ #f1 #f2 #I1 #I2 #L1 #L2 #_ #_ #H - elim (isdiv_inv_push … H) // -| /5 width=5 by lsubf_fwd_sle, lsubr_beta, sle_inv_isdiv_sn, isdiv_inv_next/ -| /5 width=5 by lsubf_fwd_sle, lsubr_unit, sle_inv_isdiv_sn, isdiv_inv_next/ + elim (pr_isd_inv_push … H) // +| /5 width=5 by lsubf_fwd_sle, lsubr_beta, pr_sle_inv_isd_sn, pr_isd_inv_next/ +| /5 width=5 by lsubf_fwd_sle, lsubr_unit, pr_sle_inv_isd_sn, pr_isd_inv_next/ ] qed-. @@ -35,12 +35,12 @@ qed-. lemma lsubr_lsubf_isid: ∀L1,L2. L1 ⫃ L2 → ∀f1,f2. 𝐈❪f1❫ → 𝐈❪f2❫ → ❪L1,f1❫ ⫃𝐅+ ❪L2,f2❫. #L1 #L2 #H elim H -L1 -L2 -[ /3 width=1 by lsubf_atom, isid_inv_eq_repl/ +[ /3 width=1 by lsubf_atom, pr_isi_inv_eq_repl/ | #I #L1 #L2 | #L1 #L2 #V #W | #I1 #I2 #L1 #L2 #V ] #_ #IH #f1 #f2 #Hf1 #Hf2 -elim (isid_inv_gen … Hf1) -Hf1 #g1 #Hg1 #H destruct -elim (isid_inv_gen … Hf2) -Hf2 #g2 #Hg2 #H destruct +elim (pr_isi_inv_gen … Hf1) -Hf1 #g1 #Hg1 #H destruct +elim (pr_isi_inv_gen … Hf2) -Hf2 #g2 #Hg2 #H destruct /3 width=1 by lsubf_push/ qed. @@ -53,7 +53,7 @@ lemma lsubr_lsubf: | #f2 #i #Hf2 #Y1 #HY1 >(lsubr_inv_atom2 … HY1) -Y1 #g1 #Hg1 elim (frees_inv_atom … Hg1) -Hg1 #f1 #Hf1 #H destruct - /5 width=5 by lsubf_atom, isid_inv_eq_repl, pushs_eq_repl, eq_next/ + /5 width=5 by lsubf_atom, pr_isi_inv_eq_repl, pr_pushs_eq_repl, pr_eq_next/ | #f2 #Z #L2 #W #_ #IH #Y1 #HY1 #g1 #Hg1 elim (lsubr_inv_pair2 … HY1) -HY1 * [ #L1 #HL12 #H destruct elim (frees_inv_pair … Hg1) -Hg1 #f1 #Hf1 #H destruct @@ -68,7 +68,7 @@ lemma lsubr_lsubf: /3 width=1 by lsubf_bind, lsubr_lsubf_isid/ | #I #L1 #V #HL12 #H destruct elim (frees_inv_pair … Hg1) -Hg1 #f1 #Hf1 #H destruct - /3 width=5 by lsubf_unit, sor_isid_sn, lsubr_lsubf_isid/ + /3 width=5 by lsubf_unit, pr_sor_isi_sn, lsubr_lsubf_isid/ ] | #f2 #I2 #L2 #i #_ #IH #Y1 #HY1 #g1 #Hg1 elim (lsubr_fwd_bind2 … HY1) -HY1 #I1 #L1 #HL12 #H destruct diff --git a/matita/matita/contribs/lambdadelta/static_2/static/req.ma b/matita/matita/contribs/lambdadelta/static_2/static/req.ma index 59efd1af8..93aaafbb4 100644 --- a/matita/matita/contribs/lambdadelta/static_2/static/req.ma +++ b/matita/matita/contribs/lambdadelta/static_2/static/req.ma @@ -20,7 +20,7 @@ include "static_2/static/reqg.ma". (* Basic_2A1: was: lleq *) definition req: relation3 term lenv lenv ≝ - reqg (eq …). + reqg (pr_eq …). interpretation "syntactic equivalence on referred entries (local environment)" diff --git a/matita/matita/contribs/lambdadelta/static_2/static/reqg.ma b/matita/matita/contribs/lambdadelta/static_2/static/reqg.ma index 1c5d5ed90..93f10a93d 100644 --- a/matita/matita/contribs/lambdadelta/static_2/static/reqg.ma +++ b/matita/matita/contribs/lambdadelta/static_2/static/reqg.ma @@ -59,10 +59,10 @@ lemma frees_teqg_conf_seqg (S): >(teqg_inv_gref1 … H1) -X /2 width=1 by frees_gref/ | #f1V #f1T #f1 #p #I #L1 #V1 #T1 #_ #_ #Hf1 #IHV #IHT #X #H1 elim (teqg_inv_pair1 … H1) -H1 #V2 #T2 #HV12 #HT12 #H1 #L2 #HL12 destruct - /6 width=5 by frees_bind, sex_inv_tl, ext2_pair, sle_sex_trans, sor_inv_sle_dx, sor_inv_sle_sn/ + /6 width=5 by frees_bind, sex_inv_tl, ext2_pair, sle_sex_trans, pr_sor_inv_sle_dx, pr_sor_inv_sle_sn/ | #f1V #f1T #f1 #I #L1 #V1 #T1 #_ #_ #Hf1 #IHV #IHT #X #H1 elim (teqg_inv_pair1 … H1) -H1 #V2 #T2 #HV12 #HT12 #H1 #L2 #HL12 destruct - /5 width=5 by frees_flat, sle_sex_trans, sor_inv_sle_dx, sor_inv_sle_sn/ + /5 width=5 by frees_flat, sle_sex_trans, pr_sor_inv_sle_dx, pr_sor_inv_sle_sn/ ] qed-. diff --git a/matita/matita/contribs/lambdadelta/static_2/static/reqg_reqg.ma b/matita/matita/contribs/lambdadelta/static_2/static/reqg_reqg.ma index cb01ec662..c5ad7a7b7 100644 --- a/matita/matita/contribs/lambdadelta/static_2/static/reqg_reqg.ma +++ b/matita/matita/contribs/lambdadelta/static_2/static/reqg_reqg.ma @@ -33,7 +33,7 @@ lemma reqg_fsle_comp (S): rex_fsle_compatible (ceqg S). #S #HS #L1 #L2 #T #HL12 elim (frees_total L1 T) #f #Hf -/4 width=8 by frees_reqg_conf, rex_fwd_length, lveq_length_eq, sle_refl, ex4_4_intro/ +/4 width=8 by frees_reqg_conf, rex_fwd_length, lveq_length_eq, pr_sle_refl, ex4_4_intro/ qed. (* Advanced properties ******************************************************) diff --git a/matita/matita/contribs/lambdadelta/static_2/static/rex.ma b/matita/matita/contribs/lambdadelta/static_2/static/rex.ma index 0eb1164eb..45e9028d7 100644 --- a/matita/matita/contribs/lambdadelta/static_2/static/rex.ma +++ b/matita/matita/contribs/lambdadelta/static_2/static/rex.ma @@ -80,7 +80,7 @@ lemma rex_inv_sort (R): #R * [ | #Y1 #I1 ] #Y2 #s * #f #H1 #H2 [ lapply (sex_inv_atom1 … H2) -H2 /3 width=1 by or_introl, conj/ | lapply (frees_inv_sort … H1) -H1 #Hf - elim (isid_inv_gen … Hf) -Hf #g #Hg #H destruct + elim (pr_isi_inv_gen … Hf) -Hf #g #Hg #H destruct elim (sex_inv_push1 … H2) -H2 #I2 #L2 #H12 #_ #H destruct /5 width=7 by frees_sort, ex3_4_intro, ex2_intro, or_intror/ ] @@ -122,7 +122,7 @@ lemma rex_inv_gref (R): #R * [ | #Y1 #I1 ] #Y2 #l * #f #H1 #H2 [ lapply (sex_inv_atom1 … H2) -H2 /3 width=1 by or_introl, conj/ | lapply (frees_inv_gref … H1) -H1 #Hf - elim (isid_inv_gen … Hf) -Hf #g #Hg #H destruct + elim (pr_isi_inv_gen … Hf) -Hf #g #Hg #H destruct elim (sex_inv_push1 … H2) -H2 #I2 #L2 #H12 #_ #H destruct /5 width=7 by frees_gref, ex3_4_intro, ex2_intro, or_intror/ ] @@ -133,7 +133,7 @@ lemma rex_inv_bind (R): ∀p,I,L1,L2,V1,V2,T. L1 ⪤[R,ⓑ[p,I]V1.T] L2 → R L1 V1 V2 → ∧∧ L1 ⪤[R,V1] L2 & L1.ⓑ[I]V1 ⪤[R,T] L2.ⓑ[I]V2. #R #p #I #L1 #L2 #V1 #V2 #T * #f #Hf #HL #HV elim (frees_inv_bind … Hf) -Hf -/6 width=6 by sle_sex_trans, sex_inv_tl, ext2_pair, sor_inv_sle_dx, sor_inv_sle_sn, ex2_intro, conj/ +/6 width=6 by sle_sex_trans, sex_inv_tl, ext2_pair, pr_sor_inv_sle_dx, pr_sor_inv_sle_sn, ex2_intro, conj/ qed-. (* Basic_2A1: uses: llpx_sn_inv_flat *) @@ -141,7 +141,7 @@ lemma rex_inv_flat (R): ∀I,L1,L2,V,T. L1 ⪤[R,ⓕ[I]V.T] L2 → ∧∧ L1 ⪤[R,V] L2 & L1 ⪤[R,T] L2. #R #I #L1 #L2 #V #T * #f #Hf #HL elim (frees_inv_flat … Hf) -Hf -/5 width=6 by sle_sex_trans, sor_inv_sle_dx, sor_inv_sle_sn, ex2_intro, conj/ +/5 width=6 by sle_sex_trans, pr_sor_inv_sle_dx, pr_sor_inv_sle_sn, ex2_intro, conj/ qed-. (* Advanced inversion lemmas ************************************************) @@ -255,7 +255,7 @@ lemma rex_fwd_pair_sn (R): ∀I,L1,L2,V,T. L1 ⪤[R,②[I]V.T] L2 → L1 ⪤[R,V] L2. #R * [ #p ] #I #L1 #L2 #V #T * #f #Hf #HL [ elim (frees_inv_bind … Hf) | elim (frees_inv_flat … Hf) ] -Hf -/4 width=6 by sle_sex_trans, sor_inv_sle_sn, ex2_intro/ +/4 width=6 by sle_sex_trans, pr_sor_inv_sle_sn, ex2_intro/ qed-. (* Basic_2A1: uses: llpx_sn_fwd_bind_dx llpx_sn_fwd_bind_O_dx *) @@ -274,7 +274,7 @@ qed-. lemma rex_fwd_dx (R): ∀I2,L1,K2,T. L1 ⪤[R,T] K2.ⓘ[I2] → ∃∃I1,K1. L1 = K1.ⓘ[I1]. -#R #I2 #L1 #K2 #T * #f elim (pn_split f) * #g #Hg #_ #Hf destruct +#R #I2 #L1 #K2 #T * #f elim (pr_map_split_tl f) * #g #Hg #_ #Hf destruct [ elim (sex_inv_push2 … Hf) | elim (sex_inv_next2 … Hf) ] -Hf #I1 #K1 #_ #_ #H destruct /2 width=3 by ex1_2_intro/ qed-. @@ -290,7 +290,7 @@ lemma rex_sort (R): ∀I1,I2,L1,L2,s. L1 ⪤[R,⋆s] L2 → L1.ⓘ[I1] ⪤[R,⋆s] L2.ⓘ[I2]. #R #I1 #I2 #L1 #L2 #s * #f #Hf #H12 lapply (frees_inv_sort … Hf) -Hf -/4 width=3 by frees_sort, sex_push, isid_push, ex2_intro/ +/4 width=3 by frees_sort, sex_push, pr_isi_push, ex2_intro/ qed. lemma rex_pair (R): @@ -314,7 +314,7 @@ lemma rex_gref (R): ∀I1,I2,L1,L2,l. L1 ⪤[R,§l] L2 → L1.ⓘ[I1] ⪤[R,§l] L2.ⓘ[I2]. #R #I1 #I2 #L1 #L2 #l * #f #Hf #H12 lapply (frees_inv_gref … Hf) -Hf -/4 width=3 by frees_gref, sex_push, isid_push, ex2_intro/ +/4 width=3 by frees_gref, sex_push, pr_isi_push, ex2_intro/ qed. lemma rex_bind_repl_dx (R): diff --git a/matita/matita/contribs/lambdadelta/static_2/static/rex_fqup.ma b/matita/matita/contribs/lambdadelta/static_2/static/rex_fqup.ma index 063832841..5454bc032 100644 --- a/matita/matita/contribs/lambdadelta/static_2/static/rex_fqup.ma +++ b/matita/matita/contribs/lambdadelta/static_2/static/rex_fqup.ma @@ -30,7 +30,7 @@ lemma rex_pair_refl (R): ∀L,V1,V2. R L V1 V2 → ∀I,T. L.ⓑ[I]V1 ⪤[R,T] L.ⓑ[I]V2. #R #HR #L #V1 #V2 #HV12 #I #T elim (frees_total (L.ⓑ[I]V1) T) #f #Hf -elim (pn_split f) * #g #H destruct +elim (pr_map_split_tl f) * #g #H destruct /5 width=3 by sex_refl, sex_next, sex_push, ext2_refl, ext2_pair, ex2_intro/ qed. @@ -39,7 +39,7 @@ qed. lemma rex_inv_bind_void (R): ∀p,I,L1,L2,V,T. L1 ⪤[R,ⓑ[p,I]V.T] L2 → L1 ⪤[R,V] L2 ∧ L1.ⓧ ⪤[R,T] L2.ⓧ. #R #p #I #L1 #L2 #V #T * #f #Hf #HL elim (frees_inv_bind_void … Hf) -Hf -/6 width=6 by sle_sex_trans, sex_inv_tl, sor_inv_sle_dx, sor_inv_sle_sn, ex2_intro, conj/ +/6 width=6 by sle_sex_trans, sex_inv_tl, pr_sor_inv_sle_dx, pr_sor_inv_sle_sn, ex2_intro, conj/ qed-. (* Advanced forward lemmas **************************************************) diff --git a/matita/matita/contribs/lambdadelta/static_2/static/rex_fsle.ma b/matita/matita/contribs/lambdadelta/static_2/static/rex_fsle.ma index e3914f23a..8e1fbedef 100644 --- a/matita/matita/contribs/lambdadelta/static_2/static/rex_fsle.ma +++ b/matita/matita/contribs/lambdadelta/static_2/static/rex_fsle.ma @@ -83,8 +83,8 @@ lemma rex_pair_sn_split (R1) (R2): elim (frees_inv_flat … Hg) #y1 #y2 #H #_ #Hy ] lapply(frees_mono … H … Hf) -H #H1 -lapply (sor_eq_repl_back1 … Hy … H1) -y1 #Hy -lapply (sor_inv_sle_sn … Hy) -y2 #Hfg +lapply (pr_sor_eq_repl_back_sn … Hy … H1) -y1 #Hy +lapply (pr_sor_inv_sle_sn … Hy) -y2 #Hfg elim (sex_sle_split_sn (cext2 R1) (cext2 R2) … HL12 … Hfg) -HL12 /2 width=1 by ext2_refl/ #L #HL1 #HL2 lapply (sle_sex_trans … HL1 … Hfg) // #H elim (frees_sex_conf_fsge … Hf … H) -Hf -H @@ -100,8 +100,8 @@ lemma rex_flat_dx_split (R1) (R2): elim (frees_total L1 (ⓕ[I]V.T)) #g #Hg elim (frees_inv_flat … Hg) #y1 #y2 #_ #H #Hy lapply(frees_mono … H … Hf) -H #H2 -lapply (sor_eq_repl_back2 … Hy … H2) -y2 #Hy -lapply (sor_inv_sle_dx … Hy) -y1 #Hfg +lapply (pr_sor_eq_repl_back_dx … Hy … H2) -y2 #Hy +lapply (pr_sor_inv_sle_dx … Hy) -y1 #Hfg elim (sex_sle_split_sn (cext2 R1) (cext2 R2) … HL12 … Hfg) -HL12 /2 width=1 by ext2_refl/ #L #HL1 #HL2 lapply (sle_sex_trans … HL1 … Hfg) // #H elim (frees_sex_conf_fsge … Hf … H) -Hf -H @@ -117,10 +117,10 @@ lemma rex_bind_dx_split (R1) (R2): elim (frees_total L1 (ⓑ[p,I]V1.T)) #g #Hg elim (frees_inv_bind … Hg) #y1 #y2 #_ #H #Hy lapply(frees_mono … H … Hf) -H #H2 -lapply (tl_eq_repl … H2) -H2 #H2 -lapply (sor_eq_repl_back2 … Hy … H2) -y2 #Hy -lapply (sor_inv_sle_dx … Hy) -y1 #Hfg -lapply (sle_inv_tl_sn … Hfg) -Hfg #Hfg +lapply (pr_tl_eq_repl … H2) -H2 #H2 +lapply (pr_sor_eq_repl_back_dx … Hy … H2) -y2 #Hy +lapply (pr_sor_inv_sle_dx … Hy) -y1 #Hfg +lapply (pr_sle_inv_tl_sn … Hfg) -Hfg #Hfg elim (sex_sle_split_sn (cext2 R1) (cext2 R2) … HL12 … Hfg) -HL12 /2 width=1 by ext2_refl/ #Y #H #HL2 lapply (sle_sex_trans … H … Hfg) // #H0 elim (sex_inv_next1 … H) -H #Z #L #HL1 #H @@ -138,10 +138,10 @@ lemma rex_bind_dx_split_void (R1) (R2): elim (frees_total L1 (ⓑ[p,I]V.T)) #g #Hg elim (frees_inv_bind_void … Hg) #y1 #y2 #_ #H #Hy lapply(frees_mono … H … Hf) -H #H2 -lapply (tl_eq_repl … H2) -H2 #H2 -lapply (sor_eq_repl_back2 … Hy … H2) -y2 #Hy -lapply (sor_inv_sle_dx … Hy) -y1 #Hfg -lapply (sle_inv_tl_sn … Hfg) -Hfg #Hfg +lapply (pr_tl_eq_repl … H2) -H2 #H2 +lapply (pr_sor_eq_repl_back_dx … Hy … H2) -y2 #Hy +lapply (pr_sor_inv_sle_dx … Hy) -y1 #Hfg +lapply (pr_sle_inv_tl_sn … Hfg) -Hfg #Hfg elim (sex_sle_split_sn (cext2 R1) (cext2 R2) … HL12 … Hfg) -HL12 /2 width=1 by ext2_refl/ #Y #H #HL2 lapply (sle_sex_trans … H … Hfg) // #H0 elim (sex_inv_next1 … H) -H #Z #L #HL1 #H diff --git a/matita/matita/contribs/lambdadelta/static_2/static/rex_lex.ma b/matita/matita/contribs/lambdadelta/static_2/static/rex_lex.ma index e43cd5459..3fb780bb8 100644 --- a/matita/matita/contribs/lambdadelta/static_2/static/rex_lex.ma +++ b/matita/matita/contribs/lambdadelta/static_2/static/rex_lex.ma @@ -24,7 +24,7 @@ lemma rex_lex (R): ∀L1,L2. L1 ⪤[R] L2 → ∀T. L1 ⪤[R,T] L2. #R #L1 #L2 * #f #Hf #HL12 #T elim (frees_total L1 T) #g #Hg -/4 width=5 by sex_sdj, sdj_isid_sn, ex2_intro/ +/4 width=5 by sex_sdj, pr_sdj_isi_sn, ex2_intro/ qed. (* Inversion lemmas with generic extension of a context sensitive relation **) @@ -36,9 +36,9 @@ lemma rex_inv_req_lex (R): #R #H1R #H2R #L1 #L2 #T * #f1 #Hf1 #HL elim (sex_sdj_split_dx … ceq_ext … HL 𝐢) -HL [ #L0 #HL10 #HL02 - lapply (sex_sdj … HL02 f1 ?) /2 width=1 by sdj_isid_sn/ #H + lapply (sex_sdj … HL02 f1 ?) /2 width=1 by pr_sdj_isi_sn/ #H /3 width=5 by (* 2x *) ex2_intro/ -|*: /2 width=1 by ext2_refl, sdj_isid_dx/ +|*: /2 width=1 by ext2_refl, pr_sdj_isi_dx/ #g #I #K #n #HLK #Hg @H2R /width=7 by/ (**) (* no auto with H2R *) ] qed-. @@ -51,8 +51,8 @@ lemma rex_fwd_lex_req (R): ∃∃L. L1 ⪤[R] L & L ≡[T] L2. #R #H1R #H2R #L1 #L2 #T * #f1 #Hf1 #HL elim (sex_sdj_split_sn … ceq_ext … HL 𝐢 ?) -HL -[ #L0 #HL10 #HL02 |*: /2 width=1 by ext2_refl, sdj_isid_dx/ ] -H1R -lapply (sex_sdj … HL10 f1 ?) /2 width=1 by sdj_isid_sn/ #H +[ #L0 #HL10 #HL02 |*: /2 width=1 by ext2_refl, pr_sdj_isi_dx/ ] -H1R +lapply (sex_sdj … HL10 f1 ?) /2 width=1 by pr_sdj_isi_sn/ #H elim (frees_sex_conf_fsge … Hf1 … H) // -H2R -H #f0 #Hf0 #Hf01 /4 width=7 by sle_sex_trans, (* 2x *) ex2_intro/ qed-. diff --git a/matita/matita/contribs/lambdadelta/static_2/static/rex_rex.ma b/matita/matita/contribs/lambdadelta/static_2/static/rex_rex.ma index ba250697a..e3d0aee79 100644 --- a/matita/matita/contribs/lambdadelta/static_2/static/rex_rex.ma +++ b/matita/matita/contribs/lambdadelta/static_2/static/rex_rex.ma @@ -45,22 +45,22 @@ theorem rex_bind (R) (p) (I): ∀L1,L2,V1,V2,T. L1 ⪤[R,V1] L2 → L1.ⓑ[I]V1 ⪤[R,T] L2.ⓑ[I]V2 → L1 ⪤[R,ⓑ[p,I]V1.T] L2. #R #p #I #L1 #L2 #V1 #V2 #T * #f1 #HV #Hf1 * #f2 #HT #Hf2 -lapply (sex_fwd_bind … Hf2) -Hf2 #Hf2 elim (sor_isfin_ex f1 (⫰f2)) -/3 width=7 by frees_fwd_isfin, frees_bind, sex_join, isfin_tl, ex2_intro/ +lapply (sex_fwd_bind … Hf2) -Hf2 #Hf2 elim (pr_sor_isf_bi f1 (⫰f2)) +/3 width=7 by frees_fwd_isfin, frees_bind, sex_join, pr_isf_tl, ex2_intro/ qed. (* Basic_2A1: llpx_sn_flat *) theorem rex_flat (R) (I): ∀L1,L2,V,T. L1 ⪤[R,V] L2 → L1 ⪤[R,T] L2 → L1 ⪤[R,ⓕ[I]V.T] L2. -#R #I #L1 #L2 #V #T * #f1 #HV #Hf1 * #f2 #HT #Hf2 elim (sor_isfin_ex f1 f2) +#R #I #L1 #L2 #V #T * #f1 #HV #Hf1 * #f2 #HT #Hf2 elim (pr_sor_isf_bi f1 f2) /3 width=7 by frees_fwd_isfin, frees_flat, sex_join, ex2_intro/ qed. theorem rex_bind_void (R) (p) (I): ∀L1,L2,V,T. L1 ⪤[R,V] L2 → L1.ⓧ ⪤[R,T] L2.ⓧ → L1 ⪤[R,ⓑ[p,I]V.T] L2. #R #p #I #L1 #L2 #V #T * #f1 #HV #Hf1 * #f2 #HT #Hf2 -lapply (sex_fwd_bind … Hf2) -Hf2 #Hf2 elim (sor_isfin_ex f1 (⫰f2)) -/3 width=7 by frees_fwd_isfin, frees_bind_void, sex_join, isfin_tl, ex2_intro/ +lapply (sex_fwd_bind … Hf2) -Hf2 #Hf2 elim (pr_sor_isf_bi f1 (⫰f2)) +/3 width=7 by frees_fwd_isfin, frees_bind_void, sex_join, pr_isf_tl, ex2_intro/ qed. (* Negated inversion lemmas *************************************************) diff --git a/matita/matita/contribs/lambdadelta/static_2/syntax/ac.ma b/matita/matita/contribs/lambdadelta/static_2/syntax/ac.ma index aa9b4db7b..2d7d320e8 100644 --- a/matita/matita/contribs/lambdadelta/static_2/syntax/ac.ma +++ b/matita/matita/contribs/lambdadelta/static_2/syntax/ac.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "ground/lib/arith.ma". +include "ground/arith/nat_le.ma". include "static_2/notation/functions/one_0.ma". include "static_2/notation/functions/two_0.ma". include "static_2/notation/functions/omega_0.ma". @@ -46,13 +46,13 @@ qed. definition ac_eq (k): ac ≝ mk_ac (eq … k). interpretation "one (applicability domain)" - 'Two = (ac_eq (S O)). + 'Two = (ac_eq (nsucc nzero)). interpretation "zero (applicability domain)" - 'One = (ac_eq O). + 'One = (ac_eq nzero). lemma ac_eq_props (k): ac_props (ac_eq k) ≝ mk_ac_props …. -#m elim (le_dec m k) #Hm +#m elim (nle_dec m k) #Hm [ /3 width=3 by or_introl, ex2_intro/ | @or_intror * #n #Hn #Hmn destruct /2 width=1 by/ ] @@ -61,9 +61,9 @@ qed. definition ac_le (k): ac ≝ mk_ac (λn. n ≤ k). lemma ac_le_props (k): ac_props (ac_le k) ≝ mk_ac_props …. -#m elim (le_dec m k) #Hm +#m elim (nle_dec m k) #Hm [ /3 width=3 by or_introl, ex2_intro/ | @or_intror * #n #Hn #Hmn - /3 width=3 by transitive_le/ + /3 width=3 by nle_trans/ ] qed. diff --git a/matita/matita/contribs/lambdadelta/static_2/syntax/acle.ma b/matita/matita/contribs/lambdadelta/static_2/syntax/acle.ma index 30a025356..52f8e6797 100644 --- a/matita/matita/contribs/lambdadelta/static_2/syntax/acle.ma +++ b/matita/matita/contribs/lambdadelta/static_2/syntax/acle.ma @@ -45,12 +45,12 @@ qed. lemma acle_le_monotonic_le (k1) (k2): k1 ≤ k2 → (ac_le k1) ⊆ (ac_le k2). #k1 #k2 #Hk #m #Hm -/3 width=3 by acle_refl, transitive_le/ +/3 width=3 by acle_refl, nle_trans/ qed. lemma acle_eq_le (k): (ac_eq k) ⊆ (ac_le k). #k #m #Hm destruct -/2 width=1 by acle_refl, le_n/ +/2 width=1 by nle_refl, acle_refl/ qed. lemma acle_le_eq (k): (ac_le k) ⊆ (ac_eq k). diff --git a/matita/matita/contribs/lambdadelta/static_2/syntax/acle_acle.ma b/matita/matita/contribs/lambdadelta/static_2/syntax/acle_acle.ma index 9b8998900..2edee6e4c 100644 --- a/matita/matita/contribs/lambdadelta/static_2/syntax/acle_acle.ma +++ b/matita/matita/contribs/lambdadelta/static_2/syntax/acle_acle.ma @@ -22,5 +22,5 @@ theorem acle_trans: Transitive … acle. #a1 #a #Ha1 #a2 #Ha2 #m1 #Hm1 elim (Ha1 … Hm1) -Ha1 -Hm1 #m #Ha #Hm1 elim (Ha2 … Ha) -Ha2 -Ha #m2 #Ha2 #Hm2 -/3 width=5 by transitive_le, ex2_intro/ +/3 width=5 by nle_trans, ex2_intro/ qed-. diff --git a/matita/matita/contribs/lambdadelta/static_2/syntax/append.ma b/matita/matita/contribs/lambdadelta/static_2/syntax/append.ma index 220944f49..0377292d6 100644 --- a/matita/matita/contribs/lambdadelta/static_2/syntax/append.ma +++ b/matita/matita/contribs/lambdadelta/static_2/syntax/append.ma @@ -28,7 +28,7 @@ rec definition append L K on K ≝ match K with | LBind K I ⇒ (append L K).ⓘ[I] ]. -interpretation "append (local environment)" 'plus L1 L2 = (append L1 L2). +interpretation "append (local environment)" 'nplus L1 L2 = (append L1 L2). interpretation "local environment tail binding construction (generic)" 'SnItem I L = (append (LBind LAtom I) L). diff --git a/matita/matita/contribs/lambdadelta/static_2/syntax/append_length.ma b/matita/matita/contribs/lambdadelta/static_2/syntax/append_length.ma index c76a2a6e7..2222c52ff 100644 --- a/matita/matita/contribs/lambdadelta/static_2/syntax/append_length.ma +++ b/matita/matita/contribs/lambdadelta/static_2/syntax/append_length.ma @@ -72,12 +72,12 @@ lemma append_inj_length_dx: ∀K1,K2,L1,L2. L1 + K1 = L2 + K2 → |L1| = |L2| #K1 elim K1 -K1 [ * /2 width=1 by conj/ #K2 #I2 #L1 #L2 >append_atom >append_bind #H destruct - >length_bind >append_length >plus_n_Sm - #H elim (plus_xSy_x_false … H) + >length_bind >append_length >nplus_succ_dx + #H elim (succ_nplus_refl_sn … H) | #K1 #I1 #IH * [ #L1 #L2 >append_bind >append_atom #H destruct - >length_bind >append_length >plus_n_Sm #H - lapply (discr_plus_x_xy … H) -H #H destruct + >length_bind >append_length >nplus_succ_dx #H + lapply (nplus_refl_sn … H) -H #H destruct | #K2 #I2 #L1 #L2 >append_bind >append_bind #H1 #H2 elim (destruct_lbind_lbind_aux … H1) -H1 #H1 #H3 destruct (**) (* destruct lemma needed *) elim (IH … H1) -IH -H1 /2 width=1 by conj/ @@ -105,7 +105,7 @@ qed-. (* Basic_2A1: was: lenv_ind_alt *) lemma lenv_ind_tail: ∀Q:predicate lenv. Q (⋆) → (∀I,L. Q L → Q (ⓘ[I].L)) → ∀L. Q L. -#Q #IH1 #IH2 #L @(f_ind … length … L) -L #x #IHx * // +#Q #IH1 #IH2 #L @(wf1_ind_nlt … length … L) -L #x #IHx * // #L #I -IH1 #H destruct elim (lenv_case_tail … L) [2: * #K #J ] #H destruct /3 width=1 by/ diff --git a/matita/matita/contribs/lambdadelta/static_2/syntax/cl_restricted_weight.ma b/matita/matita/contribs/lambdadelta/static_2/syntax/cl_restricted_weight.ma index 8340649d8..62ce9d6fc 100644 --- a/matita/matita/contribs/lambdadelta/static_2/syntax/cl_restricted_weight.ma +++ b/matita/matita/contribs/lambdadelta/static_2/syntax/cl_restricted_weight.ma @@ -25,11 +25,11 @@ interpretation "weight (restricted closure)" 'Weight L T = (rfw L T). (* Basic_1: was: flt_shift *) lemma rfw_shift: ∀p,I,K,V,T. ♯❨K.ⓑ[I]V,T❩ < ♯❨K,ⓑ[p,I]V.T❩. -normalize /2 width=1 by monotonic_le_plus_r/ +normalize /2 width=1 by nle_plus_bi_sn/ qed. lemma rfw_clear: ∀p,I1,I2,K,V,T. ♯❨K.ⓤ[I1],T❩ < ♯❨K,ⓑ[p,I2]V.T❩. -normalize /4 width=1 by monotonic_le_plus_r, le_S_S/ +normalize /4 width=1 by nle_plus_bi_sn, nle_succ_bi/ qed. lemma rfw_tpair_sn: ∀I,L,V,T. ♯❨L,V❩ < ♯❨L,②[I]V.T❩. @@ -41,11 +41,11 @@ normalize in ⊢ (?→?→?→?→?%%); // qed. lemma rfw_lpair_sn: ∀I,L,V,T. ♯❨L,V❩ < ♯❨L.ⓑ[I]V,T❩. -normalize /3 width=1 by monotonic_lt_plus_l, monotonic_le_plus_r/ +normalize /3 width=1 by nlt_plus_bi_dx, nle_plus_bi_sn/ qed. lemma rfw_lpair_dx: ∀I,L,V,T. ♯❨L,T❩ < ♯❨L.ⓑ[I]V,T❩. -normalize /3 width=1 by monotonic_lt_plus_l, monotonic_le_plus_r/ +normalize /3 width=1 by nlt_plus_bi_dx, nle_plus_bi_sn/ qed. (* Basic_1: removed theorems 7: diff --git a/matita/matita/contribs/lambdadelta/static_2/syntax/cl_weight.ma b/matita/matita/contribs/lambdadelta/static_2/syntax/cl_weight.ma index ad3f08f93..e87996c23 100644 --- a/matita/matita/contribs/lambdadelta/static_2/syntax/cl_weight.ma +++ b/matita/matita/contribs/lambdadelta/static_2/syntax/cl_weight.ma @@ -27,11 +27,11 @@ interpretation "weight (closure)" 'Weight G L T = (fw G L T). (* Basic_1: was: flt_shift *) lemma fw_shift: ∀p,I,G,K,V,T. ♯❨G,K.ⓑ[I]V,T❩ < ♯❨G,K,ⓑ[p,I]V.T❩. -normalize /2 width=1 by monotonic_le_plus_r/ +normalize /2 width=1 by nle_plus_bi_sn/ qed. lemma fw_clear: ∀p,I1,I2,G,K,V,T. ♯❨G,K.ⓤ[I1],T❩ < ♯❨G,K,ⓑ[p,I2]V.T❩. -normalize /4 width=1 by monotonic_le_plus_r, le_S_S/ +normalize /4 width=1 by nle_plus_bi_sn, nle_succ_bi/ qed. lemma fw_tpair_sn: ∀I,G,L,V,T. ♯❨G,L,V❩ < ♯❨G,L,②[I]V.T❩. @@ -43,7 +43,7 @@ normalize in ⊢ (?→?→?→?→?→?%%); // qed. lemma fw_lpair_sn: ∀I,G,L,V,T. ♯❨G,L,V❩ < ♯❨G,L.ⓑ[I]V,T❩. -normalize /3 width=1 by monotonic_lt_plus_l, monotonic_le_plus_r/ +normalize /3 width=1 by nlt_plus_bi_dx, nle_plus_bi_sn/ qed. (* Basic_1: removed theorems 7: diff --git a/matita/matita/contribs/lambdadelta/static_2/syntax/fold.ma b/matita/matita/contribs/lambdadelta/static_2/syntax/fold.ma index 05b86e627..061ef6ed9 100644 --- a/matita/matita/contribs/lambdadelta/static_2/syntax/fold.ma +++ b/matita/matita/contribs/lambdadelta/static_2/syntax/fold.ma @@ -24,7 +24,7 @@ rec definition fold L T on L ≝ match L with ] ]. -interpretation "fold (restricted closure)" 'plus L T = (fold L T). +interpretation "fold (restricted closure)" 'nplus L T = (fold L T). (* Basic properties *********************************************************) diff --git a/matita/matita/contribs/lambdadelta/static_2/syntax/genv_weight.ma b/matita/matita/contribs/lambdadelta/static_2/syntax/genv_weight.ma index 3dd315e0a..88dcbc185 100644 --- a/matita/matita/contribs/lambdadelta/static_2/syntax/genv_weight.ma +++ b/matita/matita/contribs/lambdadelta/static_2/syntax/genv_weight.ma @@ -27,4 +27,4 @@ interpretation "weight (global environment)" 'Weight G = (gw G). (* Basic properties *********************************************************) lemma gw_pair: ∀I,G,T. ♯❨G❩ < ♯❨G.ⓑ[I]T❩. -normalize /2 width=1 by monotonic_le_plus_r/ qed. +normalize /2 width=1 by nle_plus_bi_sn/ qed. diff --git a/matita/matita/contribs/lambdadelta/static_2/syntax/item.ma b/matita/matita/contribs/lambdadelta/static_2/syntax/item.ma index bcaff1f89..c2ecea942 100644 --- a/matita/matita/contribs/lambdadelta/static_2/syntax/item.ma +++ b/matita/matita/contribs/lambdadelta/static_2/syntax/item.ma @@ -13,7 +13,7 @@ (**************************************************************************) include "ground/lib/bool.ma". -include "ground/lib/arith.ma". +include "ground/arith/nat.ma". (* ITEMS ********************************************************************) diff --git a/matita/matita/contribs/lambdadelta/static_2/syntax/lenv_length.ma b/matita/matita/contribs/lambdadelta/static_2/syntax/lenv_length.ma index 768105e54..5f4b5dcb7 100644 --- a/matita/matita/contribs/lambdadelta/static_2/syntax/lenv_length.ma +++ b/matita/matita/contribs/lambdadelta/static_2/syntax/lenv_length.ma @@ -47,7 +47,7 @@ lemma length_inv_succ_dx: ∀n,L. |L| = ↑n → ∃∃I,K. |K| = n & L = K. ⓘ[I]. #n * [ >length_atom #H destruct -| #L #I >length_bind /3 width=4 by ex2_2_intro, injective_S/ +| #L #I >length_bind /3 width=4 by ex2_2_intro, eq_inv_nsucc_bi/ ] qed-. diff --git a/matita/matita/contribs/lambdadelta/static_2/syntax/lenv_weight.ma b/matita/matita/contribs/lambdadelta/static_2/syntax/lenv_weight.ma index 19a645439..66d46a41f 100644 --- a/matita/matita/contribs/lambdadelta/static_2/syntax/lenv_weight.ma +++ b/matita/matita/contribs/lambdadelta/static_2/syntax/lenv_weight.ma @@ -28,7 +28,7 @@ interpretation "weight (local environment)" 'Weight L = (lw L). (* Basic_2A1: uses: lw_pair *) lemma lw_bind: ∀I,L. ♯❨L❩ < ♯❨L.ⓘ[I]❩. -normalize /2 width=1 by monotonic_le_plus_r/ qed. +normalize /2 width=1 by nle_plus_bi_sn/ qed. (* Basic_1: removed theorems 4: clt_cong clt_head clt_thead clt_wf_ind *) (* Basic_1: removed local theorems 1: clt_wf__q_ind *) diff --git a/matita/matita/contribs/lambdadelta/static_2/syntax/lveq_length.ma b/matita/matita/contribs/lambdadelta/static_2/syntax/lveq_length.ma index b97d967fa..da13d1248 100644 --- a/matita/matita/contribs/lambdadelta/static_2/syntax/lveq_length.ma +++ b/matita/matita/contribs/lambdadelta/static_2/syntax/lveq_length.ma @@ -32,30 +32,30 @@ qed. lemma lveq_fwd_length_le_sn: ∀L1,L2,n1,n2. L1 ≋ⓧ*[n1,n2] L2 → n1 ≤ |L1|. #L1 #L2 #n1 #n2 #H elim H -L1 -L2 -n1 -n2 normalize -/2 width=1 by le_S_S/ +/2 width=1 by nle_succ_bi/ qed-. lemma lveq_fwd_length_le_dx: ∀L1,L2,n1,n2. L1 ≋ⓧ*[n1,n2] L2 → n2 ≤ |L2|. #L1 #L2 #n1 #n2 #H elim H -L1 -L2 -n1 -n2 normalize -/2 width=1 by le_S_S/ +/2 width=1 by nle_succ_bi/ qed-. lemma lveq_fwd_length: ∀L1,L2,n1,n2. L1 ≋ⓧ*[n1,n2] L2 → ∧∧ |L1|-|L2| = n1 & |L2|-|L1| = n2. #L1 #L2 #n1 #n2 #H elim H -L1 -L2 -n1 -n2 /2 width=1 by conj/ -#K1 #K2 #n #_ * #H1 #H2 >length_bind /3 width=1 by minus_Sn_m, conj/ +#K1 #K2 #n #_ * #H1 #H2 >length_bind /3 width=1 by nminus_succ_sn, conj/ qed-. lemma lveq_length_fwd_sn: ∀L1,L2,n1,n2. L1 ≋ⓧ*[n1,n2] L2 → |L1| ≤ |L2| → 0 = n1. #L1 #L2 #n1 #n2 #H #HL elim (lveq_fwd_length … H) -H ->(eq_minus_O … HL) // +>(nle_inv_eq_zero_minus … HL) // qed-. lemma lveq_length_fwd_dx: ∀L1,L2,n1,n2. L1 ≋ⓧ*[n1,n2] L2 → |L2| ≤ |L1| → 0 = n2. #L1 #L2 #n1 #n2 #H #HL elim (lveq_fwd_length … H) -H ->(eq_minus_O … HL) // +>(nle_inv_eq_zero_minus … HL) // qed-. lemma lveq_inj_length: ∀L1,L2,n1,n2. L1 ≋ⓧ*[n1,n2] L2 → @@ -68,15 +68,15 @@ qed-. lemma lveq_fwd_length_plus: ∀L1,L2,n1,n2. L1 ≋ⓧ*[n1,n2] L2 → |L1| + n2 = |L2| + n1. #L1 #L2 #n1 #n2 #H elim H -L1 -L2 -n1 -n2 normalize -/2 width=2 by injective_plus_r/ +/2 width=2 by eq_inv_nplus_bi_sn/ qed-. lemma lveq_fwd_length_eq: ∀L1,L2. L1 ≋ⓧ*[0,0] L2 → |L1| = |L2|. -/3 width=2 by lveq_fwd_length_plus, injective_plus_l/ qed-. +/3 width=2 by lveq_fwd_length_plus, eq_inv_nplus_bi_dx/ qed-. lemma lveq_fwd_length_minus: ∀L1,L2,n1,n2. L1 ≋ⓧ*[n1,n2] L2 → |L1| - n1 = |L2| - n2. -/3 width=3 by lveq_fwd_length_plus, lveq_fwd_length_le_dx, lveq_fwd_length_le_sn, plus_to_minus_2/ qed-. +/3 width=3 by lveq_fwd_length_plus, lveq_fwd_length_le_dx, lveq_fwd_length_le_sn, nminus_plus_swap/ qed-. lemma lveq_fwd_abst_bind_length_le: ∀I1,I2,L1,L2,V1,n1,n2. L1.ⓑ[I1]V1 ≋ⓧ*[n1,n2] L2.ⓘ[I2] → |L1| ≤ |L2|. @@ -94,9 +94,9 @@ lemma lveq_fwd_bind_abst_length_le: ∀I1,I2,L1,L2,V2,n1,n2. lemma lveq_inv_void_dx_length: ∀L1,L2,n1,n2. L1 ≋ⓧ*[n1,n2] L2.ⓧ → |L1| ≤ |L2| → ∃∃m2. L1 ≋ ⓧ*[n1,m2] L2 & 0 = n1 & ↑m2 = n2. #L1 #L2 #n1 #n2 #H #HL12 -lapply (lveq_fwd_length_plus … H) normalize >plus_n_Sm #H0 -lapply (plus2_le_sn_sn … H0 HL12) -H0 -HL12 #H0 -elim (le_inv_S1 … H0) -H0 #m2 #_ #H0 destruct +lapply (lveq_fwd_length_plus … H) normalize >nplus_succ_dx #H0 +lapply (nplus_2_des_le_sn_sn … H0 HL12) -H0 -HL12 #H0 +elim (nle_inv_succ_sn … H0) -H0 #m2 #_ #H0 destruct elim (lveq_inv_void_succ_dx … H) -H /2 width=3 by ex3_intro/ qed-. diff --git a/matita/matita/contribs/lambdadelta/static_2/syntax/lveq_lveq.ma b/matita/matita/contribs/lambdadelta/static_2/syntax/lveq_lveq.ma index f3b2d18cd..6966715c4 100644 --- a/matita/matita/contribs/lambdadelta/static_2/syntax/lveq_lveq.ma +++ b/matita/matita/contribs/lambdadelta/static_2/syntax/lveq_lveq.ma @@ -42,8 +42,8 @@ theorem lveq_inj_void_sn_ge: ∀K1,K2. |K2| ≤ |K1| → #L1 #L2 #HL #n1 #n2 #Hn #m1 #m2 #Hm elim (lveq_fwd_length … Hn) -Hn #H1 #H2 destruct elim (lveq_fwd_length … Hm) -Hm #H1 #H2 destruct ->length_bind >eq_minus_S_pred >(eq_minus_O … HL) -/3 width=4 by plus_minus, and3_intro/ +>length_bind >nminus_succ_dx >(nle_inv_eq_zero_minus … HL) +/3 width=4 by nminus_plus_comm_23, and3_intro/ qed-. theorem lveq_inj_void_dx_le: ∀K1,K2. |K1| ≤ |K2| → diff --git a/matita/matita/contribs/lambdadelta/static_2/syntax/sd.ma b/matita/matita/contribs/lambdadelta/static_2/syntax/sd.ma index 533a79e05..cd62fb439 100644 --- a/matita/matita/contribs/lambdadelta/static_2/syntax/sd.ma +++ b/matita/matita/contribs/lambdadelta/static_2/syntax/sd.ma @@ -12,7 +12,10 @@ (* *) (**************************************************************************) -include "static_2/syntax/sh.ma". +include "ground/arith/nat_plus.ma". +include "ground/arith/nat_minus.ma". +include "ground/arith/nat_lt_pred.ma". +include "static_2/syntax/sh_nexts.ma". (* SORT DEGREE **************************************************************) @@ -28,41 +31,46 @@ record sd_props (h) (o): Prop ≝ { deg_total: ∀s. ∃d. deg o s d; deg_mono : ∀s,d1,d2. deg o s d1 → deg o s d2 → d1 = d2; (* compatibility condition *) - deg_next : ∀s,d. deg o s d → deg o (⫯[h]s) (↓d) + deg_next : ∀s,d. deg o s d → deg o (⇡[h]s) (↓d) }. (* Notable specifications ***************************************************) -definition deg_O: relation nat ≝ λs,d. d = 0. +definition deg_O: relation nat ≝ λs,d. d = 𝟎. definition sd_O: sd ≝ mk_sd deg_O. lemma sd_O_props (h): sd_props h sd_O ≝ mk_sd_props …. -/2 width=2 by le_n_O_to_eq, le_n, ex_intro/ qed. +/2 width=2 by nle_inv_zero_dx, nle_refl, ex_intro/ qed. (* Basic inversion lemmas ***************************************************) lemma deg_inv_pred (h) (o): sd_props h o → - ∀s,d. deg o (⫯[h]s) (↑d) → deg o s (↑↑d). + ∀s,d. deg o (⇡[h]s) (↑d) → deg o s (↑↑d). #h #o #Ho #s #d #H1 elim (deg_total … Ho s) #d0 #H0 lapply (deg_next … Ho … H0) #H2 -lapply (deg_mono … Ho … H1 H2) -H1 -H2 #H >H >S_pred -/2 width=2 by ltn_to_ltO/ +lapply (deg_mono … Ho … H1 H2) -H1 -H2 #H >H iter_n_Sm #H - lapply (nexts_inj … Hha … (↑n) 0 H) -H #H destruct - | #n @deg_SO_succ >iter_n_Sm // + [ #n #H destruct + (sh_nexts_succ_next h n s0) #H + lapply (sh_nexts_inj … Hha ???) -H #H destruct + | #n @deg_SO_succ >sh_nexts_swap // ] - | #H0 @deg_SO_zero #n >iter_n_Sm #H destruct + | #H0 @deg_SO_zero #n >sh_nexts_swap #H destruct /2 width=2 by/ ] ] @@ -75,7 +76,7 @@ rec definition sd_d (h:?) (s:?) (d:?) on d: sd ≝ [ O ⇒ sd_O | S d ⇒ match d with [ O ⇒ sd_SO h s - | _ ⇒ sd_d h (next h s) d + | _ ⇒ sd_d h (pr_next h s) d ] ]. diff --git a/matita/matita/contribs/lambdadelta/static_2/syntax/sd_lt.ma b/matita/matita/contribs/lambdadelta/static_2/syntax/sd_lt.ma index 238d1a28b..23725dba7 100644 --- a/matita/matita/contribs/lambdadelta/static_2/syntax/sd_lt.ma +++ b/matita/matita/contribs/lambdadelta/static_2/syntax/sd_lt.ma @@ -23,10 +23,10 @@ lemma deg_SO_gt (h): sh_lt h → ∀s1,s2. s1 < s2 → deg_SO h s1 s2 0. #h #Hh #s1 #s2 #Hs12 @deg_SO_zero * normalize [ #H destruct - elim (lt_refl_false … Hs12) + elim (nlt_inv_refl … Hs12) | #n #H - lapply (next_lt … Hh ((next h)^n s2)) >H -H #H - lapply (transitive_lt … H Hs12) -s1 #H1 - /3 width=5 by lt_le_false, nexts_le/ (* full auto too slow *) + lapply (next_lt … Hh ((pr_next h)^n s2)) >H -H #H + lapply (nlt_trans … H Hs12) -s1 #H1 + /3 width=5 by nlt_ge_false, nexts_le/ (* full auto too slow *) ] qed. diff --git a/matita/matita/contribs/lambdadelta/static_2/syntax/sh.ma b/matita/matita/contribs/lambdadelta/static_2/syntax/sh.ma index 812947375..9e9b8adc1 100644 --- a/matita/matita/contribs/lambdadelta/static_2/syntax/sh.ma +++ b/matita/matita/contribs/lambdadelta/static_2/syntax/sh.ma @@ -12,18 +12,18 @@ (* *) (**************************************************************************) -include "ground/lib/arith.ma". -include "static_2/notation/functions/upspoon_2.ma". +include "ground/arith/nat.ma". +include "static_2/notation/functions/uparrow_1_0.ma". (* SORT HIERARCHY ***********************************************************) (* sort hierarchy specification *) record sh: Type[0] ≝ { - next: nat → nat (* next sort in the hierarchy *) + sh_next: nat → nat (* next sort in the hierarchy *) }. interpretation "next sort (sort hierarchy)" - 'UpSpoon h s = (next h s). + 'UpArrow_1_0 h = (sh_next h). definition sh_is_next (h): relation nat ≝ - λs1,s2. ⫯[h]s1 = s2. + λs1,s2. ⇡[h]s1 = s2. diff --git a/matita/matita/contribs/lambdadelta/static_2/syntax/sh_lt.ma b/matita/matita/contribs/lambdadelta/static_2/syntax/sh_lt.ma index d33515ef8..bfeab5905 100644 --- a/matita/matita/contribs/lambdadelta/static_2/syntax/sh_lt.ma +++ b/matita/matita/contribs/lambdadelta/static_2/syntax/sh_lt.ma @@ -12,6 +12,7 @@ (* *) (**************************************************************************) +include "ground/arith/nat_lt_minus.ma". include "static_2/syntax/sh_props.ma". (* SORT HIERARCHY ***********************************************************) @@ -19,38 +20,38 @@ include "static_2/syntax/sh_props.ma". (* strict monotonicity condition *) record sh_lt (h): Prop ≝ { - next_lt: ∀s. s < ⫯[h]s + sh_next_lt: ∀s. s < ⇡[h]s }. (* Basic properties *********************************************************) -lemma nexts_le (h): sh_lt h → ∀s,n. s ≤ (next h)^n s. -#h #Hh #s #n elim n -n [ // ] normalize #n #IH -lapply (next_lt … Hh ((next h)^n s)) #H -lapply (le_to_lt_to_lt … IH H) -IH -H /2 width=2 by lt_to_le/ +lemma sh_nexts_le (h): sh_lt h → ∀s,n. s ≤ ⇡*[h,n]s. +#h #Hh #s #n @(nat_ind_succ … n) -n [ // ] #n #IH iter_O #H - elim (lt_refl_false s) - /3 width=3 by nexts_lt, transitive_lt/ - | #n2 >iter_S >iter_S <(iter_n_Sm … (next h)) <(iter_n_Sm … (next h)) #H - /3 width=2 by lt_S_S/ +| #n1 #IH #s #n2 @(nat_ind_succ … n2) -n2 + [ sh_nexts_swap >sh_nexts_swap #H + /3 width=2 by nlt_succ_bi/ ] ] qed-. @@ -59,16 +60,16 @@ lemma sh_lt_acyclic (h): sh_lt h → sh_acyclic h. #h #Hh @mk_sh_acyclic @pull_2 #n1 -elim n1 -n1 -[ #s * [ // ] #n2 >iter_O #H - elim (lt_refl_false s) >H in ⊢ (??%); -H - /2 width=1 by nexts_lt/ -| #n1 #IH #s * - [ >iter_O #H -IH - elim (lt_refl_false s) iter_S >iter_S <(iter_n_Sm … (next h)) <(iter_n_Sm … (next h)) #H - /3 width=2 by eq_f/ +@(nat_ind_succ … n1) -n1 +[ #s #n2 @(nat_ind_succ … n2) -n2 [ // ] #n2 #_ H in ⊢ (??%); -H + /2 width=1 by sh_nexts_lt/ +| #n1 #IH #s #n2 @(nat_ind_succ … n2) -n2 + [ sh_nexts_swap >sh_nexts_swap #H + lapply (IH … H) -IH -H // ] ] qed. @@ -76,33 +77,33 @@ qed. lemma sh_lt_dec (h): sh_lt h → sh_decidable h. #h #Hh @mk_sh_decidable #s1 #s2 -elim (lt_or_ge s2 s1) #Hs +elim (nat_split_lt_ge s2 s1) #Hs [ @or_intror * #n #H destruct - @(lt_le_false … Hs) /2 width=1 by nexts_le/ (**) (* full auto too slow *) -| @(nat_elim_le_sn … Hs) -s1 -s2 #s1 #s2 #IH #Hs12 - elim (lt_or_eq_or_gt s2 (⫯[h]s1)) #Hs21 destruct - [ elim (le_to_or_lt_eq … Hs12) -Hs12 #Hs12 destruct + @(nlt_ge_false … Hs) /2 width=1 by sh_nexts_le/ (**) (* full auto too slow *) +| @(nle_ind_sn … Hs) -s1 -s2 #s1 #s2 #IH #Hs12 + elim (nat_split_lt_eq_gt s2 (⇡[h]s1)) #Hs21 destruct + [ elim (nle_split_lt_eq … Hs12) -Hs12 #Hs12 destruct [ -IH @or_intror * #n #H destruct generalize in match Hs21; -Hs21 - <(iter_O … (next h) s1) in ⊢ (??%→?); <(iter_S … (next h)) #H + >sh_nexts_unit #H lapply (sh_lt_nexts_inv_lt … Hh … H) -H #H - <(le_n_O_to_eq n) in Hs12; - /2 width=2 by lt_refl_false, le_S_S_to_le/ + <(nle_inv_zero_dx n) in Hs12; + /2 width=2 by nlt_inv_refl, nle_inv_succ_bi/ | /3 width=2 by ex_intro, or_introl/ ] - | -IH @or_introl @(ex_intro … 1) // (**) (* auto fails *) - | lapply (transitive_lt s1 ??? Hs21) [ /2 width=1 by next_lt/ ] -Hs12 #Hs12 - elim (IH (s2-⫯[h]s1)) -IH - [3: /3 width=1 by next_lt, monotonic_lt_minus_r/ ] - >minus_minus_m_m [2,4: /2 width=1 by lt_to_le/ ] -Hs21 + | -IH @or_introl @(ex_intro … 𝟏) // (**) (* auto fails *) + | lapply (nlt_trans s1 ??? Hs21) [ /2 width=1 by sh_next_lt/ ] -Hs12 #Hs12 + elim (IH (s2-⇡[h]s1)) -IH + [3: /3 width=1 by sh_next_lt, nlt_minus_bi_sn/ ] + iter_S >iter_n_Sm // + @or_introl @(ex_intro … (↑n)) sh_nexts_swap // | #H1 @or_intror * #n #H2 @H1 -H1 destruct generalize in match Hs12; -Hs12 - <(iter_O … (next h) s1) in ⊢ (?%?→?); #H + >(sh_nexts_zero h s1) in ⊢ (?%?→?); #H lapply (sh_lt_nexts_inv_lt … Hh … H) -H #H - <(S_pred … H) -H - @(ex_intro … (↓n)) >(iter_n_Sm … (next h)) >iter_S // + >(nlt_des_gen … H) -H + @(ex_intro … (↓n)) sh_nexts_swap // ] ] ] diff --git a/matita/matita/contribs/lambdadelta/static_2/syntax/sh_nexts.ma b/matita/matita/contribs/lambdadelta/static_2/syntax/sh_nexts.ma new file mode 100644 index 000000000..143e2dbb8 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/static_2/syntax/sh_nexts.ma @@ -0,0 +1,46 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "ground/arith/nat_succ_iter.ma". +include "static_2/notation/functions/uparrowstar_2_0.ma". +include "static_2/syntax/sh.ma". + +(* SORT HIERARCHY ***********************************************************) + +definition sh_nexts (h) (n): nat → nat ≝ ⇡[h]^n. + +interpretation + "iterated next sort (sort hierarchy)" + 'UpArrowStar_2_0 h n = (sh_nexts h n). + +(* Basic constructions *) + +lemma sh_nexts_zero (h): ∀s. s = ⇡*[h,𝟎]s. +// qed. + +lemma sh_nexts_unit (h): ⇡[h] ≐ ⇡*[h,𝟏]. +// qed. + +lemma sh_nexts_succ (h) (n): ⇡[h] ∘ (⇡*[h,n]) ≐ ⇡*[h,↑n]. +/2 width=1 by niter_succ/ qed. + +(* Advanced constructions ****************************) + +lemma sh_nexts_swap (h) (n): ⇡[h] ∘ (⇡*[h,n]) ≐ ⇡*[h,n] ∘ ⇡[h]. +/2 width=1 by niter_appl/ qed. + +(* Helper constructions *****************************************************) + +lemma sh_nexts_succ_next (h) (n): ⇡*[h,n] ∘ (⇡[h]) ≐ ⇡*[h,↑n]. +// qed. diff --git a/matita/matita/contribs/lambdadelta/static_2/syntax/sh_props.ma b/matita/matita/contribs/lambdadelta/static_2/syntax/sh_props.ma index 4302026d4..53c4cfcfc 100644 --- a/matita/matita/contribs/lambdadelta/static_2/syntax/sh_props.ma +++ b/matita/matita/contribs/lambdadelta/static_2/syntax/sh_props.ma @@ -12,18 +12,19 @@ (* *) (**************************************************************************) -include "static_2/syntax/sh.ma". +include "static_2/syntax/sh_nexts.ma". (* SORT HIERARCHY ***********************************************************) (* acyclicity condition *) record sh_acyclic (h): Prop ≝ { - nexts_inj: ∀s,n1,n2. (next h)^n1 s = (next h)^n2 s → n1 = n2 +(**) (* use extensional equivalence *) + sh_nexts_inj: ∀s,n1,n2. ⇡*[h,n1]s = ⇡*[h,n2]s → n1 = n2 }. (* decidability condition *) record sh_decidable (h): Prop ≝ { - nexts_dec: ∀s1,s2. Decidable (∃n. (next h)^n s1 = s2) + sh_nexts_dec: ∀s1,s2. Decidable (∃n. ⇡*[h,n]s1 = s2) }. diff --git a/matita/matita/contribs/lambdadelta/static_2/syntax/teq.ma b/matita/matita/contribs/lambdadelta/static_2/syntax/teq.ma index 6b4a58e82..c8a82e16b 100644 --- a/matita/matita/contribs/lambdadelta/static_2/syntax/teq.ma +++ b/matita/matita/contribs/lambdadelta/static_2/syntax/teq.ma @@ -18,7 +18,7 @@ include "static_2/syntax/teqg.ma". (* SYNTACTIC EQUIVALENCE ON TERMS *******************************************) definition teq: relation term ≝ - teqg (eq …). + teqg (pr_eq …). interpretation "context-free syntactic equivalence (term)" diff --git a/matita/matita/contribs/lambdadelta/static_2/syntax/teq_ext.ma b/matita/matita/contribs/lambdadelta/static_2/syntax/teq_ext.ma index c91f93e93..c71e77ddc 100644 --- a/matita/matita/contribs/lambdadelta/static_2/syntax/teq_ext.ma +++ b/matita/matita/contribs/lambdadelta/static_2/syntax/teq_ext.ma @@ -19,10 +19,10 @@ include "static_2/syntax/teq.ma". (* SYNTACTIC EQUIVALENCE ****************************************************) definition ceq: relation3 lenv term term ≝ - ceqg (eq …). + ceqg (pr_eq …). definition ceq_ext: lenv → relation bind ≝ - ceqg_ext (eq …). + ceqg_ext (pr_eq …). interpretation "context-dependent syntactic equivalence (term)" diff --git a/matita/matita/contribs/lambdadelta/static_2/syntax/teqg.ma b/matita/matita/contribs/lambdadelta/static_2/syntax/teqg.ma index 46e9c67b6..8be52d4a5 100644 --- a/matita/matita/contribs/lambdadelta/static_2/syntax/teqg.ma +++ b/matita/matita/contribs/lambdadelta/static_2/syntax/teqg.ma @@ -12,6 +12,7 @@ (* *) (**************************************************************************) +include "ground/xoa/or_3.ma". include "ground/xoa/ex_3_2.ma". include "static_2/notation/relations/stareq_3.ma". include "static_2/syntax/term.ma". diff --git a/matita/matita/contribs/lambdadelta/static_2/syntax/teqw.ma b/matita/matita/contribs/lambdadelta/static_2/syntax/teqw.ma index 1412f42b6..6758d2f3d 100644 --- a/matita/matita/contribs/lambdadelta/static_2/syntax/teqw.ma +++ b/matita/matita/contribs/lambdadelta/static_2/syntax/teqw.ma @@ -210,7 +210,7 @@ elim (teqw_inv_cast_sn … H) -H #W2 #U2 #HVW #HTU #H destruct qed-. lemma teqw_inv_cast_xy_y: ∀T,V. ⓝV.T ≃ T → ⊥. -@(f_ind … tw) #n #IH #T #Hn #V #H destruct +@(wf1_ind_nlt … tw) #n #IH #T #Hn #V #H destruct elim (teqw_inv_cast_sn … H) -H #X1 #X2 #_ #HX2 #H destruct -V /2 width=4 by/ qed-. diff --git a/matita/matita/contribs/lambdadelta/static_2/syntax/term_vector.ma b/matita/matita/contribs/lambdadelta/static_2/syntax/term_vector.ma index 2714a1b91..25327ed32 100644 --- a/matita/matita/contribs/lambdadelta/static_2/syntax/term_vector.ma +++ b/matita/matita/contribs/lambdadelta/static_2/syntax/term_vector.ma @@ -21,7 +21,7 @@ include "static_2/syntax/term_simple.ma". rec definition applv Vs T on Vs ≝ match Vs with [ nil ⇒ T - | cons hd tl ⇒ ⓐhd. (applv tl T) + | cons hd pr_tl ⇒ ⓐhd. (applv pr_tl T) ]. interpretation "application to vector (term)" diff --git a/matita/matita/contribs/lambdadelta/static_2/syntax/term_weight.ma b/matita/matita/contribs/lambdadelta/static_2/syntax/term_weight.ma index ee53e62e7..bcb826bb4 100644 --- a/matita/matita/contribs/lambdadelta/static_2/syntax/term_weight.ma +++ b/matita/matita/contribs/lambdadelta/static_2/syntax/term_weight.ma @@ -32,7 +32,7 @@ lemma tw_pos: ∀T. 1 ≤ ♯❨T❩. qed. lemma tw_le_pair_dx (I): ∀V,T. ♯❨T❩ < ♯❨②[I]V.T❩. -#I #V #T /2 width=1 by le_S_S/ +#I #V #T /2 width=1 by nle_succ_bi/ qed. (* Basic_1: removed theorems 11: