chore(data/stream): dedup take and approx (#10525)

`stream.take` and `stream.approx` were propositionally equal. Merge
them into one function `stream.take`; the definition comes from the old `stream.approx`.

src/data/stream/basic.lean

@@ -5,7 +5,6 @@ Authors: Gabriel Ebner, Simon Hudon
 -/
 import tactic.ext
 import data.stream.init
-import data.list.range
 
 /-!
 # Additional instances and attributes for streams
@@ -17,16 +16,12 @@ instance {α} [inhabited α] : inhabited (stream α) :=
 ⟨stream.const (default _)⟩
 
 namespace stream
-open nat
-
-lemma length_take {α} (s : stream α) (n : ℕ) : (take s n).length = n :=
-by simp [take]
 
 /-- Use a state monad to generate a stream through corecursion -/
 def corec_state {σ α} (cmd : state σ α) (s : σ) : stream α :=
 stream.corec prod.fst (cmd.run ∘ prod.snd) (cmd.run s)
 
 @[simp] lemma head_drop {α} (a : stream α) (n : ℕ) : (a.drop n).head = a.nth n :=
-by simp only [stream.drop, stream.head, zero_add]
+by simp only [stream.drop, stream.head, nat.zero_add]
 
 end stream

src/data/stream/defs.lean

@@ -96,13 +96,10 @@ def append_stream : list α → stream α → stream α
 
 infix `++ₛ`:65 := append_stream
 
-def approx : nat → stream α → list α
+/-- `take n s` returns a list of the `n` first elements of stream `s` -/
+def take : ℕ → stream α → list α
 | 0     s := []
-| (n+1) s := list.cons (head s) (approx n (tail s))
-
-/-- `take s n` returns a list of the `n` first elements of stream `s` -/
-def take {α} (s : stream α) (n : ℕ) : list α :=
-(list.range n).map s
+| (n+1) s := list.cons (head s) (take n (tail s))
 
 /-- An auxiliary definition for `stream.cycle` corecursive def -/
 protected def cycle_f : α × list α × α × list α → α
@@ -125,7 +122,6 @@ corec_on (l, s)
   (λ ⟨a, b⟩, a)
   (λ p, match p with (l', s') := (l' ++ [head s'], tail s') end)
 
-
 def inits (s : stream α) : stream (list α) :=
 inits_core [head s] (tail s)
 

src/data/stream/init.lean

@@ -387,33 +387,36 @@ theorem mem_append_stream_left : ∀ {a : α} {l : list α} (s : stream α), a 
     (λ (aeqb : a = b), exists.intro 0 aeqb)
     (λ (ainl : a ∈ l), mem_cons_of_mem b (mem_append_stream_left s ainl))
 
-theorem approx_zero (s : stream α) : approx 0 s = [] := rfl
+@[simp] theorem take_zero (s : stream α) : take 0 s = [] := rfl
 
-theorem approx_succ (n : nat) (s : stream α) :
-  approx (succ n) s = head s :: approx n (tail s) := rfl
+@[simp] theorem take_succ (n : nat) (s : stream α) :
+  take (succ n) s = head s :: take n (tail s) := rfl
 
-theorem nth_approx : ∀ (n : nat) (s : stream α), list.nth (approx (succ n) s) n = some (nth n s)
+@[simp] theorem length_take (n : ℕ) (s : stream α) : (take n s).length = n :=
+by induction n generalizing s; simp *
+
+theorem nth_take_succ : ∀ (n : nat) (s : stream α), list.nth (take (succ n) s) n = some (nth n s)
 | 0     s := rfl
-| (n+1) s := begin rw [approx_succ, add_one, list.nth, nth_approx], refl end
+| (n+1) s := begin rw [take_succ, add_one, list.nth, nth_take_succ], refl end
 
-theorem append_approx_drop :
-  ∀ (n : nat) (s : stream α), append_stream (approx n s) (drop n s) = s :=
+theorem append_take_drop :
+  ∀ (n : nat) (s : stream α), append_stream (take n s) (drop n s) = s :=
 begin
   intro n,
   induction n with n' ih,
   { intro s, refl },
-  { intro s, rw [approx_succ, drop_succ, cons_append_stream, ih (tail s), stream.eta] }
+  { intro s, rw [take_succ, drop_succ, cons_append_stream, ih (tail s), stream.eta] }
 end
 
 -- Take theorem reduces a proof of equality of infinite streams to an
 -- induction over all their finite approximations.
-theorem take_theorem (s₁ s₂ : stream α) : (∀ (n : nat), approx n s₁ = approx n s₂) → s₁ = s₂ :=
+theorem take_theorem (s₁ s₂ : stream α) : (∀ (n : nat), take n s₁ = take n s₂) → s₁ = s₂ :=
 begin
   intro h, apply stream.ext, intro n,
   induction n with n ih,
-  { have aux := h 1, simp [approx] at aux, exact aux },
+  { have aux := h 1, simp [take] at aux, exact aux },
   { have h₁ : some (nth (succ n) s₁) = some (nth (succ n) s₂),
-    { rw [← nth_approx, ← nth_approx, h (succ (succ n))] },
+    { rw [← nth_take_succ, ← nth_take_succ, h (succ (succ n))] },
     injection h₁ }
 end
 
@@ -473,11 +476,11 @@ begin
   { intros l s, rw [nth_succ, inits_core_eq, tail_cons, ih, inits_core_eq (a::l) s], refl }
 end
 
-theorem nth_inits : ∀ (n : nat) (s : stream α), nth n (inits s) = approx (succ n) s  :=
+theorem nth_inits : ∀ (n : nat) (s : stream α), nth n (inits s) = take (succ n) s  :=
 begin
   intro n, induction n with n' ih,
   { intros, refl },
-  { intros, rw [nth_succ, approx_succ, ← ih, tail_inits, inits_tail, cons_nth_inits_core] }
+  { intros, rw [nth_succ, take_succ, ← ih, tail_inits, inits_tail, cons_nth_inits_core] }
 end
 
 theorem inits_eq (s : stream α) : inits s = [head s] :: map (list.cons (head s)) (inits (tail s)) :=
@@ -491,8 +494,8 @@ end
 theorem zip_inits_tails (s : stream α) : zip append_stream (inits s) (tails s) = const s :=
 begin
   apply stream.ext, intro n,
-  rw [nth_zip, nth_inits, nth_tails, nth_const, approx_succ,
-      cons_append_stream, append_approx_drop, stream.eta]
+  rw [nth_zip, nth_inits, nth_tails, nth_const, take_succ,
+      cons_append_stream, append_take_drop, stream.eta]
 end
 
 theorem identity (s : stream α) : pure id ⊛ s = s := rfl