]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/lib/pts_dummy/degree.ma
Many changes
[helm.git] / matita / matita / lib / pts_dummy / degree.ma
1 (**************************************************************************)
2 (*       ___                                                              *)
3 (*      ||M||                                                             *)
4 (*      ||A||       A project by Andrea Asperti                           *)
5 (*      ||T||                                                             *)
6 (*      ||I||       Developers:                                           *)
7 (*      ||T||         The HELM team.                                      *)
8 (*      ||A||         http://helm.cs.unibo.it                             *)
9 (*      \   /                                                             *)
10 (*       \ /        This file is distributed under the terms of the       *)
11 (*        v         GNU General Public License Version 2                  *)
12 (*                                                                        *)
13 (**************************************************************************)
14
15 include "pts_dummy/ext_lambda.ma".
16 (*
17 (* DEGREE ASSIGNMENT **********************************************************)
18
19 (* The degree of a term *******************************************************)
20
21 (* degree assigned to the term t in the environment L *)
22 let rec deg L t on t ≝ match t with
23    [ Sort i     ⇒ i + 3
24    | Rel i      ⇒ (nth i … L 0)
25    | App m _    ⇒ deg L m 
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
28    | D m        ⇒ deg L m
29    ].
30
31 interpretation "degree assignment (term)" 'IInt1 t L = (deg L t).
32
33 lemma deg_app: ∀m,n,L. ║App m n║_[L] = ║m║_[L].
34 // qed.
35
36 lemma deg_lambda: ∀n,m,L. ║Lambda n m║_[L] = ║m║_[║n║_[L]::L].
37 // qed.
38
39 lemma deg_prod: ∀n,m,L. ║Prod n m║_[L] = ║m║_[║n║_[L]::L].
40 // qed.
41
42 lemma deg_rel_lt: ∀L,K,i. (S i) ≤ |K| → ║Rel i║_[K @ L] = ║Rel i║_[K].
43 #L #K elim K -K [1: #i #Hie elim (not_le_Sn_O i) #Hi elim (Hi Hie) ]
44 #k #K #IHK #i elim i -i // #i #_ #Hie @IHK @le_S_S_to_le @Hie
45 qed.
46
47 lemma deg_rel_not_le: ∀L,K,i. (S i) ≰ |K| →
48                       ║Rel i║_[K @ L] = ║Rel (i-|K|)║_[L].
49 #L #K elim K -K [ normalize // ]
50 #k #K #IHK #i elim i -i [1: -IHK #Hie elim Hie -Hie #Hie; elim (Hie ?) /2/ ]
51 normalize #i #_ #Hie @IHK /2/
52 qed.
53
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 -HLk #Hik
61        >(deg_rel_lt … Hik) >(deg_rel_lt … Hik) //
62      | >(lift_rel_not_le … Hik) >HLk in Hik -HLk #Hik
63        >(deg_rel_not_le … Hik) <associative_append
64        >(deg_rel_not_le …) >length_append >HLp -HLp
65        [ >arith2 // @not_lt_to_le /2/ | @(arith3 … Hik) ]
66      ]
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 //
73    ]
74 qed.
75
76 lemma deg_lift_1: ∀t,N,L. ║lift t 0 1║_[N :: L] = ║t║_[L].
77 #t #N #L >(deg_lift ?? ([?]) … ([]) …) //
78 qed.
79
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]::L].
84 #v #L #t elim t -t //
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 -HLk #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/ ]
95        ]
96      ]
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 >(IHm … (? :: ?)) /2/
100    | #n #m #IHn #IHm #k #Lk #HLk >subst_prod > deg_prod
101      >IHn // >commutative_plus >(IHm … (? :: ?)) /2/
102    | #m #IHm #k #Lk #HLk >IHm //
103    ]
104 qed.
105
106 lemma deg_subst_0: ∀t,v,L. ║t[0≝v]║_[L] = ║t║_[║v║_[L]::L].
107 #t #v #L >(deg_subst ???? ([])) //
108 qed.
109
110 (* The degree context  ********************************************************)
111
112 (* degree context assigned to the type context G *)
113 let rec Deg L G on G ≝ match G with
114    [ nil      ⇒ L
115    | cons t F ⇒ let H ≝ Deg L F in ║t║_[H] - 1 :: H
116    ].
117
118 interpretation "degree assignment (type context)" 'IInt1 G L = (Deg L G).
119
120 interpretation "degree assignment (type context)" 'IInt G = (Deg (nil ?) G).
121
122 lemma Deg_cons: ∀L,F,t. let H ≝ Deg L F in
123                 ║t :: F║_[L] = ║t║_[H] - 1 :: H.
124 // qed.
125
126 lemma ltl_Deg: ∀L,G. ltl … (║G║_[L]) (|G|) = L.
127 #L #G elim G normalize //
128 qed.
129
130 lemma Deg_Deg: ∀L,G,H. ║H @ G║_[L] = ║H║_[║G║_[L]].
131 #L #G #H elim H normalize //
132 qed.
133
134 interpretation "degree assignment (type context)" 'IIntS1 G L = (lhd ? (Deg L G) (length ? G)).
135
136 lemma length_DegHd: ∀L,G. |║G║*_[L]| = |G|.
137 #L #G elim G normalize //
138 qed.
139
140 lemma Deg_decomp: ∀L,G. ║G║*_[L] @ L = ║G║_[L].
141 // qed.
142
143 lemma append_Deg: ∀L,G,H. ║H @ G║_[L] = ║H║*_[║G║_[L]] @ ║G║_[L].
144 // qed.
145
146 lemma DegHd_Lift: ∀L,Lp,p. p = |Lp| → 
147                   ∀G. ║Lift G p║*_[Lp @ L] = ║G║*_[L].
148 #L #Lp #p #HLp #G elim G //
149 #t #G #IH normalize >IH <Deg_decomp /4/
150 qed.
151
152 lemma Deg_lift_subst: ∀v,w,G. [║v║_[║G║]] = ║[w]║*_[║G║] →
153                       ∀t,k,Gk. k = |Gk| →
154                       ║lift t[k≝v] k 1 :: Lift Gk 1 @ [w] @ G║ =
155                       ║t :: Lift Gk 1 @ [w] @ G║.
156 #v #w #G #Hvw #t #k #Gk #HGk
157 >Deg_cons >Deg_cons in ⊢ (???%)
158 >append_Deg >append_Deg <Hvw -Hvw >DegHd_Lift; [2: //]
159 >deg_lift; [2,3: >HGk /2/] <(deg_subst … k) // >HGk /2/
160 qed.
161 *)