From 82fe07c3accb68ca4f7a1870a046128fe980dced Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Fri, 11 Oct 2013 18:44:26 +0000 Subject: [PATCH] bug fix in supclosure allows alternative definition of fpbs ! --- .../basic_2/computation/cpxs_lift.ma | 58 +++++++----- .../basic_2/computation/fpbs_alt.ma | 9 +- .../basic_2/computation/lpxs_cpxs.ma | 58 +++++++++--- .../lambdadelta/basic_2/etc/cpr_conj.etc | 88 +++++++++++++++++++ .../lambdadelta/basic_2/etc/fsup/fsups.etc | 29 ++++++ .../contribs/lambdadelta/basic_2/names.txt | 1 + .../lambdadelta/basic_2/reduction/cpx_lift.ma | 45 +++++----- .../basic_2/reduction/lpr_ldrop.ma | 24 ++--- .../basic_2/reduction/lpx_ldrop.ma | 48 ++++++++-- .../lambdadelta/basic_2/relocation/fsup.ma | 46 ++++------ .../lambdadelta/basic_2/relocation/fsupq.ma | 37 +++----- .../basic_2/relocation/fsupq_alt.ma | 14 ++- .../lambdadelta/basic_2/substitution/fsupp.ma | 28 +++--- .../basic_2/substitution/fsupp_fsupp.ma | 2 +- .../lambdadelta/basic_2/substitution/fsups.ma | 40 +++------ .../basic_2/substitution/fsups_fsups.ma | 2 +- 16 files changed, 351 insertions(+), 178 deletions(-) create mode 100644 matita/matita/contribs/lambdadelta/basic_2/etc/cpr_conj.etc create mode 100644 matita/matita/contribs/lambdadelta/basic_2/etc/fsup/fsups.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_lift.ma index 25544dd41..182043d3b 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_lift.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_lift.ma @@ -26,17 +26,20 @@ lemma lsstas_cpxs: ∀h,g,G,L,T1,T2,l1. ⦃G, L⦄ ⊢ T1 •* [h, g, l1] T2 → #h #g #G #L #T1 #T2 #l1 #H @(lsstas_ind_dx … H) -T2 -l1 // #l1 #T #T2 #HT1 #HT2 #IHT1 #l2 #Hl2 #Hl12 lapply (lsstas_da_conf … HT1 … Hl2) -HT1 ->(plus_minus_m_m (l2-l1) 1 ?) [2: /2 width=1/ ] -/4 width=5 by cpxs_strap1, ssta_cpx, lt_to_le/ +>(plus_minus_m_m (l2-l1) 1 ?) +[ /4 width=5 by cpxs_strap1, ssta_cpx, lt_to_le/ +| /2 width=1 by monotonic_le_minus_r/ +] qed. lemma cpxs_delta: ∀h,g,I,G,L,K,V,V2,i. ⇩[0, i] L ≡ K.ⓑ{I}V → ⦃G, K⦄ ⊢ V ➡*[h, g] V2 → ∀W2. ⇧[0, i + 1] V2 ≡ W2 → ⦃G, L⦄ ⊢ #i ➡*[h, g] W2. -#h #g #I #G #L #K #V #V2 #i #HLK #H elim H -V2 [ /3 width=9/ ] -#V1 #V2 #_ #HV12 #IHV1 #W2 #HVW2 -lapply (ldrop_fwd_ldrop2 … HLK) -HLK #HLK -elim (lift_total V1 0 (i+1)) /4 width=11 by cpx_lift, cpxs_strap1/ +#h #g #I #G #L #K #V #V2 #i #HLK #H elim H -V2 +[ /3 width=9 by cpx_cpxs, cpx_delta/ +| #V1 lapply (ldrop_fwd_ldrop2 … HLK) -HLK + elim (lift_total V1 0 (i+1)) /4 width=11 by cpx_lift, cpxs_strap1/ +] qed. (* Advanced inversion lemmas ************************************************) @@ -45,21 +48,22 @@ lemma cpxs_inv_lref1: ∀h,g,G,L,T2,i. ⦃G, L⦄ ⊢ #i ➡*[h, g] T2 → T2 = #i ∨ ∃∃I,K,V1,T1. ⇩[0, i] L ≡ K.ⓑ{I}V1 & ⦃G, K⦄ ⊢ V1 ➡*[h, g] T1 & ⇧[0, i + 1] T1 ≡ T2. -#h #g #G #L #T2 #i #H @(cpxs_ind … H) -T2 /2 width=1/ +#h #g #G #L #T2 #i #H @(cpxs_ind … H) -T2 /2 width=1 by or_introl/ #T #T2 #_ #HT2 * [ #H destruct - elim (cpx_inv_lref1 … HT2) -HT2 /2 width=1/ - * /4 width=7/ + elim (cpx_inv_lref1 … HT2) -HT2 /2 width=1 by or_introl/ + * /4 width=7 by cpx_cpxs, ex3_4_intro, or_intror/ | * #I #K #V1 #T1 #HLK #HVT1 #HT1 lapply (ldrop_fwd_ldrop2 … HLK) #H0LK - elim (cpx_inv_lift1 … HT2 … H0LK … HT1) -H0LK -T /4 width=7/ + elim (cpx_inv_lift1 … HT2 … H0LK … HT1) -H0LK -T + /4 width=7 by cpxs_strap1, ex3_4_intro, or_intror/ ] qed-. (* Relocation properties ****************************************************) lemma cpxs_lift: ∀h,g,G. l_liftable (cpxs h g G). -/3 width=9/ qed. +/3 width=9 by cpx_lift, cpxs_strap1, l_liftable_LTC/ qed. lemma cpxs_inv_lift1: ∀h,g,G. l_deliftable_sn (cpxs h g G). /3 width=5 by l_deliftable_sn_LTC, cpx_inv_lift1/ @@ -70,10 +74,12 @@ qed-. lemma fsupq_cpxs_trans: ∀h,g,G1,G2,L1,L2,T2,U2. ⦃G2, L2⦄ ⊢ T2 ➡*[h, g] U2 → ∀T1. ⦃G1, L1, T1⦄ ⊃⸮ ⦃G2, L2, T2⦄ → ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ➡*[h, g] U1 & ⦃G1, L1, U1⦄ ⊃* ⦃G2, L2, U2⦄. -#h #g #G1 #G2 #L1 #L2 #T2 #U2 #H @(cpxs_ind_dx … H) -T2 [ /3 width=3/ ] -#T #T2 #HT2 #_ #IHTU2 #T1 #HT1 -elim (fsupq_cpx_trans … HT1 … HT2) -T #T #HT1 #HT2 -elim (IHTU2 … HT2) -T2 /3 width=3/ +#h #g #G1 #G2 #L1 #L2 #T2 #U2 #H @(cpxs_ind_dx … H) -T2 +[ /3 width=3 by fsupq_fsups, ex2_intro/ +| #T #T2 #HT2 #_ #IHTU2 #T1 #HT1 + elim (fsupq_cpx_trans … HT1 … HT2) -T #T #HT1 #HT2 + elim (IHTU2 … HT2) -T2 /3 width=3 by cpxs_strap2, ex2_intro/ +] qed-. lemma fsupq_lsstas_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃⸮ ⦃G2, L2, T2⦄ → @@ -85,11 +91,12 @@ lemma fsupq_lsstas_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃⸮ ⦃G lemma fsups_cpxs_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃* ⦃G2, L2, T2⦄ → ∀U2. ⦃G2, L2⦄ ⊢ T2 ➡*[h, g] U2 → ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ➡*[h, g] U1 & ⦃G1, L1, U1⦄ ⊃* ⦃G2, L2, U2⦄. -#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H @(fsups_ind … H) -G2 -L2 -T2 [ /2 width=3/ ] -#G #G2 #L #L2 #T #T2 #_ #HT2 #IHT1 #U2 #HTU2 -elim (fsupq_cpxs_trans … HTU2 … HT2) -T2 #T2 #HT2 #HTU2 -elim (IHT1 … HT2) -T #T #HT1 #HT2 -lapply (fsups_trans … HT2 … HTU2) -G -L -T2 /2 width=3/ +#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H @(fsups_ind … H) -G2 -L2 -T2 +[ /2 width=3 by ex2_intro/ +| #G #G2 #L #L2 #T #T2 #_ #HT2 #IHT1 #U2 #HTU2 + elim (fsupq_cpxs_trans … HTU2 … HT2) -T2 #T2 #HT2 #HTU2 + elim (IHT1 … HT2) -T /3 width=7 by fsups_trans, ex2_intro/ +] qed-. lemma fsups_lsstas_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃* ⦃G2, L2, T2⦄ → @@ -97,3 +104,14 @@ lemma fsups_lsstas_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃* ⦃G2, ∀l2. ⦃G2, L2⦄ ⊢ T2 ▪ [h, g] l2 → l1 ≤ l2 → ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ➡*[h, g] U1 & ⦃G1, L1, U1⦄ ⊃* ⦃G2, L2, U2⦄. /3 width=7 by fsups_cpxs_trans, lsstas_cpxs/ qed-. + +lemma fsups_cpx_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃* ⦃G2, L2, T2⦄ → + ∀U2. ⦃G2, L2⦄ ⊢ T2 ➡[h, g] U2 → + ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ➡[h, g] U1 & ⦃G1, L1, U1⦄ ⊃* ⦃G2, L2, U2⦄. +#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H @(fsups_ind … H) -G2 -L2 -T2 +[ /2 width=3 by ex2_intro/ +| #G #G2 #L #L2 #T #T2 #_ #HT2 #IHT1 #U2 #HTU2 + elim (fsupq_cpx_trans … HT2 … HTU2) -T2 #T2 #HT2 #HTU2 + elim (IHT1 … HT2) -T /3 width=7 by fsups_strap1, ex2_intro/ +] +qed-. \ No newline at end of file diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_alt.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_alt.ma index dd982ac37..1b0471ddb 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_alt.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_alt.ma @@ -33,12 +33,15 @@ interpretation "'big tree' parallel computation (closure) alternative" lemma fpb_fpbsa_trans: ∀h,g,G1,G,L1,L,T1,T. ⦃G1, L1, T1⦄ ≽[h, g] ⦃G, L, T⦄ → ∀G2,L2,T2. ⦃G, L, T⦄ ≥≥[h, g] ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ ≥≥[h, g] ⦃G2, L2, T2⦄. #h #g #G1 #G #L1 #L #T1 #T * -G -L -T [ #G #L #T #HG1 | #T #HT1 | #L #HL1 ] -#G2 #L2 #T2 * #L0 #T0 #HT0 #HG2 #L2 +#G2 #L2 #T2 * #L0 #T0 #HT0 #HG2 #HL02 [ elim (fsupq_cpxs_trans … HT0 … HG1) -T /3 width=7 by fsups_trans, ex3_2_intro/ | /3 width=5 by cpxs_strap2, ex3_2_intro/ -| lapply (lpx_cpxs_trans … HT0 … HL1) -HT0 #HT10 +| lapply (lpx_cpxs_trans … HT0 … HL1) -HT0 + elim (lpx_fsups_trans … HG2 … HL1) -L + /3 width=7 by lpxs_strap2, cpxs_trans, ex3_2_intro/ ] +qed-. (* Main properties **********************************************************) @@ -52,6 +55,6 @@ qed. theorem fpbsa_inv_fpbs: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ≥≥[h, g] ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ ≥[h, g] ⦃G2, L2, T2⦄. -#h #g #G1 #G2 #L1 #L2 #T1 #T2 * +#h #g #G1 #G2 #L1 #L2 #T1 #T2 * /4 width=5 by fpbs_trans, fsups_fpbs, cpxs_fpbs, lpxs_fpbs/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_cpxs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_cpxs.ma index b2907c52b..7330188e9 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_cpxs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_cpxs.ma @@ -45,21 +45,18 @@ lemma lpxs_cpxs_trans: ∀h,g,G. s_rs_trans … (cpx h g G) (lpxs h g G). lemma cpxs_bind2: ∀h,g,G,L,V1,V2. ⦃G, L⦄ ⊢ V1 ➡*[h, g] V2 → ∀I,T1,T2. ⦃G, L.ⓑ{I}V2⦄ ⊢ T1 ➡*[h, g] T2 → ∀a. ⦃G, L⦄ ⊢ ⓑ{a,I}V1.T1 ➡*[h, g] ⓑ{a,I}V2.T2. -#h #g #G #L #V1 #V2 #HV12 #I #T1 #T2 #HT12 -lapply (lpxs_cpxs_trans … HT12 (L.ⓑ{I}V1) ?) /2 width=1/ -qed. +/4 width=5 by lpxs_cpxs_trans, lpxs_pair, cpxs_bind/ qed. (* Inversion lemmas on context-sensitive ext parallel computation for terms *) lemma cpxs_inv_abst1: ∀h,g,a,G,L,V1,T1,U2. ⦃G, L⦄ ⊢ ⓛ{a}V1.T1 ➡*[h, g] U2 → ∃∃V2,T2. ⦃G, L⦄ ⊢ V1 ➡*[h, g] V2 & ⦃G, L.ⓛV1⦄ ⊢ T1 ➡*[h, g] T2 & U2 = ⓛ{a}V2.T2. -#h #g #a #G #L #V1 #T1 #U2 #H @(cpxs_ind … H) -U2 /2 width=5/ +#h #g #a #G #L #V1 #T1 #U2 #H @(cpxs_ind … H) -U2 /2 width=5 by ex3_2_intro/ #U0 #U2 #_ #HU02 * #V0 #T0 #HV10 #HT10 #H destruct elim (cpx_inv_abst1 … HU02) -HU02 #V2 #T2 #HV02 #HT02 #H destruct -lapply (lpxs_cpx_trans … HT02 (L.ⓛV1) ?) /2 width=1/ -HT02 #HT02 -lapply (cpxs_strap1 … HV10 … HV02) -V0 -lapply (cpxs_trans … HT10 … HT02) -T0 /2 width=5/ +lapply (lpxs_cpx_trans … HT02 (L.ⓛV1) ?) +/3 width=5 by lpxs_pair, cpxs_trans, cpxs_strap1, ex3_2_intro/ qed-. lemma cpxs_inv_abbr1: ∀h,g,a,G,L,V1,T1,U2. ⦃G, L⦄ ⊢ ⓓ{a}V1.T1 ➡*[h, g] U2 → ( @@ -67,21 +64,20 @@ lemma cpxs_inv_abbr1: ∀h,g,a,G,L,V1,T1,U2. ⦃G, L⦄ ⊢ ⓓ{a}V1.T1 ➡*[h, U2 = ⓓ{a}V2.T2 ) ∨ ∃∃T2. ⦃G, L.ⓓV1⦄ ⊢ T1 ➡*[h, g] T2 & ⇧[0, 1] U2 ≡ T2 & a = true. -#h #g #a #G #L #V1 #T1 #U2 #H @(cpxs_ind … H) -U2 /3 width=5/ +#h #g #a #G #L #V1 #T1 #U2 #H @(cpxs_ind … H) -U2 /3 width=5 by ex3_2_intro, or_introl/ #U0 #U2 #_ #HU02 * * [ #V0 #T0 #HV10 #HT10 #H destruct elim (cpx_inv_abbr1 … HU02) -HU02 * [ #V2 #T2 #HV02 #HT02 #H destruct - lapply (lpxs_cpx_trans … HT02 (L.ⓓV1) ?) /2 width=1/ -HT02 #HT02 - lapply (cpxs_strap1 … HV10 … HV02) -V0 - lapply (cpxs_trans … HT10 … HT02) -T0 /3 width=5/ + lapply (lpxs_cpx_trans … HT02 (L.ⓓV1) ?) + /4 width=5 by lpxs_pair, cpxs_trans, cpxs_strap1, ex3_2_intro, or_introl/ | #T2 #HT02 #HUT2 - lapply (lpxs_cpx_trans … HT02 (L.ⓓV1) ?) -HT02 /2 width=1/ -V0 #HT02 - lapply (cpxs_trans … HT10 … HT02) -T0 /3 width=3/ + lapply (lpxs_cpx_trans … HT02 (L.ⓓV1) ?) -HT02 + /4 width=3 by lpxs_pair, cpxs_trans, ex3_intro, or_intror/ ] | #U1 #HTU1 #HU01 elim (lift_total U2 0 1) #U #HU2 - lapply (cpx_lift … HU02 (L.ⓓV1) … HU01 … HU2) -U0 /2 width=1/ /4 width=3/ + /6 width=11 by cpxs_strap1, cpx_lift, ldrop_ldrop, ex3_intro, or_intror/ ] qed-. @@ -90,3 +86,37 @@ qed-. lemma lpxs_pair2: ∀h,g,I,G,L1,L2. ⦃G, L1⦄ ⊢ ➡*[h, g] L2 → ∀V1,V2. ⦃G, L2⦄ ⊢ V1 ➡*[h, g] V2 → ⦃G, L1.ⓑ{I}V1⦄ ⊢ ➡*[h, g] L2.ⓑ{I}V2. /3 width=3 by lpxs_pair, lpxs_cpxs_trans/ qed. + +(* Properties on supclosure *************************************************) + +lemma lpxs_fsupq_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃⸮ ⦃G2, L2, T2⦄ → + ∀K1. ⦃G1, K1⦄ ⊢ ➡*[h, g] L1 → + ∃∃K2,T. ⦃G1, K1⦄ ⊢ T1 ➡*[h, g] T & ⦃G1, K1, T⦄ ⊃⸮ ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡*[h, g] L2. +#h #g #G1 #G2 #L1 #L2 #T1 #T2 #HT12 #K1 #H @(lpxs_ind_dx … H) -K1 +[ /2 width=5 by ex3_2_intro/ +| #K1 #K #HK1 #_ * #L #T #HT1 #HT2 #HL2 -HT12 + lapply (lpx_cpxs_trans … HT1 … HK1) -HT1 + elim (lpx_fsupq_trans … HT2 … HK1) -K + /3 width=7 by lpxs_strap2, cpxs_strap1, ex3_2_intro/ +] +qed-. + +lemma lpxs_fsups_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃* ⦃G2, L2, T2⦄ → + ∀K1. ⦃G1, K1⦄ ⊢ ➡*[h, g] L1 → + ∃∃K2,T. ⦃G1, K1⦄ ⊢ T1 ➡*[h, g] T & ⦃G1, K1, T⦄ ⊃* ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡*[h, g] L2. +#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H @(fsups_ind … H) -G2 -L2 -T2 /2 width=5 by ex3_2_intro/ +#G #G2 #L #L2 #T #T2 #_ #H2 #IH1 #K1 #HLK1 elim (IH1 … HLK1) -L1 +#L0 #T0 #HT10 #HT0 #HL0 elim (lpxs_fsupq_trans … H2 … HL0) -L +#L #T3 #HT3 #HT32 #HL2 elim (fsups_cpxs_trans … HT0 … HT3) -T +/3 width=7 by cpxs_trans, fsups_strap1, ex3_2_intro/ +qed-. + +lemma lpx_fsups_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃* ⦃G2, L2, T2⦄ → + ∀K1. ⦃G1, K1⦄ ⊢ ➡[h, g] L1 → + ∃∃K2,T. ⦃G1, K1⦄ ⊢ T1 ➡*[h, g] T & ⦃G1, K1, T⦄ ⊃* ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡[h, g] L2. +#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H @(fsups_ind … H) -G2 -L2 -T2 /2 width=5 by ex3_2_intro/ +#G #G2 #L #L2 #T #T2 #_ #H2 #IH1 #K1 #HLK1 elim (IH1 … HLK1) -L1 +#L0 #T0 #HT10 #HT0 #HL0 elim (lpx_fsupq_trans … H2 … HL0) -L +#L #T3 #HT3 #HT32 #HL2 elim (fsups_cpx_trans … HT0 … HT3) -T +/3 width=7 by cpxs_strap1, fsups_strap1, ex3_2_intro/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/cpr_conj.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/cpr_conj.etc new file mode 100644 index 000000000..6ffdb54db --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/cpr_conj.etc @@ -0,0 +1,88 @@ +(**************************************************************************) +(* ___ *) +(* ||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 "basic_2/reduction/lpr_ldrop.ma". + +include "basic_2/unfold/fsups.ma". +include "basic_2/reducibility/lpr_ldrop.ma". + +lamma pippo: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⊃ ⦃L2, T2⦄ → ∀V1,i. ⇧[i, 1] V1 ≡ T1 → T2 = #i → ⊥. +#L1 #L2 #T1 #T2 #H elim H -L1 -L2 -T1 -T2 +[ #I #L1 #V #W1 #j #H1 #H2 + elim (lift_inv_lref2 … H1) -H1 * #H1 #H3 + + HVT2 : () + HV2 : (K2⊢V➡V2) + + +thaorem cpr_trans_lpr: ∀L1,T1,T. L1 ⊢ T1 ➡ T → ∀L2. L1 ⊢ ➡ L2 → + ∀T2. L2 ⊢ T ➡ T2 → + (⦃L2, T2⦄ ⊃* ⦃L1, T1⦄ → ⊥) ∨ T1 = T. +#L1 #T1 @(fsupp_wf_ind … L1 T1) -L1 -T1 #n #IH #L1 * [|*] +[ #I #Hn #T #H1 #L2 #HL12 #T2 #HT2 destruct -IH + elim (cpr_inv_atom1 … H1) -H1 + [ #H destruct + elim (cpr_inv_atom1 … HT2) -HT2 + [ #H destruct // + | * #K2 #V #V2 #i #HLK2 #HV2 #HVT2 #H destruct // + ] + | * #K1 #V1 #V #i #HLK1 #HV1 #HVT #H destruct + lapply (ldrop_pair2_fwd_fw … HLK1 (#i)) #HKV1 + elim (lpr_ldrop_conf … HLK1 … HL12) -HLK1 -HL12 #X #H #HLK2 + elim (lpr_inv_pair1 … H) -H #K2 #V0 #HK12 #_ #H destruct + lapply (ldrop_fwd_ldrop2 … HLK2) -V0 #HLK2 + elim (cpr_inv_lift1 … HT2 … HLK2 … HVT) -HT2 -HLK2 -HVT #V2 #HVT2 #HV2 + @or_introl #H + + + + + + + elim (lift_inv_lref2 … HVT2) -HVT2 * #H #_ + [ elim (lt_zero_false … H) + | >commutative_plus in H; >plus_plus_comm_23 #H + elim (le_plus_xySz_x_false … H) + ] + ] +| #a #I #V1 #T1 #Hn #X1 #H1 #L2 #HL12 #X2 #H2 + elim (cpr_inv_bind1 … H1) -H1 * + [ #V #T #HV1 #HT1 #H destruct + elim (cpr_inv_bind1 … H2) -H2 * + [ #V2 #T2 #HV2 #HT2 #H destruct + elim (IH … HV1 … HV2) // #HV12 destruct + [ @or_introl #H destruct /2 width=1/ + | elim (IH … HT1 … HT2) // /2 width=1/ -L1 -L2 #HT12 destruct + @or_introl #H destruct /2 width=1/ + ] + | #T2 #HT2 #HXT2 #H1 #H2 destruct + elim (IH … HT1 … HT2) // /2 width=1/ -L1 -L2 #HT12 destruct + | elim (term_eq_dec V1 V) #HV1 destruct + + ] + | #Y1 #HTY1 #HXY1 #H11 #H12 destruct + elim (lift_total (+ⓓV1.T1) 0 1) #Y2 #HXY2 + lapply (cpr_lift … H2 (L2.ⓓV1) … HXY1 … HXY2) /2 width=1/ -X1 /4 width=5/ + ] +| #I #V1 #T1 #Hn #X1 #H1 #L2 #HL12 #X2 #H2 + elim (cpr_inv_flat1 … H1) -H1 * + [ #V #T #HV1 #HT1 #H destruct + elim (cpr_inv_flat1 … H2) -H2 * + [ #V2 #T2 #HV2 #HT2 #H destruct /3 width=5/ + | #HX2 #H destruct /3 width=5/ + ] + | #HX1 #H destruct /3 width=5/ +] +qed-. +*) diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/fsup/fsups.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/fsup/fsups.etc new file mode 100644 index 000000000..36abe1208 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/fsup/fsups.etc @@ -0,0 +1,29 @@ +(* Advanced inversion lemmas on plus-iterated supclosure ********************) + +lamma fsupp_inv_bind1_fsups: ∀b,J,G1,G2,L1,L2,W,U,T2. ⦃G1, L1, ⓑ{b,J}W.U⦄ ⊃+ ⦃G2, L2, T2⦄ → + ⦃G1, L1, W⦄ ⊃* ⦃G2, L2, T2⦄ ∨ ⦃L1.ⓑ{J}W, U⦄ ⊃* ⦃G2, L2, T2⦄. +#b #J #G1 #G2 #L1 #L2 #W #U #T2 #H @(fsupp_ind … H) -G2 -L2 -T2 +[ #G2 #L2 #T2 #H + elim (fsup_inv_bind1 … H) -H * #H1 #H2 #H3 destruct /2 width=1/ +| #G #G2 #L #L2 #T #T2 #_ #HT2 * /3 width=4/ +] +qad-. + +lamma fsupp_inv_flat1_fsups: ∀J,G1,G2,L1,L2,W,U,T2. ⦃G1, L1, ⓕ{J}W.U⦄ ⊃+ ⦃G2, L2, T2⦄ → + ⦃G1, L1, W⦄ ⊃* ⦃G2, L2, T2⦄ ∨ ⦃G1, L1, U⦄ ⊃* ⦃G2, L2, T2⦄. +#J #G1 #G2 #L1 #L2 #W #U #T2 #H @(fsupp_ind … H) -G2 -L2 -T2 +[ #G2 #L2 #T2 #H + elim (fsup_inv_flat1 … H) -H #H1 * #H2 destruct /2 width=1/ +| #G #G2 #L #L2 #T #T2 #_ #HT2 * /3 width=4/ +] +qad-. + +lamma fsupp_fsups: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃+ ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ ⊃* ⦃G2, L2, T2⦄. +/2 width=1 by tri_inj/ qed. + +lamma fsups_lref: ∀I,G,K,V,i,L. ⇩[0, i] L ≡ K.ⓑ{I}V → ⦃G, L, #i⦄ ⊃* ⦃G, K, V⦄. +/3 width=5 by _/ qed. + +lamma fsups_lref_S_lt: ∀I,G1,G2,L,K,V,T,i. + 0 < i → ⦃G1, L, #(i-1)⦄ ⊃* ⦃G2, K, T⦄ → ⦃G1, L.ⓑ{I}V, #i⦄ ⊃+ ⦃G2, K, T⦄. +/3 width=7 by _/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/names.txt b/matita/matita/contribs/lambdadelta/basic_2/names.txt index 353fd787a..57b97d1d5 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/names.txt +++ b/matita/matita/contribs/lambdadelta/basic_2/names.txt @@ -51,6 +51,7 @@ NAMING CONVENTIONS FOR TRANSFORMATIONS AND RELATED FORMS - first letter +b: bi contex-sensitive for local environments c: contex-sensitive for terms f: context-freee for closures l: sn contex-sensitive for local environments diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_lift.ma index 72b624fd3..aabc8d9b4 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_lift.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_lift.ma @@ -13,7 +13,7 @@ (**************************************************************************) include "basic_2/relocation/ldrop_ldrop.ma". -include "basic_2/relocation/fsupq.ma". +include "basic_2/relocation/fsupq_alt.ma". include "basic_2/static/ssta.ma". include "basic_2/reduction/cpx.ma". @@ -138,18 +138,32 @@ qed-. (* Properties on supclosure *************************************************) +lemma fsup_cpx_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃ ⦃G2, L2, T2⦄ → + ∀U2. ⦃G2, L2⦄ ⊢ T2 ➡[h, g] U2 → + ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ➡[h, g] U1 & ⦃G1, L1, U1⦄ ⊃ ⦃G2, L2, U2⦄. +#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2 +/3 width=3 by fsup_pair_sn, fsup_bind_dx, fsup_flat_dx, cpx_pair_sn, cpx_bind, cpx_flat, ex2_intro/ +[ #I #G #L #V2 #U2 #HVU2 + elim (lift_total U2 0 1) + /4 width=9 by fsup_drop, cpx_append, cpx_delta, ldrop_pair, ldrop_ldrop, ex2_intro/ +| #G #L #K #T1 #U1 #e #HLK1 #HTU1 #T2 #HTU2 + elim (lift_total T2 0 (e+1)) + /3 width=11 by cpx_lift, fsup_drop, ex2_intro/ +] +qed-. + +lemma fsup_ssta_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃ ⦃G2, L2, T2⦄ → + ∀U2. ⦃G2, L2⦄ ⊢ T2 •[h, g] U2 → + ∀l. ⦃G2, L2⦄ ⊢ T2 ▪[h, g] l+1 → + ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ➡[h, g] U1 & ⦃G1, L1, U1⦄ ⊃ ⦃G2, L2, U2⦄. +/3 width=5 by fsup_cpx_trans, ssta_cpx/ qed-. + lemma fsupq_cpx_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃⸮ ⦃G2, L2, T2⦄ → ∀U2. ⦃G2, L2⦄ ⊢ T2 ➡[h, g] U2 → ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ➡[h, g] U1 & ⦃G1, L1, U1⦄ ⊃⸮ ⦃G2, L2, U2⦄. -#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2 -/3 width=3 by fsup_fsupq, fsupq_refl, cpx_pair_sn, cpx_bind, cpx_flat, fsup_pair_sn, fsup_bind_dx, fsup_flat_dx, ex2_intro/ -[ #I #G #L1 #V2 #U2 #HVU2 - elim (lift_total U2 0 1) - /4 width=9 by fsupq_refl, fsupq_ldrop, cpx_delta, ldrop_pair, ldrop_ldrop, ex2_intro/ -| #G1 #G2 #L1 #K1 #K2 #T1 #T2 #U1 #d #e #HLK1 #HTU1 #_ #IHT12 #U2 #HTU2 - elim (IHT12 … HTU2) -IHT12 -HTU2 #T - elim (lift_total T d e) - /3 width=11 by cpx_lift, fsupq_ldrop, ex2_intro/ +#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H #U2 #HTU2 elim (fsupq_inv_gen … H) -H +[ #HT12 elim (fsup_cpx_trans … HT12 … HTU2) /3 width=3 by fsup_fsupq, ex2_intro/ +| * #H1 #H2 #H3 destruct /2 width=3 by ex2_intro/ ] qed-. @@ -158,14 +172,3 @@ lemma fsupq_ssta_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃⸮ ⦃G2, ∀l. ⦃G2, L2⦄ ⊢ T2 ▪[h, g] l+1 → ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ➡[h, g] U1 & ⦃G1, L1, U1⦄ ⊃⸮ ⦃G2, L2, U2⦄. /3 width=5 by fsupq_cpx_trans, ssta_cpx/ qed-. - -lemma fsup_cpx_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃ ⦃G2, L2, T2⦄ → - ∀U2. ⦃G2, L2⦄ ⊢ T2 ➡[h, g] U2 → - ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ➡[h, g] U1 & ⦃G1, L1, U1⦄ ⊃⸮ ⦃G2, L2, U2⦄. -/3 width=3 by fsupq_cpx_trans, fsup_fsupq/ qed-. - -lemma fsup_ssta_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃ ⦃G2, L2, T2⦄ → - ∀U2. ⦃G2, L2⦄ ⊢ T2 •[h, g] U2 → - ∀l. ⦃G2, L2⦄ ⊢ T2 ▪[h, g] l+1 → - ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ➡[h, g] U1 & ⦃G1, L1, U1⦄ ⊃⸮ ⦃G2, L2, U2⦄. -/3 width=5 by fsupq_ssta_trans, fsup_fsupq/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/lpr_ldrop.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/lpr_ldrop.ma index 734921de3..cfc7cd7f3 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/reduction/lpr_ldrop.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/lpr_ldrop.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "basic_2/relocation/fsup.ma". +include "basic_2/relocation/fsupq_alt.ma". include "basic_2/relocation/ldrop_lpx_sn.ma". include "basic_2/reduction/cpr_lift.ma". include "basic_2/reduction/lpr.ma". @@ -37,14 +37,18 @@ lemma lpr_ldrop_trans_O1: ∀G. dropable_dx (lpr G). lemma fsup_cpr_trans: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃ ⦃G2, L2, T2⦄ → ∀U2. ⦃G2, L2⦄ ⊢ T2 ➡ U2 → ∃∃L,U1. ⦃G1, L1⦄ ⊢ ➡ L & ⦃G1, L⦄ ⊢ T1 ➡ U1 & ⦃G1, L, U1⦄ ⊃ ⦃G2, L2, U2⦄. -#G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2 [1,2,3,4,5: /3 width=5/ ] -[ #G #L #K #U #T #d #e #HLK #HUT #He #U2 #HU2 - elim (lift_total U2 d e) #T2 #HUT2 - lapply (cpr_lift … HU2 … HLK … HUT … HUT2) -HU2 -HUT /3 width=9/ -| #G1 #G2 #L1 #K1 #K2 #T1 #T2 #U1 #d #e #HLK1 #HTU1 #_ #IHT12 #U2 #HTU2 - elim (IHT12 … HTU2) -IHT12 -HTU2 #K #T #HK1 #HT1 #HT2 - elim (lift_total T d e) #U #HTU - elim (ldrop_lpr_trans … HLK1 … HK1) -HLK1 -HK1 #L2 #HL12 #HL2K - lapply (cpr_lift … HT1 … HL2K … HTU1 … HTU) -HT1 -HTU1 /3 width=11/ +#G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2 +/3 width=5 by fsup_lref_O, fsup_pair_sn, fsup_bind_dx, fsup_flat_dx, lpr_pair, cpr_pair_sn, cpr_atom, cpr_bind, cpr_flat, ex3_2_intro/ +#G #L #K #U #T #e #HLK #HUT #U2 #HU2 +elim (lift_total U2 0 (e+1)) #T2 #HUT2 +lapply (cpr_lift … HU2 … HLK … HUT … HUT2) -HU2 -HUT /3 width=9 by fsup_drop, ex3_2_intro/ +qed-. + +lemma fsupq_cpr_trans: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃⸮ ⦃G2, L2, T2⦄ → + ∀U2. ⦃G2, L2⦄ ⊢ T2 ➡ U2 → + ∃∃L,U1. ⦃G1, L1⦄ ⊢ ➡ L & ⦃G1, L⦄ ⊢ T1 ➡ U1 & ⦃G1, L, U1⦄ ⊃⸮ ⦃G2, L2, U2⦄. +#G1 #G2 #L1 #L2 #T1 #T2 #H #U2 #HTU2 elim (fsupq_inv_gen … H) -H +[ #HT12 elim (fsup_cpr_trans … HT12 … HTU2) /3 width=5 by fsup_fsupq, ex3_2_intro/ +| * #H1 #H2 #H3 destruct /2 width=5 by ex3_2_intro/ ] qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/lpx_ldrop.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/lpx_ldrop.ma index 176c16012..9848968d7 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/reduction/lpx_ldrop.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/lpx_ldrop.ma @@ -31,18 +31,48 @@ lemma lpx_ldrop_trans_O1: ∀h,g,G. dropable_dx (lpx h g G). (* Properties on supclosure *************************************************) -lemma fsupq_lpx_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃⸮ ⦃G2, L2, T2⦄ → - ∀K2. ⦃G2, L2⦄ ⊢ ➡[h, g] K2 → - ∃∃K1,T. ⦃G1, L1⦄ ⊢ ➡[h, g] K1 & ⦃G1, L1⦄ ⊢ T1 ➡[h, g] T & ⦃G1, K1, T⦄ ⊃⸮ ⦃G2, K2, T2⦄. +lemma fsup_lpx_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃ ⦃G2, L2, T2⦄ → + ∀K2. ⦃G2, L2⦄ ⊢ ➡[h, g] K2 → + ∃∃K1,T. ⦃G1, L1⦄ ⊢ ➡[h, g] K1 & ⦃G1, L1⦄ ⊢ T1 ➡[h, g] T & ⦃G1, K1, T⦄ ⊃ ⦃G2, K2, T2⦄. #h #g #G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2 -/3 width=5 by fsup_fsupq, fsupq_refl, lpx_pair, fsup_lref_O, fsup_pair_sn, fsup_flat_dx, ex3_2_intro/ +/3 width=5 by fsup_lref_O, fsup_pair_sn, fsup_flat_dx, lpx_pair, ex3_2_intro/ [ #a #I #G2 #L2 #V2 #T2 #X #H elim (lpx_inv_pair1 … H) -H #K2 #W2 #HLK2 #HVW2 #H destruct /3 width=5 by fsup_fsupq, cpx_pair_sn, fsup_bind_dx, ex3_2_intro/ -| #G1 #G2 #L1 #K1 #K2 #T1 #T2 #U1 #d #e #HLK1 #HTU1 #_ #IH12 #K0 #HK20 - elim (IH12 … HK20) -K2 #K2 #T #HK12 - elim (ldrop_lpx_trans … HLK1 … HK12) -HK12 - elim (lift_total T d e) - /3 width=11 by cpx_lift, fsupq_ldrop, ex3_2_intro/ +| #G #L1 #K1 #T1 #U1 #e #HLK1 #HTU1 #K2 #HK12 + elim (ldrop_lpx_trans … HLK1 … HK12) -HK12 + /3 width=7 by fsup_drop, ex3_2_intro/ +] +qed-. + +lemma fsupq_lpx_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃⸮ ⦃G2, L2, T2⦄ → + ∀K2. ⦃G2, L2⦄ ⊢ ➡[h, g] K2 → + ∃∃K1,T. ⦃G1, L1⦄ ⊢ ➡[h, g] K1 & ⦃G1, L1⦄ ⊢ T1 ➡[h, g] T & ⦃G1, K1, T⦄ ⊃⸮ ⦃G2, K2, T2⦄. +#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H #K2 #HLK2 elim (fsupq_inv_gen … H) -H +[ #HT12 elim (fsup_lpx_trans … HT12 … HLK2) /3 width=5 by fsup_fsupq, ex3_2_intro/ +| * #H1 #H2 #H3 destruct /2 width=5 by ex3_2_intro/ +] +qed-. + +lemma lpx_fsup_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃ ⦃G2, L2, T2⦄ → + ∀K1. ⦃G1, K1⦄ ⊢ ➡[h, g] L1 → + ∃∃K2,T. ⦃G1, K1⦄ ⊢ T1 ➡[h, g] T & ⦃G1, K1, T⦄ ⊃ ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡[h, g] L2. +#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2 +/3 width=7 by fsup_pair_sn, fsup_bind_dx, fsup_flat_dx, lpx_pair, ex3_2_intro/ +[ #I #G1 #L1 #V1 #X #H elim (lpx_inv_pair2 … H) -H + #K1 #W1 #HKL1 #HWV1 #H destruct elim (lift_total V1 0 1) + /4 width=7 by cpx_delta, fsup_drop, ldrop_ldrop, ex3_2_intro/ +| #G #L1 #K1 #T1 #U1 #e #HLK1 #HTU1 #L0 #HL01 + elim (lpx_ldrop_trans_O1 … HL01 … HLK1) -L1 + /3 width=5 by fsup_drop, ex3_2_intro/ +] +qed-. + +lemma lpx_fsupq_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃⸮ ⦃G2, L2, T2⦄ → + ∀K1. ⦃G1, K1⦄ ⊢ ➡[h, g] L1 → + ∃∃K2,T. ⦃G1, K1⦄ ⊢ T1 ➡[h, g] T & ⦃G1, K1, T⦄ ⊃⸮ ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡[h, g] L2. +#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H #K1 #HKL1 elim (fsupq_inv_gen … H) -H +[ #HT12 elim (lpx_fsup_trans … HT12 … HKL1) /3 width=5 by fsup_fsupq, ex3_2_intro/ +| * #H1 #H2 #H3 destruct /2 width=5 by ex3_2_intro/ ] qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/fsup.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/fsup.ma index 80ec9b0b5..9719b4992 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/fsup.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/fsup.ma @@ -20,15 +20,12 @@ include "basic_2/relocation/ldrop.ma". (* activate genv *) inductive fsup: tri_relation genv lenv term ≝ -| fsup_lref_O : ∀I,G,L,V. fsup G (L.ⓑ{I}V) (#0) G L V -| fsup_pair_sn : ∀I,G,L,V,T. fsup G L (②{I}V.T) G L V -| fsup_bind_dx : ∀a,I,G,L,V,T. fsup G L (ⓑ{a,I}V.T) G (L.ⓑ{I}V) T -| fsup_flat_dx : ∀I,G,L,V,T. fsup G L (ⓕ{I}V.T) G L T -| fsup_ldrop_lt: ∀G,L,K,T,U,d,e. - ⇩[d, e] L ≡ K → ⇧[d, e] T ≡ U → 0 < e → fsup G L U G K T -| fsup_ldrop : ∀G1,G2,L1,K1,K2,T1,T2,U1,d,e. - ⇩[d, e] L1 ≡ K1 → ⇧[d, e] T1 ≡ U1 → - fsup G1 K1 T1 G2 K2 T2 → fsup G1 L1 U1 G2 K2 T2 +| fsup_lref_O : ∀I,G,L,V. fsup G (L.ⓑ{I}V) (#0) G L V +| fsup_pair_sn: ∀I,G,L,V,T. fsup G L (②{I}V.T) G L V +| fsup_bind_dx: ∀a,I,G,L,V,T. fsup G L (ⓑ{a,I}V.T) G (L.ⓑ{I}V) T +| fsup_flat_dx: ∀I,G,L,V,T. fsup G L (ⓕ{I}V.T) G L T +| fsup_drop : ∀G,L,K,T,U,e. + ⇩[0, e+1] L ≡ K → ⇧[0, e+1] T ≡ U → fsup G L U G K T . interpretation @@ -37,32 +34,23 @@ interpretation (* Basic properties *********************************************************) -lemma fsup_lref_S_lt: ∀I,G1,G2,L,K,V,T,i. 0 < i → ⦃G1, L, #(i-1)⦄ ⊃ ⦃G2, K, T⦄ → ⦃G1, L.ⓑ{I}V, #i⦄ ⊃ ⦃G2, K, T⦄. -#I #G1 #G2 #L #K #V #T #i #Hi #H /3 width=7 by fsup_ldrop, ldrop_ldrop, lift_lref_ge_minus/ (**) (* auto too slow without trace *) +lemma fsup_drop_lt: ∀G,L,K,T,U,e. 0 < e → + ⇩[0, e] L ≡ K → ⇧[0, e] T ≡ U → fsup G L U G K T. +#G #L #K #T #U #e #He >(plus_minus_m_m e 1) /2 width=3 by fsup_drop/ qed. -lemma fsup_lref: ∀I,G,K,V,i,L. ⇩[0, i] L ≡ K.ⓑ{I}V → ⦃G, L, #i⦄ ⊃ ⦃G, K, V⦄. -#I #G #K #V #i @(nat_elim1 i) -i #i #IH #L #H -elim (ldrop_inv_O1_pair2 … H) -H * -[ #H1 #H2 destruct // -| #I1 #K1 #V1 #HK1 #H #Hi destruct - lapply (IH … HK1) /2 width=1/ -] +lemma fsup_lref_S_lt: ∀I,G,L,V,i. 0 < i → ⦃G, L.ⓑ{I}V, #i⦄ ⊃ ⦃G, L, #(i-1)⦄. +/3 width=3 by fsup_drop, ldrop_ldrop, lift_lref_ge_minus/ qed. (* Basic forward lemmas *****************************************************) lemma fsup_fwd_fw: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃ ⦃G2, L2, T2⦄ → ♯{G2, L2, T2} < ♯{G1, L1, T1}. #G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2 // -[ #G #L #K #T #U #d #e #HLK #HTU #HKL - lapply (ldrop_fwd_lw_lt … HLK HKL) -HKL -HLK #HKL - lapply (lift_fwd_tw … HTU) -d -e #H - normalize in ⊢ (?%%); /2 width=1/ -| #G1 #G2 #L1 #K1 #K2 #T1 #T2 #U1 #d #e #HLK1 #HTU1 #_ #IHT12 - lapply (ldrop_fwd_lw … HLK1) -HLK1 #HLK1 - lapply (lift_fwd_tw … HTU1) -HTU1 #HTU1 - @(lt_to_le_to_lt … IHT12) -IHT12 /2 width=1/ -] +#G #L #K #T #U #e #HLK #HTU +lapply (ldrop_fwd_lw_lt … HLK ?) -HLK // #HKL +lapply (lift_fwd_tw … HTU) -e #H +normalize in ⊢ (?%%); /2 width=1 by lt_minus_to_plus/ qed-. fact fsup_fwd_length_lref1_aux: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃ ⦃G2, L2, T2⦄ → @@ -71,10 +59,6 @@ fact fsup_fwd_length_lref1_aux: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃ ⦃G2 [1: normalize // |3: #a |5: /2 width=4 by ldrop_fwd_length_lt4/ -|6: #G1 #G2 #L1 #K1 #K2 #T1 #T2 #U1 #d #e #HLK1 #HTU1 #_ #IHT12 #i #H destruct - lapply (ldrop_fwd_length_le4 … HLK1) -HLK1 #HLK1 - elim (lift_inv_lref2 … HTU1) -HTU1 * #Hdei #H destruct - @(lt_to_le_to_lt … HLK1) /2 width=2/ ] #I #G #L #V #T #j #H destruct qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/fsupq.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/fsupq.ma index d45a3c83f..0a48ca02a 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/fsupq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/fsupq.ma @@ -19,14 +19,12 @@ include "basic_2/relocation/fsup.ma". (* activate genv *) inductive fsupq: tri_relation genv lenv term ≝ -| fsupq_refl : ∀G,L,T. fsupq G L T G L T | fsupq_lref_O : ∀I,G,L,V. fsupq G (L.ⓑ{I}V) (#0) G L V | fsupq_pair_sn: ∀I,G,L,V,T. fsupq G L (②{I}V.T) G L V | fsupq_bind_dx: ∀a,I,G,L,V,T. fsupq G L (ⓑ{a,I}V.T) G (L.ⓑ{I}V) T | fsupq_flat_dx: ∀I,G, L,V,T. fsupq G L (ⓕ{I}V.T) G L T -| fsupq_ldrop : ∀G1,G2,L1,K1,K2,T1,T2,U1,d,e. - ⇩[d, e] L1 ≡ K1 → ⇧[d, e] T1 ≡ U1 → - fsupq G1 K1 T1 G2 K2 T2 → fsupq G1 L1 U1 G2 K2 T2 +| fsupq_drop : ∀G,L,K,T,U,e. + ⇩[0, e] L ≡ K → ⇧[0, e] T ≡ U → fsupq G L U G K T . interpretation @@ -35,36 +33,29 @@ interpretation (* Basic properties *********************************************************) -lemma fsup_fsupq: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃ ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ ⊃⸮ ⦃G2, L2, T2⦄. -#G1 #G2 #L1 #L2 #T1 #T2 #H elim H -L1 -L2 -T1 -T2 // /2 width=7/ qed. - -(* Basic properties *********************************************************) +lemma fsupq_refl: tri_reflexive … fsupq. +/2 width=3 by fsupq_drop/ qed. -lemma fsupq_lref_S_lt: ∀I,G1,G2,L,K,V,T,i. - 0 < i → ⦃G1, L, #(i-1)⦄ ⊃⸮ ⦃G2, K, T⦄ → ⦃G1, L.ⓑ{I}V, #i⦄ ⊃⸮ ⦃G2, K, T⦄. -/3 width=7/ qed. - -lemma fsupq_lref: ∀I,G,K,V,i,L. ⇩[0, i] L ≡ K.ⓑ{I}V → ⦃G, L, #i⦄ ⊃⸮ ⦃G, K, V⦄. -/3 width=2/ qed. +lemma fsup_fsupq: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃ ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ ⊃⸮ ⦃G2, L2, T2⦄. +#G1 #G2 #L1 #L2 #T1 #T2 #H elim H -L1 -L2 -T1 -T2 // /2 width=3 by fsupq_drop/ +qed. (* Basic forward lemmas *****************************************************) lemma fsupq_fwd_fw: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃⸮ ⦃G2, L2, T2⦄ → ♯{G2, L2, T2} ≤ ♯{G1, L1, T1}. -#G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2 // [1,2,3: /2 width=1/ ] -#G1 #G2 #L1 #K1 #K2 #T1 #T2 #U1 #d #e #HLK1 #HTU1 #_ #IHT12 -lapply (ldrop_fwd_lw … HLK1) -HLK1 #HLK1 -lapply (lift_fwd_tw … HTU1) -HTU1 #HTU1 -@(transitive_le … IHT12) -IHT12 /2 width=1/ +#G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2 /2 width=1 by lt_to_le/ +#G1 #L1 #K1 #T1 #U1 #e #HLK1 #HTU1 +lapply (ldrop_fwd_lw … HLK1) -HLK1 +lapply (lift_fwd_tw … HTU1) -HTU1 +/2 width=1 by le_plus, le_n/ qed-. fact fsupq_fwd_length_lref1_aux: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃⸮ ⦃G2, L2, T2⦄ → ∀i. T1 = #i → |L2| ≤ |L1|. #G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2 // [ #a #I #G #L #V #T #j #H destruct -| #G1 #G2 #L1 #K1 #K2 #T1 #T2 #U1 #d #e #HLK1 #HTU1 #_ #IHT12 #i #H destruct - lapply (ldrop_fwd_length_le4 … HLK1) -HLK1 #HLK1 - elim (lift_inv_lref2 … HTU1) -HTU1 * #Hdei #H destruct - @(transitive_le … HLK1) /2 width=2/ +| #G1 #L1 #K1 #T1 #U1 #e #HLK1 #HTU1 #i #H destruct + /2 width=3 by ldrop_fwd_length_le4/ ] qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/fsupq_alt.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/fsupq_alt.ma index 54e161f7f..cfbca8693 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/fsupq_alt.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/fsupq_alt.ma @@ -29,20 +29,18 @@ interpretation lemma fsupqa_refl: tri_reflexive … fsupqa. // qed. -lemma fsupqa_ldrop: ∀G1,G2,K1,K2,T1,T2. ⦃G1, K1, T1⦄ ⊃⊃⸮ ⦃G2, K2, T2⦄ → - ∀L1,d,e. ⇩[d, e] L1 ≡ K1 → - ∀U1. ⇧[d, e] T1 ≡ U1 → ⦃G1, L1, U1⦄ ⊃⊃⸮ ⦃G2, K2, T2⦄. -#G1 #G2 #K1 #K2 #T1 #T2 * [ /3 width=7/ ] * #H1 #H2 #H3 destruct -#L1 #d #e #HLK #U1 #HTU elim (eq_or_gt e) -/3 width=5 by fsup_ldrop_lt, or_introl/ #H destruct ->(ldrop_inv_O2 … HLK) -L1 >(lift_inv_O2 … HTU) -T2 -d // +lemma fsupqa_drop: ∀G,L,K,T,U,e. + ⇩[0, e] L ≡ K → ⇧[0, e] T ≡ U → ⦃G, L, U⦄ ⊃⊃⸮ ⦃G, K, T⦄. +#G #L #K #T #U #e #HLK #HTU elim (eq_or_gt e) +/3 width=5 by fsup_drop_lt, or_introl/ #H destruct +>(ldrop_inv_O2 … HLK) -L >(lift_inv_O2 … HTU) -T // qed. (* Main properties **********************************************************) theorem fsupq_fsupqa: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃⸮ ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ ⊃⊃⸮ ⦃G2, L2, T2⦄. #G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2 -/2 width=7 by fsupqa_ldrop, fsup_lref_O, fsup_pair_sn, fsup_bind_dx, fsup_flat_dx, or_introl/ +/2 width=3 by fsupqa_drop, fsup_lref_O, fsup_pair_sn, fsup_bind_dx, fsup_flat_dx, or_introl/ qed. (* Main inversion properties ************************************************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/fsupp.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/fsupp.ma index e51e5cd5a..3c8da530a 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/substitution/fsupp.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/fsupp.ma @@ -25,38 +25,46 @@ interpretation "plus-iterated structural successor (closure)" (* Basic properties *********************************************************) lemma fsup_fsupp: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃ ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ ⊃+ ⦃G2, L2, T2⦄. -/2 width=1/ qed. +/2 width=1 by tri_inj/ qed. lemma fsupp_strap1: ∀G1,G,G2,L1,L,L2,T1,T,T2. ⦃G1, L1, T1⦄ ⊃+ ⦃G, L, T⦄ → ⦃G, L, T⦄ ⊃ ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ ⊃+ ⦃G2, L2, T2⦄. -/2 width=5/ qed. +/2 width=5 by tri_step/ qed. lemma fsupp_strap2: ∀G1,G,G2,L1,L,L2,T1,T,T2. ⦃G1, L1, T1⦄ ⊃ ⦃G, L, T⦄ → ⦃G, L, T⦄ ⊃+ ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ ⊃+ ⦃G2, L2, T2⦄. -/2 width=5/ qed. +/2 width=5 by tri_TC_strap/ qed. + +lemma fsupp_ldrop: ∀G1,G2,L1,K1,K2,T1,T2,U1,e. ⇩[0, e] L1 ≡ K1 → ⇧[0, e] T1 ≡ U1 → + ⦃G1, K1, T1⦄ ⊃+ ⦃G2, K2, T2⦄ → ⦃G1, L1, U1⦄ ⊃+ ⦃G2, K2, T2⦄. +#G1 #G2 #L1 #K1 #K2 #T1 #T2 #U1 #e #HLK1 #HTU1 #HT12 elim (eq_or_gt … e) #H destruct +[ >(ldrop_inv_O2 … HLK1) -L1 <(lift_inv_O2 … HTU1) -U1 // +| /3 width=5 by fsupp_strap2, fsup_drop_lt/ +] +qed-. lemma fsupp_lref: ∀I,G,L,K,V,i. ⇩[0, i] L ≡ K.ⓑ{I}V → ⦃G, L, #i⦄ ⊃+ ⦃G, K, V⦄. -/3 width=2/ qed. +/3 width=6 by fsup_lref_O, fsup_fsupp, lift_lref_ge, fsupp_ldrop/ qed. lemma fsupp_pair_sn: ∀I,G,L,V,T. ⦃G, L, ②{I}V.T⦄ ⊃+ ⦃G, L, V⦄. -/2 width=1/ qed. +/2 width=1 by fsup_pair_sn, fsup_fsupp/ qed. lemma fsupp_bind_dx: ∀a,I,G,L,V,T. ⦃G, L, ⓑ{a,I}V.T⦄ ⊃+ ⦃G, L.ⓑ{I}V, T⦄. -/2 width=1/ qed. +/2 width=1 by fsup_bind_dx, fsup_fsupp/ qed. lemma fsupp_flat_dx: ∀I,G,L,V,T. ⦃G, L, ⓕ{I}V.T⦄ ⊃+ ⦃G, L, T⦄. -/2 width=1/ qed. +/2 width=1 by fsup_flat_dx, fsup_fsupp/ qed. lemma fsupp_flat_dx_pair_sn: ∀I1,I2,G,L,V1,V2,T. ⦃G, L, ⓕ{I1}V1.②{I2}V2.T⦄ ⊃+ ⦃G, L, V2⦄. -/2 width=5/ qed. +/2 width=5 by fsup_pair_sn, fsupp_strap1/ qed. lemma fsupp_bind_dx_flat_dx: ∀a,G,I1,I2,L,V1,V2,T. ⦃G, L, ⓑ{a,I1}V1.ⓕ{I2}V2.T⦄ ⊃+ ⦃G, L.ⓑ{I1}V1, T⦄. -/2 width=5/ qed. +/2 width=5 by fsup_flat_dx, fsupp_strap1/ qed. lemma fsupp_flat_dx_bind_dx: ∀a,I1,I2,G,L,V1,V2,T. ⦃G, L, ⓕ{I1}V1.ⓑ{a,I2}V2.T⦄ ⊃+ ⦃G, L.ⓑ{I2}V2, T⦄. -/2 width=5/ qed. +/2 width=5 by fsup_bind_dx, fsupp_strap1/ qed. (* Basic eliminators ********************************************************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/fsupp_fsupp.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/fsupp_fsupp.ma index 7740b19da..a8422e6eb 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/substitution/fsupp_fsupp.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/fsupp_fsupp.ma @@ -19,4 +19,4 @@ include "basic_2/substitution/fsupp.ma". (* Main propertis ***********************************************************) theorem fsupp_trans: tri_transitive … fsupp. -/2 width=5/ qed-. +/2 width=5 by tri_TC_transitive/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/fsups.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/fsups.ma index 51126ebd1..acc34d75c 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/substitution/fsups.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/fsups.ma @@ -41,43 +41,29 @@ qed-. (* Basic properties *********************************************************) lemma fsups_refl: tri_reflexive … fsups. -/2 width=1/ qed. +/2 width=1 by tri_inj/ qed. lemma fsupq_fsups: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃⸮ ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ ⊃* ⦃G2, L2, T2⦄. -/2 width=1/ qed. +/2 width=1 by tri_inj/ qed. lemma fsups_strap1: ∀G1,G,G2,L1,L,L2,T1,T,T2. ⦃G1, L1, T1⦄ ⊃* ⦃G, L, T⦄ → ⦃G, L, T⦄ ⊃⸮ ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ ⊃* ⦃G2, L2, T2⦄. -/2 width=5/ qed. +/2 width=5 by tri_step/ qed. lemma fsups_strap2: ∀G1,G,G2,L1,L,L2,T1,T,T2. ⦃G1, L1, T1⦄ ⊃⸮ ⦃G, L, T⦄ → ⦃G, L, T⦄ ⊃* ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ ⊃* ⦃G2, L2, T2⦄. -/2 width=5/ qed. +/2 width=5 by tri_TC_strap/ qed. + +lemma fsups_ldrop: ∀G1,G2,K1,K2,T1,T2. ⦃G1, K1, T1⦄ ⊃* ⦃G2, K2, T2⦄ → + ∀L1,U1,e. ⇩[0, e] L1 ≡ K1 → ⇧[0, e] T1 ≡ U1 → + ⦃G1, L1, U1⦄ ⊃* ⦃G2, K2, T2⦄. +#G1 #G2 #K1 #K2 #T1 #T2 #H @(fsups_ind … H) -G2 -K2 -T2 +/3 width=5 by fsups_strap1, fsupq_fsups, fsupq_drop/ +qed-. (* Basic forward lemmas *****************************************************) lemma fsups_fwd_fw: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃* ⦃G2, L2, T2⦄ → ♯{G2, L2, T2} ≤ ♯{G1, L1, T1}. -#G1 #G2 #L1 #L2 #T1 #T2 #H @(fsups_ind … H) -L2 -T2 // -/3 width=3 by fsupq_fwd_fw, transitive_le/ (**) (* slow even with trace *) +#G1 #G2 #L1 #L2 #T1 #T2 #H @(fsups_ind … H) -L2 -T2 +/3 width=3 by fsupq_fwd_fw, transitive_le/ qed-. -(* -(* Advanced inversion lemmas on plus-iterated supclosure ********************) - -lamma fsupp_inv_bind1_fsups: ∀b,J,G1,G2,L1,L2,W,U,T2. ⦃G1, L1, ⓑ{b,J}W.U⦄ ⊃+ ⦃G2, L2, T2⦄ → - ⦃G1, L1, W⦄ ⊃* ⦃G2, L2, T2⦄ ∨ ⦃L1.ⓑ{J}W, U⦄ ⊃* ⦃G2, L2, T2⦄. -#b #J #G1 #G2 #L1 #L2 #W #U #T2 #H @(fsupp_ind … H) -G2 -L2 -T2 -[ #G2 #L2 #T2 #H - elim (fsup_inv_bind1 … H) -H * #H1 #H2 #H3 destruct /2 width=1/ -| #G #G2 #L #L2 #T #T2 #_ #HT2 * /3 width=4/ -] -qad-. - -lamma fsupp_inv_flat1_fsups: ∀J,G1,G2,L1,L2,W,U,T2. ⦃G1, L1, ⓕ{J}W.U⦄ ⊃+ ⦃G2, L2, T2⦄ → - ⦃G1, L1, W⦄ ⊃* ⦃G2, L2, T2⦄ ∨ ⦃G1, L1, U⦄ ⊃* ⦃G2, L2, T2⦄. -#J #G1 #G2 #L1 #L2 #W #U #T2 #H @(fsupp_ind … H) -G2 -L2 -T2 -[ #G2 #L2 #T2 #H - elim (fsup_inv_flat1 … H) -H #H1 * #H2 destruct /2 width=1/ -| #G #G2 #L #L2 #T #T2 #_ #HT2 * /3 width=4/ -] -qad-. -*) diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/fsups_fsups.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/fsups_fsups.ma index 14f4b3f7a..fdee74619 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/substitution/fsups_fsups.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/fsups_fsups.ma @@ -19,4 +19,4 @@ include "basic_2/substitution/fsups.ma". (* Main properties **********************************************************) theorem fsups_trans: tri_transitive … fsups. -/2 width=5/ qed-. +/2 width=5 by tri_TC_transitive/ qed-. -- 2.39.2