vector.v 14.2 KB
Newer Older
Robbert Krebbers's avatar
Robbert Krebbers committed
1
(* Copyright (c) 2012-2015, Robbert Krebbers. *)
2 3 4 5 6 7
(* This file is distributed under the terms of the BSD license. *)
(** This file collects general purpose definitions and theorems on vectors
(lists of fixed length) and the fin type (bounded naturals). 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. *)
8
From stdpp Require Export list.
9
Set Default Proof Using "Type*".
10 11 12 13 14 15 16 17 18 19 20 21 22 23 24
Open Scope vector_scope.

(** * The fin type *)
(** The type [fin n] represents natural numbers [i] with [0 ≤ i < n]. We
define a scope [fin], in which we declare notations for small literals of the
[fin] type. Whereas the standard library starts counting at [1], we start
counting at [0]. This way, the embedding [fin_to_nat] preserves [0], and allows
us to define [fin_to_nat] as a coercion without introducing notational
ambiguity. *)
Notation fin := Fin.t.
Notation FS := Fin.FS.

Delimit Scope fin_scope with fin.
Arguments Fin.FS _ _%fin.

25 26 27 28 29
Notation "0" := Fin.F1 : fin_scope. Notation "1" := (FS 0) : fin_scope.
Notation "2" := (FS 1) : fin_scope. Notation "3" := (FS 2) : fin_scope.
Notation "4" := (FS 3) : fin_scope. Notation "5" := (FS 4) : fin_scope.
Notation "6" := (FS 5) : fin_scope. Notation "7" := (FS 6) : fin_scope.
Notation "8" := (FS 7) : fin_scope. Notation "9" := (FS 8) : fin_scope.
30 31 32
Notation "10" := (FS 9) : fin_scope.

Fixpoint fin_to_nat {n} (i : fin n) : nat :=
33
  match i with 0%fin => 0 | FS _ i => S (fin_to_nat i) end.
34 35
Coercion fin_to_nat : fin >-> nat.

36
Notation fin_of_nat := Fin.of_nat_lt.
37 38
Notation fin_rect2 := Fin.rect2.

39
Instance fin_dec {n} : EqDecision (fin n).
40 41 42 43 44 45 46
Proof.
 refine (fin_rect2
  (λ n (i j : fin n), { i = j } + { i  j })
  (λ _, left _)
  (λ _ _, right _)
  (λ _ _, right _)
  (λ _ _ _ H, cast_if H));
47
  abstract (f_equal; by auto using Fin.FS_inj).
48 49 50 51 52 53 54 55 56 57 58 59 60
Defined.

(** The inversion principle [fin_S_inv] is more convenient than its variant
[Fin.caseS] in the standard library, as we keep the parameter [n] fixed.
In the tactic [inv_fin i] to perform dependent case analysis on [i], we
therefore do not have to generalize over the index [n] and all assumptions
depending on it. Notice that contrary to [dependent destruction], which uses
the [JMeq_eq] axiom, the tactic [inv_fin] produces axiom free proofs.*)
Notation fin_0_inv := Fin.case0.

Definition fin_S_inv {n} (P : fin (S n)  Type)
  (H0 : P 0%fin) (HS :  i, P (FS i)) (i : fin (S n)) : P i.
Proof.
61 62
  revert P H0 HS.
  refine match i with 0%fin => λ _ H0 _, H0 | FS _ i => λ _ _ HS, HS i end.
63 64 65 66 67
Defined.

Ltac inv_fin i :=
  match type of i with
  | fin 0 =>
68
    revert dependent i; match goal with |-  i, @?P i => apply (fin_0_inv P) end
69
  | fin (S ?n) =>
70
    revert dependent i; match goal with |-  i, @?P i => apply (fin_S_inv P) end
71 72
  end.

73
Instance FS_inj: Inj (=) (=) (@FS n).
74
Proof. intros n i j. apply Fin.FS_inj. Qed.
75
Instance fin_to_nat_inj : Inj (=) (=) (@fin_to_nat n).
76
Proof.
77
  intros n i. induction i; intros j; inv_fin j; intros; f_equal/=; auto with lia.
78
Qed.
79

