From a9355590f890b133763a1593fa706c0631e2c241 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Tue, 24 May 2011 12:19:11 +0000 Subject: [PATCH] degree.ma: we defined the "degree" of a term, which is meaningful in the lambda-cube --- matita/matita/lib/lambda/degree.ma | 118 +++++++++++++++++++++++++ matita/matita/lib/lambda/ext_lambda.ma | 6 +- 2 files changed, 121 insertions(+), 3 deletions(-) create mode 100644 matita/matita/lib/lambda/degree.ma diff --git a/matita/matita/lib/lambda/degree.ma b/matita/matita/lib/lambda/degree.ma new file mode 100644 index 000000000..a0d3a5ea6 --- /dev/null +++ b/matita/matita/lib/lambda/degree.ma @@ -0,0 +1,118 @@ +(**************************************************************************) +(* ___ *) +(* ||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 "lambda/ext_lambda.ma". + +(* DEGREE ASSIGNMENT **********************************************************) + +(* The degree of a term *******************************************************) + +(* degree assigned to the term t in the environment L *) +let rec deg L t on t ≝ match t with + [ Sort i ⇒ i + 3 + | Rel i ⇒ (nth i … L 0) - 1 + | App m _ ⇒ deg L m + | Lambda n m ⇒ let l ≝ deg L n in deg (l::L) m + | Prod n m ⇒ let l ≝ deg L n in deg (l::L) m + | D m ⇒ deg L m + ]. + +interpretation "degree assignment (term)" 'IInt1 t L = (deg L t). + +lemma deg_app: ∀m,n,L. ║App m n║_[L] = ║m║_[L]. +// qed. + +lemma deg_lambda: ∀n,m,L. ║Lambda n m║_[L] = ║m║_[║n║_[L]::L]. +// qed. + +lemma deg_prod: ∀n,m,L. ║Prod n m║_[L] = ║m║_[║n║_[L]::L]. +// qed. + +lemma deg_rel_lt: ∀LK,L,i. (S i) ≤ |L| → ║Rel i║_[L @ LK] = ║Rel i║_[L]. +#LK #L elim L -L [1: #i #Hie elim (not_le_Sn_O i) #Hi elim (Hi Hie) ] +#l #L #IHL #i elim i -i // #i #_ #Hie @IHL @le_S_S_to_le @Hie +qed. + +lemma deg_rel_not_le: ∀K,L,i. (S i) ≰ |L| → + ║Rel i║_[L @ K] = ║Rel (i-|L|)║_[K]. +#K #L elim L -L [ normalize // ] +#l #L #IHL #i elim i -i [1: -IHL #Hie elim Hie -Hie #Hie; elim (Hie ?) /2/ ] +normalize #i #_ #Hie @IHL /2/ +qed. + +(* weakeing and thinning lemma for the degree assignment *) +(* NOTE: >commutative_plus comes from |a::b| ↦ S |b| rather than |b| + 1 *) +lemma deg_lift: ∀p,L,Lp. p = |Lp| → ∀t,k,Lk. k = |Lk| → + ║lift t k p║_[Lk @ Lp @ L] = ║t║_[Lk @ L]. +#p #L #Lp #HLp #t elim t -t // + [ #i #k #Lk #HLk @(leb_elim (S i) k) #Hik + [ >(lift_rel_lt … Hik) >HLk in Hik #Hik + >(deg_rel_lt … Hik) >(deg_rel_lt … Hik) // + | >(lift_rel_not_le … Hik) >HLk in Hik #Hik + >(deg_rel_not_le … Hik) (deg_rel_not_le …) >length_append >HLp; + [ >arith2 // @not_lt_to_le /2/ | @(arith3 … Hik) ] + ] + | #m #n #IHm #_ #k #Lk #HLk >lift_app >deg_app /3/ + | #n #m #IHn #IHm #k #Lk #HLk >lift_lambda >deg_lambda + >IHn // >(IHm … (? :: ?)) // >commutative_plus /2/ + | #n #m #IHn #IHm #k #Lk #HLk >lift_prod >deg_prod + >IHn // >(IHm … (? :: ?)) // >commutative_plus /2/ + | #m #IHm #k #Lk #HLk >IHm // + ] +qed. + +lemma deg_lift_1: ∀t,N,L. ║lift t 0 1║_[N :: L] = ║t║_[L]. +#t #N #L >(deg_lift ?? ([?]) … ([]) …) // +qed. + +(* substitution lemma for the degree assignment *) +(* NOTE: >commutative_plus comes from |a::b| ↦ S |b| rather than |b| + 1 *) +lemma deg_subst: ∀v,L,t,k,Lk. k = |Lk| → + ║t[k≝v]║_[Lk @ L] = ║t║_[Lk @ ║v║_[L]+1::L]. +#v #L #t elim t -t // + [ #i #k #Lk #HLk @(leb_elim (S i) k) #H1ik + [ >(subst_rel1 … H1ik) >HLk in H1ik #H1ik + >(deg_rel_lt … H1ik) >(deg_rel_lt … H1ik) // + | @(eqb_elim i k) #H2ik + [ >H2ik in H1ik -H2ik i #H1ik >subst_rel2 >HLk in H1ik #H1ik + >(deg_rel_not_le … H1ik) (deg_lift ? ? ? ? ? ? ([])) normalize // + | lapply (arith4 … H1ik H2ik) -H1ik H2ik #Hik >(subst_rel3 … Hik) + >deg_rel_not_le; [2: /2/ ] <(associative_append ? ? ([?]) ?) + >deg_rel_not_le >length_append >commutative_plus; + [ subst_app >deg_app /3/ + | #n #m #IHn #IHm #k #Lk #HLk >subst_lambda > deg_lambda + >IHn // >commutative_plus in ⊢ (??(? ? %)?) >(IHm … (? :: ?)) /2/ + | #n #m #IHn #IHm #k #Lk #HLk >subst_prod > deg_prod + >IHn // >commutative_plus in ⊢ (??(? ? %)?) >(IHm … (? :: ?)) /2/ + | #m #IHm #k #Lk #HLk >IHm // + ] +qed. + +lemma deg_subst_0: ∀t,v,L. ║t[0≝v]║_[L] = ║t║_[║v║_[L]+1::L]. +#t #v #L >(deg_subst ???? ([])) // +qed. + +(* The degree context ********************************************************) + +(* degree context assigned to the type context G *) +let rec Deg G ≝ match G with + [ nil ⇒ nil … + | cons t F ⇒ let H ≝ Deg F in ║t║_[H] :: H + ]. + +interpretation "degree assignment (type context)" 'IInt G = (Deg G). diff --git a/matita/matita/lib/lambda/ext_lambda.ma b/matita/matita/lib/lambda/ext_lambda.ma index a183047e0..e0455c204 100644 --- a/matita/matita/lib/lambda/ext_lambda.ma +++ b/matita/matita/lib/lambda/ext_lambda.ma @@ -29,12 +29,12 @@ lemma lift_appl: ∀p,k,l,F. lift (Appl F l) p k = #p #k #l (elim l) -l /2/ #A #D #IHl #F >IHl // qed. *) - +(* lemma lift_rel_lt: ∀i,p,k. (S i) ≤ k → lift (Rel i) k p = Rel i. #i #p #k #Hik normalize >(le_to_leb_true … Hik) // qed. - -lemma lift_rel_ge: ∀i,p,k. (S i) ≰ k → lift (Rel i) k p = Rel (i+p). +*) +lemma lift_rel_not_le: ∀i,p,k. (S i) ≰ k → lift (Rel i) k p = Rel (i+p). #i #p #k #Hik normalize >(lt_to_leb_false (S i) k) /2/ qed. -- 2.39.2