learning-sicp

commit ec81ef1ea7f9b86c1324cd577bc66160bc0912c5
parent 956214616b85e2569fcd69b6ae2a6e7ef0b699e8
Author: Yuval Langer <yuval.langer@gmail.com>
Date:   Thu, 23 Nov 2023 20:48:27 +0200

Add proof to chapter-1 exercise-13 (1.13).  It probably has a bunch of errors.

Diffstat:
M
sicp/solutions/chapter-1/exercise-13.scm
 | 
82
+++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
A
sicp/tests/chapter-1/exercise-13.scm
 | 
7
+++++++

2 files changed, 89 insertions(+), 0 deletions(-)
diff --git a/sicp/solutions/chapter-1/exercise-13.scm b/sicp/solutions/chapter-1/exercise-13.scm
@@ -9,3 +9,85 @@ prove that _Fib_(n) = ([phi]^n - [illegiblesymbol]^n)/[sqrt](5).
 !#
 
 #! oh boy. XXX !#
+
+#!
+
+;;; Prove fib(n) = phi^n / sqrt(5).
+;;;
+;;; First, prove that fib(n) = (phi^n - psi^n) / sqrt(5), where:
+;;;     phi = (1 + sqrt(5)) / 2,
+;;;     psi = (1 - sqrt(5)) / 2,
+;;;     n is a non-negative integer,
+;;;     fib(0) = 0,
+;;;     fib(1) = 1,
+;;;     fib(n) = fib(n - 1) + fib (n - 2).
+;;;
+;;; Proof by induction:
+;;;
+;;; For the case where n = 0:
+;;;
+;;; By definition, fib(0) = 0.
+;;;
+;;; (phi^0 - psi^0) / sqrt(5)
+;;; = (1 - 1) / sqrt(5)
+;;; = 0
+;;;
+;;; For the case where n = 1:
+;;;
+;;; By definition, fib(1) = 1.
+;;;
+;;; (phi^1 - psi^1) / sqrt(5)
+;;; = (phi - psi) / sqrt(5)
+;;; = ((1+sqrt(5))/2 - (1-sqrt(5))/2) / sqrt(5)
+;;; = (1/2 + sqrt(5)/2 - 1/2 +sqrt(5)/2) / sqrt(5)
+;;; = (2*sqrt(5)/2) / sqrt(5)
+;;; = sqrt(5) / sqrt(5)
+;;; = 1
+;;;
+;;; Induction step:
+;;;
+;;; Assume:
+;;;
+;;; fib(n) = (phi^n - psi^n) / sqrt(5)
+;;;
+;;; fib(n-1) = (phi^(n-1) - psi^(n-1)) / sqrt(5)
+;;;          = (phi^n / phi - psi^n / psi) / sqrt(5)
+;;;
+;;; fib(n+1) = (phi^(n+1) - psi^(n+1)) / sqrt(5)
+;;;          = (phi*phi^n - psi*psi^n) / sqrt(5)
+;;;          = ( (1 + sqrt(5)) * phi^n / 2 - (1 - sqrt(5)) * psi^n / 2) / sqrt(5)
+;;;          = phi^n / (2 * sqrt(5)) + phi^n / 2 - psi^n / (2 * sqrt(5)) + psi^n / 2
+;;;          = phi^n / (2 * sqrt(5)) - psi^n / (2 * sqrt(5)) + phi^n / 2 + psi^n / 2
+;;;          = ((phi^n - psi^n) / sqrt(5)) / 2 + phi^n / 2 + psi^n / 2
+;;;          = fib(n) / 2 + phi^n / 2 + psi^n / 2
+;;;          = fib(n) / 2 + (phi^n + psi^n) / 2
+;;; XXX: What am I doing here?  Is this really acceptable?  No circular reasoning?
+;;;          = fib(n) / 2 + (fib(n) + 2fib(n-1))/2
+;;;          = fib(n) / 2 + fib(n)/2 + fib(n-1)
+;;;          = fib(n) + fib(n-1)
+;;;
+;;; 2 fib(n+1) = fib(n) + phi^n + psi^n
+;;;            = 2 (fib(n) + fib(n-1))
+;;; fib(n) + phi^n + psi^n = 2fib(n) + 2fib(n-1)
+;;; phi^n + psi^n -2fib(n-1) = fib(n)
+;;; phi^n + psi^n = fib(n) + 2fib(n-1)
+;;;
+;;; Now that we know that:
+;;;
+;;; fib(n) = (phi^n - psi^n) / sqrt(5)
+;;;
+;;; we can see that at the limit of:
+;;;
+;;; n -> infinity
+;;;
+;;; psi^n -> 0
+;;;
+;;; therefore:
+;;;
+;;; (phi^n - psi^n) / sqrt(5) -> phi^n / sqrt(5)
+;;;
+;;; which means that indeed fib(n) is the closest integer to phi^n / sqrt(5)
+;;;
+;;; QED?
+
+!#
diff --git a/sicp/tests/chapter-1/exercise-13.scm b/sicp/tests/chapter-1/exercise-13.scm
@@ -0,0 +1,7 @@
+(define-library (sicp tests chapter-1 exercise-13)
+  (import (scheme base)
+          (srfi :64))
+
+  (begin
+    ;; No code to test.  Texty solution is in the solution file.
+    (test-begin "chapter-1-exercise-13")))