80 81
Lemma fin_to_nat_lt {n} (i : fin n) : fin_to_nat i < n.
Proof. induction i; simpl; lia. Qed.
82
Lemma fin_to_of_nat n m (H : n < m) : fin_to_nat (fin_of_nat H) = n.
83 84 85
Proof.
  revert m H. induction n; intros [|?]; simpl; auto; intros; exfalso; lia.
Qed.
86 87
Lemma fin_of_to_nat {n} (i : fin n) H : @fin_of_nat (fin_to_nat i) n H = i.
Proof. apply (inj fin_to_nat), fin_to_of_nat. Qed.
88

89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113
Fixpoint fin_plus_inv {n1 n2} :  (P : fin (n1 + n2)  Type)
    (H1 :  i1 : fin n1, P (Fin.L n2 i1))
    (H2 :  i2, P (Fin.R n1 i2)) (i : fin (n1 + n2)), P i :=
  match n1 with
  | 0 => λ P H1 H2 i, H2 i
  | S n => λ P H1 H2, fin_S_inv P (H1 0%fin) (fin_plus_inv _ (λ i, H1 (FS i)) H2)
  end.

Lemma fin_plus_inv_L {n1 n2} (P : fin (n1 + n2)  Type)
    (H1:  i1 : fin n1, P (Fin.L _ i1)) (H2:  i2, P (Fin.R _ i2)) (i: fin n1) :
  fin_plus_inv P H1 H2 (Fin.L n2 i) = H1 i.
Proof.
  revert P H1 H2 i.
  induction n1 as [|n1 IH]; intros P H1 H2 i; inv_fin i; simpl; auto.
  intros i. apply (IH (λ i, P (FS i))).
Qed.

Lemma fin_plus_inv_R {n1 n2} (P : fin (n1 + n2)  Type)
    (H1:  i1 : fin n1, P (Fin.L _ i1)) (H2:  i2, P (Fin.R _ i2)) (i: fin n2) :
  fin_plus_inv P H1 H2 (Fin.R n1 i) = H2 i.
Proof.
  revert P H1 H2 i; induction n1 as [|n1 IH]; intros P H1 H2 i; simpl; auto.
  apply (IH (λ i, P (FS i))).
Qed.

