From df7bc187e4cff19f717771223b7ea56db117cad0 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Tue, 1 Sep 2015 12:19:59 +0200 Subject: Adding a proof of eta on Vector.t of non-zero size. --- theories/Vectors/VectorSpec.v | 10 ++++++++++ 1 file changed, 10 insertions(+) (limited to 'theories/Vectors') diff --git a/theories/Vectors/VectorSpec.v b/theories/Vectors/VectorSpec.v index 7f4228dd6..46b537737 100644 --- a/theories/Vectors/VectorSpec.v +++ b/theories/Vectors/VectorSpec.v @@ -22,6 +22,16 @@ Definition cons_inj {A} {a1 a2} {n} {v1 v2 : t A n} with | eq_refl => conj eq_refl eq_refl end. +Lemma eta {A} {n} (v : t A (S n)) : v = hd v :: tl v. +Proof. + change + (match S n with + | 0 => fun v : t A 0 => v = v + | S n => fun v => v = hd v :: tl v + end v). + destruct v; reflexivity. +Defined. + (** Lemmas are done for functions that use [Fin.t] but thanks to [Peano_dec.le_unique], all is true for the one that use [lt] *) -- cgit v1.2.3