Memoized fibonacci #lean #lean4

FibMemoized.lean

-- lean4

import Std.Data.HashMap

structure FibCache where
  cache : Std.HashMap Nat Nat := {}

def fibMemoized : Nat → (StateM FibCache Nat)
| 0 => pure 0
| 1 => pure 1
| n+2 => do
  -- first check cache
  match (← get).cache.find? (n+2) with
  | some f => pure f
  | none =>
    --dbgTrace! s!"Computing fib {n+2}"
    let f2 ← fibMemoized (n+1)
    let f1 ← fibMemoized n
    let f := f1 + f2
    modify <| fun state => { cache := state.cache.insert (n+2) f : FibCache }
    pure f
    
def fib (n : Nat) : Nat := (fibMemoized n).run' {}

/- Sum of first n fibonacci numbers -/
def fibSumAux (n : Nat) : StateM FibCache Nat := do
  let mut s := 0
  for i in [0:n] do
    s := s + (← fibMemoized i)
  return s 

def fibSum (n : Nat) : Nat := (fibSumAux n).run' {}

#eval fib 1000
#eval fibSum 1000

I fixed a left over line of code and removed the partial.

Replaced get...set with modify.