From: Ferruccio Guidi Date: Thu, 24 Oct 2013 21:57:52 +0000 (+0000) Subject: - "small step" version of "big tree" theorem proved X-Git-Tag: make_still_working~1069 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=2ce98dc56948742e1d27ca4a8b96a3501962d968;p=helm.git - "small step" version of "big tree" theorem proved - some renaming --- diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/csx_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/csx_aaa.ma index 43e4d3ad5..f1b70f0c7 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/csx_aaa.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/csx_aaa.ma @@ -13,6 +13,7 @@ (**************************************************************************) include "basic_2/computation/acp_aaa.ma". +include "basic_2/computation/cpxs_aaa.ma". include "basic_2/computation/csx_tstc_vector.ma". (* CONTEXT-SENSITIVE EXTENDED STRONGLY NORMALIZING TERMS ********************) @@ -23,3 +24,35 @@ theorem aaa_csx: ∀h,g,G,L,T,A. ⦃G, L⦄ ⊢ T ⁝ A → ⦃G, L⦄ ⊢ ⬊*[ #h #g #G #L #T #A #H @(acp_aaa … (csx_acp h g) (csx_acr h g) … H) qed. + +(* Advanced eliminators *****************************************************) + +fact aaa_ind_csx_aux: ∀h,g,G,L,A. ∀R:predicate term. + (∀T1. ⦃G, L⦄ ⊢ T1 ⁝ A → + (∀T2. ⦃G, L⦄ ⊢ T1 ➡[h, g] T2 → (T1 = T2 → ⊥) → R T2) → R T1 + ) → + ∀T. ⦃G, L⦄ ⊢ ⬊*[h, g] T → ⦃G, L⦄ ⊢ T ⁝ A → R T. +#h #g #G #L #A #R #IH #T #H @(csx_ind … H) -T /4 width=5 by aaa_cpx_conf/ +qed-. + +lemma aaa_ind_csx: ∀h,g,G,L,A. ∀R:predicate term. + (∀T1. ⦃G, L⦄ ⊢ T1 ⁝ A → + (∀T2. ⦃G, L⦄ ⊢ T1 ➡[h, g] T2 → (T1 = T2 → ⊥) → R T2) → R T1 + ) → + ∀T. ⦃G, L⦄ ⊢ T ⁝ A → R T. +/5 width=9 by aaa_ind_csx_aux, aaa_csx/ qed-. + +fact aaa_ind_csx_alt_aux: ∀h,g,G,L,A. ∀R:predicate term. + (∀T1. ⦃G, L⦄ ⊢ T1 ⁝ A → + (∀T2. ⦃G, L⦄ ⊢ T1 ➡*[h, g] T2 → (T1 = T2 → ⊥) → R T2) → R T1 + ) → + ∀T. ⦃G, L⦄ ⊢ ⬊*[h, g] T → ⦃G, L⦄ ⊢ T ⁝ A → R T. +#h #g #G #L #A #R #IH #T #H @(csx_ind_alt … H) -T /4 width=5 by aaa_cpxs_conf/ +qed-. + +lemma aaa_ind_csx_alt: ∀h,g,G,L,A. ∀R:predicate term. + (∀T1. ⦃G, L⦄ ⊢ T1 ⁝ A → + (∀T2. ⦃G, L⦄ ⊢ T1 ➡*[h, g] T2 → (T1 = T2 → ⊥) → R T2) → R T1 + ) → + ∀T. ⦃G, L⦄ ⊢ T ⁝ A → R T. +/5 width=9 by aaa_ind_csx_alt_aux, aaa_csx/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/csx_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/csx_lift.ma index c431c349b..6c38825c8 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/csx_lift.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/csx_lift.ma @@ -13,6 +13,7 @@ (**************************************************************************) include "basic_2/reduction/cnx_lift.ma". +include "basic_2/reduction/fpbc.ma". include "basic_2/computation/acp.ma". include "basic_2/computation/csx.ma". @@ -27,7 +28,7 @@ lemma csx_lift: ∀h,g,G,L2,L1,T1,d,e. ⦃G, L1⦄ ⊢ ⬊*[h, g] T1 → @csx_intro #T #HLT2 #HT2 elim (cpx_inv_lift1 … HLT2 … HL21 … HT12) -HLT2 #T0 #HT0 #HLT10 @(IHT1 … HLT10) // -L1 -L2 #H destruct ->(lift_mono … HT0 … HT12) in HT2; -T1 /2 width=1/ +>(lift_mono … HT0 … HT12) in HT2; -T1 /2 width=1 by/ qed. (* Basic_1: was just: sn3_gen_lift *) @@ -38,9 +39,19 @@ lemma csx_inv_lift: ∀h,g,G,L2,L1,T1,d,e. ⦃G, L1⦄ ⊢ ⬊*[h, g] T1 → elim (lift_total T d e) #T0 #HT0 lapply (cpx_lift … HLT2 … HL12 … HT21 … HT0) -HLT2 #HLT10 @(IHT1 … HLT10) // -L1 -L2 #H destruct ->(lift_inj … HT0 … HT21) in HT2; -T1 /2 width=1/ +>(lift_inj … HT0 … HT21) in HT2; -T1 /2 width=1 by/ qed. +(* Advanced inversion lemmas ************************************************) + +(* Basic_1: was: sn3_gen_def *) +lemma csx_inv_lref_bind: ∀h,g,I,G,L,K,V,i. ⇩[0, i] L ≡ K.ⓑ{I}V → + ⦃G, L⦄ ⊢ ⬊*[h, g] #i → ⦃G, K⦄ ⊢ ⬊*[h, g] V. +#h #g #I #G #L #K #V #i #HLK #Hi +elim (lift_total V 0 (i+1)) +/4 width=9 by csx_inv_lift, csx_cpx_trans, cpx_delta, ldrop_fwd_ldrop2/ +qed-. + (* Advanced properties ******************************************************) (* Basic_1: was just: sn3_abbr *) @@ -51,9 +62,7 @@ elim (cpx_inv_lref1 … H) -H [ #H destruct elim Hi // | -Hi * #I0 #K0 #V0 #V1 #HLK0 #HV01 #HV1 lapply (ldrop_mono … HLK0 … HLK) -HLK #H destruct - lapply (ldrop_fwd_ldrop2 … HLK0) -HLK0 #HLK - @(csx_lift … HLK HV1) -HLK -HV1 - @(csx_cpx_trans … HV) -HV // + /3 width=7 by csx_lift, csx_cpx_trans, ldrop_fwd_ldrop2/ ] qed. @@ -65,37 +74,76 @@ lemma csx_appl_simple: ∀h,g,G,L,V. ⦃G, L⦄ ⊢ ⬊*[h, g] V → ∀T1. elim (cpx_inv_appl1_simple … H1) // -H1 #V0 #T0 #HLV0 #HLT10 #H destruct elim (eq_false_inv_tpair_dx … H2) -H2 -[ -IHV -HT1 #HT10 - @(csx_cpx_trans … (ⓐV.T0)) /2 width=1/ -HLV0 - @IHT1 -IHT1 // /2 width=1/ +[ -IHV -HT1 /4 width=3 by csx_cpx_trans, cpx_pair_sn/ | -HLT10 * #H #HV0 destruct - @IHV -IHV // -HT1 /2 width=1/ -HV0 - #T2 #HLT02 #HT02 - @(csx_cpx_trans … (ⓐV.T2)) /2 width=1/ -HLV0 - @IHT1 -IHT1 // -HLT02 /2 width=1/ + @IHV /4 width=3 by csx_cpx_trans, cpx_pair_sn/ (**) (* full auto 17s *) ] qed. -(* Advanced inversion lemmas ************************************************) +lemma csx_fqu_conf: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃ ⦃G2, L2, T2⦄ → + ⦃G1, L1⦄ ⊢ ⬊*[h, g] T1 → ⦃G2, L2⦄ ⊢ ⬊*[h, g] T2. +#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2 +/2 width=7 by csx_inv_lref_bind, csx_inv_lift, csx_fwd_flat_dx, csx_fwd_bind_dx, csx_fwd_pair_sn/ +qed-. -(* Basic_1: was: sn3_gen_def *) -lemma csx_inv_lref_bind: ∀h,g,I,G,L,K,V,i. ⇩[0, i] L ≡ K.ⓑ{I}V → - ⦃G, L⦄ ⊢ ⬊*[h, g] #i → ⦃G, K⦄ ⊢ ⬊*[h, g] V. -#h #g #I #G #L #K #V #i #HLK #Hi -elim (lift_total V 0 (i+1)) #V0 #HV0 -lapply (ldrop_fwd_ldrop2 … HLK) #H0LK -@(csx_inv_lift … H0LK … HV0) -H0LK -@(csx_cpx_trans … Hi) -Hi /2 width=7/ +lemma csx_fquq_conf: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃⸮ ⦃G2, L2, T2⦄ → + ⦃G1, L1⦄ ⊢ ⬊*[h, g] T1 → ⦃G2, L2⦄ ⊢ ⬊*[h, g] T2. +#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H12 #H elim (fquq_inv_gen … H12) -H12 +[ /2 width=5 by csx_fqu_conf/ +| * #HG #HL #HT destruct // +] +qed-. + +lemma csx_fqup_conf: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃+ ⦃G2, L2, T2⦄ → + ⦃G1, L1⦄ ⊢ ⬊*[h, g] T1 → ⦃G2, L2⦄ ⊢ ⬊*[h, g] T2. +#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H @(fqup_ind … H) -G2 -L2 -T2 +/3 width=5 by csx_fqu_conf/ +qed-. + +lemma csx_fqus_conf: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃* ⦃G2, L2, T2⦄ → + ⦃G1, L1⦄ ⊢ ⬊*[h, g] T1 → ⦃G2, L2⦄ ⊢ ⬊*[h, g] T2. +#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H12 #H elim (fqus_inv_gen … H12) -H12 +[ /2 width=5 by csx_fqup_conf/ +| * #HG #HL #HT destruct // +] +qed-. + +(* Advanced eliminators *****************************************************) + +lemma csx_ind_fpbc_fqus: ∀h,g. ∀R:relation3 genv lenv term. + (∀G1,L1,T1. ⦃G1, L1⦄ ⊢ ⬊*[h, g] T1 → + (∀G2,L2,T2. ⦃G1, L1, T1⦄ ≻[h, g] ⦃G2, L2, T2⦄ → R G2 L2 T2) → + R G1 L1 T1 + ) → + ∀G1,L1,T1. ⦃G1, L1⦄ ⊢ ⬊*[h, g] T1 → + ∀G2,L2,T2. ⦃G1, L1, T1⦄ ⊃* ⦃G2, L2, T2⦄ → R G2 L2 T2. +#h #g #R #IH1 #G1 #L1 #T1 #H @(csx_ind … H) -T1 +#T1 @(fqup_wf_ind … G1 L1 T1) -G1 -L1 -T1 +#G1 #L1 #T1 #IH2 #H1 #IH3 #G2 #L2 #T2 #H12 @IH1 -IH1 /2 width=5 by csx_fqus_conf/ +#G #L #T * +[ #G0 #L0 #T0 #H20 lapply (fqus_strap1_fqu … H12 H20) -G2 -L2 -T2 + #H10 @(IH2 … H10) -IH2 /2 width=5 by csx_fqup_conf/ + #T2 #HT02 #H #G3 #L3 #T3 #HT23 elim (fqup_cpx_trans_neq … H10 … HT02 H) -T0 + /4 width=8 by fqup_fqus_trans, fqup_fqus/ +| #T0 #HT20 #H elim (fqus_cpx_trans_neq … H12 … HT20 H) -T2 /3 width=4 by/ +] qed-. +lemma csx_ind_fpbc: ∀h,g. ∀R:relation3 genv lenv term. + (∀G1,L1,T1. ⦃G1, L1⦄ ⊢ ⬊*[h, g] T1 → + (∀G2,L2,T2. ⦃G1, L1, T1⦄ ≻[h, g] ⦃G2, L2, T2⦄ → R G2 L2 T2) → + R G1 L1 T1 + ) → + ∀G,L,T. ⦃G, L⦄ ⊢ ⬊*[h, g] T → R G L T. +/4 width=8 by csx_ind_fpbc_fqus/ qed-. + (* Main properties **********************************************************) theorem csx_acp: ∀h,g. acp (cpx h g) (eq …) (csx h g). #h #g @mk_acp -[ #G #L elim (deg_total h g 0) - #l #Hl lapply (cnx_sort_iter … L … Hl) /2 width=2/ -| @cnx_lift +[ #G #L elim (deg_total h g 0) /3 width=8 by cnx_sort_iter, ex_intro/ +| /3 width=12 by cnx_lift/ | /2 width=3 by csx_fwd_flat_dx/ -| /2 width=1/ +| /2 width=1 by csx_cast/ ] qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbg.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbg.ma index cc4ac8889..cf46c84d1 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbg.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbg.ma @@ -13,7 +13,6 @@ (**************************************************************************) include "basic_2/notation/relations/btpredstarproper_8.ma". -include "basic_2/substitution/fqup.ma". include "basic_2/reduction/fpbc.ma". include "basic_2/computation/fpbs.ma". @@ -46,7 +45,7 @@ lemma fpbg_strap1: ∀h,g,G1,G,G2,L1,L,L2,T1,T,T2. ⦃G1, L1, T1⦄ >[h, g] ⦃G ⦃G, L, T⦄ ≽[h, g] ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ >[h, g] ⦃G2, L2, T2⦄. #h #g #G1 #G #G2 #L1 #L #L2 #T1 #T #T2 #H1 #H2 lapply (fpbg_fwd_fpbs … H1) #H0 -elim (fpb_fpbc_or_refl … H2) -H2 [| * #HG2 #HL2 #HT2 destruct ] +elim (fpb_fpbc_or_fpn … H2) -H2 [| * #HG2 #HL2 #HT2 destruct ] /2 width=5 by fpbg_inj, fpbg_step/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbg_alt.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbg_alt.ma new file mode 100644 index 000000000..c74629d3f --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbg_alt.ma @@ -0,0 +1,37 @@ +(**************************************************************************) +(* ___ *) +(* ||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/notation/relations/btpredstarproper_8.ma". +include "basic_2/reduction/fpbc.ma". +include "basic_2/computation/fpbs.ma". + +(* "BIG TREE" PROPER PARALLEL COMPUTATION FOR CLOSURES **********************) + +inductive fpbg (h) (g) (G1) (L1) (T1): relation3 genv lenv term ≝ +| fpbg_cpxs: ∀L2,T2. ⦃G1, L1⦄ ⊢ T1 ➡*[h, g] T2 → (T1 = T2 → ⊥) → ⦃G1, L1⦄ ⊢ ➡*[h, g] L2 → + fpbg h g G1 L1 T1 G1 L2 T2 +| fpbg_fqup: ∀G2,L,L2,T,T2. ⦃G1, L1⦄ ⊢ T1 ➡*[h, g] T → ⦃G1, L1, T⦄ ⊃+ ⦃G2, L, T2⦄ → ⦃G2, L⦄ ⊢ ➡*[h, g] L2 → + fpbg h g G1 L1 T1 G2 L2 T2 +. + +interpretation "'big tree' proper parallel computation (closure)" + 'BTPRedStarProper h g G1 L1 T1 G2 L2 T2 = (fpbg h g G1 L1 T1 G2 L2 T2). + +(* Basic properties *********************************************************) + +lemma fpbc_fpbg: ∀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 * -G2 -L2 -T2 +/3 width=5 by fpbg_cpxs, fpbg_fqup, fqu_fqup, cpx_cpxs/ +qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs.ma index 8d42f50bf..064c94f04 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs.ma @@ -62,7 +62,7 @@ lemma fqus_fpbs: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃* ⦃G2, L2, T2 qed. lemma cpxs_fpbs: ∀h,g,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡*[h, g] T2 → ⦃G, L, T1⦄ ≥[h, g] ⦃G, L, T2⦄. -#h #g #G #L #T1 #T2 #H @(cpxs_ind … H) -T2 +#h #g #G #L #T1 #T2 #H @(cpxs_ind … H) -T2 /3 width=5 by fpb_cpx, fpbs_strap1/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/fpns.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fpns.ma new file mode 100644 index 000000000..29b81d043 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/fpns.ma @@ -0,0 +1,56 @@ +(**************************************************************************) +(* ___ *) +(* ||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/notation/relations/predsnstar_8.ma". +include "basic_2/reduction/fpn.ma". +include "basic_2/computation/lpxs.ma". + +(* ORDERED "BIG TREE" NORMAL FORMS ******************************************) + +definition fpns: ∀h. sd h → tri_relation genv lenv term ≝ + λh,g,G1,L1,T1,G2,L2,T2. + ∧∧ G1 = G2 & ⦃G1, L1⦄ ⊢ ➡*[h, g] L2 & T1 = T2. + +interpretation + "ordered 'big tree' normal forms (closure)" + 'PRedSnStar h g G1 L1 T1 G2 L2 T2 = (fpns h g G1 L1 T1 G2 L2 T2). + +(* Basic_properties *********************************************************) + +lemma fpns_refl: ∀h,g. tri_reflexive … (fpns h g). +/2 width=1 by and3_intro/ qed. + +lemma fpn_fpns: ∀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 * /3 width=1 by lpx_lpxs, and3_intro/ +qed. + +lemma fpns_strap1: ∀h,g,G1,G,G2,L1,L,L2,T1,T,T2. ⦃G1, L1, T1⦄ ⊢ ➡*[h, g] ⦃G, L, T⦄ → + ⦃G, L, T⦄ ⊢ ➡[h, g] ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ ⊢ ➡*[h, g] ⦃G2, L2, T2⦄. +#h #g #G1 #G #G2 #L1 #L #L2 #T1 #T #T2 * #H1G #H1L #G1T * +/3 width=3 by lpxs_strap1, and3_intro/ +qed-. + +lemma fpns_strap2: ∀h,g,G1,G,G2,L1,L,L2,T1,T,T2. ⦃G1, L1, T1⦄ ⊢ ➡[h, g] ⦃G, L, T⦄ → + ⦃G, L, T⦄ ⊢ ➡*[h, g] ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ ⊢ ➡*[h, g] ⦃G2, L2, T2⦄. +#h #g #G1 #G #G2 #L1 #L #L2 #T1 #T #T2 * #H1G #H1L #G1T * +/3 width=3 by lpxs_strap2, and3_intro/ +qed-. + +(* Basic forward lemmas *****************************************************) + +lemma fpns_fwd_bteq: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊢ ➡*[h, g] ⦃G2, L2, T2⦄ → + ⦃G1, L1, T1⦄ ⋕ ⦃G2, L2, T2⦄. +#h #g #G1 #G2 #L1 #L2 #T1 #T2 * /3 width=4 by lpxs_fwd_length, and3_intro/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/fsb.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fsb.ma index f8996e4a9..6c24fe86b 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/fsb.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/fsb.ma @@ -31,16 +31,14 @@ interpretation (* Basic eliminators ********************************************************) theorem fsb_ind_alt: ∀h,g. ∀R: relation3 …. ( - ∀G1,L1,T1. ( - ∀G2,L2,T2. ⦃G1, L1, T1⦄≽ [h, g] ⦃G2, L2, T2⦄ → - (|G1| = |G2| → |L1| = |L2| → T1 = T2 → ⊥) → ⦃G2, L2⦄ ⊢ ⦥[h,g] T2 - ) → ( - ∀G2,L2,T2. ⦃G1, L1, T1⦄≽ [h, g] ⦃G2, L2, T2⦄ → - (|G1| = |G2| → |L1| = |L2| → T1 = T2 → ⊥) → R G2 L2 T2 + ∀G1,L1,T1. ⦃G1, L1⦄ ⊢ ⦥[h,g] T1 → ( + ∀G2,L2,T2. ⦃G1, L1, T1⦄ ≽[h, g] ⦃G2, L2, T2⦄ → + (⦃G1, L1, T1⦄ ⋕ ⦃G2, L2, T2⦄ → ⊥) → R G2 L2 T2 ) → R G1 L1 T1 ) → ∀G,L,T. ⦃G, L⦄ ⊢ ⦥[h, g] T → R G L T. -#h #g #R #IH #G #L #T #H elim H -G -L -T /5 width=1 by fpb_fpbc/ +#h #g #R #IH #G #L #T #H elim H -G -L -T +/5 width=1 by fpb_fpbc, fsb_intro/ qed-. (* Basic inversion lemmas ***************************************************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/fsb_alt.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fsb_alt.ma new file mode 100644 index 000000000..1d9c2a497 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/fsb_alt.ma @@ -0,0 +1,48 @@ +(**************************************************************************) +(* ___ *) +(* ||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/notation/relations/btsnalt_5.ma". +include "basic_2/computation/fpbg_alt.ma". +include "basic_2/computation/fsb.ma". + +(* "BIG TREE" STRONGLY NORMALIZING TERMS ************************************) + +(* Note: alternative definition of fsb *) +inductive fsba (h) (g): relation3 genv lenv term ≝ +| fsba_intro: ∀G1,L1,T1. ( + ∀G2,L2,T2. ⦃G1, L1, T1⦄ >[h, g] ⦃G2, L2, T2⦄ → fsba h g G2 L2 T2 + ) → fsba h g G1 L1 T1. + +interpretation + "'big tree' strong normalization (closure) alternative" + 'BTSNAlt h g G L T = (fsba h g G L T). + +(* Basic eliminators ********************************************************) + +theorem fsba_ind_alt: ∀h,g. ∀R: relation3 …. ( + ∀G1,L1,T1. ⦃G1, L1⦄ ⊢ ⦥⦥[h,g] T1 → ( + ∀G2,L2,T2. ⦃G1, L1, T1⦄ >[h, g] ⦃G2, L2, T2⦄ → R G2 L2 T2 + ) → R G1 L1 T1 + ) → + ∀G,L,T. ⦃G, L⦄ ⊢ ⦥⦥[h, g] T → R G L T. +#h #g #R #IH #G #L #T #H elim H -G -L -T +/4 width=1 by fsba_intro/ +qed-. + +(* Main inversion lemmas ****************************************************) + +theorem fsba_inv_fsb: ∀h,g,G,L,T. ⦃G, L⦄ ⊢ ⦥⦥[h, g] T → ⦃G, L⦄ ⊢ ⦥[h, g] T. +#h #g #G #L #T #H @(fsba_ind_alt … H) -G -L -T +/4 width=1 by fsb_intro, fpbc_fpbg/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/fsb_csx.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fsb_csx.ma new file mode 100644 index 000000000..6b1e14497 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/fsb_csx.ma @@ -0,0 +1,30 @@ +(**************************************************************************) +(* ___ *) +(* ||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/computation/csx_aaa.ma". +include "basic_2/computation/fsb.ma". + +(* "BIG TREE" STRONGLY NORMALIZING TERMS ************************************) + +(* Advanced propreties ******************************************************) + +lemma csx_fsb: ∀h,g,G,L,T. ⦃G, L⦄ ⊢ ⬊*[h, g] T → ⦃G, L⦄ ⊢ ⦥[h, g] T. +#h #g #G #L #T #H @(csx_ind_fpbc … H) -T /3 width=1 by fsb_intro/ +qed. + +(* Main properties **********************************************************) + +(* Note: this is the "big tree" theorem ("small step" version) *) +theorem aaa_fsb: ∀h,g,G,L,T,A. ⦃G, L⦄ ⊢ T ⁝ A → ⦃G, L⦄ ⊢ ⦥[h, g] T. +/3 width=2 by aaa_csx, csx_fsb/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/fpn/fpbs_conj.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/fpn/fpbs_conj.etc new file mode 100644 index 000000000..8d0f137df --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/fpn/fpbs_conj.etc @@ -0,0 +1,34 @@ +(* +inclade "basic_2/computation/fpns.ma". +inclade "basic_2/computation/fpbs.ma". +inclade "basic_2/reduction/fpbc.ma". + +lemma fpn_dec: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ≽[h, g] ⦃G2, L2, T2⦄ → + Decidable (⦃G1, L1, T1⦄ ⊢ ➡[h, g] ⦃G2, L2, T2⦄). +#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H elim (fpb_fpbc_or_fpn … H) -H /2 width=1 by or_introl/ +#H12 @or_intror +#H @(fpbc_fwd_bteq … H12) -H12 @(fpn_fwd_bteq … H) +qed-. +*) +(* +lemma fpns_dec: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ≥[h, g] ⦃G2, L2, T2⦄ → + Decidable (⦃G1, L1, T1⦄ ⊢ ➡*[h, g] ⦃G2, L2, T2⦄). +#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H @(fpbs_ind … H) -G2 -L2 -T2 /2 width=1 by or_introl/ +#G #G2 #L #L2 #T #T2 #H #H2 * +#H1 elim (fpn_dec … H2) -H2 #H2 /3 width=5 by fpns_strap1, or_introl/ +[ @or_intror #H12 +| @or_intror #H12 @H1 -H1 +*) +(* +inclade "basic_2/grammar/bteq_bteq.ma". +inclade "basic_2/computation/fpns.ma". + +(* Advanced forward lemmas **************************************************) + +lemma fpbs_bteq_fwd_fpns: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ≥[h, g] ⦃G2, L2, T2⦄ → + ⦃G1, L1, T1⦄ ⋕ ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ ⊢ ➡*[h, g] ⦃G2, L2, T2⦄. +#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H @(fpbs_ind … H) -G2 -L2 -T2 // +#G #G2 #L #L2 #T #T2 #H1 #H2 #IH1 #H12 elim (bteq_dec G1 G L1 L T1 T) +[ -H1 /4 width=10 by fpns_strap1, fpb_bteq_fwd_fpn, bteq_canc_sn/ +| -IH1 #H +*) diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/fpn/fsb_alt.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/fpn/fsb_alt.etc new file mode 100644 index 000000000..8c69a001d --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/fpn/fsb_alt.etc @@ -0,0 +1,105 @@ +(**************************************************************************) +(* ___ *) +(* ||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/notation/relations/btsnalt_5.ma". +include "basic_2/computation/fpbs_fpbs.ma". +include "basic_2/computation/fsb.ma". + +(* "BIG TREE" STRONGLY NORMALIZING TERMS ************************************) + +(* Note: alternative definition of fsb *) +inductive fsba (h) (g): relation3 genv lenv term ≝ +| fsba_intro: ∀G1,L1,T1. ( + ∀G2,L2,T2. ⦃G1, L1, T1⦄ ≥[h, g] ⦃G2, L2, T2⦄ → + (⦃G1, L1, T1⦄ ⋕ ⦃G2, L2, T2⦄ → ⊥) → fsba h g G2 L2 T2 + ) → fsba h g G1 L1 T1. + +interpretation + "'big tree' strong normalization (closure) alternative" + 'BTSNAlt h g G L T = (fsba h g G L T). + +(* Basic eliminators ********************************************************) + +theorem fsba_ind_alt: ∀h,g. ∀R: relation3 …. ( + ∀G1,L1,T1. ⦃G1, L1⦄ ⊢ ⦥⦥[h,g] T1 → ( + ∀G2,L2,T2. ⦃G1, L1, T1⦄ ≥[h, g] ⦃G2, L2, T2⦄ → + (⦃G1, L1, T1⦄ ⋕ ⦃G2, L2, T2⦄ → ⊥) → R G2 L2 T2 + ) → R G1 L1 T1 + ) → + ∀G,L,T. ⦃G, L⦄ ⊢ ⦥⦥[h, g] T → R G L T. +#h #g #R #IH #G #L #T #H elim H -G -L -T +/5 width=1 by fsba_intro/ +qed-. + +(* Basic_properties *********************************************************) + +fact fsba_intro_aux: ∀h,g,G1,L1,T1. ( + ∀G,G2,L,L2,T,T2. ⦃G, L, T⦄ ≥[h, g] ⦃G2, L2, T2⦄ → + ⦃G1, L1, T1⦄ ⋕ ⦃G, L, T⦄ → + (⦃G1, L1, T1⦄ ⋕ ⦃G2, L2, T2⦄ → ⊥) → fsba h g G2 L2 T2 + ) → fsba h g G1 L1 T1. +/4 width=5 by fsba_intro/ qed-. + +lemma fsba_fpbs_trans: ∀h,g,G1,L1,T1. ⦃G1, L1⦄ ⊢ ⦥⦥[h, g] T1 → + ∀G2,L2,T2. ⦃G1, L1, T1⦄ ≥[h, g] ⦃G2, L2, T2⦄ → ⦃G2, L2⦄ ⊢ ⦥⦥[h, g] T2. +#h #g #G1 #L1 #T1 #H @(fsba_ind_alt … H) -G1 -L1 -T1 +#G1 #L1 #T1 #H0 #IH0 #G #L #T #H1 @fsba_intro +#G2 #L2 #T2 #H2 #_ lapply (fpbs_trans … H1 … H2) -G -L -T +#H12 elim (bteq_dec G1 G2 L1 L2 T1 T2) /3 width=6 by fpb_fpbs/ +-IH0 #H212 + + + -H0 -H #H @(IH0 … H) -IH0 -H // @(fpbs_trans … H1 … H2) + +lemma fsba_intro_fpb: ∀h,g,G1,L1,T1. ( + ∀G2,L2,T2. ⦃G1, L1, T1⦄ ≽[h, g] ⦃G2, L2, T2⦄ → + (⦃G1, L1, T1⦄ ⋕ ⦃G2, L2, T2⦄ → ⊥) → ⦃G2, L2⦄ ⊢ ⦥⦥[h, g] T2 + ) → ⦃G1, L1⦄ ⊢ ⦥⦥[h, g] T1. +#h #g #G1 #L1 #T1 #IH1 @fsba_intro_aux +#G #G2 #L #L2 #T #T2 #H @(fpbs_ind_dx … H) -G -L -T +[ #H1 #H2 -IH1 elim H2 -H2 // +| #G0 #G #L0 #L #T0 #T #H10 #H12 #IH2 #H210 #H212 elim (bteq_dec G1 G L1 L T1 T) + [ -IH1 -H210 -H10 -H12 /3 width=1 by/ + | -IH2 -H212 #H21 lapply (IH1 … H21) -IH1 -H21 + [ + | -H10 -H210 #H +(* +(* Main inversion lemmas ****************************************************) + +theorem fsba_inv_fsb: ∀h,g,G,L,T. ⦃G, L⦄ ⊢ ⦥⦥[h, g] T → ⦃G, L⦄ ⊢ ⦥[h, g] T. +#h #g #G #L #T #H elim H -G -L -T +/5 width=12 by fsb_intro, fpb_fpbs, fpbc_fwd_fpb, fpbc_fwd_gen/ +qed-. + +(* Main properties **********************************************************) + +theorem fsb_fsba: ∀h,g,G,L,T. ⦃G, L⦄ ⊢ ⦥[h, g] T → ⦃G, L⦄ ⊢ ⦥⦥[h, g] T. +#h #g #G #L #T #H @(fsb_ind_alt … H) -G -L -T +/4 width=1 by fsba_intro_fpb/ +qed. +(* +| fsba_intro: ∀G1,L1,T1. ( + ∀G2,L2,T2. ⦃G1, L1, T1⦄ ≻[h, g] ⦃G2, L2, T2⦄ → fsb h g G2 L2 T2 + ) → fsb h g G1 L1 T1 +. + + + +(****************************************************************************) + +include "basic_2/substitution/fqup.ma". + +lemma fsb_csx: ∀h,g,G,L,T. ⦃G, L⦄ ⊢ ⬊*[h, g] T → ⦃G, L⦄ ⊢ ⦥[h, g] T. +#h #g #G #L #T #H @(csx_ind … H) -T +*)*) diff --git a/matita/matita/contribs/lambdadelta/basic_2/grammar/bteq.ma b/matita/matita/contribs/lambdadelta/basic_2/grammar/bteq.ma index 73e04e3d5..c909e2ed6 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/grammar/bteq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/grammar/bteq.ma @@ -35,7 +35,7 @@ lemma bteq_sym: tri_symmetric … bteq. #G1 #G2 #L1 #L2 #T1 #T2 * // qed-. -lemma bteq_dec: ∀G1,G2,L1,L2,T1,T2. Decidable (⦃G1, L1, T1⦄ ⪴ ⦃G2, L2, T2⦄). +lemma bteq_dec: ∀G1,G2,L1,L2,T1,T2. Decidable (⦃G1, L1, T1⦄ ⋕ ⦃G2, L2, T2⦄). #G1 #G2 #L1 #L2 #T1 #T2 elim (genv_eq_dec G1 G2) #H1G [2: @or_intror * #H2G #H2L #H2T destruct /2 width=1 by/ ] elim (eq_nat_dec (|L1|) (|L2|)) diff --git a/matita/matita/contribs/lambdadelta/basic_2/grammar/bteq_bteq.ma b/matita/matita/contribs/lambdadelta/basic_2/grammar/bteq_bteq.ma index 4dad596fd..7870b2644 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/grammar/bteq_bteq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/grammar/bteq_bteq.ma @@ -21,3 +21,11 @@ include "basic_2/grammar/bteq.ma". theorem bteq_trans: tri_transitive … bteq. #G1 #G #L1 #L #T1 #T * // qed-. + +theorem bteq_canc_sn: ∀G,G1,G2,L,L1,L2,T,T1,T2. ⦃G, L, T⦄ ⋕ ⦃G1, L1, T1⦄ → + ⦃G, L, T⦄ ⋕ ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ ⋕ ⦃G2, L2, T2⦄. +/3 width=5 by bteq_trans, bteq_sym/ qed-. + +theorem bteq_canc_dx: ∀G1,G2,G,L1,L2,L,T1,T2,T. ⦃G1, L1, T1⦄ ⋕ ⦃G, L, T⦄ → + ⦃G2, L2, T2⦄ ⋕ ⦃G, L, T⦄ → ⦃G1, L1, T1⦄ ⋕ ⦃G2, L2, T2⦄. +/3 width=5 by bteq_trans, bteq_sym/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/names.txt b/matita/matita/contribs/lambdadelta/basic_2/names.txt index 5530ee711..b5405f69d 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/names.txt +++ b/matita/matita/contribs/lambdadelta/basic_2/names.txt @@ -58,7 +58,7 @@ l: sn contex-sensitive for local environments r: dx contex-sensitive for local environments t: context-free for terms --second letter +- second letter i: irreducible form n: normal form @@ -73,6 +73,7 @@ b: "big tree" reduction c: conversion d: decomposed extended reduction e: decomposed extended conversion +n: order on "big tree" normal forms q: restricted reduction r: reduction s: substitution diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/bteq_6.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/bteq_6.ma index a417d0ac7..5ee962fe5 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/bteq_6.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/bteq_6.ma @@ -14,6 +14,6 @@ (* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) -notation "hvbox( ⦃ term 46 G1, break term 46 L1, break term 46 T1 ⦄ ⪴ break ⦃ term 46 G2, break term 46 L2 , break term 46 T2 ⦄ )" +notation "hvbox( ⦃ term 46 G1, break term 46 L1, break term 46 T1 ⦄ ⋕ break ⦃ term 46 G2, break term 46 L2 , break term 46 T2 ⦄ )" non associative with precedence 45 for @{ 'BTEq $G1 $L1 $T1 $G2 $L2 $T2 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predsn_8.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predsn_8.ma new file mode 100644 index 000000000..dc3b08203 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predsn_8.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 G1, break term 46 L1, break term 46 T1 ⦄ ⊢ ➡ break [ term 46 h , break term 46 g ] break ⦃ term 46 G2, break term 46 L2 , break term 46 T2 ⦄ )" + non associative with precedence 45 + for @{ 'PRedSn $h $g $G1 $L1 $T1 $G2 $L2 $T2 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predsnstar_8.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predsnstar_8.ma new file mode 100644 index 000000000..f396ff17d --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predsnstar_8.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 G1, break term 46 L1, break term 46 T1 ⦄ ⊢ ➡ * break [ term 46 h , break term 46 g ] break ⦃ term 46 G2, break term 46 L2 , break term 46 T2 ⦄ )" + non associative with precedence 45 + for @{ 'PRedSnStar $h $g $G1 $L1 $T1 $G2 $L2 $T2 }. 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 6dd309deb..eeb23f7b5 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/fquq_alt.ma". +include "basic_2/substitution/fqus_alt.ma". include "basic_2/static/ssta.ma". include "basic_2/reduction/cpx.ma". @@ -145,7 +145,7 @@ lemma fqu_cpx_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃ ⦃G2, L2, T /3 width=3 by fqu_pair_sn, fqu_bind_dx, fqu_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 fqu_drop, cpx_append, cpx_delta, ldrop_pair, ldrop_ldrop, ex2_intro/ + /4 width=7 by fqu_drop, 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, fqu_drop, ex2_intro/ @@ -172,3 +172,63 @@ lemma fquq_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 fquq_cpx_trans, ssta_cpx/ qed-. + +lemma fqu_cpx_trans_neq: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃ ⦃G2, L2, T2⦄ → + ∀U2. ⦃G2, L2⦄ ⊢ T2 ➡[h, g] U2 → (T2 = U2 → ⊥) → + ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ➡[h, g] U1 & T1 = U1 → ⊥ & ⦃G1, L1, U1⦄ ⊃ ⦃G2, L2, U2⦄. +#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2 +[ #I #G #L #V1 #V2 #HV12 #_ elim (lift_total V2 0 1) + #U2 #HVU2 @(ex3_intro … U2) + [1,3: /3 width=7 by fqu_drop, cpx_delta, ldrop_pair, ldrop_ldrop/ + | #H destruct /2 width=7 by lift_inv_lref2_be/ + ] +| #I #G #L #V1 #T #V2 #HV12 #H @(ex3_intro … (②{I}V2.T)) + [1,3: /2 width=4 by fqu_pair_sn, cpx_pair_sn/ + | #H0 destruct /2 width=1 by/ + ] +| #a #I #G #L #V #T1 #T2 #HT12 #H @(ex3_intro … (ⓑ{a,I}V.T2)) + [1,3: /2 width=4 by fqu_bind_dx, cpx_bind/ + | #H0 destruct /2 width=1 by/ + ] +| #I #G #L #V #T1 #T2 #HT12 #H @(ex3_intro … (ⓕ{I}V.T2)) + [1,3: /2 width=4 by fqu_flat_dx, cpx_flat/ + | #H0 destruct /2 width=1 by/ + ] +| #G #L #K #T1 #U1 #e #HLK #HTU1 #T2 #HT12 #H elim (lift_total T2 0 (e+1)) + #U2 #HTU2 @(ex3_intro … U2) + [1,3: /2 width=9 by cpx_lift, fqu_drop/ + | #H0 destruct /3 width=5 by lift_inj/ +] +qed-. + +lemma fquq_cpx_trans_neq: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃⸮ ⦃G2, L2, T2⦄ → + ∀U2. ⦃G2, L2⦄ ⊢ T2 ➡[h, g] U2 → (T2 = U2 → ⊥) → + ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ➡[h, g] U1 & T1 = U1 → ⊥ & ⦃G1, L1, U1⦄ ⊃⸮ ⦃G2, L2, U2⦄. +#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H12 #U2 #HTU2 #H elim (fquq_inv_gen … H12) -H12 +[ #H12 elim (fqu_cpx_trans_neq … H12 … HTU2 H) -T2 + /3 width=4 by fqu_fquq, ex3_intro/ +| * #HG #HL #HT destruct /3 width=4 by ex3_intro/ +] +qed-. + +lemma fqup_cpx_trans_neq: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃+ ⦃G2, L2, T2⦄ → + ∀U2. ⦃G2, L2⦄ ⊢ T2 ➡[h, g] U2 → (T2 = U2 → ⊥) → + ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ➡[h, g] U1 & T1 = U1 → ⊥ & ⦃G1, L1, U1⦄ ⊃+ ⦃G2, L2, U2⦄. +#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H @(fqup_ind_dx … H) -G1 -L1 -T1 +[ #G1 #L1 #T1 #H12 #U2 #HTU2 #H elim (fqu_cpx_trans_neq … H12 … HTU2 H) -T2 + /3 width=4 by fqu_fqup, ex3_intro/ +| #G #G1 #L #L1 #T #T1 #H1 #_ #IH12 #U2 #HTU2 #H elim (IH12 … HTU2 H) -T2 + #U1 #HTU1 #H #H12 elim (fqu_cpx_trans_neq … H1 … HTU1 H) -T1 + /3 width=8 by fqup_strap2, ex3_intro/ +] +qed-. + +lemma fqus_cpx_trans_neq: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃* ⦃G2, L2, T2⦄ → + ∀U2. ⦃G2, L2⦄ ⊢ T2 ➡[h, g] U2 → (T2 = U2 → ⊥) → + ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ➡[h, g] U1 & T1 = U1 → ⊥ & ⦃G1, L1, U1⦄ ⊃* ⦃G2, L2, U2⦄. +#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H12 #U2 #HTU2 #H elim (fqus_inv_gen … H12) -H12 +[ #H12 elim (fqup_cpx_trans_neq … H12 … HTU2 H) -T2 + /3 width=4 by fqup_fqus, ex3_intro/ +| * #HG #HL #HT destruct /3 width=4 by ex3_intro/ +] +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/fpb.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/fpb.ma index 05bd28248..1abe847ab 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/reduction/fpb.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/fpb.ma @@ -13,8 +13,8 @@ (**************************************************************************) include "basic_2/notation/relations/btpred_8.ma". -include "basic_2/relocation/fquq.ma". -include "basic_2/reduction/lpx.ma". +include "basic_2/relocation/fquq_alt.ma". +include "basic_2/reduction/fpn.ma". (* "BIG TREE" PARALLEL REDUCTION FOR CLOSURES *******************************) @@ -38,3 +38,16 @@ lemma cpr_fpb: ∀h,g,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡ T2 → ⦃G, L, T1⦄ ≽ lemma lpr_fpb: ∀h,g,G,L1,L2,T. ⦃G, L1⦄ ⊢ ➡ L2 → ⦃G, L1, T⦄ ≽[h, g] ⦃G, L2, T⦄. /3 width=1 by fpb_lpx, lpr_lpx/ qed. + +(* Basic forward lemmas *****************************************************) + +lemma fpb_bteq_fwd_fpn: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ≽[h, g] ⦃G2, L2, T2⦄ → + ⦃G1, L1, T1⦄ ⋕ ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ ⊢ ➡[h, g] ⦃G2, L2, T2⦄. +#h #g #G1 #G2 #L1 #L2 #T1 #T2 * -G2 -L2 -T2 /2 width=1 by and3_intro/ +[ #G2 #L2 #T2 #H elim (fquq_inv_gen … H) -H + [ #H1 #H2 elim (fqu_fwd_bteq … H1 H2) + | * #HG #HL #HT #_ destruct // + ] +| #T2 #HT12 * // +] +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/fpbc.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/fpbc.ma index ec64bd5a6..c560a1ab0 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/reduction/fpbc.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/fpbc.ma @@ -13,7 +13,6 @@ (**************************************************************************) include "basic_2/notation/relations/btpredproper_8.ma". -include "basic_2/relocation/fquq_alt.ma". include "basic_2/reduction/fpb.ma". (* "BIG TREE" PROPER PARALLEL REDUCTION FOR CLOSURES ************************) @@ -33,9 +32,9 @@ lemma cpr_fpbc: ∀h,g,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡ T2 → (T1 = T2 → ⊥) ⦃G, L, T1⦄ ≻[h, g] ⦃G, L, T2⦄. /3 width=1 by fpbc_cpx, cpr_cpx/ qed. -lemma fpb_fpbc_or_refl: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ≽[h, g] ⦃G2, L2, T2⦄ → - ⦃G1, L1, T1⦄ ≻[h, g] ⦃G2, L2, T2⦄ ∨ - ∧∧ G1 = G2 & ⦃G1, L1⦄ ⊢ ➡[h, g] L2 & T1 = T2. +lemma fpb_fpbc_or_fpn: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ≽[h, g] ⦃G2, L2, 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 * -G2 -L2 -T2 /3 width=1 by and3_intro, or_intror/ [ #G2 #L2 #T2 #H elim (fquq_inv_gen … H) -H [| * ] @@ -46,11 +45,10 @@ lemma fpb_fpbc_or_refl: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ≽[h, g] ⦃ qed-. lemma fpb_fpbc: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ≽[h, g] ⦃G2, L2, T2⦄ → - (|G1| = |G2| → |L1| = |L2| → T1 = T2 → ⊥) → + (⦃G1, L1, T1⦄ ⋕ ⦃G2, L2, T2⦄ → ⊥) → ⦃G1, L1, T1⦄ ≻[h, g] ⦃G2, L2, T2⦄. -#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H #H0 elim (fpb_fpbc_or_refl … H) -H // * -#HG #HL #HT destruct lapply (lpx_fwd_length … HL) -HL #HL -elim H0 -H0 // +#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H #H0 elim (fpb_fpbc_or_fpn … H) -H // +#H elim H0 -H0 /2 width=3 by fpn_fwd_bteq/ qed. (* Basic forward lemmas *****************************************************) @@ -61,8 +59,8 @@ lemma fpbc_fwd_fpb: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ≻[h, g] ⦃G2, /3 width=1 by fpb_fquq, fpb_cpx, fqu_fquq/ qed-. -lemma fpbc_fwd_gen: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ≻[h, g] ⦃G2, L2, T2⦄ → - |G1| = |G2| → |L1| = |L2| → T1 = T2 → ⊥. -#h #g #G1 #G2 #L1 #L2 #T1 #T2 * -G2 -L2 -T2 /2 width=1 by / -#G2 #L2 #T2 #H #HG #HL #HT @(fqu_fwd_gen … H) -H // (**) (* auto does not work *) +lemma fpbc_fwd_bteq: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ≻[h, g] ⦃G2, L2, T2⦄ → + ⦃G1, L1, T1⦄ ⋕ ⦃G2, L2, T2⦄ → ⊥. +#h #g #G1 #G2 #L1 #L2 #T1 #T2 * -G2 -L2 -T2 /2 width=8 by fqu_fwd_bteq/ +#T2 #_ #HT12 * /2 width=1 by/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/fpn.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/fpn.ma new file mode 100644 index 000000000..f33adbde9 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/fpn.ma @@ -0,0 +1,39 @@ +(**************************************************************************) +(* ___ *) +(* ||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/notation/relations/predsn_8.ma". +include "basic_2/grammar/bteq.ma". +include "basic_2/reduction/lpx.ma". + +(* ADJACENT "BIG TREE" NORMAL FORMS *****************************************) + +definition fpn: ∀h. sd h → tri_relation genv lenv term ≝ + λh,g,G1,L1,T1,G2,L2,T2. + ∧∧ G1 = G2 & ⦃G1, L1⦄ ⊢ ➡[h, g] L2 & T1 = T2. + +interpretation + "adjacent 'big tree' normal forms (closure)" + 'PRedSn h g G1 L1 T1 G2 L2 T2 = (fpn h g G1 L1 T1 G2 L2 T2). + +(* Basic_properties *********************************************************) + +lemma fpn_refl: ∀h,g. tri_reflexive … (fpn h g). +/2 width=1 by and3_intro/ qed. + +(* Basic forward lemmas *****************************************************) + +lemma fpn_fwd_bteq: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊢➡[h, g] ⦃G2, L2, T2⦄ → + ⦃G1, L1, T1⦄ ⋕ ⦃G2, L2, T2⦄. +#h #g #G1 #G2 #L1 #L2 #T1 #T2 * /3 width=4 by lpx_fwd_length, and3_intro/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/lpr_lpr.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/lpr_lpr.ma index addc2f948..933bcd637 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/reduction/lpr_lpr.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/lpr_lpr.ma @@ -22,7 +22,7 @@ include "basic_2/reduction/lpr_ldrop.ma". fact cpr_conf_lpr_atom_atom: ∀I,G,L1,L2. ∃∃T. ⦃G, L1⦄ ⊢ ⓪{I} ➡ T & ⦃G, L2⦄ ⊢ ⓪{I} ➡ T. -/2 width=3/ qed-. +/2 width=3 by cpr_atom, ex2_intro/ qed-. fact cpr_conf_lpr_atom_delta: ∀G,L0,i. ( @@ -43,8 +43,8 @@ elim (lpr_inv_pair1 … H2) -H2 #K2 #W2 #HK02 #_ #H destruct lapply (ldrop_fwd_ldrop2 … HLK2) -W2 #HLK2 lapply (fqup_lref … G … HLK0) -HLK0 #HLK0 elim (IH … HLK0 … HV01 … HV02 … HK01 … HK02) -L0 -K0 -V0 #V #HV1 #HV2 -elim (lift_total V 0 (i+1)) #T #HVT -lapply (cpr_lift … HV2 … HLK2 … HVT2 … HVT) -K2 -V2 /3 width=6/ +elim (lift_total V 0 (i+1)) +/3 width=11 by cpr_lift, cpr_delta, ex2_intro/ qed-. (* Basic_1: includes: pr0_delta_delta pr2_delta_delta *) @@ -72,9 +72,7 @@ elim (lpr_inv_pair1 … H2) -H2 #K2 #W2 #HK02 #_ #H destruct lapply (ldrop_fwd_ldrop2 … HLK2) -W2 #HLK2 lapply (fqup_lref … G … HLK0) -HLK0 #HLK0 elim (IH … HLK0 … HV01 … HV02 … HK01 … HK02) -L0 -K0 -V0 #V #HV1 #HV2 -elim (lift_total V 0 (i+1)) #T #HVT -lapply (cpr_lift … HV1 … HLK1 … HVT1 … HVT) -K1 -V1 -lapply (cpr_lift … HV2 … HLK2 … HVT2 … HVT) -K2 -V2 -V /2 width=3/ +elim (lift_total V 0 (i+1)) /3 width=11 by cpr_lift, ex2_intro/ qed-. fact cpr_conf_lpr_bind_bind: @@ -91,7 +89,8 @@ fact cpr_conf_lpr_bind_bind: #a #I #G #L0 #V0 #T0 #IH #V1 #HV01 #T1 #HT01 #V2 #HV02 #T2 #HT02 #L1 #HL01 #L2 #HL02 elim (IH … HV01 … HV02 … HL01 … HL02) // -elim (IH … HT01 … HT02 (L1.ⓑ{I}V1) … (L2.ⓑ{I}V2)) -IH // /2 width=1/ /3 width=5/ +elim (IH … HT01 … HT02 (L1.ⓑ{I}V1) … (L2.ⓑ{I}V2)) -IH +/3 width=5 by lpr_pair, cpr_bind, ex2_intro/ qed-. fact cpr_conf_lpr_bind_zeta: @@ -107,8 +106,8 @@ fact cpr_conf_lpr_bind_zeta: ∃∃T. ⦃G, L1⦄ ⊢ +ⓓV1.T1 ➡ T & ⦃G, L2⦄ ⊢ X2 ➡ T. #G #L0 #V0 #T0 #IH #V1 #HV01 #T1 #HT01 #T2 #HT02 #X2 #HXT2 #L1 #HL01 #L2 #HL02 -elim (IH … HT01 … HT02 (L1.ⓓV1) … (L2.ⓓV1)) -IH -HT01 -HT02 // /2 width=1/ -L0 -V0 -T0 #T #HT1 #HT2 -elim (cpr_inv_lift1 … HT2 L2 … HXT2) -T2 /2 width=1/ /3 width=3/ +elim (IH … HT01 … HT02 (L1.ⓓV1) … (L2.ⓓV1)) -IH -HT01 -HT02 /2 width=1 by lpr_pair/ -L0 -V0 -T0 #T #HT1 #HT2 +elim (cpr_inv_lift1 … HT2 L2 … HXT2) -T2 /3 width=3 by cpr_zeta, ldrop_ldrop, ex2_intro/ qed-. fact cpr_conf_lpr_zeta_zeta: @@ -124,10 +123,10 @@ fact cpr_conf_lpr_zeta_zeta: ∃∃T. ⦃G, L1⦄ ⊢ X1 ➡ T & ⦃G, L2⦄ ⊢ X2 ➡ T. #G #L0 #V0 #T0 #IH #T1 #HT01 #X1 #HXT1 #T2 #HT02 #X2 #HXT2 #L1 #HL01 #L2 #HL02 -elim (IH … HT01 … HT02 (L1.ⓓV0) … (L2.ⓓV0)) -IH -HT01 -HT02 // /2 width=1/ -L0 -T0 #T #HT1 #HT2 -elim (cpr_inv_lift1 … HT1 L1 … HXT1) -T1 /2 width=1/ #T1 #HT1 #HXT1 -elim (cpr_inv_lift1 … HT2 L2 … HXT2) -T2 /2 width=1/ #T2 #HT2 #HXT2 -lapply (lift_inj … HT2 … HT1) -T #H destruct /2 width=3/ +elim (IH … HT01 … HT02 (L1.ⓓV0) … (L2.ⓓV0)) -IH -HT01 -HT02 /2 width=1 by lpr_pair/ -L0 -T0 #T #HT1 #HT2 +elim (cpr_inv_lift1 … HT1 L1 … HXT1) -T1 /2 width=1 by ldrop_ldrop/ #T1 #HT1 #HXT1 +elim (cpr_inv_lift1 … HT2 L2 … HXT2) -T2 /2 width=1 by ldrop_ldrop/ #T2 #HT2 #HXT2 +lapply (lift_inj … HT2 … HT1) -T #H destruct /2 width=3 by ex2_intro/ qed-. fact cpr_conf_lpr_flat_flat: @@ -144,7 +143,7 @@ fact cpr_conf_lpr_flat_flat: #I #G #L0 #V0 #T0 #IH #V1 #HV01 #T1 #HT01 #V2 #HV02 #T2 #HT02 #L1 #HL01 #L2 #HL02 elim (IH … HV01 … HV02 … HL01 … HL02) // -elim (IH … HT01 … HT02 … HL01 … HL02) // /3 width=5/ +elim (IH … HT01 … HT02 … HL01 … HL02) /3 width=5 by cpr_flat, ex2_intro/ qed-. fact cpr_conf_lpr_flat_tau: @@ -159,7 +158,7 @@ fact cpr_conf_lpr_flat_tau: ∃∃T. ⦃G, L1⦄ ⊢ ⓝV1.T1 ➡ T & ⦃G, L2⦄ ⊢ T2 ➡ T. #G #L0 #V0 #T0 #IH #V1 #T1 #HT01 #T2 #HT02 #L1 #HL01 #L2 #HL02 -elim (IH … HT01 … HT02 … HL01 … HL02) // -L0 -V0 -T0 /3 width=3/ +elim (IH … HT01 … HT02 … HL01 … HL02) // -L0 -V0 -T0 /3 width=3 by cpr_tau, ex2_intro/ qed-. fact cpr_conf_lpr_tau_tau: @@ -174,7 +173,7 @@ fact cpr_conf_lpr_tau_tau: ∃∃T. ⦃G, L1⦄ ⊢ T1 ➡ T & ⦃G, L2⦄ ⊢ T2 ➡ T. #G #L0 #V0 #T0 #IH #T1 #HT01 #T2 #HT02 #L1 #HL01 #L2 #HL02 -elim (IH … HT01 … HT02 … HL01 … HL02) // -L0 -V0 -T0 /2 width=3/ +elim (IH … HT01 … HT02 … HL01 … HL02) // -L0 -V0 -T0 /2 width=3 by ex2_intro/ qed-. fact cpr_conf_lpr_flat_beta: @@ -191,11 +190,11 @@ fact cpr_conf_lpr_flat_beta: #a #G #L0 #V0 #W0 #T0 #IH #V1 #HV01 #X #H #V2 #HV02 #W2 #HW02 #T2 #HT02 #L1 #HL01 #L2 #HL02 elim (cpr_inv_abst1 … H) -H #W1 #T1 #HW01 #HT01 #H destruct -elim (IH … HV01 … HV02 … HL01 … HL02) -HV01 -HV02 /2 width=1/ #V #HV1 #HV2 -elim (IH … HW01 … HW02 … HL01 … HL02) /2 width=1/ #W #HW1 #HW2 -elim (IH … HT01 … HT02 (L1.ⓛW1) … (L2.ⓛW2)) /2 width=1/ -L0 -V0 -W0 -T0 #T #HT1 #HT2 -lapply (lsubr_cpr_trans … HT2 (L2.ⓓⓝW2.V2) ?) -HT2 /2 width=1/ -/4 width=5 by cpr_bind, cpr_flat, cpr_beta, ex2_intro/ (**) (* auto too slow without trace *) +elim (IH … HV01 … HV02 … HL01 … HL02) -HV01 -HV02 /2 width=1 by/ #V #HV1 #HV2 +elim (IH … HW01 … HW02 … HL01 … HL02) /2 width=1 by/ #W #HW1 #HW2 +elim (IH … HT01 … HT02 (L1.ⓛW1) … (L2.ⓛW2)) /2 width=1 by lpr_pair/ -L0 -V0 -W0 -T0 #T #HT1 #HT2 +lapply (lsubr_cpr_trans … HT2 (L2.ⓓⓝW2.V2) ?) -HT2 /2 width=1 by lsubr_abst/ (**) (* full auto not tried *) +/4 width=5 by cpr_bind, cpr_flat, cpr_beta, ex2_intro/ qed-. (* Basic-1: includes: @@ -216,18 +215,18 @@ fact cpr_conf_lpr_flat_theta: ∃∃T. ⦃G, L1⦄ ⊢ ⓐV1.T1 ➡ T & ⦃G, L2⦄ ⊢ ⓓ{a}W2.ⓐU2.T2 ➡ T. #a #G #L0 #V0 #W0 #T0 #IH #V1 #HV01 #X #H #V2 #HV02 #U2 #HVU2 #W2 #HW02 #T2 #HT02 #L1 #HL01 #L2 #HL02 -elim (IH … HV01 … HV02 … HL01 … HL02) -HV01 -HV02 /2 width=1/ #V #HV1 #HV2 +elim (IH … HV01 … HV02 … HL01 … HL02) -HV01 -HV02 /2 width=1 by/ #V #HV1 #HV2 elim (lift_total V 0 1) #U #HVU -lapply (cpr_lift … HV2 (L2.ⓓW2) … HVU2 … HVU) -HVU2 /2 width=1/ #HU2 +lapply (cpr_lift … HV2 (L2.ⓓW2) … HVU2 … HVU) -HVU2 /2 width=1 by ldrop_ldrop/ #HU2 elim (cpr_inv_abbr1 … H) -H * [ #W1 #T1 #HW01 #HT01 #H destruct - elim (IH … HW01 … HW02 … HL01 … HL02) /2 width=1/ - elim (IH … HT01 … HT02 (L1.ⓓW1) … (L2.ⓓW2)) /2 width=1/ -L0 -V0 -W0 -T0 - /4 width=7 by cpr_bind, cpr_flat, cpr_theta, ex2_intro/ (**) (* timeout=35 *) + elim (IH … HW01 … HW02 … HL01 … HL02) /2 width=1 by/ + elim (IH … HT01 … HT02 (L1.ⓓW1) … (L2.ⓓW2)) /2 width=1 by lpr_pair/ -L0 -V0 -W0 -T0 + /4 width=7 by cpr_bind, cpr_flat, cpr_theta, ex2_intro/ | #T1 #HT01 #HXT1 #H destruct - elim (IH … HT01 … HT02 (L1.ⓓW2) … (L2.ⓓW2)) /2 width=1/ -L0 -V0 -W0 -T0 #T #HT1 #HT2 - elim (cpr_inv_lift1 … HT1 L1 … HXT1) -HXT1 /2 width=1/ #Y #HYT #HXY - @(ex2_intro … (ⓐV.Y)) /2 width=1/ /3 width=5/ (**) (* auto /4 width=9/ is too slow *) + elim (IH … HT01 … HT02 (L1.ⓓW2) … (L2.ⓓW2)) /2 width=1 by lpr_pair/ -L0 -V0 -W0 -T0 #T #HT1 #HT2 + elim (cpr_inv_lift1 … HT1 L1 … HXT1) -HXT1 + /4 width=9 by cpr_flat, cpr_zeta, ldrop_ldrop, lift_flat, ex2_intro/ ] qed-. @@ -244,12 +243,12 @@ fact cpr_conf_lpr_beta_beta: ∃∃T. ⦃G, L1⦄ ⊢ ⓓ{a}ⓝW1.V1.T1 ➡ T & ⦃G, L2⦄ ⊢ ⓓ{a}ⓝW2.V2.T2 ➡ T. #a #G #L0 #V0 #W0 #T0 #IH #V1 #HV01 #W1 #HW01 #T1 #HT01 #V2 #HV02 #W2 #HW02 #T2 #HT02 #L1 #HL01 #L2 #HL02 -elim (IH … HV01 … HV02 … HL01 … HL02) -HV01 -HV02 /2 width=1/ #V #HV1 #HV2 +elim (IH … HV01 … HV02 … HL01 … HL02) -HV01 -HV02 /2 width=1 by/ #V #HV1 #HV2 elim (IH … HW01 … HW02 … HL01 … HL02) /2 width=1/ #W #HW1 #HW2 -elim (IH … HT01 … HT02 (L1.ⓛW1) … (L2.ⓛW2)) /2 width=1/ -L0 -V0 -W0 -T0 #T #HT1 #HT2 -lapply (lsubr_cpr_trans … HT1 (L1.ⓓⓝW1.V1) ?) -HT1 /2 width=1/ -lapply (lsubr_cpr_trans … HT2 (L2.ⓓⓝW2.V2) ?) -HT2 /2 width=1/ -/4 width=5 by cpr_bind, cpr_flat, ex2_intro/ +elim (IH … HT01 … HT02 (L1.ⓛW1) … (L2.ⓛW2)) /2 width=1 by lpr_pair/ -L0 -V0 -W0 -T0 #T #HT1 #HT2 +lapply (lsubr_cpr_trans … HT1 (L1.ⓓⓝW1.V1) ?) -HT1 /2 width=1 by lsubr_abst/ +lapply (lsubr_cpr_trans … HT2 (L2.ⓓⓝW2.V2) ?) -HT2 /2 width=1 by lsubr_abst/ +/4 width=5 by cpr_bind, cpr_flat, ex2_intro/ (**) (* full auto not tried *) qed-. (* Basic_1: was: pr0_upsilon_upsilon *) @@ -268,17 +267,17 @@ fact cpr_conf_lpr_theta_theta: ∃∃T. ⦃G, L1⦄ ⊢ ⓓ{a}W1.ⓐU1.T1 ➡ T & ⦃G, L2⦄ ⊢ ⓓ{a}W2.ⓐU2.T2 ➡ T. #a #G #L0 #V0 #W0 #T0 #IH #V1 #HV01 #U1 #HVU1 #W1 #HW01 #T1 #HT01 #V2 #HV02 #U2 #HVU2 #W2 #HW02 #T2 #HT02 #L1 #HL01 #L2 #HL02 -elim (IH … HV01 … HV02 … HL01 … HL02) -HV01 -HV02 /2 width=1/ #V #HV1 #HV2 -elim (IH … HW01 … HW02 … HL01 … HL02) /2 width=1/ -elim (IH … HT01 … HT02 (L1.ⓓW1) … (L2.ⓓW2)) /2 width=1/ -L0 -V0 -W0 -T0 +elim (IH … HV01 … HV02 … HL01 … HL02) -HV01 -HV02 /2 width=1 by/ #V #HV1 #HV2 +elim (IH … HW01 … HW02 … HL01 … HL02) /2 width=1 by/ +elim (IH … HT01 … HT02 (L1.ⓓW1) … (L2.ⓓW2)) /2 width=1 by lpr_pair/ -L0 -V0 -W0 -T0 elim (lift_total V 0 1) #U #HVU -lapply (cpr_lift … HV1 (L1.ⓓW1) … HVU1 … HVU) -HVU1 /2 width=1/ -lapply (cpr_lift … HV2 (L2.ⓓW2) … HVU2 … HVU) -HVU2 /2 width=1/ -/4 width=7 by cpr_bind, cpr_flat, ex2_intro/ (**) (* timeout 40 *) +lapply (cpr_lift … HV1 (L1.ⓓW1) … HVU1 … HVU) -HVU1 /2 width=1 by ldrop_ldrop/ +lapply (cpr_lift … HV2 (L2.ⓓW2) … HVU2 … HVU) -HVU2 /2 width=1 by ldrop_ldrop/ +/4 width=7 by cpr_bind, cpr_flat, ex2_intro/ (**) (* full auto not tried *) qed-. theorem cpr_conf_lpr: ∀G. lpx_sn_confluent (cpr G) (cpr G). -#G #L0 #T0 @(fqup_wf_ind … G L0 T0) -G -L0 -T0 #G #L #T #IH #G0 #L0 * [|*] +#G #L0 #T0 @(fqup_wf_ind_eq … G L0 T0) -G -L0 -T0 #G #L #T #IH #G0 #L0 * [| * ] [ #I0 #HG #HL #HT #T1 #H1 #T2 #H2 #L1 #HL01 #L2 #HL02 destruct elim (cpr_inv_atom1 … H1) -H1 elim (cpr_inv_atom1 … H2) -H2 @@ -342,13 +341,13 @@ theorem cpr_conf: ∀G,L. confluent … (cpr G L). lemma lpr_cpr_conf_dx: ∀G,L0,T0,T1. ⦃G, L0⦄ ⊢ T0 ➡ T1 → ∀L1. ⦃G, L0⦄ ⊢ ➡ L1 → ∃∃T. ⦃G, L1⦄ ⊢ T0 ➡ T & ⦃G, L1⦄ ⊢ T1 ➡ T. #G #L0 #T0 #T1 #HT01 #L1 #HL01 -elim (cpr_conf_lpr … HT01 T0 … HL01 … HL01) // -L0 /2 width=3/ +elim (cpr_conf_lpr … HT01 T0 … HL01 … HL01) // -L0 /2 width=3 by ex2_intro/ qed-. lemma lpr_cpr_conf_sn: ∀G,L0,T0,T1. ⦃G, L0⦄ ⊢ T0 ➡ T1 → ∀L1. ⦃G, L0⦄ ⊢ ➡ L1 → ∃∃T. ⦃G, L1⦄ ⊢ T0 ➡ T & ⦃G, L0⦄ ⊢ T1 ➡ T. #G #L0 #T0 #T1 #HT01 #L1 #HL01 -elim (cpr_conf_lpr … HT01 T0 … L0 … HL01) // -HT01 -HL01 /2 width=3/ +elim (cpr_conf_lpr … HT01 T0 … L0 … HL01) // -HT01 -HL01 /2 width=3 by ex2_intro/ qed-. (* Main properties **********************************************************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/fqu.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/fqu.ma index 1da166cf3..3b4690edd 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/fqu.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/fqu.ma @@ -14,6 +14,7 @@ include "basic_2/notation/relations/supterm_6.ma". include "basic_2/grammar/cl_weight.ma". +include "basic_2/grammar/bteq.ma". include "basic_2/relocation/ldrop.ma". (* SUPCLOSURE ***************************************************************) @@ -66,15 +67,24 @@ lemma fqu_fwd_length_lref1: ∀G1,G2,L1,L2,T2,i. ⦃G1, L1, #i⦄ ⊃ ⦃G2, L2, /2 width=7 by fqu_fwd_length_lref1_aux/ qed-. -lemma fqu_fwd_gen: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃ ⦃G2, L2, T2⦄ → - |G1| = |G2| → |L1| = |L2| → T1 = T2 → ⊥. +lemma fqu_fwd_bteq: ∀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 -[ #I #G #L #V #_ #H elim (plus_xSy_x_false … H) -| #I #G #L #V #T #_ #_ #H elim (discr_tpair_xy_x … H) -| #a #I #G #L #V #T #_ #_ #H elim (discr_tpair_xy_y … H) -| #I #G #L #V #T #_ #_ #H elim (discr_tpair_xy_y … H) -| #G #L #K #T #U #e #HLK #_ #_ #H +[ #I #G #L #V * #_ #H elim (plus_xSy_x_false … H) +| #I #G #L #V #T * #_ #_ #H elim (discr_tpair_xy_x … H) +| #a #I #G #L #V #T * #_ #_ #H elim (discr_tpair_xy_y … H) +| #I #G #L #V #T * #_ #_ #H elim (discr_tpair_xy_y … H) +| #G #L #K #T #U #e #HLK #_ * #_ #H lapply (ldrop_fwd_length_lt4 … HLK ?) // >H -L #H elim (lt_refl_false … H) ] qed-. + +(* Advanced eliminators *****************************************************) + +lemma fqu_wf_ind: ∀R:relation3 …. ( + ∀G1,L1,T1. (∀G2,L2,T2. ⦃G1, L1, T1⦄ ⊃ ⦃G2, L2, T2⦄ → R G2 L2 T2) → + R G1 L1 T1 + ) → ∀G1,L1,T1. R G1 L1 T1. +#R #HR @(f3_ind … fw) #n #IHn #G1 #L1 #T1 #H destruct /4 width=1 by fqu_fwd_fw/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/fqup.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/fqup.ma index c4c26fde2..82a8f5ed0 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/substitution/fqup.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/fqup.ma @@ -96,7 +96,14 @@ qed-. lemma fqup_wf_ind: ∀R:relation3 …. ( ∀G1,L1,T1. (∀G2,L2,T2. ⦃G1, L1, T1⦄ ⊃+ ⦃G2, L2, T2⦄ → R G2 L2 T2) → - ∀G2,L2,T2. G1 = G2 → L1 = L2 → T1 = T2 → R G2 L2 T2 + R G1 L1 T1 ) → ∀G1,L1,T1. R G1 L1 T1. +#R #HR @(f3_ind … fw) #n #IHn #G1 #L1 #T1 #H destruct /4 width=1 by fqup_fwd_fw/ +qed-. + +lemma fqup_wf_ind_eq: ∀R:relation3 …. ( + ∀G1,L1,T1. (∀G2,L2,T2. ⦃G1, L1, T1⦄ ⊃+ ⦃G2, L2, T2⦄ → R G2 L2 T2) → + ∀G2,L2,T2. G1 = G2 → L1 = L2 → T1 = T2 → R G2 L2 T2 + ) → ∀G1,L1,T1. R G1 L1 T1. #R #HR @(f3_ind … fw) #n #IHn #G1 #L1 #T1 #H destruct /4 width=7 by fqup_fwd_fw/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/fqus.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/fqus.ma index ef5af3100..f33a942a6 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/substitution/fqus.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/fqus.ma @@ -14,6 +14,7 @@ include "basic_2/notation/relations/suptermstar_6.ma". include "basic_2/relocation/fquq.ma". +include "basic_2/substitution/fqup.ma". (* STAR-ITERATED SUPCLOSURE *************************************************) @@ -48,11 +49,11 @@ lemma fquq_fqus: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃⸮ ⦃G2, L2, T2⦄ lemma fqus_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 by tri_step/ qed. +/2 width=5 by tri_step/ qed-. lemma fqus_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 by tri_TC_strap/ qed. +/2 width=5 by tri_TC_strap/ qed-. lemma fqus_ldrop: ∀G1,G2,K1,K2,T1,T2. ⦃G1, K1, T1⦄ ⊃* ⦃G2, K2, T2⦄ → ∀L1,U1,e. ⇩[0, e] L1 ≡ K1 → ⇧[0, e] T1 ≡ U1 → @@ -61,6 +62,11 @@ lemma fqus_ldrop: ∀G1,G2,K1,K2,T1,T2. ⦃G1, K1, T1⦄ ⊃* ⦃G2, K2, T2⦄ /3 width=5 by fqus_strap1, fquq_fqus, fquq_drop/ qed-. +lemma fqup_fqus: ∀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 @(fqup_ind … H) -G2 -L2 -T2 +/3 width=5 by fqus_strap1, fquq_fqus, fqu_fquq/ +qed. + (* Basic forward lemmas *****************************************************) lemma fqus_fwd_fw: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃* ⦃G2, L2, T2⦄ → ♯{G2, L2, T2} ≤ ♯{G1, L1, T1}. diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/fqus_alt.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/fqus_alt.ma new file mode 100644 index 000000000..0d8241111 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/fqus_alt.ma @@ -0,0 +1,61 @@ +(**************************************************************************) +(* ___ *) +(* ||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/relocation/fquq_alt.ma". +include "basic_2/substitution/fqus.ma". + +(* STAR-ITERATED SUPCLOSURE *************************************************) + +(* Advanced inversion lemmas ************************************************) + +lemma fqus_inv_gen: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃* ⦃G2, L2, T2⦄ → + ⦃G1, L1, T1⦄ ⊃+ ⦃G2, L2, T2⦄ ∨ (∧∧ G1 = G2 & L1 = L2 & T1 = T2). +#G1 #G2 #L1 #L2 #T1 #T2 #H @(fqus_ind … H) -G2 -L2 -T2 // +#G #G2 #L #L2 #T #T2 #_ #H2 * elim (fquq_inv_gen … H2) -H2 +[ /3 width=5 by fqup_strap1, or_introl/ +| * #HG #HL #HT destruct /2 width=1 by or_introl/ +| #H2 * #HG #HL #HT destruct /3 width=1 by fqu_fqup, or_introl/ +| * #H1G #H1L #H1T * #H2G #H2L #H2T destruct /2 width=1 by or_intror/ +] +qed-. + +(* Advanced properties ******************************************************) + +lemma fqus_strap1_fqu: ∀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⦄. +#G1 #G #G2 #L1 #L #L2 #T1 #T #T2 #H1 #H2 elim (fqus_inv_gen … H1) -H1 +[ /2 width=5 by fqup_strap1/ +| * #HG #HL #HT destruct /2 width=1 by fqu_fqup/ +] +qed-. + +lemma fqus_strap2_fqu: ∀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⦄. +#G1 #G #G2 #L1 #L #L2 #T1 #T #T2 #H1 #H2 elim (fqus_inv_gen … H2) -H2 +[ /2 width=5 by fqup_strap2/ +| * #HG #HL #HT destruct /2 width=1 by fqu_fqup/ +] +qed-. + +lemma fqus_fqup_trans: ∀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⦄. +#G1 #G #G2 #L1 #L #L2 #T1 #T #T2 #H1 #H2 @(fqup_ind … H2) -H2 -G2 -L2 -T2 +/2 width=5 by fqus_strap1_fqu, fqup_strap1/ +qed-. + +lemma fqup_fqus_trans: ∀G1,G,L1,L,T1,T. ⦃G1, L1, T1⦄ ⊃+ ⦃G, L, T⦄ → + ∀G2,L2,T2. ⦃G, L, T⦄ ⊃* ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ ⊃+ ⦃G2, L2, T2⦄. +#G1 #G #L1 #L #T1 #T #H1 @(fqup_ind_dx … H1) -H1 -G1 -L1 -T1 +/3 width=5 by fqus_strap2_fqu, fqup_strap2/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/fqus_fqus.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/fqus_fqus.ma index 295d45b17..de58e2d76 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/substitution/fqus_fqus.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/fqus_fqus.ma @@ -16,7 +16,7 @@ include "basic_2/substitution/fqus.ma". (* STAR-ITERATED SUPCLOSURE *************************************************) -(* Main properties **********************************************************) +(* Advaveded properties *****************************************************) theorem fqus_trans: tri_transitive … fqus. /2 width=5 by tri_TC_transitive/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl index e7a665c66..0b1ec4de4 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl +++ b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl @@ -79,13 +79,17 @@ table { [ "cpre ( ⦃?,?⦄ ⊢ ➡* 𝐍⦃?⦄ )" "cpre_cpre" * ] } ] - [ { "strongly normalizing computation" * } { + [ { "strongly normalizing \"big tree\" computation" * } { + [ "fsb ( ⦃?,?⦄ ⊢ ⦥[?,?] ? )" "fsb_alt ( ⦃?,?⦄ ⊢ ⦥⦥[?,?] ? )" "fsb_csx" * ] + } + ] + [ { "strongly normalizing extended computation" * } { [ "csx_vector ( ⦃?,?⦄ ⊢ ⬊*[?,?] ? )" "csx_tstc_vector" + "csx_aaa" * ] [ "csx ( ⦃?,?⦄ ⊢ ⬊*[?,?] ? )" "csx_alt ( ⦃?,?⦄ ⊢ ⬊⬊*[?,?] ? )" "csx_lift" + "csx_lpx" * ] } ] [ { "\"big tree\" parallel computation" * } { - [ "fpbg ( ⦃?,?,?⦄ >[?,?] ⦃?,?,?⦄ )" "fpbg_lift" + "fpbg_fpbg" * ] + [ "fpbg ( ⦃?,?,?⦄ >[?,?] ⦃?,?,?⦄ )" "fpbg_alt" "fpbg_lift" + "fpbg_fpbg" * ] [ "fpbs ( ⦃?,?,?⦄ ≥[?,?] ⦃?,?,?⦄ )" "fpbs_alt ( ⦃?,?,?⦄ ≥≥[?,?] ⦃?,?,?⦄ )" "fpbs_lift" + "fpbs_fpbs" * ] } ] @@ -203,7 +207,7 @@ table { } ] [ { "iterated structural successor for closures" * } { - [ "fqus ( ⦃?,?,?⦄ ⊃* ⦃?,?,?⦄ )" "fqus_fqus" * ] + [ "fqus ( ⦃?,?,?⦄ ⊃* ⦃?,?,?⦄ )" "fqus_alt" "fqus_fqus" * ] [ "fqup ( ⦃?,?,?⦄ ⊃+ ⦃?,?,?⦄ )" "fqup_fqup" * ] } ] @@ -254,7 +258,7 @@ table { } ] [ { "closures" * } { - [ "bteq ( ⦃?,?,?⦄ ⪴ ⦃?,?,?⦄ )" "bteq_bteq" * ] +(* [ "bteq ( ⦃?,?,?⦄ ⪴ ⦃?,?,?⦄ )" "bteq_bteq" * ] *) [ "cl_shift ( ? @@ ? )" "cl_weight ( ♯{?,?,?} )" * ] } ]