Some random stuff I guessHEADmaster

3 files changed, 71 insertions, 38 deletions

diff --git a/lazy.lean b/lazy.lean
index 3d13537..319e2f2 100644
--- a/lazy.lean
+++ b/lazy.lean
@@ -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