matita/matita/lib/basics/vectors.ma

   1 (*
   2     ||M||  This file is part of HELM, an Hypertextual, Electronic
   3     ||A||  Library of Mathematics, developed at the Computer Science
   4     ||T||  Department of the University of Bologna, Italy.
   5     ||I||
   6     ||T||
   7     ||A||
   8     \   /  This file is distributed under the terms of the
   9      \ /   GNU General Public License Version 2
  10       V_____________________________________________________________*)
  11
  12 include "basics/finset.ma".
  13
  14 record Vector (A:Type[0]) (n:nat): Type[0] ≝
  15 { vec :> list A;
  16   len: length ? vec = n
  17 }.
  18
  19 lemma Vector_eq : ∀A,n,v1,v2.
  20   vec A n v1 = vec A n v2 → v1 = v2.
  21 #A #n * #l1 #H1 * #l2 #H2 #eql1l2 generalize in match H1;
  22 -H1 >eql1l2 //
  23 qed.
  24
  25 definition vec_tail ≝ λA.λn.λv:Vector A n.
  26 mk_Vector A (pred n) (tail A v) ?.
  27 >length_tail >(len A n v) //
  28 qed.
  29
  30 definition vec_cons ≝ λA.λa.λn.λv:Vector A n.
  31 mk_Vector A (S n) (cons A a v) ?.
  32 normalize >(len A n v) //
  33 qed.
  34
  35 definition vec_append ≝ λA.λn1,n2.λv1:Vector A n1.λv2: Vector A n2.
  36 mk_Vector A (n1+n2) (v1@v2).
  37
  38 definition vec_map ≝ λA,B.λf:A→B.λn.λv:Vector A n.
  39 mk_Vector B n (map ?? f v)
  40   (trans_eq … (length_map …) (len A n v)).
  41
  42 (* mapi: map with index to move in list.ma *)
  43 let rec mapi (A,B:Type[0]) (f: nat → A → B) (l:list A) (i:nat) on l: list B ≝
  44  match l with
  45  [ nil ⇒ nil ?
  46  | cons x tl ⇒ f i x :: (mapi A B f tl (S i))].
  47
  48 lemma length_mapi: ∀A,B,l.∀f:nat→A→B.∀i.
  49   |mapi ?? f l i| = |l|.
  50 #A #B #l #f elim l // #a #tl #Hind normalize //
  51 qed.
  52
  53 let rec make_listi (A:Type[0]) (a:nat→A) (n,i:nat) on n : list A ≝
  54 match n with
  55 [ O ⇒ [ ]
  56 | S m ⇒ a i::(make_listi A a m (S i))
  57 ].
  58
  59 lemma length_make_listi: ∀A,a,n,i.
  60   |make_listi A a n i| = n.
  61 #A #a #n elim n // #m #Hind normalize //
  62 qed.
  63
  64 definition vec_mapi ≝ λA,B.λf:nat→A→B.λn.λv:Vector A n.λi.
  65 mk_Vector B n (mapi ?? f v i)
  66   (trans_eq … (length_mapi …) (len A n v)).
  67
  68 definition make_veci ≝ λA.λa:nat→A.λn,i.
  69 mk_Vector A n (make_listi A a n i) (length_make_listi A a n i).
  70
  71 let rec pmap A B C (f:A→B→C) l1 l2 on l1 ≝
  72    match l1 with
  73    [ nil ⇒ nil C
  74    | cons a tlA ⇒
  75      match l2 with
  76      [nil ⇒ nil C
  77      |cons b tlB ⇒ (f a b)::pmap A B C f tlA tlB
  78      ]
  79    ].
  80
  81 lemma length_pmap: ∀A,B,C.∀f:A→B→C.∀l1,l2.
  82 length C (pmap  A B C f l1 l2) =
  83   min (length A l1) (length B l2).
  84 #A #B #C #f #l1 elim l1 // #a #tlA #Hind #l2 cases l2 //
  85 #b #tlB lapply (Hind tlB) normalize
  86 cases (true_or_false (leb (length A tlA) (length B tlB))) #H >H
  87 normalize //
  88 qed.
  89
  90 definition pmap_vec ≝ λA,B,C.λf:A→B→C.λn.λvA:Vector A n.λvB:Vector B n.
  91 mk_Vector C n (pmap A B C f vA vB) ?.
  92 >length_pmap >(len A n vA) >(len B n vB) normalize
  93 >(le_to_leb_true … (le_n n)) //
  94 qed.
  95