0 | ||| Properties of Fibonacci functions
 1 | module Data.Nat.Fib
 2 |
 3 | import Data.Nat
 4 |
 5 | %default total
 6 |
 7 | ||| Recursive definition of Fibonacci.
 8 | fibRec : Nat -> Nat
 9 | fibRec Z = Z
10 | fibRec (S Z) = S Z
11 | fibRec (S (S k)) = fibRec (S k) + fibRec k
12 |
13 | ||| Accumulator for fibItr.
14 | fibAcc : Nat -> Nat -> Nat -> Nat
15 | fibAcc Z a _ = a
16 | fibAcc (S k) a b = fibAcc k b (a + b)
17 |
18 | ||| Iterative definition of Fibonacci.
19 | fibItr : Nat -> Nat
20 | fibItr n = fibAcc n 0 1
21 |
22 | ||| Addend shuffling lemma.
23 | plusLemma : (a, b, c, d : Nat) -> (a + b) + (c + d) = (a + c) + (b + d)
24 | plusLemma a b c d =
25 |   rewrite sym $ plusAssociative a b (c + d) in
26 |     rewrite plusAssociative b c d in
27 |       rewrite plusCommutative b c in
28 |         rewrite sym $ plusAssociative c b d in
29 |           plusAssociative a c (b + d)
30 |
31 | ||| Helper lemma for fibacc.
32 | fibAdd : (n, a, b, c, d : Nat) ->
33 |   fibAcc n a b + fibAcc n c d = fibAcc n (a + c) (b + d)
34 | fibAdd Z _ _ _ _ = Refl
35 | fibAdd (S Z) _ _ _ _ = Refl
36 | fibAdd (S (S k)) a b c d =
37 |   rewrite fibAdd k (a + b) (b + (a + b)) (c + d) (d + (c + d)) in
38 |     rewrite plusLemma b (a + b) d (c + d) in
39 |       rewrite plusLemma a b c d in
40 |         Refl
41 |
42 | ||| Iterative and recursive Fibonacci definitions are equivalent.
43 | fibEq : (n : Nat) -> fibRec n = fibItr n
44 | fibEq Z = Refl
45 | fibEq (S Z) = Refl
46 | fibEq (S (S k)) =
47 |   rewrite fibEq k in
48 |     rewrite fibEq (S k) in
49 |       fibAdd k 1 1 0 1
50 |