vector.v 12.7 KB
 Robbert Krebbers committed Jan 29, 2019 1 ``````(* Copyright (c) 2012-2019, Coq-std++ developers. *) `````` Robbert Krebbers committed Oct 19, 2012 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. `````` Ralf Jung committed Jan 31, 2017 8 ``````Set Default Proof Using "Type". `````` Robbert Krebbers committed Oct 19, 2012 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. `````` Robbert Krebbers committed Jun 17, 2013 23 ``````Notation "(:::)" := vcons (only parsing) : vector_scope. `````` Robbert Krebbers committed Sep 19, 2019 24 25 ``````Notation "( x :::.)" := (vcons x) (only parsing) : vector_scope. Notation "(.::: v )" := (λ x, vcons x v) (only parsing) : vector_scope. `````` Robbert Krebbers committed Oct 19, 2012 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. `````` Robbert Krebbers committed Jun 17, 2013 30 ``````Notation "(+++)" := vapp (only parsing) : vector_scope. `````` Robbert Krebbers committed Sep 19, 2019 31 32 ``````Notation "( v +++.)" := (vapp v) (only parsing) : vector_scope. Notation "(.+++ w )" := (λ v, vapp v w) (only parsing) : vector_scope. `````` Robbert Krebbers committed Oct 19, 2012 33 `````` `````` Dan Frumin committed Feb 11, 2020 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. `````` Robbert Krebbers committed Oct 19, 2012 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 committed Feb 11, 2020 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. `````` Robbert Krebbers committed Oct 19, 2012 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 `````` Robbert Krebbers committed May 07, 2013 62 `````` | H' : context [ n ] |- _ => var_neq v1 H'; var_neq v2 H'; revert H' `````` Robbert Krebbers committed Oct 19, 2012 63 64 `````` end; revert n v1 v2; `````` Robbert Krebbers committed May 07, 2013 65 `````` match goal with |- ∀ n v1 v2, @?P n v1 v2 => apply (vec_rect2 P) end `````` Robbert Krebbers committed Oct 19, 2012 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. `````` Robbert Krebbers committed May 07, 2013 74 ``````Lemma vec_eq {A n} (v w : vec A n) : (∀ i, v !!! i = w !!! i) → v = w. `````` Robbert Krebbers committed Feb 19, 2013 75 76 ``````Proof. vec_double_ind v w; [done|]. intros n v w IH x y Hi. f_equal. `````` Robbert Krebbers committed Feb 17, 2016 77 78 `````` - apply (Hi 0%fin). - apply IH. intros i. apply (Hi (FS i)). `````` Robbert Krebbers committed Feb 19, 2013 79 80 ``````Qed. `````` Robbert Krebbers committed Sep 20, 2016 81 ``````Instance vec_dec {A} {dec : EqDecision A} {n} : EqDecision (vec A n). `````` Robbert Krebbers committed Oct 19, 2012 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 committed Jan 31, 2017 91 92 `````` let T := type of v in match eval hnf in T with `````` Ralf Jung committed Mar 15, 2017 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 `````` Robbert Krebbers committed Oct 19, 2012 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. *) `````` Robbert Krebbers committed May 02, 2014 106 ``````Ltac inv_all_vec_fin := block_goal; `````` Robbert Krebbers committed Oct 19, 2012 107 108 109 `````` repeat match goal with | v : vec _ _ |- _ => inv_vec v; intros | i : fin _ |- _ => inv_fin i; intros `````` Robbert Krebbers committed May 02, 2014 110 `````` end; unblock_goal. `````` Robbert Krebbers committed Oct 19, 2012 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 := `````` Robbert Krebbers committed May 02, 2014 116 `````` match v with [#] => [] | x ::: v => x :: vec_to_list v end. `````` Robbert Krebbers committed Oct 19, 2012 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. `````` Robbert Krebbers committed Feb 17, 2016 125 ``````Proof. by induction v; f_equal/=. Qed. `````` Robbert Krebbers committed Oct 19, 2012 126 ``````Lemma vec_to_list_of_list {A} (l : list A): vec_to_list (list_to_vec l) = l. `````` Robbert Krebbers committed Feb 17, 2016 127 ``````Proof. by induction l; f_equal/=. Qed. `````` Robbert Krebbers committed Oct 19, 2012 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. `````` Robbert Krebbers committed Feb 19, 2013 130 ``````Lemma vec_to_list_same_length {A B n} (v : vec A n) (w : vec B n) : `````` Robbert Krebbers committed May 02, 2014 131 132 `````` length v = length w. Proof. by rewrite !vec_to_list_length. Qed. `````` Robbert Krebbers committed Oct 19, 2012 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 ? [|???] ?; `````` Robbert Krebbers committed Feb 17, 2016 137 `````` simplify_eq/=; f_equal; eauto. `````` Robbert Krebbers committed Oct 19, 2012 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; `````` Robbert Krebbers committed Feb 17, 2016 143 `````` simplify_eq/=; f_equal; eauto. `````` Robbert Krebbers committed Oct 19, 2012 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. `````` Robbert Krebbers committed May 02, 2014 148 149 `````` induction v; simpl; [by eexists 0%fin|]. destruct IHv as [i ?]. by exists (FS i). `````` Robbert Krebbers committed Oct 19, 2012 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. `````` Robbert Krebbers committed Feb 19, 2013 159 `````` apply vec_to_list_inj2 in H; subst. induction l. simpl. `````` Robbert Krebbers committed Feb 17, 2016 160 161 `````` - eexists 0%fin. simpl. by rewrite vec_to_list_of_list. - destruct IHl as [i ?]. exists (FS i). simpl. intuition congruence. `````` Robbert Krebbers committed Oct 19, 2012 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. `````` Robbert Krebbers committed May 02, 2014 168 ``````Proof. rewrite <-(take_drop i v) at 1. by rewrite vec_to_list_drop_lookup. Qed. `````` Robbert Krebbers committed Oct 19, 2012 169 `````` `````` Jacques-Henri Jourdan committed Jan 31, 2017 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. `````` Robbert Krebbers committed Nov 12, 2012 184 185 ``````Lemma elem_of_vlookup {A n} (v : vec A n) x : x ∈ vec_to_list v ↔ ∃ i, v !!! i = x. `````` Robbert Krebbers committed Oct 19, 2012 186 ``````Proof. `````` Jacques-Henri Jourdan committed Jan 31, 2017 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. `````` Robbert Krebbers committed Oct 19, 2012 190 ``````Qed. `````` Jacques-Henri Jourdan committed Jan 31, 2017 191 `````` `````` Robbert Krebbers committed Oct 19, 2012 192 193 ``````Lemma Forall_vlookup {A} (P : A → Prop) {n} (v : vec A n) : Forall P (vec_to_list v) ↔ ∀ i, P (v !!! i). `````` Robbert Krebbers committed May 07, 2013 194 ``````Proof. rewrite Forall_forall. setoid_rewrite elem_of_vlookup. naive_solver. Qed. `````` Robbert Krebbers committed Oct 19, 2012 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). `````` Robbert Krebbers committed May 07, 2013 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). `````` Robbert Krebbers committed Oct 19, 2012 207 208 ``````Proof. split. `````` Robbert Krebbers committed Feb 17, 2016 209 `````` - vec_double_ind v1 v2; [intros _ i; inv_fin i |]. `````` Robbert Krebbers committed May 02, 2014 210 211 `````` intros n v1 v2 IH a b; simpl. inversion_clear 1. intros i. inv_fin i; simpl; auto. `````` Robbert Krebbers committed Feb 17, 2016 212 `````` - vec_double_ind v1 v2; [constructor|]. `````` Robbert Krebbers committed May 02, 2014 213 `````` intros ??? IH ?? H. constructor. apply (H 0%fin). apply IH, (λ i, H (FS i)). `````` Robbert Krebbers committed Oct 19, 2012 214 215 ``````Qed. `````` Robbert Krebbers committed May 07, 2013 216 ``````(** The function [vmap f v] applies a function [f] element wise to [v]. *) `````` Robbert Krebbers committed Oct 19, 2012 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 committed Feb 11, 2020 221 ``````Proof. by induction v; inv_fin i; eauto. Qed. `````` Robbert Krebbers committed Oct 19, 2012 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. `````` Robbert Krebbers committed Feb 19, 2013 230 ``````Lemma vlookup_zip_with `(f : A → B → C) {n} (v1 : vec A n) (v2 : vec B n) i : `````` Robbert Krebbers committed Oct 19, 2012 231 `````` vzip_with f v1 v2 !!! i = f (v1 !!! i) (v2 !!! i). `````` Dan Frumin committed Feb 11, 2020 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. `````` Robbert Krebbers committed May 07, 2013 238 ``````Lemma vec_to_list_zip_with `(f : A → B → C) {n} (v1 : vec A n) (v2 : vec B n) : `````` Robbert Krebbers committed Feb 19, 2013 239 240 241 `````` vec_to_list (vzip_with f v1 v2) = zip_with f (vec_to_list v1) (vec_to_list v2). Proof. `````` Robbert Krebbers committed May 07, 2013 242 243 `````` revert v2. induction v1; intros v2; inv_vec v2; intros; simpl; [done|]. by rewrite IHv1. `````` Robbert Krebbers committed Feb 19, 2013 244 245 ``````Qed. `````` Robbert Krebbers committed Oct 19, 2012 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 committed Oct 28, 2017 251 `````` | FS i => vec_S_inv _ (λ y v, y ::: vinsert i x v) `````` Robbert Krebbers committed Oct 19, 2012 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. `````` Robbert Krebbers committed Jun 14, 2019 257 `````` `````` Robbert Krebbers committed Oct 19, 2012 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. `````` Robbert Krebbers committed May 07, 2013 266 ``````Lemma vlookup_insert_self {A n} i (v : vec A n) : vinsert i (v !!! i) v = v. `````` Robbert Krebbers committed Feb 17, 2016 267 ``````Proof. by induction v; inv_fin i; intros; f_equal/=. Qed. `````` Ralf Jung committed Mar 15, 2017 268 `````` `````` Robbert Krebbers committed Jun 14, 2019 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. `````` Robbert Krebbers committed Mar 15, 2017 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 committed Mar 15, 2017 297 `````` `````` Robbert Krebbers committed Jun 14, 2019 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. `````` Robbert Krebbers committed Jun 14, 2019 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. `````` Robbert Krebbers committed Mar 15, 2017 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).``````