source: src/ASM/Vector.ma @ 2121

Last change on this file since 2121 was 2121, checked in by sacerdot, 8 years ago

More functions moved to the places they belong to

File size: 24.4 KB
Line 
1(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
2(* Vector.ma: Fixed length polymorphic vectors, and routine operations on     *)
3(*            them.                                                           *)
4(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
5
6include "basics/lists/list.ma".
7include "basics/bool.ma".
8include "basics/types.ma".
9
10include "ASM/Util.ma".
11
12include "arithmetics/nat.ma".
13
14include "utilities/extranat.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
24lemma Vector_O:
25  ∀A: Type[0].
26  ∀v: Vector A 0.
27    v ≃ VEmpty A.
28 #A #v
29 generalize in match (refl … 0);
30 cases v in ⊢ (??%? → ?%%??); //
31 #n #hd #tl #absurd
32 destruct(absurd)
33qed.
34
35lemma Vector_Sn:
36  ∀A: Type[0].
37  ∀n: nat.
38  ∀v: Vector A (S n).
39    ∃hd: A. ∃tl: Vector A n.
40      v ≃ VCons A n hd tl.
41  #A #n #v
42  generalize in match (refl … (S n));
43  cases v in ⊢ (??%? → ??(λ_.??(λ_.?%%??)));
44  [1:
45    #absurd destruct(absurd)
46  |2:
47    #m #hd #tl #eq
48    <(injective_S … eq)
49    %{hd} %{tl} %
50  ]
51qed.
52
53(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
54(* Syntax.                                                                    *)
55(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
56
57notation "hvbox(hd break ::: tl)"
58  right associative with precedence 57
59  for @{ 'vcons $hd $tl }.
60
61notation "[[ list0 x sep ; ]]"
62  non associative with precedence 90
63  for ${fold right @'vnil rec acc @{'vcons $x $acc}}.
64
65interpretation "Vector vnil" 'vnil = (VEmpty ?).
66interpretation "Vector vcons" 'vcons hd tl = (VCons ? ? hd tl).
67
68notation "hvbox(l break !!! break n)"
69  non associative with precedence 90
70  for @{ 'get_index_v $l $n }.
71
72lemma dependent_rewrite_vectors:
73  ∀A:Type[0].
74  ∀n, m: nat.
75  ∀v1: Vector A n.
76  ∀v2: Vector A m.
77  ∀P: ∀m. Vector A m → Prop.
78    n = m → v1 ≃ v2 → P n v1 → P m v2.
79  #A #n #m #v1 #v2 #P #eq #jmeq
80  destruct #assm assumption
81qed.
82
83lemma jmeq_cons_vector_monotone:
84  ∀A: Type[0].
85  ∀m, n: nat.
86  ∀v: Vector A m.
87  ∀q: Vector A n.
88  ∀prf: m = n.
89  ∀hd: A.
90    v ≃ q → hd:::v ≃ hd:::q.
91  #A #m #n #v #q #prf #hd #E
92  @(dependent_rewrite_vectors A … E)
93  try assumption %
94qed.
95
96(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
97(* Lookup.                                                                    *)
98(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
99
100let rec get_index_v (A: Type[0]) (n: nat)
101                   (v: Vector A n) (m: nat) (lt: m < n) on m: A ≝
102  (match m with
103    [ O ⇒
104      match v return λx.λ_. O < x → A with
105        [ VEmpty ⇒ λabsd1: O < O. ?
106        | VCons p hd tl ⇒ λprf1: O < S p. hd
107        ]
108    | S o ⇒
109      (match v return λx.λ_. S o < x → A with
110        [ VEmpty ⇒ λprf: S o < O. ?
111        | VCons p hd tl ⇒ λprf: S o < S p. get_index_v A p tl o ?
112        ])
113    ]) lt.
114    [ cases (not_le_Sn_O O)
115      normalize in absd1;
116      # H
117      cases (H absd1)
118    | cases (not_le_Sn_O (S o))
119      normalize in prf;
120      # H
121      cases (H prf)
122    | normalize
123      normalize in prf;
124      @ le_S_S_to_le
125      assumption
126    ]
127qed.
128
129definition get_index' ≝
130  λA: Type[0].
131  λn, m: nat.
132  λb: Vector A (S (n + m)).
133    get_index_v A (S (n + m)) b n ?.
134  normalize
135  @le_S_S
136  cases m //
137qed.
138
139let rec get_index_weak_v (A: Type[0]) (n: nat)
140                         (v: Vector A n) (m: nat) on m ≝
141  match m with
142    [ O ⇒
143      match v with
144        [ VEmpty ⇒ None A
145        | VCons p hd tl ⇒ Some A hd
146        ]
147    | S o ⇒
148      match v with
149        [ VEmpty ⇒ None A
150        | VCons p hd tl ⇒ get_index_weak_v A p tl o
151        ]
152    ].
153   
154interpretation "Vector get_index" 'get_index_v v n = (get_index_v ? ? v n).
155
156let rec set_index (A: Type[0]) (n: nat) (v: Vector A n) (m: nat) (a: A) (lt: m < n) on m: Vector A n ≝
157  (match m with
158    [ O ⇒
159      match v return λx.λ_. O < x → Vector A x with
160        [ VEmpty ⇒ λabsd1: O < O. [[ ]]
161        | VCons p hd tl ⇒ λprf1: O < S p. (a ::: tl)
162        ]
163    | S o ⇒
164      (match v return λx.λ_. S o < x → Vector A x with
165        [ VEmpty ⇒ λprf: S o < O. [[ ]]
166        | VCons p hd tl ⇒ λprf: S o < S p. hd ::: (set_index A p tl o a ?)
167        ])
168    ]) lt.
169    normalize in prf ⊢ %;
170    /2/;
171qed.
172
173let rec set_index_weak (A: Type[0]) (n: nat)
174                       (v: Vector A n) (m: nat) (a: A) on m ≝
175  match m with
176    [ O ⇒
177      match v with
178        [ VEmpty ⇒ None (Vector A n)
179        | VCons o hd tl ⇒ Some (Vector A n) (? (VCons A o a tl))
180        ]
181    | S o ⇒
182      match v with
183        [ VEmpty ⇒ None (Vector A n)
184        | VCons p hd tl ⇒
185            let settail ≝ set_index_weak A p tl o a in
186              match settail with
187                [ None ⇒ None (Vector A n)
188                | Some j ⇒ Some (Vector A n) (? (VCons A p hd j))
189                ]
190        ]
191    ].
192    //.
193qed.
194
195let rec drop (A: Type[0]) (n: nat)
196             (v: Vector A n) (m: nat) on m ≝
197  match m with
198    [ O ⇒ Some (Vector A n) v
199    | S o ⇒
200      match v with
201        [ VEmpty ⇒ None (Vector A n)
202        | VCons p hd tl ⇒ ? (drop A p tl o)
203        ]
204    ].
205    //.
206qed.
207
208definition head' : ∀A:Type[0]. ∀n:nat. Vector A (S n) → A ≝
209λA,n,v. match v return λx.λ_. match x with [ O ⇒ True | _ ⇒ A ] with
210[ VEmpty ⇒ I | VCons _ hd _ ⇒ hd ].
211
212definition tail : ∀A:Type[0]. ∀n:nat. Vector A (S n) → Vector A n ≝
213λA,n,v. match v return λx.λ_. match x with [ O ⇒ True | S m ⇒ Vector A m ] with
214[ VEmpty ⇒ I | VCons m hd tl ⇒ tl ].
215
216let rec vsplit' (A: Type[0]) (m, n: nat) on m: Vector A (plus m n) → (Vector A m) × (Vector A n) ≝
217 match m return λm. Vector A (plus m n) → (Vector A m) × (Vector A n) with
218  [ O ⇒ λv. 〈[[ ]], v〉
219  | S m' ⇒ λv. let 〈l,r〉 ≝ vsplit' A m' n (tail ?? v) in 〈head' ?? v:::l, r〉
220  ].
221(* Prevent undesirable unfolding. *)
222let rec vsplit (A: Type[0]) (m, n: nat) (v:Vector A (plus m n)) on v : (Vector A m) × (Vector A n) ≝
223 vsplit' A m n v.
224
225lemma vsplit_zero:
226  ∀A,m.
227  ∀v: Vector A m.
228    〈[[]], v〉 = vsplit A 0 m v.
229  #A #m #v
230  cases v try %
231  #n #hd #tl %
232qed.
233
234definition head: ∀A: Type[0]. ∀n: nat. Vector A (S n) → A × (Vector A n) ≝
235  λA: Type[0].
236  λn: nat.
237  λv: Vector A (S n).
238  match v return λl. λ_: Vector A l. l = S n → A × (Vector A n) with
239  [ VEmpty ⇒ λK. ⊥
240  | VCons o he tl ⇒ λK. 〈he, (tl⌈Vector A o ↦ Vector A n⌉)〉
241  ] (? : S ? = S ?).
242  //
243  destruct
244qed.
245
246definition from_singl: ∀A:Type[0]. Vector A (S O) → A ≝
247 λA: Type[0].
248 λv: Vector A (S 0).
249   fst … (head … v).
250   
251(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
252(* Folds and builds.                                                          *)
253(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
254   
255let rec fold_right (A: Type[0]) (B: Type[0]) (n: nat)
256                    (f: A → B → B) (x: B) (v: Vector A n) on v ≝
257  match v with
258    [ VEmpty ⇒ x
259    | VCons n hd tl ⇒ f hd (fold_right A B n f x tl)
260    ].
261
262let rec fold_right_i (A: Type[0]) (B: nat → Type[0]) (n: nat)
263                     (f: ∀n. A → B n → B (S n)) (x: B 0) (v: Vector A n) on v ≝
264  match v with
265    [ VEmpty ⇒ x
266    | VCons n hd tl ⇒ f ? hd (fold_right_i A B n f x tl)
267    ].
268
269let rec fold_right2_i (A: Type[0]) (B: Type[0]) (C: nat → Type[0])
270                      (f: ∀N. A → B → C N → C (S N)) (c: C O) (n: nat)
271                      (v: Vector A n) (q: Vector B n) on v : C n ≝
272  (match v return λx.λ_. x = n → C n with
273    [ VEmpty ⇒
274      match q return λx.λ_. O = x → C x with
275        [ VEmpty ⇒ λprf: O = O. c
276        | VCons o hd tl ⇒ λabsd. ⊥
277        ]
278    | VCons o hd tl ⇒
279      match q return λx.λ_. S o = x → C x with
280        [ VEmpty ⇒ λabsd: S o = O. ⊥
281        | VCons p hd' tl' ⇒ λprf: S o = S p.
282           (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)⌉
283        ]
284    ]) (refl ? n).
285  [1,2:
286    destruct
287  |3,4:
288    lapply (injective_S … prf)
289    //
290  ]
291qed.
292 
293let rec fold_left (A: Type[0]) (B: Type[0]) (n: nat)
294                    (f: A → B → A) (x: A) (v: Vector B n) on v ≝
295  match v with
296    [ VEmpty ⇒ x
297    | VCons n hd tl ⇒ fold_left A B n f (f x hd) tl
298    ].
299   
300(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
301(* Maps and zips.                                                             *)
302(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
303
304let rec map (A: Type[0]) (B: Type[0]) (n: nat)
305             (f: A → B) (v: Vector A n) on v ≝
306  match v with
307    [ VEmpty ⇒ [[ ]]
308    | VCons n hd tl ⇒ (f hd) ::: (map A B n f tl)
309    ].
310
311let rec zip_with (A: Type[0]) (B: Type[0]) (C: Type[0]) (n: nat)
312             (f: A → B → C) (v: Vector A n) (q: Vector B n) on v ≝
313  (match v return (λx.λr. x = n → Vector C x) with
314    [ VEmpty ⇒ λ_. [[ ]]
315    | VCons n hd tl ⇒
316      match q return (λy.λr. S n = y → Vector C (S n)) with
317        [ VEmpty ⇒ ?
318        | VCons m hd' tl' ⇒
319            λe: S n = S m.
320              (f hd hd') ::: (zip_with A B C n f tl ?)
321        ]
322    ])
323    (refl ? n).
324  [ #e
325    destruct(e);
326  | lapply (injective_S … e)
327    # H
328    > H
329    @ tl'
330  ]
331qed.
332
333definition zip ≝
334  λA, B: Type[0].
335  λn: nat.
336  λv: Vector A n.
337  λq: Vector B n.
338    zip_with A B (A × B) n (mk_Prod A B) v q.
339
340(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
341(* Building vectors from scratch                                              *)
342(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
343
344let rec replicate (A: Type[0]) (n: nat) (h: A) on n ≝
345  match n return λn. Vector A n with
346    [ O ⇒ [[ ]]
347    | S m ⇒ h ::: (replicate A m h)
348    ].
349
350(* DPM: fixme.  Weird matita bug in base case. *)
351let rec append (A: Type[0]) (n: nat) (m: nat)
352                (v: Vector A n) (q: Vector A m) on v ≝
353  match v return (λn.λv. Vector A (n + m)) with
354    [ VEmpty ⇒ (? q)
355    | VCons o hd tl ⇒ hd ::: (append A o m tl q)
356    ].
357    # H
358    assumption
359qed.
360   
361notation "hvbox(l break @@ r)"
362  right associative with precedence 47
363  for @{ 'vappend $l $r }.
364   
365interpretation "Vector append" 'vappend v1 v2 = (append ??? v1 v2).
366
367lemma vector_append_zero:
368  ∀A,m.
369  ∀v: Vector A m.
370  ∀q: Vector A 0.
371    v = q@@v.
372  #A #m #v #q
373  >(Vector_O A q) %
374qed.
375
376lemma vector_cons_empty:
377  ∀A: Type[0].
378  ∀n: nat.
379  ∀v: Vector A n.
380    [[ ]] @@ v = v.
381  #A #n #v
382  cases v try %
383  #n' #hd #tl %
384qed.
385
386lemma vector_cons_append:
387  ∀A: Type[0].
388  ∀n: nat.
389  ∀e: A.
390  ∀v: Vector A n.
391    e ::: v = [[ e ]] @@ v.
392  #A #n #e #v
393  cases v try %
394  #n' #hd #tl %
395qed.
396
397lemma vector_cons_append2:
398  ∀A: Type[0].
399  ∀n, m: nat.
400  ∀v: Vector A n.
401  ∀q: Vector A m.
402  ∀hd: A.
403    hd:::(v@@q) = (hd:::v)@@q.
404  #A #n #m #v #q
405  elim v try (#hd %)
406  #n' #hd' #tl' #ih #hd'
407  <ih %
408qed.
409
410lemma vector_associative_append:
411  ∀A: Type[0].
412  ∀n, m, o:  nat.
413  ∀v: Vector A n.
414  ∀q: Vector A m.
415  ∀r: Vector A o.
416    (v @@ q) @@ r ≃ v @@ (q @@ r).
417  #A #n #m #o #v #q #r
418  elim v try %
419  #n' #hd #tl #ih
420  <(vector_cons_append2 A … hd)
421  @jmeq_cons_vector_monotone
422  try assumption
423  @associative_plus
424qed.
425
426lemma tail_head:
427  ∀a: Type[0].
428  ∀m, n: nat.
429  ∀hd: a.
430  ∀l: Vector a m.
431  ∀r: Vector a n.
432    tail a ? (hd:::(l@@r)) = l@@r.
433  #a #m #n #hd #l #r
434  cases l try %
435  #m' #hd' #tl' %
436qed.
437
438lemma head_head':
439  ∀a: Type[0].
440  ∀m: nat.
441  ∀hd: a.
442  ∀l: Vector a m.
443    hd = head' … (hd:::l).
444  #a #m #hd #l cases l try %
445  #m' #hd' #tl %
446qed.
447
448axiom vsplit_elim':
449  ∀A: Type[0].
450  ∀B: Type[1].
451  ∀l, m, v.
452  ∀T: Vector A l → Vector A m → B.
453  ∀P: B → Prop.
454    (∀lft, rgt. v = lft @@ rgt → P (T lft rgt)) →
455      P (let 〈lft, rgt〉 ≝ vsplit A l m v in T lft rgt).
456
457axiom vsplit_elim'':
458  ∀A: Type[0].
459  ∀B,B': Type[1].
460  ∀l, m, v.
461  ∀T: Vector A l → Vector A m → B.
462  ∀T': Vector A l → Vector A m → B'.
463  ∀P: B → B' → Prop.
464    (∀lft, rgt. v = lft @@ rgt → P (T lft rgt) (T' lft rgt)) →
465      P (let 〈lft, rgt〉 ≝ vsplit A l m v in T lft rgt)
466        (let 〈lft, rgt〉 ≝ vsplit A l m v in T' lft rgt).
467
468lemma vsplit_succ:
469  ∀A: Type[0].
470  ∀m, n: nat.
471  ∀l: Vector A m.
472  ∀r: Vector A n.
473  ∀v: Vector A (m + n).
474  ∀hd: A.
475    v = l@@r → (〈l, r〉 = vsplit A m n v → 〈hd:::l, r〉 = vsplit A (S m) n (hd:::v)).
476  #A #m
477  elim m
478  [1:
479    #n #l #r #v #hd #eq #hyp
480    destruct >(Vector_O … l) %
481  |2:
482    #m' #inductive_hypothesis #n #l #r #v #hd #equal #hyp
483    destruct
484    cases (Vector_Sn … l) #hd' #tl'
485    whd in ⊢ (???%);
486    >tail_head
487    <(? : vsplit A (S m') n (l@@r) = vsplit' A (S m') n (l@@r))
488    try (<hyp <head_head' %)
489    elim l normalize //
490  ]
491qed.
492
493corollary prod_vector_zero_eq_left:
494  ∀A, n.
495  ∀q: Vector A O.
496  ∀r: Vector A n.
497    〈q, r〉 = 〈[[ ]], r〉.
498  #A #n #q #r
499  generalize in match (Vector_O A q …);
500  #hyp destruct %
501qed.
502
503lemma vsplit_prod:
504  ∀A: Type[0].
505  ∀m, n: nat.
506  ∀p: Vector A (m + n).
507  ∀v: Vector A m.
508  ∀q: Vector A n.
509    p = v@@q → 〈v, q〉 = vsplit A m n p.
510  #A #m elim m
511  [1:
512    #n #p #v #q #hyp
513    >hyp <(vector_append_zero A n q v)
514    >(prod_vector_zero_eq_left A …)
515    @vsplit_zero
516  |2:
517    #r #ih #n #p #v #q #hyp
518    >hyp
519    cases (Vector_Sn A r v) #hd #exists
520    cases exists #tl #jmeq
521    >jmeq @vsplit_succ try %
522    @ih %
523  ]
524qed.
525
526definition vsplit_elim:
527  ∀A: Type[0].
528  ∀l, m: nat.
529  ∀v: Vector A (l + m).
530  ∀P: (Vector A l) × (Vector A m) → Prop.
531    (∀vl: Vector A l.
532     ∀vm: Vector A m.
533      v = vl@@vm → P 〈vl,vm〉) → P (vsplit A l m v) ≝
534  λa: Type[0].
535  λl, m: nat.
536  λv: Vector a (l + m).
537  λP. ?.
538  cases daemon
539qed.
540
541axiom vsplit_append:
542  ∀A: Type[0].
543  ∀m, n: nat.
544  ∀v, v': Vector A m.
545  ∀q, q': Vector A n.
546    let 〈v', q'〉 ≝ vsplit A m n (v@@q) in
547      v = v' ∧ q = q'.
548
549lemma vsplit_vector_singleton:
550  ∀A: Type[0].
551  ∀n: nat.
552  ∀v: Vector A (S n).
553  ∀rest: Vector A n.
554  ∀s: Vector A 1.
555    v = s @@ rest →
556    ((get_index_v A ? v 0 ?) ::: rest) = v.
557  [1:
558    #A #n #v cases daemon (* XXX: !!! *)
559  |2:
560    @le_S_S @le_O_n
561  ]
562qed.
563
564let rec scan_left (A: Type[0]) (B: Type[0]) (n: nat)
565                   (f: A → B → A) (a: A) (v: Vector B n) on v ≝
566  a :::
567    (match v with
568       [ VEmpty ⇒ VEmpty A
569       | VCons o hd tl ⇒ scan_left A B o f (f a hd) tl
570       ]).
571
572let rec scan_right (A: Type[0]) (B: Type[0]) (n: nat)
573                    (f: A → B → A) (b: B) (v: Vector A n) on v ≝
574  match v with
575    [ VEmpty ⇒ ?
576    | VCons o hd tl ⇒ f hd b :: (scan_right A B o f b tl)
577    ].
578    //
579qed.
580   
581(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
582(* Other manipulations.                                                       *)
583(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
584
585(* At some points matita will attempt to reduce reverse with a known vector,
586   which reduces the equality proof for the cast.  Normalising this proof needs
587   to be fast enough to keep matita usable, so use plus_n_Sm_fast. *)
588
589let rec revapp (A: Type[0]) (n: nat) (m:nat)
590                (v: Vector A n) (acc: Vector A m) on v : Vector A (n + m) ≝
591  match v return λn'.λ_. Vector A (n' + m) with
592    [ VEmpty ⇒ acc
593    | VCons o hd tl ⇒ (revapp ??? tl (hd:::acc))⌈Vector A (o+S m) ↦ Vector A (S o + m)⌉
594    ].
595< plus_n_Sm_fast @refl qed.
596
597let rec reverse (A: Type[0]) (n: nat) (v: Vector A n) on v : Vector A n ≝
598  (revapp A n 0 v [[ ]])⌈Vector A (n+0) ↦ Vector A n⌉.
599< plus_n_O @refl qed.
600
601let rec pad_vector (A:Type[0]) (a:A) (n,m:nat) (v:Vector A m) on n : Vector A (n+m) ≝
602match n return λn.Vector A (n+m) with
603[ O ⇒ v
604| S n' ⇒ a:::(pad_vector A a n' m v)
605].
606
607(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
608(* Conversions to and from lists.                                             *)
609(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
610
611let rec list_of_vector (A: Type[0]) (n: nat)
612                        (v: Vector A n) on v ≝
613  match v return λn.λv. list A with
614    [ VEmpty ⇒ []
615    | VCons o hd tl ⇒ hd :: (list_of_vector A o tl)
616    ].
617
618let rec vector_of_list (A: Type[0]) (l: list A) on l ≝
619  match l return λl. Vector A (length A l) with
620    [ nil ⇒ ?
621    | cons hd tl ⇒ hd ::: (vector_of_list A tl)
622    ].
623    normalize
624    @ VEmpty
625qed.
626
627(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)   
628(* Rotates and shifts.                                                        *)
629(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
630   
631let rec rotate_left (A: Type[0]) (n: nat)
632                     (m: nat) (v: Vector A n) on m: Vector A n ≝
633  match m with
634    [ O ⇒ v
635    | S o ⇒
636        match v with
637          [ VEmpty ⇒ [[ ]]
638          | VCons p hd tl ⇒
639             rotate_left A (S p) o ((append A p ? tl [[hd]])⌈Vector A (p + S O) ↦ Vector A (S p)⌉)
640          ]
641    ].
642  /2/
643qed.
644
645definition rotate_right ≝
646  λA: Type[0].
647  λn, m: nat.
648  λv: Vector A n.
649    reverse A n (rotate_left A n m (reverse A n v)).
650
651definition shift_left_1 ≝
652  λA: Type[0].
653  λn: nat.
654  λv: Vector A (S n).
655  λa: A.
656   match v return λy.λ_. y = S n → Vector A y with
657     [ VEmpty ⇒ λH.⊥
658     | VCons o hd tl ⇒ λH.reverse … (a::: reverse … tl)
659     ] (refl ? (S n)).
660 destruct.
661qed.
662
663
664(* XXX this is horrible - but useful to ensure that we can normalise in the proof assistant. *)
665definition switch_bv_plus : ∀A:Type[0]. ∀n,m. Vector A (n+m) → Vector A (m+n) ≝
666λA,n,m. match commutative_plus_faster n m return λx.λ_.Vector A (n+m) → Vector A x with [ refl ⇒ λi.i ].
667
668definition shift_right_1 ≝
669  λA: Type[0].
670  λn: nat.
671  λv: Vector A (S n).
672  λa: A.
673    let 〈v',dropped〉 ≝ vsplit ? n 1 (switch_bv_plus ? 1 n v) in a:::v'.
674(*    reverse … (shift_left_1 … (reverse … v) a).*)
675
676definition shift_left : ∀A:Type[0]. ∀n,m:nat. Vector A n → A → Vector A n ≝
677  λA: Type[0].
678  λn, m: nat.
679    match nat_compare n m return λx,y.λ_. Vector A x → A → Vector A x with
680    [ nat_lt _ _ ⇒ λv,a. replicate … a
681    | nat_eq _   ⇒ λv,a. replicate … a
682    | nat_gt d m ⇒ λv,a. let 〈v0,v'〉 ≝ vsplit … v in switch_bv_plus … (v' @@ (replicate … a))
683    ].
684
685(*    iterate … (λx. shift_left_1 … x a) v m.*)
686   
687definition shift_right ≝
688  λA: Type[0].
689  λn, m: nat.
690  λv: Vector A (S n).
691  λa: A.
692    iterate … (λx. shift_right_1 … x a) v m.
693
694(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
695(* Decidable equality.                                                        *)
696(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
697
698let rec eq_v (A: Type[0]) (n: nat) (f: A → A → bool) (b: Vector A n) (c: Vector A n) on b : bool ≝
699  (match b return λx.λ_. Vector A x → bool with
700   [ VEmpty ⇒ λc.
701       match c return λx.λ_. match x return λ_.Type[0] with [ O ⇒ bool | _ ⇒ True ] with
702       [ VEmpty ⇒ true
703       | VCons p hd tl ⇒ I
704       ]
705   | VCons m hd tl ⇒ λc. andb (f hd (head' A m c)) (eq_v A m f tl (tail A m c))
706   ]
707  ) c.
708
709lemma vector_inv_n: ∀A,n. ∀P:Vector A n → Type[0]. ∀v:Vector A n.
710  match n return λn'. (Vector A n' → Type[0]) → Vector A n' → Type[0] with
711  [ O ⇒ λP.λv.P [[ ]] → P v
712  | S m ⇒ λP.λv.(∀h,t. P (VCons A m h t)) → P v
713  ] P v.
714#A #n #P #v lapply P cases v normalize //
715qed.
716
717lemma eq_v_elim: ∀P:bool → Type[0]. ∀A,f.
718  (∀Q:bool → Type[0]. ∀a,b. (a = b → Q true) → (a ≠ b → Q false) → Q (f a b)) →
719  ∀n,x,y.
720  (x = y → P true) →
721  (x ≠ y → P false) →
722  P (eq_v A n f x y).
723#P #A #f #f_elim #n #x elim x
724[ #y @(vector_inv_n … y)
725  normalize /2/
726| #m #h #t #IH #y @(vector_inv_n … y)
727  #h' #t' #Ht #Hf whd in ⊢ (?%);
728  @(f_elim ? h h') #Eh
729  [ @IH [ #Et @Ht >Eh >Et @refl | #NEt @Hf % #E' destruct (E') elim NEt /2/ ]
730  | @Hf % #E' destruct (E') elim Eh /2/
731  ]
732] qed.
733
734lemma eq_v_true : ∀A,f. (∀a. f a a = true) → ∀n,v. eq_v A n f v v = true.
735#A #f #f_true #n #v elim v
736[ //
737| #m #h #t #IH whd in ⊢ (??%%); >f_true >IH @refl
738] qed.
739
740lemma vector_neq_tail : ∀A,n,h. ∀t,t':Vector A n. h:::t≠h:::t' → t ≠ t'.
741#A #n #h #t #t' * #NE % #E @NE >E @refl
742qed.
743
744lemma  eq_v_false : ∀A,f. (∀a,a'. f a a' = true → a = a') → ∀n,v,v'. v≠v' → eq_v A n f v v' = false.
745#A #f #f_true #n elim n
746[ #v #v' @(vector_inv_n ??? v) @(vector_inv_n ??? v') * #H @False_ind @H @refl
747| #m #IH #v #v' @(vector_inv_n ??? v) #h #t @(vector_inv_n ??? v') #h' #t'
748  #NE normalize lapply (f_true h h') cases (f h h') // #E @IH >E in NE; /2/
749] qed.
750
751(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
752(* Subvectors.                                                                *)
753(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
754
755definition mem ≝
756 λA: Type[0].
757 λeq_a : A → A → bool.
758 λn: nat.
759 λl: Vector A n.
760 λx: A.
761  fold_right … (λy,v. (eq_a x y) ∨ v) false l.
762
763lemma mem_append: ∀A,eq_a. (∀x. eq_a x x = true) → ∀n,m.∀v: Vector A n. ∀w: Vector A m. ∀x. mem A eq_a … (v@@x:::w) x.
764 #A #eq_a #refl #n #m #v elim v
765 [ #w #x whd whd in match (mem ?????); >refl //
766 | /2/
767 ]
768qed.
769
770lemma mem_monotonic_wrt_append:
771  ∀A: Type[0].
772  ∀m, o: nat.
773  ∀eq: A → A → bool.
774  ∀reflex: ∀a. eq a a = true.
775  ∀p: Vector A m.
776  ∀a: A.
777  ∀r: Vector A o.
778    mem A eq ? r a = true → mem A eq ? (p @@ r) a = true.
779  #A #m #o #eq #reflex #p #a
780  elim p try (#r #assm assumption)
781  #m' #hd #tl #inductive_hypothesis #r #assm
782  normalize
783  cases (eq ??) try %
784  @inductive_hypothesis assumption
785qed.
786
787
788let rec subvector_with
789  (a: Type[0]) (n: nat) (m: nat) (eq: a → a → bool) (sub: Vector a n) (sup: Vector a m)
790    on sub: bool ≝
791  match sub with
792  [ VEmpty         ⇒ true
793  | VCons n' hd tl ⇒
794    if mem … eq … sup hd then
795      subvector_with … eq tl sup
796    else
797      false
798  ].
799
800lemma subvector_with_refl0:
801 ∀A:Type[0]. ∀n. ∀eq: A → A → bool. (∀a. eq a a = true) → ∀v: Vector A n.
802  ∀m. ∀w: Vector A m. subvector_with A … eq v (w@@v).
803 #A #n #eq #refl #v elim v
804 [ //
805 | #m #hd #tl #IH #m #w whd in match (subvector_with ??????); >mem_append //
806   change with (bool_to_Prop (subvector_with ??????)) lapply (IH … (w@@[[hd]]))
807  lapply (vector_associative_append ???? w [[hd]] tl) #EQ
808  @(dependent_rewrite_vectors … EQ) //
809 ]
810qed.
811
812lemma subvector_with_refl:
813 ∀A:Type[0]. ∀n. ∀eq: A → A → bool. (∀a. eq a a = true) → ∀v: Vector A n.
814  subvector_with A … eq v v.
815 #A #n #eq #refl #v @(subvector_with_refl0 … v … [[]]) //
816qed.
817
818lemma subvector_multiple_append:
819  ∀A: Type[0].
820  ∀o, n: nat.
821  ∀eq: A → A → bool.
822  ∀refl: ∀a. eq a a = true.
823  ∀h: Vector A o.
824  ∀v: Vector A n.
825  ∀m: nat.
826  ∀q: Vector A m.
827    bool_to_Prop (subvector_with A ? ? eq v (h @@ q @@ v)).
828  #A #o #n #eq #reflex #h #v
829  elim v try (normalize #m #irrelevant @I)
830  #m' #hd #tl #inductive_hypothesis #m #q
831  change with (bool_to_Prop (andb ??))
832  cut ((mem A eq (o + (m + S m')) (h@@q@@hd:::tl) hd) = true)
833  [1:
834    @mem_monotonic_wrt_append try assumption
835    @mem_monotonic_wrt_append try assumption
836    normalize >reflex %
837  |2:
838    #assm >assm
839    >vector_cons_append
840    change with (bool_to_Prop (subvector_with ??????))
841    @(dependent_rewrite_vectors … (vector_associative_append … q [[hd]] tl))
842    try @associative_plus
843    @inductive_hypothesis
844  ]
845qed.
846
847
848
849(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
850(* Lemmas.                                                                    *)
851(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)   
852   
853lemma map_fusion:
854  ∀A, B, C: Type[0].
855  ∀n: nat.
856  ∀v: Vector A n.
857  ∀f: A → B.
858  ∀g: B → C.
859    map B C n g (map A B n f v) = map A C n (λx. g (f x)) v.
860  #A #B #C #n #v #f #g
861  elim v
862  [ normalize
863    %
864  | #N #H #V #H2
865    normalize
866    > H2
867    %
868  ]
869qed.
Note: See TracBrowser for help on using the repository browser.