114 115 116 117 118 119 120 121 122 123 124 125 126
(** * Vectors *)
(** 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.
127 128 129
Notation "(:::)" := vcons (only parsing) : vector_scope.
Notation "( x :::)" := (vcons x) (only parsing) : vector_scope.
Notation "(::: v )" := (λ x, vcons x v) (only parsing) : vector_scope.
130 131 132 133
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.
134 135 136
Notation "(+++)" := vapp (only parsing) : vector_scope.
Notation "( v +++)" := (vapp v) (only parsing) : vector_scope.
Notation "(+++ w )" := (λ v, vapp v w) (only parsing) : vector_scope.
137 138 139 140 141 142 143 144 145 146 147 148 149

(** 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 /.
Infix "!!!" := Vector.nth (at level 20) : vector_scope.

(** 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
150
    | H' : context [ n ] |- _ => var_neq v1 H'; var_neq v2 H'; revert H'
151 152
    end;
    revert n v1 v2;
153
    match goal with |-  n v1 v2, @?P n v1 v2 => apply (vec_rect2 P) end
154 155 156 157 158 159 160 161
  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.

162
Lemma vec_eq {A n} (v w : vec A n) : ( i, v !!! i = w !!! i)  v = w.
163 164
Proof.
  vec_double_ind v w; [done|]. intros n v w IH x y Hi. f_equal.
165 166
  - apply (Hi 0%fin).
  - apply IH. intros i. apply (Hi (FS i)).
167 168
Qed.

169
Instance vec_dec {A} {dec : EqDecision A} {n} : EqDecision (vec A n).
170 171 172 173 174 175 176 177 178 179 180 181 182 183 184
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.

(** 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.
185 186
  revert P Hcons.
  refine match v with [#] => tt | x ::: v => λ P Hcons, Hcons x v end.
187 188 189 190 191
Defined.

Ltac inv_vec v :=
  match type of v with
  | vec _ 0 =>
192
    revert dependent v; match goal with |-  v, @?P v => apply (vec_0_inv P) end
193
  | vec _ (S ?n) =>
194
    revert dependent v; match goal with |-  v, @?P v => apply (vec_S_inv P) end
195 196 197 198 199
  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. *)
200
Ltac inv_all_vec_fin := block_goal;
201 202 203
  repeat match goal with
  | v : vec _ _ |- _ => inv_vec v; intros
  | i : fin _ |- _ => inv_fin i; intros
204
  end; unblock_goal.
205 206 207 208 209

(** 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 :=
210
  match v with [#] => [] | x ::: v => x :: vec_to_list v end.
211 212 213 214 215 216 217 218
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.
219
Proof. by induction v; f_equal/=. Qed.
220
Lemma vec_to_list_of_list {A} (l : list A): vec_to_list (list_to_vec l) = l.
221
Proof. by induction l; f_equal/=. Qed.
222 223
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.
224
Lemma vec_to_list_same_length {A B n} (v : vec A n) (w : vec B n) :
225 226
  length v = length w.
Proof. by rewrite !vec_to_list_length. Qed.
227 228 229 230
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 ? [|???] ?;
231
    simplify_eq/=; f_equal; eauto.
232 233 234 235 236
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;
237
    simplify_eq/=; f_equal; eauto.
238 239 240 241
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.
242 243
  induction v; simpl; [by eexists 0%fin|].
  destruct IHv as [i ?]. by exists (FS i).
244 245 246 247 248 249 250 251 252
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.
253
  apply vec_to_list_inj2 in H; subst. induction l. simpl.
254 255
  - eexists 0%fin. simpl. by rewrite vec_to_list_of_list.
  - destruct IHl as [i ?]. exists (FS i). simpl. intuition congruence.
256 257 258 259 260 261
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.
262
Proof. rewrite <-(take_drop i v) at 1. by rewrite vec_to_list_drop_lookup. Qed.
263

264 265 266 267 268 269 270 271 272 273 274 275 276 277
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.
278 279
Lemma elem_of_vlookup {A n} (v : vec A n) x :
  x  vec_to_list v   i, v !!! i = x.
280
Proof.
281 282 283
  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.
284
Qed.
285

286 287
Lemma Forall_vlookup {A} (P : A  Prop) {n} (v : vec A n) :
  Forall P (vec_to_list v)   i, P (v !!! i).
288
Proof. rewrite Forall_forall. setoid_rewrite elem_of_vlookup. naive_solver. Qed.
289 290 291 292 293 294 295 296
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).
297 298 299 300
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).
301 302
Proof.
  split.
303
  - vec_double_ind v1 v2; [intros _ i; inv_fin i |].
304 305
    intros n v1 v2 IH a b; simpl. inversion_clear 1.
    intros i. inv_fin i; simpl; auto.
306
  - vec_double_ind v1 v2; [constructor|].
307
    intros ??? IH ?? H. constructor. apply (H 0%fin). apply IH, (λ i, H (FS i)).
308 309
Qed.

310
(** The function [vmap f v] applies a function [f] element wise to [v]. *)
311 312 313 314 315 316 317 318 319 320 321 322 323
Notation vmap := Vector.map.

Lemma vlookup_map `(f : A  B) {n} (v : vec A n) i :
  vmap f v !!! i = f (v !!! i).
Proof. by apply Vector.nth_map. Qed.
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.

324
Lemma vlookup_zip_with `(f : A  B  C) {n} (v1 : vec A n) (v2 : vec B n) i :
325 326
  vzip_with f v1 v2 !!! i = f (v1 !!! i) (v2 !!! i).
Proof. by apply Vector.nth_map2. Qed.
327
Lemma vec_to_list_zip_with `(f : A  B  C) {n} (v1 : vec A n) (v2 : vec B n) :
328 329 330
  vec_to_list (vzip_with f v1 v2) =
    zip_with f (vec_to_list v1) (vec_to_list v2).
Proof.
331 332
  revert v2. induction v1; intros v2; inv_vec v2; intros; simpl; [done|].
  by rewrite IHv1.
333 334
Qed.

335 336 337 338 339 340 341 342 343 344 345 346 347 348 349 350 351 352 353
(** 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)
  | FS _ i => vec_S_inv _ (λ y v, y ::: vinsert i x v)
  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.
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.
354
Lemma vlookup_insert_self {A n} i (v : vec A n) : vinsert i (v !!! i) v = v.
355
Proof. by induction v; inv_fin i; intros; f_equal/=. Qed.