**Paste:**#95123**Author:**GallagherJD**Language:**Agda (via Haskell)**Channel:**-**Created:**2013-11-03 01:34:27 UTC

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) |