<< Previous exercise (1.12) | sicp-solutions | Next exercise (1.14) >>
A simple, beautiful modern solution by Sébastien Gignoux:
https://codology.net/post/sicp-solution-exercise-1-13/
Another one by Lucia:
This is a solution by Seninha (aka phillbush).
The solution is divided in two proofs, the first one divided in two parts. First, it's proved by induction that Fib(n)=(φⁿ-ψⁿ)/√5, this involves two parts: proving for the base case, and proving for the inductive case. Then, that proof is used to prove that Fib(n) is the closest integer to φⁿ/√5.
The solution uses the ⊦ notation, known as sequent calculus. What is after the ⊦ is what we want to prove. So, for example, ⊦ A means that we want to prove A; we will simplify or apply properties to A during the proof. What comes before the ⊦ are hypotheses that are helpful for our proof. So, for example, H₁ ⊦ A means that we are using the hypothesis H₁ to prove A. We may use ellipsis to omit previous hypotheses. The symbol ⊤ means tautology or truth.
Proof 1, part 1 (base case).
We need to prove that Fib(n)=(φⁿ-ψⁿ)/√5 is valid for n=0 and for n=1.
⊦ Fib(0)=(φ⁰-ψ⁰)/√5 ∧ Fib(1)=(φ¹-ψ¹)/√5.
Simplifying both sides of the conjunction.
⊦ Fib(0)=0 ∧ Fib(1)=1.
By definition, Fib(0)=0 and Fib(1)=1, so both sides of the conjunction are true.
⊦ ⊤ ∧ ⊤.
Simplifying this conjunction, we prove this part.
⊦ ⊤.
Proof 1, part 2 (inductive case).
Let k be a natural number. We are given the two inductive hypothesis H₁ and H₂, and we need to prove that Fib(n) = (φⁿ-ψⁿ)/√5 is valid for n=k+2.
k:ℕ;
H₁:Fib(k) = (φᵏ-ψᵏ)/√5;
H₂:Fib(k+1) = (φᵏ⁺¹-ψᵏ⁺¹)/√5
⊦ Fib(k+2) = (φᵏ⁺²-ψᵏ⁺²)/√5.
By the definition of Fib on the goal, we know that Fib(k+2) is equal to Fib(k) + Fib(k+1). We can rewrite the goal with this fact.
… ⊦ Fib(k) + Fib(k+1) = (φᵏ⁺²-ψᵏ⁺²)/√5.
We can rewrite the goal with the hypotheses H₁ and H₂.
… ⊦ (φᵏ-ψᵏ)/√5 + (φᵏ⁺¹-ψᵏ⁺¹)/√5 = (φᵏ⁺²-ψᵏ⁺²)/√5.
We can simplify the left side of the equation on the goal.
… ⊦ (φᵏ(φ+1) - ψᵏ(ψ+1))/√5 = (φᵏ⁺²-ψᵏ⁺²)/√5.
As declared in page 38, φ is the golden ratio, the only positive solution to the equation x²=x+1. The ψ constant also share that property, being the only negative solution to that equation. We can apply this equation to φ and to ψ:
… ⊦ (φᵏ·φ² - ψᵏ·ψ²)/√5 = (φᵏ⁺²-ψᵏ⁺²)/√5.
We can simplify the left side of the equation on the goal.
… ⊦ (φᵏ⁺² - ψᵏ⁺²)/√5 = (φᵏ⁺²-ψᵏ⁺²)/√5.
Both sides of the equation on the goal are equal. We achieved truth.
… ⊦ ⊤.
Proof 2.
Now that we proved that Fib(n)=(φⁿ-ψⁿ)/√5, we can use this fact as hypothesis H₁ to prove that Fib(n) is the closest integer to φⁿ/√5. Formally, we want to prove that the absolute value of Fib(n) minus φⁿ/√5 is less than 1/2, for all n natural.
n:ℕ;
H₁:Fib(n)=(φⁿ-ψⁿ)/√5
⊦ |Fib(n) - φⁿ/√5| < 1/2.
We can rewrite Fib(n) on the goal with the hypothesis H₁.
… ⊦ |(φⁿ-ψⁿ)/√5 - φⁿ/√5| < 1/2.
We can simplify the left side of the inequality on the goal.
… ⊦ |ψⁿ|/√5 < 1/2.
We can then apply the definition of ψ.
… ⊦ |((1-√5)/2)ⁿ|/√5 < 1/2.
We can simplify the left side of the inequality on the goal.
… ⊦ ((√5-1)/2)ⁿ/√5 < 1/2.
We can add another hypothesis (H₂) for the fact that √5<3.
…; H₂:√5<3 ⊦ ((√5-1)/2)ⁿ/√5 < 1/2.
We can subtract both sides of the inequality in the hypothesis H₂ by one, then divide both sides by two, raise both sides to the n-th power, and multiply both sides by 1/√5.
…; H₂:1/√5 × ((√5-1)/2)ⁿ < 1/√5 ⊦ ((√5-1)/2)ⁿ/√5 < 1/2.
It's a fact that 1/√5 < 1/2, we can apply this fact to H₂.
…; H₂:((√5-1)/2)ⁿ/√5 < 1/√5 < 1/2 ⊦ ((√5-1)/2)ⁿ/√5 < 1/2.
We can fold the double inequality in H₂ by removing the middle part.
…; H₂:((√5-1)/2)ⁿ/√5 < 1/2 ⊦ ((√5-1)/2)ⁿ/√5 < 1/2.
The hypothesis H₂ is exactly what we want to prove, we achieved the truth by redundancy.
… ⊦ ⊤.
QED.