From: Ferruccio Guidi Date: Wed, 5 Jun 2013 21:54:08 +0000 (+0000) Subject: some work on extended reduction ... X-Git-Tag: make_still_working~1136 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=143c97a8fe657eb7b041dec2747b0e67b5899762;p=helm.git some work on extended reduction ... --- diff --git a/matita/matita/contribs/lambdadelta/basic_2/names.txt b/matita/matita/contribs/lambdadelta/basic_2/names.txt index 1e1fc78cc..003b33747 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/names.txt +++ b/matita/matita/contribs/lambdadelta/basic_2/names.txt @@ -51,9 +51,10 @@ NAMING CONVENTIONS FOR TRANSFORMATIONS - first letter +c: contex-sensitive for terms f: context-freee for closures -l: sn contex-sensitive for terms -r: dx contex-sensitive for terms +l: sn contex-sensitive for local environments +r: dx contex-sensitive for local environments t: context-free for terms -second letter @@ -73,4 +74,5 @@ x: extended reduction - forth letter (if present) p: non-reflexive transitive closure +q: reflexive closure s: reflexive transitive closure diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation.ma b/matita/matita/contribs/lambdadelta/basic_2/notation.ma index d53b103c8..b956f9049 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/notation.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/notation.ma @@ -150,6 +150,10 @@ notation "hvbox( ⦃ term 46 L1, break term 46 T1 ⦄ ⊃ break ⦃ term 46 L2 , non associative with precedence 45 for @{ 'SupTerm $L1 $T1 $L2 $T2 }. +notation "hvbox( ⦃ term 46 L1, break term 46 T1 ⦄ ⊃⸮ break ⦃ term 46 L2 , break term 46 T2 ⦄ )" + non associative with precedence 45 + for @{ 'SupTermOpt $L1 $T1 $L2 $T2 }. + notation "hvbox( L ⊢ break ⌘ ⦃ term 46 T ⦄ ≡ break term 46 k )" non associative with precedence 45 for @{ 'ICM $L $T $k }. @@ -254,6 +258,14 @@ notation "hvbox( L1 ⊢ ➡ break term 46 L2 )" non associative with precedence 45 for @{ 'PRedSn $L1 $L2 }. +notation "hvbox( ⦃ term 46 h, break term 46 L ⦄ ⊢ break term 46 T1 ➡ break [ term 46 g ] break term 46 T2 )" + non associative with precedence 45 + for @{ 'PRed $h $g $L $T1 $T2 }. + +notation "hvbox( ⦃ term 46 h, break term 46 L ⦄ ⊢ break term 46 T1 ➡ ➡ break [ term 46 g ] break term 46 T2 )" + non associative with precedence 45 + for @{ 'PRedAlt $h $g $L $T1 $T2 }. + (* Computation **************************************************************) notation "hvbox( L ⊢ break term 46 T1 ➡ * break term 46 T2 )" diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx.ma new file mode 100644 index 000000000..0c6d10fa1 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx.ma @@ -0,0 +1,53 @@ +(**************************************************************************) +(* ___ *) +(* ||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/static/ssta.ma". +include "basic_2/reduction/cpr.ma". + +(* CONTEXT-SENSITIVE EXTENDED PARALLEL REDUCTION FOR TERMS ******************) + +inductive cpx (h) (g): lenv → relation term ≝ +| cpx_cpr : ∀I,L,U2. L ⊢ ⓪{I} ➡ U2 → cpx h g L (⓪{I}) U2 +| cpx_ssta: ∀I,L,U2,l. ⦃h, L⦄ ⊢ ⓪{I} •[g] ⦃l+1, U2⦄ → cpx h g L (⓪{I}) U2 +| cpx_bind: ∀a,I,L,V1,V2,T1,T2,U2. cpx h g L V1 V2 → cpx h g (L.ⓑ{I}V1) T1 T2 → + L ⊢ ⓑ{a,I}V2.T2 ➡ U2 → cpx h g L (ⓑ{a,I}V1.T1) U2 +| cpx_flat: ∀I,L,V1,V2,T1,T2,U2. cpx h g L V1 V2 → cpx h g L T1 T2 → + L ⊢ ⓕ{I}V2.T2 ➡ U2 → cpx h g L (ⓕ{I}V1.T1) U2 +. + +interpretation + "context-sensitive extended parallel reduction (term)" + 'PRed h g L T1 T2 = (cpx h g L T1 T2). + +(* Basic properties *********************************************************) + +(* Note: this is "∀h,g,L. reflexive … (cpx h g L)" *) +lemma cpx_refl: ∀h,g,T,L. ⦃h, L⦄ ⊢ T ➡[g] T. +#h #g #T elim T -T /2 width=1/ * /2 width=5/ +qed. + +lemma cpr_cpx: ∀h,g,T1,L,T2. L ⊢ T1 ➡ T2 → ⦃h, L⦄ ⊢ T1 ➡[g] T2. +#h #g #T1 elim T1 -T1 /2 width=1/ * /2 width=5/ +qed. + +lemma ssta_cpx: ∀h,g,T1,L,T2,l. ⦃h, L⦄ ⊢ T1 •[g] ⦃l+1, T2⦄ → ⦃h, L⦄ ⊢ T1 ➡[g] T2. +#h #g #T1 elim T1 -T1 /2 width=2/ * [|*] +[ #a #I #V1 #T1 #_ #IHT1 #L #X #l #H + elim (ssta_inv_bind1 … H) -H #T2 #HT12 #H destruct /3 width=5/ +| #V1 #T1 #_ #IHT1 #L #X #l #H + elim (ssta_inv_appl1 … H) -H #T2 #HT12 #H destruct /3 width=5/ +| #V1 #T1 #_ #IHT1 #L #X #l #H + lapply (ssta_inv_cast1 … H) -H /3 width=5/ +] +qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_ldrop.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_ldrop.ma new file mode 100644 index 000000000..20445e154 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_ldrop.ma @@ -0,0 +1,64 @@ +(**************************************************************************) +(* ___ *) +(* ||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/cpx.ma". + +(* CONTEXT-SENSITIVE EXTENDED PARALLEL REDUCTION FOR TERMS ******************) + +include "basic_2/substitution/lpss_ldrop.ma". +include "basic_2/substitution/fsups.ma". + +lemma fsup_cpss_trans: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⊃ ⦃L2, T2⦄ → ∀U2. L2 ⊢ T2 ▶* U2 → + ∃∃U1. L1 ⊢ T1 ▶* U1 & ⦃L1, U1⦄ ⊃ ⦃L2, U2⦄. +#L1 #L2 #T1 #T2 #H elim H -L1 -L2 -T1 -T2 [2: * ] [1,2,3,4,5: /3 width=5/ ] +[ * #L1 + [ #V2 #U2 #HVU2 + elim (lift_total U2 0 1) #W2 #HUW2 + @(ex2_intro … W2) /2 width=7/ + @(fsup_ldrop … L1 … HUW2) /2 width=1/ + | #W #U2 #H + @(ex2_intro … (#0)) /2 width=7/ + +| #L1 #K1 #K2 #T1 #T2 #U1 #d #e #HLK1 #HTU1 #_ #IHT12 #U2 #HTU2 + elim (IHT12 … HTU2) -IHT12 -HTU2 #T #HT1 #HT2 + elim (lift_total T d e) #U #HTU + lapply (cpss_lift … HT1 … HLK1 … HTU1 … HTU) -HT1 -HTU1 /3 width=11/ +] +qed-. + + + +(* +include "basic_2/relocation/lift_lift.ma". +include "basic_2/substitution/fsups.ma". +*) +(* +lemma fsup_ssta_trans: ∀h,g,L1,L2,T1,T2. ⦃L1, T1⦄ ⊃ ⦃L2, T2⦄ → + ∀U2,l. ⦃h, L2⦄ ⊢ T2 •[g] ⦃l+1, U2⦄ → + ∃∃L,U1. ⦃h, L1⦄ ⊢ T1 ➡[g] U1 & ⦃L1, U1⦄ ⊃* ⦃L2, U2⦄. + +*) +lemma fsup_ssta_trans: ∀h,g,L1,L2,T1,T2. ⦃L1, T1⦄ ⊃ ⦃L2, T2⦄ → + ∀U2,l. ⦃h, L2⦄ ⊢ T2 •[g] ⦃l+1, U2⦄ → + ∃∃U1. ⦃h, L1⦄ ⊢ T1 ➡[g] U1 & ⦃L1, U1⦄ ⊃ ⦃L2, U2⦄. +#h #g #L1 #L2 #T1 #T2 #H elim H -L1 -L2 -T1 -T2 +[ * #L1 #V1 #U2 #l #H + elim (lift_total U2 0 1) #W2 #HUW2 +(* + [ @(ex2_intro … W2) [ @(cpx_ssta … l) @(ssta_ldef … H) // + | @(fsups_ldrop … L1 … HUW2) /2 width=1/ +*) +| +| #a #I #L1 #V1 #T1 #U2 #l #HT1 + @(ex2_intro … (ⓑ{a,I}V1.U2)) /2 width=1/ diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/xpr.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/xpr.ma deleted file mode 100644 index 8cec0b050..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/reduction/xpr.ma +++ /dev/null @@ -1,66 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -include "basic_2/static/ssta.ma". -include "basic_2/reduction/cpr.ma". - -lemma arith1: ∀x,y,z,w. z < y → x + (y + w) - z = x + y - z + w. -#x #y #z #w #H