Fibonacci function by ikegami__

module Theorem where

open import Algebra using (CommutativeSemiring)
open import Function using (_∘_)
open import Data.Nat
open import Data.Nat.Properties using (commutativeSemiring)
open import Relation.Binary.PropositionalEquality using (_≡_; subst)
open import Definitions

fib : ℕ → ℕ
fib 0 = 1
fib 1 = 1
-- fib (suc (suc n)) = fib (suc n) + fib n {- easy -}
fib (suc (suc n)) = fib n + fib (suc n) {- not clear -}

substFib : (n : ℕ) {x y : ℕ} → x ≡ y → Fib n x → Fib n y
substFib = subst ∘ Fib

transFib : (n x y : ℕ) → Fib n (y + x) → Fib n (x + y)
transFib n x y p 
  = substFib n (CommutativeSemiring.+-comm commutativeSemiring y x) p

genFib : (n x y : ℕ) → Fib n x → Fib (suc n) y → Fib (suc (suc n)) (x + y)
genFib n x y p q = transFib (suc (suc n)) x y (FibN q p)

fib-is-FibFunc : FibFunc fib
fib-is-FibFunc 0 = Fib0
fib-is-FibFunc 1 = Fib1
fib-is-FibFunc (suc (suc n))
  = genFib n (fib n) (fib (suc n)) (fib-is-FibFunc n) (fib-is-FibFunc (suc n))