Context Navigation

Vector.ma @ 535

Last change on this file since 535 was 535, checked in by campbell, 8 years ago

Minimal integration of bitvectors into Clight semantics

does a "round trip" through Z for most operations (slow)
a few extra bits for equality on vectors
version of reverse that doesn't make matita fall over on size 32 vectors during disambiguation and automation

File size: 15.8 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 "cerco/Util.ma".
11
12	include "arithmetics/nat.ma".
13
14	include "oldlib/eq.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	//
83	qed.
84
85	let rec get_index_weak_v (A: Type[0]) (n: nat)
86	(v: Vector A n) (m: nat) on m ≝
87	match m with
88	[ O ⇒
89	match v with
90	[ VEmpty ⇒ None A
91	\| VCons p hd tl ⇒ Some A hd
92	]
93	\| S o ⇒
94	match v with
95	[ VEmpty ⇒ None A
96	\| VCons p hd tl ⇒ get_index_weak_v A p tl o
97	]
98	].
99
100	interpretation "Vector get_index" 'get_index_v v n = (get_index_v ? ? v n).
101
102	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 ≝
103	(match m with
104	[ O ⇒
105	match v return λx.λ_. O < x → Vector A x with
106	[ VEmpty ⇒ λabsd1: O < O. [[ ]]
107	\| VCons p hd tl ⇒ λprf1: O < S p. (a ::: tl)
108	]
109	\| S o ⇒
110	(match v return λx.λ_. S o < x → Vector A x with
111	[ VEmpty ⇒ λprf: S o < O. [[ ]]
112	\| VCons p hd tl ⇒ λprf: S o < S p. hd ::: (set_index A p tl o a ?)
113	])
114	]) lt.
115	normalize in prf ⊢ %;
116	/2/;
117	qed.
118
119	let rec set_index_weak (A: Type[0]) (n: nat)
120	(v: Vector A n) (m: nat) (a: A) on m ≝
121	match m with
122	[ O ⇒
123	match v with
124	[ VEmpty ⇒ None (Vector A n)
125	\| VCons o hd tl ⇒ Some (Vector A n) (? (VCons A o a tl))
126	]
127	\| S o ⇒
128	match v with
129	[ VEmpty ⇒ None (Vector A n)
130	\| VCons p hd tl ⇒
131	let settail ≝ set_index_weak A p tl o a in
132	match settail with
133	[ None ⇒ None (Vector A n)
134	\| Some j ⇒ Some (Vector A n) (? (VCons A p hd j))
135	]
136	]
137	].
138	//.
139	qed.
140
141	let rec drop (A: Type[0]) (n: nat)
142	(v: Vector A n) (m: nat) on m ≝
143	match m with
144	[ O ⇒ Some (Vector A n) v
145	\| S o ⇒
146	match v with
147	[ VEmpty ⇒ None (Vector A n)
148	\| VCons p hd tl ⇒ ? (drop A p tl o)
149	]
150	].
151	//.
152	qed.
153
154	let rec split (A: Type[0]) (m, n: nat) on m: Vector A (plus m n) → (Vector A m) × (Vector A n) ≝
155	match m return λm. Vector A (plus m n) → (Vector A m) × (Vector A n) with
156	[ O ⇒ λv. 〈[[ ]], v〉
157	\| S m' ⇒ λv.
158	match v return λl. λ_: Vector A l. l = S (plus m' n) → (Vector A (S m')) × (Vector A n) with
159	[ VEmpty ⇒ λK. ⊥
160	\| VCons o he tl ⇒ λK.
161	match split A m' n (tl⌈Vector A o ↦ Vector A (m' + n)⌉) with
162	[ pair v1 v2 ⇒ 〈he:::v1, v2〉
163	]
164	] (?: (S (m' + n)) = S (m' + n))].
165	//
166	[ destruct
167	\| lapply (injective_S … K)
168	//
169	]
170	qed.
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	\| lapply (injective_S … K)
183	//
184	]
185	qed.
186
187	definition from_singl: ∀A:Type[0]. Vector A (S O) → A ≝
188	λA: Type[0].
189	λv: Vector A (S 0).
190	fst … (head … v).
191
192	(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
193	(* Folds and builds. *)
194	(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
195
196	let rec fold_right (A: Type[0]) (B: Type[0]) (n: nat)
197	(f: A → B → B) (x: B) (v: Vector A n) on v ≝
198	match v with
199	[ VEmpty ⇒ x
200	\| VCons n hd tl ⇒ f hd (fold_right A B n f x tl)
201	].
202
203	let rec fold_right2_i (A: Type[0]) (B: Type[0]) (C: nat → Type[0])
204	(f: ∀N. A → B → C N → C (S N)) (c: C O) (n: nat)
205	(v: Vector A n) (q: Vector B n) on v : C n ≝
206	(match v return λx.λ_. x = n → C n with
207	[ VEmpty ⇒
208	match q return λx.λ_. O = x → C x with
209	[ VEmpty ⇒ λprf: O = O. c
210	\| VCons o hd tl ⇒ λabsd. ⊥
211	]
212	\| VCons o hd tl ⇒
213	match q return λx.λ_. S o = x → C x with
214	[ VEmpty ⇒ λabsd: S o = O. ⊥
215	\| VCons p hd' tl' ⇒ λprf: S o = S p.
216	(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)⌉
217	]
218	]) (refl ? n).
219	[1,2:
220	destruct
221	\|3,4:
222	lapply (injective_S … prf)
223	//
224	]
225	qed.
226
227	let rec fold_left (A: Type[0]) (B: Type[0]) (n: nat)
228	(f: A → B → A) (x: A) (v: Vector B n) on v ≝
229	match v with
230	[ VEmpty ⇒ x
231	\| VCons n hd tl ⇒ fold_left A B n f (f x hd) tl
232	].
233
234	(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
235	(* Maps and zips. *)
236	(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
237
238	let rec map (A: Type[0]) (B: Type[0]) (n: nat)
239	(f: A → B) (v: Vector A n) on v ≝
240	match v with
241	[ VEmpty ⇒ [[ ]]
242	\| VCons n hd tl ⇒ (f hd) ::: (map A B n f tl)
243	].
244
245	let rec zip_with (A: Type[0]) (B: Type[0]) (C: Type[0]) (n: nat)
246	(f: A → B → C) (v: Vector A n) (q: Vector B n) on v ≝
247	(match v return (λx.λr. x = n → Vector C x) with
248	[ VEmpty ⇒ λ_. [[ ]]
249	\| VCons n hd tl ⇒
250	match q return (λy.λr. S n = y → Vector C (S n)) with
251	[ VEmpty ⇒ ?
252	\| VCons m hd' tl' ⇒
253	λe: S n = S m.
254	(f hd hd') ::: (zip_with A B C n f tl ?)
255	]
256	])
257	(refl ? n).
258	[ #e
259	destruct(e);
260	\| lapply (injective_S … e)
261	# H
262	> H
263	@ tl'
264	]
265	qed.
266
267	definition zip ≝
268	λA, B: Type[0].
269	λn: nat.
270	λv: Vector A n.
271	λq: Vector B n.
272	zip_with A B (A × B) n (pair A B) v q.
273
274	(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
275	(* Building vectors from scratch *)
276	(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
277
278	let rec replicate (A: Type[0]) (n: nat) (h: A) on n ≝
279	match n return λn. Vector A n with
280	[ O ⇒ [[ ]]
281	\| S m ⇒ h ::: (replicate A m h)
282	].
283
284	(* DPM: fixme. Weird matita bug in base case. *)
285	let rec append (A: Type[0]) (n: nat) (m: nat)
286	(v: Vector A n) (q: Vector A m) on v ≝
287	match v return (λn.λv. Vector A (n + m)) with
288	[ VEmpty ⇒ (? q)
289	\| VCons o hd tl ⇒ hd ::: (append A o m tl q)
290	].
291	# H
292	assumption
293	qed.
294
295	notation "hvbox(l break @@ r)"
296	right associative with precedence 47
297	for @{ 'vappend $l $r }.
298
299	interpretation "Vector append" 'vappend v1 v2 = (append ??? v1 v2).
300
301	let rec scan_left (A: Type[0]) (B: Type[0]) (n: nat)
302	(f: A → B → A) (a: A) (v: Vector B n) on v ≝
303	a :::
304	(match v with
305	[ VEmpty ⇒ VEmpty A
306	\| VCons o hd tl ⇒ scan_left A B o f (f a hd) tl
307	]).
308
309	let rec scan_right (A: Type[0]) (B: Type[0]) (n: nat)
310	(f: A → B → A) (b: B) (v: Vector A n) on v ≝
311	match v with
312	[ VEmpty ⇒ ?
313	\| VCons o hd tl ⇒ f hd b :: (scan_right A B o f b tl)
314	].
315	//
316	qed.
317
318	(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
319	(* Other manipulations. *)
320	(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
321
322	(* At some points matita will attempt to reduce reverse with a known vector,
323	which reduces the equality proof for the cast. Normalising this proof needs
324	to be fast enough to keep matita usable. *)
325	let rec plus_n_Sm_fast (n:nat) on n : ∀m:nat. S (n+m) = n+S m ≝
326	match n return λn'.∀m.S(n'+m) = n'+S m with
327	[ O ⇒ λm.refl ??
328	\| S n' ⇒ λm. ?
329	]. normalize @(match plus_n_Sm_fast n' m with [ refl ⇒ ? ]) @refl qed.
330
331	let rec revapp (A: Type[0]) (n: nat) (m:nat)
332	(v: Vector A n) (acc: Vector A m) on v : Vector A (n + m) ≝
333	match v return λn'.λ_. Vector A (n' + m) with
334	[ VEmpty ⇒ acc
335	\| VCons o hd tl ⇒ (revapp ??? tl (hd:::acc))⌈Vector A (o+S m) ↦ Vector A (S o + m)⌉
336	].
337	> plus_n_Sm_fast @refl qed.
338
339	let rec reverse (A: Type[0]) (n: nat) (v: Vector A n) on v : Vector A n ≝
340	(revapp A n 0 v [[ ]])⌈Vector A (n+0) ↦ Vector A n⌉.
341	< plus_n_O @refl qed.
342
343	(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
344	(* Conversions to and from lists. *)
345	(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
346
347	let rec list_of_vector (A: Type[0]) (n: nat)
348	(v: Vector A n) on v ≝
349	match v return λn.λv. list A with
350	[ VEmpty ⇒ []
351	\| VCons o hd tl ⇒ hd :: (list_of_vector A o tl)
352	].
353
354	let rec vector_of_list (A: Type[0]) (l: list A) on l ≝
355	match l return λl. Vector A (length A l) with
356	[ nil ⇒ ?
357	\| cons hd tl ⇒ hd ::: (vector_of_list A tl)
358	].
359	normalize
360	@ VEmpty
361	qed.
362
363	(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
364	(* Rotates and shifts. *)
365	(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
366
367	let rec rotate_left (A: Type[0]) (n: nat)
368	(m: nat) (v: Vector A n) on m: Vector A n ≝
369	match m with
370	[ O ⇒ v
371	\| S o ⇒
372	match v with
373	[ VEmpty ⇒ [[ ]]
374	\| VCons p hd tl ⇒
375	rotate_left A (S p) o ((append A p ? tl [[hd]])⌈Vector A (p + S O) ↦ Vector A (S p)⌉)
376	]
377	].
378	//
379	qed.
380
381	definition rotate_right ≝
382	λA: Type[0].
383	λn, m: nat.
384	λv: Vector A n.
385	reverse A n (rotate_left A n m (reverse A n v)).
386
387	definition shift_left_1 ≝
388	λA: Type[0].
389	λn: nat.
390	λv: Vector A (S n).
391	λa: A.
392	match v return λy.λ_. y = S n → Vector A y with
393	[ VEmpty ⇒ λH.⊥
394	\| VCons o hd tl ⇒ λH.reverse … (a::: reverse … tl)
395	] (refl ? (S n)).
396	destruct.
397	qed.
398
399	definition shift_right_1 ≝
400	λA: Type[0].
401	λn: nat.
402	λv: Vector A (S n).
403	λa: A.
404	reverse … (shift_left_1 … (reverse … v) a).
405
406	definition shift_left ≝
407	λA: Type[0].
408	λn, m: nat.
409	λv: Vector A (S n).
410	λa: A.
411	iterate … (λx. shift_left_1 … x a) v m.
412
413	definition shift_right ≝
414	λA: Type[0].
415	λn, m: nat.
416	λv: Vector A (S n).
417	λa: A.
418	iterate … (λx. shift_right_1 … x a) v m.
419
420	(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
421	(* Decidable equality. *)
422	(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
423
424	let rec eq_v (A: Type[0]) (n: nat) (f: A → A → bool) (b: Vector A n) (c: Vector A n) on b : bool ≝
425	(match b return λx.λ_. n = x → bool with
426	[ VEmpty ⇒
427	match c return λx.λ_. x = O → bool with
428	[ VEmpty ⇒ λ_. true
429	\| VCons p hd tl ⇒ λabsd.⊥
430	]
431	\| VCons o hd tl ⇒
432	match c return λx.λ_. x = S o → bool with
433	[ VEmpty ⇒ λabsd.⊥
434	\| VCons p hd' tl' ⇒
435	λprf.
436	if (f hd hd') then
437	(eq_v A o f tl (tl'⌈Vector A p ↦ Vector A o⌉))
438	else
439	false
440	]
441	]) (refl ? n).
442	[1,2:
443	destruct
444	\| lapply (injective_S … prf);
445	# X
446	< X
447	%
448	]
449	qed.
450
451	lemma vector_inv_n: ∀A,n. ∀P:Vector A n → Prop. ∀v:Vector A n.
452	match n return λn'. (Vector A n' → Prop) → Vector A n' → Prop with
453	[ O ⇒ λP.λv.P [[ ]] → P v
454	\| S m ⇒ λP.λv.(∀h,t. P (VCons A m h t)) → P v
455	] P v.
456	@(λA,n. λP:Vector A n → Prop. λv. match v return
457	?
458	with [ VEmpty ⇒ ? \| VCons m h t ⇒ ? ] P)
459	[ // \| // ] qed.
460	(* XXX Proof below fails at qed.
461	#A #n #P * [ #H @H \| #m #h #t #H @H ] qed.
462	*)
463
464	lemma eq_v_elim: ∀P:bool → Prop. ∀A,f.
465	(∀Q:bool → Prop. ∀a,b. (a = b → Q true) → (a ≠ b → Q false) → Q (f a b)) →
466	∀n,x,y.
467	(x = y → P true) →
468	(x ≠ y → P false) →
469	P (eq_v A n f x y).
470	#P #A #f #f_elim #n #x elim x
471	[ #y @(vector_inv_n … y)
472	normalize /2/
473	\| #m #h #t #IH #y @(vector_inv_n … y)
474	#h' #t' #Ht #Hf whd in ⊢ (?%)
475	@(f_elim ? h h') #Eh
476	[ @IH [ #Et @Ht >Eh >Et @refl \| #NEt @Hf % #E' destruct (E') elim NEt /2/ ]
477	\| @Hf % #E' destruct (E') elim Eh /2/
478	]
479	] qed.
480
481	(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
482	(* Subvectors. *)
483	(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
484
485	definition mem ≝
486	λA: Type[0].
487	λeq_a : A → A → bool.
488	λn: nat.
489	λl: Vector A n.
490	λx: A.
491	fold_right … (λy,v. (eq_a x y) ∨ v) false l.
492
493	definition subvector_with ≝
494	λA: Type[0].
495	λn: nat.
496	λm: nat.
497	λf: A → A → bool.
498	λv: Vector A n.
499	λq: Vector A m.
500	fold_right ? ? ? (λx, v. (mem ? f ? q x) ∧ v) true v.
501
502	(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
503	(* Lemmas. *)
504	(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
505
506	lemma map_fusion:
507	∀A, B, C: Type[0].
508	∀n: nat.
509	∀v: Vector A n.
510	∀f: A → B.
511	∀g: B → C.
512	map B C n g (map A B n f v) = map A C n (λx. g (f x)) v.
513	#A #B #C #n #v #f #g
514	elim v
515	[ normalize
516	%
517	\| #N #H #V #H2
518	normalize
519	> H2
520	%
521	]
522	qed.

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

Download in other formats:

Original Format