Decidable function that recognize fibonacci numbers

Stream: new members

[Marcelo Fornet]

I want to create decidable function that recognize if a number is part of the fibonacci sequence or not, and I want to prove the function is correct. So far this is what I have:

import Mathlib.Data.Nat.Fib.Basic

def isFib (n : ℕ) : Prop :=
  ∃ (k : ℕ), Nat.fib k = n

partial def isFibDecidable (n : ℕ) : Bool :=
  iter n 1 2
  where
    iter n a b :=
      if a = n then
        true
      else if a > n then
        false
      else
        iter n b (a + b)

theorem isFibDecidableCorrect (n : ℕ) : isFibDecidable n = true ↔ isFib n := by
  sorry

• 1) How to provide a termination proof for isFibDecidable if I remove the partial keyword?
• 2) I'm not sure where to begin the proof for isFibDecidableCorrect since I need to deal with a recursive function and if/then/else statement.

[Eric Wieser]

You might find it easier to skip the bool function and jump straight to showing DecidablePred isFib

[Eric Wieser]

Where you use .isFalse and .isTrue instead of false and true

[Marcelo Fornet]

Just for the sake of testing I got to this point

theorem isFibIsDecidable : DecidablePred isFib := by
  intro n
  cases n with
  | zero => exact Decidable.isTrue ⟨0, rfl⟩
  | succ n => cases n with
    | zero => exact Decidable.isTrue ⟨1, rfl⟩
    | succ n => sorry

I guess that if a prove the following lemma

lemma isNotFib (n : ℕ) (h : ∃ k, Nat.fib k < n ∧ n < Nat.fib (k + 1)) : ¬ isFib n := by
  sorry

then I can loop through all values of k until either I found a value such that it is fib, or that it triggers the lemma isNotFib.

The main question now is how can I loop (or do recursion) inside the theorem isFibIsDecidable

[Eric Wieser]

It should be a def not a theorem; and you can write it as

def isFibIsDecidable : DecidablePred isFib
  | 0 => Decidable.isTrue ⟨0, rfl⟩
  | 1 => Decidable.isTrue ⟨1, rfl⟩
  | (n + 2) => sorry  -- use `isFibIsDecidable n` or similar as necessary

[Eric Wieser]

Which is to say; you can recurse in exactly the same way you did in isFibDecidable , you're just replacing Bool with Decidable (isFib n)

[Mark Fischer]

The chapter on induction_and_recursion in theorem proving in lean should be helpfull here too.

[Matt Diamond]

one approach you could take is to prove ∀ n, ∃ k, Nat.fib k ≥ n and use docs#Nat.find to find the least such value of k for a given n, and then check whether or not fib k equals n