From be15c746dc96479c10b0c69d37b5d3384a03be37 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 14 Jun 2019 08:00:01 +0200
Subject: [PATCH] Add lemma `vec_to_list_replicate`.
---
theories/vector.v | 4 ++++
1 file changed, 4 insertions(+)
diff --git a/theories/vector.v b/theories/vector.v
index 3607efbe..c81fa660 100644
--- a/theories/vector.v
+++ b/theories/vector.v
@@ -260,6 +260,10 @@ with value [x]. *)
Fixpoint vreplicate {A} (n : nat) (x : A) : vec A n :=
match n with 0 => [#] | S n => x ::: vreplicate n x end.
+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.
+
(* 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) :=
--
GitLab