From 2f42e0081e96a2d0a4097066af8349feebbd86fe Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Tue, 15 Jan 2013 10:34:32 +0000 Subject: [PATCH] - a few more lemmas ... - some renaming --- .../paths/alternative_standard_order.ma | 48 +++++++ .../lambda/paths/labeled_st_reduction.ma | 3 +- .../contribs/lambda/paths/standard_order.ma | 65 +-------- .../lambda/paths/standard_precedence.ma | 49 +++++++ .../contribs/lambda/subterms/boolean.ma | 70 ++++++++++ .../contribs/lambda/subterms/booleanize.ma | 57 ++++++++ .../contribs/lambda/subterms/carrier.ma | 69 ++++++++++ .../contribs/lambda/subterms/projections.ma | 128 ------------------ ...titution.ma => relocating_substitution.ma} | 10 +- .../subterms/{lift.ma => relocation.ma} | 3 +- .../contribs/lambda/terms/multiplicity.ma | 2 +- ...titution.ma => relocating_substitution.ma} | 6 +- .../lambda/terms/{lift.ma => relocation.ma} | 0 matita/matita/contribs/lambda/terms/size.ma | 2 +- 14 files changed, 306 insertions(+), 206 deletions(-) create mode 100644 matita/matita/contribs/lambda/paths/alternative_standard_order.ma create mode 100644 matita/matita/contribs/lambda/paths/standard_precedence.ma create mode 100644 matita/matita/contribs/lambda/subterms/boolean.ma create mode 100644 matita/matita/contribs/lambda/subterms/booleanize.ma create mode 100644 matita/matita/contribs/lambda/subterms/carrier.ma delete mode 100644 matita/matita/contribs/lambda/subterms/projections.ma rename matita/matita/contribs/lambda/subterms/{delifting_substitution.ma => relocating_substitution.ma} (97%) rename matita/matita/contribs/lambda/subterms/{lift.ma => relocation.ma} (99%) rename matita/matita/contribs/lambda/terms/{delifting_substitution.ma => relocating_substitution.ma} (97%) rename matita/matita/contribs/lambda/terms/{lift.ma => relocation.ma} (100%) 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/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/delifting_substitution.ma b/matita/matita/contribs/lambda/subterms/relocating_substitution.ma similarity index 97% rename from matita/matita/contribs/lambda/subterms/delifting_substitution.ma rename to matita/matita/contribs/lambda/subterms/relocating_substitution.ma index 272c75460..43702a703 100644 --- a/matita/matita/contribs/lambda/subterms/delifting_substitution.ma +++ b/matita/matita/contribs/lambda/subterms/relocating_substitution.ma @@ -12,9 +12,9 @@ (* *) (**************************************************************************) -include "subterms/lift.ma". +include "subterms/relocation.ma". -(* DELIFTING SUBSTITUTION ***************************************************) +(* RELOCATING SUBSTITUTION **************************************************) (* Policy: depth (level) metavariables: d, e (as for lift) *) let rec sdsubst G d F on F ≝ match F with @@ -23,7 +23,7 @@ let rec sdsubst G d F on F ≝ match F with | SAppl b V T ⇒ {b}@ (sdsubst G d V). (sdsubst G d T) ]. -interpretation "delifting substitution for subterms" +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. @@ -141,13 +141,13 @@ definition sdsubstable: predicate (relation subterms) ≝ λR. lemma star_sdsubstable_dx: ∀R. sdsubstable_dx R → sdsubstable_dx (star … R). #R #HR #G #F1 #F2 #H elim H -F2 // /3 width=3/ qed. - +*) lemma lstar_sdsubstable_dx: ∀S,R. (∀a. sdsubstable_dx (R a)) → ∀l. sdsubstable_dx (lstar S … R l). #S #R #HR #l #G #F1 #F2 #H @(lstar_ind_l ????????? H) -l -F1 // /3 width=3/ qed. - +(* lemma star_sdsubstable: ∀R. reflexive ? R → sdsubstable R → sdsubstable (star … R). #R #H1R #H2 #G1 #G2 #H elim H -G2 /3 width=1/ /3 width=5/ diff --git a/matita/matita/contribs/lambda/subterms/lift.ma b/matita/matita/contribs/lambda/subterms/relocation.ma similarity index 99% rename from matita/matita/contribs/lambda/subterms/lift.ma rename to matita/matita/contribs/lambda/subterms/relocation.ma index 0917949f0..5f64efc93 100644 --- a/matita/matita/contribs/lambda/subterms/lift.ma +++ b/matita/matita/contribs/lambda/subterms/relocation.ma @@ -236,7 +236,7 @@ lemma star_deliftable_sn: ∀R. sdeliftable_sn R → sdeliftable_sn (star … R) 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 @@ -251,4 +251,3 @@ lemma lstar_sdeliftable_sn: ∀S,R. (∀a. sdeliftable_sn (R a)) → elim (HR … HG1 … HFG1) -G1 #F #HF1 #HFG elim (IHG2 … HFG) -G /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/delifting_substitution.ma b/matita/matita/contribs/lambda/terms/relocating_substitution.ma similarity index 97% rename from matita/matita/contribs/lambda/terms/delifting_substitution.ma rename to matita/matita/contribs/lambda/terms/relocating_substitution.ma index 3603fc031..ebf08b2f7 100644 --- a/matita/matita/contribs/lambda/terms/delifting_substitution.ma +++ b/matita/matita/contribs/lambda/terms/relocating_substitution.ma @@ -12,9 +12,9 @@ (* *) (**************************************************************************) -include "terms/lift.ma". +include "terms/relocation.ma". -(* DELIFTING SUBSTITUTION ***************************************************) +(* RELOCATING SUBSTITUTION **************************************************) (* Policy: depth (level) metavariables: d, e (as for lift) *) let rec dsubst N d M on M ≝ match M with @@ -23,7 +23,7 @@ let rec dsubst N d M on M ≝ match M with | Appl B A ⇒ @ (dsubst N d B). (dsubst N d A) ]. -interpretation "delifting substitution" +interpretation "relocating substitution" 'DSubst N d M = (dsubst N d M). lemma dsubst_vref_lt: ∀i,d,N. i < d → [d ↙ N] #i = #i. diff --git a/matita/matita/contribs/lambda/terms/lift.ma b/matita/matita/contribs/lambda/terms/relocation.ma similarity index 100% rename from matita/matita/contribs/lambda/terms/lift.ma rename to matita/matita/contribs/lambda/terms/relocation.ma 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 *********************************************************************) -- 2.39.2