1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 include "lambda/ext_lambda.ma".
17 (* DEGREE ASSIGNMENT **********************************************************)
19 (* The degree of a term *******************************************************)
21 (* degree assigned to the term t in the environment L *)
22 let rec deg L t on t ≝ match t with
24 | Rel i ⇒ (nth i … L 0) - 1
26 | Lambda n m ⇒ let l ≝ deg L n in deg (l::L) m
27 | Prod n m ⇒ let l ≝ deg L n in deg (l::L) m
31 interpretation "degree assignment (term)" 'IInt1 t L = (deg L t).
33 lemma deg_app: ∀m,n,L. ║App m n║_[L] = ║m║_[L].
36 lemma deg_lambda: ∀n,m,L. ║Lambda n m║_[L] = ║m║_[║n║_[L]::L].
39 lemma deg_prod: ∀n,m,L. ║Prod n m║_[L] = ║m║_[║n║_[L]::L].
42 lemma deg_rel_lt: ∀LK,L,i. (S i) ≤ |L| → ║Rel i║_[L @ LK] = ║Rel i║_[L].
43 #LK #L elim L -L [1: #i #Hie elim (not_le_Sn_O i) #Hi elim (Hi Hie) ]
44 #l #L #IHL #i elim i -i // #i #_ #Hie @IHL @le_S_S_to_le @Hie
47 lemma deg_rel_not_le: ∀K,L,i. (S i) ≰ |L| →
48 ║Rel i║_[L @ K] = ║Rel (i-|L|)║_[K].
49 #K #L elim L -L [ normalize // ]
50 #l #L #IHL #i elim i -i [1: -IHL #Hie elim Hie -Hie #Hie; elim (Hie ?) /2/ ]
51 normalize #i #_ #Hie @IHL /2/
54 (* weakeing and thinning lemma for the degree assignment *)
55 (* NOTE: >commutative_plus comes from |a::b| ↦ S |b| rather than |b| + 1 *)
56 lemma deg_lift: ∀p,L,Lp. p = |Lp| → ∀t,k,Lk. k = |Lk| →
57 ║lift t k p║_[Lk @ Lp @ L] = ║t║_[Lk @ L].
58 #p #L #Lp #HLp #t elim t -t //
59 [ #i #k #Lk #HLk @(leb_elim (S i) k) #Hik
60 [ >(lift_rel_lt … Hik) >HLk in Hik #Hik
61 >(deg_rel_lt … Hik) >(deg_rel_lt … Hik) //
62 | >(lift_rel_not_le … Hik) >HLk in Hik #Hik
63 >(deg_rel_not_le … Hik) <associative_append
64 >(deg_rel_not_le …) >length_append >HLp;
65 [ >arith2 // @not_lt_to_le /2/ | @(arith3 … Hik) ]
67 | #m #n #IHm #_ #k #Lk #HLk >lift_app >deg_app /3/
68 | #n #m #IHn #IHm #k #Lk #HLk >lift_lambda >deg_lambda
69 >IHn // >(IHm … (? :: ?)) // >commutative_plus /2/
70 | #n #m #IHn #IHm #k #Lk #HLk >lift_prod >deg_prod
71 >IHn // >(IHm … (? :: ?)) // >commutative_plus /2/
72 | #m #IHm #k #Lk #HLk >IHm //
76 lemma deg_lift_1: ∀t,N,L. ║lift t 0 1║_[N :: L] = ║t║_[L].
77 #t #N #L >(deg_lift ?? ([?]) … ([]) …) //
80 (* substitution lemma for the degree assignment *)
81 (* NOTE: >commutative_plus comes from |a::b| ↦ S |b| rather than |b| + 1 *)
82 lemma deg_subst: ∀v,L,t,k,Lk. k = |Lk| →
83 ║t[k≝v]║_[Lk @ L] = ║t║_[Lk @ ║v║_[L]+1::L].
85 [ #i #k #Lk #HLk @(leb_elim (S i) k) #H1ik
86 [ >(subst_rel1 … H1ik) >HLk in H1ik #H1ik
87 >(deg_rel_lt … H1ik) >(deg_rel_lt … H1ik) //
88 | @(eqb_elim i k) #H2ik
89 [ >H2ik in H1ik -H2ik i #H1ik >subst_rel2 >HLk in H1ik #H1ik
90 >(deg_rel_not_le … H1ik) <minus_n_n >(deg_lift ? ? ? ? ? ? ([])) normalize //
91 | lapply (arith4 … H1ik H2ik) -H1ik H2ik #Hik >(subst_rel3 … Hik)
92 >deg_rel_not_le; [2: /2/ ] <(associative_append ? ? ([?]) ?)
93 >deg_rel_not_le >length_append >commutative_plus;
94 [ <minus_plus // | <HLk -HLk Lk @not_le_to_not_le_S_S /3/ ]
97 | #m #n #IHm #_ #k #Lk #HLk >subst_app >deg_app /3/
98 | #n #m #IHn #IHm #k #Lk #HLk >subst_lambda > deg_lambda
99 >IHn // >commutative_plus in ⊢ (??(? ? %)?) >(IHm … (? :: ?)) /2/
100 | #n #m #IHn #IHm #k #Lk #HLk >subst_prod > deg_prod
101 >IHn // >commutative_plus in ⊢ (??(? ? %)?) >(IHm … (? :: ?)) /2/
102 | #m #IHm #k #Lk #HLk >IHm //
106 lemma deg_subst_0: ∀t,v,L. ║t[0≝v]║_[L] = ║t║_[║v║_[L]+1::L].
107 #t #v #L >(deg_subst ???? ([])) //
110 (* The degree context ********************************************************)
112 (* degree context assigned to the type context G *)
113 let rec Deg G ≝ match G with
115 | cons t F ⇒ let H ≝ Deg F in ║t║_[H] :: H
118 interpretation "degree assignment (type context)" 'IInt G = (Deg G).