The goal of this lecture note is to reflect on the structure of the Fibonacci numbers.
Let us abstract the structure of the Fibonacci function by parameterizing its career, its addition function, its two base cases, and the function itself:
Definition Fibonacci (career : Type)
(add : career -> career -> career)
(fib_0 : career)
(fib_1 : career)
(fib : nat -> career) :=
(fib 0 = fib_0)
/\
(fib 1 = fib_1)
/\
(forall n : nat,
fib (S (S n)) = add (fib n) (fib (S n))).
In the rest of this note, we instantiate this structure with the standard Fibonacci function over natural numbers, and then with 2x2 matrices.
Here is the standard definition:
Fixpoint fib_nat (n : nat) : nat :=
match n with
0 => 0
| S n' => match n' with
0 => 1
| S n'' => fib_nat n'' + fib_nat n'
end
end.
Unsurprisingly, this standard definition fits the Fibonacci structure:
Theorem fib_nat_fits_Fibonacci :
Fibonacci nat Nat.add 0 1 fib_nat.
As discovered last week, Fibonacci numbers can be computed linearly by exponentiating the following 2x2 matrix of natural numbers:
Inductive m22_nat : Type :=
| M22_nat : nat -> nat -> nat -> nat -> m22_nat.
Definition zero_m22_nat :=
M22_nat 0 0
0 0.
Definition add_m22_nat (x y : m22_nat) : m22_nat :=
match (x, y) with
(M22_nat x11 x12
x21 x22,
M22_nat y11 y12
y21 y22) =>
M22_nat (x11 + y11) (x12 + y12)
(x21 + y21) (x22 + y22)
end.
Definition one_m22_nat :=
M22_nat 1 0
0 1.
Definition mul_m22_nat (x y : m22_nat) : m22_nat :=
match (x, y) with
(M22_nat x11 x12
x21 x22,
M22_nat y11 y12
y21 y22) =>
(M22_nat (x11 * y11 + x12 * y21) (x11 * y12 + x12 * y22)
(x21 * y11 + x22 * y21) (x21 * y12 + x22 * y22))
end.
Fixpoint power_m22_nat (x : m22_nat) (n : nat) : m22_nat:=
match n with
0 =>
one_m22_nat
| S n' =>
mul_m22_nat x (power_m22_nat x n')
end.
Definition F_nat :=
M22_nat 0 1
1 1.
Proposition about_exponentiating_F_nat :
forall n : nat,
power_m22_nat F_nat (S n) =
M22_nat (fib_nat n) (fib_nat (S n))
(fib_nat (S n)) (fib_nat (S (S n))).
We already met the following identity when investigating mystery functions:
Proposition an_identity_about_Fibonacci_numbers :
forall p q : nat,
fib_nat (S (p + q)) =
fib_nat p * fib_nat q + fib_nat (S p) * fib_nat (S q).
The goal of this exercise is to prove this identity:
in and of itself, i.e., by induction;
as a corollary of Proposition about_exponentiating_F_nat and of the following property when it is applied to F_nat, S p, and S q, for any p and q of type nat:
Property about_exponentiating_2x2_matrices_of_nats :
forall (x : m22_nat)
(p q : nat),
power_m22_nat x (p + q) =
mul_m22_nat (power_m22_nat x p) (power_m22_nat x q).
Hint: look at the top-left cell of mult_m22 (power_m22_nat F_nat (S p)) (power_m22_nat F_nat (S q)).
The following property might come as a surprise, but then again:
+- -+ +- -+ +- -+
|fib(n) fib(n+1)| |fib(n+1) fib(n+2)| |fib(n+2) fib(n+2)|
| | + | | = | |
|fib(n+1) fib(n+2)| |fib(n+2) fib(n+3)| |fib(n+2) fib(n+3)|
+- -+ +- -+ +- -+
Formally:
Property as_luck_has_it :
forall n : nat,
power_m22_nat F_nat (S (S n)) =
add_m22_nat (power_m22_nat F_nat n) (power_m22_nat F_nat (S n)).
Proof.
intros [ | n'].
- ...
- rewrite ->3 about_exponentiating_F_nat.
unfold add_m22_nat.
rewrite <-3 fold_unfold_fib_nat_SS.
reflexivity.
Qed.
So successive exponents of F_nat fit the Fibonacci structure:
Definition fib_m22_nat (n : nat) : m22_nat :=
power_m22_nat F_nat n.
Theorem fib_m22_nat_fits_Fibonacci :
Fibonacci m22_nat add_m22_nat one_m22_nat F_nat fib_m22_nat.
Can this property be generalized? The following section embarks in such a generalization by parameterizing the type of the cells of the 2x2 matrices.
The following declaration defines polymorphic 2x2 matrices:
Inductive pm22 (V : Type) :=
| PM22 : V -> V -> V -> V -> pm22 V.
For example, 2x2 matrices of natural numbers are obtained as pm22 nat and 2x2 matrices of 2x2 matrices of natural numbers are obtained as pm22 (pm22 nat).
Let us develop the algebra of these polymorphic matrices:
Definition zero_pm22 (V : Type) (zero : V) : pm22 V :=
PM22 V
zero zero
zero zero.
Definition add_pm22 (V : Type) (add : V -> V -> V) (x y : pm22 V) : pm22 V :=
match (x, y) with
(PM22 _
x11 x12
x21 x22,
PM22 _
y11 y12
y21 y22) =>
PM22 V
(add x11 y11) (add x12 y12)
(add x21 y21) (add x22 y22)
end.
Definition one_pm22 (V : Type) (zero : V) (one : V) : pm22 V :=
PM22 V
one zero
zero one.
Definition mul_pm22 (V : Type) (add : V -> V -> V) (mul : V -> V -> V) (x y : pm22 V) : pm22 V :=
match (x, y) with
(PM22 _
x11 x12
x21 x22,
PM22 _
y11 y12
y21 y22) =>
PM22 V
(add (mul x11 y11) (mul x12 y21)) (add (mul x11 y12) (mul x12 y22))
(add (mul x21 y11) (mul x22 y21)) (add (mul x21 y12) (mul x22 y22))
end.
Provided a type V and an addition function add : V -> V -> V that is associative and that has a zero element which is neutral on its left (resp. on its right), it is simple to prove that add_pm22 is also associative, and that zero_pm22 V zero is neutral on its left (resp. on its right). Likewise for mul_pm22: provided a type V and suitable addition and multiplication functions add : V -> V -> V and mul : V -> V -> V, it is simple to prove that mul_pm22 is associative, that one_pm11 V zero one is neutral on its left and on its right, and that zero_pm22 V zero is absorbing on its left and on its right.
Thus equipped, we can define a polymorphic exponentiation function as well as the polymorphic analogue of F_nat:
Fixpoint power_pm22 (V : Type) (add mul : V -> V -> V) (zero one : V) (x : pm22 V) (n : nat) : pm22 V :=
match n with
0 =>
one_pm22 V zero one
| S n' =>
mul_pm22 V add mul x (power_pm22 V add mul zero one x n')
end.
Definition F_pm22 (V : Type) (zero : V) (one : V) : pm22 V :=
PM22 V
zero one
one one.
And as before, successive exponents of F_pm22 fit the Fibonacci structure with one_pm22 in the first base case and F_pm22 in the second base case:
Definition fib_pm22 (V : Type) (add mul : V -> V -> V) (zero one : V) (n : nat) : pm22 V :=
power_pm22 V add mul zero one (F_pm22 V zero one) n.
Theorem fib_pm22_fits_Fibonacci :
forall (V : Type)
(zero one : V)
(add mul : V -> V -> V),
(forall v : V,
add zero v = v) ->
(forall v : V,
add v zero = v) ->
(forall v : V,
mul zero v = zero) ->
(forall v : V,
mul v zero = zero) ->
(forall v : V,
mul one v = v) ->
(forall v : V,
mul v one = v) ->
Fibonacci (pm22 V)
(add_pm22 V add)
(one_pm22 V zero one)
(F_pm22 V zero one)
(fib_pm22 V add mul zero one).
Instantiating pm22 with nat provides us with 2x2 matrices of natural numbers:
Definition pm22_nat := pm22 nat.
So we can define fib_m22_nat as an instance of fib_pm22 and prove fib_m22_nat_fits_Fibonacci as an instance of fib_pm22_fits_Fibonacci:
Definition zero_pm22_nat := zero_pm22 nat 0.
Definition add_pm22_nat := add_pm22 nat Nat.add.
Definition one_pm22_nat := one_pm22 nat 0 1.
Definition mul_pm22_nat := mul_pm22 nat Nat.add Nat.mul.
Definition power_pm22_nat := power_pm22 nat Nat.add Nat.mul 0 1.
Definition F_pm22_nat := F_pm22 nat 0 1.
Definition fib_pm22_nat := fib_pm22 nat Nat.add Nat.mul 0 1.
Corollary fib_pm22_nat_fits_Fibonacci :
Fibonacci pm22_nat add_pm22_nat one_pm22_nat F_pm22_nat fib_pm22_nat.
Proof.
exact (fib_pm22_fits_Fibonacci nat 0 1 Nat.add Nat.mul Nat.add_0_l Nat.add_0_r Nat.mul_0_l Nat.mul_0_r Nat.mul_1_l Nat.mul_1_r).
Qed.
The following theorem captures how a Fibonacci structure at type V that features a Fibonacci function fib gives rise to a new Fibonacci structure at type pm22 V by exponentiating the matrix PM22 V (fib 0) (fib 1) (fib 1) (fib 1):
Theorem about_layering :
forall (V : Type)
(zero one : V)
(add mul : V -> V -> V),
(forall v : V,
add zero v = v) ->
(forall v : V,
add v zero = v) ->
(forall v : V,
mul zero v = zero) ->
(forall v : V,
mul v zero = zero) ->
(forall v : V,
mul one v = v) ->
(forall v : V,
mul v one = v) ->
forall fib : nat -> V,
Fibonacci V add zero one fib ->
Fibonacci (pm22 V)
(add_pm22 V add)
(one_pm22 V (fib 0) (fib 1))
(F_pm22 V (fib 0) (fib 1))
(fib_pm22 V add mul (fib 0) (fib 1)).
It is one thing to know that fib_pm22 fits the Fibonacci structure and another to see what these successive “Fibonacci numbers” look like. The following two sections answer this question in the base case where fib_pm22 is instantiated with a given type V and in the induction step where given a type V, fib_pm22 is instantiated with pm22 V.
In the base case, given a type V and two zero and one elements zero and one, the successive exponents of F_pm22 V (fib 0) (fib 1) feature the underlying Fibonacci numbers at type V:
Proposition about_fib_pm22_base_case :
forall (V : Type)
(add mul : V -> V -> V)
(zero one : V),
(forall v : V,
add zero v = v) ->
(forall v : V,
add v zero = v) ->
(forall v : V,
mul zero v = zero) ->
(forall v : V,
mul v zero = zero) ->
(forall v : V,
mul one v = v) ->
(forall v : V,
mul v one = v) ->
forall (fib : nat -> V),
Fibonacci V add zero one fib ->
forall n : nat,
fib_pm22 V add mul (fib 0) (fib 1) (S n) =
PM22 V
(fib n) (fib (S n))
(fib (S n)) (fib (S (S n))).
In the induction step, given a type V and two zero and one elements zero and one, the successive exponents of F_pm22 V (zero_pm22 V (fib 0)) (one_pm22 V (fib 0) (fib 1)) feature the scalar product of the underlying Fibonacci numbers at type V and of the given identity matrix one_pm22 V zero one, reflecting the underlying Fibonacci structure, the matrix layering induced by pm22, and its multiplicative growth:
Proposition about_fib_pm22_induction_step :
forall (V : Type)
(add mul : V -> V -> V)
(zero one : V),
(forall v : V,
add zero v = v) ->
(forall v : V,
add v zero = v) ->
(forall v : V,
mul zero v = zero) ->
(forall v : V,
mul v zero = zero) ->
(forall v : V,
mul one v = v) ->
(forall v : V,
mul v one = v) ->
forall (fib : nat -> V),
Fibonacci V add zero one fib ->
forall n : nat,
fib_pm22 (pm22 V) (add_pm22 V add) (mul_pm22 V add mul) (zero_pm22 V (fib 0)) (one_pm22 V (fib 0) (fib 1)) (S n) =
PM22 (pm22 V)
(scalar_mul_pm22 V mul (fib n) (one_pm22 V zero one)) (scalar_mul_pm22 V mul (fib (S n)) (one_pm22 V zero one))
(scalar_mul_pm22 V mul (fib (S n)) (one_pm22 V zero one)) (scalar_mul_pm22 V mul (fib (S (S n))) (one_pm22 V zero one)).
Ideas come from somewhere, and Proposition about_fib_pm22_induction_step arose from the following property, which initially came as a surprise to the author of this lecture note:
Property as_luck_has_it_too :
forall n : nat,
fib_pm22 (pm22 nat) (add_pm22 nat Nat.add) (mul_pm22 nat Nat.add Nat.mul) (zero_pm22 nat 0) (one_pm22 nat 0 1) (S n) =
PM22 (pm22 nat)
(PM22 nat (fib_nat n) 0 0 (fib_nat n)) (PM22 nat (fib_nat (S n)) 0 0 (fib_nat (S n)))
(PM22 nat (fib_nat (S n)) 0 0 (fib_nat (S n))) (PM22 nat (fib_nat (S (S n))) 0 0 (fib_nat (S (S n)))).
Je ne sais pas le reste.
Created [04 Apr 2024]