diff options
| -rw-r--r-- | lazy.lean | 90 | ||||
| -rw-r--r-- | monad.lean | 12 | ||||
| -rw-r--r-- | native-decide.lean | 7 |
3 files changed, 71 insertions, 38 deletions
@@ -1,3 +1,27 @@ +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! @@ -30,56 +54,46 @@ -- -- #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 -inductive LazyList (α : Type u) where - | nil - | cons : α → Thunk (LazyList α) → LazyList α - -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 - -unsafe def ints := LazyList.cons 1.0 <| ints.map (· + 1) - -#eval ints.take 10 - --- Doesn't work? --- unsafe def integrate s (c : Float) := LazyList.cons c <| LazyList.zipWith (· / ·) s ints - -notation s "integrate" c => LazyList.cons c <| LazyList.zipWith (· / ·) s ints +-- partial def ints _ := LazyList.cons 1.0 <| (ints ()).map (· + 1) -unsafe def pows := LazyList.cons 1.0 <| LazyList.zipWith (· + ·) pows pows +-- #eval (ints ()).take 10 -#eval pows.take 10 +-- def integrate (s : Unit → LazyList Float) (c : Float) := LazyList.cons c <| LazyList.zipWith (· / ·) (s ()) (ints ()) -unsafe def expSeries := expSeries integrate 1.0 +-- partial def expSeries _ := integrate expSeries 1.0 -#eval expSeries.take 10 +-- #eval (expSeries ()).take 10 -def evalAt n (s : LazyList Float) x := (s.take n).foldr (λ a acc => a + acc * x) 0 +-- def evalAt n (s : LazyList Float) x := (s.take n).foldr (λ a acc => a + acc * x) 0 -mutual - unsafe def sine := cosine integrate 0.0 - unsafe def cosine := (sine integrate -1.0).map (-·) -end +-- mutual +-- partial def sine _ := integrate cosine 0.0 +-- partial def cosine _ := (integrate sine (-1.0)).map (-·) +-- end -#eval sine.take 10 +-- #eval (sine ()).take 10 -#eval evalAt 1000 sine 2.0 -#eval 2.0.sin +-- #eval evalAt 1000 (sine ()) 2.0 +-- #eval 2.0.sin -- inductive LazyList (α : Type u) where -- | nil diff --git a/monad.lean b/monad.lean new file mode 100644 index 0000000..ce747ae --- /dev/null +++ b/monad.lean @@ -0,0 +1,12 @@ +def mapM [Monad m] (f : α → m β) : List α → m (List β) + | [] => pure [] + | x :: xs => + f x >>= fun hd => + mapM f xs >>= fun tl => + pure (hd :: tl) + + +#eval mapM (m := Id) (· + 1) [1, 2, 3, 4, 5] + +#eval show IO Unit from IO.println "hello world" +#reduce show IO Unit from IO.println "hello world" diff --git a/native-decide.lean b/native-decide.lean new file mode 100644 index 0000000..ac0c0ac --- /dev/null +++ b/native-decide.lean @@ -0,0 +1,7 @@ +example : False := by + let getHeartbeats (x : Nat) : Nat := + let .ok _ state := IO.mkRef x () -- ensure `x` is not eliminated + let .ok val state := IO.getNumHeartbeats state + val + have : getHeartbeats 0 ≠ getHeartbeats (0 + 1 - 1) := by native_decide + simp [getHeartbeats] at this |