From f0d2b68d4e29e8cdebb485a6722a38c0420d8e94 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 5 Mar 2020 12:41:03 +0100
Subject: [PATCH] =?UTF-8?q?Function=20`fun=5Fto=5Fvec=20:=20(fin=20n=20?=
 =?UTF-8?q?=E2=86=92=20A)=20=E2=86=92=20vec=20A=20n`.?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 theories/vector.v | 12 ++++++++++++
 1 file changed, 12 insertions(+)

diff --git a/theories/vector.v b/theories/vector.v
index 908eadce..a4343745 100644
--- a/theories/vector.v
+++ b/theories/vector.v
@@ -221,6 +221,18 @@ Proof.
     intros ??? IH ?? H. constructor. apply (H 0%fin). apply IH, (λ i, H (FS i)).
 Qed.
 
+(** Given a function [fin n → A], we can construct a vector. *)
+Fixpoint fun_to_vec {A n} {struct n} : (fin n → A) → vec A n :=
+  match n with
+  | 0 => λ f, [#]
+  | S n => λ f, f 0%fin ::: fun_to_vec (f ∘ FS)
+  end.
+
+Lemma lookup_fun_to_vec {A n} (f : fin n → A) i : fun_to_vec f !!! i = f i.
+Proof.
+  revert f. induction i as [|n i IH]; intros f; simpl; [done|]. by rewrite IH.
+Qed.
+
 (** The function [vmap f v] applies a function [f] element wise to [v]. *)
 Notation vmap := Vector.map.
 
-- 
GitLab