From 178820be7648a60af17837727e51fd1f3f2791db Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Sat, 8 Dec 2012 14:54:25 +0000 Subject: [PATCH] - new pointes can point to any subterm - new star_ind_l-like eliminator for lstar now in use --- .../contribs/lambda/delifting_substitution.ma | 3 +- .../lambda/labelled_hap_computation.ma | 52 +++++++------- .../contribs/lambda/labelled_hap_reduction.ma | 49 +++++++++++-- .../lambda/labelled_sequential_computation.ma | 8 +-- .../lambda/labelled_sequential_reduction.ma | 72 +++++++++---------- matita/matita/contribs/lambda/lift.ma | 8 ++- .../contribs/lambda/parallel_reduction.ma | 28 ++++---- matita/matita/contribs/lambda/pointer.ma | 45 ++++++++++++ .../{redex_pointer.ma => pointer_order.ma} | 48 +++++-------- ...ointer_sequence.ma => pointer_sequence.ma} | 19 ++--- matita/matita/contribs/lambda/policy.txt | 6 +- matita/matita/contribs/lambda/preamble.ma | 16 +++-- .../matita/contribs/lambda/st_computation.ma | 4 +- matita/matita/contribs/lambda/xoa.conf.xml | 4 +- matita/matita/contribs/lambda/xoa.ma | 16 +++++ matita/matita/contribs/lambda/xoa_notation.ma | 20 ++++++ 16 files changed, 253 insertions(+), 145 deletions(-) create mode 100644 matita/matita/contribs/lambda/pointer.ma rename matita/matita/contribs/lambda/{redex_pointer.ma => pointer_order.ma} (55%) rename matita/matita/contribs/lambda/{redex_pointer_sequence.ma => pointer_sequence.ma} (69%) diff --git a/matita/matita/contribs/lambda/delifting_substitution.ma b/matita/matita/contribs/lambda/delifting_substitution.ma index 79a65396a..6ad8d252c 100644 --- a/matita/matita/contribs/lambda/delifting_substitution.ma +++ b/matita/matita/contribs/lambda/delifting_substitution.ma @@ -160,5 +160,6 @@ qed. lemma lstar_dsubstable_dx: ∀T,R. (∀t. dsubstable_dx (R t)) → ∀l. dsubstable_dx (lstar T … R l). -#T #R #HR #l #D #M1 #M2 #H elim H -l -M1 -M2 // /3 width=3/ +#T #R #HR #l #D #M1 #M2 #H +@(lstar_ind_l ????????? H) -l -M1 // /3 width=3/ qed. diff --git a/matita/matita/contribs/lambda/labelled_hap_computation.ma b/matita/matita/contribs/lambda/labelled_hap_computation.ma index e7804cb7c..70cc06b79 100644 --- a/matita/matita/contribs/lambda/labelled_hap_computation.ma +++ b/matita/matita/contribs/lambda/labelled_hap_computation.ma @@ -20,7 +20,7 @@ include "labelled_hap_reduction.ma". (* Note: this is the "head in application" computation of: R. Kashima: "A proof of the Standization Theorem in λ-Calculus". Typescript note, (2000). *) -definition lhap: rpseq → relation term ≝ lstar … lhap1. +definition lhap: pseq → relation term ≝ lstar … lhap1. interpretation "labelled 'hap' computation" 'HApStar M p N = (lhap p M N). @@ -57,38 +57,42 @@ qed-. lemma lhap_dsubst: ∀s. dsubstable_dx (lhap s). /2 width=1/ qed. -(* + theorem lhap_mono: ∀s. singlevalued … (lhap s). /3 width=7 by lstar_singlevalued, lhap1_mono/ qed-. -*) + theorem lhap_trans: ∀s1,M1,M. M1 ⓗ⇀*[s1] M → ∀s2,M2. M ⓗ⇀*[s2] M2 → M1 ⓗ⇀*[s1@s2] M2. /2 width=3 by lstar_trans/ qed-. -(* -lemma hap_appl: appl_compatible_dx hap. -/3 width=1/ + +lemma lhap_appl: ∀s,B,A1,A2. A1 ⓗ⇀*[s] A2 → @B.A1 ⓗ⇀*[dx:::s] @B.A2. +#s #B #A1 #A2 #H @(lstar_ind_l ????????? H) -s -A1 // /3 width=3/ qed. -*) -lemma lhap_spine_fwd: ∀s,M1,M2. M1 ⓗ⇀*[s] M2 → is_spine s. -#s #M1 #M2 #H elim H -s -M1 -M2 // -#p #M1 #M #HM1 #s #M2 #_ #IHM2 -lapply (lhap1_spine_fwd … HM1) -HM1 /2 width=1/ + +lemma head_lsreds_lhap: ∀s,M1,M2. M1 ⇀*[s] M2 → is_head s → M1 ⓗ⇀*[s] M2. +#s #M1 #M2 #H @(lstar_ind_l ????????? H) -s -M1 // +#a #s #M1 #M #HM1 #_ #IHM2 * /3 width=3/ +qed. + +lemma lhap_inv_head: ∀s,M1,M2. M1 ⓗ⇀*[s] M2 → is_head s. +#s #M1 #M2 #H @(lstar_ind_l ????????? H) -s -M1 // +#p #s #M1 #M #HM1 #_ #IHM2 +lapply (lhap1_inv_head … HM1) -HM1 /2 width=1/ qed-. -lemma lhap_lsreds_fwd: ∀s,M1,M2. M1 ⓗ⇀*[s] M2 → M1 ⇀*[s] M2. -#s #M1 #M2 #H elim H -s -M1 -M2 // -#p #M1 #M #HM1 #s #M2 #_ #IHM2 -lapply (lhap1_lsred_fwd … HM1) -HM1 /2 width=3/ +lemma lhap_inv_lsreds: ∀s,M1,M2. M1 ⓗ⇀*[s] M2 → M1 ⇀*[s] M2. +#s #M1 #M2 #H @(lstar_ind_l ????????? H) -s -M1 // +#p #s #M1 #M #HM1 #_ #IHM2 +lapply (lhap1_inv_lsred … HM1) -HM1 /2 width=3/ qed-. -lemma lhap_le_fwd: ∀s,M1,M2. M1 ⓗ⇀*[s] M2 → is_le s. -(* -#M1 #M2 #H @(star_ind_l ??????? H) -M1 /3 width=3/ -#M1 #M #HM1 #H * #s * #H1s #H2s -generalize in match HM1; -HM1 generalize in match M1; -M1 -@(star_ind_l ??????? H) -M -[ #M1 #HM12 elim (hap1_lsred … HM12) -HM12 /4 width=3/ -| #M0 #M1 #HM01 #HM12 #_ #M #HM0 #HM02 -*) +lemma lhap_fwd_le: ∀s,M1,M2. M1 ⓗ⇀*[s] M2 → is_le s. +#s #M1 #M2 #H @(lstar_ind_l ????????? H) -s -M1 /3 width=3/ +#a1 #s #M1 #M #HM1 #IHM1 +generalize in match HM1; -HM1 +cases IHM1 -s -M -M2 // +#a #M0 #M #HM0 #s #M2 #_ #HM10 #H -M2 +lapply (lhap1_fwd_le … HM10 … HM0) -M -M0 -M1 /2 width=1/ +qed-. diff --git a/matita/matita/contribs/lambda/labelled_hap_reduction.ma b/matita/matita/contribs/lambda/labelled_hap_reduction.ma index 705069f8b..575abd342 100644 --- a/matita/matita/contribs/lambda/labelled_hap_reduction.ma +++ b/matita/matita/contribs/lambda/labelled_hap_reduction.ma @@ -12,6 +12,7 @@ (* *) (**************************************************************************) +include "pointer_order.ma". include "labelled_sequential_reduction.ma". (* KASHIMA'S "HAP" COMPUTATION (LABELLED SINGLE STEP) ***********************) @@ -19,9 +20,9 @@ include "labelled_sequential_reduction.ma". (* Note: this is one step of the "head in application" computation of: R. Kashima: "A proof of the Standization Theorem in λ-Calculus". Typescript note, (2000). *) -inductive lhap1: rptr → relation term ≝ +inductive lhap1: ptr → relation term ≝ | hap1_beta: ∀B,A. lhap1 (◊) (@B.𝛌.A) ([⬐B]A) -| hap1_appl: ∀p,B,A1,A2. lhap1 p A1 A2 → lhap1 (false::p) (@B.A1) (@B.A2) +| hap1_appl: ∀p,B,A1,A2. lhap1 p A1 A2 → lhap1 (dx::p) (@B.A1) (@B.A2) . interpretation "labelled 'hap' reduction" @@ -31,6 +32,22 @@ notation "hvbox( M break ⓗ⇀ [ term 46 p ] break term 46 N )" non associative with precedence 45 for @{ 'HAp $M $p $N }. +lemma lhap1_inv_nil: ∀p,M,N. M ⓗ⇀[p] N → ◊ = p → + ∃∃B,A. @B.𝛌.A = M & [⬐B]A = N. +#p #M #N * -p -M -N +[ #B #A #_ /2 width=4/ +| #p #B #A1 #A2 #_ #H destruct +] +qed-. + +lemma lhap1_inv_cons: ∀p,M,N. M ⓗ⇀[p] N → ∀c,q. c::q = p → + ∃∃B,A1,A2. dx = c & A1 ⓗ⇀[q] A2 & @B.A1 = M & @B.A2 = N. +#p #M #N * -p -M -N +[ #B #A #c #q #H destruct +| #p #B #A1 #A2 #HA12 #c #q #H destruct /2 width=6/ +] +qed-. + lemma lhap1_inv_abst_sn: ∀p,M,N. M ⓗ⇀[p] N → ∀A. 𝛌.A = M → ⊥. #p #M #N * -p -M -N [ #B #A #A0 #H destruct @@ -40,7 +57,7 @@ qed-. lemma lhap1_inv_appl_sn: ∀p,M,N. M ⓗ⇀[p] N → ∀B,A. @B.A = M → (∃∃C. ◊ = p & 𝛌.C = A & [⬐B]C = N) ∨ - ∃∃q,C. A ⓗ⇀[q] C & false::q = p & @B.C = N. + ∃∃q,C. A ⓗ⇀[q] C & dx::q = p & @B.C = N. #p #M #N * -p -M -N [ #B #A #B0 #A0 #H destruct /3 width=3/ | #p #B #A1 #A2 #HA12 #B0 #A0 #H destruct /3 width=5/ @@ -77,15 +94,23 @@ lemma lhap1_dsubst: ∀p. dsubstable_dx (lhap1 p). #D2 #A #d >dsubst_dsubst_ge // qed. -lemma lhap1_spine_fwd: ∀p,M,N. M ⓗ⇀[p] N → in_spine p. -#p #M #N #H elim H -p -M -N // /2 width=1/ +lemma head_lsred_lhap1: ∀p. in_head p → ∀M,N. M ⇀[p] N → M ⓗ⇀[p] N. +#p #H @(in_head_ind … H) -p +[ #M #N #H elim (lsred_inv_nil … H ?) -H // +| #p #_ #IHp #M #N #H + elim (lsred_inv_dx … H ??) -H [3: // |2: skip ] /3 width=1/ (**) (* simplify line *) +] +qed. + +lemma lhap1_inv_head: ∀p,M,N. M ⓗ⇀[p] N → in_head p. +#p #M #N #H elim H -p -M -N // /2 width=1/ qed-. -lemma lhap1_lsred_fwd: ∀p,M,N. M ⓗ⇀[p] N → M ⇀[p] N. +lemma lhap1_inv_lsred: ∀p,M,N. M ⓗ⇀[p] N → M ⇀[p] N. #p #M #N #H elim H -p -M -N // /2 width=1/ qed-. -lemma lhap1_le_fwd: ∀p1,M1,M. M1 ⓗ⇀[p1] M → ∀p2,M2. M ⓗ⇀[p2] M2 → p1 ≤ p2. +lemma lhap1_fwd_le: ∀p1,M1,M. M1 ⓗ⇀[p1] M → ∀p2,M2. M ⓗ⇀[p2] M2 → p1 ≤ p2. #p1 #M1 #M #H elim H -p1 -M1 -M // #p1 #B #A1 #A2 #HA12 #IHA12 #p2 #M2 #H elim (lhap1_inv_appl_sn … H ???) -H [5: // |2,3: skip ] * (**) (* simplify line *) @@ -94,3 +119,13 @@ elim (lhap1_inv_appl_sn … H ???) -H [5: // |2,3: skip ] * (**) (* simplify lin | -HA12 /3 width=2/ ] qed-. + +theorem lhap1_mono: ∀p. singlevalued … (lhap1 p). +#p #M #N1 #H elim H -p -M -N1 +[ #B #A #N2 #H + elim (lhap1_inv_nil … H ?) -H // #D #C #H #HN2 destruct // +| #p #B #A1 #A2 #_ #IHA12 #N2 #H + elim (lhap1_inv_cons … H ???) -H [4: // |2,3: skip ] (**) (* simplify line *) + #D #C1 #C2 #_ #HC12 #H #HN2 destruct /3 width=1/ +] +qed-. diff --git a/matita/matita/contribs/lambda/labelled_sequential_computation.ma b/matita/matita/contribs/lambda/labelled_sequential_computation.ma index 52fef2514..1ec666483 100644 --- a/matita/matita/contribs/lambda/labelled_sequential_computation.ma +++ b/matita/matita/contribs/lambda/labelled_sequential_computation.ma @@ -12,12 +12,12 @@ (* *) (**************************************************************************) -include "redex_pointer_sequence.ma". +include "pointer_sequence.ma". include "labelled_sequential_reduction.ma". (* LABELLED SEQUENTIAL COMPUTATION (MULTISTEP) ******************************) -definition lsreds: rpseq → relation term ≝ lstar … lsred. +definition lsreds: pseq → relation term ≝ lstar … lsred. interpretation "labelled sequential computation" 'SeqRedStar M s N = (lsreds s M N). @@ -66,8 +66,8 @@ qed-. (* Note: "|s|" should be unparetesized *) lemma lsreds_fwd_mult: ∀s,M1,M2. M1 ⇀*[s] M2 → #{M2} ≤ #{M1} ^ (2 ^ (|s|)). -#s #M1 #M2 #H elim H -s -M1 -M2 normalize // -#p #M1 #M #HM1 #s #M2 #_ #IHM2 +#s #M1 #M2 #H @(lstar_ind_l ????????? H) -s -M1 normalize // +#p #s #M1 #M #HM1 #_ #IHM2 lapply (lsred_fwd_mult … HM1) -p #HM1 @(transitive_le … IHM2) -M2 /3 width=1 by le_exp1, lt_O_exp, lt_to_le/ (**) (* auto: slow without trace *) diff --git a/matita/matita/contribs/lambda/labelled_sequential_reduction.ma b/matita/matita/contribs/lambda/labelled_sequential_reduction.ma index 208eb4023..21d24c668 100644 --- a/matita/matita/contribs/lambda/labelled_sequential_reduction.ma +++ b/matita/matita/contribs/lambda/labelled_sequential_reduction.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "redex_pointer.ma". +include "pointer.ma". include "multiplicity.ma". (* LABELLED SEQUENTIAL REDUCTION (SINGLE STEP) ******************************) @@ -21,11 +21,11 @@ include "multiplicity.ma". F. Kamareddine and R.P. Nederpelt: "A useful λ-notation". Theoretical Computer Science 155(1), Elsevier (1996), pp. 85-109. *) -inductive lsred: rptr → relation term ≝ +inductive lsred: ptr → relation term ≝ | lsred_beta : ∀B,A. lsred (◊) (@B.𝛌.A) ([⬐B]A) -| lsred_abst : ∀p,A,C. lsred p A C → lsred p (𝛌.A) (𝛌.C) -| lsred_appl_sn: ∀p,B,D,A. lsred p B D → lsred (true::p) (@B.A) (@D.A) -| lsred_appl_dx: ∀p,B,A,C. lsred p A C → lsred (false::p) (@B.A) (@B.C) +| lsred_abst : ∀p,A1,A2. lsred p A1 A2 → lsred (rc::p) (𝛌.A1) (𝛌.A2) +| lsred_appl_sn: ∀p,B1,B2,A. lsred p B1 B2 → lsred (sn::p) (@B1.A) (@B2.A) +| lsred_appl_dx: ∀p,B,A1,A2. lsred p A1 A2 → lsred (dx::p) (@B.A1) (@B.A2) . interpretation "labelled sequential reduction" @@ -39,49 +39,49 @@ notation "hvbox( M break ⇀ [ term 46 p ] break term 46 N )" lemma lsred_inv_vref: ∀p,M,N. M ⇀[p] N → ∀i. #i = M → ⊥. #p #M #N * -p -M -N [ #B #A #i #H destruct -| #p #A #C #_ #i #H destruct -| #p #B #D #A #_ #i #H destruct -| #p #B #A #C #_ #i #H destruct +| #p #A1 #A2 #_ #i #H destruct +| #p #B1 #B2 #A #_ #i #H destruct +| #p #B #A1 #A2 #_ #i #H destruct ] qed-. -lemma lsred_inv_beta: ∀p,M,N. M ⇀[p] N → ∀D,C. @D.C = M → ◊ = p → - ∃∃A. 𝛌.A = C & [⬐D] A = N. +lemma lsred_inv_nil: ∀p,M,N. M ⇀[p] N → ◊ = p → + ∃∃B,A. @B. 𝛌.A = M & [⬐B] A = N. #p #M #N * -p -M -N -[ #B #A #D0 #C0 #H #_ destruct /2 width=3/ -| #p #A #C #_ #D0 #C0 #H destruct -| #p #B #D #A #_ #D0 #C0 #_ #H destruct -| #p #B #A #C #_ #D0 #C0 #_ #H destruct +[ #B #A #_ destruct /2 width=4/ +| #p #A1 #A2 #_ #H destruct +| #p #B1 #B2 #A #_ #H destruct +| #p #B #A1 #A2 #_ #H destruct ] qed-. -lemma lsred_inv_abst: ∀p,M,N. M ⇀[p] N → ∀A. 𝛌.A = M → - ∃∃C. A ⇀[p] C & 𝛌.C = N. +lemma lsred_inv_rc: ∀p,M,N. M ⇀[p] N → ∀q. rc::q = p → + ∃∃A1,A2. A1 ⇀[q] A2 & 𝛌.A1 = M & 𝛌.A2 = N. #p #M #N * -p -M -N -[ #B #A #A0 #H destruct -| #p #A #C #HAC #A0 #H destruct /2 width=3/ -| #p #B #D #A #_ #A0 #H destruct -| #p #B #A #C #_ #A0 #H destruct +[ #B #A #q #H destruct +| #p #A1 #A2 #HA12 #q #H destruct /2 width=5/ +| #p #B1 #B2 #A #_ #q #H destruct +| #p #B #A1 #A2 #_ #q #H destruct ] qed-. -lemma lsred_inv_appl_sn: ∀p,M,N. M ⇀[p] N → ∀B,A,q. @B.A = M → true::q = p → - ∃∃D. B ⇀[q] D & @D.A = N. +lemma lsred_inv_sn: ∀p,M,N. M ⇀[p] N → ∀q. sn::q = p → + ∃∃B1,B2,A. B1 ⇀[q] B2 & @B1.A = M & @B2.A = N. #p #M #N * -p -M -N -[ #B #A #B0 #A0 #p0 #_ #H destruct -| #p #A #C #_ #B0 #D0 #p0 #H destruct -| #p #B #D #A #HBD #B0 #A0 #p0 #H1 #H2 destruct /2 width=3/ -| #p #B #A #C #_ #B0 #A0 #p0 #_ #H destruct +[ #B #A #q #H destruct +| #p #A1 #A2 #_ #q #H destruct +| #p #B1 #B2 #A #HB12 #q #H destruct /2 width=6/ +| #p #B #A1 #A2 #_ #q #H destruct ] qed-. -lemma lsred_inv_appl_dx: ∀p,M,N. M ⇀[p] N → ∀B,A,q. @B.A = M → false::q = p → - ∃∃C. A ⇀[q] C & @B.C = N. +lemma lsred_inv_dx: ∀p,M,N. M ⇀[p] N → ∀q. dx::q = p → + ∃∃B,A1,A2. A1 ⇀[q] A2 & @B.A1 = M & @B.A2 = N. #p #M #N * -p -M -N -[ #B #A #B0 #A0 #p0 #_ #H destruct -| #p #A #C #_ #B0 #D0 #p0 #H destruct -| #p #B #D #A #_ #B0 #A0 #p0 #_ #H destruct -| #p #B #A #C #HAC #B0 #A0 #p0 #H1 #H2 destruct /2 width=3/ +[ #B #A #q #H destruct +| #p #A1 #A2 #_ #q #H destruct +| #p #B1 #B2 #A #_ #q #H destruct +| #p #B #A1 #A2 #HA12 #q #H destruct /2 width=6/ ] qed-. @@ -131,9 +131,9 @@ qed. theorem lsred_mono: ∀p. singlevalued … (lsred p). #p #M #N1 #H elim H -p -M -N1 -[ #B #A #N2 #H elim (lsred_inv_beta … H ????) -H [4,5: // |2,3: skip ] #A0 #H1 #H2 destruct // (**) (* simplify line *) -| #p #A #C #_ #IHAC #N2 #H elim (lsred_inv_abst … H ??) -H [3: // |2: skip ] #C0 #HAC #H destruct /3 width=1/ (**) (* simplify line *) -| #p #B #D #A #_ #IHBD #N2 #H elim (lsred_inv_appl_sn … H ?????) -H [5,6: // |2,3,4: skip ] #D0 #HBD #H destruct /3 width=1/ (**) (* simplify line *) -| #p #B #A #C #_ #IHAC #N2 #H elim (lsred_inv_appl_dx … H ?????) -H [5,6: // |2,3,4: skip ] #C0 #HAC #H destruct /3 width=1/ (**) (* simplify line *) +[ #B #A #N2 #H elim (lsred_inv_nil … H ?) -H // #D #C #H #HN2 destruct // +| #p #A1 #A2 #_ #IHA12 #N2 #H elim (lsred_inv_rc … H ??) -H [3: // |2: skip ] #C1 #C2 #HC12 #H #HN2 destruct /3 width=1/ (**) (* simplify line *) +| #p #B1 #B2 #A #_ #IHB12 #N2 #H elim (lsred_inv_sn … H ??) -H [3: // |2: skip ] #D1 #D2 #C #HD12 #H #HN2 destruct /3 width=1/ (**) (* simplify line *) +| #p #B #A1 #A2 #_ #IHA12 #N2 #H elim (lsred_inv_dx … H ??) -H [3: // |2: skip ] #D #C1 #C2 #HC12 #H #HN2 destruct /3 width=1/ (**) (* simplify line *) ] qed-. diff --git a/matita/matita/contribs/lambda/lift.ma b/matita/matita/contribs/lambda/lift.ma index 60038de76..43443e5b4 100644 --- a/matita/matita/contribs/lambda/lift.ma +++ b/matita/matita/contribs/lambda/lift.ma @@ -260,13 +260,15 @@ qed-. lemma lstar_liftable: ∀T,R. (∀t. liftable (R t)) → ∀l. liftable (lstar T … R l). -#T #R #HR #l #h #M1 #M2 #H elim H -l -M1 -M2 // /3 width=3/ +#T #R #HR #l #h #M1 #M2 #H +@(lstar_ind_l ????????? H) -l -M1 // /3 width=3/ qed. lemma lstar_deliftable_sn: ∀T,R. (∀t. deliftable_sn (R t)) → ∀l. deliftable_sn (lstar T … R l). -#T #R #HR #l #h #N1 #N2 #H elim H -l -N1 -N2 /2 width=3/ -#t #N1 #N #HN1 #l #N2 #_ #IHN2 #d #M1 #HMN1 +#T #R #HR #l #h #N1 #N2 #H +@(lstar_ind_l ????????? H) -l -N1 /2 width=3/ +#t #l #N1 #N #HN1 #_ #IHN2 #d #M1 #HMN1 elim (HR … HN1 … HMN1) -N1 #M #HM1 #HMN elim (IHN2 … HMN) -N /3 width=3/ qed-. diff --git a/matita/matita/contribs/lambda/parallel_reduction.ma b/matita/matita/contribs/lambda/parallel_reduction.ma index f5285bad1..91fe30e1c 100644 --- a/matita/matita/contribs/lambda/parallel_reduction.ma +++ b/matita/matita/contribs/lambda/parallel_reduction.ma @@ -22,9 +22,9 @@ include "labelled_sequential_reduction.ma". *) inductive pred: relation term ≝ | pred_vref: ∀i. pred (#i) (#i) -| pred_abst: ∀A,C. pred A C → pred (𝛌.A) (𝛌.C) -| pred_appl: ∀B,D,A,C. pred B D → pred A C → pred (@B.A) (@D.C) -| pred_beta: ∀B,D,A,C. pred B D → pred A C → pred (@B.𝛌.A) ([⬐D]C) +| pred_abst: ∀A1,A2. pred A1 A2 → pred (𝛌.A1) (𝛌.A2) +| pred_appl: ∀B1,B2,A1,A2. pred B1 B2 → pred A1 A2 → pred (@B1.A1) (@B2.A2) +| pred_beta: ∀B1,B2,A1,A2. pred B1 B2 → pred A1 A2 → pred (@B1.𝛌.A1) ([⬐B2]A2) . interpretation "parallel reduction" @@ -40,9 +40,9 @@ qed. lemma pred_inv_vref: ∀M,N. M ⥤ N → ∀i. #i = M → #i = N. #M #N * -M -N // -[ #A #C #_ #i #H destruct -| #B #D #A #C #_ #_ #i #H destruct -| #B #D #A #C #_ #_ #i #H destruct +[ #A1 #A2 #_ #i #H destruct +| #B1 #B2 #A1 #A2 #_ #_ #i #H destruct +| #B1 #B2 #A1 #A2 #_ #_ #i #H destruct ] qed-. @@ -50,9 +50,9 @@ lemma pred_inv_abst: ∀M,N. M ⥤ N → ∀A. 𝛌.A = M → ∃∃C. A ⥤ C & 𝛌.C = N. #M #N * -M -N [ #i #A0 #H destruct -| #A #C #HAC #A0 #H destruct /2 width=3/ -| #B #D #A #C #_ #_ #A0 #H destruct -| #B #D #A #C #_ #_ #A0 #H destruct +| #A1 #A2 #HA12 #A0 #H destruct /2 width=3/ +| #B1 #B2 #A1 #A2 #_ #_ #A0 #H destruct +| #B1 #B2 #A1 #A2 #_ #_ #A0 #H destruct ] qed-. @@ -61,15 +61,15 @@ lemma pred_inv_appl: ∀M,N. M ⥤ N → ∀B,A. @B.A = M → ∃∃A0,D,C0. B ⥤ D & A0 ⥤ C0 & 𝛌.A0 = A & [⬐D]C0 = N. #M #N * -M -N [ #i #B0 #A0 #H destruct -| #A #C #_ #B0 #A0 #H destruct -| #B #D #A #C #HBD #HAC #B0 #A0 #H destruct /3 width=5/ -| #B #D #A #C #HBD #HAC #B0 #A0 #H destruct /3 width=7/ +| #A1 #A2 #_ #B0 #A0 #H destruct +| #B1 #B2 #A1 #A2 #HB12 #HA12 #B0 #A0 #H destruct /3 width=5/ +| #B1 #B2 #A1 #A2 #HB12 #HA12 #B0 #A0 #H destruct /3 width=7/ ] qed-. lemma pred_lift: liftable pred. #h #M1 #M2 #H elim H -M1 -M2 normalize // /2 width=1/ -#D #D #A #C #_ #_ #IHBD #IHAC #d dsubst_dsubst_ge // /2 width=1/ ] qed. diff --git a/matita/matita/contribs/lambda/pointer.ma b/matita/matita/contribs/lambda/pointer.ma new file mode 100644 index 000000000..8d7afa1aa --- /dev/null +++ b/matita/matita/contribs/lambda/pointer.ma @@ -0,0 +1,45 @@ +(**************************************************************************) +(* ___ *) +(* ||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 "preamble.ma". + +(* POINTER ******************************************************************) + +(* Policy: pointer step metavariables: c *) +(* Note: this is a step of a path in the tree representation of a term: + rc (rectus) : proceed on the argument of an abstraction + sn (sinister): proceed on the left argument of an application + dx (dexter) : proceed on the right argument of an application +*) +inductive ptr_step: Type[0] ≝ +| rc: ptr_step +| sn: ptr_step +| dx: ptr_step +. + +definition is_dx: predicate ptr_step ≝ λc. dx = c. + +(* Policy: pointer metavariables: p, q *) +(* Note: this is a path in the tree representation of a term, heading to a redex *) +definition ptr: Type[0] ≝ list ptr_step. + +(* Note: a redex is "in the head" when is not under an abstraction nor in the lefr argument of an application *) +definition in_head: predicate ptr ≝ All … is_dx. + +lemma in_head_ind: ∀R:predicate ptr. R (◊) → + (∀p. in_head p → R p → R (dx::p)) → + ∀p. in_head p → R p. +#R #H #IH #p elim p -p // -H * +#p #IHp * #H1 #H2 destruct /3 width=1/ +qed-. diff --git a/matita/matita/contribs/lambda/redex_pointer.ma b/matita/matita/contribs/lambda/pointer_order.ma similarity index 55% rename from matita/matita/contribs/lambda/redex_pointer.ma rename to matita/matita/contribs/lambda/pointer_order.ma index 5746787c5..9d79e9dc6 100644 --- a/matita/matita/contribs/lambda/redex_pointer.ma +++ b/matita/matita/contribs/lambda/pointer_order.ma @@ -12,35 +12,21 @@ (* *) (**************************************************************************) -include "term.ma". +include "pointer.ma". -(* REDEX POINTER ************************************************************) - -(* Policy: boolean metavariables: a, b - pointer metavariables: p, q -*) -(* Note: this is a path in the tree representation of a term - in which abstraction nodes are omitted; - on application nodes, "false" means "proceed right" - and "true" means "proceed left" -*) -definition rptr: Type[0] ≝ list bool. - -(* Note: a redex is "in the spine" when is not in the argument of an application *) -definition in_spine: predicate rptr ≝ λp. - All … is_false p. +(* POINTER ORDER ************************************************************) (* Note: precedence relation on redex pointers: p ≺ q to serve as base for the order relations: p < q and p ≤ q *) -inductive rpprec: relation rptr ≝ -| rpprec_nil : ∀b,q. rpprec (◊) (b::q) -| rppprc_cons: ∀p,q. rpprec (false::p) (true::q) -| rpprec_comp: ∀b,p,q. rpprec p q → rpprec (b::p) (b::q) -| rpprec_skip: rpprec (false::◊) ◊ +inductive pprec: relation ptr ≝ +| pprec_nil : ∀c,q. pprec (◊) (c::q) +| ppprc_cons: ∀p,q. pprec (dx::p) (sn::q) +| pprec_comp: ∀c,p,q. pprec p q → pprec (c::p) (c::q) +| pprec_skip: pprec (dx::◊) ◊ . -interpretation "'precedes' on redex pointers" - 'prec p q = (rpprec p q). +interpretation "'precedes' on pointers" + 'prec p q = (pprec p q). (* Note: this should go to core_notation *) notation "hvbox(a break ≺ b)" @@ -48,29 +34,29 @@ notation "hvbox(a break ≺ b)" for @{ 'prec $a $b }. (* Note: this is p < q *) -definition rplt: relation rptr ≝ TC … rpprec. +definition plt: relation ptr ≝ TC … pprec. interpretation "'less than' on redex pointers" - 'lt p q = (rplt p q). + 'lt p q = (plt p q). (* Note: this is p ≤ q *) -definition rple: relation rptr ≝ star … rpprec. +definition ple: relation ptr ≝ star … pprec. interpretation "'less or equal to' on redex pointers" - 'leq p q = (rple p q). + 'leq p q = (ple p q). -lemma rpprec_rple: ∀p,q. p ≺ q → p ≤ q. +lemma pprec_ple: ∀p,q. p ≺ q → p ≤ q. /2 width=1/ qed. -lemma rple_false: false::◊ ≤ ◊. +lemma ple_dx: dx::◊ ≤ ◊. /2 width=1/ qed. -lemma rple_nil: ∀p. ◊ ≤ p. +lemma ple_nil: ∀p. ◊ ≤ p. * // /2 width=1/ qed. -lemma rple_comp: ∀p1,p2. p1 ≤ p2 → ∀b. (b::p1) ≤ (b::p2). +lemma ple_comp: ∀p1,p2. p1 ≤ p2 → ∀c. (c::p1) ≤ (c::p2). #p1 #p2 #H elim H -p2 // /3 width=3/ qed. diff --git a/matita/matita/contribs/lambda/redex_pointer_sequence.ma b/matita/matita/contribs/lambda/pointer_sequence.ma similarity index 69% rename from matita/matita/contribs/lambda/redex_pointer_sequence.ma rename to matita/matita/contribs/lambda/pointer_sequence.ma index 43b7aa1d4..131711426 100644 --- a/matita/matita/contribs/lambda/redex_pointer_sequence.ma +++ b/matita/matita/contribs/lambda/pointer_sequence.ma @@ -12,22 +12,15 @@ (* *) (**************************************************************************) -include "redex_pointer.ma". +include "pointer_order.ma". -(* REDEX POINTER SEQUENCE ***************************************************) +(* POINTER SEQUENCE *********************************************************) (* Policy: pointer sequence metavariables: r, s *) +definition pseq: Type[0] ≝ list ptr. -definition rpseq: Type[0] \def list rptr. - -(* Note: a "spine" computation contracts just redexes in the spine *) -definition is_spine: predicate rpseq ≝ λs. - All … in_spine s. +(* Note: a "head" computation contracts just redexes in the head *) +definition is_head: predicate pseq ≝ All … in_head. (* Note: to us, a "normal" computation contracts redexes in non-decreasing positions *) -definition is_le: predicate rpseq ≝ λs. - Allr … rple s. - -(* Note: a normal spine computation *) -definition is_spine_le: predicate rpseq ≝ λs. - is_spine s ∧ is_le s. +definition is_le: predicate pseq ≝ Allr … ple. diff --git a/matita/matita/contribs/lambda/policy.txt b/matita/matita/contribs/lambda/policy.txt index 9f74e2339..ef8c96fce 100644 --- a/matita/matita/contribs/lambda/policy.txt +++ b/matita/matita/contribs/lambda/policy.txt @@ -7,13 +7,13 @@ M, N : term R : arbitrary relation T, U : arbitrary small type -a, b : boolean +c : pointer step d, e : variable reference depth h : relocation height i, j : de Bruijn index k : relocation height l : arbitrary list m, n : measures on terms -p, q : redex pointer -r, s : redex pointer sequence +p, q : pointer +r, s : pointer sequence t, u : arbitrary element diff --git a/matita/matita/contribs/lambda/preamble.ma b/matita/matita/contribs/lambda/preamble.ma index c272595a2..640615d59 100644 --- a/matita/matita/contribs/lambda/preamble.ma +++ b/matita/matita/contribs/lambda/preamble.ma @@ -13,7 +13,7 @@ (**************************************************************************) include "basics/star.ma". -include "basics/lists/list.ma". +include "basics/lists/lstar.ma". include "arithmetics/exp.ma". include "xoa_notation.ma". @@ -38,11 +38,6 @@ definition confluent1: ∀A. relation A → predicate A ≝ λA,R,a0. definition confluent: ∀A. predicate (relation A) ≝ λA,R. ∀a0. confluent1 … R a0. -(* booleans *) - -definition is_false: predicate bool ≝ λb. - false = b. - (* arithmetics *) lemma lt_refl_false: ∀n. n < n → ⊥. @@ -96,3 +91,12 @@ qed. notation > "◊" non associative with precedence 90 for @{'nil}. + +definition map_cons: ∀A. A → list (list A) → list (list A) ≝ λA,a. + map … (cons … a). + +interpretation "map_cons" 'ho_cons a l = (map_cons ? a l). + +notation "hvbox(a ::: break l)" + right associative with precedence 47 + for @{'ho_cons $a $l}. diff --git a/matita/matita/contribs/lambda/st_computation.ma b/matita/matita/contribs/lambda/st_computation.ma index fc7667a40..c9f9aa947 100644 --- a/matita/matita/contribs/lambda/st_computation.ma +++ b/matita/matita/contribs/lambda/st_computation.ma @@ -21,7 +21,7 @@ include "labelled_hap_computation.ma". *) inductive st: relation term ≝ | st_vref: ∀s,M,i. lhap s M (#i) → st M (#i) -| st_abst: ∀s,M,A,C. lhap s M (𝛌.A) → st A C → st M (𝛌.C) -| st_appl: ∀s,M,B,D,A,C. lhap s M (@B.A) → st B D → st A C → st M (@D.C) +| st_abst: ∀s,M,A1,A2. lhap s M (𝛌.A1) → st A1 A2 → st M (𝛌.A2) +| st_appl: ∀s,M,B1,B2,A1,A2. lhap s M (@B1.A1) → st B1 B2 → st A1 A2 → st M (@B2.A2) . diff --git a/matita/matita/contribs/lambda/xoa.conf.xml b/matita/matita/contribs/lambda/xoa.conf.xml index 4d8185190..f6a3e9d8d 100644 --- a/matita/matita/contribs/lambda/xoa.conf.xml +++ b/matita/matita/contribs/lambda/xoa.conf.xml @@ -8,8 +8,10 @@ xoa xoa_notation basics/pts.ma - 3 1 + 2 2 + 3 1 3 2 + 3 3 4 3 3 diff --git a/matita/matita/contribs/lambda/xoa.ma b/matita/matita/contribs/lambda/xoa.ma index 5529e4560..9d4ee880b 100644 --- a/matita/matita/contribs/lambda/xoa.ma +++ b/matita/matita/contribs/lambda/xoa.ma @@ -16,6 +16,14 @@ include "basics/pts.ma". +(* multiple existental quantifier (2, 2) *) + +inductive ex2_2 (A0,A1:Type[0]) (P0,P1:A0→A1→Prop) : Prop ≝ + | ex2_2_intro: ∀x0,x1. P0 x0 x1 → P1 x0 x1 → ex2_2 ? ? ? ? +. + +interpretation "multiple existental quantifier (2, 2)" 'Ex P0 P1 = (ex2_2 ? ? P0 P1). + (* multiple existental quantifier (3, 1) *) inductive ex3_1 (A0:Type[0]) (P0,P1,P2:A0→Prop) : Prop ≝ @@ -32,6 +40,14 @@ inductive ex3_2 (A0,A1:Type[0]) (P0,P1,P2:A0→A1→Prop) : Prop ≝ interpretation "multiple existental quantifier (3, 2)" 'Ex P0 P1 P2 = (ex3_2 ? ? P0 P1 P2). +(* multiple existental quantifier (3, 3) *) + +inductive ex3_3 (A0,A1,A2:Type[0]) (P0,P1,P2:A0→A1→A2→Prop) : Prop ≝ + | ex3_3_intro: ∀x0,x1,x2. P0 x0 x1 x2 → P1 x0 x1 x2 → P2 x0 x1 x2 → ex3_3 ? ? ? ? ? ? +. + +interpretation "multiple existental quantifier (3, 3)" 'Ex P0 P1 P2 = (ex3_3 ? ? ? P0 P1 P2). + (* multiple existental quantifier (4, 3) *) inductive ex4_3 (A0,A1,A2:Type[0]) (P0,P1,P2,P3:A0→A1→A2→Prop) : Prop ≝ diff --git a/matita/matita/contribs/lambda/xoa_notation.ma b/matita/matita/contribs/lambda/xoa_notation.ma index fbb7ca5fa..6151aa044 100644 --- a/matita/matita/contribs/lambda/xoa_notation.ma +++ b/matita/matita/contribs/lambda/xoa_notation.ma @@ -14,6 +14,16 @@ (* This file was generated by xoa.native: do not edit *********************) +(* multiple existental quantifier (2, 2) *) + +notation > "hvbox(∃∃ ident x0 , ident x1 break . term 19 P0 break & term 19 P1)" + non associative with precedence 20 + for @{ 'Ex (λ${ident x0}.λ${ident x1}.$P0) (λ${ident x0}.λ${ident x1}.$P1) }. + +notation < "hvbox(∃∃ ident x0 , ident x1 break . term 19 P0 break & term 19 P1)" + non associative with precedence 20 + for @{ 'Ex (λ${ident x0}:$T0.λ${ident x1}:$T1.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.$P1) }. + (* multiple existental quantifier (3, 1) *) notation > "hvbox(∃∃ ident x0 break . term 19 P0 break & term 19 P1 break & term 19 P2)" @@ -34,6 +44,16 @@ notation < "hvbox(∃∃ ident x0 , ident x1 break . term 19 P0 break & term 19 non associative with precedence 20 for @{ 'Ex (λ${ident x0}:$T0.λ${ident x1}:$T1.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.$P1) (λ${ident x0}:$T0.λ${ident x1}:$T1.$P2) }. +(* multiple existental quantifier (3, 3) *) + +notation > "hvbox(∃∃ ident x0 , ident x1 , ident x2 break . term 19 P0 break & term 19 P1 break & term 19 P2)" + non associative with precedence 20 + for @{ 'Ex (λ${ident x0}.λ${ident x1}.λ${ident x2}.$P0) (λ${ident x0}.λ${ident x1}.λ${ident x2}.$P1) (λ${ident x0}.λ${ident x1}.λ${ident x2}.$P2) }. + +notation < "hvbox(∃∃ ident x0 , ident x1 , ident x2 break . term 19 P0 break & term 19 P1 break & term 19 P2)" + non associative with precedence 20 + for @{ 'Ex (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P1) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P2) }. + (* multiple existental quantifier (4, 3) *) notation > "hvbox(∃∃ ident x0 , ident x1 , ident x2 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3)" -- 2.39.2