From 4e2f5572f3f578409b91ea56cdca3f1faf38e1d6 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 7 Sep 2014 19:06:03 -0700 Subject: [PATCH] feat(library/data/vector): add vec.is_inhabited theorem --- library/data/vector.lean | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/library/data/vector.lean b/library/data/vector.lean index 259e3c441..a431a0b94 100644 --- a/library/data/vector.lean +++ b/library/data/vector.lean @@ -27,6 +27,14 @@ namespace vec (Hcons : ∀(x : T) {n : ℕ} (w : vec T n), C (succ n) (cons x w)) : C n v := rec_on v Hnil (take x n v IH, Hcons x v) + theorem is_inhabited [instance] [protected] (A : Type) (H : inhabited A) (n : nat) : inhabited (vec A n) := + nat.rec_on n + (inhabited.mk (@vec.nil A)) + (λ (n : nat) (iH : inhabited (vec A n)), + inhabited.destruct H + (λa, inhabited.destruct iH + (λv, inhabited.mk (vec.cons a v)))) + theorem case_zero_lem [private] {C : vec T 0 → Type} {n : ℕ} (v : vec T n) (Hnil : C nil) : ∀ H : n = 0, C (cast (congr_arg (vec T) H) v) := rec_on v (take H : 0 = 0, (eq.rec Hnil (cast_eq _ nil⁻¹)))