source: src/ASM/Vector.ma @ 2122

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

More stuff moved around in proper places

File size: 24.6 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_ok:
226  ∀A: Type[0].
227  ∀m, n: nat.
228  ∀v: Vector A (m + n).
229  ∀upper: Vector A m.
230  ∀lower: Vector A n.
231    〈upper, lower〉 = vsplit A m n v →
232      upper @@ lower = v.
233  #A #m #n #v #upper #lower
234  cases daemon
235qed.
236
237lemma vsplit_zero:
238  ∀A,m.
239  ∀v: Vector A m.
240    〈[[]], v〉 = vsplit A 0 m v.
241  #A #m #v
242  cases v try %
243  #n #hd #tl %
244qed.
245
246definition head: ∀A: Type[0]. ∀n: nat. Vector A (S n) → A × (Vector A n) ≝
247  λA: Type[0].
248  λn: nat.
249  λv: Vector A (S n).
250  match v return λl. λ_: Vector A l. l = S n → A × (Vector A n) with
251  [ VEmpty ⇒ λK. ⊥
252  | VCons o he tl ⇒ λK. 〈he, (tl⌈Vector A o ↦ Vector A n⌉)〉
253  ] (? : S ? = S ?).
254  //
255  destruct
256qed.
257
258definition from_singl: ∀A:Type[0]. Vector A (S O) → A ≝
259 λA: Type[0].
260 λv: Vector A (S 0).
261   fst … (head … v).
262   
263(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
264(* Folds and builds.                                                          *)
265(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
266   
267let rec fold_right (A: Type[0]) (B: Type[0]) (n: nat)
268                    (f: A → B → B) (x: B) (v: Vector A n) on v ≝
269  match v with
270    [ VEmpty ⇒ x
271    | VCons n hd tl ⇒ f hd (fold_right A B n f x tl)
272    ].
273
274let rec fold_right_i (A: Type[0]) (B: nat → Type[0]) (n: nat)
275                     (f: ∀n. A → B n → B (S n)) (x: B 0) (v: Vector A n) on v ≝
276  match v with
277    [ VEmpty ⇒ x
278    | VCons n hd tl ⇒ f ? hd (fold_right_i A B n f x tl)
279    ].
280
281let rec fold_right2_i (A: Type[0]) (B: Type[0]) (C: nat → Type[0])
282                      (f: ∀N. A → B → C N → C (S N)) (c: C O) (n: nat)
283                      (v: Vector A n) (q: Vector B n) on v : C n ≝
284  (match v return λx.λ_. x = n → C n with
285    [ VEmpty ⇒
286      match q return λx.λ_. O = x → C x with
287        [ VEmpty ⇒ λprf: O = O. c
288        | VCons o hd tl ⇒ λabsd. ⊥
289        ]
290    | VCons o hd tl ⇒
291      match q return λx.λ_. S o = x → C x with
292        [ VEmpty ⇒ λabsd: S o = O. ⊥
293        | VCons p hd' tl' ⇒ λprf: S o = S p.
294           (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)⌉
295        ]
296    ]) (refl ? n).
297  [1,2:
298    destruct
299  |3,4:
300    lapply (injective_S … prf)
301    //
302  ]
303qed.
304 
305let rec fold_left (A: Type[0]) (B: Type[0]) (n: nat)
306                    (f: A → B → A) (x: A) (v: Vector B n) on v ≝
307  match v with
308    [ VEmpty ⇒ x
309    | VCons n hd tl ⇒ fold_left A B n f (f x hd) tl
310    ].
311   
312(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
313(* Maps and zips.                                                             *)
314(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
315
316let rec map (A: Type[0]) (B: Type[0]) (n: nat)
317             (f: A → B) (v: Vector A n) on v ≝
318  match v with
319    [ VEmpty ⇒ [[ ]]
320    | VCons n hd tl ⇒ (f hd) ::: (map A B n f tl)
321    ].
322
323let rec zip_with (A: Type[0]) (B: Type[0]) (C: Type[0]) (n: nat)
324             (f: A → B → C) (v: Vector A n) (q: Vector B n) on v ≝
325  (match v return (λx.λr. x = n → Vector C x) with
326    [ VEmpty ⇒ λ_. [[ ]]
327    | VCons n hd tl ⇒
328      match q return (λy.λr. S n = y → Vector C (S n)) with
329        [ VEmpty ⇒ ?
330        | VCons m hd' tl' ⇒
331            λe: S n = S m.
332              (f hd hd') ::: (zip_with A B C n f tl ?)
333        ]
334    ])
335    (refl ? n).
336  [ #e
337    destruct(e);
338  | lapply (injective_S … e)
339    # H
340    > H
341    @ tl'
342  ]
343qed.
344
345definition zip ≝
346  λA, B: Type[0].
347  λn: nat.
348  λv: Vector A n.
349  λq: Vector B n.
350    zip_with A B (A × B) n (mk_Prod A B) v q.
351
352(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
353(* Building vectors from scratch                                              *)
354(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
355
356let rec replicate (A: Type[0]) (n: nat) (h: A) on n ≝
357  match n return λn. Vector A n with
358    [ O ⇒ [[ ]]
359    | S m ⇒ h ::: (replicate A m h)
360    ].
361
362(* DPM: fixme.  Weird matita bug in base case. *)
363let rec append (A: Type[0]) (n: nat) (m: nat)
364                (v: Vector A n) (q: Vector A m) on v ≝
365  match v return (λn.λv. Vector A (n + m)) with
366    [ VEmpty ⇒ (? q)
367    | VCons o hd tl ⇒ hd ::: (append A o m tl q)
368    ].
369    # H
370    assumption
371qed.
372   
373notation "hvbox(l break @@ r)"
374  right associative with precedence 47
375  for @{ 'vappend $l $r }.
376   
377interpretation "Vector append" 'vappend v1 v2 = (append ??? v1 v2).
378
379lemma vector_append_zero:
380  ∀A,m.
381  ∀v: Vector A m.
382  ∀q: Vector A 0.
383    v = q@@v.
384  #A #m #v #q
385  >(Vector_O A q) %
386qed.
387
388lemma vector_cons_empty:
389  ∀A: Type[0].
390  ∀n: nat.
391  ∀v: Vector A n.
392    [[ ]] @@ v = v.
393  #A #n #v
394  cases v try %
395  #n' #hd #tl %
396qed.
397
398lemma vector_cons_append:
399  ∀A: Type[0].
400  ∀n: nat.
401  ∀e: A.
402  ∀v: Vector A n.
403    e ::: v = [[ e ]] @@ v.
404  #A #n #e #v
405  cases v try %
406  #n' #hd #tl %
407qed.
408
409lemma vector_cons_append2:
410  ∀A: Type[0].
411  ∀n, m: nat.
412  ∀v: Vector A n.
413  ∀q: Vector A m.
414  ∀hd: A.
415    hd:::(v@@q) = (hd:::v)@@q.
416  #A #n #m #v #q
417  elim v try (#hd %)
418  #n' #hd' #tl' #ih #hd'
419  <ih %
420qed.
421
422lemma vector_associative_append:
423  ∀A: Type[0].
424  ∀n, m, o:  nat.
425  ∀v: Vector A n.
426  ∀q: Vector A m.
427  ∀r: Vector A o.
428    (v @@ q) @@ r ≃ v @@ (q @@ r).
429  #A #n #m #o #v #q #r
430  elim v try %
431  #n' #hd #tl #ih
432  <(vector_cons_append2 A … hd)
433  @jmeq_cons_vector_monotone
434  try assumption
435  @associative_plus
436qed.
437
438lemma tail_head:
439  ∀a: Type[0].
440  ∀m, n: nat.
441  ∀hd: a.
442  ∀l: Vector a m.
443  ∀r: Vector a n.
444    tail a ? (hd:::(l@@r)) = l@@r.
445  #a #m #n #hd #l #r
446  cases l try %
447  #m' #hd' #tl' %
448qed.
449
450lemma head_head':
451  ∀a: Type[0].
452  ∀m: nat.
453  ∀hd: a.
454  ∀l: Vector a m.
455    hd = head' … (hd:::l).
456  #a #m #hd #l cases l try %
457  #m' #hd' #tl %
458qed.
459
460axiom vsplit_elim':
461  ∀A: Type[0].
462  ∀B: Type[1].
463  ∀l, m, v.
464  ∀T: Vector A l → Vector A m → B.
465  ∀P: B → Prop.
466    (∀lft, rgt. v = lft @@ rgt → P (T lft rgt)) →
467      P (let 〈lft, rgt〉 ≝ vsplit A l m v in T lft rgt).
468
469axiom vsplit_elim'':
470  ∀A: Type[0].
471  ∀B,B': Type[1].
472  ∀l, m, v.
473  ∀T: Vector A l → Vector A m → B.
474  ∀T': Vector A l → Vector A m → B'.
475  ∀P: B → B' → Prop.
476    (∀lft, rgt. v = lft @@ rgt → P (T lft rgt) (T' lft rgt)) →
477      P (let 〈lft, rgt〉 ≝ vsplit A l m v in T lft rgt)
478        (let 〈lft, rgt〉 ≝ vsplit A l m v in T' lft rgt).
479
480lemma vsplit_succ:
481  ∀A: Type[0].
482  ∀m, n: nat.
483  ∀l: Vector A m.
484  ∀r: Vector A n.
485  ∀v: Vector A (m + n).
486  ∀hd: A.
487    v = l@@r → (〈l, r〉 = vsplit A m n v → 〈hd:::l, r〉 = vsplit A (S m) n (hd:::v)).
488  #A #m
489  elim m
490  [1:
491    #n #l #r #v #hd #eq #hyp
492    destruct >(Vector_O … l) %
493  |2:
494    #m' #inductive_hypothesis #n #l #r #v #hd #equal #hyp
495    destruct
496    cases (Vector_Sn … l) #hd' #tl'
497    whd in ⊢ (???%);
498    >tail_head
499    <(? : vsplit A (S m') n (l@@r) = vsplit' A (S m') n (l@@r))
500    try (<hyp <head_head' %)
501    elim l normalize //
502  ]
503qed.
504
505corollary prod_vector_zero_eq_left:
506  ∀A, n.
507  ∀q: Vector A O.
508  ∀r: Vector A n.
509    〈q, r〉 = 〈[[ ]], r〉.
510  #A #n #q #r
511  generalize in match (Vector_O A q …);
512  #hyp destruct %
513qed.
514
515lemma vsplit_prod:
516  ∀A: Type[0].
517  ∀m, n: nat.
518  ∀p: Vector A (m + n).
519  ∀v: Vector A m.
520  ∀q: Vector A n.
521    p = v@@q → 〈v, q〉 = vsplit A m n p.
522  #A #m elim m
523  [1:
524    #n #p #v #q #hyp
525    >hyp <(vector_append_zero A n q v)
526    >(prod_vector_zero_eq_left A …)
527    @vsplit_zero
528  |2:
529    #r #ih #n #p #v #q #hyp
530    >hyp
531    cases (Vector_Sn A r v) #hd #exists
532    cases exists #tl #jmeq
533    >jmeq @vsplit_succ try %
534    @ih %
535  ]
536qed.
537
538definition vsplit_elim:
539  ∀A: Type[0].
540  ∀l, m: nat.
541  ∀v: Vector A (l + m).
542  ∀P: (Vector A l) × (Vector A m) → Prop.
543    (∀vl: Vector A l.
544     ∀vm: Vector A m.
545      v = vl@@vm → P 〈vl,vm〉) → P (vsplit A l m v) ≝
546  λa: Type[0].
547  λl, m: nat.
548  λv: Vector a (l + m).
549  λP. ?.
550  cases daemon
551qed.
552
553axiom vsplit_append:
554  ∀A: Type[0].
555  ∀m, n: nat.
556  ∀v, v': Vector A m.
557  ∀q, q': Vector A n.
558    let 〈v', q'〉 ≝ vsplit A m n (v@@q) in
559      v = v' ∧ q = q'.
560
561lemma vsplit_vector_singleton:
562  ∀A: Type[0].
563  ∀n: nat.
564  ∀v: Vector A (S n).
565  ∀rest: Vector A n.
566  ∀s: Vector A 1.
567    v = s @@ rest →
568    ((get_index_v A ? v 0 ?) ::: rest) = v.
569  [1:
570    #A #n #v cases daemon (* XXX: !!! *)
571  |2:
572    @le_S_S @le_O_n
573  ]
574qed.
575
576let rec scan_left (A: Type[0]) (B: Type[0]) (n: nat)
577                   (f: A → B → A) (a: A) (v: Vector B n) on v ≝
578  a :::
579    (match v with
580       [ VEmpty ⇒ VEmpty A
581       | VCons o hd tl ⇒ scan_left A B o f (f a hd) tl
582       ]).
583
584let rec scan_right (A: Type[0]) (B: Type[0]) (n: nat)
585                    (f: A → B → A) (b: B) (v: Vector A n) on v ≝
586  match v with
587    [ VEmpty ⇒ ?
588    | VCons o hd tl ⇒ f hd b :: (scan_right A B o f b tl)
589    ].
590    //
591qed.
592   
593(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
594(* Other manipulations.                                                       *)
595(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
596
597(* At some points matita will attempt to reduce reverse with a known vector,
598   which reduces the equality proof for the cast.  Normalising this proof needs
599   to be fast enough to keep matita usable, so use plus_n_Sm_fast. *)
600
601let rec revapp (A: Type[0]) (n: nat) (m:nat)
602                (v: Vector A n) (acc: Vector A m) on v : Vector A (n + m) ≝
603  match v return λn'.λ_. Vector A (n' + m) with
604    [ VEmpty ⇒ acc
605    | VCons o hd tl ⇒ (revapp ??? tl (hd:::acc))⌈Vector A (o+S m) ↦ Vector A (S o + m)⌉
606    ].
607< plus_n_Sm_fast @refl qed.
608
609let rec reverse (A: Type[0]) (n: nat) (v: Vector A n) on v : Vector A n ≝
610  (revapp A n 0 v [[ ]])⌈Vector A (n+0) ↦ Vector A n⌉.
611< plus_n_O @refl qed.
612
613let rec pad_vector (A:Type[0]) (a:A) (n,m:nat) (v:Vector A m) on n : Vector A (n+m) ≝
614match n return λn.Vector A (n+m) with
615[ O ⇒ v
616| S n' ⇒ a:::(pad_vector A a n' m v)
617].
618
619(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
620(* Conversions to and from lists.                                             *)
621(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
622
623let rec list_of_vector (A: Type[0]) (n: nat)
624                        (v: Vector A n) on v ≝
625  match v return λn.λv. list A with
626    [ VEmpty ⇒ []
627    | VCons o hd tl ⇒ hd :: (list_of_vector A o tl)
628    ].
629
630let rec vector_of_list (A: Type[0]) (l: list A) on l ≝
631  match l return λl. Vector A (length A l) with
632    [ nil ⇒ ?
633    | cons hd tl ⇒ hd ::: (vector_of_list A tl)
634    ].
635    normalize
636    @ VEmpty
637qed.
638
639(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)   
640(* Rotates and shifts.                                                        *)
641(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
642   
643let rec rotate_left (A: Type[0]) (n: nat)
644                     (m: nat) (v: Vector A n) on m: Vector A n ≝
645  match m with
646    [ O ⇒ v
647    | S o ⇒
648        match v with
649          [ VEmpty ⇒ [[ ]]
650          | VCons p hd tl ⇒
651             rotate_left A (S p) o ((append A p ? tl [[hd]])⌈Vector A (p + S O) ↦ Vector A (S p)⌉)
652          ]
653    ].
654  /2/
655qed.
656
657definition rotate_right ≝
658  λA: Type[0].
659  λn, m: nat.
660  λv: Vector A n.
661    reverse A n (rotate_left A n m (reverse A n v)).
662
663definition shift_left_1 ≝
664  λA: Type[0].
665  λn: nat.
666  λv: Vector A (S n).
667  λa: A.
668   match v return λy.λ_. y = S n → Vector A y with
669     [ VEmpty ⇒ λH.⊥
670     | VCons o hd tl ⇒ λH.reverse … (a::: reverse … tl)
671     ] (refl ? (S n)).
672 destruct.
673qed.
674
675
676(* XXX this is horrible - but useful to ensure that we can normalise in the proof assistant. *)
677definition switch_bv_plus : ∀A:Type[0]. ∀n,m. Vector A (n+m) → Vector A (m+n) ≝
678λA,n,m. match commutative_plus_faster n m return λx.λ_.Vector A (n+m) → Vector A x with [ refl ⇒ λi.i ].
679
680definition shift_right_1 ≝
681  λA: Type[0].
682  λn: nat.
683  λv: Vector A (S n).
684  λa: A.
685    let 〈v',dropped〉 ≝ vsplit ? n 1 (switch_bv_plus ? 1 n v) in a:::v'.
686(*    reverse … (shift_left_1 … (reverse … v) a).*)
687
688definition shift_left : ∀A:Type[0]. ∀n,m:nat. Vector A n → A → Vector A n ≝
689  λA: Type[0].
690  λn, m: nat.
691    match nat_compare n m return λx,y.λ_. Vector A x → A → Vector A x with
692    [ nat_lt _ _ ⇒ λv,a. replicate … a
693    | nat_eq _   ⇒ λv,a. replicate … a
694    | nat_gt d m ⇒ λv,a. let 〈v0,v'〉 ≝ vsplit … v in switch_bv_plus … (v' @@ (replicate … a))
695    ].
696
697(*    iterate … (λx. shift_left_1 … x a) v m.*)
698   
699definition shift_right ≝
700  λA: Type[0].
701  λn, m: nat.
702  λv: Vector A (S n).
703  λa: A.
704    iterate … (λx. shift_right_1 … x a) v m.
705
706(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
707(* Decidable equality.                                                        *)
708(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
709
710let rec eq_v (A: Type[0]) (n: nat) (f: A → A → bool) (b: Vector A n) (c: Vector A n) on b : bool ≝
711  (match b return λx.λ_. Vector A x → bool with
712   [ VEmpty ⇒ λc.
713       match c return λx.λ_. match x return λ_.Type[0] with [ O ⇒ bool | _ ⇒ True ] with
714       [ VEmpty ⇒ true
715       | VCons p hd tl ⇒ I
716       ]
717   | VCons m hd tl ⇒ λc. andb (f hd (head' A m c)) (eq_v A m f tl (tail A m c))
718   ]
719  ) c.
720
721lemma vector_inv_n: ∀A,n. ∀P:Vector A n → Type[0]. ∀v:Vector A n.
722  match n return λn'. (Vector A n' → Type[0]) → Vector A n' → Type[0] with
723  [ O ⇒ λP.λv.P [[ ]] → P v
724  | S m ⇒ λP.λv.(∀h,t. P (VCons A m h t)) → P v
725  ] P v.
726#A #n #P #v lapply P cases v normalize //
727qed.
728
729lemma eq_v_elim: ∀P:bool → Type[0]. ∀A,f.
730  (∀Q:bool → Type[0]. ∀a,b. (a = b → Q true) → (a ≠ b → Q false) → Q (f a b)) →
731  ∀n,x,y.
732  (x = y → P true) →
733  (x ≠ y → P false) →
734  P (eq_v A n f x y).
735#P #A #f #f_elim #n #x elim x
736[ #y @(vector_inv_n … y)
737  normalize /2/
738| #m #h #t #IH #y @(vector_inv_n … y)
739  #h' #t' #Ht #Hf whd in ⊢ (?%);
740  @(f_elim ? h h') #Eh
741  [ @IH [ #Et @Ht >Eh >Et @refl | #NEt @Hf % #E' destruct (E') elim NEt /2/ ]
742  | @Hf % #E' destruct (E') elim Eh /2/
743  ]
744] qed.
745
746lemma eq_v_true : ∀A,f. (∀a. f a a = true) → ∀n,v. eq_v A n f v v = true.
747#A #f #f_true #n #v elim v
748[ //
749| #m #h #t #IH whd in ⊢ (??%%); >f_true >IH @refl
750] qed.
751
752lemma vector_neq_tail : ∀A,n,h. ∀t,t':Vector A n. h:::t≠h:::t' → t ≠ t'.
753#A #n #h #t #t' * #NE % #E @NE >E @refl
754qed.
755
756lemma  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.
757#A #f #f_true #n elim n
758[ #v #v' @(vector_inv_n ??? v) @(vector_inv_n ??? v') * #H @False_ind @H @refl
759| #m #IH #v #v' @(vector_inv_n ??? v) #h #t @(vector_inv_n ??? v') #h' #t'
760  #NE normalize lapply (f_true h h') cases (f h h') // #E @IH >E in NE; /2/
761] qed.
762
763(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
764(* Subvectors.                                                                *)
765(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
766
767definition mem ≝
768 λA: Type[0].
769 λeq_a : A → A → bool.
770 λn: nat.
771 λl: Vector A n.
772 λx: A.
773  fold_right … (λy,v. (eq_a x y) ∨ v) false l.
774
775lemma 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.
776 #A #eq_a #refl #n #m #v elim v
777 [ #w #x whd whd in match (mem ?????); >refl //
778 | /2/
779 ]
780qed.
781
782lemma mem_monotonic_wrt_append:
783  ∀A: Type[0].
784  ∀m, o: nat.
785  ∀eq: A → A → bool.
786  ∀reflex: ∀a. eq a a = true.
787  ∀p: Vector A m.
788  ∀a: A.
789  ∀r: Vector A o.
790    mem A eq ? r a = true → mem A eq ? (p @@ r) a = true.
791  #A #m #o #eq #reflex #p #a
792  elim p try (#r #assm assumption)
793  #m' #hd #tl #inductive_hypothesis #r #assm
794  normalize
795  cases (eq ??) try %
796  @inductive_hypothesis assumption
797qed.
798
799
800let rec subvector_with
801  (a: Type[0]) (n: nat) (m: nat) (eq: a → a → bool) (sub: Vector a n) (sup: Vector a m)
802    on sub: bool ≝
803  match sub with
804  [ VEmpty         ⇒ true
805  | VCons n' hd tl ⇒
806    if mem … eq … sup hd then
807      subvector_with … eq tl sup
808    else
809      false
810  ].
811
812lemma subvector_with_refl0:
813 ∀A:Type[0]. ∀n. ∀eq: A → A → bool. (∀a. eq a a = true) → ∀v: Vector A n.
814  ∀m. ∀w: Vector A m. subvector_with A … eq v (w@@v).
815 #A #n #eq #refl #v elim v
816 [ //
817 | #m #hd #tl #IH #m #w whd in match (subvector_with ??????); >mem_append //
818   change with (bool_to_Prop (subvector_with ??????)) lapply (IH … (w@@[[hd]]))
819  lapply (vector_associative_append ???? w [[hd]] tl) #EQ
820  @(dependent_rewrite_vectors … EQ) //
821 ]
822qed.
823
824lemma subvector_with_refl:
825 ∀A:Type[0]. ∀n. ∀eq: A → A → bool. (∀a. eq a a = true) → ∀v: Vector A n.
826  subvector_with A … eq v v.
827 #A #n #eq #refl #v @(subvector_with_refl0 … v … [[]]) //
828qed.
829
830lemma subvector_multiple_append:
831  ∀A: Type[0].
832  ∀o, n: nat.
833  ∀eq: A → A → bool.
834  ∀refl: ∀a. eq a a = true.
835  ∀h: Vector A o.
836  ∀v: Vector A n.
837  ∀m: nat.
838  ∀q: Vector A m.
839    bool_to_Prop (subvector_with A ? ? eq v (h @@ q @@ v)).
840  #A #o #n #eq #reflex #h #v
841  elim v try (normalize #m #irrelevant @I)
842  #m' #hd #tl #inductive_hypothesis #m #q
843  change with (bool_to_Prop (andb ??))
844  cut ((mem A eq (o + (m + S m')) (h@@q@@hd:::tl) hd) = true)
845  [1:
846    @mem_monotonic_wrt_append try assumption
847    @mem_monotonic_wrt_append try assumption
848    normalize >reflex %
849  |2:
850    #assm >assm
851    >vector_cons_append
852    change with (bool_to_Prop (subvector_with ??????))
853    @(dependent_rewrite_vectors … (vector_associative_append … q [[hd]] tl))
854    try @associative_plus
855    @inductive_hypothesis
856  ]
857qed.
858
859
860
861(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
862(* Lemmas.                                                                    *)
863(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)   
864   
865lemma map_fusion:
866  ∀A, B, C: Type[0].
867  ∀n: nat.
868  ∀v: Vector A n.
869  ∀f: A → B.
870  ∀g: B → C.
871    map B C n g (map A B n f v) = map A C n (λx. g (f x)) v.
872  #A #B #C #n #v #f #g
873  elim v
874  [ normalize
875    %
876  | #N #H #V #H2
877    normalize
878    > H2
879    %
880  ]
881qed.
Note: See TracBrowser for help on using the repository browser.