From 3181471024aa69b41cf3c3f3b51705b2d184e3e6 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 24 May 2015 10:10:23 -0700 Subject: [PATCH] feat(library/data/list/basic): add nth_eq_some aux theorem --- library/data/list/basic.lean | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/library/data/list/basic.lean b/library/data/list/basic.lean index 5f21a439d..057ba99eb 100644 --- a/library/data/list/basic.lean +++ b/library/data/list/basic.lean @@ -381,6 +381,14 @@ theorem nth_zero (a : T) (l : list T) : nth (a :: l) 0 = some a theorem nth_succ (a : T) (l : list T) (n : nat) : nth (a::l) (succ n) = nth l n +theorem nth_eq_some : ∀ {l : list T} {n : nat}, n < length l → Σ a : T, nth l n = some a +| [] n h := absurd h !not_lt_zero +| (a::l) 0 h := ⟨a, rfl⟩ +| (a::l) (succ n) h := + have aux : n < length l, from lt_of_succ_lt_succ h, + obtain (r : T) (req : nth l n = some r), from nth_eq_some aux, + ⟨r, by rewrite [nth_succ, req]⟩ + open decidable theorem find_nth [h : decidable_eq T] {a : T} : ∀ {l}, a ∈ l → nth l (find a l) = some a | [] ain := absurd ain !not_mem_nil