source: Deliverables/D4.1/Matita/Vector.ma @ 370

Last change on this file since 370 was 370, checked in by mulligan, 9 years ago

Most of critical lemma done. Hole remaining that I can't coax matita into solving.

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