using Nat.brecOn to define the fibonacci function

Stream: general

[Bulhwi Cha]

namespace Nat

def fib : Nat → Nat
  | 0   => 1
  | 1   => 1
  | n+2 => fib (n+1) + fib n

noncomputable def fib' (n : Nat) : Nat :=
  Nat.brecOn n aux
where
  aux (n : Nat) (prev : Nat.below n) : Nat :=
    match n with
    | 0 => 1
    | 1 => 1
    | _ + 2 => prev.1 + prev.2.1

end Nat

It's not easy for me to prove that fib = fib'. Do you think these two functions are the same?

[Bulhwi Cha]

I wrote the above code while reviewing Section Structural Recursion and Induction of #tpil.

[Bulhwi Cha]

I think I know how to prove it. Edit: here's the proof:

namespace Nat

def fib : Nat → Nat
  | 0   => 1
  | 1   => 1
  | n+2 => fib (n+1) + fib n

noncomputable def fib' (n : Nat) : Nat :=
  Nat.brecOn n aux
where
  aux (n : Nat) (prev : Nat.below n) : Nat :=
    match n with
    | 0 => 1
    | 1 => 1
    | _ + 2 => prev.1 + prev.2.1

theorem brecOn.go_succ_succ {motive : Nat → Sort u} (n : Nat)
    (F : (t : Nat) → Nat.below (motive := motive) t → motive t) :
    Nat.brecOn.go (n + 2) F = ⟨F (n + 2) (Nat.brecOn.go (n + 1) F), F (n + 1) (Nat.brecOn.go n F),
      Nat.brecOn.go n F⟩ :=
  rfl

theorem fib'_succ_succ (n : Nat) : fib' (n + 2) = fib' (n + 1) + fib' n := by
  unfold fib' Nat.brecOn
  rw [brecOn.go_succ_succ, fib'.aux]

theorem fib_eq_fib' (n : Nat) : fib n = fib' n := by
  match n with
  | 0 => rfl
  | 1 => rfl
  | k + 2 => rw [fib, fib'_succ_succ, fib_eq_fib' k, fib_eq_fib' (k + 1)]

end Nat

[Jovan Gerbscheid]

The following works as well

theorem fib_eq_fib' (n : Nat) : fib n = fib' n := by
  fun_induction fib
  rfl
  rfl
  grind [fib', fib'.aux]

[Kim Morrison]

Oh, oh, a chance for me to teach fishing!

theorem fib_eq_fib' (n : Nat) : fib n = fib' n := by try?

[Kim Morrison]

(which reproduces Jovan's proof immediately above, although with bullets)

[Jovan Gerbscheid]

Why does try? put the whole proof in a focus dot?

theorem fib_eq_fib' (n : Nat) : fib n = fib' n := by
  · fun_induction fib
    · rfl
    · rfl
    · grind only [fib', fib'.aux]