From 85f50214eda497b4c5c82cbd9528cbf2248e6b99 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 24 Feb 2020 08:35:42 +0100
Subject: [PATCH] Prove lemma `list_to_vec_to_list`.

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

diff --git a/theories/vector.v b/theories/vector.v
index fd63b07a..63bd1856 100644
--- a/theories/vector.v
+++ b/theories/vector.v
@@ -142,6 +142,13 @@ Proof.
   revert w. induction v; intros w; inv_vec w; intros;
     simplify_eq/=; f_equal; eauto.
 Qed.
+Lemma list_to_vec_to_list {A n} (v : vec A n) :
+  list_to_vec (vec_to_list v) = eq_rect _ _ v _ (eq_sym (vec_to_list_length v)).
+Proof.
+  apply vec_to_list_inj2. rewrite vec_to_list_to_vec.
+  by destruct (eq_sym (vec_to_list_length v)).
+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.
-- 
GitLab