vector.v 12.7 KB
Newer Older
1
(* Copyright (c) 2012-2019, Coq-std++ developers. *)
2 3
(* This file is distributed under the terms of the BSD license. *)
(** This file collects general purpose definitions and theorems on vectors
4 5 6 7
(lists of fixed length). It uses the definitions from the standard library, but
renames or changes their notations, so that it becomes more consistent with the
naming conventions in this development. *)
From stdpp Require Export fin list.
8
Set Default Proof Using "Type".
9 10 11 12 13 14 15 16 17 18 19 20 21 22
Open Scope vector_scope.

(** The type [vec n] represents lists of consisting of exactly [n] elements.
Whereas the standard library declares exactly the same notations for vectors as
used for lists, we use slightly different notations so it becomes easier to use
lists and vectors together. *)
Notation vec := Vector.t.
Notation vnil := Vector.nil.
Arguments vnil {_}.
Notation vcons := Vector.cons.
Notation vapp := Vector.append.
Arguments vcons {_} _ {_} _.

Infix ":::" := vcons (at level 60, right associativity) : vector_scope.
23
Notation "(:::)" := vcons (only parsing) : vector_scope.
24 25
Notation "( x :::.)" := (vcons x) (only parsing) : vector_scope.
Notation "(.::: v )" := (λ x, vcons x v) (only parsing) : vector_scope.
26 27 28 29
Notation "[# ] " := vnil : vector_scope.
Notation "[# x ] " := (vcons x vnil) : vector_scope.
Notation "[# x ; .. ; y ] " := (vcons x .. (vcons y vnil) ..) : vector_scope.
Infix "+++" := vapp (at level 60, right associativity) : vector_scope.
30
Notation "(+++)" := vapp (only parsing) : vector_scope.
31 32
Notation "( v +++.)" := (vapp v) (only parsing) : vector_scope.
Notation "(.+++ w )" := (λ v, vapp v w) (only parsing) : vector_scope.
33

Dan Frumin's avatar
Dan Frumin committed
34 35 36 37 38 39 40 41 42 43 44
(** Similar to [fin], we provide an inversion principle that keeps the length
fixed. We define a tactic [inv_vec v] to perform case analysis on [v], using
this inversion principle. *)
Notation vec_0_inv := Vector.case0.
Definition vec_S_inv {A n} (P : vec A (S n)  Type)
  (Hcons :  x v, P (x ::: v)) v : P v.
