Proving extensionally equivalent fibonacci functions using Idris

fibequiv.idr

%default total

||| A stream (an infinite list) of natural numbers representing the
||| fibbonacci sequence.
fibs : Stream Nat 
fibs = f 0 1 
  where
    f : Nat -> Nat -> Stream Nat 
    f a b = a :: f b (a + b)

||| A constructive proof that forall natural numbers 'n', and 
||| some stream 'xs', the length of the list derived by
||| taking the first n + 1 elements of 'xs' is always greater than 'n'.
nAlwaysLteSn : (n : Nat) -> (xs : Stream a) ->  
               LTE (S n) (length (Stream.take (S n) xs))
nAlwaysLteSn Z (value :: xs) = lteRefl
nAlwaysLteSn (S k) (value :: xs) = 
  let rec = nAlwaysLteSn k xs
  in LTESucc rec 

||| A constructive proof that forall natural numbers 'n' and some
||| list 'xs'. Given a proof that n < the length of 'xs'. Then n is
||| a valid index into 'xs'.
ltLenAlwaysBound : (n : Nat) -> (xs : List a) ->  
                   (prf : LTE (S n) (length xs)) -> InBounds n xs
ltLenAlwaysBound Z [] prf = absurd prf 
ltLenAlwaysBound Z (x :: xs) prf = InFirst
ltLenAlwaysBound (S k) [] prf = absurd prf
ltLenAlwaysBound (S k) (x :: xs) prf =
  let rec = ltLenAlwaysBound k xs
  in InLater (rec (fromLteSucc prf))

||| A function that returns the fibonacci term at index 'n'.
fib' : Nat -> Nat
fib' n =
  let p1 = nAlwaysLteSn n fibs
      xs = take (S n) fibs
      p2 = ltLenAlwaysBound n xs p1
  in List.index n (take (S n) fibs) {ok = p2}

||| A second function that returns the fibonacci term at index 'n'.
fib'' : Nat -> Nat
fib'' n = f n 0 1
  where
    f : Nat -> Nat -> Nat -> Nat
    f Z a b = a
    f (S k) a b = f k b (a + b)

||| An axiom of functional extensionality.
||| (two functions are equal if they "do the same thing").
postulate
functional_extensionality : {a, b : Type} -> {f, g : a -> b} ->
                            (prf : (x : a) -> f x = g x) -> f = g

fibIsFib : (\x => fib'' x) = (\x => fib' x)
fibIsFib = functional_extensionality $ \x => ?test

-- Gives the following type error:

-- 56 | fibIsFib = functional_extensionality $ \x => ?test
--    |            ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-- When checking deferred type of Main.test:
-- Type mismatch between
--         LTE (S x1) (S (length (take x1 (Main.fibs, f 1 1))))
-- and
--         LTE (S x1) (S (length (take x1 (1 :: Delay (Main.fibs, f 1 2)))))