From: Ferruccio Guidi Date: Thu, 1 Aug 2013 20:30:06 +0000 (+0000) Subject: partial commit: "unfold" component X-Git-Tag: make_still_working~1121 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=518b7a1751763431b7e0358b7fd471f025141f11;p=helm.git partial commit: "unfold" component --- diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/statictypestar_5.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/statictypestar_5.ma deleted file mode 100644 index 425babd90..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/statictypestar_5.ma +++ /dev/null @@ -1,19 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) - -notation "hvbox( ⦃ term 46 h , break term 46 L ⦄ ⊢ break term 46 T1 •* break [ term 46 g ] break term 46 T2 )" - non associative with precedence 45 - for @{ 'StaticTypeStar $h $g $L $T1 $T2 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/statictypestar_6.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/statictypestar_6.ma new file mode 100644 index 000000000..02adbeb66 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/statictypestar_6.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 G , break term 46 L ⦄ ⊢ break term 46 T1 •* break [ term 46 h, break term 46 g ] break term 46 T2 )" + non associative with precedence 45 + for @{ 'StaticTypeStar $h $g $G $L $T1 $T2 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/unfold_3.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/unfold_3.ma deleted file mode 100644 index 935cd2a0b..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/unfold_3.ma +++ /dev/null @@ -1,19 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) - -notation "hvbox( L1 ⊢ ⧫ * break term 46 T ≡ break term 46 L2 )" - non associative with precedence 45 - for @{ 'Unfold $L1 $T $L2 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/unfold_4.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/unfold_4.ma new file mode 100644 index 000000000..3381c5632 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/unfold_4.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 G, break term 46 L1 ⦄ ⊢ ⧫ * break term 46 T ≡ break term 46 L2 )" + non associative with precedence 45 + for @{ 'Unfold $G $L1 $T $L2 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/unfold/sstas.ma b/matita/matita/contribs/lambdadelta/basic_2/unfold/sstas.ma index 191da2bef..ce1aea36e 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/unfold/sstas.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/unfold/sstas.ma @@ -12,70 +12,70 @@ (* *) (**************************************************************************) -include "basic_2/notation/relations/statictypestar_5.ma". +include "basic_2/notation/relations/statictypestar_6.ma". include "basic_2/static/ssta.ma". (* ITERATED STRATIFIED STATIC TYPE ASSIGNMENT FOR TERMS *********************) (* Note: includes: stass_refl *) -definition sstas: ∀h. sd h → lenv → relation term ≝ - λh,g,L. star … (ssta_step h g L). +definition sstas: ∀h. sd h → genv → lenv → relation term ≝ + λh,g,G,L. star … (ssta_step h g G L). interpretation "iterated stratified static type assignment (term)" - 'StaticTypeStar h g L T U = (sstas h g L T U). + 'StaticTypeStar h g G L T U = (sstas h g G L T U). (* Basic eliminators ********************************************************) -lemma sstas_ind: ∀h,g,L,T. ∀R:predicate term. +lemma sstas_ind: ∀h,g,G,L,T. ∀R:predicate term. R T → ( ∀U1,U2,l. ⦃G, L⦄ ⊢ T •* [h, g] U1 → ⦃G, L⦄ ⊢ U1 •[h, g] ⦃l+1, U2⦄ → R U1 → R U2 ) → ∀U. ⦃G, L⦄ ⊢ T •*[h, g] U → R U. -#h #g #L #T #R #IH1 #IH2 #U #H elim H -U // +#h #g #G #L #T #R #IH1 #IH2 #U #H elim H -U // #U1 #U2 #H * /2 width=5/ qed-. -lemma sstas_ind_dx: ∀h,g,L,U2. ∀R:predicate term. +lemma sstas_ind_dx: ∀h,g,G,L,U2. ∀R:predicate term. R U2 → ( ∀T,U1,l. ⦃G, L⦄ ⊢ T •[h, g] ⦃l+1, U1⦄ → ⦃G, L⦄ ⊢ U1 •* [h, g] U2 → R U1 → R T ) → ∀T. ⦃G, L⦄ ⊢ T •*[h, g] U2 → R T. -#h #g #L #U2 #R #IH1 #IH2 #T #H @(star_ind_l … T H) -T // +#h #g #G #L #U2 #R #IH1 #IH2 #T #H @(star_ind_l … T H) -T // #T #T0 * /2 width=5/ qed-. (* Basic properties *********************************************************) -lemma sstas_refl: ∀h,g,L. reflexive … (sstas h g L). +lemma sstas_refl: ∀h,g,G,L. reflexive … (sstas h g G L). // qed. -lemma ssta_sstas: ∀h,g,L,T,U,l. ⦃G, L⦄ ⊢ T •[h, g] ⦃l+1, U⦄ → ⦃G, L⦄ ⊢ T •*[h, g] U. +lemma ssta_sstas: ∀h,g,G,L,T,U,l. ⦃G, L⦄ ⊢ T •[h, g] ⦃l+1, U⦄ → ⦃G, L⦄ ⊢ T •*[h, g] U. /3 width=2 by R_to_star, ex_intro/ qed. (**) (* auto fails without trace *) -lemma sstas_strap1: ∀h,g,L,T1,T2,U2,l. ⦃G, L⦄ ⊢ T1 •*[h, g] T2 → ⦃G, L⦄ ⊢ T2 •[h, g] ⦃l+1, U2⦄ → +lemma sstas_strap1: ∀h,g,G,L,T1,T2,U2,l. ⦃G, L⦄ ⊢ T1 •*[h, g] T2 → ⦃G, L⦄ ⊢ T2 •[h, g] ⦃l+1, U2⦄ → ⦃G, L⦄ ⊢ T1 •*[h, g] U2. /3 width=4 by sstep, ex_intro/ (**) (* auto fails without trace *) qed. -lemma sstas_strap2: ∀h,g,L,T1,U1,U2,l. ⦃G, L⦄ ⊢ T1 •[h, g] ⦃l+1, U1⦄ → ⦃G, L⦄ ⊢ U1 •*[h, g] U2 → +lemma sstas_strap2: ∀h,g,G,L,T1,U1,U2,l. ⦃G, L⦄ ⊢ T1 •[h, g] ⦃l+1, U1⦄ → ⦃G, L⦄ ⊢ U1 •*[h, g] U2 → ⦃G, L⦄ ⊢ T1 •*[h, g] U2. /3 width=3 by star_compl, ex_intro/ (**) (* auto fails without trace *) qed. (* Basic inversion lemmas ***************************************************) -lemma sstas_inv_bind1: ∀h,g,a,I,L,Y,X,U. ⦃G, L⦄ ⊢ ⓑ{a,I}Y.X •*[h, g] U → - ∃∃Z. ⦃h, L.ⓑ{I}Y⦄ ⊢ X •*[h, g] Z & U = ⓑ{a,I}Y.Z. -#h #g #a #I #L #Y #X #U #H @(sstas_ind … H) -U /2 width=3/ +lemma sstas_inv_bind1: ∀h,g,a,I,G,L,Y,X,U. ⦃G, L⦄ ⊢ ⓑ{a,I}Y.X •*[h, g] U → + ∃∃Z. ⦃G, L.ⓑ{I}Y⦄ ⊢ X •*[h, g] Z & U = ⓑ{a,I}Y.Z. +#h #g #a #I #G #L #Y #X #U #H @(sstas_ind … H) -U /2 width=3/ #T #U #l #_ #HTU * #Z #HXZ #H destruct elim (ssta_inv_bind1 … HTU) -HTU #Z0 #HZ0 #H destruct /3 width=4/ qed-. -lemma sstas_inv_appl1: ∀h,g,L,Y,X,U. ⦃G, L⦄ ⊢ ⓐY.X •*[h, g] U → +lemma sstas_inv_appl1: ∀h,g,G,L,Y,X,U. ⦃G, L⦄ ⊢ ⓐY.X •*[h, g] U → ∃∃Z. ⦃G, L⦄ ⊢ X •*[h, g] Z & U = ⓐY.Z. -#h #g #L #Y #X #U #H @(sstas_ind … H) -U /2 width=3/ +#h #g #G #L #Y #X #U #H @(sstas_ind … H) -U /2 width=3/ #T #U #l #_ #HTU * #Z #HXZ #H destruct elim (ssta_inv_appl1 … HTU) -HTU #Z0 #HZ0 #H destruct /3 width=4/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/unfold/sstas_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/unfold/sstas_aaa.ma index b369caa72..ff3c48fe8 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/unfold/sstas_aaa.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/unfold/sstas_aaa.ma @@ -19,7 +19,7 @@ include "basic_2/unfold/sstas.ma". (* Properties on atomic arity assignment for terms **************************) -lemma sstas_aaa: ∀h,g,L,T,U. ⦃G, L⦄ ⊢ T •*[h, g] U → +lemma sstas_aaa: ∀h,g,G,L,T,U. ⦃G, L⦄ ⊢ T •*[h, g] U → ∀A. ⦃G, L⦄ ⊢ T ⁝ A → ⦃G, L⦄ ⊢ U ⁝ A. -#h #g #L #T #U #H @(sstas_ind_dx … H) -T // /3 width=6/ +#h #g #G #L #T #U #H @(sstas_ind_dx … H) -T // /3 width=6/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/unfold/sstas_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/unfold/sstas_lift.ma index 8bde8538f..ec6fdc0c3 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/unfold/sstas_lift.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/unfold/sstas_lift.ma @@ -19,20 +19,20 @@ include "basic_2/unfold/sstas.ma". (* Advanced forward lemmas **************************************************) -lemma sstas_fwd_correct: ∀h,g,L,T1,U1,l1. ⦃G, L⦄ ⊢ T1 •[h, g] ⦃l1, U1⦄ → +lemma sstas_fwd_correct: ∀h,g,G,L,T1,U1,l1. ⦃G, L⦄ ⊢ T1 •[h, g] ⦃l1, U1⦄ → ∀T2. ⦃G, L⦄ ⊢ T1 •*[h, g] T2 → ∃∃U2,l2. ⦃G, L⦄ ⊢ T2 •[h, g] ⦃l2, U2⦄. -#h #g #L #T1 #U1 #l1 #HTU1 #T2 #H @(sstas_ind … H) -T2 [ /2 width=3/ ] -HTU1 +#h #g #G #L #T1 #U1 #l1 #HTU1 #T2 #H @(sstas_ind … H) -T2 [ /2 width=3/ ] -HTU1 #T #T2 #l #_ #HT2 * #U #l0 #_ -l0 elim (ssta_fwd_correct … HT2) -T /2 width=3/ qed-. (* Properties on relocation *************************************************) -lemma sstas_lift: ∀h,g,L1,T1,U1. ⦃h, L1⦄ ⊢ T1 •*[h, g] U1 → +lemma sstas_lift: ∀h,g,G,L1,T1,U1. ⦃G, L1⦄ ⊢ T1 •*[h, g] U1 → ∀L2,d,e. ⇩[d, e] L2 ≡ L1 → ∀T2. ⇧[d, e] T1 ≡ T2 → - ∀U2. ⇧[d, e] U1 ≡ U2 → ⦃h, L2⦄ ⊢ T2 •*[h, g] U2. -#h #g #L1 #T1 #U1 #H @(sstas_ind_dx … H) -T1 + ∀U2. ⇧[d, e] U1 ≡ U2 → ⦃G, L2⦄ ⊢ T2 •*[h, g] U2. +#h #g #G #L1 #T1 #U1 #H @(sstas_ind_dx … H) -T1 [ #L2 #d #e #HL21 #X #HX #U2 #HU12 >(lift_mono … HX … HU12) -X // | #T0 #U0 #l0 #HTU0 #_ #IHU01 #L2 #d #e #HL21 #T2 #HT02 #U2 #HU12 @@ -42,10 +42,10 @@ qed. (* Inversion lemmas on relocation *******************************************) -lemma sstas_inv_lift1: ∀h,g,L2,T2,U2. ⦃h, L2⦄ ⊢ T2 •*[h, g] U2 → +lemma sstas_inv_lift1: ∀h,g,G,L2,T2,U2. ⦃G, L2⦄ ⊢ T2 •*[h, g] U2 → ∀L1,d,e. ⇩[d, e] L2 ≡ L1 → ∀T1. ⇧[d, e] T1 ≡ T2 → - ∃∃U1. ⦃h, L1⦄ ⊢ T1 •*[h, g] U1 & ⇧[d, e] U1 ≡ U2. -#h #g #L2 #T2 #U2 #H @(sstas_ind_dx … H) -T2 /2 width=3/ + ∃∃U1. ⦃G, L1⦄ ⊢ T1 •*[h, g] U1 & ⇧[d, e] U1 ≡ U2. +#h #g #G #L2 #T2 #U2 #H @(sstas_ind_dx … H) -T2 /2 width=3/ #T0 #U0 #l0 #HTU0 #_ #IHU01 #L1 #d #e #HL21 #U1 #HU12 elim (ssta_inv_lift1 … HTU0 … HL21 … HU12) -HTU0 -HU12 #U #HU1 #HU0 elim (IHU01 … HL21 … HU0) -IHU01 -HL21 -U0 /3 width=4/ diff --git a/matita/matita/contribs/lambdadelta/basic_2/unfold/sstas_sstas.ma b/matita/matita/contribs/lambdadelta/basic_2/unfold/sstas_sstas.ma index 2d7febf1d..cc98d0ea0 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/unfold/sstas_sstas.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/unfold/sstas_sstas.ma @@ -19,33 +19,33 @@ include "basic_2/unfold/sstas.ma". (* Advanced inversion lemmas ************************************************) -lemma sstas_inv_O: ∀h,g,L,T,U. ⦃G, L⦄ ⊢ T •*[h, g] U → +lemma sstas_inv_O: ∀h,g,G,L,T,U. ⦃G, L⦄ ⊢ T •*[h, g] U → ∀T0. ⦃G, L⦄ ⊢ T •[h, g] ⦃0, T0⦄ → U = T. -#h #g #L #T #U #H @(sstas_ind_dx … H) -T // +#h #g #G #L #T #U #H @(sstas_ind_dx … H) -T // #T0 #U0 #l0 #HTU0 #_ #_ #T1 #HT01 elim (ssta_mono … HTU0 … HT01)