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/lists/list.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_of_list ≝ λA,l.
  20   mk_Vector A (|l|) l (refl ??).
  21
  22 lemma Vector_eq : ∀A,n,v1,v2.
  23   vec A n v1 = vec A n v2 → v1 = v2.
  24 #A #n * #l1 #H1 * #l2 #H2 #eql1l2 generalize in match H1;
  25 -H1 >eql1l2 //
  26 qed.
  27
  28 definition vec_tail ≝ λA.λn.λv:Vector A n.
  29 mk_Vector A (pred n) (tail A v) ?.
  30 >length_tail >(len A n v) //
  31 qed.
  32
  33 definition vec_cons ≝ λA.λa.λn.λv:Vector A n.
  34 mk_Vector A (S n) (cons A a v) ?.
  35 normalize >(len A n v) //
  36 qed.
  37
  38 definition vec_hd ≝ λA.λn.λv:Vector A (S n).
  39 hd A v ?. elim v * [normalize #H destruct | #a #H #eq @a]
  40 qed.
  41
  42 lemma vec_expand: ∀A,n,v.
  43  v = vec_cons A (vec_hd A n v) n (vec_tail A (S n) v).
  44 #A #n * #l cases l [normalize in ⊢ (%→?); #H destruct  |//]
  45 qed.
  46
  47 lemma vector_nil: ∀A.∀v:Vector A 0.
  48   v = mk_Vector A 0 (nil A) (refl ??).
  49 #A * * // #a #tl normalize #H destruct
  50 qed.
  51
  52 definition vec_append ≝ λA.λn1,n2.λv1:Vector A n1.λv2: Vector A n2.
  53 mk_Vector A (n1+n2) (v1@v2).
  54
  55 definition vec_map ≝ λA,B.λf:A→B.λn.λv:Vector A n.
  56 mk_Vector B n (map ?? f v)
  57   (trans_eq … (length_map …) (len A n v)).
  58
  59 lemma nth_default : ∀A,i,n.∀v:Vector A n.∀d1,d2. i < n →
  60   nth i ? v d1 = nth i ? v d2.
  61 #A #i elim i -i
  62   [#n #v #d1 #d2 #ltOn lapply v @(lt_O_n_elim … ltOn)
  63    -v #m #v >(vec_expand … v) //
  64   |#i #Hind #n #v #d1 #d2 #ltn lapply ltn lapply v @(lt_O_n_elim … (ltn_to_ltO … ltn))
  65    -v -ltn #m #v #ltim >(vec_expand … v) @(Hind m (vec_tail A (S m) v) d1 d2 ?)
  66    @le_S_S_to_le //
  67   ]
  68 qed.
  69
  70 lemma eq_vec: ∀A,n.∀v1,v2:Vector A n.∀d.
  71   (∀i. i < n → nth i A v1 d = nth i A v2 d) → v1 = v2.
  72 #A #n elim n -n
  73   [#v1 #v2 #H >(vector_nil A v1) >(vector_nil A v2) //
  74   |#n #Hind #v1 #v2 #d #H >(vec_expand … v1) >(vec_expand … v2)
  75    >(Hind (vec_tail … v1) (vec_tail … v2) d)
  76     [cut (vec_hd A n v1 = vec_hd A n v2) //
  77      cut (∀i,d1,d2. i < S n → nth i A v1 d1 = nth i A v2 d2)
  78        [#i #d1 #d2 #Hi >(nth_default ????? d) // >(nth_default ???? d2 d) // @H //]
  79      -H #H @(H 0) //
  80     |#i #ltin @(H (S i)) @le_S_S //
  81     ]
  82   ]
  83 qed.
  84
  85 lemma nth_vec_map :
  86   ∀A,B,f,i,n.∀v:Vector A n.∀d.
  87   f (nth i ? v d) = nth i ? (vec_map A B f n v) (f d).
  88 #A #B #f #i elim i
  89 [ *
  90   [ #v #d >(vector_nil … v) %
  91   | #n0 #v #d >(vec_expand … v) % ]
  92 | #i0 #IH *
  93   [ #v #d >(vector_nil … v) normalize cases i0 //
  94   | #n #v #d >(vec_expand … v) whd in ⊢ (??(?%)%);
  95     >(IH n (vec_tail A (S n) v) d) % ] ]
  96 qed.
  97
  98
  99 (* mapi: map with index to move in list.ma *)
 100 let rec change_vec (A:Type[0]) (n:nat) on n ≝
 101 match n return λn0.∀v:Vector A n0.A→nat→Vector A n0 with
 102 [ O ⇒ λv,a,i.v
 103 | S m ⇒ λv,a,i.
 104   match i with
 105   [ O ⇒ vec_cons A a m (vec_tail … v)
 106   | S j ⇒ vec_cons A (vec_hd A m v) m (change_vec A m (vec_tail … v) a j)
 107   ]
 108 ].
 109
 110 lemma nth_change_vec : ∀A,i,n,v,a,d. i < n →
 111   nth i ? (change_vec A n v a i) d = a.
 112 #A #i elim i
 113   [#n #v #a #d #ltOn lapply v -v @(lt_O_n_elim n ltOn ??) //
 114   |#m #Hind #n #v #a #d #Hlt
 115    lapply Hlt lapply v @(lt_O_n_elim … (ltn_to_ltO … Hlt))
 116    #p #v #ltmp @Hind @le_S_S_to_le //
 117   ]
 118 qed.
 119
 120 lemma nth_change_vec_neq : ∀A,j,i,n,v,a,d. i ≠ j →
 121   nth j ? (change_vec A n v a i) d = nth j ? v d.
 122 #A #j elim j
 123   [#i * // #n #v #a #d cases i
 124     [#H @False_ind @(absurd ?? H) //
 125     |#i0 #_ >(vec_expand ?? v) in ⊢ (???%); //
 126     ]
 127   |#m #Hind #i * // cases i // #i0 #n #v #a #d #neqim
 128    whd in ⊢(??%?); whd in match (tail ??); >Hind
 129     [>(vec_expand ??v) in ⊢ (???%); // |@(not_to_not … neqim) // ]
 130   ]
 131 qed.
 132
 133 lemma change_vec_same : ∀sig,n,v,i,d.
 134   change_vec sig n v (nth i ? v d) i = v.
 135 #sig #n #v #i #d @(eq_vec … d)
 136 #i0 #Hi0 cases (decidable_eq_nat i i0) #Hi0
 137 [ >Hi0 >nth_change_vec //
 138 | >nth_change_vec_neq //
 139 ]
 140 qed.
 141
 142 lemma change_vec_cons_tail :∀A,n,vA,a,b,i.
 143   change_vec A (S n) (vec_cons ? a n vA) b (S i) =
 144   vec_cons ? a n (change_vec A n vA b i).
 145 #A #n #vA cases vA //
 146 qed.
 147
 148 lemma change_vec_commute : ∀A,n,v,a,b,i,j. i ≠ j →
 149   change_vec A n (change_vec A n v a i) b j
 150   = change_vec A n (change_vec A n v b j) a i.
 151 #A #n #v #a #b #i #j #Hij @(eq_vec … a)
 152 #k #Hk cases (decidable_eq_nat k i) #Hki
 153 [ >Hki >nth_change_vec // >(nth_change_vec_neq ??????? (sym_not_eq … Hij))
 154   >nth_change_vec //
 155 | cases (decidable_eq_nat k j) #Hkj
 156   [ >Hkj >nth_change_vec // >(nth_change_vec_neq ??????? Hij) >nth_change_vec //
 157   | >(nth_change_vec_neq ??????? (sym_not_eq … Hki))
 158     >(nth_change_vec_neq ??????? (sym_not_eq … Hkj))
 159     >(nth_change_vec_neq ??????? (sym_not_eq … Hki))
 160     >(nth_change_vec_neq ??????? (sym_not_eq … Hkj)) //
 161   ]
 162 ]
 163 qed.
 164
 165 lemma change_vec_change_vec : ∀A,n,v,a,b,i.
 166   change_vec A n (change_vec A n v a i) b i = change_vec A n v b i.
 167 #A #n #v #a #b #i @(eq_vec … a) #i0 #Hi0
 168 cases (decidable_eq_nat i i0) #Hii0
 169 [ >Hii0 >nth_change_vec // >nth_change_vec //
 170 | >nth_change_vec_neq // >nth_change_vec_neq //
 171   >nth_change_vec_neq // ]
 172 qed.
 173
 174 lemma eq_vec_change_vec : ∀sig,n.∀v1,v2:Vector sig n.∀i,t,d.
 175   nth i ? v2 d = t →
 176   (∀j.i ≠ j → nth j ? v1 d = nth j ? v2 d) →
 177   v2 = change_vec ?? v1 t i.
 178 #sig #n #v1 #v2 #i #t #d #H1 #H2 @(eq_vec … d)
 179 #i0 #Hlt cases (decidable_eq_nat i0 i) #Hii0
 180 [ >Hii0 >nth_change_vec //
 181 | >nth_change_vec_neq [|@sym_not_eq //] @sym_eq @H2 @sym_not_eq // ]
 182 qed-.
 183
 184 (* map *)
 185
 186 let rec pmap A B C (f:A→B→C) l1 l2 on l1 ≝
 187    match l1 with
 188    [ nil ⇒ nil C
 189    | cons a tlA ⇒
 190      match l2 with
 191      [nil ⇒ nil C
 192      |cons b tlB ⇒ (f a b)::pmap A B C f tlA tlB
 193      ]
 194    ].
 195
 196 lemma length_pmap: ∀A,B,C.∀f:A→B→C.∀l1,l2.
 197 length C (pmap  A B C f l1 l2) =
 198   min (length A l1) (length B l2).
 199 #A #B #C #f #l1 elim l1 // #a #tlA #Hind #l2 cases l2 //
 200 #b #tlB lapply (Hind tlB) normalize
 201 cases (true_or_false (leb (length A tlA) (length B tlB))) #H >H
 202 normalize //
 203 qed.
 204
 205 definition pmap_vec ≝ λA,B,C.λf:A→B→C.λn.λvA:Vector A n.λvB:Vector B n.
 206 mk_Vector C n (pmap A B C f vA vB) ?.
 207 >length_pmap >(len A n vA) >(len B n vB) normalize
 208 >(le_to_leb_true … (le_n n)) //
 209 qed.
 210
 211 lemma pmap_vec_cons :∀A,B,C,f,n,vA,vB,a,b.
 212   pmap_vec A B C f (S n) (vec_cons ? a n vA) (vec_cons ? b n vB) =
 213   vec_cons ? (f a b) n (pmap_vec A B C f n vA vB).
 214 // qed.
 215
 216 lemma pmap_change : ∀A,B,C,f,n,vA,vB,a,b,i.
 217   pmap_vec A B C f n (change_vec ? n vA a i) (change_vec ? n vB b i) =
 218   change_vec ? n (pmap_vec A B C f n vA vB) (f a b) i.
 219 #A #B #C #f #n elim n //
 220 #m #Hind #vA #vB #a #b >(vec_expand … vA) >(vec_expand … vB) * //
 221 #i >pmap_vec_cons >pmap_vec_cons >change_vec_cons_tail @eq_f @Hind
 222 qed.