michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

feat(library/data/vector): add vec.is_inhabited theorem

Browse source
This commit is contained in:
Leonardo de Moura 2014-09-07 19:06:03 -07:00
parent da701eb6de
commit 4e2f5572f3
1 changed files with 8 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
library/data/vector.lean
View file

@ -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⁻¹)))