= Solution
Let $T(n)=(F_n,F_{n+1})$. The equations derived in part (e) become $T(0)=(0,1)$ and $T(n+1)=s(T(n))$, where $s(a,b)=(b,a+b)$. Replacing zero and successor by that seed and step is exactly a <natural-number fold>:
``
twoFibsNat :: Natural -> (Integer, Integer)
twoFibsNat = foldNat step (0, 1)
where
step :: (Integer, Integer) -> (Integer, Integer)
step (a, b) = (b, a + b)
fibNat :: Natural -> Integer
fibNat = fst . twoFibsNat
``
Consequently
$$
\boxed{\operatorname{fibNat}=\operatorname{fst}\circ\operatorname{foldNat}\bigl((a,b)\mapsto(b,a+b)\bigr)(0,1).}
$$
<Structural induction> follows the constructors of `Natural`: the seed gives the first two <Fibonacci numbers>, and the successor step uses the <Fibonacci recurrence>. The extra component carries exactly the information needed for the next update.
Back to article page
