Solution of SICP Exercise 1.13

seninha.org
2022-06-08

In this post, I write my solution for the exercise 1.13 of the book Structure and Interpretation of Computer Programs, by Harold Abelson and Gerald Jay Sussman with Julie Sussman. I have already posted this solution elsewhere; but I'm reposting it here at my site just because.

Background

The section 1.2.2 of the book says that the value of Fib(n) grows exponentially with n. More precisely, Fib(n) is the closest integer to φⁿ/√5, where φ = (1 + √5)/2 ≈ 1.6180 is the golden ratio, which satisfies the equation φ² = φ + 1.

The exercise 1.13, which follows that section, is the following:

The book defines Fib(n) as follows:

         ⎧ 0                    if n = 0,
Fib(n) = ⎨ 1                    if n = 1,
         ⎩ Fib(n-1) + Fib(n-2)  otherwise.

The Solution

The solution is divided in two proofs, the first one divided in two parts. First, we follow the hint from the exercise and prove by induction that Fib(n) = (φⁿ - ψⁿ)/√5; this involves two parts: proving for the base case, and proving for the inductive case. Then, we use that proof 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.

k:ℕ;
H₁:Fib(k) = (φᵏ-ψᵏ)/√5;
H₂:Fib(k+1) = (φᵏ⁺¹-ψᵏ⁺¹)/√5
⊦ 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 section 1.2.2, φ 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.