f

Implement the following in lean 4. Given a binary operator op, we define the function f : Nat->Nat to be: f 0 =1; f 1=1; f n = op (f (n-1)) (f (n-2)). Write a lean 4 function that, given the op and the natural number n as arguments, computes f n. Additionally, op returns a value wrapped in a monad. Your function should have the signature def f [Monad m] (op: Nat->Nat->(m Nat)) (n: Nat): (m Nat) :=

Function Signature

def f[Monad m] (op: Nat->Nat->(m Nat)) (n: Nat): (m Nat)

Theorem Signature

theorem f_base (op : Nat → Nat → Id Nat) :
    (f op 0 = pure 1) ∧  (f op 1 = pure 1)

Additional Theorem Signature

theorem f_recursive (op : Nat → Nat → Id Nat) (n : Nat) : f op (n+2) =do {op (←  f op (n+1)) (←  f op n) }

View All Submissions

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