Fibonacci function by notogawa

module Theorem where

open import Definitions

open import Data.Nat
open import Data.Product
import Relation.Binary.PropositionalEquality as PropEq
open PropEq using (_≡_; refl; sym; subst)
open import Data.Nat.Properties using (commutativeSemiring)
import Algebra
open Algebra.CommutativeSemiring commutativeSemiring using (+-assoc; +-comm)

private
  fib' : ℕ × ℕ → ℕ → ℕ
  fib' (a , b) zero = a
  fib' (a , b) (suc n) = fib' (b , b + a) n

  lemma : ∀ n a₁ a₂ b₁ b₂ →
          fib' (a₁ , b₁) n + fib' (a₂ , b₂) n ≡ fib' (a₁ + a₂ , b₁ + b₂) n
  lemma zero a₁ a₂ b₁ b₂ = refl
  lemma (suc n) a₁ a₂ b₁ b₂
    rewrite +-assoc b₁ b₂ (a₁ + a₂)
          | sym (+-assoc b₂ a₁ a₂)
          | +-comm b₂ a₁
          | +-assoc a₁ b₂ a₂
          | sym (+-assoc b₁ a₁ (b₂ + a₂))
          = lemma n b₁ b₂ (b₁ + a₁) (b₂ + a₂)

fib : ℕ → ℕ
fib = fib' (1 , 1)

private
  fibSSn≡fibSn+fibn : ∀ n → fib (suc (suc n)) ≡ fib (suc n) + fib n
  fibSSn≡fibSn+fibn zero = refl
  fibSSn≡fibSn+fibn (suc n)
    rewrite fibSSn≡fibSn+fibn n
          | lemma n 1 1 2 1
          | lemma n 2 1 3 2
          = refl

fib-is-FibFunc : FibFunc fib
fib-is-FibFunc zero = Fib0
fib-is-FibFunc (suc zero) = Fib1
fib-is-FibFunc (suc (suc n)) = subst (Fib (suc (suc n)))
                                     (sym (fibSSn≡fibSn+fibn n))
                                     (FibN (fib-is-FibFunc (suc n)) (fib-is-FibFunc n))

{-
fib : ℕ → ℕ
fib (suc (suc n)) = fib n + fib (suc n)
fib n = 1

fib-is-FibFunc : FibFunc fib
fib-is-FibFunc 0 = Fib0
fib-is-FibFunc 1 = Fib1
fib-is-FibFunc (suc (suc n)) =
  subst (Fib (suc (suc n)))
        (+-comm (fib (suc n)) (fib n))
        (FibN (fib-is-FibFunc (suc n)) (fib-is-FibFunc n))
-}