2 ||M|| This file is part of HELM, an Hypertextual, Electronic
3 ||A|| Library of Mathematics, developed at the Computer Science
4 ||T|| Department of the University of Bologna, Italy.
7 ||A|| This file is distributed under the terms of the
8 \ / GNU General Public License Version 2
10 V_______________________________________________________________ *)
12 include "basics/finset.ma".
13 include "basics/star.ma".
16 inductive FType (O:Type[0]): Type[0] ≝
18 | arrow : FType O → FType O → FType O.
20 inductive T (O:Type[0]) (D:O → FinSet): Type[0] ≝
21 | Val: ∀o:O.carr (D o) → T O D (* a value in a finset *)
22 | Rel: nat → T O D (* DB index, base is 0 *)
23 | App: T O D → T O D → T O D (* function, argument *)
24 | Lambda: FType O → T O D → T O D (* type, body *)
25 | Vec: FType O → list (T O D) → T O D (* type, body *)
28 let rec FinSet_of_FType O (D:O→FinSet) (ty:FType O) on ty : FinSet ≝
31 |arrow ty1 ty2 ⇒ FinFun (FinSet_of_FType O D ty1) (FinSet_of_FType O D ty2)
36 let rec size O D (M:T O D) on M ≝
40 |App P Q ⇒ size O D P + size O D Q + 1
41 |Lambda Ty P ⇒ size O D P + 1
42 |Vec Ty v ⇒ foldr ?? (λx,a. size O D x + a) 0 v +1
46 (* axiom pos_size: ∀M. 1 ≤ size M. *)
48 theorem Telim_size: ∀O,D.∀P: T O D → Prop.
49 (∀M. (∀N. size O D N < size O D M → P N) → P M) → ∀M. P M.
50 #O #D #P #H #M (cut (∀p,N. size O D N = p → P N))
52 #p @(nat_elim1 p) #m #H1 #N #sizeN @H #N0 #Hlt @(H1 (size O D N0)) //
56 ∀O: Type[0].∀D:O→FinSet.∀P:T O D→Prop.
57 (∀o:O.∀x:D o.P (Val O D o x)) →
59 (∀m,n:T O D.P m→P n→P (App O D m n)) →
60 (∀Ty:FType O.∀m:T O D.P m→P(Lambda O D Ty m)) →
61 (∀Ty:FType O.∀v:list (T O D).
62 (∀x:T O D. mem ? x v → P x) → P(Vec O D Ty v)) →
64 #O #D #P #Hval #Hrel #Happ #Hlam #Hvec @Telim_size #x cases x //
65 [ (* app *) #m #n #Hind @Happ @Hind // /2 by le_minus_to_plus/
66 | (* lam *) #ty #m #Hind @Hlam @Hind normalize //
67 | (* vec *) #ty #v #Hind @Hvec #x lapply Hind elim v
69 |#hd #tl #Hind1 #Hind2 *
70 [#Hx >Hx @Hind2 normalize //
71 |@Hind1 #N #H @Hind2 @(lt_to_le_to_lt … H) normalize //
77 (* since we only consider beta reduction with closed arguments we could avoid
78 lifting. We define it for the sake of generality *)
80 (* arguments: k is the nesting depth (starts from 0), p is the lift
81 let rec lift O D t k p on t ≝
83 [ Val o a ⇒ Val O D o a
84 | Rel n ⇒ if (leb k n) then Rel O D (n+p) else Rel O D n
85 | App m n ⇒ App O D (lift O D m k p) (lift O D n k p)
86 | Lambda Ty n ⇒ Lambda O D Ty (lift O D n (S k) p)
87 | Vec Ty v ⇒ Vec O D Ty (map ?? (λx. lift O D x k p) v)
90 notation "↑ ^ n ( M )" non associative with precedence 40 for @{'Lift 0 $n $M}.
91 notation "↑ _ k ^ n ( M )" non associative with precedence 40 for @{'Lift $n $k $M}.
93 interpretation "Lift" 'Lift n k M = (lift ?? M k n).
95 let rec subst O D t k s on t ≝
97 [ Val o a ⇒ Val O D o a
98 | Rel n ⇒ if (leb k n) then
99 (if (eqb k n) then lift O D s 0 n else Rel O D (n-1))
101 | App m n ⇒ App O D (subst O D m k s) (subst O D n k s)
102 | Lambda T n ⇒ Lambda O D T (subst O D n (S k) s)
103 | Vec T v ⇒ Vec O D T (map ?? (λx. subst O D x k s) v)
107 (* simplified version of subst, assuming the argument s is closed *)
109 let rec subst O D t k s on t ≝
111 [ Val o a ⇒ Val O D o a
112 | Rel n ⇒ if (leb k n) then
113 (if (eqb k n) then (* lift O D s 0 n*) s else Rel O D (n-1))
115 | App m n ⇒ App O D (subst O D m k s) (subst O D n k s)
116 | Lambda T n ⇒ Lambda O D T (subst O D n (S k) s)
117 | Vec T v ⇒ Vec O D T (map ?? (λx. subst O D x k s) v)
119 (* notation "hvbox(M break [ k ≝ N ])"
120 non associative with precedence 90
121 for @{'Subst1 $M $k $N}. *)
123 interpretation "Subst" 'Subst1 M k N = (subst M k N).
126 lemma subst_rel1: ∀O,D,A.∀k,i. i < k →
127 (Rel O D i) [k ≝ A] = Rel O D i.
128 #A #k #i normalize #ltik >(lt_to_leb_false … ltik) //
131 lemma subst_rel2: ∀O,D, A.∀k.
132 (Rel k) [k ≝ A] = lift A 0 k.
133 #A #k normalize >(le_to_leb_true k k) // >(eq_to_eqb_true … (refl …)) //
136 lemma subst_rel3: ∀A.∀k,i. k < i →
137 (Rel i) [k ≝ A] = Rel (i-1).
138 #A #k #i normalize #ltik >(le_to_leb_true k i) /2/
139 >(not_eq_to_eqb_false k i) // @lt_to_not_eq //
144 let rec closed_k O D (t: T O D) k on t ≝
148 | App m n ⇒ (closed_k O D m k) ∧ (closed_k O D n k)
149 | Lambda T n ⇒ closed_k O D n (k+1)
150 | Vec T v ⇒ closed_list O D v k
153 and closed_list O D (l: list (T O D)) k on l ≝
156 | cons hd tl ⇒ closed_k O D hd k ∧ closed_list O D tl k
160 inductive is_closed (O:Type[0]) (D:O→FinSet): nat → T O D → Prop ≝
161 | cval : ∀k,o,a.is_closed O D k (Val O D o a)
162 | crel : ∀k,n. n < k → is_closed O D k (Rel O D n)
163 | capp : ∀k,m,n. is_closed O D k m → is_closed O D k n →
164 is_closed O D k (App O D m n)
165 | clam : ∀T,k,m. is_closed O D (S k) m → is_closed O D k (Lambda O D T m)
166 | cvec: ∀T,k,v. (∀m. mem ? m v → is_closed O D k m) →
167 is_closed O D k (Vec O D T v).
169 lemma is_closed_rel: ∀O,D,n,k.
170 is_closed O D k (Rel O D n) → n < k.
171 #O #D #n #k #H inversion H
172 [#k0 #o #a #eqk #H destruct
173 |#k0 #n0 #ltn0 #eqk #H destruct //
174 |#k0 #M #N #_ #_ #_ #_ #_ #H destruct
175 |#T #k0 #M #_ #_ #_ #H destruct
176 |#T #k0 #v #_ #_ #_ #H destruct
180 lemma is_closed_app: ∀O,D,k,M, N.
181 is_closed O D k (App O D M N) → is_closed O D k M ∧ is_closed O D k N.
182 #O #D #k #M #N #H inversion H
183 [#k0 #o #a #eqk #H destruct
184 |#k0 #n0 #ltn0 #eqk #H destruct
185 |#k0 #M1 #N1 #HM #HN #_ #_ #_ #H1 destruct % //
186 |#T #k0 #M #_ #_ #_ #H destruct
187 |#T #k0 #v #_ #_ #_ #H destruct
191 lemma is_closed_lam: ∀O,D,k,ty,M.
192 is_closed O D k (Lambda O D ty M) → is_closed O D (S k) M.
193 #O #D #k #ty #M #H inversion H
194 [#k0 #o #a #eqk #H destruct
195 |#k0 #n0 #ltn0 #eqk #H destruct
196 |#k0 #M1 #N1 #HM #HN #_ #_ #_ #H1 destruct
197 |#T #k0 #M1 #HM1 #_ #_ #H1 destruct //
198 |#T #k0 #v #_ #_ #_ #H destruct
202 lemma is_closed_vec: ∀O,D,k,ty,v.
203 is_closed O D k (Vec O D ty v) → ∀m. mem ? m v → is_closed O D k m.
204 #O #D #k #ty #M #H inversion H
205 [#k0 #o #a #eqk #H destruct
206 |#k0 #n0 #ltn0 #eqk #H destruct
207 |#k0 #M1 #N1 #HM #HN #_ #_ #_ #H1 destruct
208 |#T #k0 #M1 #HM1 #_ #_ #H1 destruct
209 |#T #k0 #v #Hv #_ #_ #H1 destruct @Hv
213 lemma is_closed_S: ∀O,D,M,m.
214 is_closed O D m M → is_closed O D (S m) M.
215 #O #D #M #m #H elim H //
216 [#k #n0 #Hlt @crel @le_S //
217 |#k #P #Q #HP #HC #H1 #H2 @capp //
218 |#ty #k #P #HP #H1 @clam //
219 |#ty #k #v #Hind #Hv @cvec @Hv
223 lemma is_closed_mono: ∀O,D,M,m,n. m ≤ n →
224 is_closed O D m M → is_closed O D n M.
225 #O #D #M #m #n #lemn elim lemn // #i #j #H #H1 @is_closed_S @H @H1
229 (*** properties of lift and subst ***)
232 lemma lift_0: ∀O,D.∀t:T O D.∀k. lift O D t k 0 = t.
233 #O #D #t @(T_elim … t) normalize //
234 [#n #k cases (leb k n) normalize //
235 |#o #v #Hind #k @eq_f lapply Hind -Hind elim v //
236 #hd #tl #Hind #Hind1 normalize @eq_f2
237 [@Hind1 %1 //|@Hind #x #Hx @Hind1 %2 //]
241 lemma lift_closed: ∀O,D.∀t:T O D.∀k,p.
242 is_closed O D k t → lift O D t k p = t.
243 #O #D #t @(T_elim … t) normalize //
244 [#n #k #p #H >(not_le_to_leb_false … (lt_to_not_le … (is_closed_rel … H))) //
245 |#M #N #HindM #HindN #k #p #H lapply (is_closed_app … H) * #HcM #HcN
246 >(HindM … HcM) >(HindN … HcN) //
247 |#ty #M #HindM #k #p #H lapply (is_closed_lam … H) -H #H >(HindM … H) //
248 |#ty #v #HindM #k #p #H lapply (is_closed_vec … H) -H #H @eq_f
249 cut (∀m. mem ? m v → lift O D m k p = m)
250 [#m #Hmem @HindM [@Hmem | @H @Hmem]] -HindM
251 elim v // #a #tl #Hind #H1 normalize @eq_f2
252 [@H1 %1 //|@Hind #m #Hmem @H1 %2 @Hmem]
258 lemma subst_closed: ∀O,D,M,N,k,i. k ≤ i →
259 is_closed O D k M → subst O D M i N = M.
260 #O #D #M @(T_elim … M)
262 |#n #N #k #j #Hlt #Hc lapply (is_closed_rel … Hc) #Hnk normalize
263 >not_le_to_leb_false [2:@lt_to_not_le @(lt_to_le_to_lt … Hnk Hlt)] //
264 |#P #Q #HindP #HindQ #N #k #i #ltki #Hc lapply (is_closed_app … Hc) *
265 #HcP #HcQ normalize >(HindP … ltki HcP) >(HindQ … ltki HcQ) //
266 |#ty #P #HindP #N #k #i #ltki #Hc lapply (is_closed_lam … Hc)
267 #HcP normalize >(HindP … HcP) // @le_S_S @ltki
268 |#ty #v #Hindv #N #k #i #ltki #Hc lapply (is_closed_vec … Hc)
270 cut (∀m:T O D.mem (T O D) m v→ subst O D m i N=m)
271 [#m #Hmem @(Hindv … Hmem N … ltki) @Hcv @Hmem]
272 elim v // #a #tl #Hind #H normalize @eq_f2
273 [@H %1 //| @Hind #Hmem #Htl @H %2 @Htl]
277 lemma subst_lemma: ∀O,D,A,B,C,k,i. is_closed O D k B → is_closed O D i C →
278 subst O D (subst O D A i B) (k+i) C =
279 subst O D (subst O D A (k+S i) C) i B.
280 #O #D #A #B #C #k @(T_elim … A) normalize
282 |#n #i #HBc #HCc @(leb_elim i n) #Hle
283 [@(eqb_elim i n) #eqni
284 [<eqni >(lt_to_leb_false (k+(S i)) i) // normalize
285 >(subst_closed … HBc) // >le_to_leb_true // >eq_to_eqb_true //
287 [cases (le_to_or_lt_eq … Hle) // #eqin @False_ind /2/] #ltin
288 (cut (0 < n)) [@(le_to_lt_to_lt … ltin) //] #posn
289 normalize @(leb_elim (k+i) (n-1)) #nk
290 [@(eqb_elim (k+i) (n-1)) #H normalize
291 [cut (k+(S i) = n); [/2 by S_pred/] #H1
292 >(le_to_leb_true (k+(S i)) n) /2/
293 >(eq_to_eqb_true … H1) normalize >(subst_closed … HCc) //
294 |(cut (k+i < n-1)) [@not_eq_to_le_to_lt; //] #Hlt
295 >(le_to_leb_true (k+(S i)) n) normalize
296 [>(not_eq_to_eqb_false (k+(S i)) n) normalize
297 [>le_to_leb_true [2:@lt_to_le @(le_to_lt_to_lt … Hlt) //]
298 >not_eq_to_eqb_false // @lt_to_not_eq @(le_to_lt_to_lt … Hlt) //
299 |@(not_to_not … H) #Hn /2 by plus_minus/
301 |<plus_n_Sm @(lt_to_le_to_lt … Hlt) //
304 |>(not_le_to_leb_false (k+(S i)) n) normalize
305 [>(le_to_leb_true … Hle) >(not_eq_to_eqb_false … eqni) //
306 |@(not_to_not … nk) #H @le_plus_to_minus_r //
310 |(cut (n < k+i)) [@(lt_to_le_to_lt ? i) /2 by not_le_to_lt/] #ltn
311 >not_le_to_leb_false [2: @lt_to_not_le @(transitive_lt …ltn) //] normalize
312 >not_le_to_leb_false [2: @lt_to_not_le //] normalize
313 >(not_le_to_leb_false … Hle) //
315 |#M #N #HindM #HindN #i #HBC #HCc @eq_f2 [@HindM // |@HindN //]
316 |#ty #M #HindM #i #HBC #HCc @eq_f >plus_n_Sm >plus_n_Sm @HindM //
318 |#ty #v #Hindv #i #HBC #HCc @eq_f
319 cut (∀m.mem ? m v → subst O D (subst O D m i B) (k+i) C =
320 subst O D (subst O D m (k+S i) C) i B)
321 [#m #Hmem @Hindv //] -Hindv elim v normalize [//]
322 #a #tl #Hind #H @eq_f2 [@H %1 // | @Hind #m #Hmem @H %2 //]