root/src/ASM/Vector.ma @ 1908

Revision 1908, 17.8 KB (checked in by fguidi, 14 months ago)

notation fixup following last commit of matita
we shifted the levels of precedence from 50 to 60 up by 5
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 57
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 browser.