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