Update after custom sorry video

MetaExamples/CustomSorry.lean

@@ -17,3 +17,27 @@ A higly simplified view of a tactic is the following:
 
 #check getGoals -- TacticM (List MVarId)
 #check setGoals -- List MVarId → TacticM Unit
+
+elab "evil" : tactic => do
+  setGoals []
+
+-- example : 1 ≤ 34 := by
+--   evil
+
+#check sorryAx
+
+elab "todo" s:str :tactic =>
+  withMainContext do
+  logInfo m!"Message: {s}"
+  let target ← getMainTarget
+  let sorryExpr ←
+    mkAppM ``sorryAx #[target, mkConst ``false]
+  closeMainGoal `todo sorryExpr
+
+example : 3 ≤ 15 := by
+  todo "Figure out what I should be doing."
+
+example (α : Type) : α  := by
+  revert α
+  intro a
+  todo "Metaprogramming can be hard"

MetaExamples/Fib.lean

@@ -0,0 +1,11 @@
+/-!
+## Naive Fibonacci numbers
+
+The following definition is infamously slow as values are repeatedly computed
+-/
+def fib : Nat → Nat
+| 0 => 1
+| 1 => 1
+| k + 2 => fib k + fib (k + 1)
+
+-- #eval fib 32

MetaExamples/FibM.lean

@@ -0,0 +1,32 @@
+import Batteries
+import MetaExamples.State
+open Batteries State
+
+/-!
+## The `FibM` State Monad
+-/
+abbrev FibM := State (HashMap Nat Nat)
+/-!
+* We have a background state that is a `HashMap Nat Nat`, to store values already computed.
+* When computing a term of type `FibM α` we can `get` and use the state and also `set` or `update` it.
+* Future computations automatically use the updated state.
+* Using this we can efficiently compose.
+-/
+
+
+def fibM (n: Nat) : FibM Nat := do
+  let s ← get
+  match s.find? n with
+  | some y => return y
+  | none =>
+    match n with
+    | 0 => return 1
+    | 1 =>  return 1
+    | k + 2 => do
+      let f₁ ← fibM k
+      let f₂ ← fibM (k + 1)
+      let sum := f₁ + f₂
+      update fun m => m.insert n sum
+      return sum
+
+#eval fibM 3245

MetaExamples/State.lean

@@ -0,0 +1,29 @@
+/-!
+# State Monads
+
+* If `s` is a type, then we have a **State Monad** `State s`.
+* What this means is that if `α` is a type, then `State s α` is a type so that a term of this type:
+  - takes an initial state as input
+  - returns a term of type `α`,
+  - and a final state.
+* Thus, a term of type `State s α` is essentially a function `s → α × s`.
+-/
+structure State (s α: Type) where
+  run : s → α × s
+
+namespace State
+def get : State s s := ⟨fun s => (s, s)⟩
+def update (f: s → s) : State s Unit := ⟨fun s => ((), f s)⟩
+
+def run'[Inhabited s](x: State s α) (s: s := default) : α := (x.run s).1
+end State
+
+instance : Monad (State s) where
+  pure x := ⟨fun s => (x, s)⟩
+  bind x f := ⟨fun s =>
+    let (a, s') := x.run s
+    (f a).run s'⟩
+open State
+
+instance [rep : Repr α][Inhabited s] : Repr (State s α) :=
+  ⟨fun mx n => rep.reprPrec mx.run' n⟩