source: src/ASM/Vector.ma @ 961

Last change on this file since 961 was 961, checked in by campbell, 10 years ago

Use precise bitvector sizes throughout the front end, rather than 32bits
everywhere.

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