From: Ferruccio Guidi Date: Wed, 19 Dec 2012 15:52:59 +0000 (+0000) Subject: we simplified our proof of standardization X-Git-Tag: make_still_working~1382 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=0f7cb2f3a7b1b46a049d371bb40eb5a79881f064;p=helm.git we simplified our proof of standardization by removing Kashima's "hap" computation --- diff --git a/matita/matita/contribs/lambda/labelled_hap_computation.ma b/matita/matita/contribs/lambda/labelled_hap_computation.ma deleted file mode 100644 index 9eca7e7ef..000000000 --- a/matita/matita/contribs/lambda/labelled_hap_computation.ma +++ /dev/null @@ -1,99 +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 "labelled_sequential_computation.ma". -include "labelled_hap_reduction.ma". - -(* KASHIMA'S "HAP" COMPUTATION (LABELLED MULTISTEP) *************************) - -(* Note: this is the "head in application" computation of: - R. Kashima: "A proof of the Standization Theorem in λ-Calculus". Typescript note, (2000). -*) -definition lhap: pseq → relation term ≝ lstar … lhap1. - -interpretation "labelled 'hap' computation" - 'HApStar M p N = (lhap p M N). - -notation "hvbox( M break ⓗ↦* [ term 46 p ] break term 46 N )" - non associative with precedence 45 - for @{ 'HApStar $M $p $N }. - -lemma lhap_step_rc: ∀p,M1,M2. M1 ⓗ↦[p] M2 → M1 ⓗ↦*[p::◊] M2. -/2 width=1/ -qed. - -lemma lhap_inv_nil: ∀s,M1,M2. M1 ⓗ↦*[s] M2 → ◊ = s → M1 = M2. -/2 width=5 by lstar_inv_nil/ -qed-. - -lemma lhap_inv_cons: ∀s,M1,M2. M1 ⓗ↦*[s] M2 → ∀q,r. q::r = s → - ∃∃M. M1 ⓗ↦[q] M & M ⓗ↦*[r] M2. -/2 width=3 by lstar_inv_cons/ -qed-. - -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. - -lemma lhap_lift: ∀s. liftable (lhap s). -/2 width=1/ -qed. - -lemma lhap_inv_lift: ∀s. deliftable_sn (lhap s). -/3 width=3 by lstar_deliftable_sn, lhap1_inv_lift/ -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: ltransitive … lhap. -/2 width=3 by lstar_ltransitive/ -qed-. - -lemma lhap_step_dx: ∀s,M1,M. M1 ⓗ↦*[s] M → - ∀p,M2. M ⓗ↦[p] M2 → M1 ⓗ↦*[s@p::◊] M2. -#s #M1 #M #HM1 #p #M2 #HM2 -@(lhap_trans … HM1) /2 width=1/ -qed-. - -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_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-. diff --git a/matita/matita/contribs/lambda/labelled_hap_reduction.ma b/matita/matita/contribs/lambda/labelled_hap_reduction.ma deleted file mode 100644 index 6d08b8c5c..000000000 --- a/matita/matita/contribs/lambda/labelled_hap_reduction.ma +++ /dev/null @@ -1,96 +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 "labelled_sequential_reduction.ma". - -(* KASHIMA'S "HAP" COMPUTATION (LABELLED SINGLE STEP) ***********************) - -(* 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: ptr → relation term ≝ -| hap1_beta: ∀B,A. lhap1 (◊) (@B.𝛌.A) ([↙B]A) -| hap1_appl: ∀p,B,A1,A2. lhap1 p A1 A2 → lhap1 (dx::p) (@B.A1) (@B.A2) -. - -interpretation "labelled 'hap' reduction" - 'HAp M p N = (lhap1 p M N). - -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_lift: ∀p. liftable (lhap1 p). -#p #h #M1 #M2 #H elim H -p -M1 -M2 normalize /2 width=1/ -#B #A #d dsubst_dsubst_ge // -qed. - -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_inv_lsred: ∀p,M,N. M ⓗ↦[p] N → M ↦[p] N. -#p #M #N #H elim H -p -M -N // /2 width=1/ -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/pointer_sequence.ma b/matita/matita/contribs/lambda/pointer_sequence.ma index 0a3d3422c..fa153ccd4 100644 --- a/matita/matita/contribs/lambda/pointer_sequence.ma +++ b/matita/matita/contribs/lambda/pointer_sequence.ma @@ -22,6 +22,16 @@ definition pseq: Type[0] ≝ list ptr. (* Note: a "head" computation contracts just redexes in the head *) definition is_head: predicate pseq ≝ All … in_head. +lemma is_head_dx: ∀s. is_head s → is_head (dx:::s). +#s elim s -s // +#p #s #IHs * /3 width=1/ +qed. + +lemma is_head_append: ∀r. is_head r → ∀s. is_head s → is_head (r@s). +#r elim r -r // +#q #r #IHr * /3 width=1/ +qed. + (* Note: to us, a "normal" computation contracts redexes in non-decreasing positions *) definition is_le: predicate pseq ≝ Allr … ple. diff --git a/matita/matita/contribs/lambda/st_computation.ma b/matita/matita/contribs/lambda/st_computation.ma index cce418715..61f32a37b 100644 --- a/matita/matita/contribs/lambda/st_computation.ma +++ b/matita/matita/contribs/lambda/st_computation.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "labelled_hap_computation.ma". +include "labelled_sequential_computation.ma". (* KASHIMA'S "ST" COMPUTATION ***********************************************) @@ -20,9 +20,9 @@ include "labelled_hap_computation.ma". R. Kashima: "A proof of the Standization Theorem in λ-Calculus". Typescript note, (2000). *) inductive st: relation term ≝ -| st_vref: ∀s,M,i. M ⓗ↦*[s] #i → st M (#i) -| st_abst: ∀s,M,A1,A2. M ⓗ↦*[s] 𝛌.A1 → st A1 A2 → st M (𝛌.A2) -| st_appl: ∀s,M,B1,B2,A1,A2. M ⓗ↦*[s] @B1.A1 → st B1 B2 → st A1 A2 → st M (@B2.A2) +| st_vref: ∀s,M,i. is_head s → M ↦*[s] #i → st M (#i) +| st_abst: ∀s,M,A1,A2. is_head s → M ↦*[s] 𝛌.A1 → st A1 A2 → st M (𝛌.A2) +| st_appl: ∀s,M,B1,B2,A1,A2. is_head s → M ↦*[s] @B1.A1 → st B1 B2 → st A1 A2 → st M (@B2.A2) . interpretation "'st' computation" @@ -33,111 +33,105 @@ notation "hvbox( M ⓢ⤇* break term 46 N )" for @{ 'Std $M $N }. lemma st_inv_lref: ∀M,N. M ⓢ⤇* N → ∀j. #j = N → - ∃s. M ⓗ↦*[s] #j. + ∃∃s. is_head s & M ↦*[s] #j. #M #N * -M -N -[ /2 width=2/ -| #s #M #A1 #A2 #_ #_ #j #H destruct -| #s #M #B1 #B2 #A1 #A2 #_ #_ #_ #j #H destruct +[ /2 width=3/ +| #s #M #A1 #A2 #_ #_ #_ #j #H destruct +| #s #M #B1 #B2 #A1 #A2 #_ #_ #_ #_ #j #H destruct ] qed-. lemma st_inv_abst: ∀M,N. M ⓢ⤇* N → ∀C2. 𝛌.C2 = N → - ∃∃s,C1. M ⓗ↦*[s] 𝛌.C1 & C1 ⓢ⤇* C2. + ∃∃s,C1. is_head s & M ↦*[s] 𝛌.C1 & C1 ⓢ⤇* C2. #M #N * -M -N -[ #s #M #i #_ #C2 #H destruct -| #s #M #A1 #A2 #HM #A12 #C2 #H destruct /2 width=4/ -| #s #M #B1 #B2 #A1 #A2 #_ #_ #_ #C2 #H destruct +[ #s #M #i #_ #_ #C2 #H destruct +| #s #M #A1 #A2 #Hs #HM #A12 #C2 #H destruct /2 width=5/ +| #s #M #B1 #B2 #A1 #A2 #_ #_ #_ #_ #C2 #H destruct ] qed-. lemma st_inv_appl: ∀M,N. M ⓢ⤇* N → ∀D2,C2. @D2.C2 = N → - ∃∃s,D1,C1. M ⓗ↦*[s] @D1.C1 & D1 ⓢ⤇* D2 & C1 ⓢ⤇* C2. + ∃∃s,D1,C1. is_head s & M ↦*[s] @D1.C1 & D1 ⓢ⤇* D2 & C1 ⓢ⤇* C2. #M #N * -M -N -[ #s #M #i #_ #D2 #C2 #H destruct -| #s #M #A1 #A2 #_ #_ #D2 #C2 #H destruct -| #s #M #B1 #B2 #A1 #A2 #HM #HB12 #HA12 #D2 #C2 #H destruct /2 width=6/ +[ #s #M #i #_ #_ #D2 #C2 #H destruct +| #s #M #A1 #A2 #_ #_ #_ #D2 #C2 #H destruct +| #s #M #B1 #B2 #A1 #A2 #Hs #HM #HB12 #HA12 #D2 #C2 #H destruct /2 width=7/ ] qed-. lemma st_refl: reflexive … st. -#M elim M -M /2 width=2/ /2 width=4/ /2 width=6/ +#M elim M -M /2 width=3/ /2 width=5/ /2 width=7/ qed. -lemma st_step_sn: ∀N1,N2. N1 ⓢ⤇* N2 → ∀s,M. M ⓗ↦*[s] N1 → M ⓢ⤇* N2. +lemma st_step_sn: ∀N1,N2. N1 ⓢ⤇* N2 → ∀s,M. is_head s → M ↦*[s] N1 → M ⓢ⤇* N2. #N1 #N2 #H elim H -N1 -N2 -[ #r #N #i #HN #s #M #HMN - lapply (lhap_trans … HMN … HN) -N /2 width=2/ -| #r #N #C1 #C2 #HN #_ #IHC12 #s #M #HMN - lapply (lhap_trans … HMN … HN) -N /3 width=5/ -| #r #N #D1 #D2 #C1 #C2 #HN #_ #_ #IHD12 #IHC12 #s #M #HMN - lapply (lhap_trans … HMN … HN) -N /3 width=7/ +[ #r #N #i #Hr #HN #s #M #Hs #HMN + lapply (lsreds_trans … HMN … HN) -N /3 width=3/ +| #r #N #C1 #C2 #Hr #HN #_ #IHC12 #s #M #Hs #HMN + lapply (lsreds_trans … HMN … HN) -N /3 width=7/ +| #r #N #D1 #D2 #C1 #C2 #Hr #HN #_ #_ #IHD12 #IHC12 #s #M #Hs #HMN + lapply (lsreds_trans … HMN … HN) -N /3 width=9/ ] qed-. -lemma st_step_rc: ∀s,M1,M2. M1 ⓗ↦*[s] M2 → M1 ⓢ⤇* M2. -/3 width=4 by st_step_sn/ +lemma st_step_rc: ∀s,M1,M2. is_head s → M1 ↦*[s] M2 → M1 ⓢ⤇* M2. +/3 width=5 by st_step_sn/ qed. lemma st_lift: liftable st. #h #M1 #M2 #H elim H -M1 -M2 -[ /3 width=2/ -| #s #M #A1 #A2 #HM #_ #IHA12 #d - @st_abst [3: @(lhap_lift … HM) |1,2: skip ] -M // (**) (* auto fails here *) -| #s #M #B1 #B2 #A1 #A2 #HM #_ #_ #IHB12 #IHA12 #d - @st_appl [4: @(lhap_lift … HM) |1,2,3: skip ] -M // (**) (* auto fails here *) +[ /3 width=3/ +| #s #M #A1 #A2 #Hs #HM #_ #IHA12 #d + @(st_abst … Hs) [2: @(lsreds_lift … HM) | skip ] -M // (**) (* auto fails here *) +| #s #M #B1 #B2 #A1 #A2 #Hs #HM #_ #_ #IHB12 #IHA12 #d + @(st_appl … Hs) [3: @(lsreds_lift … HM) |1,2: skip ] -M // (**) (* auto fails here *) ] qed. lemma st_inv_lift: deliftable_sn st. #h #N1 #N2 #H elim H -N1 -N2 -[ #s #N1 #i #HN1 #d #M1 #HMN1 - elim (lhap_inv_lift … HN1 … HMN1) -N1 /3 width=3/ -| #s #N1 #C1 #C2 #HN1 #_ #IHC12 #d #M1 #HMN1 - elim (lhap_inv_lift … HN1 … HMN1) -N1 #M2 #HM12 #HM2 +[ #s #N1 #i #Hs #HN1 #d #M1 #HMN1 + elim (lsreds_inv_lift … HN1 … HMN1) -N1 /3 width=3/ +| #s #N1 #C1 #C2 #Hs #HN1 #_ #IHC12 #d #M1 #HMN1 + elim (lsreds_inv_lift … HN1 … HMN1) -N1 #M2 #HM12 #HM2 elim (lift_inv_abst … HM2) -HM2 #A1 #HAC1 #HM2 destruct elim (IHC12 ???) -IHC12 [4: // |2,3: skip ] #A2 #HA12 #HAC2 destruct (**) (* simplify line *) - @(ex2_intro … (𝛌.A2)) // /2 width=4/ -| #s #N1 #D1 #D2 #C1 #C2 #HN1 #_ #_ #IHD12 #IHC12 #d #M1 #HMN1 - elim (lhap_inv_lift … HN1 … HMN1) -N1 #M2 #HM12 #HM2 + @(ex2_intro … (𝛌.A2)) // /2 width=5/ +| #s #N1 #D1 #D2 #C1 #C2 #Hs #HN1 #_ #_ #IHD12 #IHC12 #d #M1 #HMN1 + elim (lsreds_inv_lift … HN1 … HMN1) -N1 #M2 #HM12 #HM2 elim (lift_inv_appl … HM2) -HM2 #B1 #A1 #HBD1 #HAC1 #HM2 destruct elim (IHD12 ???) -IHD12 [4: // |2,3: skip ] #B2 #HB12 #HBD2 destruct (**) (* simplify line *) elim (IHC12 ???) -IHC12 [4: // |2,3: skip ] #A2 #HA12 #HAC2 destruct (**) (* simplify line *) - @(ex2_intro … (@B2.A2)) // /2 width=6/ + @(ex2_intro … (@B2.A2)) // /2 width=7/ ] qed-. lemma st_dsubst: dsubstable st. #N1 #N2 #HN12 #M1 #M2 #H elim H -M1 -M2 -[ #s #M #i #HM #d elim (lt_or_eq_or_gt i d) #Hid - [ lapply (lhap_dsubst … N1 … HM d) -HM - >(dsubst_vref_lt … Hid) >(dsubst_vref_lt … Hid) /2 width=2/ +[ #s #M #i #Hs #HM #d elim (lt_or_eq_or_gt i d) #Hid + [ lapply (lsreds_dsubst … N1 … HM d) -HM + >(dsubst_vref_lt … Hid) >(dsubst_vref_lt … Hid) /2 width=3/ | destruct >dsubst_vref_eq @(st_step_sn (↑[0,i]N1) … s) /2 width=1/ - | lapply (lhap_dsubst … N1 … HM d) -HM - >(dsubst_vref_gt … Hid) >(dsubst_vref_gt … Hid) /2 width=2/ + | lapply (lsreds_dsubst … N1 … HM d) -HM + >(dsubst_vref_gt … Hid) >(dsubst_vref_gt … Hid) /2 width=3/ ] -| #s #M #A1 #A2 #HM #_ #IHA12 #d - lapply (lhap_dsubst … N1 … HM d) -HM /2 width=4/ (**) (* auto needs some help here *) -| #s #M #B1 #B2 #A1 #A2 #HM #_ #_ #IHB12 #IHA12 #d - lapply (lhap_dsubst … N1 … HM d) -HM /2 width=6/ (**) (* auto needs some help here *) +| #s #M #A1 #A2 #Hs #HM #_ #IHA12 #d + lapply (lsreds_dsubst … N1 … HM d) -HM /2 width=5/ (**) (* auto needs some help here *) +| #s #M #B1 #B2 #A1 #A2 #Hs #HM #_ #_ #IHB12 #IHA12 #d + lapply (lsreds_dsubst … N1 … HM d) -HM /2 width=7/ (**) (* auto needs some help here *) ] qed. lemma st_inv_lsreds_is_le: ∀M,N. M ⓢ⤇* N → ∃∃r. M ↦*[r] N & is_le r. #M #N #H elim H -M -N -[ #s #M #i #H - lapply (lhap_inv_lsreds … H) - lapply (lhap_inv_head … H) -H #H - lapply (is_head_is_le … H) -H /2 width=3/ -| #s #M #A1 #A2 #H #_ * #r #HA12 #Hr - lapply (lhap_inv_lsreds … H) #HM - lapply (lhap_inv_head … H) -H #Hs +[ #s #M #i #Hs #HM + lapply (is_head_is_le … Hs) -Hs /2 width=3/ +| #s #M #A1 #A2 #Hs #HM #_ * #r #HA12 #Hr 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 - lapply (lhap_inv_head … H) -H #Hs +| #s #M #B1 #B2 #A1 #A2 #Hs #HM #_ #_ * #rb #HB12 #Hrb * #ra #HA12 #Hra lapply (lsreds_trans … HM (dx:::ra) (@B1.A2) ?) /2 width=1/ -A1 #HM lapply (lsreds_trans … HM (sn:::rb) (@B2.A2) ?) /2 width=1/ -B1 #HM @(ex2_intro … HM) -M -B2 -A2 >associative_append /3 width=1/ @@ -147,41 +141,48 @@ qed-. lemma st_step_dx: ∀p,M,M2. M ↦[p] M2 → ∀M1. M1 ⓢ⤇* M → M1 ⓢ⤇* M2. #p #M #M2 #H elim H -p -M -M2 [ #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 *) - 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/ + elim (st_inv_appl … H ???) -H [4: // |2,3: skip ] #s #B1 #M #Hs #HM1 #HB1 #H (**) (* simplify line *) + elim (st_inv_abst … H ??) -H [3: // |2: skip ] #r #A1 #Hr #HM #HA1 (**) (* simplify line *) + lapply (lsreds_trans … HM1 … (dx:::r) (@B1.𝛌.A1) ?) /2 width=1/ -M #HM1 + lapply (lsreds_step_dx … HM1 (◊) ([↙B1]A1) ?) -HM1 // #HM1 + @(st_step_sn … HM1) /2 width=1/ /4 width=1/ | #p #A #A2 #_ #IHA2 #M1 #H - elim (st_inv_abst … H ??) -H [3: // |2: skip ] /3 width=4/ (**) (* simplify line *) + elim (st_inv_abst … H ??) -H [3: // |2: skip ] /3 width=5/ (**) (* simplify line *) | #p #B #B2 #A #_ #IHB2 #M1 #H - elim (st_inv_appl … H ???) -H [4: // |2,3: skip ] /3 width=6/ (**) (* simplify line *) + elim (st_inv_appl … H ???) -H [4: // |2,3: skip ] /3 width=7/ (**) (* simplify line *) | #p #B #A #A2 #_ #IHA2 #M1 #H - elim (st_inv_appl … H ???) -H [4: // |2,3: skip ] /3 width=6/ (**) (* simplify line *) + elim (st_inv_appl … H ???) -H [4: // |2,3: skip ] /3 width=7/ (**) (* simplify line *) ] 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 +(* Note: we use "lapply (rewrite_r ?? is_head … Hq)" (procedural) + in place of "cut (is_head (q::r)) [ >Hq ]" (declarative) +*) +lemma st_lsred_swap: ∀p. in_head p → ∀N1,N2. N1 ↦[p] N2 → ∀M1. M1 ⓢ⤇* N1 → + ∃∃q,M2. in_head q & M1 ↦[q] M2 & M2 ⓢ⤇* N2. +#p #H @(in_head_ind … H) -p +[ #N1 #N2 #H1 #M1 #H2 + elim (lsred_inv_nil … H1 ?) -H1 // #D #C #HN1 #HN2 + elim (st_inv_appl … H2 … HN1) -N1 #s1 #D1 #N #Hs1 #HM1 #HD1 #H + elim (st_inv_abst … H ??) -H [3: // |2: skip ] #s2 #C1 #Hs2 #HN #HC1 (**) (* simplify line *) + lapply (lsreds_trans … HM1 … (dx:::s2) (@D1.𝛌.C1) ?) /2 width=1/ -N #HM1 + lapply (lsreds_step_dx … HM1 (◊) ([↙D1]C1) ?) -HM1 // #HM1 + elim (lsreds_inv_pos … HM1 ?) -HM1 [2: >length_append normalize in ⊢ (??(??%)); // ] - #q #r #M #_ #HM1 #HM -s - @(ex2_2_intro … HM1) -M1 + #q #r #M #Hq #HM1 #HM + lapply (rewrite_r ?? is_head … Hq) -Hq /4 width=1/ -s1 -s2 * #Hq #Hr + @(ex3_2_intro … HM1) -M1 // -q @(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 +| #p #_ #IHp #N1 #N2 #H1 #M1 #H2 + elim (lsred_inv_dx … H1 ??) -H1 [3: // |2: skip ] #D #C1 #C2 #HC12 #HN1 #HN2 (**) (* simplify line *) + elim (st_inv_appl … H2 … HN1) -N1 #s #B #A1 #Hs #HM1 #HBD #HAC1 + elim (IHp … HC12 … HAC1) -p -C1 #p #C1 #Hp #HAC1 #HC12 + lapply (lsreds_step_dx … HM1 (dx::p) (@B.C1) ?) -HM1 /2 width=1/ -A1 #HM1 + elim (lsreds_inv_pos … HM1 ?) -HM1 [2: >length_append normalize in ⊢ (??(??%)); // ] - #q #r #M #_ #HM1 #HM -p -s - @(ex2_2_intro … HM1) -M1 /2 width=6/ + #q #r #M #Hq #HM1 #HM + lapply (rewrite_r ?? is_head … Hq) -Hq /4 width=1/ -p -s * #Hq #Hr + @(ex3_2_intro … HM1) -M1 // -q /2 width=7/ ] qed-. @@ -196,17 +197,17 @@ elim (st_inv_lsreds_is_le … HM2) -HM2 #s2 #HM2 #_ lapply (lsreds_trans … HM1 … HM2) -M /2 width=2/ qed-. -theorem lsreds_standard: ∀s,M,N. M ↦*[s] N → - ∃∃r. M ↦*[r] N & is_le r. +theorem lsreds_standard: ∀s,M,N. M ↦*[s] N → ∃∃r. M ↦*[r] N & is_le r. #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 +theorem lsreds_lhap1_swap: ∀s,M1,N1. M1 ↦*[s] N1 → + ∀p,N2. in_head p → N1 ↦[p] N2 → + ∃∃q,r,M2. in_head q & M1 ↦[q] M2 & M2 ↦*[r] N2 & + is_le (q::r). +#s #M1 #N1 #HMN1 #p #N2 #Hp #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/ +elim (st_lsred_swap … Hp … HN12 … HMN1) -p -N1 #q #M2 #Hq #HM12 #HMN2 +elim (st_inv_lsreds_is_le … HMN2) -HMN2 /3 width=8/ qed-.