From e1d492b882931a68bf7f84437d3fd003ec5da90a Mon Sep 17 00:00:00 2001 From: Robbert Krebbers Date: Wed, 15 Mar 2017 12:49:13 +0100 Subject: [PATCH] Tweak inhabited proofs for vectors. --- theories/vector.v | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) diff --git a/theories/vector.v b/theories/vector.v index 13ed722..947d663 100644 --- a/theories/vector.v +++ b/theories/vector.v @@ -356,12 +356,12 @@ Qed. Lemma vlookup_insert_self {A n} i (v : vec A n) : vinsert i (v !!! i) v = v. Proof. by induction v; inv_fin i; intros; f_equal/=. Qed. -(* Vectors can be inhabited. *) -Global Instance vec_nil_inh T : Inhabited (vec T 0) := populate [#]. +(** 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. -Global Instance vec_inh T n : Inhabited T → Inhabited (vec T n). -Proof. - intros HT. induction n; [apply _|]. - destruct IHn as [v]. destruct HT as [x]. - exact (populate (x:::v)). -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) := + populate (vreplicate n inhabitant). -- GitLab