source: src/ASM/Vector.ma @ 2090

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

!! BEWARE: major commit !!

1) [affects everybody]

split for vectors renamed to vsplit to reduce ambiguity since split is
now also a function in the standard library.
Note: I have not been able to propagate the changes everywhere in
the front-end/back-end because some files do not compile

2) [affects everybody]

functions on Vectors copied both in the front and back-ends moved to
Vectors.ma

3) [affects only the back-end]

subaddressing_mode_elim redesigned from scratch and now also applied to
Policy.ma. Moreover, all daemons about that have been closed.
The new one is much simpler to apply since it behaves like a standard
elimination principle: @(subaddressing_mode_elim \ldots x) where x is
the thing to eliminate.

File size: 19.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
24(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
25(* Syntax.                                                                    *)
26(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
27
28notation "hvbox(hd break ::: tl)"
29  right associative with precedence 57
30  for @{ 'vcons $hd $tl }.
31
32notation "[[ list0 x sep ; ]]"
33  non associative with precedence 90
34  for ${fold right @'vnil rec acc @{'vcons $x $acc}}.
35
36interpretation "Vector vnil" 'vnil = (VEmpty ?).
37interpretation "Vector vcons" 'vcons hd tl = (VCons ? ? hd tl).
38
39notation "hvbox(l break !!! break n)"
40  non associative with precedence 90
41  for @{ 'get_index_v $l $n }.
42
43lemma dependent_rewrite_vectors:
44  ∀A:Type[0].
45  ∀n, m: nat.
46  ∀v1: Vector A n.
47  ∀v2: Vector A m.
48  ∀P: ∀m. Vector A m → Prop.
49    n = m → v1 ≃ v2 → P n v1 → P m v2.
50  #A #n #m #v1 #v2 #P #eq #jmeq
51  destruct #assm assumption
52qed.
53
54lemma jmeq_cons_vector_monotone:
55  ∀A: Type[0].
56  ∀m, n: nat.
57  ∀v: Vector A m.
58  ∀q: Vector A n.
59  ∀prf: m = n.
60  ∀hd: A.
61    v ≃ q → hd:::v ≃ hd:::q.
62  #A #m #n #v #q #prf #hd #E
63  @(dependent_rewrite_vectors A … E)
64  try assumption %
65qed.
66
67(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
68(* Lookup.                                                                    *)
69(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
70
71let rec get_index_v (A: Type[0]) (n: nat)
72                   (v: Vector A n) (m: nat) (lt: m < n) on m: A ≝
73  (match m with
74    [ O ⇒
75      match v return λx.λ_. O < x → A with
76        [ VEmpty ⇒ λabsd1: O < O. ?
77        | VCons p hd tl ⇒ λprf1: O < S p. hd
78        ]
79    | S o ⇒
80      (match v return λx.λ_. S o < x → A with
81        [ VEmpty ⇒ λprf: S o < O. ?
82        | VCons p hd tl ⇒ λprf: S o < S p. get_index_v A p tl o ?
83        ])
84    ]) lt.
85    [ cases (not_le_Sn_O O)
86      normalize in absd1;
87      # H
88      cases (H absd1)
89    | cases (not_le_Sn_O (S o))
90      normalize in prf;
91      # H
92      cases (H prf)
93    | normalize
94      normalize in prf;
95      @ le_S_S_to_le
96      assumption
97    ]
98qed.
99
100definition get_index' ≝
101  λA: Type[0].
102  λn, m: nat.
103  λb: Vector A (S (n + m)).
104    get_index_v A (S (n + m)) b n ?.
105  normalize
106  @le_S_S
107  cases m //
108qed.
109
110let rec get_index_weak_v (A: Type[0]) (n: nat)
111                         (v: Vector A n) (m: nat) on m ≝
112  match m with
113    [ O ⇒
114      match v with
115        [ VEmpty ⇒ None A
116        | VCons p hd tl ⇒ Some A hd
117        ]
118    | S o ⇒
119      match v with
120        [ VEmpty ⇒ None A
121        | VCons p hd tl ⇒ get_index_weak_v A p tl o
122        ]
123    ].
124   
125interpretation "Vector get_index" 'get_index_v v n = (get_index_v ? ? v n).
126
127let rec set_index (A: Type[0]) (n: nat) (v: Vector A n) (m: nat) (a: A) (lt: m < n) on m: Vector A n ≝
128  (match m with
129    [ O ⇒
130      match v return λx.λ_. O < x → Vector A x with
131        [ VEmpty ⇒ λabsd1: O < O. [[ ]]
132        | VCons p hd tl ⇒ λprf1: O < S p. (a ::: tl)
133        ]
134    | S o ⇒
135      (match v return λx.λ_. S o < x → Vector A x with
136        [ VEmpty ⇒ λprf: S o < O. [[ ]]
137        | VCons p hd tl ⇒ λprf: S o < S p. hd ::: (set_index A p tl o a ?)
138        ])
139    ]) lt.
140    normalize in prf ⊢ %;
141    /2/;
142qed.
143
144let rec set_index_weak (A: Type[0]) (n: nat)
145                       (v: Vector A n) (m: nat) (a: A) on m ≝
146  match m with
147    [ O ⇒
148      match v with
149        [ VEmpty ⇒ None (Vector A n)
150        | VCons o hd tl ⇒ Some (Vector A n) (? (VCons A o a tl))
151        ]
152    | S o ⇒
153      match v with
154        [ VEmpty ⇒ None (Vector A n)
155        | VCons p hd tl ⇒
156            let settail ≝ set_index_weak A p tl o a in
157              match settail with
158                [ None ⇒ None (Vector A n)
159                | Some j ⇒ Some (Vector A n) (? (VCons A p hd j))
160                ]
161        ]
162    ].
163    //.
164qed.
165
166let rec drop (A: Type[0]) (n: nat)
167             (v: Vector A n) (m: nat) on m ≝
168  match m with
169    [ O ⇒ Some (Vector A n) v
170    | S o ⇒
171      match v with
172        [ VEmpty ⇒ None (Vector A n)
173        | VCons p hd tl ⇒ ? (drop A p tl o)
174        ]
175    ].
176    //.
177qed.
178
179definition head' : ∀A:Type[0]. ∀n:nat. Vector A (S n) → A ≝
180λA,n,v. match v return λx.λ_. match x with [ O ⇒ True | _ ⇒ A ] with
181[ VEmpty ⇒ I | VCons _ hd _ ⇒ hd ].
182
183definition tail : ∀A:Type[0]. ∀n:nat. Vector A (S n) → Vector A n ≝
184λA,n,v. match v return λx.λ_. match x with [ O ⇒ True | S m ⇒ Vector A m ] with
185[ VEmpty ⇒ I | VCons m hd tl ⇒ tl ].
186
187let rec vsplit' (A: Type[0]) (m, n: nat) on m: Vector A (plus m n) → (Vector A m) × (Vector A n) ≝
188 match m return λm. Vector A (plus m n) → (Vector A m) × (Vector A n) with
189  [ O ⇒ λv. 〈[[ ]], v〉
190  | S m' ⇒ λv. let 〈l,r〉 ≝ vsplit' A m' n (tail ?? v) in 〈head' ?? v:::l, r〉
191  ].
192(* Prevent undesirable unfolding. *)
193let rec vsplit (A: Type[0]) (m, n: nat) (v:Vector A (plus m n)) on v : (Vector A m) × (Vector A n) ≝
194 vsplit' A m n v.
195
196definition head: ∀A: Type[0]. ∀n: nat. Vector A (S n) → A × (Vector A n) ≝
197  λA: Type[0].
198  λn: nat.
199  λv: Vector A (S n).
200  match v return λl. λ_: Vector A l. l = S n → A × (Vector A n) with
201  [ VEmpty ⇒ λK. ⊥
202  | VCons o he tl ⇒ λK. 〈he, (tl⌈Vector A o ↦ Vector A n⌉)〉
203  ] (? : S ? = S ?).
204  //
205  destruct
206qed.
207
208definition from_singl: ∀A:Type[0]. Vector A (S O) → A ≝
209 λA: Type[0].
210 λv: Vector A (S 0).
211   fst … (head … v).
212   
213(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
214(* Folds and builds.                                                          *)
215(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
216   
217let rec fold_right (A: Type[0]) (B: Type[0]) (n: nat)
218                    (f: A → B → B) (x: B) (v: Vector A n) on v ≝
219  match v with
220    [ VEmpty ⇒ x
221    | VCons n hd tl ⇒ f hd (fold_right A B n f x tl)
222    ].
223
224let rec fold_right_i (A: Type[0]) (B: nat → Type[0]) (n: nat)
225                     (f: ∀n. A → B n → B (S n)) (x: B 0) (v: Vector A n) on v ≝
226  match v with
227    [ VEmpty ⇒ x
228    | VCons n hd tl ⇒ f ? hd (fold_right_i A B n f x tl)
229    ].
230
231let rec fold_right2_i (A: Type[0]) (B: Type[0]) (C: nat → Type[0])
232                      (f: ∀N. A → B → C N → C (S N)) (c: C O) (n: nat)
233                      (v: Vector A n) (q: Vector B n) on v : C n ≝
234  (match v return λx.λ_. x = n → C n with
235    [ VEmpty ⇒
236      match q return λx.λ_. O = x → C x with
237        [ VEmpty ⇒ λprf: O = O. c
238        | VCons o hd tl ⇒ λabsd. ⊥
239        ]
240    | VCons o hd tl ⇒
241      match q return λx.λ_. S o = x → C x with
242        [ VEmpty ⇒ λabsd: S o = O. ⊥
243        | VCons p hd' tl' ⇒ λprf: S o = S p.
244           (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)⌉
245        ]
246    ]) (refl ? n).
247  [1,2:
248    destruct
249  |3,4:
250    lapply (injective_S … prf)
251    //
252  ]
253qed.
254 
255let rec fold_left (A: Type[0]) (B: Type[0]) (n: nat)
256                    (f: A → B → A) (x: A) (v: Vector B n) on v ≝
257  match v with
258    [ VEmpty ⇒ x
259    | VCons n hd tl ⇒ fold_left A B n f (f x hd) tl
260    ].
261   
262(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
263(* Maps and zips.                                                             *)
264(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
265
266let rec map (A: Type[0]) (B: Type[0]) (n: nat)
267             (f: A → B) (v: Vector A n) on v ≝
268  match v with
269    [ VEmpty ⇒ [[ ]]
270    | VCons n hd tl ⇒ (f hd) ::: (map A B n f tl)
271    ].
272
273let rec zip_with (A: Type[0]) (B: Type[0]) (C: Type[0]) (n: nat)
274             (f: A → B → C) (v: Vector A n) (q: Vector B n) on v ≝
275  (match v return (λx.λr. x = n → Vector C x) with
276    [ VEmpty ⇒ λ_. [[ ]]
277    | VCons n hd tl ⇒
278      match q return (λy.λr. S n = y → Vector C (S n)) with
279        [ VEmpty ⇒ ?
280        | VCons m hd' tl' ⇒
281            λe: S n = S m.
282              (f hd hd') ::: (zip_with A B C n f tl ?)
283        ]
284    ])
285    (refl ? n).
286  [ #e
287    destruct(e);
288  | lapply (injective_S … e)
289    # H
290    > H
291    @ tl'
292  ]
293qed.
294
295definition zip ≝
296  λA, B: Type[0].
297  λn: nat.
298  λv: Vector A n.
299  λq: Vector B n.
300    zip_with A B (A × B) n (mk_Prod A B) v q.
301
302(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
303(* Building vectors from scratch                                              *)
304(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
305
306let rec replicate (A: Type[0]) (n: nat) (h: A) on n ≝
307  match n return λn. Vector A n with
308    [ O ⇒ [[ ]]
309    | S m ⇒ h ::: (replicate A m h)
310    ].
311
312(* DPM: fixme.  Weird matita bug in base case. *)
313let rec append (A: Type[0]) (n: nat) (m: nat)
314                (v: Vector A n) (q: Vector A m) on v ≝
315  match v return (λn.λv. Vector A (n + m)) with
316    [ VEmpty ⇒ (? q)
317    | VCons o hd tl ⇒ hd ::: (append A o m tl q)
318    ].
319    # H
320    assumption
321qed.
322   
323notation "hvbox(l break @@ r)"
324  right associative with precedence 47
325  for @{ 'vappend $l $r }.
326   
327interpretation "Vector append" 'vappend v1 v2 = (append ??? v1 v2).
328
329lemma vector_cons_append:
330  ∀A: Type[0].
331  ∀n: nat.
332  ∀e: A.
333  ∀v: Vector A n.
334    e ::: v = [[ e ]] @@ v.
335  #A #n #e #v
336  cases v try %
337  #n' #hd #tl %
338qed.
339
340lemma vector_cons_append2:
341  ∀A: Type[0].
342  ∀n, m: nat.
343  ∀v: Vector A n.
344  ∀q: Vector A m.
345  ∀hd: A.
346    hd:::(v@@q) = (hd:::v)@@q.
347  #A #n #m #v #q
348  elim v try (#hd %)
349  #n' #hd' #tl' #ih #hd'
350  <ih %
351qed.
352
353lemma vector_associative_append:
354  ∀A: Type[0].
355  ∀n, m, o:  nat.
356  ∀v: Vector A n.
357  ∀q: Vector A m.
358  ∀r: Vector A o.
359    (v @@ q) @@ r ≃ v @@ (q @@ r).
360  #A #n #m #o #v #q #r
361  elim v try %
362  #n' #hd #tl #ih
363  <(vector_cons_append2 A … hd)
364  @jmeq_cons_vector_monotone
365  try assumption
366  @associative_plus
367qed.
368
369axiom vsplit_elim':
370  ∀A: Type[0].
371  ∀B: Type[1].
372  ∀l, m, v.
373  ∀T: Vector A l → Vector A m → B.
374  ∀P: B → Prop.
375    (∀lft, rgt. v = lft @@ rgt → P (T lft rgt)) →
376      P (let 〈lft, rgt〉 ≝ vsplit A l m v in T lft rgt).
377
378axiom vsplit_elim'':
379  ∀A: Type[0].
380  ∀B,B': Type[1].
381  ∀l, m, v.
382  ∀T: Vector A l → Vector A m → B.
383  ∀T': Vector A l → Vector A m → B'.
384  ∀P: B → B' → Prop.
385    (∀lft, rgt. v = lft @@ rgt → P (T lft rgt) (T' lft rgt)) →
386      P (let 〈lft, rgt〉 ≝ vsplit A l m v in T lft rgt)
387        (let 〈lft, rgt〉 ≝ vsplit A l m v in T' lft rgt).
388   
389let rec scan_left (A: Type[0]) (B: Type[0]) (n: nat)
390                   (f: A → B → A) (a: A) (v: Vector B n) on v ≝
391  a :::
392    (match v with
393       [ VEmpty ⇒ VEmpty A
394       | VCons o hd tl ⇒ scan_left A B o f (f a hd) tl
395       ]).
396
397let rec scan_right (A: Type[0]) (B: Type[0]) (n: nat)
398                    (f: A → B → A) (b: B) (v: Vector A n) on v ≝
399  match v with
400    [ VEmpty ⇒ ?
401    | VCons o hd tl ⇒ f hd b :: (scan_right A B o f b tl)
402    ].
403    //
404qed.
405   
406(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
407(* Other manipulations.                                                       *)
408(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
409
410(* At some points matita will attempt to reduce reverse with a known vector,
411   which reduces the equality proof for the cast.  Normalising this proof needs
412   to be fast enough to keep matita usable, so use plus_n_Sm_fast. *)
413
414let rec revapp (A: Type[0]) (n: nat) (m:nat)
415                (v: Vector A n) (acc: Vector A m) on v : Vector A (n + m) ≝
416  match v return λn'.λ_. Vector A (n' + m) with
417    [ VEmpty ⇒ acc
418    | VCons o hd tl ⇒ (revapp ??? tl (hd:::acc))⌈Vector A (o+S m) ↦ Vector A (S o + m)⌉
419    ].
420< plus_n_Sm_fast @refl qed.
421
422let rec reverse (A: Type[0]) (n: nat) (v: Vector A n) on v : Vector A n ≝
423  (revapp A n 0 v [[ ]])⌈Vector A (n+0) ↦ Vector A n⌉.
424< plus_n_O @refl qed.
425
426let rec pad_vector (A:Type[0]) (a:A) (n,m:nat) (v:Vector A m) on n : Vector A (n+m) ≝
427match n return λn.Vector A (n+m) with
428[ O ⇒ v
429| S n' ⇒ a:::(pad_vector A a n' m v)
430].
431
432(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
433(* Conversions to and from lists.                                             *)
434(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
435
436let rec list_of_vector (A: Type[0]) (n: nat)
437                        (v: Vector A n) on v ≝
438  match v return λn.λv. list A with
439    [ VEmpty ⇒ []
440    | VCons o hd tl ⇒ hd :: (list_of_vector A o tl)
441    ].
442
443let rec vector_of_list (A: Type[0]) (l: list A) on l ≝
444  match l return λl. Vector A (length A l) with
445    [ nil ⇒ ?
446    | cons hd tl ⇒ hd ::: (vector_of_list A tl)
447    ].
448    normalize
449    @ VEmpty
450qed.
451
452(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)   
453(* Rotates and shifts.                                                        *)
454(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
455   
456let rec rotate_left (A: Type[0]) (n: nat)
457                     (m: nat) (v: Vector A n) on m: Vector A n ≝
458  match m with
459    [ O ⇒ v
460    | S o ⇒
461        match v with
462          [ VEmpty ⇒ [[ ]]
463          | VCons p hd tl ⇒
464             rotate_left A (S p) o ((append A p ? tl [[hd]])⌈Vector A (p + S O) ↦ Vector A (S p)⌉)
465          ]
466    ].
467  /2/
468qed.
469
470definition rotate_right ≝
471  λA: Type[0].
472  λn, m: nat.
473  λv: Vector A n.
474    reverse A n (rotate_left A n m (reverse A n v)).
475
476definition shift_left_1 ≝
477  λA: Type[0].
478  λn: nat.
479  λv: Vector A (S n).
480  λa: A.
481   match v return λy.λ_. y = S n → Vector A y with
482     [ VEmpty ⇒ λH.⊥
483     | VCons o hd tl ⇒ λH.reverse … (a::: reverse … tl)
484     ] (refl ? (S n)).
485 destruct.
486qed.
487
488
489(* XXX this is horrible - but useful to ensure that we can normalise in the proof assistant. *)
490definition switch_bv_plus : ∀A:Type[0]. ∀n,m. Vector A (n+m) → Vector A (m+n) ≝
491λA,n,m. match commutative_plus_faster n m return λx.λ_.Vector A (n+m) → Vector A x with [ refl ⇒ λi.i ].
492
493definition shift_right_1 ≝
494  λA: Type[0].
495  λn: nat.
496  λv: Vector A (S n).
497  λa: A.
498    let 〈v',dropped〉 ≝ vsplit ? n 1 (switch_bv_plus ? 1 n v) in a:::v'.
499(*    reverse … (shift_left_1 … (reverse … v) a).*)
500
501definition shift_left : ∀A:Type[0]. ∀n,m:nat. Vector A n → A → Vector A n ≝
502  λA: Type[0].
503  λn, m: nat.
504    match nat_compare n m return λx,y.λ_. Vector A x → A → Vector A x with
505    [ nat_lt _ _ ⇒ λv,a. replicate … a
506    | nat_eq _   ⇒ λv,a. replicate … a
507    | nat_gt d m ⇒ λv,a. let 〈v0,v'〉 ≝ vsplit … v in switch_bv_plus … (v' @@ (replicate … a))
508    ].
509
510(*    iterate … (λx. shift_left_1 … x a) v m.*)
511   
512definition shift_right ≝
513  λA: Type[0].
514  λn, m: nat.
515  λv: Vector A (S n).
516  λa: A.
517    iterate … (λx. shift_right_1 … x a) v m.
518
519(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
520(* Decidable equality.                                                        *)
521(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
522
523let rec eq_v (A: Type[0]) (n: nat) (f: A → A → bool) (b: Vector A n) (c: Vector A n) on b : bool ≝
524  (match b return λx.λ_. Vector A x → bool with
525   [ VEmpty ⇒ λc.
526       match c return λx.λ_. match x return λ_.Type[0] with [ O ⇒ bool | _ ⇒ True ] with
527       [ VEmpty ⇒ true
528       | VCons p hd tl ⇒ I
529       ]
530   | VCons m hd tl ⇒ λc. andb (f hd (head' A m c)) (eq_v A m f tl (tail A m c))
531   ]
532  ) c.
533
534lemma vector_inv_n: ∀A,n. ∀P:Vector A n → Type[0]. ∀v:Vector A n.
535  match n return λn'. (Vector A n' → Type[0]) → Vector A n' → Type[0] with
536  [ O ⇒ λP.λv.P [[ ]] → P v
537  | S m ⇒ λP.λv.(∀h,t. P (VCons A m h t)) → P v
538  ] P v.
539#A #n #P #v lapply P cases v normalize //
540qed.
541
542lemma eq_v_elim: ∀P:bool → Type[0]. ∀A,f.
543  (∀Q:bool → Type[0]. ∀a,b. (a = b → Q true) → (a ≠ b → Q false) → Q (f a b)) →
544  ∀n,x,y.
545  (x = y → P true) →
546  (x ≠ y → P false) →
547  P (eq_v A n f x y).
548#P #A #f #f_elim #n #x elim x
549[ #y @(vector_inv_n … y)
550  normalize /2/
551| #m #h #t #IH #y @(vector_inv_n … y)
552  #h' #t' #Ht #Hf whd in ⊢ (?%);
553  @(f_elim ? h h') #Eh
554  [ @IH [ #Et @Ht >Eh >Et @refl | #NEt @Hf % #E' destruct (E') elim NEt /2/ ]
555  | @Hf % #E' destruct (E') elim Eh /2/
556  ]
557] qed.
558
559lemma eq_v_true : ∀A,f. (∀a. f a a = true) → ∀n,v. eq_v A n f v v = true.
560#A #f #f_true #n #v elim v
561[ //
562| #m #h #t #IH whd in ⊢ (??%%); >f_true >IH @refl
563] qed.
564
565lemma vector_neq_tail : ∀A,n,h. ∀t,t':Vector A n. h:::t≠h:::t' → t ≠ t'.
566#A #n #h #t #t' * #NE % #E @NE >E @refl
567qed.
568
569lemma  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.
570#A #f #f_true #n elim n
571[ #v #v' @(vector_inv_n ??? v) @(vector_inv_n ??? v') * #H @False_ind @H @refl
572| #m #IH #v #v' @(vector_inv_n ??? v) #h #t @(vector_inv_n ??? v') #h' #t'
573  #NE normalize lapply (f_true h h') cases (f h h') // #E @IH >E in NE; /2/
574] qed.
575
576(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
577(* Subvectors.                                                                *)
578(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
579
580definition mem ≝
581 λA: Type[0].
582 λeq_a : A → A → bool.
583 λn: nat.
584 λl: Vector A n.
585 λx: A.
586  fold_right … (λy,v. (eq_a x y) ∨ v) false l.
587
588lemma 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.
589 #A #eq_a #refl #n #m #v elim v
590 [ #w #x whd whd in match (mem ?????); >refl //
591 | /2/
592 ]
593qed.
594
595let rec subvector_with
596  (a: Type[0]) (n: nat) (m: nat) (eq: a → a → bool) (sub: Vector a n) (sup: Vector a m)
597    on sub: bool ≝
598  match sub with
599  [ VEmpty         ⇒ true
600  | VCons n' hd tl ⇒
601    if mem … eq … sup hd then
602      subvector_with … eq tl sup
603    else
604      false
605  ].
606
607lemma subvector_with_refl0:
608 ∀A:Type[0]. ∀n. ∀eq: A → A → bool. (∀a. eq a a = true) → ∀v: Vector A n.
609  ∀m. ∀w: Vector A m. subvector_with A … eq v (w@@v).
610 #A #n #eq #refl #v elim v
611 [ //
612 | #m #hd #tl #IH #m #w whd in match (subvector_with ??????); >mem_append //
613   change with (bool_to_Prop (subvector_with ??????)) lapply (IH … (w@@[[hd]]))
614  lapply (vector_associative_append ???? w [[hd]] tl) #EQ
615  @(dependent_rewrite_vectors … EQ) //
616 ]
617qed.
618
619lemma subvector_with_refl:
620 ∀A:Type[0]. ∀n. ∀eq: A → A → bool. (∀a. eq a a = true) → ∀v: Vector A n.
621  subvector_with A … eq v v.
622 #A #n #eq #refl #v @(subvector_with_refl0 … v … [[]]) //
623qed.
624
625(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
626(* Lemmas.                                                                    *)
627(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)   
628   
629lemma map_fusion:
630  ∀A, B, C: Type[0].
631  ∀n: nat.
632  ∀v: Vector A n.
633  ∀f: A → B.
634  ∀g: B → C.
635    map B C n g (map A B n f v) = map A C n (λx. g (f x)) v.
636  #A #B #C #n #v #f #g
637  elim v
638  [ normalize
639    %
640  | #N #H #V #H2
641    normalize
642    > H2
643    %
644  ]
645qed.
Note: See TracBrowser for help on using the repository browser.