Proof.
  revert P Hcons.
  refine match v with [#] => tt | x ::: v => λ P Hcons, Hcons x v end.
Defined.

45 46 47
(** Notice that we cannot define [Vector.nth] as an instance of our [Lookup]
type class, as it has a dependent type. *)
Arguments Vector.nth {_ _} !_ !_%fin /.
Dan Frumin's avatar
Dan Frumin committed
48 49 50 51 52 53
Instance vector_lookup_total A :  m, LookupTotal (fin m) A (vec A m) :=
  fix go m i {struct i} := let _ :  m, LookupTotal _ _ _ := @go in
  match i in fin m return vec A m  A with
  | 0%fin => vec_S_inv (λ _, A) (λ x _, x)
  | FS j => vec_S_inv (λ _, A) (λ _ v, v !!! j)
  end.
54 55 56 57 58 59 60 61

(** The tactic [vec_double_ind v1 v2] performs double induction on [v1] and [v2]
provided that they have the same length. *)
Notation vec_rect2 := Vector.rect2.
Ltac vec_double_ind v1 v2 :=
  match type of v1 with
  | vec _ ?n =>
    repeat match goal with
62
    | H' : context [ n ] |- _ => var_neq v1 H'; var_neq v2 H'; revert H'
63 64
    end;
    revert n v1 v2;
65
    match goal with |-  n v1 v2, @?P n v1 v2 => apply (vec_rect2 P) end
66 67 68 69 70 71 72 73
  end.

Notation vcons_inj := VectorSpec.cons_inj.
Lemma vcons_inj_1 {A n} x y (v w : vec A n) : x ::: v = y ::: w  x = y.
Proof. apply vcons_inj. Qed.
Lemma vcons_inj_2 {A n} x y (v w : vec A n) : x ::: v = y ::: w  v = w.
Proof. apply vcons_inj. Qed.

74
Lemma vec_eq {A n} (v w : vec A n) : ( i, v !!! i = w !!! i)  v = w.
75 76
Proof.
  vec_double_ind v w; [done|]. intros n v w IH x y Hi. f_equal.
77 78
  - apply (Hi 0%fin).
  - apply IH. intros i. apply (Hi (FS i)).
79 80
Qed.

81
Instance vec_dec {A} {dec : EqDecision A} {n} : EqDecision (vec A n).
82 83 84 85 86 87 88 89 90
Proof.
 refine (vec_rect2
  (λ n (v w : vec A n), { v = w } + { v  w })
  (left _)
  (λ _ _ _ H x y, cast_if_and (dec x y) H));
  f_equal; eauto using vcons_inj_1, vcons_inj_2.
Defined.

Ltac inv_vec v :=
Robbert Krebbers's avatar
Robbert Krebbers committed
91 92
  let T := type of v in
  match eval hnf in T with
93 94 95 96 97 98 99 100
  | vec _ ?n =>
    match eval hnf in n with
    | 0 => revert dependent v; match goal with |-  v, @?P v => apply (vec_0_inv P) end
    | S ?n =>
      revert dependent v; match goal with |-  v, @?P v => apply (vec_S_inv P) end;
      (* Try going on recursively. *)
      try (let x := fresh "x" in intros x v; inv_vec v; revert x)
    end
101 102 103 104 105
  end.

(** The following tactic performs case analysis on all hypotheses of the shape
[fin 0], [fin (S n)], [vec A 0] and [vec A (S n)] until no further case
analyses are possible. *)
106
Ltac inv_all_vec_fin := block_goal;
107 108 109
  repeat match goal with
  | v : vec _ _ |- _ => inv_vec v; intros
  | i : fin _ |- _ => inv_fin i; intros
110
  end; unblock_goal.
111 112 113 114 115

(** We define a coercion from [vec] to [list] and show that it preserves the
operations on vectors. We also define a function to go in the other way, but
do not define it as a coercion, as it would otherwise introduce ambiguity. *)
Fixpoint vec_to_list {A n} (v : vec A n) : list A :=
116
  match v with [#] => [] | x ::: v => x :: vec_to_list v end.
117 118 119 120 121 122 123 124
Coercion vec_to_list : vec >-> list.
Notation list_to_vec := Vector.of_list.

Lemma vec_to_list_cons {A n} x (v : vec A n) :
  vec_to_list (x ::: v) = x :: vec_to_list v.
Proof. done. Qed.
Lemma vec_to_list_app {A n m} (v : vec A n) (w : vec A m) :
  vec_to_list (v +++ w) = vec_to_list v ++ vec_to_list w.
125
Proof. by induction v; f_equal/=. Qed.
126
Lemma vec_to_list_of_list {A} (l : list A): vec_to_list (list_to_vec l) = l.
127
Proof. by induction l; f_equal/=. Qed.
128 129
Lemma vec_to_list_length {A n} (v : vec A n) : length (vec_to_list v) = n.
Proof. induction v; simpl; by f_equal. Qed.
130
Lemma vec_to_list_same_length {A B n} (v : vec A n) (w : vec B n) :
131 132
  length v = length w.
Proof. by rewrite !vec_to_list_length. Qed.
133 134 135 136
Lemma vec_to_list_inj1 {A n m} (v : vec A n) (w : vec A m) :
  vec_to_list v = vec_to_list w  n = m.
Proof.
  revert m w. induction v; intros ? [|???] ?;
137
    simplify_eq/=; f_equal; eauto.
138 139 140 141 142
Qed.
Lemma vec_to_list_inj2 {A n} (v : vec A n) (w : vec A n) :
  vec_to_list v = vec_to_list w  v = w.
Proof.
  revert w. induction v; intros w; inv_vec w; intros;
143
    simplify_eq/=; f_equal; eauto.
144 145 146 147
Qed.
Lemma vlookup_middle {A n m} (v : vec A n) (w : vec A m) x :
   i : fin (n + S m), x = (v +++ x ::: w) !!! i.
Proof.
148 149
  induction v; simpl; [by eexists 0%fin|].
  destruct IHv as [i ?]. by exists (FS i).
150 151 152 153 154 155 156 157 158
Qed.
Lemma vec_to_list_lookup_middle {A n} (v : vec A n) (l k : list A) x :
  vec_to_list v = l ++ x :: k 
     i : fin n, l = take i v  x = v !!! i  k = drop (S i) v.
Proof.
  intros H.
  rewrite <-(vec_to_list_of_list l), <-(vec_to_list_of_list k) in H.
  rewrite <-vec_to_list_cons, <-vec_to_list_app in H.
  pose proof (vec_to_list_inj1 _ _ H); subst.
159
  apply vec_to_list_inj2 in H; subst. induction l. simpl.
160 161
  - eexists 0%fin. simpl. by rewrite vec_to_list_of_list.
  - destruct IHl as [i ?]. exists (FS i). simpl. intuition congruence.
162 163 164 165 166 167
Qed.
Lemma vec_to_list_drop_lookup {A n} (v : vec A n) (i : fin n) :
  drop i v = v !!! i :: drop (S i) v.
Proof. induction i; inv_vec v; simpl; intros; [done | by rewrite IHi]. Qed.
Lemma vec_to_list_take_drop_lookup {A n} (v : vec A n) (i : fin n) :
  vec_to_list v = take i v ++ v !!! i :: drop (S i) v.
168
Proof. rewrite <-(take_drop i v) at 1. by rewrite vec_to_list_drop_lookup. Qed.
169

170 171 172 173 174 175 176 177 178 179 180 181 182 183
Lemma vlookup_lookup {A n} (v : vec A n) (i : fin n) x :
  v !!! i = x  (v : list A) !! (i : nat) = Some x.
Proof.
  induction v as [|? ? v IH]; inv_fin i. simpl; split; congruence. done.
Qed.
Lemma vlookup_lookup' {A n} (v : vec A n) (i : nat) x :
  ( H : i < n, v !!! (fin_of_nat H) = x)  (v : list A) !! i = Some x.
Proof.
  split.
  - intros [Hlt ?]. rewrite <-(fin_to_of_nat i n Hlt). by apply vlookup_lookup.
  - intros Hvix. assert (Hlt:=lookup_lt_Some _ _ _ Hvix).
    rewrite vec_to_list_length in Hlt. exists Hlt.
    apply vlookup_lookup. by rewrite fin_to_of_nat.
Qed.
184 185
Lemma elem_of_vlookup {A n} (v : vec A n) x :
  x  vec_to_list v   i, v !!! i = x.
186
Proof.
187 188 189
  rewrite elem_of_list_lookup. setoid_rewrite <-vlookup_lookup'.
  split; [by intros (?&?&?); eauto|]. intros [i Hx].
  exists i, (fin_to_nat_lt _). by rewrite fin_of_to_nat.
190
Qed.
191

192 193
Lemma Forall_vlookup {A} (P : A  Prop) {n} (v : vec A n) :
  Forall P (vec_to_list v)   i, P (v !!! i).
194
Proof. rewrite Forall_forall. setoid_rewrite elem_of_vlookup. naive_solver. Qed.
195 196 197 198 199 200 201 202
Lemma Forall_vlookup_1 {A} (P : A  Prop) {n} (v : vec A n) i :
  Forall P (vec_to_list v)  P (v !!! i).
Proof. by rewrite Forall_vlookup. Qed.
Lemma Forall_vlookup_2 {A} (P : A  Prop) {n} (v : vec A n) :
  ( i, P (v !!! i))  Forall P (vec_to_list v).
Proof. by rewrite Forall_vlookup. Qed.
Lemma Exists_vlookup {A} (P : A  Prop) {n} (v : vec A n) :
  Exists P (vec_to_list v)   i, P (v !!! i).
203 204 205 206
Proof. rewrite Exists_exists. setoid_rewrite elem_of_vlookup. naive_solver. Qed.
Lemma Forall2_vlookup {A B} (P : A  B  Prop) {n}
    (v1 : vec A n) (v2 : vec B n) :
  Forall2 P (vec_to_list v1) (vec_to_list v2)   i, P (v1 !!! i) (v2 !!! i).
207 208
Proof.
  split.
209
  - vec_double_ind v1 v2; [intros _ i; inv_fin i |].
210 211
    intros n v1 v2 IH a b; simpl. inversion_clear 1.
    intros i. inv_fin i; simpl; auto.
212
  - vec_double_ind v1 v2; [constructor|].
213
    intros ??? IH ?? H. constructor. apply (H 0%fin). apply IH, (λ i, H (FS i)).
214 215
Qed.

216
(** The function [vmap f v] applies a function [f] element wise to [v]. *)
217 218 219 220
Notation vmap := Vector.map.

Lemma vlookup_map `(f : A  B) {n} (v : vec A n) i :
  vmap f v !!! i = f (v !!! i).
Dan Frumin's avatar
Dan Frumin committed
221
Proof. by induction v; inv_fin i; eauto. Qed.
222 223 224 225 226 227 228 229
Lemma vec_to_list_map `(f : A  B) {n} (v : vec A n) :
  vec_to_list (vmap f v) = f <$> vec_to_list v.
Proof. induction v; simpl. done. by rewrite IHv. Qed.

(** The function [vzip_with f v w] combines the vectors [v] and [w] element
wise using the function [f]. *)
Notation vzip_with := Vector.map2.

230
Lemma vlookup_zip_with `(f : A  B  C) {n} (v1 : vec A n) (v2 : vec B n) i :
231
  vzip_with f v1 v2 !!! i = f (v1 !!! i) (v2 !!! i).
Dan Frumin's avatar
Dan Frumin committed
232 233 234 235 236 237
Proof.
  vec_double_ind v1 v2.
  - intros i; inv_fin i.
  - intros n v1 v2 IH a b i.
    inv_fin i; eauto.
Qed.
238
Lemma vec_to_list_zip_with `(f : A  B  C) {n} (v1 : vec A n) (v2 : vec B n) :
239 240 241
  vec_to_list (vzip_with f v1 v2) =
    zip_with f (vec_to_list v1) (vec_to_list v2).
Proof.
242 243
  revert v2. induction v1; intros v2; inv_vec v2; intros; simpl; [done|].
  by rewrite IHv1.
244 245
Qed.

246 247 248 249 250
(** Similar to vlookup, we cannot define [vinsert] as an instance of the
[Insert] type class, as it has a dependent type. *)
Fixpoint vinsert {A n} (i : fin n) (x : A) : vec A n  vec A n :=
  match i with
  | 0%fin => vec_S_inv _ (λ _ v, x ::: v)
Ralf Jung's avatar
Ralf Jung committed
251
  | FS i => vec_S_inv _ (λ y v, y ::: vinsert i x v)
252 253 254 255 256
  end.

Lemma vec_to_list_insert {A n} i x (v : vec A n) :
  vec_to_list (vinsert i x v) = insert (fin_to_nat i) x (vec_to_list v).
Proof. induction v; inv_fin i. done. simpl. intros. by rewrite IHv. Qed.
257

258 259 260 261 262 263 264 265
Lemma vlookup_insert {A n} i x (v : vec A n) : vinsert i x v !!! i = x.
Proof. by induction i; inv_vec v. Qed.
Lemma vlookup_insert_ne {A n} i j x (v : vec A n) :
  i  j  vinsert i x v !!! j = v !!! j.
Proof.
  induction i; inv_fin j; inv_vec v; simpl; try done.
  intros. apply IHi. congruence.
Qed.
266
Lemma vlookup_insert_self {A n} i (v : vec A n) : vinsert i (v !!! i) v = v.
267
Proof. by induction v; inv_fin i; intros; f_equal/=. Qed.
Ralf Jung's avatar
Ralf Jung committed
268

269 270 271 272 273 274 275 276 277 278 279 280 281 282 283 284 285 286 287 288 289 290 291 292
Lemma vmap_insert {A B} (f : A  B) (n : nat) i x (v : vec A n) :
  vmap f (vinsert i x v) = vinsert i (f x) (vmap f v).
Proof. induction v; inv_fin i; intros; f_equal/=; auto. Qed.

(** The functions [vtake i v] and [vdrop i v] take the first [i] elements of
a vector [v], respectively remove the first [i] elements of a vector [v]. *)
Fixpoint vtake {A n} (i : fin n) : vec A n  vec A i :=
  match i in fin n return vec A n  vec A i with
  | 0%fin => λ _, [#]
  | FS i => vec_S_inv _ (λ x v, x ::: vtake i v)
  end.
Fixpoint vdrop {A n} (i : fin n) : vec A n  vec A (n - i) :=
  match i in fin n return vec A n  vec A (n - i) with
  | 0%fin => id
  | FS i => vec_S_inv _ (λ _, vdrop i)
  end.

Lemma vec_to_list_take {A n} i (v : vec A n) :
  vec_to_list (vtake i v) = take (fin_to_nat i) (vec_to_list v).
Proof. induction i; inv_vec v; intros; f_equal/=; auto. Qed.
Lemma vec_to_list_drop {A n} i (v : vec A n) :
  vec_to_list (vdrop i v) = drop (fin_to_nat i) (vec_to_list v).
Proof. induction i; inv_vec v; intros; f_equal/=; auto. Qed.

293 294 295 296
(** The function [vreplicate n x] generates a vector with length [n] of elements
with value [x]. *)
Fixpoint vreplicate {A} (n : nat) (x : A) : vec A n :=
  match n with 0 => [#] | S n => x ::: vreplicate n x end.
Ralf Jung's avatar
Ralf Jung committed
297

298 299 300 301
Lemma vec_to_list_replicate {A} n (x : A) :
  vec_to_list (vreplicate n x) = replicate n x.
Proof. induction n; by f_equal/=. Qed.

302 303 304 305 306 307 308
Lemma vlookup_replicate {A} n (x : A) i : vreplicate n x !!! i = x.
Proof. induction i; f_equal/=; auto. Qed.

Lemma vmap_replicate {A B} (f : A  B) n (x : A) :
  vmap f (vreplicate n x) = vreplicate n (f x).
Proof. induction n; f_equal/=; auto. Qed.

309 310 311 312
(* Vectors can be inhabited. *)
Global Instance vec_0_inhabited T : Inhabited (vec T 0) := populate [#].
Global Instance vec_inhabited `{Inhabited T} n : Inhabited (vec T n) :=
  populate (vreplicate n inhabitant).