From 2a91f2b3a85bc0e89c942823b741cf243db5875d Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Sun, 3 Nov 2013 12:04:22 +0000 Subject: [PATCH] second and third commutation property on lazy equivalence for local environments proved (lleq_cpx_trans, lleq_lpx_trans) --- .../lambdadelta/apps_2/functional/rtm_step.ma | 22 +++--- .../lambdadelta/basic_2/computation/fpns.ma | 39 ++++++++++ .../basic_2/computation/fpns_fpns.ma | 27 +++++++ .../etc/fpn/{predsn_8.etc => btpredsn_8.etc} | 4 +- .../lambdadelta/basic_2/etc/fpn/fpn.etc | 26 +++---- .../lambdadelta/basic_2/etc/fpn/fpn_fpn.etc | 52 +++++++++++++ .../lambdadelta/basic_2/etc/fpn/fpns.etc | 60 +++++++-------- .../lambdadelta/basic_2/etc/fpn/fpns_fpns.etc | 74 +++++++++++++++++++ .../lazyeq_6.ma => etc/fpn/lazyeq_6.etc} | 0 .../contribs/lambdadelta/basic_2/names.txt | 7 +- .../relations/btpredsnstar_8.ma} | 4 +- .../lambdadelta/basic_2/reduction/cpx_cpx.ma | 42 +++++++++++ .../lambdadelta/basic_2/reduction/lpx_lpx.ma | 69 +++++++++++++++++ .../lambdadelta/basic_2/web/basic_2_src.tbl | 28 ++++--- 14 files changed, 379 insertions(+), 75 deletions(-) create mode 100644 matita/matita/contribs/lambdadelta/basic_2/computation/fpns.ma create mode 100644 matita/matita/contribs/lambdadelta/basic_2/computation/fpns_fpns.ma rename matita/matita/contribs/lambdadelta/basic_2/etc/fpn/{predsn_8.etc => btpredsn_8.etc} (87%) create mode 100644 matita/matita/contribs/lambdadelta/basic_2/etc/fpn/fpn_fpn.etc create mode 100644 matita/matita/contribs/lambdadelta/basic_2/etc/fpn/fpns_fpns.etc rename matita/matita/contribs/lambdadelta/basic_2/{notation/relations/lazyeq_6.ma => etc/fpn/lazyeq_6.etc} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{etc/fpn/predsnstar_8.etc => notation/relations/btpredsnstar_8.ma} (86%) create mode 100644 matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_cpx.ma create mode 100644 matita/matita/contribs/lambdadelta/basic_2/reduction/lpx_lpx.ma diff --git a/matita/matita/contribs/lambdadelta/apps_2/functional/rtm_step.ma b/matita/matita/contribs/lambdadelta/apps_2/functional/rtm_step.ma index ed16d5091..40f2eddc2 100644 --- a/matita/matita/contribs/lambdadelta/apps_2/functional/rtm_step.ma +++ b/matita/matita/contribs/lambdadelta/apps_2/functional/rtm_step.ma @@ -18,15 +18,15 @@ include "apps_2/functional/rtm.ma". (* transitions *) inductive rtm_step: relation rtm ≝ -| rtm_ldrop : ∀G,u,E,I,t,F,V,S,i. - rtm_step (mk_rtm G u (E. ④{I} {t, F, V}) S (#(i + 1))) +| rtm_ldrop : ∀G,u,E,I,t,D,V,S,i. + rtm_step (mk_rtm G u (E. ④{I} {t, D, V}) S (#(i + 1))) (mk_rtm G u E S (#i)) -| rtm_ldelta: ∀G,u,E,t,F,V,S. - rtm_step (mk_rtm G u (E. ④{Abbr} {t, F, V}) S (#0)) - (mk_rtm G u F S V) -| rtm_ltype : ∀G,u,E,t,F,V,S. - rtm_step (mk_rtm G u (E. ④{Abst} {t, F, V}) S (#0)) - (mk_rtm G u F S V) +| rtm_ldelta: ∀G,u,E,t,D,V,S. + rtm_step (mk_rtm G u (E. ④{Abbr} {t, D, V}) S (#0)) + (mk_rtm G u D S V) +| rtm_ltype : ∀G,u,E,t,D,V,S. + rtm_step (mk_rtm G u (E. ④{Abst} {t, D, V}) S (#0)) + (mk_rtm G u D S V) | rtm_gdrop : ∀G,I,V,u,E,S,p. p < |G| → rtm_step (mk_rtm (G. ⓑ{I} V) u E S (§p)) (mk_rtm G u E S (§p)) @@ -42,9 +42,9 @@ inductive rtm_step: relation rtm ≝ | rtm_appl : ∀G,u,E,S,V,T. rtm_step (mk_rtm G u E S (ⓐV. T)) (mk_rtm G u E ({E, V} @ S) T) -| rtm_beta : ∀G,u,E,F,V,S,W,T. - rtm_step (mk_rtm G u E ({F, V} @ S) (+ⓛW. T)) - (mk_rtm G u (E. ④{Abbr} {u, F, V}) S T) +| rtm_beta : ∀G,u,E,D,V,S,W,T. + rtm_step (mk_rtm G u E ({D, V} @ S) (+ⓛW. T)) + (mk_rtm G u (E. ④{Abbr} {u, D, V}) S T) | rtm_push : ∀G,u,E,W,T. rtm_step (mk_rtm G u E ⟠ (+ⓛW. T)) (mk_rtm G (u + 1) (E. ④{Abst} {u, E, W}) ⟠ T) 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..3fe57b92a --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/fpns.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/btpredsnstar_8.ma". +include "basic_2/relocation/lleq.ma". +include "basic_2/computation/lpxs.ma". + +(* PARALLEL COMPUTATION FOR "BIG TREE" NORMAL FORMS *************************) + +inductive fpns (h) (g) (G) (L1) (T): relation3 genv lenv term ≝ +| fpns_intro: ∀L2. ⦃G, L1⦄ ⊢ ➡*[h, g] L2 → L1 ⋕[T] L2 → fpns h g G L1 T G L2 T +. + +interpretation + "computation for 'big tree' normal forms (closure)" + 'BTPRedSnStar 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 fpns_intro/ qed. + +(* Basic inversion lemmas ***************************************************) + +lemma fpns_inv_gen: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊢ ⋕➡*[h, g] ⦃G2, L2, T2⦄ → + ∧∧ G1 = G2 & ⦃G1, L1⦄ ⊢ ➡*[h, g] L2 & L1 ⋕[T1] L2 & T1 = T2. +#h #g #G1 #G2 #L1 #L2 #T1 #T2 * -G2 -L2 -T2 /2 width=1 by and4_intro/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/fpns_fpns.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fpns_fpns.ma new file mode 100644 index 000000000..deaa7a967 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/fpns_fpns.ma @@ -0,0 +1,27 @@ +(**************************************************************************) +(* ___ *) +(* ||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/lleq_lleq.ma". +include "basic_2/computation/lpxs_lpxs.ma". +include "basic_2/computation/fpns.ma". + +(* PARALLEL COMPUTATION FOR "BIG TREE" NORMAL FORMS *************************) + +(* Main properties **********************************************************) + +theorem fpns_trans: ∀h,g. tri_transitive … (fpns h g). +#h #g #G1 #G #L1 #L #T1 #T * -G -L -T +#L #HL1 #HT1 #G2 #L2 #T2 * -G2 -L2 -T2 +/3 width=3 by lpxs_trans, lleq_trans, fpns_intro/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/fpn/predsn_8.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/fpn/btpredsn_8.etc similarity index 87% rename from matita/matita/contribs/lambdadelta/basic_2/etc/fpn/predsn_8.etc rename to matita/matita/contribs/lambdadelta/basic_2/etc/fpn/btpredsn_8.etc index dc3b08203..0350d1495 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/etc/fpn/predsn_8.etc +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/fpn/btpredsn_8.etc @@ -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 h , break term 46 g ] 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 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 }. + for @{ 'BTPRedSn $h $g $G1 $L1 $T1 $G2 $L2 $T2 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/fpn/fpn.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/fpn/fpn.etc index f33adbde9..406e6eb8e 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/etc/fpn/fpn.etc +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/fpn/fpn.etc @@ -12,28 +12,28 @@ (* *) (**************************************************************************) -include "basic_2/notation/relations/predsn_8.ma". -include "basic_2/grammar/bteq.ma". +include "basic_2/notation/relations/btpredsn_8.ma". +include "basic_2/relocation/lleq.ma". include "basic_2/reduction/lpx.ma". -(* ADJACENT "BIG TREE" NORMAL FORMS *****************************************) +(* REDUCTION FOR "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. +inductive fpn (h) (g) (G) (L1) (T): relation3 genv lenv term ≝ +| fpn_intro: ∀L2. ⦃G, L1⦄ ⊢ ➡[h, g] L2 → L1 ⋕[T] L2 → fpn h g G L1 T G L2 T +. 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). + "reduction for 'big tree' normal forms (closure)" + 'BTPRedSn 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. +/2 width=1 by fpn_intro/ qed. -(* Basic forward lemmas *****************************************************) +(* Basic inversion 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/ +lemma fpn_inv_gen: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊢ ⋕➡[h, g] ⦃G2, L2, T2⦄ → + ∧∧ G1 = G2 & ⦃G1, L1⦄ ⊢ ➡[h, g] L2 & L1 ⋕[T1] L2 & T1 = T2. +#h #g #G1 #G2 #L1 #L2 #T1 #T2 * -G2 -L2 -T2 /2 width=1 by and4_intro/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/fpn/fpn_fpn.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/fpn/fpn_fpn.etc new file mode 100644 index 000000000..adda4b538 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/fpn/fpn_fpn.etc @@ -0,0 +1,52 @@ +(**************************************************************************) +(* ___ *) +(* ||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/lpx_lpx.ma". +include "basic_2/reduction/fpn.ma". + +(* REDUCTION FOR "BIG TREE" NORMAL FORMS ************************************) + +(* Advanced properties ******************************************************) + +lemma fpn_fqu_trans: ∀h,g,F1,G1,K1,L1,V1,T1. ⦃F1, K1, V1⦄ ⊢ ⋕➡[h, g] ⦃G1, L1, T1⦄ → + ∀G2,L2,T2. ⦃G1, L1, T1⦄ ⊃ ⦃G2, L2, T2⦄ → + ∃∃F2,K2,V2. ⦃F1, K1, V1⦄ ⊃ ⦃F2, K2, V2⦄ & ⦃F2, K2, V2⦄ ⊢ ⋕➡[h, g] ⦃G2, L2, T2⦄. +#h #g #F1 #G1 #K1 #L1 #V1 #T1 * -G1 -L1 -T1 +#L1 #HKL1 #HV1 #G2 #L2 #T2 #H12 elim (lpx_lleq_fqu_trans … H12 … HKL1 HV1) -L1 +/3 width=5 by fpn_intro, ex2_3_intro/ +qed-. + +lemma fpn_fquq_trans: ∀h,g,F1,G1,K1,L1,V1,T1. ⦃F1, K1, V1⦄ ⊢ ⋕➡[h, g] ⦃G1, L1, T1⦄ → + ∀G2,L2,T2. ⦃G1, L1, T1⦄ ⊃⸮ ⦃G2, L2, T2⦄ → + ∃∃F2,K2,V2. ⦃F1, K1, V1⦄ ⊃⸮ ⦃F2, K2, V2⦄ & ⦃F2, K2, V2⦄ ⊢ ⋕➡[h, g] ⦃G2, L2, T2⦄. +#h #g #F1 #G1 #K1 #L1 #V1 #T1 * -G1 -L1 -T1 +#L1 #HKL1 #HV1 #G2 #L2 #T2 #H12 elim (lpx_lleq_fquq_trans … H12 … HKL1 HV1) -L1 +/3 width=5 by fpn_intro, ex2_3_intro/ +qed-. + +lemma fpn_fqup_trans: ∀h,g,F1,G1,K1,L1,V1,T1. ⦃F1, K1, V1⦄ ⊢ ⋕➡[h, g] ⦃G1, L1, T1⦄ → + ∀G2,L2,T2. ⦃G1, L1, T1⦄ ⊃+ ⦃G2, L2, T2⦄ → + ∃∃F2,K2,V2. ⦃F1, K1, V1⦄ ⊃+ ⦃F2, K2, V2⦄ & ⦃F2, K2, V2⦄ ⊢ ⋕➡[h, g] ⦃G2, L2, T2⦄. +#h #g #F1 #G1 #K1 #L1 #V1 #T1 * -G1 -L1 -T1 +#L1 #HKL1 #HV1 #G2 #L2 #T2 #H12 elim (lpx_lleq_fqup_trans … H12 … HKL1 HV1) -L1 +/3 width=5 by fpn_intro, ex2_3_intro/ +qed-. + +lemma fpn_fqus_trans: ∀h,g,F1,G1,K1,L1,V1,T1. ⦃F1, K1, V1⦄ ⊢ ⋕➡[h, g] ⦃G1, L1, T1⦄ → + ∀G2,L2,T2. ⦃G1, L1, T1⦄ ⊃* ⦃G2, L2, T2⦄ → + ∃∃F2,K2,V2. ⦃F1, K1, V1⦄ ⊃* ⦃F2, K2, V2⦄ & ⦃F2, K2, V2⦄ ⊢ ⋕➡[h, g] ⦃G2, L2, T2⦄. +#h #g #F1 #G1 #K1 #L1 #V1 #T1 * -G1 -L1 -T1 +#L1 #HKL1 #HV1 #G2 #L2 #T2 #H12 elim (lpx_lleq_fqus_trans … H12 … HKL1 HV1) -L1 +/3 width=5 by fpn_intro, ex2_3_intro/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/fpn/fpns.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/fpn/fpns.etc index 29b81d043..0a208fedf 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/etc/fpn/fpns.etc +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/fpn/fpns.etc @@ -12,45 +12,47 @@ (* *) (**************************************************************************) -include "basic_2/notation/relations/predsnstar_8.ma". +include "basic_2/notation/relations/btpredsnstar_8.ma". include "basic_2/reduction/fpn.ma". -include "basic_2/computation/lpxs.ma". -(* ORDERED "BIG TREE" NORMAL FORMS ******************************************) +(* COMPUTATION FOR "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. + λh,g. tri_TC … (fpn h g). 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). + "computation for 'big tree' normal forms (closure)" + 'BTPRedSnStar 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. +(* Basic eliminators ********************************************************) -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/ +lemma fpns_ind: ∀h,g,G1,L1,T1. ∀R:relation3 …. R G1 L1 T1 → + (∀G,G2,L,L2,T,T2. ⦃G1, L1, T1⦄ ⊢ ⋕➡*[h, g] ⦃G, L, T⦄ → ⦃G, L, T⦄ ⊢ ⋕➡[h, g] ⦃G2, L2, T2⦄ → R G L T → R G2 L2 T2) → + ∀G2,L2,T2. ⦃G1, L1, T1⦄ ⊢ ⋕➡*[h, g] ⦃G2, L2, T2⦄ → R G2 L2 T2. +#h #g #G1 #L1 #T1 #R #IH1 #IH2 #G2 #L2 #T2 #H +lapply (tri_TC_star_ind … IH1 IH2 G2 L2 T2 H) // 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/ +lemma fpns_ind_dx: ∀h,g,G2,L2,T2. ∀R:relation3 …. R G2 L2 T2 → + (∀G1,G,L1,L,T1,T. ⦃G1, L1, T1⦄ ⊢ ⋕➡[h, g] ⦃G, L, T⦄ → ⦃G, L, T⦄ ⊢ ⋕➡*[h, g] ⦃G2, L2, T2⦄ → R G L T → R G1 L1 T1) → + ∀G1,L1,T1. ⦃G1, L1, T1⦄ ⊢ ⋕➡*[h, g] ⦃G2, L2, T2⦄ → R G1 L1 T1. +#h #g #G2 #L2 #T2 #R #IH1 #IH2 #G1 #L1 #T1 #H +@(tri_TC_star_ind_dx … IH1 IH2 G1 L1 T1 H) // qed-. -(* Basic forward lemmas *****************************************************) +(* Basic_properties *********************************************************) + +lemma fpns_refl: ∀h,g. tri_reflexive … (fpns h g). +/2 width=1 by tri_inj/ qed. -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-. +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⦄. +/2 width=1 by tri_inj/ 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⦄. +/2 width=5 by tri_step/ 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⦄. +/2 width=5 by tri_TC_strap/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/fpn/fpns_fpns.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/fpn/fpns_fpns.etc new file mode 100644 index 000000000..5aaea6a9e --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/fpn/fpns_fpns.etc @@ -0,0 +1,74 @@ +(**************************************************************************) +(* ___ *) +(* ||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/lleq_lleq.ma". +include "basic_2/computation/lpxs.ma". +include "basic_2/computation/fpns.ma". + +(* COMPUTATION FOR "BIG TREE" NORMAL FORMS **********************************) + +(* Advanced inversion lemmas ************************************************) + +lemma fpns_inv_gen: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊢ ⋕➡*[h, g] ⦃G2, L2, T2⦄ → + ∧∧ G1 = G2 & ⦃G1, L1⦄ ⊢ ➡*[h, g] L2 & L1 ⋕[T1] L2 & T1 = T2. +#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H @(fpns_ind … H) -G2 -L2 -T2 /2 width=1 by and4_intro/ +#G #G2 #L #L2 #T #T2 #_ #H2 * #HG #HL1 #HT1 #HT destruct +elim (fpn_inv_gen … H2) -H2 #HG #HL2 #HT #HT2 destruct +/3 width=3 by lpxs_strap1, lleq_trans, and4_intro/ +qed-. + +(* Advanced properties ******************************************************) + +lemma lpxs_lleq_fpns: ∀h,g,G,L1,L2,T. ⦃G, L1⦄ ⊢ ➡*[h, g] L2 → L1 ⋕[T] L2 → + ⦃G, L1, T⦄ ⊢ ⋕➡*[h, g] ⦃G, L2, T⦄. +#h #g #G #L1 #L2 #T #H @(lpxs_ind … H) -L2 // +#L #L2 #HL1 #HL2 #IHL1 #HL12 elim (lleq_dec T L1 L) #HT +[ -HL1 @fpns_strap1 [4: @IHL1 // |1,2,3: skip ] + /3 width=3 by fpn_intro, lleq_canc_sn/ +| -IHL1 + +(* Main properties **********************************************************) + +theorem fpns_trans: tri_transitive … fqus. +/2 width=5 by tri_TC_transitive/ qed-. + + +(* +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/notation/relations/lazyeq_6.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/fpn/lazyeq_6.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazyeq_6.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc/fpn/lazyeq_6.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/names.txt b/matita/matita/contribs/lambdadelta/basic_2/names.txt index 87d49091b..31e1d7c40 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/names.txt +++ b/matita/matita/contribs/lambdadelta/basic_2/names.txt @@ -1,9 +1,9 @@ NAMING CONVENTIONS FOR METAVARIABLES A,B : arity -C,D : candidate of reducibility -E,F : RTM environment -G : global environment +C : candidate of reducibility +D,E : RTM environment +F,G : global environment H : reserved: transient premise IH : reserved: inductive premise I,J : item @@ -73,6 +73,7 @@ b: "big tree" reduction c: conversion d: decomposed extended reduction e: decomposed extended conversion +n: reduction for "big tree" normal forms q: restricted reduction r: reduction s: substitution diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/fpn/predsnstar_8.etc b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/btpredsnstar_8.ma similarity index 86% rename from matita/matita/contribs/lambdadelta/basic_2/etc/fpn/predsnstar_8.etc rename to matita/matita/contribs/lambdadelta/basic_2/notation/relations/btpredsnstar_8.ma index f396ff17d..629d79828 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/etc/fpn/predsnstar_8.etc +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/btpredsnstar_8.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 h , break term 46 g ] 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 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 }. + for @{ 'BTPRedSnStar $h $g $G1 $L1 $T1 $G2 $L2 $T2 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_cpx.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_cpx.ma new file mode 100644 index 000000000..7cbd2520e --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_cpx.ma @@ -0,0 +1,42 @@ +(**************************************************************************) +(* ___ *) +(* ||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/lleq_lleq.ma". +include "basic_2/reduction/cpx.ma". + +(* CONTEXT-SENSITIVE EXTENDED PARALLEL REDUCTION FOR TERMS ******************) + +(* Advanced properties ******************************************************) + +lemma lleq_cpx_trans: ∀h,g,G,L2,T1,T2. ⦃G, L2⦄ ⊢ T1 ➡[h, g] T2 → + ∀L1. L1 ⋕[T1] L2 → ⦃G, L1⦄ ⊢ T1 ➡[h, g] T2. +#h #g #G #L2 #T1 #T2 #H elim H -G -L2 -T1 -T2 /2 width=2 by cpx_sort/ +[ #I #G #L2 #K2 #V1 #V2 #W2 #i #HLK2 #_ #HVW2 #IHV12 #L1 #H elim (lleq_inv_lref_dx … H … HLK2) -L2 + /3 width=7 by cpx_delta/ +| #a #I #G #L2 #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #L1 #H elim (lleq_inv_bind … H) -H + /3 width=1 by cpx_bind/ +| #I #G #L2 #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #L1 #H elim (lleq_inv_flat … H) -H + /3 width=1 by cpx_flat/ +| #G #L2 #V2 #T1 #T #T2 #_ #HT2 #IHT1 #L1 #H elim (lleq_inv_bind … H) -H + /3 width=3 by cpx_zeta/ +| #G #L2 #W1 #T1 #T2 #_ #IHT12 #L1 #H elim (lleq_inv_flat … H) -H + /3 width=1 by cpx_tau/ +| #G #L2 #W1 #W2 #T1 #_ #IHW12 #L1 #H elim (lleq_inv_flat … H) -H + /3 width=1 by cpx_ti/ +| #a #G #L1 #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #IHV12 #IHW12 #IHT12 #L1 #H elim (lleq_inv_flat … H) -H + #HV1 #H elim (lleq_inv_bind … H) -H /3 width=1 by cpx_beta/ +| #a #G #L1 #V1 #V #V2 #W1 #W2 #T1 #T2 #_ #HV2 #_ #_ #IHV1 #IHW12 #IHT12 #L1 #H elim (lleq_inv_flat … H) -H + #HV1 #H elim (lleq_inv_bind … H) -H /3 width=3 by cpx_theta/ +] +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/lpx_lpx.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/lpx_lpx.ma new file mode 100644 index 000000000..a2ffaccee --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/lpx_lpx.ma @@ -0,0 +1,69 @@ +include "basic_2/relocation/lleq_lleq.ma". +include "basic_2/reduction/lpx_ldrop.ma". + +(* SN EXTENDED PARALLEL REDUCTION FOR LOCAL ENVIRONMENTS ********************) + +(* Advanced properties ******************************************************) + +lemma lpx_lleq_fqu_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃ ⦃G2, L2, T2⦄ → + ∀K1. ⦃G1, K1⦄ ⊢ ➡[h, g] L1 → K1 ⋕[T1] L1 → + ∃∃K2. ⦃G1, K1, T1⦄ ⊃ ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡[h, g] L2 & K2 ⋕[T2] L2. +#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2 +[ #I #G1 #L1 #V1 #X #H1 #H2 elim (lpx_inv_pair2 … H1) -H1 + #K0 #V0 #H1KL1 #_ #H destruct + elim (lleq_inv_lref_dx … H2 I L1 V1) -H2 // + #K1 #H #H2KL1 lapply (ldrop_inv_O2 … H) -H #H destruct + /2 width=4 by fqu_lref_O, ex3_intro/ +| * [ #a ] #I #G1 #L1 #V1 #T1 #K1 #HLK1 #H + [ elim (lleq_inv_bind … H) + | elim (lleq_inv_flat … H) + ] -H /2 width=4 by fqu_pair_sn, ex3_intro/ +| #a #I #G1 #L1 #V1 #T1 #K1 #HLK1 #H elim (lleq_inv_bind … H) -H + /3 width=4 by lpx_pair, fqu_bind_dx, ex3_intro/ +| #I #G1 #L1 #V1 #T1 #K1 #HLK1 #H elim (lleq_inv_flat … H) -H + /2 width=4 by fqu_flat_dx, ex3_intro/ +| #G1 #L1 #L #T1 #U1 #e #HL1 #HTU1 #K1 #H1KL1 #H2KL1 + elim (ldrop_O1_le (e+1) K1) + [ #K #HK1 lapply (lleq_inv_lift … H2KL1 … HK1 HL1 … HTU1) -H2KL1 + #H2KL elim (lpx_ldrop_trans_O1 … H1KL1 … HL1) -L1 + #K0 #HK10 #H1KL lapply (ldrop_mono … HK10 … HK1) -HK10 #H destruct + /3 width=4 by fqu_drop, ex3_intro/ + | lapply (ldrop_fwd_length_le2 … HL1) -L -T1 -g + lapply (lleq_fwd_length … H2KL1) // + ] +] +qed-. + +lemma lpx_lleq_fquq_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃⸮ ⦃G2, L2, T2⦄ → + ∀K1. ⦃G1, K1⦄ ⊢ ➡[h, g] L1 → K1 ⋕[T1] L1 → + ∃∃K2. ⦃G1, K1, T1⦄ ⊃⸮ ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡[h, g] L2 & K2 ⋕[T2] L2. +#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H #K1 #H1KL1 #H2KL1 +elim (fquq_inv_gen … H) -H +[ #H elim (lpx_lleq_fqu_trans … H … H1KL1 H2KL1) -L1 + /3 width=4 by fqu_fquq, ex3_intro/ +| * #HG #HL #HT destruct /2 width=4 by ex3_intro/ +] +qed-. + +lemma lpx_lleq_fqup_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃+ ⦃G2, L2, T2⦄ → + ∀K1. ⦃G1, K1⦄ ⊢ ➡[h, g] L1 → K1 ⋕[T1] L1 → + ∃∃K2. ⦃G1, K1, T1⦄ ⊃+ ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡[h, g] L2 & K2 ⋕[T2] L2. +#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H @(fqup_ind … H) -G2 -L2 -T2 +[ #G2 #L2 #T2 #H #K1 #H1KL1 #H2KL1 elim (lpx_lleq_fqu_trans … H … H1KL1 H2KL1) -L1 + /3 width=4 by fqu_fqup, ex3_intro/ +| #G #G2 #L #L2 #T #T2 #_ #HT2 #IHT1 #K1 #H1KL1 #H2KL1 elim (IHT1 … H2KL1) // -L1 + #K #HT1 #H1KL #H2KL elim (lpx_lleq_fqu_trans … HT2 … H1KL H2KL) -L + /3 width=5 by fqup_strap1, ex3_intro/ +] +qed-. + +lemma lpx_lleq_fqus_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃* ⦃G2, L2, T2⦄ → + ∀K1. ⦃G1, K1⦄ ⊢ ➡[h, g] L1 → K1 ⋕[T1] L1 → + ∃∃K2. ⦃G1, K1, T1⦄ ⊃* ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡[h, g] L2 & K2 ⋕[T2] L2. +#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H #K1 #H1KL1 #H2KL1 +elim (fqus_inv_gen … H) -H +[ #H elim (lpx_lleq_fqup_trans … H … H1KL1 H2KL1) -L1 + /3 width=4 by fqup_fqus, ex3_intro/ +| * #HG #HL #HT destruct /2 width=4 by ex3_intro/ +] +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 775743fd2..5e21f5395 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 @@ -82,15 +82,19 @@ table { [ { "strongly normalizing \"big tree\" computation" * } { [ "fsb ( ⦃?,?⦄ ⊢ ⦥[?,?] ? )" "fsb_alt ( ⦃?,?⦄ ⊢ ⦥⦥[?,?] ? )" "fsb_fleq" + "fsb_csx" * ] } - ] - [ { "strongly normalizing extended computation" * } { + ] + [ { "strongly normalizing extended computation" * } { [ "csx_vector ( ⦃?,?⦄ ⊢ ⬊*[?,?] ? )" "csx_tstc_vector" + "csx_aaa" * ] [ "csx ( ⦃?,?⦄ ⊢ ⬊*[?,?] ? )" "csx_alt ( ⦃?,?⦄ ⊢ ⬊⬊*[?,?] ? )" "csx_lift" + "csx_lpx" * ] } ] + [ { "parallel computation for \"big tree\" normal forms" * } { + [ "fpns ( ⦃?,?,?⦄ ⊢ ⋕➡*[?,?] ⦃?,?,?⦄ )" "fpns_fpns" * ] + } + ] [ { "\"big tree\" parallel computation" * } { - [ "fpbr ( ⦃?,?,?⦄ ⊃≥[?,?] ⦃?,?,?⦄ )" "fpbr_fpbr" * ] - [ "fpbg ( ⦃?,?,?⦄ >[?,?] ⦃?,?,?⦄ )" "fpbg_lift" + "fpbg_fpbg" * ] + [ "fpbr ( ⦃?,?,?⦄ ⊃≥[?,?] ⦃?,?,?⦄ )" "fpbr_fpbr" * ] + [ "fpbg ( ⦃?,?,?⦄ >[?,?] ⦃?,?,?⦄ )" "fpbg_lift" + "fpbg_fpbg" * ] [ "fpbs ( ⦃?,?,?⦄ ≥[?,?] ⦃?,?,?⦄ )" "fpbs_alt ( ⦃?,?,?⦄ ≥≥[?,?] ⦃?,?,?⦄ )" "fpbs_lift" + "fpbs_fleq" + "fpbs_fpbs" * ] } ] @@ -130,8 +134,8 @@ table { } ] [ { "context-sensitive extended reduction" * } { - [ "lpx ( ⦃?,?⦄ ⊢ ➡[?,?] ? )" "lpx_ldrop" + "lpx_aaa" * ] - [ "cpx ( ⦃?,?⦄ ⊢ ? ➡[?,?] ? )" "cpx_lift" + "cpx_cix" * ] + [ "lpx ( ⦃?,?⦄ ⊢ ➡[?,?] ? )" "lpx_ldrop" + "lpx_aaa" + "lpx_lpx" * ] + [ "cpx ( ⦃?,?⦄ ⊢ ? ➡[?,?] ? )" "cpx_lift" + "cpx_cix" + "cpx_cpx" * ] } ] [ { "context-sensitive extended irreducible forms" * } { @@ -231,20 +235,14 @@ table { [ { "relocation" * } { [ { "structural successor for closures" * } { [ "fquq ( ⦃?,?,?⦄ ⊃⸮ ⦃?,?,?⦄ )" "fquq_alt ( ⦃?,?,?⦄ ⊃⊃⸮ ⦃?,?,?⦄ )" "fquq_fquq" * ] - [ "fqu ( ⦃?,?,?⦄ ⊃ ⦃?,?,?⦄ )" "fqu_fqu" * ] - } - ] -(* - [ { "lazy equivalence for closures" * } { - [ "fleq ( ⦃?,?,?⦄ ⋕ ⦃?,?,?⦄ )" "fleq_fleq" * ] + [ "fqu ( ⦃?,?,?⦄ ⊃ ⦃?,?,?⦄ )" "fqu_fqu" * ] } ] -*) - [ { "lazy equivalence for local environments" * } { + [ { "lazy equivalence for local environments" * } { [ "lleq ( ? ⋕[?] ? )" "lleq_fleq" * ] } ] - [ { "global env. slicing" * } { + [ { "global env. slicing" * } { [ "gdrop ( ⇩[?] ? ≡ ? )" "gdrop_gdrop" * ] } ] -- 2.39.2