Context Navigation

Vector.ma @ 1517

Last change on this file since 1517 was 1516, checked in by sacerdot, 9 years ago
Ported to syntax of Matita 0.99.1.
File size: 17.7 KB

Line
1	(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
2	(* Vector.ma: Fixed length polymorphic vectors, and routine operations on *)
3	(* them. *)
4	(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
5
6	include "basics/list.ma".
7	include "basics/bool.ma".
8	include "basics/types.ma".
9
10	include "ASM/Util.ma".
11
12	include "arithmetics/nat.ma".
13
14	include "utilities/extranat.ma".
15
16	(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
17	(* The datatype. *)
18	(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
19
20	inductive Vector (A: Type[0]): nat → Type[0] ≝
21	VEmpty: Vector A O
22	\| VCons: ∀n: nat. A → Vector A n → Vector A (S n).
23
24	(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
25	(* Syntax. *)
26	(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
27
28	notation "hvbox(hd break ::: tl)"
29	right associative with precedence 52
30	for @{ 'vcons $hd $tl }.
31
32	notation "[[ list0 x sep ; ]]"
33	non associative with precedence 90
34	for ${fold right @'vnil rec acc @{'vcons $x $acc}}.
35
36	interpretation "Vector vnil" 'vnil = (VEmpty ?).
37	interpretation "Vector vcons" 'vcons hd tl = (VCons ? ? hd tl).
38
39	notation "hvbox(l break !!! break n)"
40	non associative with precedence 90
41	for @{ 'get_index_v $l $n }.
42
43	(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
44	(* Lookup. *)
45	(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
46
47	let rec get_index_v (A: Type[0]) (n: nat)
48	(v: Vector A n) (m: nat) (lt: m < n) on m: A ≝
49	(match m with
50	[ O ⇒
51	match v return λx.λ_. O < x → A with
52	[ VEmpty ⇒ λabsd1: O < O. ?
53	\| VCons p hd tl ⇒ λprf1: O < S p. hd
54	]
55	\| S o ⇒
56	(match v return λx.λ_. S o < x → A with
57	[ VEmpty ⇒ λprf: S o < O. ?
58	\| VCons p hd tl ⇒ λprf: S o < S p. get_index_v A p tl o ?
59	])
60	]) lt.
61	[ cases (not_le_Sn_O O)
62	normalize in absd1;
63	# H
64	cases (H absd1)
65	\| cases (not_le_Sn_O (S o))
66	normalize in prf;
67	# H
68	cases (H prf)
69	\| normalize
70	normalize in prf;
71	@ le_S_S_to_le
72	assumption
73	]
74	qed.
75
76	definition get_index' ≝
77	λA: Type[0].
78	λn, m: nat.
79	λb: Vector A (S (n + m)).
80	get_index_v A (S (n + m)) b n ?.
81	normalize
82	@le_S_S
83	cases m //
84	qed.
85
86	let rec get_index_weak_v (A: Type[0]) (n: nat)
87	(v: Vector A n) (m: nat) on m ≝
88	match m with
89	[ O ⇒
90	match v with
91	[ VEmpty ⇒ None A
92	\| VCons p hd tl ⇒ Some A hd
93	]
94	\| S o ⇒
95	match v with
96	[ VEmpty ⇒ None A
97	\| VCons p hd tl ⇒ get_index_weak_v A p tl o
98	]
99	].
100
101	interpretation "Vector get_index" 'get_index_v v n = (get_index_v ? ? v n).
102
103	let rec set_index (A: Type[0]) (n: nat) (v: Vector A n) (m: nat) (a: A) (lt: m < n) on m: Vector A n ≝
104	(match m with
105	[ O ⇒
106	match v return λx.λ_. O < x → Vector A x with
107	[ VEmpty ⇒ λabsd1: O < O. [[ ]]
108	\| VCons p hd tl ⇒ λprf1: O < S p. (a ::: tl)
109	]
110	\| S o ⇒
111	(match v return λx.λ_. S o < x → Vector A x with
112	[ VEmpty ⇒ λprf: S o < O. [[ ]]
113	\| VCons p hd tl ⇒ λprf: S o < S p. hd ::: (set_index A p tl o a ?)
114	])
115	]) lt.
116	normalize in prf ⊢ %;
117	/2/;
118	qed.
119
120	let rec set_index_weak (A: Type[0]) (n: nat)
121	(v: Vector A n) (m: nat) (a: A) on m ≝
122	match m with
123	[ O ⇒
124	match v with
125	[ VEmpty ⇒ None (Vector A n)
126	\| VCons o hd tl ⇒ Some (Vector A n) (? (VCons A o a tl))
127	]
128	\| S o ⇒
129	match v with
130	[ VEmpty ⇒ None (Vector A n)
131	\| VCons p hd tl ⇒
132	let settail ≝ set_index_weak A p tl o a in
133	match settail with
134	[ None ⇒ None (Vector A n)
135	\| Some j ⇒ Some (Vector A n) (? (VCons A p hd j))
136	]
137	]
138	].
139	//.
140	qed.
141
142	let rec drop (A: Type[0]) (n: nat)
143	(v: Vector A n) (m: nat) on m ≝
144	match m with
145	[ O ⇒ Some (Vector A n) v
146	\| S o ⇒
147	match v with
148	[ VEmpty ⇒ None (Vector A n)
149	\| VCons p hd tl ⇒ ? (drop A p tl o)
150	]
151	].
152	//.
153	qed.
154
155	definition head' : ∀A:Type[0]. ∀n:nat. Vector A (S n) → A ≝
156	λA,n,v. match v return λx.λ_. match x with [ O ⇒ True \| _ ⇒ A ] with
157	[ VEmpty ⇒ I \| VCons _ hd _ ⇒ hd ].
158
159	definition tail : ∀A:Type[0]. ∀n:nat. Vector A (S n) → Vector A n ≝
160	λA,n,v. match v return λx.λ_. match x with [ O ⇒ True \| S m ⇒ Vector A m ] with
161	[ VEmpty ⇒ I \| VCons m hd tl ⇒ tl ].
162
163	let rec split' (A: Type[0]) (m, n: nat) on m: Vector A (plus m n) → (Vector A m) × (Vector A n) ≝
164	match m return λm. Vector A (plus m n) → (Vector A m) × (Vector A n) with
165	[ O ⇒ λv. 〈[[ ]], v〉
166	\| S m' ⇒ λv. let 〈l,r〉 ≝ split' A m' n (tail ?? v) in 〈head' ?? v:::l, r〉
167	].
168	(* Prevent undesirable unfolding. *)
169	let rec split (A: Type[0]) (m, n: nat) (v:Vector A (plus m n)) on v : (Vector A m) × (Vector A n) ≝
170	split' A m n v.
171
172	definition head: ∀A: Type[0]. ∀n: nat. Vector A (S n) → A × (Vector A n) ≝
173	λA: Type[0].
174	λn: nat.
175	λv: Vector A (S n).
176	match v return λl. λ_: Vector A l. l = S n → A × (Vector A n) with
177	[ VEmpty ⇒ λK. ⊥
178	\| VCons o he tl ⇒ λK. 〈he, (tl⌈Vector A o ↦ Vector A n⌉)〉
179	] (? : S ? = S ?).
180	//
181	destruct
182	//
183	qed.
184
185	definition from_singl: ∀A:Type[0]. Vector A (S O) → A ≝
186	λA: Type[0].
187	λv: Vector A (S 0).
188	fst … (head … v).
189
190	(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
191	(* Folds and builds. *)
192	(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
193
194	let rec fold_right (A: Type[0]) (B: Type[0]) (n: nat)
195	(f: A → B → B) (x: B) (v: Vector A n) on v ≝
196	match v with
197	[ VEmpty ⇒ x
198	\| VCons n hd tl ⇒ f hd (fold_right A B n f x tl)
199	].
200
201	let rec fold_right_i (A: Type[0]) (B: nat → Type[0]) (n: nat)
202	(f: ∀n. A → B n → B (S n)) (x: B 0) (v: Vector A n) on v ≝
203	match v with
204	[ VEmpty ⇒ x
205	\| VCons n hd tl ⇒ f ? hd (fold_right_i A B n f x tl)
206	].
207
208	let rec fold_right2_i (A: Type[0]) (B: Type[0]) (C: nat → Type[0])
209	(f: ∀N. A → B → C N → C (S N)) (c: C O) (n: nat)
210	(v: Vector A n) (q: Vector B n) on v : C n ≝
211	(match v return λx.λ_. x = n → C n with
212	[ VEmpty ⇒
213	match q return λx.λ_. O = x → C x with
214	[ VEmpty ⇒ λprf: O = O. c
215	\| VCons o hd tl ⇒ λabsd. ⊥
216	]
217	\| VCons o hd tl ⇒
218	match q return λx.λ_. S o = x → C x with
219	[ VEmpty ⇒ λabsd: S o = O. ⊥
220	\| VCons p hd' tl' ⇒ λprf: S o = S p.
221	(f ? hd hd' (fold_right2_i A B C f c ? tl (tl'⌈Vector B p ↦ Vector B o⌉)))⌈C (S o) ↦ C (S p)⌉
222	]
223	]) (refl ? n).
224	[1,2:
225	destruct
226	\|3,4:
227	lapply (injective_S … prf)
228	//
229	]
230	qed.
231
232	let rec fold_left (A: Type[0]) (B: Type[0]) (n: nat)
233	(f: A → B → A) (x: A) (v: Vector B n) on v ≝
234	match v with
235	[ VEmpty ⇒ x
236	\| VCons n hd tl ⇒ fold_left A B n f (f x hd) tl
237	].
238
239	(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
240	(* Maps and zips. *)
241	(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
242
243	let rec map (A: Type[0]) (B: Type[0]) (n: nat)
244	(f: A → B) (v: Vector A n) on v ≝
245	match v with
246	[ VEmpty ⇒ [[ ]]
247	\| VCons n hd tl ⇒ (f hd) ::: (map A B n f tl)
248	].
249
250	let rec zip_with (A: Type[0]) (B: Type[0]) (C: Type[0]) (n: nat)
251	(f: A → B → C) (v: Vector A n) (q: Vector B n) on v ≝
252	(match v return (λx.λr. x = n → Vector C x) with
253	[ VEmpty ⇒ λ_. [[ ]]
254	\| VCons n hd tl ⇒
255	match q return (λy.λr. S n = y → Vector C (S n)) with
256	[ VEmpty ⇒ ?
257	\| VCons m hd' tl' ⇒
258	λe: S n = S m.
259	(f hd hd') ::: (zip_with A B C n f tl ?)
260	]
261	])
262	(refl ? n).
263	[ #e
264	destruct(e);
265	\| lapply (injective_S … e)
266	# H
267	> H
268	@ tl'
269	]
270	qed.
271
272	definition zip ≝
273	λA, B: Type[0].
274	λn: nat.
275	λv: Vector A n.
276	λq: Vector B n.
277	zip_with A B (A × B) n (pair A B) v q.
278
279	(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
280	(* Building vectors from scratch *)
281	(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
282
283	let rec replicate (A: Type[0]) (n: nat) (h: A) on n ≝
284	match n return λn. Vector A n with
285	[ O ⇒ [[ ]]
286	\| S m ⇒ h ::: (replicate A m h)
287	].
288
289	(* DPM: fixme. Weird matita bug in base case. *)
290	let rec append (A: Type[0]) (n: nat) (m: nat)
291	(v: Vector A n) (q: Vector A m) on v ≝
292	match v return (λn.λv. Vector A (n + m)) with
293	[ VEmpty ⇒ (? q)
294	\| VCons o hd tl ⇒ hd ::: (append A o m tl q)
295	].
296	# H
297	assumption
298	qed.
299
300	notation "hvbox(l break @@ r)"
301	right associative with precedence 47
302	for @{ 'vappend $l $r }.
303
304	interpretation "Vector append" 'vappend v1 v2 = (append ??? v1 v2).
305
306	axiom split_elim':
307	∀A: Type[0].
308	∀B: Type[1].
309	∀l, m, v.
310	∀T: Vector A l → Vector A m → B.
311	∀P: B → Prop.
312	(∀lft, rgt. v = lft @@ rgt → P (T lft rgt)) →
313	P (let 〈lft, rgt〉 ≝ split A l m v in T lft rgt).
314
315	axiom split_elim'':
316	∀A: Type[0].
317	∀B,B': Type[1].
318	∀l, m, v.
319	∀T: Vector A l → Vector A m → B.
320	∀T': Vector A l → Vector A m → B'.
321	∀P: B → B' → Prop.
322	(∀lft, rgt. v = lft @@ rgt → P (T lft rgt) (T' lft rgt)) →
323	P (let 〈lft, rgt〉 ≝ split A l m v in T lft rgt)
324	(let 〈lft, rgt〉 ≝ split A l m v in T' lft rgt).
325
326	let rec scan_left (A: Type[0]) (B: Type[0]) (n: nat)
327	(f: A → B → A) (a: A) (v: Vector B n) on v ≝
328	a :::
329	(match v with
330	[ VEmpty ⇒ VEmpty A
331	\| VCons o hd tl ⇒ scan_left A B o f (f a hd) tl
332	]).
333
334	let rec scan_right (A: Type[0]) (B: Type[0]) (n: nat)
335	(f: A → B → A) (b: B) (v: Vector A n) on v ≝
336	match v with
337	[ VEmpty ⇒ ?
338	\| VCons o hd tl ⇒ f hd b :: (scan_right A B o f b tl)
339	].
340	//
341	qed.
342
343	(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
344	(* Other manipulations. *)
345	(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
346
347	(* At some points matita will attempt to reduce reverse with a known vector,
348	which reduces the equality proof for the cast. Normalising this proof needs
349	to be fast enough to keep matita usable, so use plus_n_Sm_fast. *)
350
351	let rec revapp (A: Type[0]) (n: nat) (m:nat)
352	(v: Vector A n) (acc: Vector A m) on v : Vector A (n + m) ≝
353	match v return λn'.λ_. Vector A (n' + m) with
354	[ VEmpty ⇒ acc
355	\| VCons o hd tl ⇒ (revapp ??? tl (hd:::acc))⌈Vector A (o+S m) ↦ Vector A (S o + m)⌉
356	].
357	< plus_n_Sm_fast @refl qed.
358
359	let rec reverse (A: Type[0]) (n: nat) (v: Vector A n) on v : Vector A n ≝
360	(revapp A n 0 v [[ ]])⌈Vector A (n+0) ↦ Vector A n⌉.
361	< plus_n_O @refl qed.
362
363	let rec pad_vector (A:Type[0]) (a:A) (n,m:nat) (v:Vector A m) on n : Vector A (n+m) ≝
364	match n return λn.Vector A (n+m) with
365	[ O ⇒ v
366	\| S n' ⇒ a:::(pad_vector A a n' m v)
367	].
368
369	(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
370	(* Conversions to and from lists. *)
371	(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
372
373	let rec list_of_vector (A: Type[0]) (n: nat)
374	(v: Vector A n) on v ≝
375	match v return λn.λv. list A with
376	[ VEmpty ⇒ []
377	\| VCons o hd tl ⇒ hd :: (list_of_vector A o tl)
378	].
379
380	let rec vector_of_list (A: Type[0]) (l: list A) on l ≝
381	match l return λl. Vector A (length A l) with
382	[ nil ⇒ ?
383	\| cons hd tl ⇒ hd ::: (vector_of_list A tl)
384	].
385	normalize
386	@ VEmpty
387	qed.
388
389	(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
390	(* Rotates and shifts. *)
391	(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
392
393	let rec rotate_left (A: Type[0]) (n: nat)
394	(m: nat) (v: Vector A n) on m: Vector A n ≝
395	match m with
396	[ O ⇒ v
397	\| S o ⇒
398	match v with
399	[ VEmpty ⇒ [[ ]]
400	\| VCons p hd tl ⇒
401	rotate_left A (S p) o ((append A p ? tl [[hd]])⌈Vector A (p + S O) ↦ Vector A (S p)⌉)
402	]
403	].
404	/2/
405	qed.
406
407	definition rotate_right ≝
408	λA: Type[0].
409	λn, m: nat.
410	λv: Vector A n.
411	reverse A n (rotate_left A n m (reverse A n v)).
412
413	definition shift_left_1 ≝
414	λA: Type[0].
415	λn: nat.
416	λv: Vector A (S n).
417	λa: A.
418	match v return λy.λ_. y = S n → Vector A y with
419	[ VEmpty ⇒ λH.⊥
420	\| VCons o hd tl ⇒ λH.reverse … (a::: reverse … tl)
421	] (refl ? (S n)).
422	destruct.
423	qed.
424
425
426	(* XXX this is horrible - but useful to ensure that we can normalise in the proof assistant. *)
427	definition switch_bv_plus : ∀A:Type[0]. ∀n,m. Vector A (n+m) → Vector A (m+n) ≝
428	λA,n,m. match commutative_plus_faster n m return λx.λ_.Vector A (n+m) → Vector A x with [ refl ⇒ λi.i ].
429
430	definition shift_right_1 ≝
431	λA: Type[0].
432	λn: nat.
433	λv: Vector A (S n).
434	λa: A.
435	let 〈v',dropped〉 ≝ split ? n 1 (switch_bv_plus ? 1 n v) in a:::v'.
436	(* reverse … (shift_left_1 … (reverse … v) a).*)
437
438	definition shift_left : ∀A:Type[0]. ∀n,m:nat. Vector A n → A → Vector A n ≝
439	λA: Type[0].
440	λn, m: nat.
441	match nat_compare n m return λx,y.λ_. Vector A x → A → Vector A x with
442	[ nat_lt _ _ ⇒ λv,a. replicate … a
443	\| nat_eq _ ⇒ λv,a. replicate … a
444	\| nat_gt d m ⇒ λv,a. let 〈v0,v'〉 ≝ split … v in switch_bv_plus … (v' @@ (replicate … a))
445	].
446
447	(* iterate … (λx. shift_left_1 … x a) v m.*)
448
449	definition shift_right ≝
450	λA: Type[0].
451	λn, m: nat.
452	λv: Vector A (S n).
453	λa: A.
454	iterate … (λx. shift_right_1 … x a) v m.
455
456	(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
457	(* Decidable equality. *)
458	(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
459
460	let rec eq_v (A: Type[0]) (n: nat) (f: A → A → bool) (b: Vector A n) (c: Vector A n) on b : bool ≝
461	(match b return λx.λ_. Vector A x → bool with
462	[ VEmpty ⇒ λc.
463	match c return λx.λ_. match x return λ_.Type[0] with [ O ⇒ bool \| _ ⇒ True ] with
464	[ VEmpty ⇒ true
465	\| VCons p hd tl ⇒ I
466	]
467	\| VCons m hd tl ⇒ λc. andb (f hd (head' A m c)) (eq_v A m f tl (tail A m c))
468	]
469	) c.
470
471	lemma vector_inv_n: ∀A,n. ∀P:Vector A n → Type[0]. ∀v:Vector A n.
472	match n return λn'. (Vector A n' → Type[0]) → Vector A n' → Type[0] with
473	[ O ⇒ λP.λv.P [[ ]] → P v
474	\| S m ⇒ λP.λv.(∀h,t. P (VCons A m h t)) → P v
475	] P v.
476	#A #n #P #v lapply P cases v normalize //
477	qed.
478
479	lemma eq_v_elim: ∀P:bool → Type[0]. ∀A,f.
480	(∀Q:bool → Type[0]. ∀a,b. (a = b → Q true) → (a ≠ b → Q false) → Q (f a b)) →
481	∀n,x,y.
482	(x = y → P true) →
483	(x ≠ y → P false) →
484	P (eq_v A n f x y).
485	#P #A #f #f_elim #n #x elim x
486	[ #y @(vector_inv_n … y)
487	normalize /2/
488	\| #m #h #t #IH #y @(vector_inv_n … y)
489	#h' #t' #Ht #Hf whd in ⊢ (?%);
490	@(f_elim ? h h') #Eh
491	[ @IH [ #Et @Ht >Eh >Et @refl \| #NEt @Hf % #E' destruct (E') elim NEt /2/ ]
492	\| @Hf % #E' destruct (E') elim Eh /2/
493	]
494	] qed.
495
496	lemma eq_v_true : ∀A,f. (∀a. f a a = true) → ∀n,v. eq_v A n f v v = true.
497	#A #f #f_true #n #v elim v
498	[ //
499	\| #m #h #t #IH whd in ⊢ (??%%); >f_true >IH @refl
500	] qed.
501
502	lemma vector_neq_tail : ∀A,n,h. ∀t,t':Vector A n. h:::t≠h:::t' → t ≠ t'.
503	#A #n #h #t #t' * #NE % #E @NE >E @refl
504	qed.
505
506	lemma eq_v_false : ∀A,f. (∀a,a'. f a a' = true → a = a') → ∀n,v,v'. v≠v' → eq_v A n f v v' = false.
507	#A #f #f_true #n elim n
508	[ #v #v' @(vector_inv_n ??? v) @(vector_inv_n ??? v') * #H @False_ind @H @refl
509	\| #m #IH #v #v' @(vector_inv_n ??? v) #h #t @(vector_inv_n ??? v') #h' #t'
510	#NE normalize lapply (f_true h h') cases (f h h') // #E @IH >E in NE; /2/
511	] qed.
512
513	(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
514	(* Subvectors. *)
515	(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
516
517	definition mem ≝
518	λA: Type[0].
519	λeq_a : A → A → bool.
520	λn: nat.
521	λl: Vector A n.
522	λx: A.
523	fold_right … (λy,v. (eq_a x y) ∨ v) false l.
524
525
526	definition subvector_with ≝
527	λA: Type[0].
528	λn: nat.
529	λm: nat.
530	λf: A → A → bool.
531	λv: Vector A n.
532	λq: Vector A m.
533	fold_right ? ? ? (λx, v. (mem ? f ? q x) ∧ v) true v.
534
535	(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
536	(* Lemmas. *)
537	(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
538
539	lemma map_fusion:
540	∀A, B, C: Type[0].
541	∀n: nat.
542	∀v: Vector A n.
543	∀f: A → B.
544	∀g: B → C.
545	map B C n g (map A B n f v) = map A C n (λx. g (f x)) v.
546	#A #B #C #n #v #f #g
547	elim v
548	[ normalize
549	%
550	\| #N #H #V #H2
551	normalize
552	> H2
553	%
554	]
555	qed.

Note: See TracBrowser for help on using the repository browser.

Download in other formats:

Original Format