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

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

Do not use ndestruct for injectivity since it introduces StreickerK that
blocks reductions.

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