source: Deliverables/D3.1/C-semantics/cerco/Vector.ma @ 533

Last change on this file since 533 was 533, checked in by campbell, 9 years ago

Make stuff from D4.1 work with my copy of matita.

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/types.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        [ 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 (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.