### Tweak inhabited proofs for vectors.

parent cb021200
Pipeline #4063 passed with stage
in 2 minutes and 43 seconds
 ... @@ -356,12 +356,12 @@ Qed. ... @@ -356,12 +356,12 @@ Qed. Lemma vlookup_insert_self {A n} i (v : vec A n) : vinsert i (v !!! i) v = v. 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. Proof. by induction v; inv_fin i; intros; f_equal/=. Qed. (* Vectors can be inhabited. *) (** The function [vreplicate n x] generates a vector with length [n] of elements Global Instance vec_nil_inh T : Inhabited (vec T 0) := populate [#]. 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). (* Vectors can be inhabited. *) Proof. Global Instance vec_0_inhabited T : Inhabited (vec T 0) := populate [#]. intros HT. induction n; [apply _|]. Global Instance vec_inhabited `{Inhabited T} n : Inhabited (vec T n) := destruct IHn as [v]. destruct HT as [x]. populate (vreplicate n inhabitant). exact (populate (x:::v)). Qed.
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment