/Lazy.lean at 3e2e3f47cff6a832e37e076937834dca36433d04

inductive LazyList (α : Type u)
  | nil
  | cons : α → Thunk (LazyList α) → LazyList α

def LazyList.map (f: α → β) : LazyList α → LazyList β
  | nil => nil
  | cons x xs => cons (f x) <| xs.get.map f

def LazyList.length {α} : LazyList α → Nat
  | .nil => 0
  | .cons a b => b.get.length + 1

@[simp]
theorem LazyList.length_map {α β} (l : LazyList α) (f : α → β) : (l.map f).length = l.length := by
  match l with
  | .nil => simp [LazyList.length, LazyList.map]
  | .cons x xs => simp only [LazyList.length, LazyList.map, Thunk.get]; rw [LazyList.length_map]

theorem not_exists_ints : ¬∃ ints : Unit → LazyList Float, ints = (fun _ => LazyList.cons 1.0 <| (ints ()).map (· + 1)) := by
  intro ⟨ints, h⟩
  have ss := congrArg (fun f => (f ()).length) h
  simp [LazyList.length, Thunk.get] at ss


-- Want:
-- def ints := LazyList.cons 1 <| ints.map (· + 1)
-- Problem: This is recursive, bad!
-- Idea: use dependent types to encode promise that recursion won't exceed certain depth? Bake that into cons
-- Problem: memoization?
-- Like let's say I take 10 then take 20, the initial elements will have different types
-- Well let's try implementing this first

-- inductive Vect (α : Type u) : Nat → Type u where
--   | nil : Vect α 0
--   | cons : α → Vect α n → Vect α (n + 1)

-- def Vect.map (f : α → β) : Vect α n → Vect β n
--   | nil => nil
--   | cons x xs => cons (f x) <| xs.map f

-- -- def Vect.map (f : α → β) : Vect α (n + 1) → Vect β n :=
-- --   match n with
-- --   | 0 => λ _ => nil
-- --   | _ + 1 => λ v => match v with
-- --     | cons x xs => cons (f x) <| xs.map f

-- def a := Vect.cons 1 (Vect.cons 2 Vect.nil)

-- #eval a.map (· + 1)

-- def ints (n : Nat) : Vect Nat n
--   | 0 => Vect.nil
--   | n + 1 => Vect.cons 1 <| (ints n).map (· + 1)

-- -- #eval ints 10

-- inductive LazyList (α : Type u)
--   | nil
--   | cons : α → Thunk (LazyList α) → LazyList α
-- deriving Inhabited

-- def LazyList.take : Nat → LazyList α → List α
--   | 0, _ => .nil
--   | _, nil => .nil
--   | n + 1, cons x xs => .cons x <| xs.get.take n

-- def LazyList.map (f: α → β) : LazyList α → LazyList β
--   | nil => nil
--   | cons x xs => cons (f x) <| xs.get.map f

-- def LazyList.zipWith (f: α → β → γ) : LazyList α → LazyList β → LazyList γ
--   | nil, _ => nil
--   | _, nil => nil
--   | cons x xs, cons y ys => cons (f x y) <| zipWith f xs.get ys.get

-- partial def ints _ := LazyList.cons 1.0 <| (ints ()).map (· + 1)

-- #eval (ints ()).take 10

-- def integrate (s : Unit → LazyList Float) (c : Float) := LazyList.cons c <| LazyList.zipWith (· / ·) (s ()) (ints ())

-- partial def expSeries _ := integrate expSeries 1.0

-- #eval (expSeries ()).take 10

-- def evalAt n (s : LazyList Float) x := (s.take n).foldr (λ a acc => a + acc * x) 0

-- mutual
--   partial def sine _ := integrate cosine 0.0
--   partial def cosine _ := (integrate sine (-1.0)).map (-·)
-- end

-- #eval (sine ()).take 10

-- #eval evalAt 1000 (sine ()) 2.0
-- #eval 2.0.sin

-- inductive LazyList (α : Type u) where
--   | nil
--   | cons : α → Thunk (LazyList α) → LazyList α
--   | delayed : Thunk (LazyList α) → LazyList α

-- def LazyList.take : Nat → LazyList α → List α
--   | 0, _ => .nil
--   | _, .nil => .nil
--   | n + 1, .cons x xs => .cons x <| xs.get.take n
--   | n + 1, .delayed xs => xs.get.take n

-- def LazyList.map (f: α → β) : LazyList α → LazyList β
--   | .nil => .nil
--   | .cons x xs => .cons (f x) <| xs.get.map f
--   | .delayed xs => xs.get.map f

-- def LazyList.zipWith (f: α → β → γ) : LazyList α → LazyList β → LazyList γ
--   | .nil, _ => .nil
--   | _, .nil => .nil
--   | .cons x xs, .cons y ys => .cons (f x y) <| zipWith f xs.get ys.get
--   | .delayed xs, y => zipWith f xs.get y
--   | x, .delayed ys => zipWith f x ys.get

-- unsafe def ints := LazyList.cons 1 <| ints.map (· + 1)

-- #eval ints.take 10

-- def hi := LazyList.delayed LazyList

-- unsafe def integrate s c := LazyList.cons c <| LazyList.delayed <| LazyList.zipWith (· / ·) s ints

-- unsafe def expSeries := integrate expSeries 1

-- #eval expSeries.take 10

-- inductive LazyList (α : Type u) where
--   | nil
--   | cons : α → LazyList α → LazyList α
--   | delayed : Thunk (LazyList α) → LazyList α

-- unsafe def LazyList.map (f: α → β) : LazyList α → Thunk (LazyList β)
--   | nil => Thunk.pure nil
--   | cons x xs => cons (f x) <| delayed <| xs.map f
--   | delayed xs => xs.bind <| λ l => l.map f

-- -- def LazyList.take : Nat → LazyList α → LazyList α
-- --   | 0, _ => .nil
-- --   | _, .nil => .nil
-- --   | n + 1, .cons x xs => .cons x <| .delayed <| take n xs
-- --   | n + 1, .delayed xs => .delayed <| take (n + 1) xs.get

-- def LazyList.take : Nat → LazyList α → List α
--   | 0, _ => .nil
--   | _, .nil => .nil
--   | n + 1, .cons x xs => .cons x <| xs.take n
--   | n + 1, .delayed xs => take (n + 1) xs.get

-- -- def LazyList.toList : LazyList α → List α
-- --   | .nil => []
-- --   | .cons x xs => x :: xs.toList
-- --   | .delayed xs => xs.get.toList

-- unsafe def ints := LazyList.cons 1 <| LazyList.delayed <| ints.map (· + 1)

-- -- #eval ints.take 10



-- inductive LazyList (α : Type u) : Type u
--   /-- The empty lazy list. -/
--   | nil : LazyList α
--   /-- Construct a lazy list from an element and a tail inside a thunk. -/
--   | cons (hd : α) (tl : Thunk <| LazyList α) : LazyList α


-- namespace LazyList


-- instance : Inhabited (LazyList α) :=
--   ⟨nil⟩

-- /-- The singleton lazy list.  -/
-- def singleton : α → LazyList α
--   | a => cons a <| Thunk.pure nil

-- /-- Constructs a lazy list from a list. -/
-- def ofList : List α → LazyList α
--   | [] => nil
--   | h :: t => cons h (ofList t)

-- /-- Converts a lazy list to a list.
-- If the lazy list is infinite,
-- then this function does not terminate.
-- -/
-- def toList : LazyList α → List α
--   | nil => []
--   | cons h t => h :: toList (t.get)

-- /-- Returns the first element of the lazy list,
-- or `default` if the lazy list is empty.
-- -/
-- def headI [Inhabited α] : LazyList α → α
--   | nil => default
--   | cons h _ => h

-- /-- Removes the first element of the lazy list.
-- -/
-- def tail : LazyList α → LazyList α
--   | nil => nil
--   | cons _ t => t.get

-- /-- Appends two lazy lists.  -/
-- def append : LazyList α → Thunk (LazyList α) → LazyList α
--   | nil, l => l.get
--   | cons h t, l => cons h (append (t.get) l)

-- /-- Maps a function over a lazy list. -/
-- def map (f : α → β) : LazyList α → LazyList β
--   | nil => nil
--   | cons h t => cons (f h) (map f t.get)

-- /-- Maps a binary function over two lazy list.
-- Like `LazyList.zip`, the result is only as long as the smaller input.
-- -/
-- def map₂ (f : α → β → δ) : LazyList α → LazyList β → LazyList δ
--   | nil, _ => nil
--   | _, nil => nil
--   | cons h₁ t₁, cons h₂ t₂ => cons (f h₁ h₂) (Thunk.pure (map₂ f t₁.get t₂.get))

-- /-- Zips two lazy lists. -/
-- def zip : LazyList α → LazyList β → LazyList (α × β) :=
--   map₂ Prod.mk

-- /-- The monadic join operation for lazy lists. -/
-- def join : LazyList (LazyList α) → LazyList α
--   | nil => nil
--   | cons h t => append h (join (t.get))

-- /-- The list containing the first `n` elements of a lazy list.  -/
-- def take : Nat → LazyList α → List α
--   | 0, _ => []
--   | _, nil => []
--   | a + 1, cons h t => h :: take a (t.get)

-- /-- The lazy list of all elements satisfying the predicate.
-- If the lazy list is infinite and none of the elements satisfy the predicate,
-- then this function will not terminate.
-- -/
-- def filter (p : α → Prop) [DecidablePred p] : LazyList α → LazyList α
--   | nil => nil
--   | cons h t => if p h then cons h (filter p t.get) else filter p (t.get)

-- /-- The nth element of a lazy list as an option (like `List.get?`). -/
-- def get? : LazyList α → Nat → Option α
--   | nil, _ => none
--   | cons a _, 0 => some a
--   | cons _ l, n + 1 => get? (l.get) n

-- /-- The infinite lazy list `[x, f x, f (f x), ...]` of iterates of a function.
-- This definition is partial because it creates an infinite list.
-- -/
-- partial def iterates (f : α → α) : α → LazyList α
--   | x => cons x (iterates f (f x))

-- /-- The infinite lazy list `[i, i+1, i+2, ...]` -/
-- partial def iota (i : Nat) : LazyList Nat :=
--   iterates Nat.succ i

-- end LazyList

-- unsafe def ints := LazyList.cons 1 (ints.map λ x => x + 1)

-- #eval ints.take 13

-- unsafe def integrate f c := LazyList.cons c <| LazyList.map₂ (λ a b => a / b) f ints

-- unsafe def expSeries := integrate expSeries 1

-- -- #eval expSeries.take 13



-- structure FibStream : Type where
--   x₁ : ℕ
--   x₂ : ℕ
-- deriving Repr

-- namespace FibStream
--   def next? (s : FibStream) : Option (ℕ × FibStream) :=
--     match s with
--     | ⟨x₁, x₂⟩ =>
--       let x₃ := x₁ + x₂
--       some (x₃, ⟨x₂, x₃⟩)

--   instance : Stream FibStream ℕ where
--     next? := next?

--   def init : FibStream := ⟨0, 1⟩

-- end FibStream

-- namespace Stream
--   variable {Stream_α : Type} {α : Type} [Stream Stream_α α]

--   def take (n : Nat) (s : Stream_α) : List α :=
--     match n with
--     | 0   => []
--     | n+1 =>
--       let next? := Stream.next? s
--       match next? with
--       | none => []
--       | some (next, s') => next :: take n s'

--   structure Filter (Stream_α : Type) [Stream Stream_α α] where
--     stream : Stream_α
--     filter_by : α → Bool


--   partial def Filter.next? (s : Filter Stream_α) : Option (α × Filter Stream_α) :=
--     let next? := Stream.next? s.stream
--     match next? with
--     | none => none
--     | some (next, s') =>
--       let next_filtered : Filter Stream_α := { stream := s', filter_by := s.filter_by : Filter Stream_α }
--       if s.filter_by next then
--         some (next, next_filtered)
--       else
--         Filter.next? next_filtered

--   def filter (p : α → Bool) (s : Stream_α) : Filter Stream_α :=
--     { stream := s, filter_by := p }

--   instance : Stream (Filter Stream_α) α where
--     next? := Filter.next?
-- end Stream


-- -- def natOrStringThree (b : Bool) : if b then Nat else String :=
-- --   match b with
-- --   | true => (3 : Nat)
-- --   | false => "three"