source: src/ASM/Vector.ma @ 2276

Last change on this file since 2276 was 2124, checked in by sacerdot, 7 years ago

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