Linear-Time Fibonacci

Implement the Finbonacci function using a linear number of operations.

Instead of using addition, use the monadic function op that is passed in as input argument.

Function Signature

import Mathlib.Data.Nat.Defs
-- Original recursive implementation
def f [Monad m] (op : Nat → Nat → m Nat) (n : Nat) : m Nat :=
  match n with
  | 0 => pure 1
  | 1 => pure 1
  | n + 2 =>
    do
      let x ← f op (n + 1)
      let y ← f op n
      op x y

-- Linear-time implementation of f
def fLinear [Monad m] (op : Nat → Nat → m Nat) (n : Nat) : m Nat 

Theorem Signature

theorem fLinear_correct (op : Nat → Nat → Id Nat) (n : Nat)  :
  (fLinear op n) =f op n 

Additional Theorem Signature

structure State (s α : Type) where
  run : s → (α × s)

instance : Monad (State s) where
  pure x := ⟨fun s => (x, s)⟩
  bind ma f := ⟨fun s =>
    let (a, s') := ma.run s
    (f a).run s'⟩


def increment : State Nat Unit :=
  ⟨fun s => ((), s + 1)⟩

def countingOp (a b : Nat) : State Nat Nat := do
  increment
  pure (a + b)

theorem fLinear_op_calls (n : Nat):
 (cnt:Nat)->
  ((fLinear countingOp n).run cnt |>.2) = match n with
  | 0 => cnt
  | 1 => cnt
  | n' + 2 => n'+1+cnt

View All Submissions

Please log in or register to submit a solution for this challenge.