From 1e8607eee93cec71e1d4d3bb93e321a460f59cec Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Tue, 11 Dec 2012 19:15:02 +0000 Subject: [PATCH] - pointer structure simplified - new properties on poiner orders - last lemma in Kashima's article proved --- .../lambda/labelled_hap_computation.ma | 5 +++ .../lambda/labelled_sequential_computation.ma | 5 +++ .../lambda/labelled_sequential_reduction.ma | 27 ++++++------ matita/matita/contribs/lambda/pointer.ma | 11 +++-- .../matita/contribs/lambda/pointer_order.ma | 38 +++++++++++++++-- .../contribs/lambda/pointer_sequence.ma | 2 +- matita/matita/contribs/lambda/preamble.ma | 11 +++++ .../matita/contribs/lambda/st_computation.ma | 41 +++++++++++++++++-- 8 files changed, 114 insertions(+), 26 deletions(-) diff --git a/matita/matita/contribs/lambda/labelled_hap_computation.ma b/matita/matita/contribs/lambda/labelled_hap_computation.ma index 6309d6b53..4441961e1 100644 --- a/matita/matita/contribs/lambda/labelled_hap_computation.ma +++ b/matita/matita/contribs/lambda/labelled_hap_computation.ma @@ -46,6 +46,11 @@ lemma lhap_inv_step_rc: ∀p,M1,M2. M1 ⓗ⇀*[p::◊] M2 → M1 ⓗ⇀[p] M2. /2 width=1 by lstar_inv_step/ qed-. +lemma lhap_inv_pos: ∀s,M1,M2. M1 ⓗ⇀*[s] M2 → 0 < |s| → + ∃∃p,r,M. p::r = s & M1 ⓗ⇀[p] M & M ⓗ⇀*[r] M2. +/2 width=1 by lstar_inv_pos/ +qed-. + lemma lhap_compatible_dx: ho_compatible_dx lhap. /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 4a7392a76..a609078fe 100644 --- a/matita/matita/contribs/lambda/labelled_sequential_computation.ma +++ b/matita/matita/contribs/lambda/labelled_sequential_computation.ma @@ -43,6 +43,11 @@ lemma lsreds_inv_step_rc: ∀p,M1,M2. M1 ⇀*[p::◊] M2 → M1 ⇀[p] M2. /2 width=1 by lstar_inv_step/ qed-. +lemma lsreds_inv_pos: ∀s,M1,M2. M1 ⇀*[s] M2 → 0 < |s| → + ∃∃p,r,M. p::r = s & M1 ⇀[p] M & M ⇀*[r] M2. +/2 width=1 by lstar_inv_pos/ +qed-. + lemma lsred_compatible_rc: ho_compatible_rc lsreds. /3 width=1/ qed. diff --git a/matita/matita/contribs/lambda/labelled_sequential_reduction.ma b/matita/matita/contribs/lambda/labelled_sequential_reduction.ma index 21d24c668..0c75f86e2 100644 --- a/matita/matita/contribs/lambda/labelled_sequential_reduction.ma +++ b/matita/matita/contribs/lambda/labelled_sequential_reduction.ma @@ -23,7 +23,7 @@ include "multiplicity.ma". *) inductive lsred: ptr → relation term ≝ | lsred_beta : ∀B,A. lsred (◊) (@B.𝛌.A) ([⬐B]A) -| lsred_abst : ∀p,A1,A2. lsred p A1 A2 → lsred (rc::p) (𝛌.A1) (𝛌.A2) +| lsred_abst : ∀p,A1,A2. lsred p A1 A2 → lsred (sn::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) . @@ -55,22 +55,13 @@ lemma lsred_inv_nil: ∀p,M,N. M ⇀[p] N → ◊ = p → ] qed-. -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 #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_sn: ∀p,M,N. M ⇀[p] N → ∀q. sn::q = p → + (∃∃A1,A2. A1 ⇀[q] A2 & 𝛌.A1 = M & 𝛌.A2 = N) ∨ ∃∃B1,B2,A. B1 ⇀[q] B2 & @B1.A = M & @B2.A = N. #p #M #N * -p -M -N [ #B #A #q #H destruct -| #p #A1 #A2 #_ #q #H destruct -| #p #B1 #B2 #A #HB12 #q #H destruct /2 width=6/ +| #p #A1 #A2 #HA12 #q #H destruct /3 width=5/ +| #p #B1 #B2 #A #HB12 #q #H destruct /3 width=6/ | #p #B #A1 #A2 #_ #q #H destruct ] qed-. @@ -132,8 +123,14 @@ qed. theorem lsred_mono: ∀p. singlevalued … (lsred p). #p #M #N1 #H elim H -p -M -N1 [ #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 #A1 #A2 #_ #IHA12 #N2 #H elim (lsred_inv_sn … H ??) -H [4: // |2: skip ] * (**) (* simplify line *) + [ #C1 #C2 #HC12 #H #HN2 destruct /3 width=1/ + | #D1 #D2 #C #_ #H destruct + ] +| #p #B1 #B2 #A #_ #IHB12 #N2 #H elim (lsred_inv_sn … H ??) -H [4: // |2: skip ] * (**) (* simplify line *) + [ #C1 #C2 #_ #H destruct + | #D1 #D2 #C #HD12 #H #HN2 destruct /3 width=1/ + ] | #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/pointer.ma b/matita/matita/contribs/lambda/pointer.ma index 74977c390..30b4fdf64 100644 --- a/matita/matita/contribs/lambda/pointer.ma +++ b/matita/matita/contribs/lambda/pointer.ma @@ -18,12 +18,17 @@ include "term.ma". (* 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 + rc (rectus) : not needed (we use sn instead) sn (sinister): proceed on the left argument of an application + or on the argument of an abstraction (this would be rc) dx (dexter) : proceed on the right argument of an application *) +(* Remark: the following breaks destruct because of δ-expansions + definition ptr_step: Type[0] ≝ bool. + definition sn: bool ≝ true. + definition dx: bool ≝ false. +*) inductive ptr_step: Type[0] ≝ -| rc: ptr_step | sn: ptr_step | dx: ptr_step . @@ -45,7 +50,7 @@ lemma in_head_ind: ∀R:predicate ptr. R (◊) → qed-. definition compatible_rc: predicate (ptr→relation term) ≝ λR. - ∀p,A1,A2. R p A1 A2 → R (rc::p) (𝛌.A1) (𝛌.A2). + ∀p,A1,A2. R p A1 A2 → R (sn::p) (𝛌.A1) (𝛌.A2). definition compatible_sn: predicate (ptr→relation term) ≝ λR. ∀p,B1,B2,A. R p B1 B2 → R (sn::p) (@B1.A) (@B2.A). diff --git a/matita/matita/contribs/lambda/pointer_order.ma b/matita/matita/contribs/lambda/pointer_order.ma index ffd1e725d..24dcad4fa 100644 --- a/matita/matita/contribs/lambda/pointer_order.ma +++ b/matita/matita/contribs/lambda/pointer_order.ma @@ -20,8 +20,7 @@ include "pointer.ma". to serve as base for the order relations: p < q and p ≤ q *) inductive pprec: relation ptr ≝ | pprec_nil : ∀c,q. pprec (◊) (c::q) -| ppprc_rc : ∀p,q. pprec (dx::p) (rc::q) -| ppprc_sn : ∀p,q. pprec (dx::p) (sn::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::◊) ◊ . @@ -37,7 +36,6 @@ notation "hvbox(a break ≺ b)" lemma pprec_fwd_in_head: ∀p,q. p ≺ q → in_head q → in_head p. #p #q #H elim H -p -q // /2 width=1/ [ #p #q * #H destruct -| #p #q * #H destruct | #c #p #q #_ #IHpq * #H destruct /3 width=1/ ] qed-. @@ -48,6 +46,31 @@ definition plt: relation ptr ≝ TC … pprec. interpretation "'less than' on redex pointers" 'lt p q = (plt p q). +lemma plt_step_rc: ∀p,q. p ≺ q → p < q. +/2 width=1/ +qed. + +lemma plt_nil: ∀c,p. ◊ < c::p. +/2 width=1/ +qed. + +lemma plt_skip: dx::◊ < ◊. +/2 width=1/ +qed. + +lemma plt_comp: ∀c,p,q. p < q → c::p < c::q. +#c #p #q #H elim H -q /3 width=1/ /3 width=3/ +qed. + +theorem plt_trans: transitive … plt. +/2 width=3/ +qed-. + +lemma plt_refl: ∀p. p < p. +#p elim p -p /2 width=1/ +@(plt_trans … (dx::◊)) // +qed. + (* Note: this is p ≤ q *) definition ple: relation ptr ≝ star … pprec. @@ -83,6 +106,15 @@ lemma ple_skip_ple: ∀p. p ≤ ◊ → dx::p ≤ ◊. #p #q #Hpq #_ #H @(ple_step_sn … H) -H /2 width=1/ qed. +lemma ple_dichotomy: ∀p1,p2:ptr. p1 ≤ p2 ∨ p2 ≤ p1. +#p1 elim p1 -p1 +[ * /2 width=1/ +| #c1 #p1 #IHp1 * /2 width=1/ + * #p2 cases c1 -c1 /2 width=1/ + elim (IHp1 p2) -IHp1 /3 width=1/ +] +qed-. + lemma in_head_ple_nil: ∀p. in_head p → p ≤ ◊. #p #H @(in_head_ind … H) -p // /2 width=1/ qed. diff --git a/matita/matita/contribs/lambda/pointer_sequence.ma b/matita/matita/contribs/lambda/pointer_sequence.ma index 9f4e63cd6..0a3d3422c 100644 --- a/matita/matita/contribs/lambda/pointer_sequence.ma +++ b/matita/matita/contribs/lambda/pointer_sequence.ma @@ -57,7 +57,7 @@ theorem is_head_is_le_trans: ∀r. is_head r → ∀s. is_le s → is_le (r@s). qed. definition ho_compatible_rc: predicate (pseq→relation term) ≝ λR. - ∀s,A1,A2. R s A1 A2 → R (rc:::s) (𝛌.A1) (𝛌.A2). + ∀s,A1,A2. R s A1 A2 → R (sn:::s) (𝛌.A1) (𝛌.A2). definition ho_compatible_sn: predicate (pseq→relation term) ≝ λR. ∀s,B1,B2,A. R s B1 B2 → R (sn:::s) (@B1.A) (@B2.A). diff --git a/matita/matita/contribs/lambda/preamble.ma b/matita/matita/contribs/lambda/preamble.ma index 640615d59..958f1059a 100644 --- a/matita/matita/contribs/lambda/preamble.ma +++ b/matita/matita/contribs/lambda/preamble.ma @@ -100,3 +100,14 @@ 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}. + +(* lstar *) + +(* Note: this cannot be in lib because of the missing xoa quantifier *) +lemma lstar_inv_pos: ∀A,B,R,l,b1,b2. lstar A B R l b1 b2 → 0 < |l| → + ∃∃a,ll,b. a::ll = l & R a b1 b & lstar A B R ll b b2. +#A #B #R #l #b1 #b2 #H @(lstar_ind_l ????????? H) -b1 +[ #H elim (lt_refl_false … H) +| #a #ll #b1 #b #Hb1 #Hb2 #_ #_ /2 width=6/ (**) (* auto fail if we do not remove the inductive premise *) +] +qed-. diff --git a/matita/matita/contribs/lambda/st_computation.ma b/matita/matita/contribs/lambda/st_computation.ma index b536bb3a3..75d72ed0c 100644 --- a/matita/matita/contribs/lambda/st_computation.ma +++ b/matita/matita/contribs/lambda/st_computation.ma @@ -133,7 +133,7 @@ lemma st_inv_lsreds_is_le: ∀M,N. M ⓢ⥤* N → | #s #M #A1 #A2 #H #_ * #r #HA12 #Hr lapply (lhap_inv_lsreds … H) #HM lapply (lhap_inv_head … H) -H #Hs - lapply (lsreds_trans … HM (rc:::r) (𝛌.A2) ?) /2 width=1/ -A1 #HM + lapply (lsreds_trans … HM (sn:::r) (𝛌.A2) ?) /2 width=1/ -A1 #HM @(ex2_intro … HM) -M -A2 /3 width=1/ | #s #M #B1 #B2 #A1 #A2 #H #_ #_ * #rb #HB12 #Hrb * #ra #HA12 #Hra lapply (lhap_inv_lsreds … H) #HM @@ -149,9 +149,9 @@ lemma st_step_dx: ∀p,M,M2. M ⇀[p] M2 → ∀M1. M1 ⓢ⥤* M → M1 ⓢ⥤* [ #B #A #M1 #H elim (st_inv_appl … H ???) -H [4: // |2,3: skip ] #s #B1 #M #HM1 #HB1 #H (**) (* simplify line *) elim (st_inv_abst … H ??) -H [3: // |2: skip ] #r #A1 #HM #HA1 (**) (* simplify line *) - @(st_step_sn … ([⬐B1]A1) … (s@(dx:::r)@(◊::◊))) /2 width=1/ -B -A - @(lhap_trans … HM1) -M1 - @(lhap_step_dx … (@B1.𝛌.A1)) // -s /2 width=1/ + lapply (lhap_trans … HM1 … (dx:::r) (@B1.𝛌.A1) ?) /2 width=1/ -M #HM1 + lapply (lhap_step_dx … HM1 (◊) ([⬐B1]A1) ?) -HM1 // #HM1 + @(st_step_sn … HM1) /2 width=1/ | #p #A #A2 #_ #IHA2 #M1 #H elim (st_inv_abst … H ??) -H [3: // |2: skip ] /3 width=4/ (**) (* simplify line *) | #p #B #B2 #A #_ #IHB2 #M1 #H @@ -161,6 +161,30 @@ lemma st_step_dx: ∀p,M,M2. M ⇀[p] M2 → ∀M1. M1 ⓢ⥤* M → M1 ⓢ⥤* ] qed-. +lemma st_lhap1_swap: ∀p,N1,N2. N1 ⓗ⇀[p] N2 → ∀M1. M1 ⓢ⥤* N1 → + ∃∃q,M2. M1 ⓗ⇀[q] M2 & M2 ⓢ⥤* N2. +#p #N1 #N2 #H elim H -p -N1 -N2 +[ #D #C #M1 #H + elim (st_inv_appl … H ???) -H [4: // |2,3: skip ] #s #D1 #N #HM1 #HD1 #H (**) (* simplify line *) + elim (st_inv_abst … H ??) -H [3: // |2: skip ] #r #C1 #HN #HC1 (**) (* simplify line *) + lapply (lhap_trans … HM1 … (dx:::r) (@D1.𝛌.C1) ?) /2 width=1/ -N #HM1 + lapply (lhap_step_dx … HM1 (◊) ([⬐D1]C1) ?) -HM1 // #HM1 + elim (lhap_inv_pos … HM1 ?) -HM1 + [2: >length_append normalize in ⊢ (??(??%)); // ] + #q #r #M #_ #HM1 #HM -s + @(ex2_2_intro … HM1) -M1 + @(st_step_sn … HM) /2 width=1/ +| #p #D #C1 #C2 #_ #IHC12 #M1 #H -p + elim (st_inv_appl … H ???) -H [4: // |2,3: skip ] #s #B #A1 #HM1 #HBD #HAC1 (**) (* simplify line *) + elim (IHC12 … HAC1) -C1 #p #C1 #HAC1 #HC12 + lapply (lhap_step_dx … HM1 (dx::p) (@B.C1) ?) -HM1 /2 width=1/ -A1 #HM1 + elim (lhap_inv_pos … HM1 ?) -HM1 + [2: >length_append normalize in ⊢ (??(??%)); // ] + #q #r #M #_ #HM1 #HM -p -s + @(ex2_2_intro … HM1) -M1 /2 width=6/ +] +qed-. + lemma st_lsreds: ∀s,M1,M2. M1 ⇀*[s] M2 → M1 ⓢ⥤* M2. #s #M1 #M2 #H @(lstar_ind_r ????????? H) -s -M2 // /2 width=4 by st_step_dx/ qed. @@ -177,3 +201,12 @@ theorem lsreds_standard: ∀s,M,N. M ⇀*[s] N → #s #M #N #H @st_inv_lsreds_is_le /2 width=2/ qed-. + +theorem lsreds_lhap1_swap: ∀s,M1,N1. M1 ⇀*[s] N1 → ∀p,N2. N1 ⓗ⇀[p] N2 → + ∃∃q,r,M2. M1 ⓗ⇀[q] M2 & M2 ⇀*[r] N2 & is_le (q::r). +#s #M1 #N1 #HMN1 #p #N2 #HN12 +lapply (st_lsreds … HMN1) -s #HMN1 +elim (st_lhap1_swap … HN12 … HMN1) -p -N1 #q #M2 #HM12 #HMN2 +elim (st_inv_lsreds_is_le … HMN2) -HMN2 #r #HMN2 #Hr +lapply (lhap1_inv_head … HM12) /3 width=7/ +qed-. -- 2.39.2