From: Ferruccio Guidi Date: Tue, 27 Nov 2012 21:09:22 +0000 (+0000) Subject: - the theory of delifting substitution is done X-Git-Tag: make_still_working~1434 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=d5da44537d93ee16e1f440e5ce3fd69b32c3b730;p=helm.git - the theory of delifting substitution is done - the theory of multiplicity is done --- diff --git a/matita/matita/contribs/lambda/delifting_substitution.ma b/matita/matita/contribs/lambda/delifting_substitution.ma new file mode 100644 index 000000000..6e648c9a8 --- /dev/null +++ b/matita/matita/contribs/lambda/delifting_substitution.ma @@ -0,0 +1,142 @@ +(**************************************************************************) +(* ___ *) +(* ||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 C d M on M ≝ match M with +[ VRef i ⇒ tri … i d (#i) (↑[i] C) (#(i-1)) +| Abst A ⇒ 𝛌. (dsubst C (d+1) A) +| Appl B A ⇒ @ (dsubst C d B). (dsubst C d A) +]. + +interpretation "delifting substitution" + 'DSubst C d M = (dsubst C d M). + +(* Note: the notation with "/" does not work *) +notation "hvbox( [ d ⬐ break C ] break term 55 M )" + non associative with precedence 55 + for @{ 'DSubst $C $d $M }. + +notation > "hvbox( [ ⬐ C ] break term 55 M )" + non associative with precedence 55 + for @{ 'DSubst $C 0 $M }. + +lemma dsubst_vref_lt: ∀i,d,C. i < d → [d ⬐ C] #i = #i. +normalize /2 width=1/ +qed. + +lemma dsubst_vref_eq: ∀d,C. [d ⬐ C] #d = ↑[d]C. +normalize // +qed. + +lemma dsubst_vref_gt: ∀i,d,C. d < i → [d ⬐ C] #i = #(i-1). +normalize /2 width=1/ +qed. + +theorem dsubst_lift_le: ∀h,C,M,d1,d2. d2 ≤ d1 → + [d2 ⬐ ↑[d1 - d2, h] C] ↑[d1 + 1, h] M = ↑[d1, h] [d2 ⬐ C] M. +#h #C #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,C,M,d1,d2. d1 ≤ d2 → d2 ≤ d1 + h → + [d2 ⬐ C] ↑[d1, h + 1] M = ↑[d1, h] M. +#h #C #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,C,M,d1,d2. d1 + h ≤ d2 → + [d2 ⬐ C] ↑[d1, h] M = ↑[d1, h] [d2 - h ⬐ C] M. +#h #C #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 subst_subst_ge: ∀C1,C2,M,d1,d2. d1 ≤ d2 → + [d2 ⬐ C2] [d1 ⬐ C1] M = [d1 ⬐ [d2 - d1 ⬐ C2] C1] [d2 + 1 ⬐ C2] M. +#C1 #C2 #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 subst_subst_lt: ∀C1,C2,M,d1,d2. d2 < d1 → + [d2 ⬐ [d1 - d2 -1 ⬐ C1] C2] [d1 ⬐ C1] M = [d1 - 1 ⬐ C1] [d2 ⬐ C2] M. +#C1 #C2 #M #d1 #d2 #Hd21 +lapply (ltn_to_ltO … Hd21) #Hd1 +>subst_subst_ge in ⊢ (???%); /2 width=1/ "hvbox( [ ⬐ C ] break term 55 M )" - non associative with precedence 55 - for @{ 'DSubst $C 0 $M }. - -lemma dsubst_vref_lt: ∀i,d,C. i < d → [ d ⬐ C ] #i = #i. -normalize /2 width=1/ -qed. - -lemma dsubst_vref_eq: ∀d,C. [ d ⬐ C ] #d = ↑[d]C. -normalize // -qed. - -lemma dsubst_vref_gt: ∀i,d,C. d < i → [ d ⬐ C ] #i = #(i-1). -normalize /2 width=1/ -qed. - -theorem dsubst_lift_le: ∀h,C,M,d1,d2. d2 ≤ d1 → - [ d2 ⬐ ↑[d1 - d2, h] C ] ↑[d1 + 1, h] M = ↑[d1, h] [ d2 ⬐ C ] M. -#h #C #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,C,M,d1,d2. d1 ≤ d2 → d2 ≤ d1 + h → - [ d2 ⬐ C ] ↑[d1, h + 1] M = ↑[d1, h] M. -#h #C #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. diff --git a/matita/matita/contribs/lambda/multiplicity.ma b/matita/matita/contribs/lambda/multiplicity.ma new file mode 100644 index 000000000..d6d5af110 --- /dev/null +++ b/matita/matita/contribs/lambda/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 "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 "multiplicity" + 'Multiplicity M = (mult M). + +notation "hvbox( #{M} )" + non associative with precedence 55 + 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: ∀C,M,d. #{[d ⬐ C] M} ≤ #{M} * #{C}. +#C #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.