@@ -0,0 +1,50 @@
1+||| Properties of the Fibonacci function.
8+||| Recursive definition of Fibonacci.
12+fibRec (S (S k)) = fibRec (S k) + fibRec k
14+||| Accumulator for fibItr.
15+fibAcc : Nat -> Nat -> Nat -> Nat
17+fibAcc (S k) a b = fibAcc k b (a + b)
19+||| Iterative definition of Fibonacci.
21+fibItr n = fibAcc n 0 1
23+||| Addend shuffling lemma.
24+plusLemma : (a, b, c, d : Nat) -> (a + b) + (c + d) = (a + c) + (b + 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)
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
43+||| Iterative and recursive Fibonacci definitions are equivalent.
44+fibEq : (n : Nat) -> fibRec n = fibItr n
49+ rewrite fibEq (S k) in