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

Last change on this file since 374 was 374, checked in by sacerdot, 9 years ago

1) notation for cast fixed
2) ambiguity reduced: Empty => VEmpty, Cons => VCons
3) DoTest? modified to pretty-print the execution trace.

This should make debugging easier.

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