(Joint Center)Library fib

(* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *)
Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq choice fintype.
Require Import bigop div prime finfun tuple ssralg zmodp matrix binomial.

This files contains the definitions of: fib n == n.+1 th fibonacci number
lucas n == n.+1 lucas number
and some of their standard properties

Fixpoint fib_rec (n : nat) {struct n} : nat :=
  if n is n1.+1 then
    if n1 is n2.+1 then fib_rec n1 + fib_rec n2
    else 1
  else 0.

Definition fib := nosimpl fib_rec.

Lemma fibE : fib = fib_rec.

Lemma fib0 : fib 0 = 0.

Lemma fib1 : fib 1 = 1.

Lemma fibSS : n, fib n.+2 = fib n.+1 + fib n.

Fixpoint lin_fib_rec (a b n : nat) {struct n} : nat :=
  if n is n1.+1 then
    if n1 is n2.+1
      then lin_fib_rec b (b + a) n1
      else b
    else a.

Definition lin_fib := nosimpl lin_fib_rec.

Lemma lin_fibE : lin_fib = lin_fib_rec.

Lemma lin_fib0 : a b, lin_fib a b 0 = a.

Lemma lin_fib1 : a b, lin_fib a b 1 = b.

Lemma lin_fibSS : a b n, lin_fib a b n.+2 = lin_fib b (b + a) n.+1.

Lemma lin_fib_alt : n a b,
  lin_fib a b n.+2 = lin_fib a b n.+1 + lin_fib a b n.

Lemma fib_is_linear : fib =1 lin_fib 0 1.

Lemma fib_add : m n,
 m != 0 → fib (m + n) = fib m.-1 × fib n + fib m × fib n.+1.

Theorem dvdn_fib: m n, m %| nfib m %| fib n.

Lemma fib_gt0 : m, 0 < m → 0 < fib m.

Lemma fib_smonotone : m n, 1 < m < nfib m < fib n.

Lemma fib_monotone : m n, m nfib m fib n.

Lemma fib_eq1 : n, (fib n == 1) = ((n == 1) || (n == 2)).

Lemma fib_eq : m n,
  (fib m == fib n) = [|| m == n, (m == 1) && (n == 2) | (m == 2) && (n == 1)].

Lemma fib_prime : p, p != 4 → prime (fib p) → prime p.

Lemma fib_sub : m n, n m
   fib (m - n) = if odd n then fib m.+1 × fib n - fib m × fib n.+1
                 else fib m × fib n.+1 - fib m.+1 × fib n.

Lemma gcdn_fib: m n, gcdn (fib m) (fib n) = fib (gcdn m n).

Lemma coprimeSn_fib: n, coprime (fib n.+1) (fib n).

Fixpoint lucas_rec (n : nat) {struct n} : nat :=
  if n is n1.+1 then
    if n1 is n2.+1 then lucas_rec n1 + lucas_rec n2
    else 1
  else 2.

Definition lucas := nosimpl lucas_rec.

Lemma lucasE : lucas = lucas_rec.

Lemma lucas0 : lucas 0 = 2.

Lemma lucas1 : lucas 1 = 1.

Lemma lucasSS : n, lucas n.+2 = lucas n.+1 + lucas n.

Lemma lucas_is_linear : lucas =1 lin_fib 2 1.

Lemma lucas_fib: n, n != 0 → lucas n = fib n.+1 + fib n.-1.

Lemma lucas_gt0 : m, 0 < lucas m.

Lemma double_lucas: n, 3 n(lucas n).*2 = fib (n.+3) + fib (n-3).

Lemma fib_double_lucas : n, fib (n.*2) = fib n × lucas n.

Lemma fib_doubleS: n, fib (n.*2.+1) = fib n.+1 ^ 2 + fib n ^ 2.

Lemma fib_square: n, (fib n)^2 = if odd n then (fib n.+1 × fib n.-1).+1
                                        else (fib n.+1 × fib n.-1).-1.

Lemma fib_sum : n, \sum_(i < n) fib i = (fib n.+1).-1.

Lemma fib_sum_even : n, \sum_(i < n) fib i.*2 = (fib n.*2.-1).-1.

Lemma fib_sum_odd: n, \sum_(i < n) fib i.*2.+1 = fib n.*2.

Lemma fib_sum_square: n, \sum_(i < n) (fib i)^2 = fib n × fib n.-1.

Lemma bin_sum_diag: n, \sum_(i < n) 'C(n.-1-i,i) = fib n.

The matrix

Section Matrix.

Open Local Scope ring_scope.
Import GRing.Theory.

Variable R: ringType.

Equivalence ^ n.+1 fib n.+2 fib n.+1 1 1 = fib n.+1 fib n 1 0

Definition seq2matrix m n (l: seq (seq R)) :=
  \matrix_(i<m,j<n) nth 1 (nth [::] l i) j.

Local Notation "''M{' l } " := (seq2matrix _ _ l).

Lemma matrix_fib : n,
  'M{[:: [::(fib n.+2)%:R; (fib n.+1)%:R];
         [::(fib n.+1)%:R; (fib n)%:R]]} =
 ('M{[:: [:: 1; 1];
         [:: 1; 0]]})^+n.+1 :> 'M[R]_(2,2).

End Matrix.