source: src/ASM/Vector.ma @ 697

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

Merge Clight branch of vectors and friends.
Start making stuff build.

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