source: src/ASM/new-matita-development/Vector.ma @ 688

Last change on this file since 688 was 475, checked in by mulligan, 10 years ago

Matita interpreter ported to latest version of matita (the one with the tabs). To use, this directory must be copied into the /lib directory in the matita directory.

File size: 14.1 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/sums.ma".
9
10include "cerco/Util.ma".
11
12include "arithmetics/nat.ma".
13
14
15(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
16(* The datatype.                                                              *)
17(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
18
19inductive Vector (A: Type[0]): nat → Type[0] ≝
20  VEmpty: Vector A O
21| VCons: ∀n: nat. A → Vector A n → Vector A (S n).
22
23(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
24(* Syntax.                                                                    *)
25(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
26
27notation "hvbox(hd break ::: tl)"
28  right associative with precedence 52
29  for @{ 'vcons $hd $tl }.
30
31notation "[[ list0 x sep ; ]]"
32  non associative with precedence 90
33  for ${fold right @'vnil rec acc @{'vcons $x $acc}}.
34
35interpretation "Vector vnil" 'vnil = (VEmpty ?).
36interpretation "Vector vcons" 'vcons hd tl = (VCons ? ? hd tl).
37
38notation "hvbox(l break !!! break n)"
39  non associative with precedence 90
40  for @{ 'get_index_v $l $n }.
41
42(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
43(* Lookup.                                                                    *)
44(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
45
46let rec get_index_v (A: Type[0]) (n: nat)
47                   (v: Vector A n) (m: nat) (lt: m < n) on m: A ≝
48  (match m with
49    [ O ⇒
50      match v return λx.λ_. O < x → A with
51        [ VEmpty ⇒ λabsd1: O < O. ?
52        | VCons p hd tl ⇒ λprf1: O < S p. hd
53        ]
54    | S o ⇒
55      (match v return λx.λ_. S o < x → A with
56        [ VEmpty ⇒ λprf: S o < O. ?
57        | VCons p hd tl ⇒ λprf: S o < S p. get_index_v A p tl o ?
58        ])
59    ]) lt.
60    [ cases (not_le_Sn_O O)
61      normalize in absd1
62      # H
63      cases (H absd1)
64    | cases (not_le_Sn_O (S o))
65      normalize in prf
66      # H
67      cases (H prf)
68    | normalize
69      normalize in prf
70      @ le_S_S_to_le
71      assumption
72    ]
73qed.
74
75definition get_index' ≝
76  λA: Type[0].
77  λn, m: nat.
78  λb: Vector A (S (n + m)).
79    get_index_v A (S (n + m)) b n ?.
80  normalize
81  //
82qed.
83
84let rec get_index_weak_v (A: Type[0]) (n: nat)
85                         (v: Vector A n) (m: nat) on m ≝
86  match m with
87    [ O ⇒
88      match v with
89        [ VEmpty ⇒ None A
90        | VCons p hd tl ⇒ Some A hd
91        ]
92    | S o ⇒
93      match v with
94        [ VEmpty ⇒ None A
95        | VCons p hd tl ⇒ get_index_weak_v A p tl o
96        ]
97    ].
98   
99interpretation "Vector get_index" 'get_index_v v n = (get_index_v ? ? v n).
100
101let rec set_index (A: Type[0]) (n: nat) (v: Vector A n) (m: nat) (a: A) (lt: m < n) on m: Vector A n ≝
102  (match m with
103    [ O ⇒
104      match v return λx.λ_. O < x → Vector A x with
105        [ VEmpty ⇒ λabsd1: O < O. [[ ]]
106        | VCons p hd tl ⇒ λprf1: O < S p. (a ::: tl)
107        ]
108    | S o ⇒
109      (match v return λx.λ_. S o < x → Vector A x with
110        [ VEmpty ⇒ λprf: S o < O. [[ ]]
111        | VCons p hd tl ⇒ λprf: S o < S p. hd ::: (set_index A p tl o a ?)
112        ])
113    ]) lt.
114    normalize in prf ⊢ %;
115    /2/;
116qed.
117   
118let rec set_index_weak (A: Type[0]) (n: nat)
119                       (v: Vector A n) (m: nat) (a: A) on m ≝
120  match m with
121    [ O ⇒
122      match v with
123        [ VEmpty ⇒ None (Vector A n)
124        | VCons o hd tl ⇒ Some (Vector A n) (? (VCons A o a tl))
125        ]
126    | S o ⇒
127      match v with
128        [ VEmpty ⇒ None (Vector A n)
129        | VCons p hd tl ⇒
130            let settail ≝ set_index_weak A p tl o a in
131              match settail with
132                [ None ⇒ None (Vector A n)
133                | Some j ⇒ Some (Vector A n) (? (VCons A p hd j))
134                ]
135        ]
136    ].
137    //.
138qed.
139
140let rec drop (A: Type[0]) (n: nat)
141             (v: Vector A n) (m: nat) on m ≝
142  match m with
143    [ O ⇒ Some (Vector A n) v
144    | S o ⇒
145      match v with
146        [ VEmpty ⇒ None (Vector A n)
147        | VCons p hd tl ⇒ ? (drop A p tl o)
148        ]
149    ].
150    //.
151qed.
152
153let rec split (A: Type[0]) (m, n: nat) on m: Vector A (plus m n) → (Vector A m) × (Vector A n) ≝
154 match m return λm. Vector A (plus m n) → (Vector A m) × (Vector A n) with
155  [ O ⇒ λv. 〈[[ ]], v〉
156  | S m' ⇒ λv.
157    match v return λl. λ_: Vector A l. l = S (plus m' n) → (Vector A (S m')) × (Vector A n) with
158      [ VEmpty ⇒ λK. ⊥
159      | VCons o he tl ⇒ λK.
160        match split A m' n (tl⌈Vector A o ↦ Vector A (m' + n)⌉) with
161        [ mk_pair v1 v2 ⇒ 〈he:::v1, v2〉
162        ]
163      ] (?: (S (m' + n)) = S (m' + n))].
164      //
165      [ destruct
166      | lapply (injective_S … K)
167        //
168      ]
169qed.
170
171definition head: ∀A: Type[0]. ∀n: nat. Vector A (S n) → A × (Vector A n) ≝
172  λA: Type[0].
173  λn: nat.
174  λv: Vector A (S n).
175  match v return λl. λ_: Vector A l. l = S n → A × (Vector A n) with
176  [ VEmpty ⇒ λK. ⊥
177  | VCons o he tl ⇒ λK. 〈he, (tl⌈Vector A o ↦ Vector A n⌉)〉
178  ] (? : S ? = S ?).
179  //
180  [ destruct
181  | lapply (injective_S … K)
182    //
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_right2_i (A: Type[0]) (B: Type[0]) (C: nat → Type[0])
203                      (f: ∀N. A → B → C N → C (S N)) (c: C O) (n: nat)
204                      (v: Vector A n) (q: Vector B n) on v : C n ≝
205  (match v return λx.λ_. x = n → C n with
206    [ VEmpty ⇒
207      match q return λx.λ_. O = x → C x with
208        [ VEmpty ⇒ λprf: O = O. c
209        | VCons o hd tl ⇒ λabsd. ⊥
210        ]
211    | VCons o hd tl ⇒
212      match q return λx.λ_. S o = x → C x with
213        [ VEmpty ⇒ λabsd: S o = O. ⊥
214        | VCons p hd' tl' ⇒ λprf: S o = S p.
215           (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)⌉
216        ]
217    ]) (refl ? n).
218  [1,2:
219    destruct
220  |3,4:
221    lapply (injective_S … prf)
222    //
223  ]
224qed.
225 
226let rec fold_left (A: Type[0]) (B: Type[0]) (n: nat)
227                    (f: A → B → A) (x: A) (v: Vector B n) on v ≝
228  match v with
229    [ VEmpty ⇒ x
230    | VCons n hd tl ⇒ f (fold_left A B n f x tl) hd
231    ].
232   
233(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
234(* Maps and zips.                                                             *)
235(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
236
237let rec map (A: Type[0]) (B: Type[0]) (n: nat)
238             (f: A → B) (v: Vector A n) on v ≝
239  match v with
240    [ VEmpty ⇒ [[ ]]
241    | VCons n hd tl ⇒ (f hd) ::: (map A B n f tl)
242    ].
243
244let rec zip_with (A: Type[0]) (B: Type[0]) (C: Type[0]) (n: nat)
245             (f: A → B → C) (v: Vector A n) (q: Vector B n) on v ≝
246  (match v return (λx.λr. x = n → Vector C x) with
247    [ VEmpty ⇒ λ_. [[ ]]
248    | VCons n hd tl ⇒
249      match q return (λy.λr. S n = y → Vector C (S n)) with
250        [ VEmpty ⇒ ?
251        | VCons m hd' tl' ⇒
252            λe: S n = S m.
253              (f hd hd') ::: (zip_with A B C n f tl ?)
254        ]
255    ])
256    (refl ? n).
257  [ #e
258    destruct(e);
259  | lapply (injective_S … e)
260    # H
261    > H
262    @ tl'
263  ]
264qed.
265
266definition zip ≝
267  λA, B: Type[0].
268  λn: nat.
269  λv: Vector A n.
270  λq: Vector B n.
271    zip_with A B (A × B) n (mk_pair A B) v q.
272
273(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
274(* Building vectors from scratch                                              *)
275(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
276
277let rec replicate (A: Type[0]) (n: nat) (h: A) on n ≝
278  match n return λn. Vector A n with
279    [ O ⇒ [[ ]]
280    | S m ⇒ h ::: (replicate A m h)
281    ].
282
283(* DPM: fixme.  Weird matita bug in base case. *)
284let rec append (A: Type[0]) (n: nat) (m: nat)
285                (v: Vector A n) (q: Vector A m) on v ≝
286  match v return (λn.λv. Vector A (n + m)) with
287    [ VEmpty ⇒ (? q)
288    | VCons o hd tl ⇒ hd ::: (append A o m tl q)
289    ].
290    # H
291    assumption
292qed.
293   
294notation "hvbox(l break @@ r)"
295  right associative with precedence 47
296  for @{ 'vappend $l $r }.
297   
298interpretation "Vector append" 'vappend v1 v2 = (append ??? v1 v2).
299   
300let rec scan_left (A: Type[0]) (B: Type[0]) (n: nat)
301                   (f: A → B → A) (a: A) (v: Vector B n) on v ≝
302  a :::
303    (match v with
304       [ VEmpty ⇒ VEmpty A
305       | VCons o hd tl ⇒ scan_left A B o f (f a hd) tl
306       ]).
307
308let rec scan_right (A: Type[0]) (B: Type[0]) (n: nat)
309                    (f: A → B → A) (b: B) (v: Vector A n) on v ≝
310  match v with
311    [ VEmpty ⇒ ?
312    | VCons o hd tl ⇒ f hd b :: (scan_right A B o f b tl)
313    ].
314    //
315qed.
316   
317(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
318(* Other manipulations.                                                       *)
319(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
320
321let rec reverse (A: Type[0]) (n: nat)
322                 (v: Vector A n) on v ≝
323  match v return (λm.λv. Vector A m) with
324    [ VEmpty ⇒ [[ ]]
325    | VCons o hd tl ⇒ ? (append A o ? (reverse A o tl) [[hd]])
326    ].
327    //
328qed.
329
330(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
331(* Conversions to and from lists.                                             *)
332(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
333
334let rec list_of_vector (A: Type[0]) (n: nat)
335                        (v: Vector A n) on v ≝
336  match v return λn.λv. list A with
337    [ VEmpty ⇒ []
338    | VCons o hd tl ⇒ hd :: (list_of_vector A o tl)
339    ].
340
341let rec vector_of_list (A: Type[0]) (l: list A) on l ≝
342  match l return λl. Vector A (length A l) with
343    [ nil ⇒ ?
344    | cons hd tl ⇒ hd ::: (vector_of_list A tl)
345    ].
346    normalize
347    @ VEmpty
348qed.
349
350(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)   
351(* Rotates and shifts.                                                        *)
352(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
353   
354let rec rotate_left (A: Type[0]) (n: nat)
355                     (m: nat) (v: Vector A n) on m: Vector A n ≝
356  match m with
357    [ O ⇒ v
358    | S o ⇒
359        match v with
360          [ VEmpty ⇒ [[ ]]
361          | VCons p hd tl ⇒
362             rotate_left A (S p) o ((append A p ? tl [[hd]])⌈Vector A (p + S O) ↦ Vector A (S p)⌉)
363          ]
364    ].
365  //
366qed.
367
368definition rotate_right ≝
369  λA: Type[0].
370  λn, m: nat.
371  λv: Vector A n.
372    reverse A n (rotate_left A n m (reverse A n v)).
373
374definition shift_left_1 ≝
375  λA: Type[0].
376  λn: nat.
377  λv: Vector A (S n).
378  λa: A.
379   match v return λy.λ_. y = S n → Vector A y with
380     [ VEmpty ⇒ λH.⊥
381     | VCons o hd tl ⇒ λH.reverse … (a::: reverse … tl)
382     ] (refl ? (S n)).
383 destruct.
384qed.
385
386definition shift_right_1 ≝
387  λA: Type[0].
388  λn: nat.
389  λv: Vector A (S n).
390  λa: A.
391    reverse … (shift_left_1 … (reverse … v) a).
392   
393definition shift_left ≝
394  λA: Type[0].
395  λn, m: nat.
396  λv: Vector A (S n).
397  λa: A.
398    iterate … (λx. shift_left_1 … x a) v m.
399   
400definition shift_right ≝
401  λA: Type[0].
402  λn, m: nat.
403  λv: Vector A (S n).
404  λa: A.
405    iterate … (λx. shift_right_1 … x a) v m.
406
407(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
408(* Decidable equality.                                                        *)
409(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
410
411let rec eq_v (A: Type[0]) (n: nat) (f: A → A → bool) (b: Vector A n) (c: Vector A n) on b : bool ≝
412  (match b return λx.λ_. n = x → bool with
413    [ VEmpty ⇒
414      match c return λx.λ_. x = O → bool with
415        [ VEmpty ⇒ λ_. true
416        | VCons p hd tl ⇒ λabsd.⊥
417        ]
418    | VCons o hd tl ⇒
419        match c return λx.λ_. x = S o → bool with
420          [ VEmpty ⇒ λabsd.⊥
421          | VCons p hd' tl' ⇒
422            λprf.
423              if (f hd hd') then
424                (eq_v A o f tl (tl'⌈Vector A p ↦ Vector A o⌉))
425              else
426                false
427          ]
428    ]) (refl ? n).
429    [1,2:
430      destruct
431    | lapply (injective_S … prf);
432      # X
433      < X
434      %
435    ]
436qed.
437
438(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
439(* Subvectors.                                                                *)
440(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
441
442definition mem ≝
443 λA: Type[0].
444 λeq_a : A → A → bool.
445 λn: nat.
446 λl: Vector A n.
447 λx: A.
448  fold_right … (λy,v. (eq_a x y) ∨ v) false l.
449
450definition subvector_with ≝
451  λA: Type[0].
452  λn: nat.
453  λm: nat.
454  λf: A → A → bool.
455  λv: Vector A n.
456  λq: Vector A m.
457    fold_right ? ? ? (λx, v. (mem ? f ? q x) ∧ v) true v.
458   
459(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
460(* Lemmas.                                                                    *)
461(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)   
462   
463lemma map_fusion:
464  ∀A, B, C: Type[0].
465  ∀n: nat.
466  ∀v: Vector A n.
467  ∀f: A → B.
468  ∀g: B → C.
469    map B C n g (map A B n f v) = map A C n (λx. g (f x)) v.
470  #A #B #C #n #v #f #g
471  elim v
472  [ normalize
473    %
474  | #N #H #V #H2
475    normalize
476    > H2
477    %
478  ]
479qed.
Note: See TracBrowser for help on using the repository browser.