From: Ferruccio Guidi Date: Wed, 2 Jan 2013 22:12:53 +0000 (+0000) Subject: lambda: some refactoring + support for subsets of subterms started X-Git-Tag: make_still_working~1367 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=c821924472ab07f543c0e4acd0b808715de7a934;p=helm.git lambda: some refactoring + support for subsets of subterms started core_notation: some "term 19" added predefined_virtuals: an addition --- diff --git a/matita/matita/contribs/lambda/delifting_substitution.ma b/matita/matita/contribs/lambda/delifting_substitution.ma deleted file mode 100644 index fe45c35a2..000000000 --- a/matita/matita/contribs/lambda/delifting_substitution.ma +++ /dev/null @@ -1,163 +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 "lift.ma". - -(* DELIFTING SUBSTITUTION ***************************************************) - -(* Policy: depth (level) metavariables: d, e (as for lift) *) -let rec dsubst D d M on M ≝ match M with -[ VRef i ⇒ tri … i d (#i) (↑[i] D) (#(i-1)) -| Abst A ⇒ 𝛌. (dsubst D (d+1) A) -| Appl B A ⇒ @ (dsubst D d B). (dsubst D d A) -]. - -interpretation "delifting substitution" - 'DSubst D d M = (dsubst D d M). - -(* Note: the notation with "/" does not work *) -notation "hvbox( [ term 46 d ↙ break term 46 D ] break term 46 M )" - non associative with precedence 46 - for @{ 'DSubst $D $d $M }. - -notation > "hvbox( [ ↙ term 46 D ] break term 46 M )" - non associative with precedence 46 - for @{ 'DSubst $D 0 $M }. - -lemma dsubst_vref_lt: ∀i,d,D. i < d → [d ↙ D] #i = #i. -normalize /2 width=1/ -qed. - -lemma dsubst_vref_eq: ∀i,D. [i ↙ D] #i = ↑[i]D. -normalize // -qed. - -lemma dsubst_vref_gt: ∀i,d,D. d < i → [d ↙ D] #i = #(i-1). -normalize /2 width=1/ -qed. - -theorem dsubst_lift_le: ∀h,D,M,d1,d2. d2 ≤ d1 → - [d2 ↙ ↑[d1 - d2, h] D] ↑[d1 + 1, h] M = ↑[d1, h] [d2 ↙ D] M. -#h #D #M elim M -M -[ #i #d1 #d2 #Hd21 elim (lt_or_eq_or_gt i d2) #Hid2 - [ lapply (lt_to_le_to_lt … Hid2 Hd21) -Hd21 #Hid1 - >(dsubst_vref_lt … Hid2) >(lift_vref_lt … Hid1) >lift_vref_lt /2 width=1/ - | destruct >dsubst_vref_eq >lift_vref_lt /2 width=1/ - | >(dsubst_vref_gt … Hid2) -Hd21 elim (lt_or_ge (i-1) d1) #Hi1d1 - [ >(lift_vref_lt … Hi1d1) >lift_vref_lt /2 width=1/ - | lapply (ltn_to_ltO … Hid2) #Hi - >(lift_vref_ge … Hi1d1) >lift_vref_ge /2 width=1/ -Hi1d1 >plus_minus // /3 width=1/ - ] - ] -| normalize #A #IHA #d1 #d2 #Hd21 - lapply (IHA (d1+1) (d2+1) ?) -IHA /2 width=1/ -| normalize #B #A #IHB #IHA #d1 #d2 #Hd21 - >IHB -IHB // >IHA -IHA // -] -qed. - -theorem dsubst_lift_be: ∀h,D,M,d1,d2. d1 ≤ d2 → d2 ≤ d1 + h → - [d2 ↙ D] ↑[d1, h + 1] M = ↑[d1, h] M. -#h #D #M elim M -M -[ #i #d1 #d2 #Hd12 #Hd21 elim (lt_or_ge i d1) #Hid1 - [ lapply (lt_to_le_to_lt … Hid1 Hd12) -Hd12 -Hd21 #Hid2 - >(lift_vref_lt … Hid1) >(lift_vref_lt … Hid1) /2 width=1/ - | lapply (transitive_le … (i+h) Hd21 ?) -Hd12 -Hd21 /2 width=1/ #Hd2 - >(lift_vref_ge … Hid1) >(lift_vref_ge … Hid1) -Hid1 - >dsubst_vref_gt // /2 width=1/ - ] -| normalize #A #IHA #d1 #d2 #Hd12 #Hd21 - >IHA -IHA // /2 width=1/ -| normalize #B #A #IHB #IHA #d1 #d2 #Hd12 #Hd21 - >IHB -IHB // >IHA -IHA // -] -qed. - -theorem dsubst_lift_ge: ∀h,D,M,d1,d2. d1 + h ≤ d2 → - [d2 ↙ D] ↑[d1, h] M = ↑[d1, h] [d2 - h ↙ D] M. -#h #D #M elim M -M -[ #i #d1 #d2 #Hd12 elim (lt_or_eq_or_gt i (d2-h)) #Hid2h - [ >(dsubst_vref_lt … Hid2h) elim (lt_or_ge i d1) #Hid1 - [ lapply (lt_to_le_to_lt … (d1+h) Hid1 ?) -Hid2h // #Hid1h - lapply (lt_to_le_to_lt … Hid1h Hd12) -Hid1h -Hd12 #Hid2 - >(lift_vref_lt … Hid1) -Hid1 /2 width=1/ - | >(lift_vref_ge … Hid1) -Hid1 -Hd12 /3 width=1/ - ] - | destruct elim (le_inv_plus_l … Hd12) -Hd12 #Hd12 #Hhd2 - >dsubst_vref_eq >lift_vref_ge // >lift_lift_be // (dsubst_vref_gt … Hid2h) - >lift_vref_ge /2 width=1/ >lift_vref_ge /2 width=1/ -Hid1 - >dsubst_vref_gt /2 width=1/ -Hid2h >plus_minus // - ] -| normalize #A #IHA #d1 #d2 #Hd12 - elim (le_inv_plus_l … Hd12) #_ #Hhd2 - >IHA -IHA /2 width=1/ IHB -IHB // >IHA -IHA // -] -qed. - -theorem dsubst_dsubst_ge: ∀D1,D2,M,d1,d2. d1 ≤ d2 → - [d2 ↙ D2] [d1 ↙ D1] M = [d1 ↙ [d2 - d1 ↙ D2] D1] [d2 + 1 ↙ D2] M. -#D1 #D2 #M elim M -M -[ #i #d1 #d2 #Hd12 elim (lt_or_eq_or_gt i d1) #Hid1 - [ lapply (lt_to_le_to_lt … Hid1 Hd12) -Hd12 #Hid2 - >(dsubst_vref_lt … Hid1) >(dsubst_vref_lt … Hid2) >dsubst_vref_lt /2 width=1/ - | destruct >dsubst_vref_eq >dsubst_vref_lt /2 width=1/ - | >(dsubst_vref_gt … Hid1) elim (lt_or_eq_or_gt i (d2+1)) #Hid2 - [ lapply (ltn_to_ltO … Hid1) #Hi - >(dsubst_vref_lt … Hid2) >dsubst_vref_lt /2 width=1/ - | destruct /2 width=1/ - | lapply (le_to_lt_to_lt (d1+1) … Hid2) -Hid1 /2 width=1/ -Hd12 #Hid1 - >(dsubst_vref_gt … Hid2) >dsubst_vref_gt /2 width=1/ - >dsubst_vref_gt // /2 width=1/ - ] - ] -| normalize #A #IHA #d1 #d2 #Hd12 - lapply (IHA (d1+1) (d2+1) ?) -IHA /2 width=1/ -| normalize #B #A #IHB #IHA #d1 #d2 #Hd12 - >IHB -IHB // >IHA -IHA // -] -qed. - -theorem dsubst_dsubst_lt: ∀D1,D2,M,d1,d2. d2 < d1 → - [d2 ↙ [d1 - d2 -1 ↙ D1] D2] [d1 ↙ D1] M = [d1 - 1 ↙ D1] [d2 ↙ D2] M. -#D1 #D2 #M #d1 #d2 #Hd21 -lapply (ltn_to_ltO … Hd21) #Hd1 ->dsubst_dsubst_ge in ⊢ (???%); /2 width=1/ distributive_times_plus normalize /2 width=1/ -qed-. - -lemma lsred_lift: ∀p. liftable (lsred p). -#p #h #M1 #M2 #H elim H -p -M1 -M2 normalize /2 width=1/ -#B #A #d dsubst_dsubst_ge // -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 ] (**) (* simplify line *) - #C1 #C2 #HC12 #H #HN2 destruct /3 width=1/ -| #p #B1 #B2 #A #_ #IHB12 #N2 #H elim (lsred_inv_sn … H ??) -H [3: // |2: skip ] (**) (* simplify line *) - #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 ] (**) (* simplify line *) - #D #C1 #C2 #HC12 #H #HN2 destruct /3 width=1/ -] -qed-. diff --git a/matita/matita/contribs/lambda/length.ma b/matita/matita/contribs/lambda/length.ma deleted file mode 100644 index abb629433..000000000 --- a/matita/matita/contribs/lambda/length.ma +++ /dev/null @@ -1,31 +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 "lift.ma". - -(* LENGTH *******************************************************************) - -(* Note: this gives the number of abstractions and applications in M *) -let rec length M on M ≝ match M with -[ VRef i ⇒ 0 -| Abst A ⇒ length A + 1 -| Appl B A ⇒ (length B) + (length A) + 1 -]. - -interpretation "term length" - 'card M = (length M). - -lemma length_lift: ∀h,M,d. |↑[d, h] M| = |M|. -#h #M elim M -M normalize // -qed. diff --git a/matita/matita/contribs/lambda/lift.ma b/matita/matita/contribs/lambda/lift.ma deleted file mode 100644 index 17ea9692b..000000000 --- a/matita/matita/contribs/lambda/lift.ma +++ /dev/null @@ -1,274 +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 "term.ma". - -(* RELOCATION ***************************************************************) - -(* Policy: level metavariables : d, e - height metavariables: h, k -*) -(* Note: indexes start at zero *) -let rec lift h d M on M ≝ match M with -[ VRef i ⇒ #(tri … i d i (i + h) (i + h)) -| Abst A ⇒ 𝛌. (lift h (d+1) A) -| Appl B A ⇒ @(lift h d B). (lift h d A) -]. - -interpretation "relocation" 'Lift h d M = (lift h d M). - -notation "hvbox( ↑ [ term 46 d , break term 46 h ] break term 46 M )" - non associative with precedence 46 - for @{ 'Lift $h $d $M }. - -notation > "hvbox( ↑ [ term 46 h ] break term 46 M )" - non associative with precedence 46 - for @{ 'Lift $h 0 $M }. - -notation > "hvbox( ↑ term 46 M )" - non associative with precedence 46 - for @{ 'Lift 1 0 $M }. - -lemma lift_vref_lt: ∀d,h,i. i < d → ↑[d, h] #i = #i. -normalize /3 width=1/ -qed. - -lemma lift_vref_ge: ∀d,h,i. d ≤ i → ↑[d, h] #i = #(i+h). -#d #h #i #H elim (le_to_or_lt_eq … H) -H -normalize // /3 width=1/ -qed. -(* -lemma lift_vref_pred: ∀d,i. d < i → ↑[d, 1] #(i-1) = #i. -#d #i #Hdi >lift_vref_ge /2 width=1/ -(tri_lt ???? … Hid) -Hid -Hjd // - | #H destruct >tri_eq in Hjd; #H - elim (plus_lt_false … H) - | >(tri_gt ???? … Hid) - lapply (transitive_lt … Hjd Hid) -d #H #H0 destruct - elim (plus_lt_false … H) - ] -| #A #H destruct -| #B #A #H destruct -] -qed. - -lemma lift_inv_vref_ge: ∀j,d. d ≤ j → ∀h,M. ↑[d, h] M = #j → - d + h ≤ j ∧ M = #(j-h). -#j #d #Hdj #h * normalize -[ #i elim (lt_or_eq_or_gt i d) #Hid - [ >(tri_lt ???? … Hid) #H destruct - lapply (le_to_lt_to_lt … Hdj Hid) -Hdj -Hid #H - elim (lt_refl_false … H) - | #H -Hdj destruct /2 width=1/ - | >(tri_gt ???? … Hid) #H -Hdj destruct /4 width=1/ - ] -| #A #H destruct -| #B #A #H destruct -] -qed-. - -lemma lift_inv_vref_be: ∀j,d,h. d ≤ j → j < d + h → ∀M. ↑[d, h] M = #j → ⊥. -#j #d #h #Hdj #Hjdh #M #H elim (lift_inv_vref_ge … H) -H // -Hdj #Hdhj #_ -M -lapply (lt_to_le_to_lt … Hjdh Hdhj) -d -h #H -elim (lt_refl_false … H) -qed-. - -lemma lift_inv_vref_ge_plus: ∀j,d,h. d + h ≤ j → - ∀M. ↑[d, h] M = #j → M = #(j-h). -#j #d #h #Hdhj #M #H elim (lift_inv_vref_ge … H) -H // -M /2 width=2/ -qed. - -lemma lift_inv_abst: ∀C,d,h,M. ↑[d, h] M = 𝛌.C → - ∃∃A. ↑[d+1, h] A = C & M = 𝛌.A. -#C #d #h * normalize -[ #i #H destruct -| #A #H destruct /2 width=3/ -| #B #A #H destruct -] -qed-. - -lemma lift_inv_appl: ∀D,C,d,h,M. ↑[d, h] M = @D.C → - ∃∃B,A. ↑[d, h] B = D & ↑[d, h] A = C & M = @B.A. -#D #C #d #h * normalize -[ #i #H destruct -| #A #H destruct -| #B #A #H destruct /2 width=5/ -] -qed-. - -theorem lift_lift_le: ∀h1,h2,M,d1,d2. d2 ≤ d1 → - ↑[d2, h2] ↑[d1, h1] M = ↑[d1 + h2, h1] ↑[d2, h2] M. -#h1 #h2 #M elim M -M -[ #i #d1 #d2 #Hd21 elim (lt_or_ge i d2) #Hid2 - [ lapply (lt_to_le_to_lt … Hid2 Hd21) -Hd21 #Hid1 - >(lift_vref_lt … Hid1) >(lift_vref_lt … Hid2) - >lift_vref_lt // /2 width=1/ - | >(lift_vref_ge … Hid2) elim (lt_or_ge i d1) #Hid1 - [ >(lift_vref_lt … Hid1) >(lift_vref_ge … Hid2) - >lift_vref_lt // -d2 /2 width=1/ - | >(lift_vref_ge … Hid1) >lift_vref_ge /2 width=1/ - >lift_vref_ge // /2 width=1/ - ] - ] -| normalize #A #IHA #d1 #d2 #Hd21 >IHA // /2 width=1/ -| normalize #B #A #IHB #IHA #d1 #d2 #Hd21 >IHB >IHA // -] -qed. - -theorem lift_lift_be: ∀h1,h2,M,d1,d2. d1 ≤ d2 → d2 ≤ d1 + h1 → - ↑[d2, h2] ↑[d1, h1] M = ↑[d1, h1 + h2] M. -#h1 #h2 #M elim M -M -[ #i #d1 #d2 #Hd12 #Hd21 elim (lt_or_ge i d1) #Hid1 - [ lapply (lt_to_le_to_lt … Hid1 Hd12) -Hd12 -Hd21 #Hid2 - >(lift_vref_lt … Hid1) >(lift_vref_lt … Hid1) /2 width=1/ - | lapply (transitive_le … (i+h1) Hd21 ?) -Hd21 -Hd12 /2 width=1/ #Hd2 - >(lift_vref_ge … Hid1) >(lift_vref_ge … Hid1) /2 width=1/ - ] -| normalize #A #IHA #d1 #d2 #Hd12 #Hd21 >IHA // /2 width=1/ -| normalize #B #A #IHB #IHA #d1 #d2 #Hd12 #Hd21 >IHB >IHA // -] -qed. - -theorem lift_lift_ge: ∀h1,h2,M,d1,d2. d1 + h1 ≤ d2 → - ↑[d2, h2] ↑[d1, h1] M = ↑[d1, h1] ↑[d2 - h1, h2] M. -#h1 #h2 #M #d1 #d2 #Hd12 ->(lift_lift_le h2 h1) /2 width=1/ (lift_vref_lt … Hid) in H; #H - >(lift_inv_vref_lt … Hid … H) -M2 -d -h // - | >(lift_vref_ge … Hid) in H; #H - >(lift_inv_vref_ge_plus … H) -M2 // /2 width=1/ - ] -| normalize #A1 #IHA1 #M2 #d #H - elim (lift_inv_abst … H) -H #A2 #HA12 #H destruct - >(IHA1 … HA12) -IHA1 -A2 // -| normalize #B1 #A1 #IHB1 #IHA1 #M2 #d #H - elim (lift_inv_appl … H) -H #B2 #A2 #HB12 #HA12 #H destruct - >(IHB1 … HB12) -IHB1 -B2 >(IHA1 … HA12) -IHA1 -A2 // -] -qed-. - -theorem lift_inv_lift_le: ∀h1,h2,M1,M2,d1,d2. d2 ≤ d1 → - ↑[d2, h2] M2 = ↑[d1 + h2, h1] M1 → - ∃∃M. ↑[d1, h1] M = M2 & ↑[d2, h2] M = M1. -#h1 #h2 #M1 elim M1 -M1 -[ #i #M2 #d1 #d2 #Hd21 elim (lt_or_ge i (d1+h2)) #Hid1 - [ >(lift_vref_lt … Hid1) elim (lt_or_ge i d2) #Hid2 #H - [ lapply (lt_to_le_to_lt … Hid2 Hd21) -Hd21 -Hid1 #Hid1 - >(lift_inv_vref_lt … Hid2 … H) -M2 /3 width=3/ - | elim (lift_inv_vref_ge … H) -H -Hd21 // -Hid2 #Hdh2i #H destruct - elim (le_inv_plus_l … Hdh2i) -Hdh2i #Hd2i #Hh2i - @(ex2_intro … (#(i-h2))) [ /4 width=1/ ] -Hid1 - >lift_vref_ge // -Hd2i /3 width=1/ (**) (* auto: needs some help here *) - ] - | elim (le_inv_plus_l … Hid1) #Hd1i #Hh2i - lapply (transitive_le (d2+h2) … Hid1) /2 width=1/ -Hd21 #Hdh2i - elim (le_inv_plus_l … Hdh2i) #Hd2i #_ - >(lift_vref_ge … Hid1) #H -Hid1 - >(lift_inv_vref_ge_plus … H) -H /2 width=3/ -Hdh2i - @(ex2_intro … (#(i-h2))) (**) (* auto: needs some help here *) - [ >lift_vref_ge // -Hd1i /3 width=1/ - | >lift_vref_ge // -Hd2i -Hd1i /3 width=1/ - ] - ] -| normalize #A1 #IHA1 #M2 #d1 #d2 #Hd21 #H - elim (lift_inv_abst … H) -H >plus_plus_comm_23 #A2 #HA12 #H destruct - elim (IHA1 … HA12) -IHA1 -HA12 /2 width=1/ -Hd21 #A #HA2 #HA1 - @(ex2_intro … (𝛌.A)) normalize // -| normalize #B1 #A1 #IHB1 #IHA1 #M2 #d1 #d2 #Hd21 #H - elim (lift_inv_appl … H) -H #B2 #A2 #HB12 #HA12 #H destruct - elim (IHB1 … HB12) -IHB1 -HB12 // #B #HB2 #HB1 - elim (IHA1 … HA12) -IHA1 -HA12 // -Hd21 #A #HA2 #HA1 - @(ex2_intro … (@B.A)) normalize // -] -qed-. - -theorem lift_inv_lift_be: ∀h1,h2,M1,M2,d1,d2. d1 ≤ d2 → d2 ≤ d1 + h1 → - ↑[d2, h2] M2 = ↑[d1, h1 + h2] M1 → ↑[d1, h1] M1 = M2. -#h1 #h2 #M1 elim M1 -M1 -[ #i #M2 #d1 #d2 #Hd12 #Hd21 elim (lt_or_ge i d1) #Hid1 - [ lapply (lt_to_le_to_lt … Hid1 Hd12) -Hd12 -Hd21 #Hid2 - >(lift_vref_lt … Hid1) #H >(lift_inv_vref_lt … Hid2 … H) -h2 -M2 -d2 /2 width=1/ - | lapply (transitive_le … (i+h1) Hd21 ?) -Hd12 -Hd21 /2 width=1/ #Hd2 - >(lift_vref_ge … Hid1) #H >(lift_inv_vref_ge_plus … H) -M2 /2 width=1/ - ] -| normalize #A1 #IHA1 #M2 #d1 #d2 #Hd12 #Hd21 #H - elim (lift_inv_abst … H) -H #A #HA12 #H destruct - >(IHA1 … HA12) -IHA1 -HA12 // /2 width=1/ -| normalize #B1 #A1 #IHB1 #IHA1 #M2 #d1 #d2 #Hd12 #Hd21 #H - elim (lift_inv_appl … H) -H #B #A #HB12 #HA12 #H destruct - >(IHB1 … HB12) -IHB1 -HB12 // >(IHA1 … HA12) -IHA1 -HA12 // -] -qed-. - -theorem lift_inv_lift_ge: ∀h1,h2,M1,M2,d1,d2. d1 + h1 ≤ d2 → - ↑[d2, h2] M2 = ↑[d1, h1] M1 → - ∃∃M. ↑[d1, h1] M = M2 & ↑[d2 - h1, h2] M = M1. -#h1 #h2 #M1 #M2 #d1 #d2 #Hd12 #H -elim (le_inv_plus_l … Hd12) -Hd12 #Hd12 #Hh1d2 -lapply (sym_eq term … H) -H >(plus_minus_m_m … Hh1d2) in ⊢ (???%→?); -Hh1d2 #H -elim (lift_inv_lift_le … Hd12 … H) -H -Hd12 /2 width=3/ -qed-. - -definition liftable: predicate (relation term) ≝ λR. - ∀h,M1,M2. R M1 M2 → ∀d. R (↑[d, h] M1) (↑[d, h] M2). - -definition deliftable_sn: predicate (relation term) ≝ λR. - ∀h,N1,N2. R N1 N2 → ∀d,M1. ↑[d, h] M1 = N1 → - ∃∃M2. R M1 M2 & ↑[d, h] M2 = N2. - -lemma star_liftable: ∀R. liftable R → liftable (star … R). -#R #HR #h #M1 #M2 #H elim H -M2 // /3 width=3/ -qed. - -lemma star_deliftable_sn: ∀R. deliftable_sn R → deliftable_sn (star … R). -#R #HR #h #N1 #N2 #H elim H -N2 /2 width=3/ -#N #N2 #_ #HN2 #IHN1 #d #M1 #HMN1 -elim (IHN1 … HMN1) -N1 #M #HM1 #HMN -elim (HR … HN2 … HMN) -N /3 width=3/ -qed-. - -lemma lstar_liftable: ∀T,R. (∀t. liftable (R t)) → - ∀l. liftable (lstar T … R l). -#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 -@(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/multiplicity.ma b/matita/matita/contribs/lambda/multiplicity.ma deleted file mode 100644 index 4f91a6308..000000000 --- a/matita/matita/contribs/lambda/multiplicity.ma +++ /dev/null @@ -1,52 +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 "delifting_substitution.ma". - -(* MULTIPLICITY *************************************************************) - -(* Note: this gives the number of variable references in M *) -let rec mult M on M ≝ match M with -[ VRef i ⇒ 1 -| Abst A ⇒ mult A -| Appl B A ⇒ (mult B) + (mult A) -]. - -interpretation "term multiplicity" - 'Multiplicity M = (mult M). - -notation "hvbox( #{ term 46 M } )" - non associative with precedence 90 - for @{ 'Multiplicity $M }. - -lemma mult_positive: ∀M. 0 < #{M}. -#M elim M -M // /2 width=1/ -qed. - -lemma mult_lift: ∀h,M,d. #{↑[d, h] M} = #{M}. -#h #M elim M -M normalize // -qed. - -theorem mult_dsubst: ∀D,M,d. #{[d ↙ D] M} ≤ #{M} * #{D}. -#D #M elim M -M -[ #i #d elim (lt_or_eq_or_gt i d) #Hid - [ >(dsubst_vref_lt … Hid) normalize // - | destruct >dsubst_vref_eq normalize // - | >(dsubst_vref_gt … Hid) normalize // - ] -| normalize // -| normalize #B #A #IHB #IHA #d - >distributive_times_plus_r /2 width=1/ -] -qed. diff --git a/matita/matita/contribs/lambda/notation.ma b/matita/matita/contribs/lambda/notation.ma new file mode 100644 index 000000000..4bfca6887 --- /dev/null +++ b/matita/matita/contribs/lambda/notation.ma @@ -0,0 +1,61 @@ +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) + +(* GENERIC NOTATION *********************************************************) + +notation "hvbox( # term 90 i )" + non associative with precedence 46 + for @{ 'VariableReferenceByIndex $i }. + +notation "hvbox( { term 46 b } # break term 90 i )" + non associative with precedence 46 + for @{ 'VariableReferenceByIndex $b $i }. + +notation "hvbox( 𝛌 . term 46 A )" + non associative with precedence 46 + for @{ 'Abstraction $A }. + +notation "hvbox( { term 46 b } 𝛌 . break term 46 T)" + non associative with precedence 46 + for @{ 'Abstraction $b $T }. + +notation "hvbox( @ term 46 C . break term 46 A )" + non associative with precedence 46 + for @{ 'Application $C $A }. + +notation "hvbox( { term 46 b } @ break term 46 V . break term 46 T )" + non associative with precedence 46 + for @{ 'Application $b $V $T }. + +notation "hvbox( ↑ [ term 46 d , break term 46 h ] break term 46 M )" + non associative with precedence 46 + for @{ 'Lift $h $d $M }. + +notation > "hvbox( ↑ [ term 46 h ] break term 46 M )" + non associative with precedence 46 + for @{ 'Lift $h 0 $M }. + +notation > "hvbox( ↑ term 46 M )" + non associative with precedence 46 + for @{ 'Lift 1 0 $M }. + +(* Note: the notation with "/" does not work *) +notation "hvbox( [ term 46 d ↙ break term 46 N ] break term 46 M )" + non associative with precedence 46 + for @{ 'DSubst $N $d $M }. + +notation > "hvbox( [ ↙ term 46 N ] break term 46 M )" + non associative with precedence 46 + for @{ 'DSubst $N 0 $M }. + \ No newline at end of file diff --git a/matita/matita/contribs/lambda/parallel_computation.ma b/matita/matita/contribs/lambda/parallel_computation.ma deleted file mode 100644 index af64cc09c..000000000 --- a/matita/matita/contribs/lambda/parallel_computation.ma +++ /dev/null @@ -1,87 +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 "parallel_reduction.ma". - -(* PARALLEL COMPUTATION (MULTISTEP) *****************************************) - -definition preds: relation term ≝ star … pred. - -interpretation "parallel computation" - 'ParRedStar M N = (preds M N). - -notation "hvbox( M ⤇* break term 46 N )" - non associative with precedence 45 - for @{ 'ParRedStar $M $N }. - -lemma preds_refl: reflexive … preds. -// -qed. - -lemma preds_step_sn: ∀M1,M. M1 ⤇ M → ∀M2. M ⤇* M2 → M1 ⤇* M2. -/2 width=3/ -qed-. - -lemma preds_step_dx: ∀M1,M. M1 ⤇* M → ∀M2. M ⤇ M2 → M1 ⤇* M2. -/2 width=3/ -qed-. - -lemma preds_step_rc: ∀M1,M2. M1 ⤇ M2 → M1 ⤇* M2. -/2 width=1/ -qed. - -lemma preds_compatible_abst: compatible_abst preds. -/3 width=1/ -qed. - -lemma preds_compatible_sn: compatible_sn preds. -/3 width=1/ -qed. - -lemma preds_compatible_dx: compatible_dx preds. -/3 width=1/ -qed. - -lemma preds_compatible_appl: compatible_appl preds. -/3 width=1/ -qed. - -lemma preds_lift: liftable preds. -/2 width=1/ -qed. - -lemma preds_inv_lift: deliftable_sn preds. -/3 width=3 by star_deliftable_sn, pred_inv_lift/ -qed-. - -lemma preds_dsubst_dx: dsubstable_dx preds. -/2 width=1/ -qed. - -lemma preds_dsubst: dsubstable preds. -/2 width=1/ -qed. - -theorem preds_trans: transitive … preds. -/2 width=3 by trans_star/ -qed-. - -lemma preds_strip: ∀M0,M1. M0 ⤇* M1 → ∀M2. M0 ⤇ M2 → - ∃∃M. M1 ⤇ M & M2 ⤇* M. -/3 width=3 by star_strip, pred_conf/ -qed-. - -theorem preds_conf: confluent … preds. -/3 width=3 by star_confluent, pred_conf/ -qed-. diff --git a/matita/matita/contribs/lambda/parallel_reduction.ma b/matita/matita/contribs/lambda/parallel_reduction.ma deleted file mode 100644 index 1d97b3b87..000000000 --- a/matita/matita/contribs/lambda/parallel_reduction.ma +++ /dev/null @@ -1,156 +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 "length.ma". -include "labeled_sequential_reduction.ma". - -(* PARALLEL REDUCTION (SINGLE STEP) *****************************************) - -(* Note: the application "(A B)" is represented by "@B.A" - as for labelled sequential reduction -*) -inductive pred: relation term ≝ -| pred_vref: ∀i. pred (#i) (#i) -| 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" - 'ParRed M N = (pred M N). - -notation "hvbox( M ⤇ break term 46 N )" - non associative with precedence 45 - for @{ 'ParRed $M $N }. - -lemma pred_refl: reflexive … pred. -#M elim M -M // /2 width=1/ -qed. - -lemma pred_inv_vref: ∀M,N. M ⤇ N → ∀i. #i = M → #i = N. -#M #N * -M -N // -[ #A1 #A2 #_ #i #H destruct -| #B1 #B2 #A1 #A2 #_ #_ #i #H destruct -| #B1 #B2 #A1 #A2 #_ #_ #i #H destruct -] -qed-. - -lemma pred_inv_abst: ∀M,N. M ⤇ N → ∀A. 𝛌.A = M → - ∃∃C. A ⤇ C & 𝛌.C = N. -#M #N * -M -N -[ #i #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-. - -lemma pred_inv_appl: ∀M,N. M ⤇ N → ∀B,A. @B.A = M → - (∃∃D,C. B ⤇ D & A ⤇ C & @D.C = N) ∨ - ∃∃A0,D,C0. B ⤇ D & A0 ⤇ C0 & 𝛌.A0 = A & [↙D]C0 = N. -#M #N * -M -N -[ #i #B0 #A0 #H destruct -| #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/ -#B1 #B2 #A1 #A2 #_ #_ #IHB12 #IHC12 #d (dsubst_vref_lt … Hid) >(dsubst_vref_lt … Hid) // - | destruct >dsubst_vref_eq >dsubst_vref_eq /2 width=1/ - | >(dsubst_vref_gt … Hid) >(dsubst_vref_gt … Hid) // - ] -| normalize /2 width=1/ -| normalize /2 width=1/ -| normalize #B1 #B2 #A1 #A2 #_ #_ #IHB12 #IHC12 #d - >dsubst_dsubst_ge // /2 width=1/ -] -qed. - -lemma pred_conf1_vref: ∀i. confluent1 … pred (#i). -#i #M1 #H1 #M2 #H2 -<(pred_inv_vref … H1) -H1 [3: // |2: skip ] (**) (* simplify line *) -<(pred_inv_vref … H2) -H2 [3: // |2: skip ] (**) (* simplify line *) -/2 width=3/ -qed-. - -lemma pred_conf1_abst: ∀A. confluent1 … pred A → confluent1 … pred (𝛌.A). -#A #IH #M1 #H1 #M2 #H2 -elim (pred_inv_abst … H1 ??) -H1 [3: // |2: skip ] #A1 #HA1 #H destruct (**) (* simplify line *) -elim (pred_inv_abst … H2 ??) -H2 [3: // |2: skip ] #A2 #HA2 #H destruct (**) (* simplify line *) -elim (IH … HA1 … HA2) -A /3 width=3/ -qed-. - -lemma pred_conf1_appl_beta: ∀B,B1,B2,C,C2,M1. - (∀M0. |M0| < |B|+|𝛌.C|+1 → confluent1 ? pred M0) → (**) (* ? needed in place of … *) - B ⤇ B1 → B ⤇ B2 → 𝛌.C ⤇ M1 → C ⤇ C2 → - ∃∃M. @B1.M1 ⤇ M & [↙B2]C2 ⤇ M. -#B #B1 #B2 #C #C2 #M1 #IH #HB1 #HB2 #H1 #HC2 -elim (pred_inv_abst … H1 ??) -H1 [3: // |2: skip ] #C1 #HC1 #H destruct (**) (* simplify line *) -elim (IH B … HB1 … HB2) -HB1 -HB2 // -elim (IH C … HC1 … HC2) normalize // -B -C /3 width=5/ -qed-. - -theorem pred_conf: confluent … pred. -#M @(f_ind … length … M) -M #n #IH * normalize -[ /2 width=3 by pred_conf1_vref/ -| /3 width=4 by pred_conf1_abst/ -| #B #A #H #M1 #H1 #M2 #H2 destruct - elim (pred_inv_appl … H1 ???) -H1 [5: // |2,3: skip ] * (**) (* simplify line *) - elim (pred_inv_appl … H2 ???) -H2 [5,10: // |2,3,7,8: skip ] * (**) (* simplify line *) - [ #B2 #A2 #HB2 #HA2 #H2 #B1 #A1 #HB1 #HA1 #H1 destruct - elim (IH A … HA1 … HA2) -HA1 -HA2 // - elim (IH B … HB1 … HB2) // -A -B /3 width=5/ - | #C #B2 #C2 #HB2 #HC2 #H2 #HM2 #B1 #N #HB1 #H #HM1 destruct - @(pred_conf1_appl_beta … IH) // (**) (* /2 width=7 by pred_conf1_appl_beta/ does not work *) - | #B2 #N #B2 #H #HM2 #C #B1 #C1 #HB1 #HC1 #H1 #HM1 destruct - @ex2_commute @(pred_conf1_appl_beta … IH) // - | #C #B2 #C2 #HB2 #HC2 #H2 #HM2 #C0 #B1 #C1 #HB1 #HC1 #H1 #HM1 destruct - elim (IH B … HB1 … HB2) -HB1 -HB2 // - elim (IH C … HC1 … HC2) normalize // -B -C /3 width=5/ - ] -] -qed-. - -lemma lsred_pred: ∀p,M,N. M ↦[p] N → M ⤇ N. -#p #M #N #H elim H -p -M -N /2 width=1/ -qed. diff --git a/matita/matita/contribs/lambda/pointer.ma b/matita/matita/contribs/lambda/pointer.ma deleted file mode 100644 index d71574e74..000000000 --- a/matita/matita/contribs/lambda/pointer.ma +++ /dev/null @@ -1,54 +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 "term.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 whd" when is not under an abstraction nor in the lefr argument of an application *) -definition in_whd: predicate ptr ≝ All … is_dx. - -lemma in_whd_ind: ∀R:predicate ptr. R (◊) → - (∀p. in_whd p → R p → R (dx::p)) → - ∀p. in_whd p → R p. -#R #H #IH #p elim p -p // -H * -#p #IHp * #H1 #H2 destruct /3 width=1/ -qed-. - -definition compatible_rc: predicate (ptr→relation term) ≝ λR. - ∀p,A1,A2. R p A1 A2 → R (rc::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). - -definition compatible_dx: predicate (ptr→relation term) ≝ λR. - ∀p,B,A1,A2. R p A1 A2 → R (dx::p) (@B.A1) (@B.A2). diff --git a/matita/matita/contribs/lambda/pointer_list.ma b/matita/matita/contribs/lambda/pointer_list.ma deleted file mode 100644 index becfc0a5e..000000000 --- a/matita/matita/contribs/lambda/pointer_list.ma +++ /dev/null @@ -1,54 +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 "pointer.ma". - -(* POINTER LIST *************************************************************) - -(* Policy: pointer list metavariables: r, s *) -definition ptrl: Type[0] ≝ list ptr. - -(* Note: a "whd" computation contracts just redexes in the whd *) -definition is_whd: predicate ptrl ≝ All … in_whd. - -lemma is_whd_dx: ∀s. is_whd s → is_whd (dx:::s). -#s elim s -s // -#p #s #IHs * /3 width=1/ -qed. - -lemma is_whd_append: ∀r. is_whd r → ∀s. is_whd s → is_whd (r@s). -#r elim r -r // -#q #r #IHr * /3 width=1/ -qed. - -definition ho_compatible_rc: predicate (ptrl→relation term) ≝ λR. - ∀s,A1,A2. R s A1 A2 → R (rc:::s) (𝛌.A1) (𝛌.A2). - -definition ho_compatible_sn: predicate (ptrl→relation term) ≝ λR. - ∀s,B1,B2,A. R s B1 B2 → R (sn:::s) (@B1.A) (@B2.A). - -definition ho_compatible_dx: predicate (ptrl→relation term) ≝ λR. - ∀s,B,A1,A2. R s A1 A2 → R (dx:::s) (@B.A1) (@B.A2). - -lemma lstar_compatible_rc: ∀R. compatible_rc R → ho_compatible_rc (lstar … R). -#R #HR #s #A1 #A2 #H @(lstar_ind_l ????????? H) -s -A1 // /3 width=3/ -qed. - -lemma lstar_compatible_sn: ∀R. compatible_sn R → ho_compatible_sn (lstar … R). -#R #HR #s #B1 #B2 #A #H @(lstar_ind_l ????????? H) -s -B1 // /3 width=3/ -qed. - -lemma lstar_compatible_dx: ∀R. compatible_dx R → ho_compatible_dx (lstar … R). -#R #HR #s #B #A1 #A2 #H @(lstar_ind_l ????????? H) -s -A1 // /3 width=3/ -qed. diff --git a/matita/matita/contribs/lambda/pointer_list_standard.ma b/matita/matita/contribs/lambda/pointer_list_standard.ma deleted file mode 100644 index 8ae8d5aa1..000000000 --- a/matita/matita/contribs/lambda/pointer_list_standard.ma +++ /dev/null @@ -1,52 +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 "pointer_list.ma". -include "pointer_order.ma". - -(* STANDARD POINTER LIST ****************************************************) - -(* Note: to us, a "normal" computation contracts redexes in non-decreasing positions *) -definition is_standard: predicate ptrl ≝ Allr … ple. - -lemma is_standard_compatible: ∀c,s. is_standard s → is_standard (c:::s). -#c #s elim s -s // #p * // -#q #s #IHs * /3 width=1/ -qed. - -lemma is_standard_cons: ∀p,s. is_standard s → is_standard ((dx::p)::sn:::s). -#p #s elim s -s // #q1 * /2 width=1/ -#q2 #s #IHs * /4 width=1/ -qed. - -lemma is_standard_append: ∀r. is_standard r → ∀s. is_standard s → is_standard ((dx:::r)@sn:::s). -#r elim r -r /3 width=1/ #p * /2 width=1/ -#q #r #IHr * /3 width=1/ -qed. - -theorem is_whd_is_standard: ∀s. is_whd s → is_standard s. -#s elim s -s // #p * // -#q #s #IHs * /3 width=1/ -qed. - -lemma is_standard_in_whd: ∀p. in_whd p → ∀s. is_standard s → is_standard (p::s). -#p #Hp * // /3 width=1/ -qed. - -theorem is_whd_is_standard_trans: ∀r. is_whd r → ∀s. is_standard s → is_standard (r@s). -#r elim r -r // #p * -[ #_ * /2 width=1/ -| #q #r #IHr * /3 width=1/ -] -qed. diff --git a/matita/matita/contribs/lambda/pointer_order.ma b/matita/matita/contribs/lambda/pointer_order.ma deleted file mode 100644 index 0b738215a..000000000 --- a/matita/matita/contribs/lambda/pointer_order.ma +++ /dev/null @@ -1,148 +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 "pointer.ma". - -(* POINTER ORDER ************************************************************) - -(* Note: precedence relation on redex pointers: p ≺ q - 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 (rc::p) (sn::q) -| pprec_comp: ∀c,p,q. pprec p q → pprec (c::p) (c::q) -| pprec_skip: pprec (dx::◊) ◊ -. - -interpretation "'precedes' on pointers" - 'prec p q = (pprec p q). - -(* Note: this should go to core_notation *) -notation "hvbox(a break ≺ b)" - non associative with precedence 45 - for @{ 'prec $a $b }. - -lemma pprec_fwd_in_whd: ∀p,q. p ≺ q → in_whd q → in_whd 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-. - -(* Note: this is p < q *) -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. - -interpretation "'less or equal to' on redex pointers" - 'leq p q = (ple p q). - -lemma ple_step_rc: ∀p,q. p ≺ q → p ≤ q. -/2 width=1/ -qed. - -lemma ple_step_sn: ∀p1,p,p2. p1 ≺ p → p ≤ p2 → p1 ≤ p2. -/2 width=3/ -qed-. - -lemma ple_rc: ∀p,q. dx::p ≤ rc::q. -/2 width=1/ -qed. - -lemma ple_sn: ∀p,q. rc::p ≤ sn::q. -/2 width=1/ -qed. - -lemma ple_skip: dx::◊ ≤ ◊. -/2 width=1/ -qed. - -lemma ple_nil: ∀p. ◊ ≤ p. -* // /2 width=1/ -qed. - -lemma ple_comp: ∀p1,p2. p1 ≤ p2 → ∀c. (c::p1) ≤ (c::p2). -#p1 #p2 #H elim H -p2 // /3 width=3/ -qed. - -lemma ple_skip_ple: ∀p. p ≤ ◊ → dx::p ≤ ◊. -#p #H @(star_ind_l ??????? H) -p // -#p #q #Hpq #_ #H @(ple_step_sn … H) -H /2 width=1/ -qed. - -theorem ple_trans: transitive … ple. -/2 width=3/ -qed-. - -lemma ple_cons: ∀p,q. dx::p ≤ sn::q. -#p #q -@(ple_trans … (rc::q)) /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_whd_ple_nil: ∀p. in_whd p → p ≤ ◊. -#p #H @(in_whd_ind … H) -p // /2 width=1/ -qed. - -theorem in_whd_ple: ∀p. in_whd p → ∀q. p ≤ q. -#p #H @(in_whd_ind … H) -p // -#p #_ #IHp * /3 width=1/ * #q /2 width=1/ -qed. - -lemma ple_nil_inv_in_whd: ∀p. p ≤ ◊ → in_whd p. -#p #H @(star_ind_l ??????? H) -p // /2 width=3 by pprec_fwd_in_whd/ -qed-. - -lemma ple_inv_in_whd: ∀p. (∀q. p ≤ q) → in_whd p. -/2 width=1 by ple_nil_inv_in_whd/ -qed-. diff --git a/matita/matita/contribs/lambda/pointer_tree.ma b/matita/matita/contribs/lambda/pointer_tree.ma deleted file mode 100644 index 4381cd62c..000000000 --- a/matita/matita/contribs/lambda/pointer_tree.ma +++ /dev/null @@ -1,31 +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 "pointer_list.ma". - -(* POINTER TREE *************************************************************) - -(* Policy: pointer tree metavariables: P, Q *) -(* Note: this is a binary tree on pointer sequences *) -inductive ptrt: Type[0] ≝ -| tnil : ptrt -| tcons: ptrl → ptrt → ptrt → ptrt -. - -let rec length (P:ptrt) on P ≝ match P with -[ tnil ⇒ 0 -| tcons s Q1 Q2 ⇒ length Q2 + length Q1 + |s| -]. - -interpretation "pointer tree length" 'card P = (length P). diff --git a/matita/matita/contribs/lambda/policy.txt b/matita/matita/contribs/lambda/policy.txt index 7743f9bbd..33fc5979b 100644 --- a/matita/matita/contribs/lambda/policy.txt +++ b/matita/matita/contribs/lambda/policy.txt @@ -1,13 +1,17 @@ NAMING CONVENTIONS FOR METAVARIABLES A, B, C, D: term +F,G : subset of subterms H : transient premise IH : inductive premise M, N : term P, Q : pointer tree R : arbitrary relation -T, U : arbitrary small type +S : arbitrary small type +T, U, V, W: subset of subterms +a : arbitrary element +b : boolean mark c : pointer step d, e : variable reference level h : relocation height @@ -17,4 +21,4 @@ l : arbitrary list m, n : measures on terms p, q : pointer r, s : pointer sequence -t, u : arbitrary element + diff --git a/matita/matita/contribs/lambda/st_computation.ma b/matita/matita/contribs/lambda/st_computation.ma deleted file mode 100644 index ebcc572a4..000000000 --- a/matita/matita/contribs/lambda/st_computation.ma +++ /dev/null @@ -1,214 +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 "labeled_sequential_computation.ma". -include "pointer_list_standard.ma". - -(* KASHIMA'S "ST" COMPUTATION ***********************************************) - -(* Note: this is the "standard" computation of: - R. Kashima: "A proof of the Standization Theorem in λ-Calculus". Typescript note, (2000). -*) -inductive st: relation term ≝ -| st_vref: ∀s,M,i. is_whd s → M ↦*[s] #i → st M (#i) -| st_abst: ∀s,M,A1,A2. is_whd s → M ↦*[s] 𝛌.A1 → st A1 A2 → st M (𝛌.A2) -| st_appl: ∀s,M,B1,B2,A1,A2. is_whd s → M ↦*[s] @B1.A1 → st B1 B2 → st A1 A2 → st M (@B2.A2) -. - -interpretation "'st' computation" - 'Std M N = (st M N). - -notation "hvbox( M ⓢ⤇* break term 46 N )" - non associative with precedence 45 - for @{ 'Std $M $N }. - -lemma st_inv_lref: ∀M,N. M ⓢ⤇* N → ∀j. #j = N → - ∃∃s. is_whd s & M ↦*[s] #j. -#M #N * -M -N -[ /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. is_whd s & M ↦*[s] 𝛌.C1 & C1 ⓢ⤇* C2. -#M #N * -M -N -[ #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. is_whd 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 #Hs #HM #HB12 #HA12 #D2 #C2 #H destruct /2 width=7/ -] -qed-. - -lemma st_refl: reflexive … st. -#M elim M -M /2 width=3/ /2 width=5/ /2 width=7/ -qed. - -lemma st_step_sn: ∀N1,N2. N1 ⓢ⤇* N2 → ∀s,M. is_whd s → M ↦*[s] N1 → M ⓢ⤇* N2. -#N1 #N2 #H elim H -N1 -N2 -[ #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. is_whd 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=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 #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=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=7/ -] -qed-. - -lemma st_dsubst: dsubstable st. -#N1 #N2 #HN12 #M1 #M2 #H elim H -M1 -M2 -[ #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 (lsreds_dsubst … N1 … HM d) -HM - >(dsubst_vref_gt … Hid) >(dsubst_vref_gt … Hid) /2 width=3/ - ] -| #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_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 #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=5/ (**) (* simplify line *) -| #p #B #B2 #A #_ #IHB2 #M1 #H - 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=7/ (**) (* simplify line *) -] -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. - -lemma st_inv_lsreds_is_standard: ∀M,N. M ⓢ⤇* N → - ∃∃r. M ↦*[r] N & is_standard r. -#M #N #H elim H -M -N -[ #s #M #i #Hs #HM - lapply (is_whd_is_standard … Hs) -Hs /2 width=3/ -| #s #M #A1 #A2 #Hs #HM #_ * #r #HA12 #Hr - lapply (lsreds_trans … HM (rc:::r) (𝛌.A2) ?) /2 width=1/ -A1 #HM - @(ex2_intro … HM) -M -A2 /3 width=1/ -| #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/ -] -qed-. - -theorem st_trans: transitive … st. -#M1 #M #M2 #HM1 #HM2 -elim (st_inv_lsreds_is_standard … HM1) -HM1 #s1 #HM1 #_ -elim (st_inv_lsreds_is_standard … 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_standard r. -#s #M #N #H -@st_inv_lsreds_is_standard /2 width=2/ -qed-. - -(* Note: we use "lapply (rewrite_r ?? is_whd … Hq)" (procedural) - in place of "cut (is_whd (q::r)) [ >Hq ]" (declarative) -*) -lemma st_lsred_swap: ∀p. in_whd p → ∀N1,N2. N1 ↦[p] N2 → ∀M1. M1 ⓢ⤇* N1 → - ∃∃q,M2. in_whd q & M1 ↦[q] M2 & M2 ⓢ⤇* N2. -#p #H @(in_whd_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 #Hq #HM1 #HM - lapply (rewrite_r ?? is_whd … Hq) -Hq /4 width=1/ -s1 -s2 * #Hq #Hr - @(ex3_2_intro … HM1) -M1 // -q - @(st_step_sn … HM) /2 width=1/ -| #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 #Hq #HM1 #HM - lapply (rewrite_r ?? is_whd … Hq) -Hq /4 width=1/ -p -s * #Hq #Hr - @(ex3_2_intro … HM1) -M1 // -q /2 width=7/ -] -qed-. - -theorem lsreds_lsred_swap: ∀s,M1,N1. M1 ↦*[s] N1 → - ∀p,N2. in_whd p → N1 ↦[p] N2 → - ∃∃q,r,M2. in_whd q & M1 ↦[q] M2 & M2 ↦*[r] N2 & - is_standard (q::r). -#s #M1 #N1 #HMN1 #p #N2 #Hp #HN12 -lapply (st_lsreds … HMN1) -s #HMN1 -elim (st_lsred_swap … Hp … HN12 … HMN1) -p -N1 #q #M2 #Hq #HM12 #HMN2 -elim (st_inv_lsreds_is_standard … HMN2) -HMN2 /3 width=8/ -qed-. diff --git a/matita/matita/contribs/lambda/subterms/lift.ma b/matita/matita/contribs/lambda/subterms/lift.ma new file mode 100644 index 000000000..c86695ffb --- /dev/null +++ b/matita/matita/contribs/lambda/subterms/lift.ma @@ -0,0 +1,254 @@ +(**************************************************************************) +(* ___ *) +(* ||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 "subterms/subterms.ma". + +(* RELOCATION FOR SUBTERMS **************************************************) + +let rec slift h d E on E ≝ match E with +[ SVRef b i ⇒ {b}#(tri … i d i (i + h) (i + h)) +| SAbst b T ⇒ {b}𝛌.(slift h (d+1) T) +| SAppl b V T ⇒ {b}@(slift h d V).(slift h d T) +]. + +interpretation "relocation for subterms" 'Lift h d E = (slift h d E). + +lemma slift_vref_lt: ∀b,d,h,i. i < d → ↑[d, h] {b}#i = {b}#i. +normalize /3 width=1/ +qed. + +lemma slift_vref_ge: ∀b,d,h,i. d ≤ i → ↑[d, h] {b}#i = {b}#(i+h). +#b #d #h #i #H elim (le_to_or_lt_eq … H) -H +normalize // /3 width=1/ +qed. + +lemma slift_id: ∀E,d. ↑[d, 0] E = E. +#E elim E -E +[ #b #i #d elim (lt_or_ge i d) /2 width=1/ +| /3 width=1/ +| /3 width=1/ +] +qed. + +lemma slift_inv_vref_lt: ∀b0,j,d. j < d → ∀h,E. ↑[d, h] E = {b0}#j → E = {b0}#j. +#b0 #j #d #Hjd #h * normalize +[ #b #i elim (lt_or_eq_or_gt i d) #Hid + [ >(tri_lt ???? … Hid) -Hid -Hjd // + | #H destruct >tri_eq in Hjd; #H + elim (plus_lt_false … H) + | >(tri_gt ???? … Hid) + lapply (transitive_lt … Hjd Hid) -d #H #H0 destruct + elim (plus_lt_false … H) + ] +| #b #T #H destruct +| #b #V #T #H destruct +] +qed. + +lemma slift_inv_vref_ge: ∀b0,j,d. d ≤ j → ∀h,E. ↑[d, h] E = {b0}#j → + d + h ≤ j ∧ E = {b0}#(j-h). +#b0 #j #d #Hdj #h * normalize +[ #b #i elim (lt_or_eq_or_gt i d) #Hid + [ >(tri_lt ???? … Hid) #H destruct + lapply (le_to_lt_to_lt … Hdj Hid) -Hdj -Hid #H + elim (lt_refl_false … H) + | #H -Hdj destruct /2 width=1/ + | >(tri_gt ???? … Hid) #H -Hdj destruct /4 width=1/ + ] +| #b #T #H destruct +| #b #V #T #H destruct +] +qed-. + +lemma slift_inv_vref_be: ∀b0,j,d,h. d ≤ j → j < d + h → ∀E. ↑[d, h] E = {b0}#j → ⊥. +#b0 #j #d #h #Hdj #Hjdh #E #H elim (slift_inv_vref_ge … H) -H // -Hdj #Hdhj #_ -E +lapply (lt_to_le_to_lt … Hjdh Hdhj) -d -h #H +elim (lt_refl_false … H) +qed-. + +lemma slift_inv_vref_ge_plus: ∀b0,j,d,h. d + h ≤ j → + ∀E. ↑[d, h] E = {b0}#j → E = {b0}#(j-h). +#b0 #j #d #h #Hdhj #E #H elim (slift_inv_vref_ge … H) -H // -E /2 width=2/ +qed. + +lemma slift_inv_abst: ∀b0,U,d,h,E. ↑[d, h] E = {b0}𝛌.U → + ∃∃T. ↑[d+1, h] T = U & E = {b0}𝛌.T. +#b0 #U #d #h * normalize +[ #b #i #H destruct +| #b #T #H destruct /2 width=3/ +| #b #V #T #H destruct +] +qed-. + +lemma slift_inv_appl: ∀b0,W,U,d,h,E. ↑[d, h] E = {b0}@W.U → + ∃∃V,T. ↑[d, h] V = W & ↑[d, h] T = U & E = {b0}@V.T. +#b0 #W #U #d #h * normalize +[ #b #i #H destruct +| #b #T #H destruct +| #b #V #T #H destruct /2 width=5/ +] +qed-. + +theorem slift_slift_le: ∀h1,h2,E,d1,d2. d2 ≤ d1 → + ↑[d2, h2] ↑[d1, h1] E = ↑[d1 + h2, h1] ↑[d2, h2] E. +#h1 #h2 #E elim E -E +[ #b #i #d1 #d2 #Hd21 elim (lt_or_ge i d2) #Hid2 + [ lapply (lt_to_le_to_lt … Hid2 Hd21) -Hd21 #Hid1 + >(slift_vref_lt … Hid1) >(slift_vref_lt … Hid2) + >slift_vref_lt // /2 width=1/ + | >(slift_vref_ge … Hid2) elim (lt_or_ge i d1) #Hid1 + [ >(slift_vref_lt … Hid1) >(slift_vref_ge … Hid2) + >slift_vref_lt // -d2 /2 width=1/ + | >(slift_vref_ge … Hid1) >slift_vref_ge /2 width=1/ + >slift_vref_ge // /2 width=1/ + ] + ] +| normalize #b #T #IHT #d1 #d2 #Hd21 >IHT // /2 width=1/ +| normalize #b #V #T #IHV #IHT #d1 #d2 #Hd21 >IHV >IHT // +] +qed. + +theorem slift_slift_be: ∀h1,h2,E,d1,d2. d1 ≤ d2 → d2 ≤ d1 + h1 → + ↑[d2, h2] ↑[d1, h1] E = ↑[d1, h1 + h2] E. +#h1 #h2 #E elim E -E +[ #b #i #d1 #d2 #Hd12 #Hd21 elim (lt_or_ge i d1) #Hid1 + [ lapply (lt_to_le_to_lt … Hid1 Hd12) -Hd12 -Hd21 #Hid2 + >(slift_vref_lt … Hid1) >(slift_vref_lt … Hid1) /2 width=1/ + | lapply (transitive_le … (i+h1) Hd21 ?) -Hd21 -Hd12 /2 width=1/ #Hd2 + >(slift_vref_ge … Hid1) >(slift_vref_ge … Hid1) /2 width=1/ + ] +| normalize #b #T #IHT #d1 #d2 #Hd12 #Hd21 >IHT // /2 width=1/ +| normalize #b #V #T #IHV #IHT #d1 #d2 #Hd12 #Hd21 >IHV >IHT // +] +qed. + +theorem slift_slift_ge: ∀h1,h2,E,d1,d2. d1 + h1 ≤ d2 → + ↑[d2, h2] ↑[d1, h1] E = ↑[d1, h1] ↑[d2 - h1, h2] E. +#h1 #h2 #E #d1 #d2 #Hd12 +>(slift_slift_le h2 h1) /2 width=1/ (slift_vref_lt … Hid) in H; #H + >(slift_inv_vref_lt … Hid … H) -E2 -d -h // + | >(slift_vref_ge … Hid) in H; #H + >(slift_inv_vref_ge_plus … H) -E2 // /2 width=1/ + ] +| normalize #b #T1 #IHT1 #E2 #d #H + elim (slift_inv_abst … H) -H #T2 #HT12 #H destruct + >(IHT1 … HT12) -IHT1 -T2 // +| normalize #b #V1 #T1 #IHV1 #IHT1 #E2 #d #H + elim (slift_inv_appl … H) -H #V2 #T2 #HV12 #HT12 #H destruct + >(IHV1 … HV12) -IHV1 -V2 >(IHT1 … HT12) -IHT1 -T2 // +] +qed-. + +theorem slift_inv_slift_le: ∀h1,h2,E1,E2,d1,d2. d2 ≤ d1 → + ↑[d2, h2] E2 = ↑[d1 + h2, h1] E1 → + ∃∃E. ↑[d1, h1] E = E2 & ↑[d2, h2] E = E1. +#h1 #h2 #E1 elim E1 -E1 +[ #b #i #E2 #d1 #d2 #Hd21 elim (lt_or_ge i (d1+h2)) #Hid1 + [ >(slift_vref_lt … Hid1) elim (lt_or_ge i d2) #Hid2 #H + [ lapply (lt_to_le_to_lt … Hid2 Hd21) -Hd21 -Hid1 #Hid1 + >(slift_inv_vref_lt … Hid2 … H) -E2 /3 width=3/ + | elim (slift_inv_vref_ge … H) -H -Hd21 // -Hid2 #Hdh2i #H destruct + elim (le_inv_plus_l … Hdh2i) -Hdh2i #Hd2i #Hh2i + @(ex2_intro … ({b}#(i-h2))) [ /4 width=1/ ] -Hid1 + >slift_vref_ge // -Hd2i /3 width=1/ (**) (* auto: needs some help here *) + ] + | elim (le_inv_plus_l … Hid1) #Hd1i #Hh2i + lapply (transitive_le (d2+h2) … Hid1) /2 width=1/ -Hd21 #Hdh2i + elim (le_inv_plus_l … Hdh2i) #Hd2i #_ + >(slift_vref_ge … Hid1) #H -Hid1 + >(slift_inv_vref_ge_plus … H) -H /2 width=3/ -Hdh2i + @(ex2_intro … ({b}#(i-h2))) (**) (* auto: needs some help here *) + [ >slift_vref_ge // -Hd1i /3 width=1/ + | >slift_vref_ge // -Hd2i -Hd1i /3 width=1/ + ] + ] +| normalize #b #T1 #IHT1 #E2 #d1 #d2 #Hd21 #H + elim (slift_inv_abst … H) -H >plus_plus_comm_23 #T2 #HT12 #H destruct + elim (IHT1 … HT12) -IHT1 -HT12 /2 width=1/ -Hd21 #T #HT2 #HT1 + @(ex2_intro … ({b}𝛌.T)) normalize // +| normalize #b #V1 #T1 #IHV1 #IHT1 #E2 #d1 #d2 #Hd21 #H + elim (slift_inv_appl … H) -H #V2 #T2 #HV12 #HT12 #H destruct + elim (IHV1 … HV12) -IHV1 -HV12 // #V #HV2 #HV1 + elim (IHT1 … HT12) -IHT1 -HT12 // -Hd21 #T #HT2 #HT1 + @(ex2_intro … ({b}@V.T)) normalize // +] +qed-. + +theorem slift_inv_slift_be: ∀h1,h2,E1,E2,d1,d2. d1 ≤ d2 → d2 ≤ d1 + h1 → + ↑[d2, h2] E2 = ↑[d1, h1 + h2] E1 → ↑[d1, h1] E1 = E2. +#h1 #h2 #E1 elim E1 -E1 +[ #b #i #E2 #d1 #d2 #Hd12 #Hd21 elim (lt_or_ge i d1) #Hid1 + [ lapply (lt_to_le_to_lt … Hid1 Hd12) -Hd12 -Hd21 #Hid2 + >(slift_vref_lt … Hid1) #H >(slift_inv_vref_lt … Hid2 … H) -h2 -E2 -d2 /2 width=1/ + | lapply (transitive_le … (i+h1) Hd21 ?) -Hd12 -Hd21 /2 width=1/ #Hd2 + >(slift_vref_ge … Hid1) #H >(slift_inv_vref_ge_plus … H) -E2 /2 width=1/ + ] +| normalize #b #T1 #IHT1 #E2 #d1 #d2 #Hd12 #Hd21 #H + elim (slift_inv_abst … H) -H #T #HT12 #H destruct + >(IHT1 … HT12) -IHT1 -HT12 // /2 width=1/ +| normalize #b #V1 #T1 #IHV1 #IHT1 #E2 #d1 #d2 #Hd12 #Hd21 #H + elim (slift_inv_appl … H) -H #V #T #HV12 #HT12 #H destruct + >(IHV1 … HV12) -IHV1 -HV12 // >(IHT1 … HT12) -IHT1 -HT12 // +] +qed-. + +theorem slift_inv_slift_ge: ∀h1,h2,E1,E2,d1,d2. d1 + h1 ≤ d2 → + ↑[d2, h2] E2 = ↑[d1, h1] E1 → + ∃∃E. ↑[d1, h1] E = E2 & ↑[d2 - h1, h2] E = E1. +#h1 #h2 #E1 #E2 #d1 #d2 #Hd12 #H +elim (le_inv_plus_l … Hd12) -Hd12 #Hd12 #Hh1d2 +lapply (sym_eq subterms … H) -H >(plus_minus_m_m … Hh1d2) in ⊢ (???%→?); -Hh1d2 #H +elim (slift_inv_slift_le … Hd12 … H) -H -Hd12 /2 width=3/ +qed-. +(* +definition liftable: predicate (relation term) ≝ λR. + ∀h,M1,M2. R M1 M2 → ∀d. R (↑[d, h] M1) (↑[d, h] M2). + +definition deliftable_sn: predicate (relation term) ≝ λR. + ∀h,N1,N2. R N1 N2 → ∀d,M1. ↑[d, h] M1 = N1 → + ∃∃M2. R M1 M2 & ↑[d, h] M2 = N2. + +lemma star_liftable: ∀R. liftable R → liftable (star … R). +#R #HR #h #M1 #M2 #H elim H -M2 // /3 width=3/ +qed. + +lemma star_deliftable_sn: ∀R. deliftable_sn R → deliftable_sn (star … R). +#R #HR #h #N1 #N2 #H elim H -N2 /2 width=3/ +#N #N2 #_ #HN2 #IHN1 #d #M1 #HMN1 +elim (IHN1 … HMN1) -N1 #M #HM1 #HMN +elim (HR … HN2 … HMN) -N /3 width=3/ +qed-. + +lemma lstar_liftable: ∀S,R. (∀a. liftable (R a)) → + ∀l. liftable (lstar S … R l). +#S #R #HR #l #h #M1 #M2 #H +@(lstar_ind_l ????????? H) -l -M1 // /3 width=3/ +qed. + +lemma lstar_deliftable_sn: ∀S,R. (∀a. deliftable_sn (R a)) → + ∀l. deliftable_sn (lstar S … R l). +#S #R #HR #l #h #N1 #N2 #H +@(lstar_ind_l ????????? H) -l -N1 /2 width=3/ +#a #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/subterms/subterms.ma b/matita/matita/contribs/lambda/subterms/subterms.ma new file mode 100644 index 000000000..1a2582a81 --- /dev/null +++ b/matita/matita/contribs/lambda/subterms/subterms.ma @@ -0,0 +1,69 @@ +(**************************************************************************) +(* ___ *) +(* ||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". +include "notation.ma". + +(* SUBSETS OF SUBTERMS ******************************************************) + +(* Policy: boolean marks metavariables: b + subterms metavariables: F,G,T,U,V,W +*) +(* Note: each subterm is marked with true if it belongs to the subset *) +inductive subterms: Type[0] ≝ +| SVRef: bool → nat → subterms +| SAbst: bool → subterms → subterms +| SAppl: bool → subterms → subterms → subterms +. + +interpretation "subterms construction (variable reference by index)" + 'VariableReferenceByIndex b i = (SVRef b i). + +interpretation "subterms construction (abstraction)" + 'Abstraction b T = (SAbst b T). + +interpretation "subterms construction (application)" + 'Application b V T = (SAppl b V T). + +(* +definition compatible_abst: predicate (relation term) ≝ λR. + ∀A1,A2. R A1 A2 → R (𝛌.A1) (𝛌.A2). + +definition compatible_sn: predicate (relation term) ≝ λR. + ∀A,B1,B2. R B1 B2 → R (@B1.A) (@B2.A). + +definition compatible_dx: predicate (relation term) ≝ λR. + ∀B,A1,A2. R A1 A2 → R (@B.A1) (@B.A2). + +definition compatible_appl: predicate (relation term) ≝ λR. + ∀B1,B2. R B1 B2 → ∀A1,A2. R A1 A2 → + R (@B1.A1) (@B2.A2). + +lemma star_compatible_abst: ∀R. compatible_abst R → compatible_abst (star … R). +#R #HR #A1 #A2 #H elim H -A2 // /3 width=3/ +qed. + +lemma star_compatible_sn: ∀R. compatible_sn R → compatible_sn (star … R). +#R #HR #A #B1 #B2 #H elim H -B2 // /3 width=3/ +qed. + +lemma star_compatible_dx: ∀R. compatible_dx R → compatible_dx (star … R). +#R #HR #B #A1 #A2 #H elim H -A2 // /3 width=3/ +qed. + +lemma star_compatible_appl: ∀R. reflexive ? R → + compatible_appl R → compatible_appl (star … R). +#R #H1R #H2R #B1 #B2 #H elim H -B2 /3 width=1/ /3 width=5/ +qed. +*) diff --git a/matita/matita/contribs/lambda/term.ma b/matita/matita/contribs/lambda/term.ma deleted file mode 100644 index 2e08b861e..000000000 --- a/matita/matita/contribs/lambda/term.ma +++ /dev/null @@ -1,79 +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 *) -(* *) -(**************************************************************************) - -(* Initial invocation: - Patience on us to gain peace and perfection! - *) - -include "preamble.ma". - -(* TERM STRUCTURE ***********************************************************) - -(* Policy: term metavariables : A, B, C, D, M, N - depth metavariables: i, j -*) -inductive term: Type[0] ≝ -| VRef: nat → term (* variable reference by depth *) -| Abst: term → term (* function formation *) -| Appl: term → term → term (* function application *) -. - -interpretation "term construction (variable reference by index)" - 'VariableReferenceByIndex i = (VRef i). - -interpretation "term construction (abstraction)" - 'Abstraction A = (Abst A). - -interpretation "term construction (application)" - 'Application C A = (Appl C A). - -notation "hvbox( # term 90 i )" - non associative with precedence 90 - for @{ 'VariableReferenceByIndex $i }. - -notation "hvbox( 𝛌 . term 46 A )" - non associative with precedence 46 - for @{ 'Abstraction $A }. - -notation "hvbox( @ term 46 C . break term 46 A )" - non associative with precedence 46 - for @{ 'Application $C $A }. - -definition compatible_abst: predicate (relation term) ≝ λR. - ∀A1,A2. R A1 A2 → R (𝛌.A1) (𝛌.A2). - -definition compatible_sn: predicate (relation term) ≝ λR. - ∀A,B1,B2. R B1 B2 → R (@B1.A) (@B2.A). - -definition compatible_dx: predicate (relation term) ≝ λR. - ∀B,A1,A2. R A1 A2 → R (@B.A1) (@B.A2). - -definition compatible_appl: predicate (relation term) ≝ λR. - ∀B1,B2. R B1 B2 → ∀A1,A2. R A1 A2 → - R (@B1.A1) (@B2.A2). - -lemma star_compatible_abst: ∀R. compatible_abst R → compatible_abst (star … R). -#R #HR #A1 #A2 #H elim H -A2 // /3 width=3/ -qed. - -lemma star_compatible_sn: ∀R. compatible_sn R → compatible_sn (star … R). -#R #HR #A #B1 #B2 #H elim H -B2 // /3 width=3/ -qed. - -lemma star_compatible_dx: ∀R. compatible_dx R → compatible_dx (star … R). -#R #HR #B #A1 #A2 #H elim H -A2 // /3 width=3/ -qed. - -lemma star_compatible_appl: ∀R. reflexive ? R → - compatible_appl R → compatible_appl (star … R). -#R #H1R #H2R #B1 #B2 #H elim H -B2 /3 width=1/ /3 width=5/ -qed. diff --git a/matita/matita/contribs/lambda/terms/delifting_substitution.ma b/matita/matita/contribs/lambda/terms/delifting_substitution.ma new file mode 100644 index 000000000..7926c3948 --- /dev/null +++ b/matita/matita/contribs/lambda/terms/delifting_substitution.ma @@ -0,0 +1,154 @@ +(**************************************************************************) +(* ___ *) +(* ||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 "terms/lift.ma". + +(* DELIFTING SUBSTITUTION ***************************************************) + +(* Policy: depth (level) metavariables: d, e (as for lift) *) +let rec dsubst D d M on M ≝ match M with +[ VRef i ⇒ tri … i d (#i) (↑[i] D) (#(i-1)) +| Abst A ⇒ 𝛌. (dsubst D (d+1) A) +| Appl B A ⇒ @ (dsubst D d B). (dsubst D d A) +]. + +interpretation "delifting substitution" + 'DSubst D d M = (dsubst D d M). + +lemma dsubst_vref_lt: ∀i,d,D. i < d → [d ↙ D] #i = #i. +normalize /2 width=1/ +qed. + +lemma dsubst_vref_eq: ∀i,D. [i ↙ D] #i = ↑[i]D. +normalize // +qed. + +lemma dsubst_vref_gt: ∀i,d,D. d < i → [d ↙ D] #i = #(i-1). +normalize /2 width=1/ +qed. + +theorem dsubst_lift_le: ∀h,D,M,d1,d2. d2 ≤ d1 → + [d2 ↙ ↑[d1 - d2, h] D] ↑[d1 + 1, h] M = ↑[d1, h] [d2 ↙ D] M. +#h #D #M elim M -M +[ #i #d1 #d2 #Hd21 elim (lt_or_eq_or_gt i d2) #Hid2 + [ lapply (lt_to_le_to_lt … Hid2 Hd21) -Hd21 #Hid1 + >(dsubst_vref_lt … Hid2) >(lift_vref_lt … Hid1) >lift_vref_lt /2 width=1/ + | destruct >dsubst_vref_eq >lift_vref_lt /2 width=1/ + | >(dsubst_vref_gt … Hid2) -Hd21 elim (lt_or_ge (i-1) d1) #Hi1d1 + [ >(lift_vref_lt … Hi1d1) >lift_vref_lt /2 width=1/ + | lapply (ltn_to_ltO … Hid2) #Hi + >(lift_vref_ge … Hi1d1) >lift_vref_ge /2 width=1/ -Hi1d1 >plus_minus // /3 width=1/ + ] + ] +| normalize #A #IHA #d1 #d2 #Hd21 + lapply (IHA (d1+1) (d2+1) ?) -IHA /2 width=1/ +| normalize #B #A #IHB #IHA #d1 #d2 #Hd21 + >IHB -IHB // >IHA -IHA // +] +qed. + +theorem dsubst_lift_be: ∀h,D,M,d1,d2. d1 ≤ d2 → d2 ≤ d1 + h → + [d2 ↙ D] ↑[d1, h + 1] M = ↑[d1, h] M. +#h #D #M elim M -M +[ #i #d1 #d2 #Hd12 #Hd21 elim (lt_or_ge i d1) #Hid1 + [ lapply (lt_to_le_to_lt … Hid1 Hd12) -Hd12 -Hd21 #Hid2 + >(lift_vref_lt … Hid1) >(lift_vref_lt … Hid1) /2 width=1/ + | lapply (transitive_le … (i+h) Hd21 ?) -Hd12 -Hd21 /2 width=1/ #Hd2 + >(lift_vref_ge … Hid1) >(lift_vref_ge … Hid1) -Hid1 + >dsubst_vref_gt // /2 width=1/ + ] +| normalize #A #IHA #d1 #d2 #Hd12 #Hd21 + >IHA -IHA // /2 width=1/ +| normalize #B #A #IHB #IHA #d1 #d2 #Hd12 #Hd21 + >IHB -IHB // >IHA -IHA // +] +qed. + +theorem dsubst_lift_ge: ∀h,D,M,d1,d2. d1 + h ≤ d2 → + [d2 ↙ D] ↑[d1, h] M = ↑[d1, h] [d2 - h ↙ D] M. +#h #D #M elim M -M +[ #i #d1 #d2 #Hd12 elim (lt_or_eq_or_gt i (d2-h)) #Hid2h + [ >(dsubst_vref_lt … Hid2h) elim (lt_or_ge i d1) #Hid1 + [ lapply (lt_to_le_to_lt … (d1+h) Hid1 ?) -Hid2h // #Hid1h + lapply (lt_to_le_to_lt … Hid1h Hd12) -Hid1h -Hd12 #Hid2 + >(lift_vref_lt … Hid1) -Hid1 /2 width=1/ + | >(lift_vref_ge … Hid1) -Hid1 -Hd12 /3 width=1/ + ] + | destruct elim (le_inv_plus_l … Hd12) -Hd12 #Hd12 #Hhd2 + >dsubst_vref_eq >lift_vref_ge // >lift_lift_be // (dsubst_vref_gt … Hid2h) + >lift_vref_ge /2 width=1/ >lift_vref_ge /2 width=1/ -Hid1 + >dsubst_vref_gt /2 width=1/ -Hid2h >plus_minus // + ] +| normalize #A #IHA #d1 #d2 #Hd12 + elim (le_inv_plus_l … Hd12) #_ #Hhd2 + >IHA -IHA /2 width=1/ IHB -IHB // >IHA -IHA // +] +qed. + +theorem dsubst_dsubst_ge: ∀D1,D2,M,d1,d2. d1 ≤ d2 → + [d2 ↙ D2] [d1 ↙ D1] M = [d1 ↙ [d2 - d1 ↙ D2] D1] [d2 + 1 ↙ D2] M. +#D1 #D2 #M elim M -M +[ #i #d1 #d2 #Hd12 elim (lt_or_eq_or_gt i d1) #Hid1 + [ lapply (lt_to_le_to_lt … Hid1 Hd12) -Hd12 #Hid2 + >(dsubst_vref_lt … Hid1) >(dsubst_vref_lt … Hid2) >dsubst_vref_lt /2 width=1/ + | destruct >dsubst_vref_eq >dsubst_vref_lt /2 width=1/ + | >(dsubst_vref_gt … Hid1) elim (lt_or_eq_or_gt i (d2+1)) #Hid2 + [ lapply (ltn_to_ltO … Hid1) #Hi + >(dsubst_vref_lt … Hid2) >dsubst_vref_lt /2 width=1/ + | destruct /2 width=1/ + | lapply (le_to_lt_to_lt (d1+1) … Hid2) -Hid1 /2 width=1/ -Hd12 #Hid1 + >(dsubst_vref_gt … Hid2) >dsubst_vref_gt /2 width=1/ + >dsubst_vref_gt // /2 width=1/ + ] + ] +| normalize #A #IHA #d1 #d2 #Hd12 + lapply (IHA (d1+1) (d2+1) ?) -IHA /2 width=1/ +| normalize #B #A #IHB #IHA #d1 #d2 #Hd12 + >IHB -IHB // >IHA -IHA // +] +qed. + +theorem dsubst_dsubst_lt: ∀D1,D2,M,d1,d2. d2 < d1 → + [d2 ↙ [d1 - d2 -1 ↙ D1] D2] [d1 ↙ D1] M = [d1 - 1 ↙ D1] [d2 ↙ D2] M. +#D1 #D2 #M #d1 #d2 #Hd21 +lapply (ltn_to_ltO … Hd21) #Hd1 +>dsubst_dsubst_ge in ⊢ (???%); /2 width=1/ distributive_times_plus normalize /2 width=1/ +qed-. + +lemma lsred_lift: ∀p. liftable (lsred p). +#p #h #M1 #M2 #H elim H -p -M1 -M2 normalize /2 width=1/ +#B #A #d dsubst_dsubst_ge // +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 ] (**) (* simplify line *) + #C1 #C2 #HC12 #H #HN2 destruct /3 width=1/ +| #p #B1 #B2 #A #_ #IHB12 #N2 #H elim (lsred_inv_sn … H ??) -H [3: // |2: skip ] (**) (* simplify line *) + #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 ] (**) (* simplify line *) + #D #C1 #C2 #HC12 #H #HN2 destruct /3 width=1/ +] +qed-. diff --git a/matita/matita/contribs/lambda/terms/length.ma b/matita/matita/contribs/lambda/terms/length.ma new file mode 100644 index 000000000..81ce2e379 --- /dev/null +++ b/matita/matita/contribs/lambda/terms/length.ma @@ -0,0 +1,31 @@ +(**************************************************************************) +(* ___ *) +(* ||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 "terms/lift.ma". + +(* LENGTH *******************************************************************) + +(* Note: this gives the number of abstractions and applications in M *) +let rec length M on M ≝ match M with +[ VRef i ⇒ 0 +| Abst A ⇒ length A + 1 +| Appl B A ⇒ (length B) + (length A) + 1 +]. + +interpretation "term length" + 'card M = (length M). + +lemma length_lift: ∀h,M,d. |↑[d, h] M| = |M|. +#h #M elim M -M normalize // +qed. diff --git a/matita/matita/contribs/lambda/terms/lift.ma b/matita/matita/contribs/lambda/terms/lift.ma new file mode 100644 index 000000000..62da59661 --- /dev/null +++ b/matita/matita/contribs/lambda/terms/lift.ma @@ -0,0 +1,257 @@ +(**************************************************************************) +(* ___ *) +(* ||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 "terms/term.ma". + +(* RELOCATION ***************************************************************) + +(* Policy: level metavariables : d, e + height metavariables: h, k +*) +(* Note: indexes start at zero *) +let rec lift h d M on M ≝ match M with +[ VRef i ⇒ #(tri … i d i (i + h) (i + h)) +| Abst A ⇒ 𝛌. (lift h (d+1) A) +| Appl B A ⇒ @(lift h d B). (lift h d A) +]. + +interpretation "relocation" 'Lift h d M = (lift h d M). + +lemma lift_vref_lt: ∀d,h,i. i < d → ↑[d, h] #i = #i. +normalize /3 width=1/ +qed. + +lemma lift_vref_ge: ∀d,h,i. d ≤ i → ↑[d, h] #i = #(i+h). +#d #h #i #H elim (le_to_or_lt_eq … H) -H +normalize // /3 width=1/ +qed. + +lemma lift_id: ∀M,d. ↑[d, 0] M = M. +#M elim M -M +[ #i #d elim (lt_or_ge i d) /2 width=1/ +| /3 width=1/ +| /3 width=1/ +] +qed. + +lemma lift_inv_vref_lt: ∀j,d. j < d → ∀h,M. ↑[d, h] M = #j → M = #j. +#j #d #Hjd #h * normalize +[ #i elim (lt_or_eq_or_gt i d) #Hid + [ >(tri_lt ???? … Hid) -Hid -Hjd // + | #H destruct >tri_eq in Hjd; #H + elim (plus_lt_false … H) + | >(tri_gt ???? … Hid) + lapply (transitive_lt … Hjd Hid) -d #H #H0 destruct + elim (plus_lt_false … H) + ] +| #A #H destruct +| #B #A #H destruct +] +qed. + +lemma lift_inv_vref_ge: ∀j,d. d ≤ j → ∀h,M. ↑[d, h] M = #j → + d + h ≤ j ∧ M = #(j-h). +#j #d #Hdj #h * normalize +[ #i elim (lt_or_eq_or_gt i d) #Hid + [ >(tri_lt ???? … Hid) #H destruct + lapply (le_to_lt_to_lt … Hdj Hid) -Hdj -Hid #H + elim (lt_refl_false … H) + | #H -Hdj destruct /2 width=1/ + | >(tri_gt ???? … Hid) #H -Hdj destruct /4 width=1/ + ] +| #A #H destruct +| #B #A #H destruct +] +qed-. + +lemma lift_inv_vref_be: ∀j,d,h. d ≤ j → j < d + h → ∀M. ↑[d, h] M = #j → ⊥. +#j #d #h #Hdj #Hjdh #M #H elim (lift_inv_vref_ge … H) -H // -Hdj #Hdhj #_ -M +lapply (lt_to_le_to_lt … Hjdh Hdhj) -d -h #H +elim (lt_refl_false … H) +qed-. + +lemma lift_inv_vref_ge_plus: ∀j,d,h. d + h ≤ j → + ∀M. ↑[d, h] M = #j → M = #(j-h). +#j #d #h #Hdhj #M #H elim (lift_inv_vref_ge … H) -H // -M /2 width=2/ +qed. + +lemma lift_inv_abst: ∀C,d,h,M. ↑[d, h] M = 𝛌.C → + ∃∃A. ↑[d+1, h] A = C & M = 𝛌.A. +#C #d #h * normalize +[ #i #H destruct +| #A #H destruct /2 width=3/ +| #B #A #H destruct +] +qed-. + +lemma lift_inv_appl: ∀D,C,d,h,M. ↑[d, h] M = @D.C → + ∃∃B,A. ↑[d, h] B = D & ↑[d, h] A = C & M = @B.A. +#D #C #d #h * normalize +[ #i #H destruct +| #A #H destruct +| #B #A #H destruct /2 width=5/ +] +qed-. + +theorem lift_lift_le: ∀h1,h2,M,d1,d2. d2 ≤ d1 → + ↑[d2, h2] ↑[d1, h1] M = ↑[d1 + h2, h1] ↑[d2, h2] M. +#h1 #h2 #M elim M -M +[ #i #d1 #d2 #Hd21 elim (lt_or_ge i d2) #Hid2 + [ lapply (lt_to_le_to_lt … Hid2 Hd21) -Hd21 #Hid1 + >(lift_vref_lt … Hid1) >(lift_vref_lt … Hid2) + >lift_vref_lt // /2 width=1/ + | >(lift_vref_ge … Hid2) elim (lt_or_ge i d1) #Hid1 + [ >(lift_vref_lt … Hid1) >(lift_vref_ge … Hid2) + >lift_vref_lt // -d2 /2 width=1/ + | >(lift_vref_ge … Hid1) >lift_vref_ge /2 width=1/ + >lift_vref_ge // /2 width=1/ + ] + ] +| normalize #A #IHA #d1 #d2 #Hd21 >IHA // /2 width=1/ +| normalize #B #A #IHB #IHA #d1 #d2 #Hd21 >IHB >IHA // +] +qed. + +theorem lift_lift_be: ∀h1,h2,M,d1,d2. d1 ≤ d2 → d2 ≤ d1 + h1 → + ↑[d2, h2] ↑[d1, h1] M = ↑[d1, h1 + h2] M. +#h1 #h2 #M elim M -M +[ #i #d1 #d2 #Hd12 #Hd21 elim (lt_or_ge i d1) #Hid1 + [ lapply (lt_to_le_to_lt … Hid1 Hd12) -Hd12 -Hd21 #Hid2 + >(lift_vref_lt … Hid1) >(lift_vref_lt … Hid1) /2 width=1/ + | lapply (transitive_le … (i+h1) Hd21 ?) -Hd21 -Hd12 /2 width=1/ #Hd2 + >(lift_vref_ge … Hid1) >(lift_vref_ge … Hid1) /2 width=1/ + ] +| normalize #A #IHA #d1 #d2 #Hd12 #Hd21 >IHA // /2 width=1/ +| normalize #B #A #IHB #IHA #d1 #d2 #Hd12 #Hd21 >IHB >IHA // +] +qed. + +theorem lift_lift_ge: ∀h1,h2,M,d1,d2. d1 + h1 ≤ d2 → + ↑[d2, h2] ↑[d1, h1] M = ↑[d1, h1] ↑[d2 - h1, h2] M. +#h1 #h2 #M #d1 #d2 #Hd12 +>(lift_lift_le h2 h1) /2 width=1/ (lift_vref_lt … Hid) in H; #H + >(lift_inv_vref_lt … Hid … H) -M2 -d -h // + | >(lift_vref_ge … Hid) in H; #H + >(lift_inv_vref_ge_plus … H) -M2 // /2 width=1/ + ] +| normalize #A1 #IHA1 #M2 #d #H + elim (lift_inv_abst … H) -H #A2 #HA12 #H destruct + >(IHA1 … HA12) -IHA1 -A2 // +| normalize #B1 #A1 #IHB1 #IHA1 #M2 #d #H + elim (lift_inv_appl … H) -H #B2 #A2 #HB12 #HA12 #H destruct + >(IHB1 … HB12) -IHB1 -B2 >(IHA1 … HA12) -IHA1 -A2 // +] +qed-. + +theorem lift_inv_lift_le: ∀h1,h2,M1,M2,d1,d2. d2 ≤ d1 → + ↑[d2, h2] M2 = ↑[d1 + h2, h1] M1 → + ∃∃M. ↑[d1, h1] M = M2 & ↑[d2, h2] M = M1. +#h1 #h2 #M1 elim M1 -M1 +[ #i #M2 #d1 #d2 #Hd21 elim (lt_or_ge i (d1+h2)) #Hid1 + [ >(lift_vref_lt … Hid1) elim (lt_or_ge i d2) #Hid2 #H + [ lapply (lt_to_le_to_lt … Hid2 Hd21) -Hd21 -Hid1 #Hid1 + >(lift_inv_vref_lt … Hid2 … H) -M2 /3 width=3/ + | elim (lift_inv_vref_ge … H) -H -Hd21 // -Hid2 #Hdh2i #H destruct + elim (le_inv_plus_l … Hdh2i) -Hdh2i #Hd2i #Hh2i + @(ex2_intro … (#(i-h2))) [ /4 width=1/ ] -Hid1 + >lift_vref_ge // -Hd2i /3 width=1/ (**) (* auto: needs some help here *) + ] + | elim (le_inv_plus_l … Hid1) #Hd1i #Hh2i + lapply (transitive_le (d2+h2) … Hid1) /2 width=1/ -Hd21 #Hdh2i + elim (le_inv_plus_l … Hdh2i) #Hd2i #_ + >(lift_vref_ge … Hid1) #H -Hid1 + >(lift_inv_vref_ge_plus … H) -H /2 width=3/ -Hdh2i + @(ex2_intro … (#(i-h2))) (**) (* auto: needs some help here *) + [ >lift_vref_ge // -Hd1i /3 width=1/ + | >lift_vref_ge // -Hd2i -Hd1i /3 width=1/ + ] + ] +| normalize #A1 #IHA1 #M2 #d1 #d2 #Hd21 #H + elim (lift_inv_abst … H) -H >plus_plus_comm_23 #A2 #HA12 #H destruct + elim (IHA1 … HA12) -IHA1 -HA12 /2 width=1/ -Hd21 #A #HA2 #HA1 + @(ex2_intro … (𝛌.A)) normalize // +| normalize #B1 #A1 #IHB1 #IHA1 #M2 #d1 #d2 #Hd21 #H + elim (lift_inv_appl … H) -H #B2 #A2 #HB12 #HA12 #H destruct + elim (IHB1 … HB12) -IHB1 -HB12 // #B #HB2 #HB1 + elim (IHA1 … HA12) -IHA1 -HA12 // -Hd21 #A #HA2 #HA1 + @(ex2_intro … (@B.A)) normalize // +] +qed-. + +theorem lift_inv_lift_be: ∀h1,h2,M1,M2,d1,d2. d1 ≤ d2 → d2 ≤ d1 + h1 → + ↑[d2, h2] M2 = ↑[d1, h1 + h2] M1 → ↑[d1, h1] M1 = M2. +#h1 #h2 #M1 elim M1 -M1 +[ #i #M2 #d1 #d2 #Hd12 #Hd21 elim (lt_or_ge i d1) #Hid1 + [ lapply (lt_to_le_to_lt … Hid1 Hd12) -Hd12 -Hd21 #Hid2 + >(lift_vref_lt … Hid1) #H >(lift_inv_vref_lt … Hid2 … H) -h2 -M2 -d2 /2 width=1/ + | lapply (transitive_le … (i+h1) Hd21 ?) -Hd12 -Hd21 /2 width=1/ #Hd2 + >(lift_vref_ge … Hid1) #H >(lift_inv_vref_ge_plus … H) -M2 /2 width=1/ + ] +| normalize #A1 #IHA1 #M2 #d1 #d2 #Hd12 #Hd21 #H + elim (lift_inv_abst … H) -H #A #HA12 #H destruct + >(IHA1 … HA12) -IHA1 -HA12 // /2 width=1/ +| normalize #B1 #A1 #IHB1 #IHA1 #M2 #d1 #d2 #Hd12 #Hd21 #H + elim (lift_inv_appl … H) -H #B #A #HB12 #HA12 #H destruct + >(IHB1 … HB12) -IHB1 -HB12 // >(IHA1 … HA12) -IHA1 -HA12 // +] +qed-. + +theorem lift_inv_lift_ge: ∀h1,h2,M1,M2,d1,d2. d1 + h1 ≤ d2 → + ↑[d2, h2] M2 = ↑[d1, h1] M1 → + ∃∃M. ↑[d1, h1] M = M2 & ↑[d2 - h1, h2] M = M1. +#h1 #h2 #M1 #M2 #d1 #d2 #Hd12 #H +elim (le_inv_plus_l … Hd12) -Hd12 #Hd12 #Hh1d2 +lapply (sym_eq term … H) -H >(plus_minus_m_m … Hh1d2) in ⊢ (???%→?); -Hh1d2 #H +elim (lift_inv_lift_le … Hd12 … H) -H -Hd12 /2 width=3/ +qed-. + +definition liftable: predicate (relation term) ≝ λR. + ∀h,M1,M2. R M1 M2 → ∀d. R (↑[d, h] M1) (↑[d, h] M2). + +definition deliftable_sn: predicate (relation term) ≝ λR. + ∀h,N1,N2. R N1 N2 → ∀d,M1. ↑[d, h] M1 = N1 → + ∃∃M2. R M1 M2 & ↑[d, h] M2 = N2. + +lemma star_liftable: ∀R. liftable R → liftable (star … R). +#R #HR #h #M1 #M2 #H elim H -M2 // /3 width=3/ +qed. + +lemma star_deliftable_sn: ∀R. deliftable_sn R → deliftable_sn (star … R). +#R #HR #h #N1 #N2 #H elim H -N2 /2 width=3/ +#N #N2 #_ #HN2 #IHN1 #d #M1 #HMN1 +elim (IHN1 … HMN1) -N1 #M #HM1 #HMN +elim (HR … HN2 … HMN) -N /3 width=3/ +qed-. + +lemma lstar_liftable: ∀S,R. (∀a. liftable (R a)) → + ∀l. liftable (lstar S … R l). +#S #R #HR #l #h #M1 #M2 #H +@(lstar_ind_l ????????? H) -l -M1 // /3 width=3/ +qed. + +lemma lstar_deliftable_sn: ∀S,R. (∀a. deliftable_sn (R a)) → + ∀l. deliftable_sn (lstar S … R l). +#S #R #HR #l #h #N1 #N2 #H +@(lstar_ind_l ????????? H) -l -N1 /2 width=3/ +#a #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/terms/multiplicity.ma b/matita/matita/contribs/lambda/terms/multiplicity.ma new file mode 100644 index 000000000..97306ef5d --- /dev/null +++ b/matita/matita/contribs/lambda/terms/multiplicity.ma @@ -0,0 +1,52 @@ +(**************************************************************************) +(* ___ *) +(* ||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 "terms/delifting_substitution.ma". + +(* MULTIPLICITY *************************************************************) + +(* Note: this gives the number of variable references in M *) +let rec mult M on M ≝ match M with +[ VRef i ⇒ 1 +| Abst A ⇒ mult A +| Appl B A ⇒ (mult B) + (mult A) +]. + +interpretation "term multiplicity" + 'Multiplicity M = (mult M). + +notation "hvbox( ♯{ term 46 M } )" + non associative with precedence 90 + for @{ 'Multiplicity $M }. + +lemma mult_positive: ∀M. 0 < ♯{M}. +#M elim M -M // /2 width=1/ +qed. + +lemma mult_lift: ∀h,M,d. ♯{↑[d, h] M} = ♯{M}. +#h #M elim M -M normalize // +qed. + +theorem mult_dsubst: ∀D,M,d. ♯{[d ↙ D] M} ≤ ♯{M} * ♯{D}. +#D #M elim M -M +[ #i #d elim (lt_or_eq_or_gt i d) #Hid + [ >(dsubst_vref_lt … Hid) normalize // + | destruct >dsubst_vref_eq normalize // + | >(dsubst_vref_gt … Hid) normalize // + ] +| normalize // +| normalize #B #A #IHB #IHA #d + >distributive_times_plus_r /2 width=1/ +] +qed. diff --git a/matita/matita/contribs/lambda/terms/parallel_computation.ma b/matita/matita/contribs/lambda/terms/parallel_computation.ma new file mode 100644 index 000000000..4f93f90a7 --- /dev/null +++ b/matita/matita/contribs/lambda/terms/parallel_computation.ma @@ -0,0 +1,87 @@ +(**************************************************************************) +(* ___ *) +(* ||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 "terms/parallel_reduction.ma". + +(* PARALLEL COMPUTATION (MULTISTEP) *****************************************) + +definition preds: relation term ≝ star … pred. + +interpretation "parallel computation" + 'ParRedStar M N = (preds M N). + +notation "hvbox( M ⤇* break term 46 N )" + non associative with precedence 45 + for @{ 'ParRedStar $M $N }. + +lemma preds_refl: reflexive … preds. +// +qed. + +lemma preds_step_sn: ∀M1,M. M1 ⤇ M → ∀M2. M ⤇* M2 → M1 ⤇* M2. +/2 width=3/ +qed-. + +lemma preds_step_dx: ∀M1,M. M1 ⤇* M → ∀M2. M ⤇ M2 → M1 ⤇* M2. +/2 width=3/ +qed-. + +lemma preds_step_rc: ∀M1,M2. M1 ⤇ M2 → M1 ⤇* M2. +/2 width=1/ +qed. + +lemma preds_compatible_abst: compatible_abst preds. +/3 width=1/ +qed. + +lemma preds_compatible_sn: compatible_sn preds. +/3 width=1/ +qed. + +lemma preds_compatible_dx: compatible_dx preds. +/3 width=1/ +qed. + +lemma preds_compatible_appl: compatible_appl preds. +/3 width=1/ +qed. + +lemma preds_lift: liftable preds. +/2 width=1/ +qed. + +lemma preds_inv_lift: deliftable_sn preds. +/3 width=3 by star_deliftable_sn, pred_inv_lift/ +qed-. + +lemma preds_dsubst_dx: dsubstable_dx preds. +/2 width=1/ +qed. + +lemma preds_dsubst: dsubstable preds. +/2 width=1/ +qed. + +theorem preds_trans: transitive … preds. +/2 width=3 by trans_star/ +qed-. + +lemma preds_strip: ∀M0,M1. M0 ⤇* M1 → ∀M2. M0 ⤇ M2 → + ∃∃M. M1 ⤇ M & M2 ⤇* M. +/3 width=3 by star_strip, pred_conf/ +qed-. + +theorem preds_conf: confluent … preds. +/3 width=3 by star_confluent, pred_conf/ +qed-. diff --git a/matita/matita/contribs/lambda/terms/parallel_reduction.ma b/matita/matita/contribs/lambda/terms/parallel_reduction.ma new file mode 100644 index 000000000..a9190151b --- /dev/null +++ b/matita/matita/contribs/lambda/terms/parallel_reduction.ma @@ -0,0 +1,156 @@ +(**************************************************************************) +(* ___ *) +(* ||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 "terms/length.ma". +include "terms/labeled_sequential_reduction.ma". + +(* PARALLEL REDUCTION (SINGLE STEP) *****************************************) + +(* Note: the application "(A B)" is represented by "@B.A" + as for labelled sequential reduction +*) +inductive pred: relation term ≝ +| pred_vref: ∀i. pred (#i) (#i) +| 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" + 'ParRed M N = (pred M N). + +notation "hvbox( M ⤇ break term 46 N )" + non associative with precedence 45 + for @{ 'ParRed $M $N }. + +lemma pred_refl: reflexive … pred. +#M elim M -M // /2 width=1/ +qed. + +lemma pred_inv_vref: ∀M,N. M ⤇ N → ∀i. #i = M → #i = N. +#M #N * -M -N // +[ #A1 #A2 #_ #i #H destruct +| #B1 #B2 #A1 #A2 #_ #_ #i #H destruct +| #B1 #B2 #A1 #A2 #_ #_ #i #H destruct +] +qed-. + +lemma pred_inv_abst: ∀M,N. M ⤇ N → ∀A. 𝛌.A = M → + ∃∃C. A ⤇ C & 𝛌.C = N. +#M #N * -M -N +[ #i #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-. + +lemma pred_inv_appl: ∀M,N. M ⤇ N → ∀B,A. @B.A = M → + (∃∃D,C. B ⤇ D & A ⤇ C & @D.C = N) ∨ + ∃∃A0,D,C0. B ⤇ D & A0 ⤇ C0 & 𝛌.A0 = A & [↙D]C0 = N. +#M #N * -M -N +[ #i #B0 #A0 #H destruct +| #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/ +#B1 #B2 #A1 #A2 #_ #_ #IHB12 #IHC12 #d (dsubst_vref_lt … Hid) >(dsubst_vref_lt … Hid) // + | destruct >dsubst_vref_eq >dsubst_vref_eq /2 width=1/ + | >(dsubst_vref_gt … Hid) >(dsubst_vref_gt … Hid) // + ] +| normalize /2 width=1/ +| normalize /2 width=1/ +| normalize #B1 #B2 #A1 #A2 #_ #_ #IHB12 #IHC12 #d + >dsubst_dsubst_ge // /2 width=1/ +] +qed. + +lemma pred_conf1_vref: ∀i. confluent1 … pred (#i). +#i #M1 #H1 #M2 #H2 +<(pred_inv_vref … H1) -H1 [3: // |2: skip ] (**) (* simplify line *) +<(pred_inv_vref … H2) -H2 [3: // |2: skip ] (**) (* simplify line *) +/2 width=3/ +qed-. + +lemma pred_conf1_abst: ∀A. confluent1 … pred A → confluent1 … pred (𝛌.A). +#A #IH #M1 #H1 #M2 #H2 +elim (pred_inv_abst … H1 ??) -H1 [3: // |2: skip ] #A1 #HA1 #H destruct (**) (* simplify line *) +elim (pred_inv_abst … H2 ??) -H2 [3: // |2: skip ] #A2 #HA2 #H destruct (**) (* simplify line *) +elim (IH … HA1 … HA2) -A /3 width=3/ +qed-. + +lemma pred_conf1_appl_beta: ∀B,B1,B2,C,C2,M1. + (∀M0. |M0| < |B|+|𝛌.C|+1 → confluent1 ? pred M0) → (**) (* ? needed in place of … *) + B ⤇ B1 → B ⤇ B2 → 𝛌.C ⤇ M1 → C ⤇ C2 → + ∃∃M. @B1.M1 ⤇ M & [↙B2]C2 ⤇ M. +#B #B1 #B2 #C #C2 #M1 #IH #HB1 #HB2 #H1 #HC2 +elim (pred_inv_abst … H1 ??) -H1 [3: // |2: skip ] #C1 #HC1 #H destruct (**) (* simplify line *) +elim (IH B … HB1 … HB2) -HB1 -HB2 // +elim (IH C … HC1 … HC2) normalize // -B -C /3 width=5/ +qed-. + +theorem pred_conf: confluent … pred. +#M @(f_ind … length … M) -M #n #IH * normalize +[ /2 width=3 by pred_conf1_vref/ +| /3 width=4 by pred_conf1_abst/ +| #B #A #H #M1 #H1 #M2 #H2 destruct + elim (pred_inv_appl … H1 ???) -H1 [5: // |2,3: skip ] * (**) (* simplify line *) + elim (pred_inv_appl … H2 ???) -H2 [5,10: // |2,3,7,8: skip ] * (**) (* simplify line *) + [ #B2 #A2 #HB2 #HA2 #H2 #B1 #A1 #HB1 #HA1 #H1 destruct + elim (IH A … HA1 … HA2) -HA1 -HA2 // + elim (IH B … HB1 … HB2) // -A -B /3 width=5/ + | #C #B2 #C2 #HB2 #HC2 #H2 #HM2 #B1 #N #HB1 #H #HM1 destruct + @(pred_conf1_appl_beta … IH) // (**) (* /2 width=7 by pred_conf1_appl_beta/ does not work *) + | #B2 #N #B2 #H #HM2 #C #B1 #C1 #HB1 #HC1 #H1 #HM1 destruct + @ex2_commute @(pred_conf1_appl_beta … IH) // + | #C #B2 #C2 #HB2 #HC2 #H2 #HM2 #C0 #B1 #C1 #HB1 #HC1 #H1 #HM1 destruct + elim (IH B … HB1 … HB2) -HB1 -HB2 // + elim (IH C … HC1 … HC2) normalize // -B -C /3 width=5/ + ] +] +qed-. + +lemma lsred_pred: ∀p,M,N. M ↦[p] N → M ⤇ N. +#p #M #N #H elim H -p -M -N /2 width=1/ +qed. diff --git a/matita/matita/contribs/lambda/terms/pointer.ma b/matita/matita/contribs/lambda/terms/pointer.ma new file mode 100644 index 000000000..79b269351 --- /dev/null +++ b/matita/matita/contribs/lambda/terms/pointer.ma @@ -0,0 +1,54 @@ +(**************************************************************************) +(* ___ *) +(* ||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 "terms/term.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 whd" when is not under an abstraction nor in the lefr argument of an application *) +definition in_whd: predicate ptr ≝ All … is_dx. + +lemma in_whd_ind: ∀R:predicate ptr. R (◊) → + (∀p. in_whd p → R p → R (dx::p)) → + ∀p. in_whd p → R p. +#R #H #IH #p elim p -p // -H * +#p #IHp * #H1 #H2 destruct /3 width=1/ +qed-. + +definition compatible_rc: predicate (ptr→relation term) ≝ λR. + ∀p,A1,A2. R p A1 A2 → R (rc::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). + +definition compatible_dx: predicate (ptr→relation term) ≝ λR. + ∀p,B,A1,A2. R p A1 A2 → R (dx::p) (@B.A1) (@B.A2). diff --git a/matita/matita/contribs/lambda/terms/pointer_list.ma b/matita/matita/contribs/lambda/terms/pointer_list.ma new file mode 100644 index 000000000..c1e710649 --- /dev/null +++ b/matita/matita/contribs/lambda/terms/pointer_list.ma @@ -0,0 +1,54 @@ +(**************************************************************************) +(* ___ *) +(* ||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 "terms/pointer.ma". + +(* POINTER LIST *************************************************************) + +(* Policy: pointer list metavariables: r, s *) +definition ptrl: Type[0] ≝ list ptr. + +(* Note: a "whd" computation contracts just redexes in the whd *) +definition is_whd: predicate ptrl ≝ All … in_whd. + +lemma is_whd_dx: ∀s. is_whd s → is_whd (dx:::s). +#s elim s -s // +#p #s #IHs * /3 width=1/ +qed. + +lemma is_whd_append: ∀r. is_whd r → ∀s. is_whd s → is_whd (r@s). +#r elim r -r // +#q #r #IHr * /3 width=1/ +qed. + +definition ho_compatible_rc: predicate (ptrl→relation term) ≝ λR. + ∀s,A1,A2. R s A1 A2 → R (rc:::s) (𝛌.A1) (𝛌.A2). + +definition ho_compatible_sn: predicate (ptrl→relation term) ≝ λR. + ∀s,B1,B2,A. R s B1 B2 → R (sn:::s) (@B1.A) (@B2.A). + +definition ho_compatible_dx: predicate (ptrl→relation term) ≝ λR. + ∀s,B,A1,A2. R s A1 A2 → R (dx:::s) (@B.A1) (@B.A2). + +lemma lstar_compatible_rc: ∀R. compatible_rc R → ho_compatible_rc (lstar … R). +#R #HR #s #A1 #A2 #H @(lstar_ind_l ????????? H) -s -A1 // /3 width=3/ +qed. + +lemma lstar_compatible_sn: ∀R. compatible_sn R → ho_compatible_sn (lstar … R). +#R #HR #s #B1 #B2 #A #H @(lstar_ind_l ????????? H) -s -B1 // /3 width=3/ +qed. + +lemma lstar_compatible_dx: ∀R. compatible_dx R → ho_compatible_dx (lstar … R). +#R #HR #s #B #A1 #A2 #H @(lstar_ind_l ????????? H) -s -A1 // /3 width=3/ +qed. diff --git a/matita/matita/contribs/lambda/terms/pointer_list_standard.ma b/matita/matita/contribs/lambda/terms/pointer_list_standard.ma new file mode 100644 index 000000000..0c3cc2364 --- /dev/null +++ b/matita/matita/contribs/lambda/terms/pointer_list_standard.ma @@ -0,0 +1,52 @@ +(**************************************************************************) +(* ___ *) +(* ||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 "terms/pointer_list.ma". +include "terms/pointer_order.ma". + +(* STANDARD POINTER LIST ****************************************************) + +(* Note: to us, a "normal" computation contracts redexes in non-decreasing positions *) +definition is_standard: predicate ptrl ≝ Allr … ple. + +lemma is_standard_compatible: ∀c,s. is_standard s → is_standard (c:::s). +#c #s elim s -s // #p * // +#q #s #IHs * /3 width=1/ +qed. + +lemma is_standard_cons: ∀p,s. is_standard s → is_standard ((dx::p)::sn:::s). +#p #s elim s -s // #q1 * /2 width=1/ +#q2 #s #IHs * /4 width=1/ +qed. + +lemma is_standard_append: ∀r. is_standard r → ∀s. is_standard s → is_standard ((dx:::r)@sn:::s). +#r elim r -r /3 width=1/ #p * /2 width=1/ +#q #r #IHr * /3 width=1/ +qed. + +theorem is_whd_is_standard: ∀s. is_whd s → is_standard s. +#s elim s -s // #p * // +#q #s #IHs * /3 width=1/ +qed. + +lemma is_standard_in_whd: ∀p. in_whd p → ∀s. is_standard s → is_standard (p::s). +#p #Hp * // /3 width=1/ +qed. + +theorem is_whd_is_standard_trans: ∀r. is_whd r → ∀s. is_standard s → is_standard (r@s). +#r elim r -r // #p * +[ #_ * /2 width=1/ +| #q #r #IHr * /3 width=1/ +] +qed. diff --git a/matita/matita/contribs/lambda/terms/pointer_order.ma b/matita/matita/contribs/lambda/terms/pointer_order.ma new file mode 100644 index 000000000..1ead95b99 --- /dev/null +++ b/matita/matita/contribs/lambda/terms/pointer_order.ma @@ -0,0 +1,148 @@ +(**************************************************************************) +(* ___ *) +(* ||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 "terms/pointer.ma". + +(* POINTER ORDER ************************************************************) + +(* Note: precedence relation on redex pointers: p ≺ q + 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 (rc::p) (sn::q) +| pprec_comp: ∀c,p,q. pprec p q → pprec (c::p) (c::q) +| pprec_skip: pprec (dx::◊) ◊ +. + +interpretation "'precedes' on pointers" + 'prec p q = (pprec p q). + +(* Note: this should go to core_notation *) +notation "hvbox(a break ≺ b)" + non associative with precedence 45 + for @{ 'prec $a $b }. + +lemma pprec_fwd_in_whd: ∀p,q. p ≺ q → in_whd q → in_whd 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-. + +(* Note: this is p < q *) +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. + +interpretation "'less or equal to' on redex pointers" + 'leq p q = (ple p q). + +lemma ple_step_rc: ∀p,q. p ≺ q → p ≤ q. +/2 width=1/ +qed. + +lemma ple_step_sn: ∀p1,p,p2. p1 ≺ p → p ≤ p2 → p1 ≤ p2. +/2 width=3/ +qed-. + +lemma ple_rc: ∀p,q. dx::p ≤ rc::q. +/2 width=1/ +qed. + +lemma ple_sn: ∀p,q. rc::p ≤ sn::q. +/2 width=1/ +qed. + +lemma ple_skip: dx::◊ ≤ ◊. +/2 width=1/ +qed. + +lemma ple_nil: ∀p. ◊ ≤ p. +* // /2 width=1/ +qed. + +lemma ple_comp: ∀p1,p2. p1 ≤ p2 → ∀c. (c::p1) ≤ (c::p2). +#p1 #p2 #H elim H -p2 // /3 width=3/ +qed. + +lemma ple_skip_ple: ∀p. p ≤ ◊ → dx::p ≤ ◊. +#p #H @(star_ind_l ??????? H) -p // +#p #q #Hpq #_ #H @(ple_step_sn … H) -H /2 width=1/ +qed. + +theorem ple_trans: transitive … ple. +/2 width=3/ +qed-. + +lemma ple_cons: ∀p,q. dx::p ≤ sn::q. +#p #q +@(ple_trans … (rc::q)) /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_whd_ple_nil: ∀p. in_whd p → p ≤ ◊. +#p #H @(in_whd_ind … H) -p // /2 width=1/ +qed. + +theorem in_whd_ple: ∀p. in_whd p → ∀q. p ≤ q. +#p #H @(in_whd_ind … H) -p // +#p #_ #IHp * /3 width=1/ * #q /2 width=1/ +qed. + +lemma ple_nil_inv_in_whd: ∀p. p ≤ ◊ → in_whd p. +#p #H @(star_ind_l ??????? H) -p // /2 width=3 by pprec_fwd_in_whd/ +qed-. + +lemma ple_inv_in_whd: ∀p. (∀q. p ≤ q) → in_whd p. +/2 width=1 by ple_nil_inv_in_whd/ +qed-. diff --git a/matita/matita/contribs/lambda/terms/pointer_tree.ma b/matita/matita/contribs/lambda/terms/pointer_tree.ma new file mode 100644 index 000000000..fff98a856 --- /dev/null +++ b/matita/matita/contribs/lambda/terms/pointer_tree.ma @@ -0,0 +1,31 @@ +(**************************************************************************) +(* ___ *) +(* ||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 "terms/pointer_list.ma". + +(* POINTER TREE *************************************************************) + +(* Policy: pointer tree metavariables: P, Q *) +(* Note: this is a binary tree on pointer sequences *) +inductive ptrt: Type[0] ≝ +| tnil : ptrt +| tcons: ptrl → ptrt → ptrt → ptrt +. + +let rec length (P:ptrt) on P ≝ match P with +[ tnil ⇒ 0 +| tcons s Q1 Q2 ⇒ length Q2 + length Q1 + |s| +]. + +interpretation "pointer tree length" 'card P = (length P). diff --git a/matita/matita/contribs/lambda/terms/st_computation.ma b/matita/matita/contribs/lambda/terms/st_computation.ma new file mode 100644 index 000000000..1cd7a9f97 --- /dev/null +++ b/matita/matita/contribs/lambda/terms/st_computation.ma @@ -0,0 +1,214 @@ +(**************************************************************************) +(* ___ *) +(* ||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 "terms/labeled_sequential_computation.ma". +include "terms/pointer_list_standard.ma". + +(* KASHIMA'S "ST" COMPUTATION ***********************************************) + +(* Note: this is the "standard" computation of: + R. Kashima: "A proof of the Standization Theorem in λ-Calculus". Typescript note, (2000). +*) +inductive st: relation term ≝ +| st_vref: ∀s,M,i. is_whd s → M ↦*[s] #i → st M (#i) +| st_abst: ∀s,M,A1,A2. is_whd s → M ↦*[s] 𝛌.A1 → st A1 A2 → st M (𝛌.A2) +| st_appl: ∀s,M,B1,B2,A1,A2. is_whd s → M ↦*[s] @B1.A1 → st B1 B2 → st A1 A2 → st M (@B2.A2) +. + +interpretation "'st' computation" + 'Std M N = (st M N). + +notation "hvbox( M ⓢ⤇* break term 46 N )" + non associative with precedence 45 + for @{ 'Std $M $N }. + +lemma st_inv_lref: ∀M,N. M ⓢ⤇* N → ∀j. #j = N → + ∃∃s. is_whd s & M ↦*[s] #j. +#M #N * -M -N +[ /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. is_whd s & M ↦*[s] 𝛌.C1 & C1 ⓢ⤇* C2. +#M #N * -M -N +[ #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. is_whd 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 #Hs #HM #HB12 #HA12 #D2 #C2 #H destruct /2 width=7/ +] +qed-. + +lemma st_refl: reflexive … st. +#M elim M -M /2 width=3/ /2 width=5/ /2 width=7/ +qed. + +lemma st_step_sn: ∀N1,N2. N1 ⓢ⤇* N2 → ∀s,M. is_whd s → M ↦*[s] N1 → M ⓢ⤇* N2. +#N1 #N2 #H elim H -N1 -N2 +[ #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. is_whd 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=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 #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=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=7/ +] +qed-. + +lemma st_dsubst: dsubstable st. +#N1 #N2 #HN12 #M1 #M2 #H elim H -M1 -M2 +[ #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 (lsreds_dsubst … N1 … HM d) -HM + >(dsubst_vref_gt … Hid) >(dsubst_vref_gt … Hid) /2 width=3/ + ] +| #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_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 #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=5/ (**) (* simplify line *) +| #p #B #B2 #A #_ #IHB2 #M1 #H + 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=7/ (**) (* simplify line *) +] +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. + +lemma st_inv_lsreds_is_standard: ∀M,N. M ⓢ⤇* N → + ∃∃r. M ↦*[r] N & is_standard r. +#M #N #H elim H -M -N +[ #s #M #i #Hs #HM + lapply (is_whd_is_standard … Hs) -Hs /2 width=3/ +| #s #M #A1 #A2 #Hs #HM #_ * #r #HA12 #Hr + lapply (lsreds_trans … HM (rc:::r) (𝛌.A2) ?) /2 width=1/ -A1 #HM + @(ex2_intro … HM) -M -A2 /3 width=1/ +| #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/ +] +qed-. + +theorem st_trans: transitive … st. +#M1 #M #M2 #HM1 #HM2 +elim (st_inv_lsreds_is_standard … HM1) -HM1 #s1 #HM1 #_ +elim (st_inv_lsreds_is_standard … 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_standard r. +#s #M #N #H +@st_inv_lsreds_is_standard /2 width=2/ +qed-. + +(* Note: we use "lapply (rewrite_r ?? is_whd … Hq)" (procedural) + in place of "cut (is_whd (q::r)) [ >Hq ]" (declarative) +*) +lemma st_lsred_swap: ∀p. in_whd p → ∀N1,N2. N1 ↦[p] N2 → ∀M1. M1 ⓢ⤇* N1 → + ∃∃q,M2. in_whd q & M1 ↦[q] M2 & M2 ⓢ⤇* N2. +#p #H @(in_whd_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 #Hq #HM1 #HM + lapply (rewrite_r ?? is_whd … Hq) -Hq /4 width=1/ -s1 -s2 * #Hq #Hr + @(ex3_2_intro … HM1) -M1 // -q + @(st_step_sn … HM) /2 width=1/ +| #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 #Hq #HM1 #HM + lapply (rewrite_r ?? is_whd … Hq) -Hq /4 width=1/ -p -s * #Hq #Hr + @(ex3_2_intro … HM1) -M1 // -q /2 width=7/ +] +qed-. + +theorem lsreds_lsred_swap: ∀s,M1,N1. M1 ↦*[s] N1 → + ∀p,N2. in_whd p → N1 ↦[p] N2 → + ∃∃q,r,M2. in_whd q & M1 ↦[q] M2 & M2 ↦*[r] N2 & + is_standard (q::r). +#s #M1 #N1 #HMN1 #p #N2 #Hp #HN12 +lapply (st_lsreds … HMN1) -s #HMN1 +elim (st_lsred_swap … Hp … HN12 … HMN1) -p -N1 #q #M2 #Hq #HM12 #HMN2 +elim (st_inv_lsreds_is_standard … HMN2) -HMN2 /3 width=8/ +qed-. diff --git a/matita/matita/contribs/lambda/terms/term.ma b/matita/matita/contribs/lambda/terms/term.ma new file mode 100644 index 000000000..6910bdda6 --- /dev/null +++ b/matita/matita/contribs/lambda/terms/term.ma @@ -0,0 +1,68 @@ +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) + +(* Initial invocation: - Patience on us to gain peace and perfection! - *) + +include "preamble.ma". +include "notation.ma". + +(* TERM STRUCTURE ***********************************************************) + +(* Policy: term metavariables : A, B, C, D, M, N + depth metavariables: i, j +*) +inductive term: Type[0] ≝ +| VRef: nat → term (* variable reference by depth *) +| Abst: term → term (* function formation *) +| Appl: term → term → term (* function application *) +. + +interpretation "term construction (variable reference by index)" + 'VariableReferenceByIndex i = (VRef i). + +interpretation "term construction (abstraction)" + 'Abstraction A = (Abst A). + +interpretation "term construction (application)" + 'Application C A = (Appl C A). + +definition compatible_abst: predicate (relation term) ≝ λR. + ∀A1,A2. R A1 A2 → R (𝛌.A1) (𝛌.A2). + +definition compatible_sn: predicate (relation term) ≝ λR. + ∀A,B1,B2. R B1 B2 → R (@B1.A) (@B2.A). + +definition compatible_dx: predicate (relation term) ≝ λR. + ∀B,A1,A2. R A1 A2 → R (@B.A1) (@B.A2). + +definition compatible_appl: predicate (relation term) ≝ λR. + ∀B1,B2. R B1 B2 → ∀A1,A2. R A1 A2 → + R (@B1.A1) (@B2.A2). + +lemma star_compatible_abst: ∀R. compatible_abst R → compatible_abst (star … R). +#R #HR #A1 #A2 #H elim H -A2 // /3 width=3/ +qed. + +lemma star_compatible_sn: ∀R. compatible_sn R → compatible_sn (star … R). +#R #HR #A #B1 #B2 #H elim H -B2 // /3 width=3/ +qed. + +lemma star_compatible_dx: ∀R. compatible_dx R → compatible_dx (star … R). +#R #HR #B #A1 #A2 #H elim H -A2 // /3 width=3/ +qed. + +lemma star_compatible_appl: ∀R. reflexive ? R → + compatible_appl R → compatible_appl (star … R). +#R #H1R #H2R #B1 #B2 #H elim H -B2 /3 width=1/ /3 width=5/ +qed. diff --git a/matita/matita/lib/basics/core_notation.ma b/matita/matita/lib/basics/core_notation.ma index a37b4d859..3f6eda5a7 100644 --- a/matita/matita/lib/basics/core_notation.ma +++ b/matita/matita/lib/basics/core_notation.ma @@ -257,10 +257,10 @@ for @{ 'subset (\lambda ${ident i} : $nonexistent . $p)}. notation > "hvbox({ ident i | term 19 p })" with precedence 90 for @{ 'subset (\lambda ${ident i}. $p)}. -notation < "hvbox({ ident i ∈ s | term 19 p })" with precedence 90 +notation < "hvbox({ ident i ∈ term 19 s | term 19 p })" with precedence 90 for @{ 'comprehension $s (\lambda ${ident i} : $nonexistent . $p)}. -notation > "hvbox({ ident i ∈ s | term 19 p })" with precedence 90 +notation > "hvbox({ ident i ∈ term 19 s | term 19 p })" with precedence 90 for @{ 'comprehension $s (\lambda ${ident i}. $p)}. notation "hvbox(a break ∈ b)" non associative with precedence 45 diff --git a/matita/matita/predefined_virtuals.ml b/matita/matita/predefined_virtuals.ml index 51f3f0781..d87e5a460 100644 --- a/matita/matita/predefined_virtuals.ml +++ b/matita/matita/predefined_virtuals.ml @@ -1505,7 +1505,7 @@ let load_predefined_virtuals () = let predefined_classes = [ [":"; "⁝"; ]; ["."; "•"; "◦"; ]; - ["#"; "⌘"; ]; + ["#"; "♯"; "⌘"; ]; ["-"; "÷"; "⊢"; "⊩"; ]; ["="; "≃"; "≈"; "≝"; "≡"; "≅"; "≐"; "≑"; ]; ["→"; "↦"; "⇝"; "⇾"; "⤍"; "⤏"; "⤳"; ] ;