From: Ferruccio Guidi Date: Tue, 15 Jan 2013 10:34:32 +0000 (+0000) Subject: - a few more lemmas ... X-Git-Tag: make_still_working~1348 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=2f42e0081e96a2d0a4097066af8349feebbd86fe;p=helm.git - a few more lemmas ... - some renaming --- diff --git a/matita/matita/contribs/lambda/paths/alternative_standard_order.ma b/matita/matita/contribs/lambda/paths/alternative_standard_order.ma new file mode 100644 index 000000000..144c1dabf --- /dev/null +++ b/matita/matita/contribs/lambda/paths/alternative_standard_order.ma @@ -0,0 +1,48 @@ +(**************************************************************************) +(* ___ *) +(* ||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 "paths/standard_precedence.ma". + +(* ALTERNATIVE STANDARD ORDER ***********************************************) + +(* Note: this is p < q *) +definition slt: relation path ≝ TC … sprec. + +interpretation "standard 'less than' on paths" + 'lt p q = (slt p q). + +lemma slt_step_rc: ∀p,q. p ≺ q → p < q. +/2 width=1/ +qed. + +lemma slt_nil: ∀c,p. ◊ < c::p. +/2 width=1/ +qed. + +lemma slt_skip: dx::◊ < ◊. +/2 width=1/ +qed. + +lemma slt_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 slt_trans: transitive … slt. +/2 width=3/ +qed-. + +lemma slt_refl: ∀p. p < p. +#p elim p -p /2 width=1/ +@(slt_trans … (dx::◊)) // +qed. diff --git a/matita/matita/contribs/lambda/paths/labeled_st_reduction.ma b/matita/matita/contribs/lambda/paths/labeled_st_reduction.ma index 253f2ae73..f6f93d6fb 100644 --- a/matita/matita/contribs/lambda/paths/labeled_st_reduction.ma +++ b/matita/matita/contribs/lambda/paths/labeled_st_reduction.ma @@ -12,8 +12,7 @@ (* *) (**************************************************************************) -include "subterms/delifting_substitution.ma". -include "subterms/projections.ma". +include "subterms/booleanize.ma". include "paths/standard_order.ma". (* PATH-LABELED STANDARD REDUCTION ON SUBTERMS (SINGLE STEP) ****************) diff --git a/matita/matita/contribs/lambda/paths/standard_order.ma b/matita/matita/contribs/lambda/paths/standard_order.ma index 563cdce34..8ce5b8790 100644 --- a/matita/matita/contribs/lambda/paths/standard_order.ma +++ b/matita/matita/contribs/lambda/paths/standard_order.ma @@ -12,73 +12,10 @@ (* *) (**************************************************************************) -include "paths/path.ma". +include "paths/standard_precedence.ma". (* STANDARD ORDER ************************************************************) -(* Note: standard precedence relation on paths: p ≺ q - to serve as base for the order relations: p < q and p ≤ q *) -inductive sprec: relation path ≝ -| sprec_nil : ∀c,q. sprec (◊) (c::q) -| sprec_rc : ∀p,q. sprec (dx::p) (rc::q) -| sprec_sn : ∀p,q. sprec (rc::p) (sn::q) -| sprec_comp: ∀c,p,q. sprec p q → sprec (c::p) (c::q) -| sprec_skip: sprec (dx::◊) ◊ -. - -interpretation "standard 'precedes' on paths" - 'prec p q = (sprec p q). - -lemma sprec_inv_sn: ∀p,q. p ≺ q → ∀p0. sn::p0 = p → - ∃∃q0. p0 ≺ q0 & sn::q0 = q. -#p #q * -p -q -[ #c #q #p0 #H destruct -| #p #q #p0 #H destruct -| #p #q #p0 #H destruct -| #c #p #q #Hpq #p0 #H destruct /2 width=3/ -| #p0 #H destruct -] -qed-. - -lemma sprec_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 slt: relation path ≝ TC … sprec. - -interpretation "standard 'less than' on paths" - 'lt p q = (slt p q). - -lemma slt_step_rc: ∀p,q. p ≺ q → p < q. -/2 width=1/ -qed. - -lemma slt_nil: ∀c,p. ◊ < c::p. -/2 width=1/ -qed. - -lemma slt_skip: dx::◊ < ◊. -/2 width=1/ -qed. - -lemma slt_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 slt_trans: transitive … slt. -/2 width=3/ -qed-. - -lemma slt_refl: ∀p. p < p. -#p elim p -p /2 width=1/ -@(slt_trans … (dx::◊)) // -qed. - (* Note: this is p ≤ q *) definition sle: relation path ≝ star … sprec. diff --git a/matita/matita/contribs/lambda/paths/standard_precedence.ma b/matita/matita/contribs/lambda/paths/standard_precedence.ma new file mode 100644 index 000000000..e8f41eecf --- /dev/null +++ b/matita/matita/contribs/lambda/paths/standard_precedence.ma @@ -0,0 +1,49 @@ +(**************************************************************************) +(* ___ *) +(* ||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 "paths/path.ma". + +(* STANDARD PRECEDENCE ******************************************************) + +(* Note: standard precedence relation on paths: p ≺ q + to serve as base for the order relations: p < q and p ≤ q *) +inductive sprec: relation path ≝ +| sprec_nil : ∀c,q. sprec (◊) (c::q) +| sprec_rc : ∀p,q. sprec (dx::p) (rc::q) +| sprec_sn : ∀p,q. sprec (rc::p) (sn::q) +| sprec_comp: ∀c,p,q. sprec p q → sprec (c::p) (c::q) +| sprec_skip: sprec (dx::◊) ◊ +. + +interpretation "standard 'precedes' on paths" + 'prec p q = (sprec p q). + +lemma sprec_inv_sn: ∀p,q. p ≺ q → ∀p0. sn::p0 = p → + ∃∃q0. p0 ≺ q0 & sn::q0 = q. +#p #q * -p -q +[ #c #q #p0 #H destruct +| #p #q #p0 #H destruct +| #p #q #p0 #H destruct +| #c #p #q #Hpq #p0 #H destruct /2 width=3/ +| #p0 #H destruct +] +qed-. + +lemma sprec_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-. diff --git a/matita/matita/contribs/lambda/subterms/boolean.ma b/matita/matita/contribs/lambda/subterms/boolean.ma new file mode 100644 index 000000000..294063d03 --- /dev/null +++ b/matita/matita/contribs/lambda/subterms/boolean.ma @@ -0,0 +1,70 @@ +(**************************************************************************) +(* ___ *) +(* ||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/relocating_substitution.ma". +include "subterms/relocating_substitution.ma". + +(* BOOLEAN (EMPTY OR FULL) SUBSET *******************************************) + +let rec boolean b M on M ≝ match M with +[ VRef i ⇒ {b}#i +| Abst A ⇒ {b}𝛌.(boolean b A) +| Appl B A ⇒ {b}@(boolean b B).(boolean b A) +]. + +interpretation "boolean subset (subterms)" + 'ProjectUp b M = (boolean b M). + +notation "hvbox( { term 46 b } ⇑ break term 46 M)" + non associative with precedence 46 + for @{ 'ProjectUp $b $M }. + +lemma boolean_inv_vref: ∀j,b0,b,M. {b}⇑ M = {b0}#j → b = b0 ∧ M = #j. +#j #b0 #b * normalize +[ #i #H destruct /2 width=1/ +| #A #H destruct +| #B #A #H destruct +] +qed-. + +lemma boolean_inv_abst: ∀U,b0,b,M. {b}⇑ M = {b0}𝛌.U → + ∃∃C. b = b0 & {b}⇑C = U & M = 𝛌.C. +#U #b0 #b * normalize +[ #i #H destruct +| #A #H destruct /2 width=3/ +| #B #A #H destruct +] +qed-. + +lemma boolean_inv_appl: ∀W,U,b0,b,M. {b}⇑ M = {b0}@W.U → + ∃∃D,C. b = b0 & {b}⇑D = W & {b}⇑C = U & M = @D.C. +#W #U #b0 #b * normalize +[ #i #H destruct +| #A #H destruct +| #B #A #H destruct /2 width=5/ +] +qed-. + +lemma boolean_lift: ∀b,h,M,d. {b}⇑ ↑[d, h] M = ↑[d, h] {b}⇑ M. +#b #h #M elim M -M normalize // +qed. + +lemma boolean_dsubst: ∀b,N,M,d. {b}⇑ [d ↙ N] M = [d ↙ {b}⇑ N] {b}⇑ M. +#b #N #M elim M -M [2,3: normalize // ] +#i #d elim (lt_or_eq_or_gt i d) #Hid +[ >(sdsubst_vref_lt … Hid) >(dsubst_vref_lt … Hid) // +| destruct normalize // +| >(sdsubst_vref_gt … Hid) >(dsubst_vref_gt … Hid) // +] +qed. diff --git a/matita/matita/contribs/lambda/subterms/booleanize.ma b/matita/matita/contribs/lambda/subterms/booleanize.ma new file mode 100644 index 000000000..f49a95335 --- /dev/null +++ b/matita/matita/contribs/lambda/subterms/booleanize.ma @@ -0,0 +1,57 @@ +(**************************************************************************) +(* ___ *) +(* ||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/carrier.ma". +include "subterms/boolean.ma". + +(* BOOLEANIZE (EMPTY OR FILL) **********************************************) + +definition booleanize: bool → subterms → subterms ≝ + λb,F. {b}⇑⇓F. + +interpretation "make boolean (subterms)" + 'ProjectSame b F = (booleanize b F). + +notation "hvbox( { term 46 b } ⇕ break term 46 F)" + non associative with precedence 46 + for @{ 'ProjectSame $b $F }. + +lemma booleanize_inv_vref: ∀j,b0,b,F. {b}⇕ F = {b0}#j → + ∃∃b1. b = b0 & F = {b1}#j. +#j #b0 #b #F #H +elim (boolean_inv_vref … H) -H #H0 #H +elim (carrier_inv_vref … H) -H /2 width=2/ +qed-. + +lemma booleanize_inv_abst: ∀U,b0,b,F. {b}⇕ F = {b0}𝛌.U → + ∃∃b1,T. b = b0 & {b}⇕T = U & F = {b1}𝛌.T. +#U #b0 #b #F #H +elim (boolean_inv_abst … H) -H #C #H0 #H1 #H +elim (carrier_inv_abst … H) -H #b1 #U1 #H3 destruct /2 width=4/ +qed-. + +lemma booleanize_inv_appl: ∀W,U,b0,b,F. {b}⇕ F = {b0}@W.U → + ∃∃b1,V,T. b = b0 & {b}⇕V = W & {b}⇕T = U & F = {b1}@V.T. +#W #U #b0 #b #F #H +elim (boolean_inv_appl … H) -H #D #C #H0 #H1 #H2 #H +elim (carrier_inv_appl … H) -H #b1 #W1 #U1 #H3 #H4 destruct /2 width=6/ +qed-. +(* +lemma booleanize_lift: ∀b,h,F,d. {b}⇕ ↑[d, h] F = ↑[d, h] {b}⇕ F. +#b #h #M elim M -M normalize // +qed. + +lemma booleanize_dsubst: ∀b,G,F,d. {b}⇕ [d ↙ G] F = [d ↙ {b}⇕ G] {b}⇕ F. +#b #N #M elim M -M [2,3: normalize // ] +*) diff --git a/matita/matita/contribs/lambda/subterms/carrier.ma b/matita/matita/contribs/lambda/subterms/carrier.ma new file mode 100644 index 000000000..8936792e2 --- /dev/null +++ b/matita/matita/contribs/lambda/subterms/carrier.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 "terms/relocating_substitution.ma". +include "subterms/relocating_substitution.ma". + +(* CARRIER (UNDERLYING TERM) ************************************************) + +let rec carrier F on F ≝ match F with +[ SVRef _ i ⇒ #i +| SAbst _ T ⇒ 𝛌.(carrier T) +| SAppl _ V T ⇒ @(carrier V).(carrier T) +]. + +interpretation "carrier (subterms)" + 'ProjectDown F = (carrier F). + +notation "hvbox(⇓ term 46 F)" + non associative with precedence 46 + for @{ 'ProjectDown $F }. + +lemma carrier_inv_vref: ∀j,F. ⇓F = #j → ∃b. F = {b}#j. +#j * normalize +[ #b #i #H destruct /2 width=2/ +| #b #T #H destruct +| #b #V #T #H destruct +] +qed-. + +lemma carrier_inv_abst: ∀C,F. ⇓F = 𝛌.C → ∃∃b,U. ⇓U = C & F = {b}𝛌.U. +#C * normalize +[ #b #i #H destruct +| #b #T #H destruct /2 width=4/ +| #b #V #T #H destruct +] +qed-. + +lemma carrier_inv_appl: ∀D,C,F. ⇓F = @D.C → + ∃∃b,W,U. ⇓W = D & ⇓U = C & F = {b}@W.U. +#D #C * normalize +[ #b #i #H destruct +| #b #T #H destruct +| #b #V #T #H destruct /2 width=6/ +] +qed-. + +lemma carrier_lift: ∀h,F,d. ⇓ ↑[d, h] F = ↑[d, h] ⇓F. +#h #F elim F -F normalize // +qed. + +lemma carrier_dsubst: ∀G,F,d. ⇓ [d ↙ G] F = [d ↙ ⇓G] ⇓F. +#G #F elim F -F [2,3: normalize // ] +#b #i #d elim (lt_or_eq_or_gt i d) #Hid +[ >(sdsubst_vref_lt … Hid) >(dsubst_vref_lt … Hid) // +| destruct normalize // +| >(sdsubst_vref_gt … Hid) >(dsubst_vref_gt … Hid) // +] +qed. diff --git a/matita/matita/contribs/lambda/subterms/delifting_substitution.ma b/matita/matita/contribs/lambda/subterms/delifting_substitution.ma deleted file mode 100644 index 272c75460..000000000 --- a/matita/matita/contribs/lambda/subterms/delifting_substitution.ma +++ /dev/null @@ -1,155 +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 "subterms/lift.ma". - -(* DELIFTING SUBSTITUTION ***************************************************) - -(* Policy: depth (level) metavariables: d, e (as for lift) *) -let rec sdsubst G d F on F ≝ match F with -[ SVRef b i ⇒ tri … i d ({b}#i) (↑[i] G) ({b}#(i-1)) -| SAbst b T ⇒ {b}𝛌. (sdsubst G (d+1) T) -| SAppl b V T ⇒ {b}@ (sdsubst G d V). (sdsubst G d T) -]. - -interpretation "delifting substitution for subterms" - 'DSubst G d F = (sdsubst G d F). - -lemma sdsubst_vref_lt: ∀b,i,d,G. i < d → [d ↙ G] {b}#i = {b}#i. -normalize /2 width=1/ -qed. - -lemma sdsubst_vref_eq: ∀b,i,G. [i ↙ G] {b}#i = ↑[i]G. -normalize // -qed. - -lemma sdsubst_vref_gt: ∀b,i,d,G. d < i → [d ↙ G] {b}#i = {b}#(i-1). -normalize /2 width=1/ -qed. - -theorem sdsubst_slift_le: ∀h,G,F,d1,d2. d2 ≤ d1 → - [d2 ↙ ↑[d1 - d2, h] G] ↑[d1 + 1, h] F = ↑[d1, h] [d2 ↙ G] F. -#h #G #F elim F -F -[ #b #i #d1 #d2 #Hd21 elim (lt_or_eq_or_gt i d2) #Hid2 - [ lapply (lt_to_le_to_lt … Hid2 Hd21) -Hd21 #Hid1 - >(sdsubst_vref_lt … Hid2) >(slift_vref_lt … Hid1) >slift_vref_lt /2 width=1/ - | destruct >sdsubst_vref_eq >slift_vref_lt /2 width=1/ - | >(sdsubst_vref_gt … Hid2) -Hd21 elim (lt_or_ge (i-1) d1) #Hi1d1 - [ >(slift_vref_lt … Hi1d1) >slift_vref_lt /2 width=1/ - | lapply (ltn_to_ltO … Hid2) #Hi - >(slift_vref_ge … Hi1d1) >slift_vref_ge /2 width=1/ -Hi1d1 >plus_minus // /3 width=1/ - ] - ] -| normalize #b #T #IHT #d1 #d2 #Hd21 - lapply (IHT (d1+1) (d2+1) ?) -IHT /2 width=1/ -| normalize #b #V #T #IHV #IHT #d1 #d2 #Hd21 - >IHV -IHV // >IHT -IHT // -] -qed. - -theorem sdsubst_slift_be: ∀h,G,F,d1,d2. d1 ≤ d2 → d2 ≤ d1 + h → - [d2 ↙ G] ↑[d1, h + 1] F = ↑[d1, h] F. -#h #G #F elim F -F -[ #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+h) Hd21 ?) -Hd12 -Hd21 /2 width=1/ #Hd2 - >(slift_vref_ge … Hid1) >(slift_vref_ge … Hid1) -Hid1 - >sdsubst_vref_gt // /2 width=1/ - ] -| normalize #b #T #IHT #d1 #d2 #Hd12 #Hd21 - >IHT -IHT // /2 width=1/ -| normalize #b #V #T #IHV #IHT #d1 #d2 #Hd12 #Hd21 - >IHV -IHV // >IHT -IHT // -] -qed. - -theorem sdsubst_slift_ge: ∀h,G,F,d1,d2. d1 + h ≤ d2 → - [d2 ↙ G] ↑[d1, h] F = ↑[d1, h] [d2 - h ↙ G] F. -#h #G #F elim F -F -[ #b #i #d1 #d2 #Hd12 elim (lt_or_eq_or_gt i (d2-h)) #Hid2h - [ >(sdsubst_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 - >(slift_vref_lt … Hid1) -Hid1 /2 width=1/ - | >(slift_vref_ge … Hid1) -Hid1 -Hd12 /3 width=1/ - ] - | destruct elim (le_inv_plus_l … Hd12) -Hd12 #Hd12 #Hhd2 - >sdsubst_vref_eq >slift_vref_ge // >slift_slift_be // (sdsubst_vref_gt … Hid2h) - >slift_vref_ge /2 width=1/ >slift_vref_ge /2 width=1/ -Hid1 - >sdsubst_vref_gt /2 width=1/ -Hid2h >plus_minus // - ] -| normalize #b #T #IHT #d1 #d2 #Hd12 - elim (le_inv_plus_l … Hd12) #_ #Hhd2 - >IHT -IHT /2 width=1/ IHV -IHV // >IHT -IHT // -] -qed. - -theorem sdsubst_sdsubst_ge: ∀G1,G2,F,d1,d2. d1 ≤ d2 → - [d2 ↙ G2] [d1 ↙ G1] F = [d1 ↙ [d2 - d1 ↙ G2] G1] [d2 + 1 ↙ G2] F. -#G1 #G2 #F elim F -F -[ #b #i #d1 #d2 #Hd12 elim (lt_or_eq_or_gt i d1) #Hid1 - [ lapply (lt_to_le_to_lt … Hid1 Hd12) -Hd12 #Hid2 - >(sdsubst_vref_lt … Hid1) >(sdsubst_vref_lt … Hid2) >sdsubst_vref_lt /2 width=1/ - | destruct >sdsubst_vref_eq >sdsubst_vref_lt /2 width=1/ - | >(sdsubst_vref_gt … Hid1) elim (lt_or_eq_or_gt i (d2+1)) #Hid2 - [ lapply (ltn_to_ltO … Hid1) #Hi - >(sdsubst_vref_lt … Hid2) >sdsubst_vref_lt /2 width=1/ - | destruct /2 width=1/ - | lapply (le_to_lt_to_lt (d1+1) … Hid2) -Hid1 /2 width=1/ -Hd12 #Hid1 - >(sdsubst_vref_gt … Hid2) >sdsubst_vref_gt /2 width=1/ - >sdsubst_vref_gt // /2 width=1/ - ] - ] -| normalize #b #T #IHT #d1 #d2 #Hd12 - lapply (IHT (d1+1) (d2+1) ?) -IHT /2 width=1/ -| normalize #b #V #T #IHV #IHT #d1 #d2 #Hd12 - >IHV -IHV // >IHT -IHT // -] -qed. - -theorem sdsubst_sdsubst_lt: ∀G1,G2,F,d1,d2. d2 < d1 → - [d2 ↙ [d1 - d2 -1 ↙ G1] G2] [d1 ↙ G1] F = [d1 - 1 ↙ G1] [d2 ↙ G2] F. -#G1 #G2 #F #d1 #d2 #Hd21 -lapply (ltn_to_ltO … Hd21) #Hd1 ->sdsubst_sdsubst_ge in ⊢ (???%); /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) - ] -| #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 sliftable: predicate (relation subterms) ≝ λR. - ∀h,F1,F2. R F1 F2 → ∀d. R (↑[d, h] F1) (↑[d, h] F2). - -definition sdeliftable_sn: predicate (relation subterms) ≝ λR. - ∀h,G1,G2. R G1 G2 → ∀d,F1. ↑[d, h] F1 = G1 → - ∃∃F2. R F1 F2 & ↑[d, h] F2 = G2. -(* -lemma star_sliftable: ∀R. sliftable R → sliftable (star … R). -#R #HR #h #F1 #F2 #H elim H -F2 // /3 width=3/ -qed. - -lemma star_deliftable_sn: ∀R. sdeliftable_sn R → sdeliftable_sn (star … R). -#R #HR #h #G1 #G2 #H elim H -G2 /2 width=3/ -#G #G2 #_ #HG2 #IHG1 #d #F1 #HFG1 -elim (IHG1 … HFG1) -G1 #F #HF1 #HFG -elim (HR … HG2 … HFG) -G /3 width=3/ -qed-. - -lemma lstar_sliftable: ∀S,R. (∀a. sliftable (R a)) → - ∀l. sliftable (lstar S … R l). -#S #R #HR #l #h #F1 #F2 #H -@(lstar_ind_l ????????? H) -l -F1 // /3 width=3/ -qed. - -lemma lstar_sdeliftable_sn: ∀S,R. (∀a. sdeliftable_sn (R a)) → - ∀l. sdeliftable_sn (lstar S … R l). -#S #R #HR #l #h #G1 #G2 #H -@(lstar_ind_l ????????? H) -l -G1 /2 width=3/ -#a #l #G1 #G #HG1 #_ #IHG2 #d #F1 #HFG1 -elim (HR … HG1 … HFG1) -G1 #F #HF1 #HFG -elim (IHG2 … HFG) -G /3 width=3/ -qed-. -*) diff --git a/matita/matita/contribs/lambda/subterms/projections.ma b/matita/matita/contribs/lambda/subterms/projections.ma deleted file mode 100644 index 026a359c9..000000000 --- a/matita/matita/contribs/lambda/subterms/projections.ma +++ /dev/null @@ -1,128 +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 "terms/term.ma". -include "subterms/subterms.ma". - -(* PROJECTIONS **************************************************************) - -(* Note: the boolean subset of subterms *) -let rec boolean b M on M ≝ match M with -[ VRef i ⇒ {b}#i -| Abst A ⇒ {b}𝛌.(boolean b A) -| Appl B A ⇒ {b}@(boolean b B).(boolean b A) -]. - -interpretation "boolean subset (subterms)" - 'ProjectUp b M = (boolean b M). - -notation "hvbox( { term 46 b } ⇑ break term 46 M)" - non associative with precedence 46 - for @{ 'ProjectUp $b $M }. - -lemma boolean_inv_vref: ∀j,b0,b,M. {b}⇑ M = {b0}#j → b = b0 ∧ M = #j. -#j #b0 #b * normalize -[ #i #H destruct /2 width=1/ -| #A #H destruct -| #B #A #H destruct -] -qed-. - -lemma boolean_inv_abst: ∀U,b0,b,M. {b}⇑ M = {b0}𝛌.U → - ∃∃C. b = b0 & {b}⇑C = U & M = 𝛌.C. -#U #b0 #b * normalize -[ #i #H destruct -| #A #H destruct /2 width=3/ -| #B #A #H destruct -] -qed-. - -lemma boolean_inv_appl: ∀W,U,b0,b,M. {b}⇑ M = {b0}@W.U → - ∃∃D,C. b = b0 & {b}⇑D = W & {b}⇑C = U & M = @D.C. -#W #U #b0 #b * normalize -[ #i #H destruct -| #A #H destruct -| #B #A #H destruct /2 width=5/ -] -qed-. - -(* Note: the carrier (underlying term) of a subset of subterms *) -let rec carrier F on F ≝ match F with -[ SVRef _ i ⇒ #i -| SAbst _ T ⇒ 𝛌.(carrier T) -| SAppl _ V T ⇒ @(carrier V).(carrier T) -]. - -interpretation "carrier (subterms)" - 'ProjectDown F = (carrier F). - -notation "hvbox(⇓ term 46 F)" - non associative with precedence 46 - for @{ 'ProjectDown $F }. - -lemma carrier_inv_vref: ∀j,F. ⇓F = #j → ∃b. F = {b}#j. -#j * normalize -[ #b #i #H destruct /2 width=2/ -| #b #T #H destruct -| #b #V #T #H destruct -] -qed-. - -lemma carrier_inv_abst: ∀C,F. ⇓F = 𝛌.C → ∃∃b,U. ⇓U = C & F = {b}𝛌.U. -#C * normalize -[ #b #i #H destruct -| #b #T #H destruct /2 width=4/ -| #b #V #T #H destruct -] -qed-. - -lemma carrier_inv_appl: ∀D,C,F. ⇓F = @D.C → - ∃∃b,W,U. ⇓W = D & ⇓U = C & F = {b}@W.U. -#D #C * normalize -[ #b #i #H destruct -| #b #T #H destruct -| #b #V #T #H destruct /2 width=6/ -] -qed-. - -definition mk_boolean: bool → subterms → subterms ≝ - λb,F. {b}⇑⇓F. - -interpretation "make boolean (subterms)" - 'ProjectSame b F = (mk_boolean b F). - -notation "hvbox( { term 46 b } ⇕ break term 46 F)" - non associative with precedence 46 - for @{ 'ProjectSame $b $F }. - -lemma mk_boolean_inv_vref: ∀j,b0,b,F. {b}⇕ F = {b0}#j → - ∃∃b1. b = b0 & F = {b1}#j. -#j #b0 #b #F #H -elim (boolean_inv_vref … H) -H #H0 #H -elim (carrier_inv_vref … H) -H /2 width=2/ -qed-. - -lemma mk_boolean_inv_abst: ∀U,b0,b,F. {b}⇕ F = {b0}𝛌.U → - ∃∃b1,T. b = b0 & {b}⇕T = U & F = {b1}𝛌.T. -#U #b0 #b #F #H -elim (boolean_inv_abst … H) -H #C #H0 #H1 #H -elim (carrier_inv_abst … H) -H #b1 #U1 #H3 destruct /2 width=4/ -qed-. - -lemma mk_boolean_inv_appl: ∀W,U,b0,b,F. {b}⇕ F = {b0}@W.U → - ∃∃b1,V,T. b = b0 & {b}⇕V = W & {b}⇕T = U & F = {b1}@V.T. -#W #U #b0 #b #F #H -elim (boolean_inv_appl … H) -H #D #C #H0 #H1 #H2 #H -elim (carrier_inv_appl … H) -H #b1 #W1 #U1 #H3 #H4 destruct /2 width=6/ -qed-. diff --git a/matita/matita/contribs/lambda/subterms/relocating_substitution.ma b/matita/matita/contribs/lambda/subterms/relocating_substitution.ma new file mode 100644 index 000000000..43702a703 --- /dev/null +++ b/matita/matita/contribs/lambda/subterms/relocating_substitution.ma @@ -0,0 +1,155 @@ +(**************************************************************************) +(* ___ *) +(* ||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/relocation.ma". + +(* RELOCATING SUBSTITUTION **************************************************) + +(* Policy: depth (level) metavariables: d, e (as for lift) *) +let rec sdsubst G d F on F ≝ match F with +[ SVRef b i ⇒ tri … i d ({b}#i) (↑[i] G) ({b}#(i-1)) +| SAbst b T ⇒ {b}𝛌. (sdsubst G (d+1) T) +| SAppl b V T ⇒ {b}@ (sdsubst G d V). (sdsubst G d T) +]. + +interpretation "relocating substitution for subterms" + 'DSubst G d F = (sdsubst G d F). + +lemma sdsubst_vref_lt: ∀b,i,d,G. i < d → [d ↙ G] {b}#i = {b}#i. +normalize /2 width=1/ +qed. + +lemma sdsubst_vref_eq: ∀b,i,G. [i ↙ G] {b}#i = ↑[i]G. +normalize // +qed. + +lemma sdsubst_vref_gt: ∀b,i,d,G. d < i → [d ↙ G] {b}#i = {b}#(i-1). +normalize /2 width=1/ +qed. + +theorem sdsubst_slift_le: ∀h,G,F,d1,d2. d2 ≤ d1 → + [d2 ↙ ↑[d1 - d2, h] G] ↑[d1 + 1, h] F = ↑[d1, h] [d2 ↙ G] F. +#h #G #F elim F -F +[ #b #i #d1 #d2 #Hd21 elim (lt_or_eq_or_gt i d2) #Hid2 + [ lapply (lt_to_le_to_lt … Hid2 Hd21) -Hd21 #Hid1 + >(sdsubst_vref_lt … Hid2) >(slift_vref_lt … Hid1) >slift_vref_lt /2 width=1/ + | destruct >sdsubst_vref_eq >slift_vref_lt /2 width=1/ + | >(sdsubst_vref_gt … Hid2) -Hd21 elim (lt_or_ge (i-1) d1) #Hi1d1 + [ >(slift_vref_lt … Hi1d1) >slift_vref_lt /2 width=1/ + | lapply (ltn_to_ltO … Hid2) #Hi + >(slift_vref_ge … Hi1d1) >slift_vref_ge /2 width=1/ -Hi1d1 >plus_minus // /3 width=1/ + ] + ] +| normalize #b #T #IHT #d1 #d2 #Hd21 + lapply (IHT (d1+1) (d2+1) ?) -IHT /2 width=1/ +| normalize #b #V #T #IHV #IHT #d1 #d2 #Hd21 + >IHV -IHV // >IHT -IHT // +] +qed. + +theorem sdsubst_slift_be: ∀h,G,F,d1,d2. d1 ≤ d2 → d2 ≤ d1 + h → + [d2 ↙ G] ↑[d1, h + 1] F = ↑[d1, h] F. +#h #G #F elim F -F +[ #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+h) Hd21 ?) -Hd12 -Hd21 /2 width=1/ #Hd2 + >(slift_vref_ge … Hid1) >(slift_vref_ge … Hid1) -Hid1 + >sdsubst_vref_gt // /2 width=1/ + ] +| normalize #b #T #IHT #d1 #d2 #Hd12 #Hd21 + >IHT -IHT // /2 width=1/ +| normalize #b #V #T #IHV #IHT #d1 #d2 #Hd12 #Hd21 + >IHV -IHV // >IHT -IHT // +] +qed. + +theorem sdsubst_slift_ge: ∀h,G,F,d1,d2. d1 + h ≤ d2 → + [d2 ↙ G] ↑[d1, h] F = ↑[d1, h] [d2 - h ↙ G] F. +#h #G #F elim F -F +[ #b #i #d1 #d2 #Hd12 elim (lt_or_eq_or_gt i (d2-h)) #Hid2h + [ >(sdsubst_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 + >(slift_vref_lt … Hid1) -Hid1 /2 width=1/ + | >(slift_vref_ge … Hid1) -Hid1 -Hd12 /3 width=1/ + ] + | destruct elim (le_inv_plus_l … Hd12) -Hd12 #Hd12 #Hhd2 + >sdsubst_vref_eq >slift_vref_ge // >slift_slift_be // (sdsubst_vref_gt … Hid2h) + >slift_vref_ge /2 width=1/ >slift_vref_ge /2 width=1/ -Hid1 + >sdsubst_vref_gt /2 width=1/ -Hid2h >plus_minus // + ] +| normalize #b #T #IHT #d1 #d2 #Hd12 + elim (le_inv_plus_l … Hd12) #_ #Hhd2 + >IHT -IHT /2 width=1/ IHV -IHV // >IHT -IHT // +] +qed. + +theorem sdsubst_sdsubst_ge: ∀G1,G2,F,d1,d2. d1 ≤ d2 → + [d2 ↙ G2] [d1 ↙ G1] F = [d1 ↙ [d2 - d1 ↙ G2] G1] [d2 + 1 ↙ G2] F. +#G1 #G2 #F elim F -F +[ #b #i #d1 #d2 #Hd12 elim (lt_or_eq_or_gt i d1) #Hid1 + [ lapply (lt_to_le_to_lt … Hid1 Hd12) -Hd12 #Hid2 + >(sdsubst_vref_lt … Hid1) >(sdsubst_vref_lt … Hid2) >sdsubst_vref_lt /2 width=1/ + | destruct >sdsubst_vref_eq >sdsubst_vref_lt /2 width=1/ + | >(sdsubst_vref_gt … Hid1) elim (lt_or_eq_or_gt i (d2+1)) #Hid2 + [ lapply (ltn_to_ltO … Hid1) #Hi + >(sdsubst_vref_lt … Hid2) >sdsubst_vref_lt /2 width=1/ + | destruct /2 width=1/ + | lapply (le_to_lt_to_lt (d1+1) … Hid2) -Hid1 /2 width=1/ -Hd12 #Hid1 + >(sdsubst_vref_gt … Hid2) >sdsubst_vref_gt /2 width=1/ + >sdsubst_vref_gt // /2 width=1/ + ] + ] +| normalize #b #T #IHT #d1 #d2 #Hd12 + lapply (IHT (d1+1) (d2+1) ?) -IHT /2 width=1/ +| normalize #b #V #T #IHV #IHT #d1 #d2 #Hd12 + >IHV -IHV // >IHT -IHT // +] +qed. + +theorem sdsubst_sdsubst_lt: ∀G1,G2,F,d1,d2. d2 < d1 → + [d2 ↙ [d1 - d2 -1 ↙ G1] G2] [d1 ↙ G1] F = [d1 - 1 ↙ G1] [d2 ↙ G2] F. +#G1 #G2 #F #d1 #d2 #Hd21 +lapply (ltn_to_ltO … Hd21) #Hd1 +>sdsubst_sdsubst_ge in ⊢ (???%); /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) + ] +| #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 sliftable: predicate (relation subterms) ≝ λR. + ∀h,F1,F2. R F1 F2 → ∀d. R (↑[d, h] F1) (↑[d, h] F2). + +definition sdeliftable_sn: predicate (relation subterms) ≝ λR. + ∀h,G1,G2. R G1 G2 → ∀d,F1. ↑[d, h] F1 = G1 → + ∃∃F2. R F1 F2 & ↑[d, h] F2 = G2. +(* +lemma star_sliftable: ∀R. sliftable R → sliftable (star … R). +#R #HR #h #F1 #F2 #H elim H -F2 // /3 width=3/ +qed. + +lemma star_deliftable_sn: ∀R. sdeliftable_sn R → sdeliftable_sn (star … R). +#R #HR #h #G1 #G2 #H elim H -G2 /2 width=3/ +#G #G2 #_ #HG2 #IHG1 #d #F1 #HFG1 +elim (IHG1 … HFG1) -G1 #F #HF1 #HFG +elim (HR … HG2 … HFG) -G /3 width=3/ +qed-. +*) +lemma lstar_sliftable: ∀S,R. (∀a. sliftable (R a)) → + ∀l. sliftable (lstar S … R l). +#S #R #HR #l #h #F1 #F2 #H +@(lstar_ind_l ????????? H) -l -F1 // /3 width=3/ +qed. + +lemma lstar_sdeliftable_sn: ∀S,R. (∀a. sdeliftable_sn (R a)) → + ∀l. sdeliftable_sn (lstar S … R l). +#S #R #HR #l #h #G1 #G2 #H +@(lstar_ind_l ????????? H) -l -G1 /2 width=3/ +#a #l #G1 #G #HG1 #_ #IHG2 #d #F1 #HFG1 +elim (HR … HG1 … HFG1) -G1 #F #HF1 #HFG +elim (IHG2 … HFG) -G /3 width=3/ +qed-. diff --git a/matita/matita/contribs/lambda/terms/delifting_substitution.ma b/matita/matita/contribs/lambda/terms/delifting_substitution.ma deleted file mode 100644 index 3603fc031..000000000 --- a/matita/matita/contribs/lambda/terms/delifting_substitution.ma +++ /dev/null @@ -1,154 +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 "terms/lift.ma". - -(* DELIFTING SUBSTITUTION ***************************************************) - -(* Policy: depth (level) metavariables: d, e (as for lift) *) -let rec dsubst N d M on M ≝ match M with -[ VRef i ⇒ tri … i d (#i) (↑[i] N) (#(i-1)) -| Abst A ⇒ 𝛌. (dsubst N (d+1) A) -| Appl B A ⇒ @ (dsubst N d B). (dsubst N d A) -]. - -interpretation "delifting substitution" - 'DSubst N d M = (dsubst N d M). - -lemma dsubst_vref_lt: ∀i,d,N. i < d → [d ↙ N] #i = #i. -normalize /2 width=1/ -qed. - -lemma dsubst_vref_eq: ∀i,N. [i ↙ N] #i = ↑[i]N. -normalize // -qed. - -lemma dsubst_vref_gt: ∀i,d,N. d < i → [d ↙ N] #i = #(i-1). -normalize /2 width=1/ -qed. - -theorem dsubst_lift_le: ∀h,N,M,d1,d2. d2 ≤ d1 → - [d2 ↙ ↑[d1 - d2, h] N] ↑[d1 + 1, h] M = ↑[d1, h] [d2 ↙ N] M. -#h #N #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,N,M,d1,d2. d1 ≤ d2 → d2 ≤ d1 + h → - [d2 ↙ N] ↑[d1, h + 1] M = ↑[d1, h] M. -#h #N #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,N,M,d1,d2. d1 + h ≤ d2 → - [d2 ↙ N] ↑[d1, h] M = ↑[d1, h] [d2 - h ↙ N] M. -#h #N #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: ∀N1,N2,M,d1,d2. d1 ≤ d2 → - [d2 ↙ N2] [d1 ↙ N1] M = [d1 ↙ [d2 - d1 ↙ N2] N1] [d2 + 1 ↙ N2] M. -#N1 #N2 #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: ∀N1,N2,M,d1,d2. d2 < d1 → - [d2 ↙ [d1 - d2 -1 ↙ N1] N2] [d1 ↙ N1] M = [d1 - 1 ↙ N1] [d2 ↙ N2] M. -#N1 #N2 #M #d1 #d2 #Hd21 -lapply (ltn_to_ltO … Hd21) #Hd1 ->dsubst_dsubst_ge in ⊢ (???%); /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: ∀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 index 97306ef5d..4f41b75db 100644 --- a/matita/matita/contribs/lambda/terms/multiplicity.ma +++ b/matita/matita/contribs/lambda/terms/multiplicity.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "terms/delifting_substitution.ma". +include "terms/relocating_substitution.ma". (* MULTIPLICITY *************************************************************) diff --git a/matita/matita/contribs/lambda/terms/relocating_substitution.ma b/matita/matita/contribs/lambda/terms/relocating_substitution.ma new file mode 100644 index 000000000..ebf08b2f7 --- /dev/null +++ b/matita/matita/contribs/lambda/terms/relocating_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/relocation.ma". + +(* RELOCATING SUBSTITUTION **************************************************) + +(* Policy: depth (level) metavariables: d, e (as for lift) *) +let rec dsubst N d M on M ≝ match M with +[ VRef i ⇒ tri … i d (#i) (↑[i] N) (#(i-1)) +| Abst A ⇒ 𝛌. (dsubst N (d+1) A) +| Appl B A ⇒ @ (dsubst N d B). (dsubst N d A) +]. + +interpretation "relocating substitution" + 'DSubst N d M = (dsubst N d M). + +lemma dsubst_vref_lt: ∀i,d,N. i < d → [d ↙ N] #i = #i. +normalize /2 width=1/ +qed. + +lemma dsubst_vref_eq: ∀i,N. [i ↙ N] #i = ↑[i]N. +normalize // +qed. + +lemma dsubst_vref_gt: ∀i,d,N. d < i → [d ↙ N] #i = #(i-1). +normalize /2 width=1/ +qed. + +theorem dsubst_lift_le: ∀h,N,M,d1,d2. d2 ≤ d1 → + [d2 ↙ ↑[d1 - d2, h] N] ↑[d1 + 1, h] M = ↑[d1, h] [d2 ↙ N] M. +#h #N #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,N,M,d1,d2. d1 ≤ d2 → d2 ≤ d1 + h → + [d2 ↙ N] ↑[d1, h + 1] M = ↑[d1, h] M. +#h #N #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,N,M,d1,d2. d1 + h ≤ d2 → + [d2 ↙ N] ↑[d1, h] M = ↑[d1, h] [d2 - h ↙ N] M. +#h #N #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: ∀N1,N2,M,d1,d2. d1 ≤ d2 → + [d2 ↙ N2] [d1 ↙ N1] M = [d1 ↙ [d2 - d1 ↙ N2] N1] [d2 + 1 ↙ N2] M. +#N1 #N2 #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: ∀N1,N2,M,d1,d2. d2 < d1 → + [d2 ↙ [d1 - d2 -1 ↙ N1] N2] [d1 ↙ N1] M = [d1 - 1 ↙ N1] [d2 ↙ N2] M. +#N1 #N2 #M #d1 #d2 #Hd21 +lapply (ltn_to_ltO … Hd21) #Hd1 +>dsubst_dsubst_ge in ⊢ (???%); /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: ∀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/size.ma b/matita/matita/contribs/lambda/terms/size.ma index 8ba84e7cc..1fd9a060e 100644 --- a/matita/matita/contribs/lambda/terms/size.ma +++ b/matita/matita/contribs/lambda/terms/size.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "terms/lift.ma". +include "terms/relocation.ma". (* SIZE *********************************************************************)