source: src/ASM/Vector.ma @ 2593

Last change on this file since 2593 was 2286, checked in by tranquil, 8 years ago

Big update!

  • merge of all _paolo variants
  • reorganised some depends (in particular, Register and thus back-end laguages no longer have fake ASM dependency)
  • split I8051.ma spawning new BackEndOps?.ma

compiler.ma broken at the moment, but not by these changes as far as I can tell
File size: 34.9 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
96lemma Vector_singl_elim : ∀A.∀P : Vector A 1 → Prop.∀v.
97  (∀a.v = [[ a ]] → P [[ a ]]) → P v.
98#A #P #v
99elim (Vector_Sn … v) #a * #tl >(Vector_O … tl) #EQ >EQ #H @H % qed.
100
101lemma Vector_pair_elim : ∀A.∀P : Vector A 2 → Prop.∀v.
102  (∀a,b.v = [[ a ; b ]] → P [[ a ; b ]]) → P v.
103#A #P #v
104elim (Vector_Sn … v) #a * #tl @(Vector_singl_elim … tl) #b #EQ1 #EQ2 destruct
105#H @H %
106qed.
107
108lemma Vector_triple_elim : ∀A.∀P : Vector A 3 → Prop.∀v.
109  (∀a,b,c.v = [[ a ; b ; c ]] → P [[ a ; b ; c ]]) → P v.
110#A #P #v
111elim (Vector_Sn … v) #a * #tl @(Vector_pair_elim … tl) #b #c #EQ1 #EQ2 destruct
112#H @H %
113qed.
114
115(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
116(* Lookup.                                                                    *)
117(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
118
119let rec get_index_v (A: Type[0]) (n: nat)
120                   (v: Vector A n) (m: nat) (lt: m < n) on m: A ≝
121  (match m with
122    [ O ⇒
123      match v return λx.λ_. O < x → A with
124        [ VEmpty ⇒ λabsd1: O < O. ?
125        | VCons p hd tl ⇒ λprf1: O < S p. hd
126        ]
127    | S o ⇒
128      (match v return λx.λ_. S o < x → A with
129        [ VEmpty ⇒ λprf: S o < O. ?
130        | VCons p hd tl ⇒ λprf: S o < S p. get_index_v A p tl o ?
131        ])
132    ]) lt.
133    [ cases (not_le_Sn_O O)
134      normalize in absd1;
135      # H
136      cases (H absd1)
137    | cases (not_le_Sn_O (S o))
138      normalize in prf;
139      # H
140      cases (H prf)
141    | normalize
142      normalize in prf;
143      @ le_S_S_to_le
144      assumption
145    ]
146qed.
147
148definition get_index' ≝
149  λA: Type[0].
150  λn, m: nat.
151  λb: Vector A (S (n + m)).
152    get_index_v A (S (n + m)) b n ?.
153  normalize
154  @le_S_S
155  cases m //
156qed.
157
158let rec get_index_weak_v (A: Type[0]) (n: nat)
159                         (v: Vector A n) (m: nat) on m ≝
160  match m with
161    [ O ⇒
162      match v with
163        [ VEmpty ⇒ None A
164        | VCons p hd tl ⇒ Some A hd
165        ]
166    | S o ⇒
167      match v with
168        [ VEmpty ⇒ None A
169        | VCons p hd tl ⇒ get_index_weak_v A p tl o
170        ]
171    ].
172   
173interpretation "Vector get_index" 'get_index_v v n = (get_index_v ? ? v n).
174
175let rec set_index (A: Type[0]) (n: nat) (v: Vector A n) (m: nat) (a: A) (lt: m < n) on m: Vector A n ≝
176  (match m with
177    [ O ⇒
178      match v return λx.λ_. O < x → Vector A x with
179        [ VEmpty ⇒ λabsd1: O < O. [[ ]]
180        | VCons p hd tl ⇒ λprf1: O < S p. (a ::: tl)
181        ]
182    | S o ⇒
183      (match v return λx.λ_. S o < x → Vector A x with
184        [ VEmpty ⇒ λprf: S o < O. [[ ]]
185        | VCons p hd tl ⇒ λprf: S o < S p. hd ::: (set_index A p tl o a ?)
186        ])
187    ]) lt.
188    normalize in prf ⊢ %;
189    /2/;
190qed.
191
192let rec set_index_weak (A: Type[0]) (n: nat)
193                       (v: Vector A n) (m: nat) (a: A) on m ≝
194  match m with
195    [ O ⇒
196      match v with
197        [ VEmpty ⇒ None (Vector A n)
198        | VCons o hd tl ⇒ Some (Vector A n) (? (VCons A o a tl))
199        ]
200    | S o ⇒
201      match v with
202        [ VEmpty ⇒ None (Vector A n)
203        | VCons p hd tl ⇒
204            let settail ≝ set_index_weak A p tl o a in
205              match settail with
206                [ None ⇒ None (Vector A n)
207                | Some j ⇒ Some (Vector A n) (? (VCons A p hd j))
208                ]
209        ]
210    ].
211    //.
212qed.
213
214let rec drop (A: Type[0]) (n: nat)
215             (v: Vector A n) (m: nat) on m ≝
216  match m with
217    [ O ⇒ Some (Vector A n) v
218    | S o ⇒
219      match v with
220        [ VEmpty ⇒ None (Vector A n)
221        | VCons p hd tl ⇒ ? (drop A p tl o)
222        ]
223    ].
224    //.
225qed.
226
227definition head' : ∀A:Type[0]. ∀n:nat. Vector A (S n) → A ≝
228λA,n,v. match v return λx.λ_. match x with [ O ⇒ True | _ ⇒ A ] with
229[ VEmpty ⇒ I | VCons _ hd _ ⇒ hd ].
230
231definition tail : ∀A:Type[0]. ∀n:nat. Vector A (S n) → Vector A n ≝
232λA,n,v. match v return λx.λ_. match x with [ O ⇒ True | S m ⇒ Vector A m ] with
233[ VEmpty ⇒ I | VCons m hd tl ⇒ tl ].
234
235lemma tail_head' : ∀A,n,v.v = head' A n v ::: tail … v.
236#A #n #v elim (Vector_Sn … v) #hd * #tl #EQ >EQ % qed.
237
238let rec vsplit' (A: Type[0]) (m, n: nat) on m: Vector A (plus m n) → (Vector A m) × (Vector A n) ≝
239 match m return λm. Vector A (plus m n) → (Vector A m) × (Vector A n) with
240  [ O ⇒ λv. 〈[[ ]], v〉
241  | S m' ⇒ λv. let 〈l,r〉 ≝ vsplit' A m' n (tail ?? v) in 〈head' ?? v:::l, r〉
242  ].
243(* Prevent undesirable unfolding. *)
244let rec vsplit (A: Type[0]) (m, n: nat) (v:Vector A (plus m n)) on v : (Vector A m) × (Vector A n) ≝
245 vsplit' A m n v.
246
247lemma vsplit_zero:
248  ∀A,m.
249  ∀v: Vector A m.
250    〈[[]], v〉 = vsplit A 0 m v.
251  #A #m #v
252  cases v try %
253  #n #hd #tl %
254qed.
255
256definition head: ∀A: Type[0]. ∀n: nat. Vector A (S n) → A × (Vector A n) ≝
257  λA: Type[0].
258  λn: nat.
259  λv: Vector A (S n).
260  match v return λl. λ_: Vector A l. l = S n → A × (Vector A n) with
261  [ VEmpty ⇒ λK. ⊥
262  | VCons o he tl ⇒ λK. 〈he, (tl⌈Vector A o ↦ Vector A n⌉)〉
263  ] (? : S ? = S ?).
264  //
265  destruct
266qed.
267
268definition from_singl: ∀A:Type[0]. Vector A (S O) → A ≝
269 λA: Type[0].
270 λv: Vector A (S 0).
271   fst … (head … v).
272   
273(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
274(* Folds and builds.                                                          *)
275(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
276   
277let rec fold_right (A: Type[0]) (B: Type[0]) (n: nat)
278                    (f: A → B → B) (x: B) (v: Vector A n) on v ≝
279  match v with
280    [ VEmpty ⇒ x
281    | VCons n hd tl ⇒ f hd (fold_right A B n f x tl)
282    ].
283
284let rec fold_right_i (A: Type[0]) (B: nat → Type[0]) (n: nat)
285                     (f: ∀n. A → B n → B (S n)) (x: B 0) (v: Vector A n) on v ≝
286  match v with
287    [ VEmpty ⇒ x
288    | VCons n hd tl ⇒ f ? hd (fold_right_i A B n f x tl)
289    ].
290
291let rec fold_right2_i (A: Type[0]) (B: Type[0]) (C: nat → Type[0])
292                      (f: ∀N. A → B → C N → C (S N)) (c: C O) (n: nat)
293                      (v: Vector A n) (q: Vector B n) on v : C n ≝
294  (match v return λx.λ_. x = n → C n with
295    [ VEmpty ⇒
296      match q return λx.λ_. O = x → C x with
297        [ VEmpty ⇒ λprf: O = O. c
298        | VCons o hd tl ⇒ λabsd. ⊥
299        ]
300    | VCons o hd tl ⇒
301      match q return λx.λ_. S o = x → C x with
302        [ VEmpty ⇒ λabsd: S o = O. ⊥
303        | VCons p hd' tl' ⇒ λprf: S o = S p.
304           (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)⌉
305        ]
306    ]) (refl ? n).
307  [1,2:
308    destruct
309  |3,4:
310    lapply (injective_S … prf)
311    //
312  ]
313qed.
314 
315let rec fold_left (A: Type[0]) (B: Type[0]) (n: nat)
316                    (f: A → B → A) (x: A) (v: Vector B n) on v ≝
317  match v with
318    [ VEmpty ⇒ x
319    | VCons n hd tl ⇒ fold_left A B n f (f x hd) tl
320    ].
321   
322(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
323(* Maps and zips.                                                             *)
324(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
325
326let rec map (A: Type[0]) (B: Type[0]) (n: nat)
327             (f: A → B) (v: Vector A n) on v ≝
328  match v with
329    [ VEmpty ⇒ [[ ]]
330    | VCons n hd tl ⇒ (f hd) ::: (map A B n f tl)
331    ].
332
333let rec zip_with (A: Type[0]) (B: Type[0]) (C: Type[0]) (n: nat)
334             (f: A → B → C) (v: Vector A n) (q: Vector B n) on v ≝
335  (match v return (λx.λr. x = n → Vector C x) with
336    [ VEmpty ⇒ λ_. [[ ]]
337    | VCons n hd tl ⇒
338      match q return (λy.λr. S n = y → Vector C (S n)) with
339        [ VEmpty ⇒ ?
340        | VCons m hd' tl' ⇒
341            λe: S n = S m.
342              (f hd hd') ::: (zip_with A B C n f tl ?)
343        ]
344    ])
345    (refl ? n).
346  [ #e
347    destruct(e);
348  | lapply (injective_S … e)
349    # H
350    > H
351    @ tl'
352  ]
353qed.
354
355definition zip ≝
356  λA, B: Type[0].
357  λn: nat.
358  λv: Vector A n.
359  λq: Vector B n.
360    zip_with A B (A × B) n (mk_Prod A B) v q.
361
362(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
363(* Building vectors from scratch                                              *)
364(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
365
366let rec replicate (A: Type[0]) (n: nat) (h: A) on n ≝
367  match n return λn. Vector A n with
368    [ O ⇒ [[ ]]
369    | S m ⇒ h ::: (replicate A m h)
370    ].
371
372(* DPM: fixme.  Weird matita bug in base case. *)
373let rec append (A: Type[0]) (n: nat) (m: nat)
374                (v: Vector A n) (q: Vector A m) on v ≝
375  match v return (λn.λv. Vector A (n + m)) with
376    [ VEmpty ⇒ (? q)
377    | VCons o hd tl ⇒ hd ::: (append A o m tl q)
378    ].
379    # H
380    assumption
381qed.
382   
383notation "hvbox(l break @@ r)"
384  right associative with precedence 47
385  for @{ 'vappend $l $r }.
386   
387interpretation "Vector append" 'vappend v1 v2 = (append ??? v1 v2).
388
389
390lemma vsplit_ok:
391  ∀A: Type[0].
392  ∀m, n: nat.
393  ∀v: Vector A (m + n).
394  ∀upper: Vector A m.
395  ∀lower: Vector A n.
396    〈upper, lower〉 = vsplit A m n v →
397      upper @@ lower = v.
398  #A #m #n #v #upper #lower
399  cases daemon
400qed.
401
402lemma vector_append_zero:
403  ∀A,m.
404  ∀v: Vector A m.
405  ∀q: Vector A 0.
406    v = q@@v.
407  #A #m #v #q
408  >(Vector_O A q) %
409qed.
410
411lemma vector_cons_empty:
412  ∀A: Type[0].
413  ∀n: nat.
414  ∀v: Vector A n.
415    [[ ]] @@ v = v.
416  #A #n #v
417  cases v try %
418  #n' #hd #tl %
419qed.
420
421lemma vector_cons_append:
422  ∀A: Type[0].
423  ∀n: nat.
424  ∀e: A.
425  ∀v: Vector A n.
426    e ::: v = [[ e ]] @@ v.
427  #A #n #e #v
428  cases v try %
429  #n' #hd #tl %
430qed.
431
432lemma vector_cons_append2:
433  ∀A: Type[0].
434  ∀n, m: nat.
435  ∀v: Vector A n.
436  ∀q: Vector A m.
437  ∀hd: A.
438    hd:::(v@@q) = (hd:::v)@@q.
439  #A #n #m #v #q
440  elim v try (#hd %)
441  #n' #hd' #tl' #ih #hd'
442  <ih %
443qed.
444
445lemma vector_append_empty : ∀A,n.∀v : Vector A n.v @@ [[ ]] ≃ v.
446#A #n #v elim v -n [%]
447#n #hd #tl change with (?→?:::(?@@?)≃?)
448lapply (tl@@[[ ]])
449<plus_n_O #v #EQ >EQ %
450qed.
451
452lemma vector_associative_append:
453  ∀A: Type[0].
454  ∀n, m, o:  nat.
455  ∀v: Vector A n.
456  ∀q: Vector A m.
457  ∀r: Vector A o.
458    (v @@ q) @@ r ≃ v @@ (q @@ r).
459  #A #n #m #o #v #q #r
460  elim v try %
461  #n' #hd #tl #ih
462  <(vector_cons_append2 A … hd)
463  @jmeq_cons_vector_monotone
464  try assumption
465  @associative_plus
466qed.
467
468lemma tail_head:
469  ∀a: Type[0].
470  ∀m, n: nat.
471  ∀hd: a.
472  ∀l: Vector a m.
473  ∀r: Vector a n.
474    tail a ? (hd:::(l@@r)) = l@@r.
475  #a #m #n #hd #l #r
476  cases l try %
477  #m' #hd' #tl' %
478qed.
479
480lemma head_head':
481  ∀a: Type[0].
482  ∀m: nat.
483  ∀hd: a.
484  ∀l: Vector a m.
485    hd = head' … (hd:::l).
486  #a #m #hd #l cases l try %
487  #m' #hd' #tl %
488qed.
489
490axiom vsplit_elim':
491  ∀A: Type[0].
492  ∀B: Type[1].
493  ∀l, m, v.
494  ∀T: Vector A l → Vector A m → B.
495  ∀P: B → Prop.
496    (∀lft, rgt. v = lft @@ rgt → P (T lft rgt)) →
497      P (let 〈lft, rgt〉 ≝ vsplit A l m v in T lft rgt).
498
499axiom vsplit_elim'':
500  ∀A: Type[0].
501  ∀B,B': Type[1].
502  ∀l, m, v.
503  ∀T: Vector A l → Vector A m → B.
504  ∀T': Vector A l → Vector A m → B'.
505  ∀P: B → B' → Prop.
506    (∀lft, rgt. v = lft @@ rgt → P (T lft rgt) (T' lft rgt)) →
507      P (let 〈lft, rgt〉 ≝ vsplit A l m v in T lft rgt)
508        (let 〈lft, rgt〉 ≝ vsplit A l m v in T' lft rgt).
509
510lemma vsplit_succ:
511  ∀A: Type[0].
512  ∀m, n: nat.
513  ∀l: Vector A m.
514  ∀r: Vector A n.
515  ∀v: Vector A (m + n).
516  ∀hd: A.
517    v = l@@r → (〈l, r〉 = vsplit A m n v → 〈hd:::l, r〉 = vsplit A (S m) n (hd:::v)).
518  #A #m
519  elim m
520  [1:
521    #n #l #r #v #hd #eq #hyp
522    destruct >(Vector_O … l) %
523  |2:
524    #m' #inductive_hypothesis #n #l #r #v #hd #equal #hyp
525    destruct
526    cases (Vector_Sn … l) #hd' #tl'
527    whd in ⊢ (???%);
528    >tail_head
529    <(? : vsplit A (S m') n (l@@r) = vsplit' A (S m') n (l@@r))
530    try (<hyp <head_head' %)
531    elim l normalize //
532  ]
533qed.
534
535corollary prod_vector_zero_eq_left:
536  ∀A, n.
537  ∀q: Vector A O.
538  ∀r: Vector A n.
539    〈q, r〉 = 〈[[ ]], r〉.
540  #A #n #q #r
541  generalize in match (Vector_O A q …);
542  #hyp destruct %
543qed.
544
545lemma vsplit_prod:
546  ∀A: Type[0].
547  ∀m, n: nat.
548  ∀p: Vector A (m + n).
549  ∀v: Vector A m.
550  ∀q: Vector A n.
551    p = v@@q → 〈v, q〉 = vsplit A m n p.
552  #A #m elim m
553  [1:
554    #n #p #v #q #hyp
555    >hyp <(vector_append_zero A n q v)
556    >(prod_vector_zero_eq_left A …)
557    @vsplit_zero
558  |2:
559    #r #ih #n #p #v #q #hyp
560    >hyp
561    cases (Vector_Sn A r v) #hd #exists
562    cases exists #tl #jmeq
563    >jmeq @vsplit_succ try %
564    @ih %
565  ]
566qed.
567
568definition vsplit_elim:
569  ∀A: Type[0].
570  ∀l, m: nat.
571  ∀v: Vector A (l + m).
572  ∀P: (Vector A l) × (Vector A m) → Prop.
573    (∀vl: Vector A l.
574     ∀vm: Vector A m.
575      v = vl@@vm → P 〈vl,vm〉) → P (vsplit A l m v) ≝
576  λa: Type[0].
577  λl, m: nat.
578  λv: Vector a (l + m).
579  λP. ?.
580  cases daemon
581qed.
582
583axiom vsplit_append:
584  ∀A: Type[0].
585  ∀m, n: nat.
586  ∀v, v': Vector A m.
587  ∀q, q': Vector A n.
588    let 〈v', q'〉 ≝ vsplit A m n (v@@q) in
589      v = v' ∧ q = q'.
590
591lemma vsplit_vector_singleton:
592  ∀A: Type[0].
593  ∀n: nat.
594  ∀v: Vector A (S n).
595  ∀rest: Vector A n.
596  ∀s: Vector A 1.
597    v = s @@ rest →
598    ((get_index_v A ? v 0 ?) ::: rest) = v.
599  [1:
600    #A #n #v cases daemon (* XXX: !!! *)
601  |2:
602    @le_S_S @le_O_n
603  ]
604qed.
605
606let rec scan_left (A: Type[0]) (B: Type[0]) (n: nat)
607                   (f: A → B → A) (a: A) (v: Vector B n) on v ≝
608  a :::
609    (match v with
610       [ VEmpty ⇒ VEmpty A
611       | VCons o hd tl ⇒ scan_left A B o f (f a hd) tl
612       ]).
613
614let rec scan_right (A: Type[0]) (B: Type[0]) (n: nat)
615                    (f: A → B → A) (b: B) (v: Vector A n) on v ≝
616  match v with
617    [ VEmpty ⇒ ?
618    | VCons o hd tl ⇒ f hd b :: (scan_right A B o f b tl)
619    ].
620    //
621qed.
622
623lemma v_invert_append : ∀A,n,m.∀v,v' : Vector A n.∀u,u' : Vector A m.
624  v @@ u = v' @@ u' → v = v' ∧ u = u'.
625#A #n #m #v elim v -n
626[ #v' >(Vector_O ? v') #u #u' normalize #EQ %{EQ} %
627| #n #hd #tl #IH #v' elim (Vector_Sn ?? v') #hd' * #tl' #EQv' >EQv' -v'
628  #u #u' normalize #EQ destruct(EQ) elim (IH … e0) #EQ' #EQ'' %{EQ''}
629  >EQ' %
630]
631qed.
632
633(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
634(* Other manipulations.                                                       *)
635(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
636
637(* At some points matita will attempt to reduce reverse with a known vector,
638   which reduces the equality proof for the cast.  Normalising this proof needs
639   to be fast enough to keep matita usable, so use plus_n_Sm_fast. *)
640
641let rec revapp (A: Type[0]) (n: nat) (m:nat)
642                (v: Vector A n) (acc: Vector A m) on v : Vector A (n + m) ≝
643  match v return λn'.λ_. Vector A (n' + m) with
644    [ VEmpty ⇒ acc
645    | VCons o hd tl ⇒ (revapp ??? tl (hd:::acc))⌈Vector A (o+S m) ↦ Vector A (S o + m)⌉
646    ].
647< plus_n_Sm_fast @refl qed.
648
649let rec reverse (A: Type[0]) (n: nat) (v: Vector A n) on v : Vector A n ≝
650  (revapp A n 0 v [[ ]])⌈Vector A (n+0) ↦ Vector A n⌉.
651< plus_n_O @refl qed.
652
653let rec pad_vector (A:Type[0]) (a:A) (n,m:nat) (v:Vector A m) on n : Vector A (n+m) ≝
654match n return λn.Vector A (n+m) with
655[ O ⇒ v
656| S n' ⇒ a:::(pad_vector A a n' m v)
657].
658
659(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
660(* Conversions to and from lists.                                             *)
661(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
662
663let rec list_of_vector (A: Type[0]) (n: nat)
664                        (v: Vector A n) on v ≝
665  match v return λn.λv. list A with
666    [ VEmpty ⇒ []
667    | VCons o hd tl ⇒ hd :: (list_of_vector A o tl)
668    ].
669
670let rec vector_of_list (A: Type[0]) (l: list A) on l ≝
671  match l return λl. Vector A (length A l) with
672    [ nil ⇒ ?
673    | cons hd tl ⇒ hd ::: (vector_of_list A tl)
674    ].
675    normalize
676    @ VEmpty
677qed.
678
679(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)   
680(* Rotates and shifts.                                                        *)
681(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
682   
683let rec rotate_left (A: Type[0]) (n: nat)
684                     (m: nat) (v: Vector A n) on m: Vector A n ≝
685  match m with
686    [ O ⇒ v
687    | S o ⇒
688        match v with
689          [ VEmpty ⇒ [[ ]]
690          | VCons p hd tl ⇒
691             rotate_left A (S p) o ((append A p ? tl [[hd]])⌈Vector A (p + S O) ↦ Vector A (S p)⌉)
692          ]
693    ].
694  /2/
695qed.
696
697definition rotate_right ≝
698  λA: Type[0].
699  λn, m: nat.
700  λv: Vector A n.
701    reverse A n (rotate_left A n m (reverse A n v)).
702
703definition shift_left_1 ≝
704  λA: Type[0].
705  λn: nat.
706  λv: Vector A (S n).
707  λa: A.
708   match v return λy.λ_. y = S n → Vector A y with
709     [ VEmpty ⇒ λH.⊥
710     | VCons o hd tl ⇒ λH.reverse … (a::: reverse … tl)
711     ] (refl ? (S n)).
712 destruct.
713qed.
714
715
716(* XXX this is horrible - but useful to ensure that we can normalise in the proof assistant. *)
717definition switch_bv_plus : ∀A:Type[0]. ∀n,m. Vector A (n+m) → Vector A (m+n) ≝
718λA,n,m. match commutative_plus_faster n m return λx.λ_.Vector A (n+m) → Vector A x with [ refl ⇒ λi.i ].
719
720definition shift_right_1 ≝
721  λA: Type[0].
722  λn: nat.
723  λv: Vector A (S n).
724  λa: A.
725    let 〈v',dropped〉 ≝ vsplit ? n 1 (switch_bv_plus ? 1 n v) in a:::v'.
726(*    reverse … (shift_left_1 … (reverse … v) a).*)
727
728definition shift_left : ∀A:Type[0]. ∀n,m:nat. Vector A n → A → Vector A n ≝
729  λA: Type[0].
730  λn, m: nat.
731    match nat_compare n m return λx,y.λ_. Vector A x → A → Vector A x with
732    [ nat_lt _ _ ⇒ λv,a. replicate … a
733    | nat_eq _   ⇒ λv,a. replicate … a
734    | nat_gt d m ⇒ λv,a. let 〈v0,v'〉 ≝ vsplit … v in switch_bv_plus … (v' @@ (replicate … a))
735    ].
736
737(*    iterate … (λx. shift_left_1 … x a) v m.*)
738   
739definition shift_right ≝
740  λA: Type[0].
741  λn, m: nat.
742  λv: Vector A (S n).
743  λa: A.
744    iterate … (λx. shift_right_1 … x a) v m.
745
746(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
747(* Decidable equality.                                                        *)
748(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
749
750let rec eq_v (A: Type[0]) (n: nat) (f: A → A → bool) (b: Vector A n) (c: Vector A n) on b : bool ≝
751  (match b return λx.λ_. Vector A x → bool with
752   [ VEmpty ⇒ λc.
753       match c return λx.λ_. match x return λ_.Type[0] with [ O ⇒ bool | _ ⇒ True ] with
754       [ VEmpty ⇒ true
755       | VCons p hd tl ⇒ I
756       ]
757   | VCons m hd tl ⇒ λc. andb (f hd (head' A m c)) (eq_v A m f tl (tail A m c))
758   ]
759  ) c.
760
761lemma vector_inv_n: ∀A,n. ∀P:Vector A n → Type[0]. ∀v:Vector A n.
762  match n return λn'. (Vector A n' → Type[0]) → Vector A n' → Type[0] with
763  [ O ⇒ λP.λv.P [[ ]] → P v
764  | S m ⇒ λP.λv.(∀h,t. P (VCons A m h t)) → P v
765  ] P v.
766#A #n #P #v lapply P cases v normalize //
767qed.
768
769lemma eq_v_elim: ∀P:bool → Type[0]. ∀A,f.
770  (∀Q:bool → Type[0]. ∀a,b. (a = b → Q true) → (a ≠ b → Q false) → Q (f a b)) →
771  ∀n,x,y.
772  (x = y → P true) →
773  (x ≠ y → P false) →
774  P (eq_v A n f x y).
775#P #A #f #f_elim #n #x elim x
776[ #y @(vector_inv_n … y)
777  normalize /2/
778| #m #h #t #IH #y @(vector_inv_n … y)
779  #h' #t' #Ht #Hf whd in ⊢ (?%);
780  @(f_elim ? h h') #Eh
781  [ @IH [ #Et @Ht >Eh >Et @refl | #NEt @Hf % #E' destruct (E') elim NEt /2/ ]
782  | @Hf % #E' destruct (E') elim Eh /2/
783  ]
784] qed.
785
786lemma eq_v_true : ∀A,f. (∀a. f a a = true) → ∀n,v. eq_v A n f v v = true.
787#A #f #f_true #n #v elim v
788[ //
789| #m #h #t #IH whd in ⊢ (??%%); >f_true >IH @refl
790] qed.
791
792lemma vector_neq_tail : ∀A,n,h. ∀t,t':Vector A n. h:::t≠h:::t' → t ≠ t'.
793#A #n #h #t #t' * #NE % #E @NE >E @refl
794qed.
795
796lemma  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.
797#A #f #f_true #n elim n
798[ #v #v' @(vector_inv_n ??? v) @(vector_inv_n ??? v') * #H @False_ind @H @refl
799| #m #IH #v #v' @(vector_inv_n ??? v) #h #t @(vector_inv_n ??? v') #h' #t'
800  #NE normalize lapply (f_true h h') cases (f h h') // #E @IH >E in NE; /2/
801] qed.
802
803lemma eq_v_append : ∀A,n,m,test,v1,v2,u1,u2.
804  eq_v A (n+m) test (v1@@u1) (v2@@u2) =
805  (eq_v A n test v1 v2 ∧ eq_v A m test u1 u2).
806#A #n #m #test #v1 lapply m -m elim v1 -n
807[ #m #v2 >(Vector_O … v2) #u1 #u2 % ]
808#n #hd #tl #IH #m #v2
809elim (Vector_Sn … v2) #hd' * #tl' #EQ >EQ -v2
810#u1 #u2 whd in ⊢ (??%(?%?));
811whd in match (head' ???);
812whd in match (tail ???);
813whd in match (tail ???);
814elim (test ??) normalize nodelta [ @IH | % ]
815qed.
816
817(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
818(* Subvectors.                                                                *)
819(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
820
821definition mem ≝
822 λA: Type[0].
823 λeq_a : A → A → bool.
824 λn: nat.
825 λl: Vector A n.
826 λx: A.
827  fold_right … (λy,v. (eq_a x y) ∨ v) false l.
828
829lemma 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.
830 #A #eq_a #refl #n #m #v elim v
831 [ #w #x whd whd in match (mem ?????); >refl //
832 | /2/
833 ]
834qed.
835
836lemma mem_monotonic_wrt_append:
837  ∀A: Type[0].
838  ∀m, o: nat.
839  ∀eq: A → A → bool.
840  ∀reflex: ∀a. eq a a = true.
841  ∀p: Vector A m.
842  ∀a: A.
843  ∀r: Vector A o.
844    mem A eq ? r a = true → mem A eq ? (p @@ r) a = true.
845  #A #m #o #eq #reflex #p #a
846  elim p try (#r #assm assumption)
847  #m' #hd #tl #inductive_hypothesis #r #assm
848  normalize
849  cases (eq ??) try %
850  @inductive_hypothesis assumption
851qed.
852
853
854let rec subvector_with
855  (a: Type[0]) (n: nat) (m: nat) (eq: a → a → bool) (sub: Vector a n) (sup: Vector a m)
856    on sub: bool ≝
857  match sub with
858  [ VEmpty         ⇒ true
859  | VCons n' hd tl ⇒
860    if mem … eq … sup hd then
861      subvector_with … eq tl sup
862    else
863      false
864  ].
865
866lemma subvector_with_refl0:
867 ∀A:Type[0]. ∀n. ∀eq: A → A → bool. (∀a. eq a a = true) → ∀v: Vector A n.
868  ∀m. ∀w: Vector A m. subvector_with A … eq v (w@@v).
869 #A #n #eq #refl #v elim v
870 [ //
871 | #m #hd #tl #IH #m #w whd in match (subvector_with ??????); >mem_append //
872   change with (bool_to_Prop (subvector_with ??????)) lapply (IH … (w@@[[hd]]))
873  lapply (vector_associative_append ???? w [[hd]] tl) #EQ
874  @(dependent_rewrite_vectors … EQ) //
875 ]
876qed.
877
878lemma subvector_with_refl:
879 ∀A:Type[0]. ∀n. ∀eq: A → A → bool. (∀a. eq a a = true) → ∀v: Vector A n.
880  subvector_with A … eq v v.
881 #A #n #eq #refl #v @(subvector_with_refl0 … v … [[]]) //
882qed.
883
884lemma subvector_multiple_append:
885  ∀A: Type[0].
886  ∀o, n: nat.
887  ∀eq: A → A → bool.
888  ∀refl: ∀a. eq a a = true.
889  ∀h: Vector A o.
890  ∀v: Vector A n.
891  ∀m: nat.
892  ∀q: Vector A m.
893    bool_to_Prop (subvector_with A ? ? eq v (h @@ q @@ v)).
894  #A #o #n #eq #reflex #h #v
895  elim v try (normalize #m #irrelevant @I)
896  #m' #hd #tl #inductive_hypothesis #m #q
897  change with (bool_to_Prop (andb ??))
898  cut ((mem A eq (o + (m + S m')) (h@@q@@hd:::tl) hd) = true)
899  [1:
900    @mem_monotonic_wrt_append try assumption
901    @mem_monotonic_wrt_append try assumption
902    normalize >reflex %
903  |2:
904    #assm >assm
905    >vector_cons_append
906    change with (bool_to_Prop (subvector_with ??????))
907    @(dependent_rewrite_vectors … (vector_associative_append … q [[hd]] tl))
908    try @associative_plus
909    @inductive_hypothesis
910  ]
911qed.
912
913
914
915(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
916(* Lemmas.                                                                    *)
917(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)   
918   
919lemma map_fusion:
920  ∀A, B, C: Type[0].
921  ∀n: nat.
922  ∀v: Vector A n.
923  ∀f: A → B.
924  ∀g: B → C.
925    map B C n g (map A B n f v) = map A C n (λx. g (f x)) v.
926  #A #B #C #n #v #f #g
927  elim v
928  [ normalize
929    %
930  | #N #H #V #H2
931    normalize
932    > H2
933    %
934  ]
935qed.
936
937(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
938(* Vector prefix and suffix relations.                                        *)
939(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)   
940
941(* n.b.: if n = m this is equivalent to equality, without n and m needing to be
942   Leibniz-equal *)
943let rec vprefix A n m (test : A → A → bool) (v1 : Vector A n) (v2 : Vector A m) on v1 : bool ≝
944match v1 with
945[ VEmpty ⇒ true
946| VCons n' hd1 tl1 ⇒
947  match v2 with
948  [ VEmpty ⇒ false
949  | VCons m' hd2 tl2 ⇒ test hd1 hd2 ∧ vprefix … test tl1 tl2
950  ]
951].
952
953let rec vsuffix A n m test (v1 : Vector A n) (v2 : Vector A m) on v2 : bool ≝
954If leb (S n) m then with prf do
955  match v2 return λm.λv2:Vector A m.leb (S n) m → bool with
956  [ VEmpty ⇒ Ⓧ
957  | VCons m' hd2 tl2 ⇒ λ_.vsuffix ?? m' test v1 tl2
958  ] prf
959else (if eqb n m then
960  vprefix A n m test v1 v2
961else
962  false).
963
964include alias "arithmetics/nat.ma".
965
966lemma prefix_to_le : ∀A,n,m,test,v1,v2.
967  vprefix A n m test v1 v2 → n ≤ m.
968#A #n #m #test #v1 lapply m -m elim v1 -n [//]
969#n #hd #tl #IH #m * -m [*]
970#m #hd' #tl'
971whd in ⊢ (?%→?);
972elim (test ??) [2: *]
973whd in ⊢ (?%→?);
974#H @le_S_S @(IH … H)
975qed.
976
977lemma vprefix_ok : ∀A,n,m,test,v1,v2.
978  vprefix A n m test v1 v2 → le n m ∧
979  ∃pre.∃post : Vector A (m - n).v2 ≃ pre @@ post ∧
980            bool_to_Prop (eq_v … test v1 pre).
981#A #n #m #test #v1 #v2 #G %{(prefix_to_le … G)}
982lapply G lapply v2 lapply m -m elim v1 -n
983[ #m #v2 * <minus_n_O %{[[ ]]} %{v2} % % ]
984#n #hd1 #tl1 #IH #m * -m [*]
985#m #hd2 #tl2 whd in ⊢ (?%→?);
986elim (true_or_false_Prop (test hd1 hd2)) #H >H normalize nodelta [2: *]
987#G elim (IH … G) #pre * #post * #EQ #EQ'
988%{(hd2:::pre)} %{post} %
989[ change with (?≃hd2 ::: (? @@ ?)) lapply EQ lapply (pre @@ post)
990  <(minus_to_plus m … (prefix_to_le … G) (refl …))
991  #V #EQ'' >EQ'' %
992| whd in ⊢ (?%);
993  whd in match (head' ???); >H
994  @EQ'
995]
996qed.
997
998lemma vprefix_to_eq : ∀A,n,test,v1,v2.
999  vprefix A n n test v1 v2 = eq_v … test v1 v2.
1000#A #n #test #v1 elim v1 -n
1001[ #v2 >(Vector_O … v2) %
1002| #n #hd1 #tl1 #IH
1003  #v2 elim (Vector_Sn … v2) #hd2 * #tl2 #EQ destruct(EQ)
1004  normalize elim (test ??) [2: %]
1005  normalize @IH
1006]
1007qed.
1008
1009lemma vprefix_true : ∀A,n,m,test.∀v1,pre : Vector A n.∀post : Vector A m.
1010  eq_v … test v1 pre → bool_to_Prop (vprefix … test v1 (pre @@ post)).
1011#A #n #m #test #v1 lapply m -m elim v1 -n
1012[ #m #pre #post #_ %
1013| #n #hd #tl #IH #m #pre elim (Vector_Sn … pre) #hd' * #tl' #EQpre >EQpre
1014  #post
1015  whd in ⊢ (?%→?%); whd in match (head' ???);
1016  elim (test hd hd') [2: *] normalize nodelta whd in match (tail ???);
1017  @IH
1018]
1019qed.
1020
1021lemma vsuffix_to_le : ∀A,n,m,test,v1,v2.
1022  vsuffix A n m test v1 v2 → n ≤ m.
1023#A #n #m #test #v1 #v2 lapply v1 lapply n -n elim v2 -m
1024[ #n * -n
1025  [ * %
1026  | #n #hd #tl *
1027  ]
1028| #m #hd2 #tl2 #IH
1029  #n #v1 change with (bool_to_Prop (If ? then with prf do ? else ?) → ?)
1030  @If_elim normalize nodelta @leb_elim #H *
1031  [ #_ @(transitive_le … H) %2 %1
1032  | #ABS elim (ABS I)
1033  | #_ @eqb_elim #G normalize nodelta [2: *]
1034    destruct #_ %
1035  ]
1036]
1037qed.
1038 
1039lemma vsuffix_ok : ∀A,n,m,test,v1,v2.
1040  vsuffix A n m test v1 v2 → le n m ∧
1041  ∃pre : Vector A (m - n).∃post.v2 ≃ pre @@ post ∧
1042            bool_to_Prop (eq_v … test v1 post).
1043#A #n #m #test #v1 #v2 #G %{(vsuffix_to_le … G)}
1044lapply G lapply v1 lapply n -n
1045elim v2 -m
1046[ #n #v1
1047  whd in ⊢ (?%→?);
1048  @eqb_elim #EQ1 [2: *]
1049  normalize nodelta lapply v1 -v1 >EQ1 #v1
1050  >(Vector_O … v1) * %{[[ ]]} %{[[ ]]} % %
1051| #m #hd2 #tl2 #IH #n #v1
1052  change with (bool_to_Prop (If ? then with prf do ? else ?) → ?)
1053  @If_elim normalize nodelta #H
1054  [ #G elim (IH … G) #pre * #post * #EQ1 #EQ2
1055    >minus_Sn_m
1056    [ %{(hd2:::pre)} %{post} %{EQ2}
1057      change with (?≃?:::(?@@?))
1058      lapply EQ1 lapply (pre@@post)
1059      <plus_minus_m_m
1060      [ #v #EQ >EQ %]
1061    ]
1062    @(vsuffix_to_le … G)
1063  | @eqb_elim #EQn [2: *] normalize nodelta
1064    generalize in match (hd2:::tl2);
1065    <EQn in ⊢ (%→%→??(λ_.??(λ_.?(?%%??)?)));
1066    #v2' >vprefix_to_eq #G
1067    <EQn in ⊢ (?%(λ_:%.??(λ_.?(???%%)?)));
1068    <minus_n_n %{[[ ]]} %{v2'} %{G}
1069    %
1070  ]
1071]
1072qed.
1073
1074lemma vsuffix_true : ∀A,n,m,test.∀pre : Vector A n.∀v1,post : Vector A m.
1075  eq_v … test v1 post → bool_to_Prop (vsuffix … test v1 (pre @@ post)).
1076#A #n #m #test #pre lapply m -m elim pre -n
1077[ #m #v1 #post lapply v1 -v1 cases post -m
1078  [ #v1 >(Vector_O … v1) * %
1079  | #m #hd #tl #v1 #G
1080    change with (bool_to_Prop (If ? then with prf do ? else ?))
1081    @If_elim normalize nodelta
1082    [ @leb_elim #H * @⊥ @(absurd ? H ?) normalize // ]
1083    #_ >eqb_n_n normalize nodelta
1084    >vprefix_to_eq assumption
1085  ]
1086| #n #hd2 #tl2 #IH
1087  #m #v1 #post #G
1088  change with (bool_to_Prop (If ? then with prf do ? else ?))
1089  @If_elim normalize nodelta
1090  [ #H @IH @G
1091  | @leb_elim [ #_ * #ABS elim (ABS I) ]
1092    #H #_ @eqb_elim #K
1093    [ @⊥ @(absurd ? K) @lt_to_not_eq // ]
1094    normalize elim H -H #H @H normalize
1095    >plus_n_Sm_fast //
1096  ]
1097]
1098qed.
1099
1100(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
1101(* Vector flattening and recursive splitting.                                 *)
1102(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)   
1103
1104let rec rvsplit A n m on n : Vector A (n * m) → Vector (Vector A m) n ≝
1105match n return λn.Vector ? (n * m) → Vector (Vector ? m) n with
1106[ O ⇒ λ_.VEmpty ?
1107| S k ⇒
1108  λv.let 〈pre,post〉 ≝ vsplit … m (k*m) v in
1109  pre ::: rvsplit … post
1110].
1111
1112let rec vflatten A n m (v : Vector (Vector A m) n) on v : Vector A (n * m) ≝
1113match v return λn.λ_ : Vector ? n.Vector ? (n * m) with
1114[ VEmpty ⇒ VEmpty ?
1115| VCons n' hd tl ⇒ hd @@ vflatten ? n' m tl
1116].
1117
1118lemma vflatten_rvsplit : ∀A,n,m,v.vflatten A n m (rvsplit A n m v) = v.
1119#A #n elim n -n
1120[ #m #v >(Vector_O ? v) %
1121| #n #IH #m #v
1122  whd in match (rvsplit ????);
1123  @vsplit_elim #pre #post #EQ
1124  normalize nodelta
1125  whd in match (vflatten ????); >IH >EQ %
1126]
1127qed.
1128
1129lemma rvsplit_vflatten : ∀A,n,m,v.rvsplit A n m (vflatten A n m v) = v.
1130#A #n #m #v elim v -n
1131[ %
1132| #n #hd #tl #IH
1133  whd in match (vflatten ????);
1134  whd in match (rvsplit ????);
1135  @vsplit_elim #pre #post #EQ
1136  elim (v_invert_append … EQ) #EQ1 #EQ2 <EQ1 <EQ2
1137  normalize nodelta >IH %
1138]
1139qed.
1140
1141(* Paolo: should'nt it be in the standard library? *)
1142lemma sym_jmeq : ∀A,B.∀a : A.∀b : B.a≃b → b≃a.
1143#A #B #a #b * % qed.
1144
1145lemma vflatten_append : ∀A,n,m,p,v1,v2.
1146  vflatten A (n+m) p (v1 @@ v2) ≃ vflatten A n p v1 @@ vflatten A m p v2.
1147#A #n #m #p #v1 lapply m -m elim v1
1148[ #m #v2 %
1149| #n #hd1 #tl1 #IH #m #v2
1150  whd in ⊢ (??%?(????%?));
1151  lapply (IH … v2)
1152  lapply (vflatten … (tl1@@v2))
1153  cut ((n+m)*p = n*p + m*p)
1154  [ // ] #EQ whd in match (S n + m); whd in match (S ? * ?);
1155  whd in match (S n * ?); >EQ in ⊢ (%→?%%??→?%%??); -EQ
1156  #V #EQ >EQ -V @sym_jmeq @vector_associative_append
1157]
1158qed.
1159
1160lemma eq_v_vflatten : ∀A,n,m,test,v1,v2.
1161  eq_v A ? test (vflatten A n m v1) (vflatten A n m v2) =
1162  eq_v ?? (eq_v … test) v1 v2.
1163#A #n #m #test #v1 elim v1 -n
1164[ #v2 >(Vector_O … v2) % ]
1165#n #hd #tl #IH #v2
1166elim (Vector_Sn … v2) #hd' * #tl' #EQ >EQ -v2
1167whd in ⊢ (??(????%%)%);
1168whd in match (head' ???);
1169whd in match (tail ???);
1170>eq_v_append >IH %
1171qed.
1172
1173lemma vprefix_vflatten : ∀A,n,m,p,test.∀v1,v2.
1174  vprefix ? n m (eq_v ? p test) v1 v2 →
1175  bool_to_Prop (vprefix A (n*p) (m*p) test (vflatten … v1) (vflatten … v2)).
1176#A #n #m #p #test #v1 #v2 #G
1177elim (vprefix_ok … G) #le_nm
1178* #pre * #post *
1179lapply (vflatten_append … pre post)
1180lapply (pre @@ post)
1181<(minus_to_plus … le_nm (refl …)) in ⊢ (%→?%%??→???%%→?);
1182#v2' #EQ1 #EQ2 >EQ2 -v2 lapply EQ1 -EQ1
1183lapply (vflatten A m p v2')
1184cut (m*p = n*p + (m-n)*p)
1185[ <(commutative_times p) <(commutative_times p) <(commutative_times p)
1186  <distributive_times_plus <(minus_to_plus … le_nm (refl …)) % ]
1187#EQ >EQ #v2' #EQ' >EQ' -v2' -v2'
1188#G @vprefix_true
1189>eq_v_vflatten @G
1190qed.
1191
1192lemma vsuffix_vflatten : ∀A,n,m,p,test.∀v1,v2.
1193  vsuffix ? n m (eq_v ? p test) v1 v2 →
1194  bool_to_Prop (vsuffix A (n*p) (m*p) test (vflatten … v1) (vflatten … v2)).
1195#A #n #m #p #test #v1 #v2 #G
1196elim (vsuffix_ok … G) #le_nm * #pre * #post *
1197lapply (vflatten_append … pre post)
1198lapply (pre @@ post)
1199>commutative_plus in ⊢ (%→?%%??→???%%→?);
1200<(minus_to_plus … le_nm (refl …)) in ⊢ (%→?%%??→???%%→?);
1201#v2' #EQ1 #EQ2 >EQ2 -v2 lapply EQ1 -EQ1
1202lapply (vflatten A m p v2')
1203cut (m*p = (m-n)*p + n*p)
1204[ <(commutative_times p) <(commutative_times p) <(commutative_times p)
1205  <distributive_times_plus <commutative_plus <(minus_to_plus … le_nm (refl …)) % ]
1206#EQ >EQ #v2' #EQ' >EQ'
1207#G @vsuffix_true
1208>eq_v_vflatten @G
1209qed.
Note: See TracBrowser for help on using the repository browser.