sicp-2e/c1/e1.13.scm

; to prove via induction, we evaluate the base case and its iteration
; our assumption is that:
;
; fib(n) = (((1 + sqrt(5))/2)^n - ((1 - sqrt(5))/2)^n) / sqrt(5)
;
; for better illustration, define phi and psi to be the following:
;
; phi = (1 + sqrt(5)) / 2
; psi = (1 - sqrt(5)) / 2
;
; [ they are identical except for their sign in front of the sqrt(5), this is called congruency ]
; 
; as such, fib(n) is better defined as:
; 
; fib(n) = (phi^n - psi^n) / sqrt(5)
;
; our previous definition of fibonacci, used for our implementation, looked like this:
;
; fib(n) = { 0                    .. if n = 0,
;            1                    .. if n = 1,
;            fib(n-1) + fib(n-2)  .. if n > 0 }
;
; filling our two base cases:
;
; fib(0) = (phi^0 - psi^0) / sqrt(5) = (1 - 1) / sqrt(5) = 0 / sqrt(5) = 0
; 
; [ in this case, we needn't even know what phi and psi are supposed to be ]
; 
; fib(1) = (phi^1 - psi^1) / sqrt(5)
; fib(1) = ((1 + sqrt(5)) / 2 - (1 - sqrt(5)) / 2) / sqrt(5)
; 1/sqrt(5) * fib(1) = 1/2 * (1 + sqrt(5) - (1 - sqrt(5)))
; 1/sqrt(5) * fib(1) = 1/2 * (1 + sqrt(5) - 1 + sqrt(5))
; 1/sqrt(5) * fib(1) = 1/2 * (2 * sqrt(5)) = sqrt(5)
; fib(1) = sqrt(5) / sqrt(5) = 1
; 
; [ thus our second base case (n = 1) is satisfied ]
;
; now for the tough part of the assignment, we need to prove that fib(n + 1) = fib(n) + fib(n - 1)
; to better suit our definition as well as assumption above, we rewrite to fib(n) = fib(n - 1) + fib(n - 2)
;
; we beginn by reducing fib to our assumption formula above, replacing fib by it's constituents phi, psi and other constants:
;
; fib(n) = fib(n - 1) + fib(n - 2)
; fib(n) = (phi^n - psi^n) / sqrt(5)
;
; (phi^n - psi^n) / sqrt(5) = ((phi^(n - 1) - psi^(n - 1)) / sqrt(5)) + ((phi^(n - 2) - psi^(n - 2)) / sqrt(5))
;
; [ the fib(n - 1) and fib(n - 2) parts can be brought under one divisor ]
;
; (phi^n - psi^n) / sqrt(5) = (phi^(n - 1) - psi^(n - 1) + phi^(n - 2) - psi^(n - 2)) / sqrt(5)
;
; [ we multiply sqrt(5) to both sides, eliminating our common divisor ]
; 
; (phi^n - psi^n) / sqrt(5) * sqrt(5) = (phi^(n - 1) - psi^(n - 1) + phi^(n - 2) - psi^(n - 2)) / sqrt(5) * sqrt(5)
; phi^n - psi^n = phi^(n - 1) - psi^(n - 1) + phi^(n - 2) - psi^(n - 2)
;
; [ now as we try to prove equality, the right side has to mimic the left, thus we attempt to bring every phi/psi component on the RHS (right hand side) to the same exponent of the LHS (left hand side) ]
;
; phi^n - psi^n = phi^(n - 1) - psi^(n - 1) + phi^(n - 2) - psi^(n - 2)
;
; phi^n - psi^n = (phi^(n - 1) * phi) / phi - (psi^(n - 1) * psi) / psi + (phi^(n - 2) * phi^2) / phi^2 - (psi^(n - 2) * psi^2) / psi^2
; 
; [ as the constituents of fib(n - 1) are closer to our target constituents fib(n), we only complement phi/psi once, whereas for the constituents of fib(n - 2), we complement by phi/psi to the power of 2 respectively ]
; [ our next possible step is to now simplify to a more workable representation ]
; 
; phi^n - psi^n = phi^n * (1 / phi + 1 / phi^2) - psi^n * (1 / psi + 1 / psi^2)
;
; [ in this step, we simply extracted the common numerator phi/psi respetively, and left the fraction in tact in all othe respects ]
; [ next up is substituting phi and psi values within the brackets ]
; [ our reason for doing so, notice how the RHS has *almost* exactly the structure we want? ]
; [ in theory, if LHS and RHS truly equal each other, meaning, if fib(n) truly equals fib(n - 1) + fib(n - 2), the contents of the brackets should evaluate to 1 ]
; [ such that the RHS assumes the form psi^n * (1) - psi^n * (1) ]
; [ this is based on the logical deduction that there cannot be equality otherwise, so whatever the brackets evaluate to determines the outcome of our proof attempt ]
; [ thus we continue on... ]
;
; phi^n - psi^n = phi^n * (1 / (...)^1 + 1 / (...)^2) - psi^n * (1 / (...)^1 + 1 / (...)^2)
;
; [ our substitution assumes the above form, which is simplified for readability above, and expanded for real below ]
;
; phi^n - psi^n = phi^n * (1 / ((1 + sqrt(5)) / 2)^1 + 1 / ((1 + sqrt(5) / 2)^2)) - psi^n * (1 / ((1 - sqrt(5)) / 2)^1 + 1 / ((1 - sqrt(5) / 2)^2))
;
; [ looks bad I know ]
; [ next up, simplify the double brackets (of the expanded phi/psi components) by multiplying each 1/2 or (1/2)^2 upwards ]
;
; phi^n - psi^n = phi^n * (2 / (...)^1 + 4 / (...)^2) - psi^n * (2 / (...)^1 + 4 / (...)^2)
;
; [ again, a simplified view to better showcase the transformation, expanded for real below ]
;
; phi^n - psi^n = phi^n * (2 / (1 + sqrt(5))^1 + 4 / (1 + sqrt(5))^2) - psi^n * (2 / (1 - sqrt(5))^1 + 4 / (1 - sqrt(5))^2)
;
; [ next up we complement the fractions by the respective values needed to unify both fractions under a single one, such that the structures 2/(...)^1 and 4/(...)^2 merge into a single fraction ]
;
; phi^n - psi^n = phi^n * ((2 * (1 + sqrt(5))) / (1 + sqrt(5))^2 + 4 / (1 + sqrt(5))^2) - psi^n * ((2 * (1 - sqrt(5))) / (1 - sqrt(5))^2 + 4 / (1 - sqrt(5))^2)
;
; [ if you looked carefully, you can see each fraction now has a divisor in the form of (...)^2, further reducing to... ]
;
; phi^n - psi^n = phi^n * ((2 * (1 + sqrt(5)) + 4) / (1 + sqrt(5))^2) - psi^n * ((2 * (1 - sqrt(5)) + 4) / (1 - sqrt(5))^2)
;
; [ multiplying the numerators... ]
;
; phi^n - psi^n = phi^n * ((2 + 2sqrt(5) + 4) / (1 + sqrt(5))^2) - psi^n * ((2 - 2sqrt(5) + 4) / (1 - sqrt(5))^2)
;
; [ applying the binomial formula to the divisor ]
;
; phi^n - psi^n = phi^n * ((2 + 2sqrt(5) + 4) / (1^2 + 2sqrt(5) + sqrt(5)^2)) - psi^n * ((2 - 2sqrt(5) + 4) / (1^2 - 2sqrt(5) + sqrt(5)^2))
;
; phi^n - psi^n = phi^n * ((2 + 2sqrt(5) + 4) / (1 + 2sqrt(5) + 5)) - psi^n * ((2 - 2sqrt(5) + 4) / (1 - 2sqrt(5) + 5))
;
; [ we notice the denominator and numerator resemble each other closely, only the summands are different ]
; [ (2 + ... + 4) for the numerator ]
; [ (1 + ... + 5) for the denominator ]
; [ the summands add to 6 in both cases! ]
; [ understanding this, we can finally make our final reductions ]
;
; 
; phi^n - psi^n = phi^n * ((6 + 2sqrt(5)) / (6 + 2sqrt(5))) - psi^n * ((6 - 2sqrt(5)) / (6 - 2sqrt(5)))
; phi^n - psi^n = phi^n * 1 + psi^n * 1
; phi^n - psi^n = phi^n - psi^n
;
; thus, our proof is established, fib(n) does equal fib(n - 1) + fib(n - 2) after all
; as every fib(n) can be iteratively deduced from its previous components, and as fib(n + 1) is true as well as the base case, we can assume fib(n) to be true for every n (element of positive integers)

#|
2019-08-26 it seems this lousy programmer finally figured out how to use block comments! (albeit dialect dependent)
|#