From c821924472ab07f543c0e4acd0b808715de7a934 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Wed, 2 Jan 2013 22:12:53 +0000 Subject: [PATCH 1/1] lambda: some refactoring + support for subsets of subterms started core_notation: some "term 19" added predefined_virtuals: an addition --- matita/matita/contribs/lambda/notation.ma | 61 +++++ matita/matita/contribs/lambda/policy.txt | 8 +- .../matita/contribs/lambda/subterms/lift.ma | 254 ++++++++++++++++++ .../contribs/lambda/subterms/subterms.ma | 69 +++++ .../{ => terms}/delifting_substitution.ma | 17 +- .../labeled_sequential_computation.ma | 6 +- .../labeled_sequential_reduction.ma | 14 +- .../contribs/lambda/{ => terms}/length.ma | 2 +- .../contribs/lambda/{ => terms}/lift.ma | 35 +-- .../lambda/{ => terms}/multiplicity.ma | 10 +- .../{ => terms}/parallel_computation.ma | 2 +- .../lambda/{ => terms}/parallel_reduction.ma | 4 +- .../contribs/lambda/{ => terms}/pointer.ma | 2 +- .../lambda/{ => terms}/pointer_list.ma | 2 +- .../{ => terms}/pointer_list_standard.ma | 4 +- .../lambda/{ => terms}/pointer_order.ma | 2 +- .../lambda/{ => terms}/pointer_tree.ma | 2 +- .../lambda/{ => terms}/st_computation.ma | 4 +- .../contribs/lambda/{ => terms}/term.ma | 13 +- matita/matita/lib/basics/core_notation.ma | 4 +- matita/matita/predefined_virtuals.ml | 2 +- 21 files changed, 434 insertions(+), 83 deletions(-) create mode 100644 matita/matita/contribs/lambda/notation.ma create mode 100644 matita/matita/contribs/lambda/subterms/lift.ma create mode 100644 matita/matita/contribs/lambda/subterms/subterms.ma rename matita/matita/contribs/lambda/{ => terms}/delifting_substitution.ma (92%) rename matita/matita/contribs/lambda/{ => terms}/labeled_sequential_computation.ma (96%) rename matita/matita/contribs/lambda/{ => terms}/labeled_sequential_reduction.ma (93%) rename matita/matita/contribs/lambda/{ => terms}/length.ma (98%) rename matita/matita/contribs/lambda/{ => terms}/lift.ma (91%) rename matita/matita/contribs/lambda/{ => terms}/multiplicity.ma (87%) rename matita/matita/contribs/lambda/{ => terms}/parallel_computation.ma (98%) rename matita/matita/contribs/lambda/{ => terms}/parallel_reduction.ma (98%) rename matita/matita/contribs/lambda/{ => terms}/pointer.ma (99%) rename matita/matita/contribs/lambda/{ => terms}/pointer_list.ma (98%) rename matita/matita/contribs/lambda/{ => terms}/pointer_list_standard.ma (96%) rename matita/matita/contribs/lambda/{ => terms}/pointer_order.ma (99%) rename matita/matita/contribs/lambda/{ => terms}/pointer_tree.ma (97%) rename matita/matita/contribs/lambda/{ => terms}/st_computation.ma (99%) rename matita/matita/contribs/lambda/{ => terms}/term.ma (89%) 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/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/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/delifting_substitution.ma b/matita/matita/contribs/lambda/terms/delifting_substitution.ma similarity index 92% rename from matita/matita/contribs/lambda/delifting_substitution.ma rename to matita/matita/contribs/lambda/terms/delifting_substitution.ma index fe45c35a2..7926c3948 100644 --- a/matita/matita/contribs/lambda/delifting_substitution.ma +++ b/matita/matita/contribs/lambda/terms/delifting_substitution.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "lift.ma". +include "terms/lift.ma". (* DELIFTING SUBSTITUTION ***************************************************) @@ -26,15 +26,6 @@ let rec dsubst D d M on M ≝ match M with 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. @@ -151,9 +142,9 @@ lemma star_dsubstable_dx: ∀R. dsubstable_dx R → dsubstable_dx (star … R). #R #HR #D #M1 #M2 #H elim H -M2 // /3 width=3/ qed. -lemma lstar_dsubstable_dx: ∀T,R. (∀t. dsubstable_dx (R t)) → - ∀l. dsubstable_dx (lstar T … R l). -#T #R #HR #l #D #M1 #M2 #H +lemma lstar_dsubstable_dx: ∀S,R. (∀a. dsubstable_dx (R a)) → + ∀l. dsubstable_dx (lstar S … R l). +#S #R #HR #l #D #M1 #M2 #H @(lstar_ind_l ????????? H) -l -M1 // /3 width=3/ qed. diff --git a/matita/matita/contribs/lambda/labeled_sequential_computation.ma b/matita/matita/contribs/lambda/terms/labeled_sequential_computation.ma similarity index 96% rename from matita/matita/contribs/lambda/labeled_sequential_computation.ma rename to matita/matita/contribs/lambda/terms/labeled_sequential_computation.ma index 4c2a6fc9e..0dc7c53b5 100644 --- a/matita/matita/contribs/lambda/labeled_sequential_computation.ma +++ b/matita/matita/contribs/lambda/terms/labeled_sequential_computation.ma @@ -12,8 +12,8 @@ (* *) (**************************************************************************) -include "pointer_list.ma". -include "parallel_computation.ma". +include "terms/pointer_list.ma". +include "terms/parallel_computation.ma". (* LABELED SEQUENTIAL COMPUTATION (MULTISTEP) *******************************) @@ -106,7 +106,7 @@ lemma lsreds_compatible_beta: ∀r,B1,B2. B1 ↦*[r] B2 → ∀s,A1,A2. A1 ↦*[ qed. (* Note: "|s|" should be unparetesized *) -lemma lsreds_fwd_mult: ∀s,M1,M2. M1 ↦*[s] M2 → #{M2} ≤ #{M1} ^ (2 ^ (|s|)). +lemma lsreds_fwd_mult: ∀s,M1,M2. M1 ↦*[s] M2 → ♯{M2} ≤ ♯{M1} ^ (2 ^ (|s|)). #s #M1 #M2 #H @(lstar_ind_l ????????? H) -s -M1 normalize // #p #s #M1 #M #HM1 #_ #IHM2 lapply (lsred_fwd_mult … HM1) -p #HM1 diff --git a/matita/matita/contribs/lambda/labeled_sequential_reduction.ma b/matita/matita/contribs/lambda/terms/labeled_sequential_reduction.ma similarity index 93% rename from matita/matita/contribs/lambda/labeled_sequential_reduction.ma rename to matita/matita/contribs/lambda/terms/labeled_sequential_reduction.ma index 7dd2bccb3..54daa9257 100644 --- a/matita/matita/contribs/lambda/labeled_sequential_reduction.ma +++ b/matita/matita/contribs/lambda/terms/labeled_sequential_reduction.ma @@ -12,8 +12,8 @@ (* *) (**************************************************************************) -include "pointer.ma". -include "multiplicity.ma". +include "terms/pointer.ma". +include "terms/multiplicity.ma". (* LABELED SEQUENTIAL REDUCTION (SINGLE STEP) *******************************) @@ -85,17 +85,17 @@ lemma lsred_inv_dx: ∀p,M,N. M ↦[p] N → ∀q. dx::q = p → ] qed-. -lemma lsred_fwd_mult: ∀p,M,N. M ↦[p] N → #{N} < #{M} * #{M}. +lemma lsred_fwd_mult: ∀p,M,N. M ↦[p] N → ♯{N} < ♯{M} * ♯{M}. #p #M #N #H elim H -p -M -N -[ #B #A @(le_to_lt_to_lt … (#{A}*#{B})) // +[ #B #A @(le_to_lt_to_lt … (♯{A}*♯{B})) // normalize /3 width=1 by lt_minus_to_plus_r, lt_times/ (**) (* auto: too slow without trace *) | // | #p #B #D #A #_ #IHBD - @(lt_to_le_to_lt … (#{B}*#{B}+#{A})) [ /2 width=1/ ] -D -p + @(lt_to_le_to_lt … (♯{B}*♯{B}+♯{A})) [ /2 width=1/ ] -D -p | #p #B #A #C #_ #IHAC - @(lt_to_le_to_lt … (#{B}+#{A}*#{A})) [ /2 width=1/ ] -C -p + @(lt_to_le_to_lt … (♯{B}+♯{A}*♯{A})) [ /2 width=1/ ] -C -p ] -@(transitive_le … (#{B}*#{B}+#{A}*#{A})) [ /2 width=1/ ] +@(transitive_le … (♯{B}*♯{B}+♯{A}*♯{A})) [ /2 width=1/ ] >distributive_times_plus normalize /2 width=1/ qed-. diff --git a/matita/matita/contribs/lambda/length.ma b/matita/matita/contribs/lambda/terms/length.ma similarity index 98% rename from matita/matita/contribs/lambda/length.ma rename to matita/matita/contribs/lambda/terms/length.ma index abb629433..81ce2e379 100644 --- a/matita/matita/contribs/lambda/length.ma +++ b/matita/matita/contribs/lambda/terms/length.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "lift.ma". +include "terms/lift.ma". (* LENGTH *******************************************************************) diff --git a/matita/matita/contribs/lambda/lift.ma b/matita/matita/contribs/lambda/terms/lift.ma similarity index 91% rename from matita/matita/contribs/lambda/lift.ma rename to matita/matita/contribs/lambda/terms/lift.ma index 17ea9692b..62da59661 100644 --- a/matita/matita/contribs/lambda/lift.ma +++ b/matita/matita/contribs/lambda/terms/lift.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "term.ma". +include "terms/term.ma". (* RELOCATION ***************************************************************) @@ -28,18 +28,6 @@ let rec lift h d M on M ≝ match M with 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. @@ -48,12 +36,7 @@ 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/ -(dsubst_vref_lt … Hid) normalize // diff --git a/matita/matita/contribs/lambda/parallel_computation.ma b/matita/matita/contribs/lambda/terms/parallel_computation.ma similarity index 98% rename from matita/matita/contribs/lambda/parallel_computation.ma rename to matita/matita/contribs/lambda/terms/parallel_computation.ma index af64cc09c..4f93f90a7 100644 --- a/matita/matita/contribs/lambda/parallel_computation.ma +++ b/matita/matita/contribs/lambda/terms/parallel_computation.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "parallel_reduction.ma". +include "terms/parallel_reduction.ma". (* PARALLEL COMPUTATION (MULTISTEP) *****************************************) diff --git a/matita/matita/contribs/lambda/parallel_reduction.ma b/matita/matita/contribs/lambda/terms/parallel_reduction.ma similarity index 98% rename from matita/matita/contribs/lambda/parallel_reduction.ma rename to matita/matita/contribs/lambda/terms/parallel_reduction.ma index 1d97b3b87..a9190151b 100644 --- a/matita/matita/contribs/lambda/parallel_reduction.ma +++ b/matita/matita/contribs/lambda/terms/parallel_reduction.ma @@ -12,8 +12,8 @@ (* *) (**************************************************************************) -include "length.ma". -include "labeled_sequential_reduction.ma". +include "terms/length.ma". +include "terms/labeled_sequential_reduction.ma". (* PARALLEL REDUCTION (SINGLE STEP) *****************************************) diff --git a/matita/matita/contribs/lambda/pointer.ma b/matita/matita/contribs/lambda/terms/pointer.ma similarity index 99% rename from matita/matita/contribs/lambda/pointer.ma rename to matita/matita/contribs/lambda/terms/pointer.ma index d71574e74..79b269351 100644 --- a/matita/matita/contribs/lambda/pointer.ma +++ b/matita/matita/contribs/lambda/terms/pointer.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "term.ma". +include "terms/term.ma". (* POINTER ******************************************************************) diff --git a/matita/matita/contribs/lambda/pointer_list.ma b/matita/matita/contribs/lambda/terms/pointer_list.ma similarity index 98% rename from matita/matita/contribs/lambda/pointer_list.ma rename to matita/matita/contribs/lambda/terms/pointer_list.ma index becfc0a5e..c1e710649 100644 --- a/matita/matita/contribs/lambda/pointer_list.ma +++ b/matita/matita/contribs/lambda/terms/pointer_list.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "pointer.ma". +include "terms/pointer.ma". (* POINTER LIST *************************************************************) diff --git a/matita/matita/contribs/lambda/pointer_list_standard.ma b/matita/matita/contribs/lambda/terms/pointer_list_standard.ma similarity index 96% rename from matita/matita/contribs/lambda/pointer_list_standard.ma rename to matita/matita/contribs/lambda/terms/pointer_list_standard.ma index 8ae8d5aa1..0c3cc2364 100644 --- a/matita/matita/contribs/lambda/pointer_list_standard.ma +++ b/matita/matita/contribs/lambda/terms/pointer_list_standard.ma @@ -12,8 +12,8 @@ (* *) (**************************************************************************) -include "pointer_list.ma". -include "pointer_order.ma". +include "terms/pointer_list.ma". +include "terms/pointer_order.ma". (* STANDARD POINTER LIST ****************************************************) diff --git a/matita/matita/contribs/lambda/pointer_order.ma b/matita/matita/contribs/lambda/terms/pointer_order.ma similarity index 99% rename from matita/matita/contribs/lambda/pointer_order.ma rename to matita/matita/contribs/lambda/terms/pointer_order.ma index 0b738215a..1ead95b99 100644 --- a/matita/matita/contribs/lambda/pointer_order.ma +++ b/matita/matita/contribs/lambda/terms/pointer_order.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "pointer.ma". +include "terms/pointer.ma". (* POINTER ORDER ************************************************************) diff --git a/matita/matita/contribs/lambda/pointer_tree.ma b/matita/matita/contribs/lambda/terms/pointer_tree.ma similarity index 97% rename from matita/matita/contribs/lambda/pointer_tree.ma rename to matita/matita/contribs/lambda/terms/pointer_tree.ma index 4381cd62c..fff98a856 100644 --- a/matita/matita/contribs/lambda/pointer_tree.ma +++ b/matita/matita/contribs/lambda/terms/pointer_tree.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "pointer_list.ma". +include "terms/pointer_list.ma". (* POINTER TREE *************************************************************) diff --git a/matita/matita/contribs/lambda/st_computation.ma b/matita/matita/contribs/lambda/terms/st_computation.ma similarity index 99% rename from matita/matita/contribs/lambda/st_computation.ma rename to matita/matita/contribs/lambda/terms/st_computation.ma index ebcc572a4..1cd7a9f97 100644 --- a/matita/matita/contribs/lambda/st_computation.ma +++ b/matita/matita/contribs/lambda/terms/st_computation.ma @@ -12,8 +12,8 @@ (* *) (**************************************************************************) -include "labeled_sequential_computation.ma". -include "pointer_list_standard.ma". +include "terms/labeled_sequential_computation.ma". +include "terms/pointer_list_standard.ma". (* KASHIMA'S "ST" COMPUTATION ***********************************************) diff --git a/matita/matita/contribs/lambda/term.ma b/matita/matita/contribs/lambda/terms/term.ma similarity index 89% rename from matita/matita/contribs/lambda/term.ma rename to matita/matita/contribs/lambda/terms/term.ma index 2e08b861e..6910bdda6 100644 --- a/matita/matita/contribs/lambda/term.ma +++ b/matita/matita/contribs/lambda/terms/term.ma @@ -15,6 +15,7 @@ (* Initial invocation: - Patience on us to gain peace and perfection! - *) include "preamble.ma". +include "notation.ma". (* TERM STRUCTURE ***********************************************************) @@ -36,18 +37,6 @@ interpretation "term construction (abstraction)" 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). 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 = [ [":"; "⁝"; ]; ["."; "•"; "◦"; ]; - ["#"; "⌘"; ]; + ["#"; "♯"; "⌘"; ]; ["-"; "÷"; "⊢"; "⊩"; ]; ["="; "≃"; "≈"; "≝"; "≡"; "≅"; "≐"; "≑"; ]; ["→"; "↦"; "⇝"; "⇾"; "⤍"; "⤏"; "⤳"; ] ; -- 2.39.2