# 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:

## 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`.

Simplifying both sides of the conjunction.

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`.

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.

We can rewrite the goal with the hypotheses `H₁` and `H₂`.

We can simplify the left side of the equation on the goal.

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 `ψ`:

We can simplify the left side of the equation on the goal.

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.

We can rewrite `Fib(n)` on the goal with the hypothesis `H₁`.

We can simplify the left side of the inequality on the goal.

We can then apply the definition of `ψ`.

We can simplify the left side of the inequality on the goal.

We can add another hypothesis (`H₂`) for the fact that `√5<3`.

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`.

It's a fact that `1/√5 < 1/2`, we can apply this fact to `H₂`.

We can fold the double inequality in `H₂` by removing the middle part.

The hypothesis `H₂` is exactly what we want to prove, we achieved the truth by redundancy.

QED.