source: src/ASM/Vector.ma @ 1646

Last change on this file since 1646 was 1646, checked in by mulligan, 8 years ago

finished the block_costs computation, and propagated the changes forward, subject to closing two axioms (an elimination principle, and a lemma on subvectors). moved some code around to its rightful place.

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