Fibonacci Divide and Conquer

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
{-
First, I acknowledge there is a better way to compute fib (n) with a divide and conquer method that uses only 
one recursive call instead of two.

So the problem is that to do this with well-founded recursion, I need to supply a proof that
   floor(n/2) < n

However, this is not true for 0.  However, I know that n/2 > 0, but I don't know how to use the fact that I've pattern matched, and
know that n>2 in fact.
-}
fibDivNonTer :   
fibDivNonTer 0 = 0
fibDivNonTer 1 = 1
fibDivNonTer 2 = 1
fibDivNonTer n with even n
fibDivNonTer n | true =
  let
    k =  n /2
    fibkmin1 = fibDivNonTer (pred k)
    fibk = fibDivNonTer k
    fibkplus1 = fibkmin1 + fibk
  in
    (fibkplus1 * fibk) + (fibk * fibkmin1)
fibDivNonTer n | false = 
  let
    k =  n /2
    fibk = fibDivNonTer k
    fibkplus1 = fibDivNonTer (k + 1)
  in
    (fibkplus1 * fibkplus1) + (fibk * fibk)