source: Deliverables/D3.3/id-lookup-branch/ASM/Vector.ma @ 3341

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

Change odd proof obligation problem back.

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