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 definition vec_tail ≝ λA.λn.λv:Vector A n.
  20 mk_Vector A (pred n) (tail A v) ?.
  21 >length_tail >(len A n v) //
  22 qed.
  23
  24 definition vec_cons ≝ λA.λa.λn.λv:Vector A n.
  25 mk_Vector A (S n) (cons A a v) ?.
  26 normalize >(len A n v) //
  27 qed.
  28
  29 definition vec_append ≝ λA.λn1,n2.λv1:Vector A n1.λv2: Vector A n2.
  30 mk_Vector A (n1+n2) (v1@v2).
  31
  32 definition vec_map ≝ λA,B.λf:A→B.λn.λv:Vector A n.
  33 mk_Vector B n (map ?? f v)
  34   (trans_eq … (length_map …) (len A n v)).
  35
  36 let rec pmap A B C (f:A→B→C) l1 l2 on l1 ≝
  37    match l1 with
  38    [ nil ⇒ nil C
  39    | cons a tlA ⇒
  40      match l2 with
  41      [nil ⇒ nil C
  42      |cons b tlB ⇒ (f a b)::pmap A B C f tlA tlB
  43      ]
  44    ].
  45
  46 lemma length_pmap: ∀A,B,C.∀f:A→B→C.∀l1,l2.
  47 length C (pmap  A B C f l1 l2) =
  48   min (length A l1) (length B l2).
  49 #A #B #C #f #l1 elim l1 // #a #tlA #Hind #l2 cases l2 //
  50 #b #tlB lapply (Hind tlB) normalize
  51 cases (true_or_false (leb (length A tlA) (length B tlB))) #H >H
  52 normalize //
  53 qed.
  54
  55 definition pmap_vec ≝ λA,B,C.λf:A→B→C.λn.λvA:Vector A n.λvB:Vector B n.
  56 mk_Vector C n (pmap A B C f vA vB) ?.
  57 >length_pmap >(len A n vA) >(len B n vB) normalize
  58 >(le_to_leb_true … (le_n n)) //
  59 qed.
  60