Library Fib: Fibonacci sequence and decomposition


Require Import Arith Omega Wf_nat List NPeano.
Require Import DeltaList.
Import ListNotations.
Set Implicit Arguments.

Fibonacci sequence

First, a definition of the Fibonacci sequence. We use the standard definition that starts with 0 1 1 2 3 ... (See OEIS A000045).
Note: an earlier version of this development was using a shifted Fibonacci sequence, without its initial 0 (e.g. fib(0)=1, fib(1)=1, fib(2)=2, ...). This was convenient during some Coq proofs, but confusing for external readers, so we migrated back to the standard definition (with little overhead to the proofs, btw).

Fixpoint fib (n:nat) : nat :=
  match n with
  | 0 ⇒ 0
  | S n´ ⇒
    match n´ with
    | 0 ⇒ 1
    | S n´´ ⇒ fib n´ + fib n´´
    end
  end.

Lemma fib_eqn n : fib (S (S n)) = fib (S n) + fib n.

Lemma fib_eqn´ n : n≠0 → fib (S n) = fib n + fib (n-1).

Lemma fib_S_nz k : 1 ≤ fib (S k).

Lemma fib_nz k : k≠0 → 1 ≤ fib k.

Lemma fib_0_inv k : fib k = 0 → k = 0.

Lemma fib_lt_S k : 1 < k → fib k < fib (S k).

Lemma fib_lt k k´ : 1 < k → k < k´ → fib k < fib k´.

Lemma fib_mono_S k : fib k ≤ fib (S k).

Lemma fib_mono k k´ : k ≤ k´ → fib k ≤ fib k´.

Lemma fib_inj k k´ : 1<k → 1<k´ → fib k = fib k´ → k = k´.

Lemma fib_lt_inv k k´ : fib k < fib k´ → k < k´.

Lemma fib_le_id k : k ≤ S (fib k).

Lemma fib_inv n : { k | fib k ≤ n < fib (S k) }.

Decomposition via sums of Fibonacci numbers.

Zeckendorf's theorem (actually discovered earlier by Lekkerkerker) states that any natural number can be obtained by a sum of distinct Fibonacci numbers, and this decomposition is moreover unique when :
  • fib 0 and fib 1 aren't in the decomposition
  • Fibonacci numbers in the decomposition aren't consecutive.

The sumfib function

We represent a Fibonacci decomposition by the list of ranks of the Fibonacci numbers in this decomposition. The sumfib function is the sum of the Fibonacci numbers of these ranks. For the first results below, the ranks may be arbitrary : redundant, in any order, ...

Definition sumfib l := fold_right (fun n acc ⇒ fib n + acc) 0 l.

Lemma sumfib_cons a l : sumfib (a::l) = fib a + sumfib l.

Lemma sumfib_eqn l :
 ¬In 0 l →
 sumfib l + sumfib (map pred l) = sumfib (map S l).

Lemma sumfib_eqn´ l : ¬In 0 l →
 sumfib (map S l) - sumfib (map pred l) = sumfib l.

Lemma sumfib_app l l´ : sumfib (l++l´) = sumfib l + sumfib l´.

Lemma sumfib_rev l : sumfib (rev l) = sumfib l.

Lemma sumfib_0 l : ¬In 0 l → (sumfib l = 0 ↔ l = []).

Zeckendorf's Theorem

Technical lemma: A canonical decomposition cannot excess the next Fibonacci.

Lemma decomp_max k l :
  ¬In 1 (k::l) → DeltaRev 2 (k::l) → sumfib (k::l) < fib (S k).

Zeckendorf's Theorem, in a variant that consider decompositions with largest terms first (easiest for the proof).

Lemma decomp_exists_rev n :
  { l | sumfib l = n ∧ DeltaRev 2 l ∧ ¬In 0 l ∧ ¬In 1 l }.

Lemma decomp_unique_rev l l´ :
 ¬In 0 l → ¬In 1 l → DeltaRev 2 l →
 ¬In 0 l´ → ¬In 1 l´ → DeltaRev 2 l´ →
 sumfib l = sumfib l´ → l = l´.

Same theorem, in the other order (smallest term first).

Lemma decomp_exists n :
  { l | sumfib l = n ∧ Delta 2 (0::l) }.

Lemma decomp_unique l l´ :
 Delta 2 (0::l) → Delta 2 (0::l´) →
 sumfib l = sumfib l´ → l = l´.

Normalisation of a Fibonacci decomposition.

Starting from an increasing decomposition, we can transform it into a canonical decomposition (with no consecutive Fibonacci numbers), by simply saturating the basic Fibonacci equation fib k + fib (k+1) = fib (k+2) in the right order (highest terms first).
Termination isn't obvious for Coq, since we might have to re-launch normalisation on by-products of a first normalisation. The number of terms in the decomposition decreases strictly during the process, we use that to justify the termination.
Moreover, the lowest term in the decomposition grows (or stays equal), and the parity of its rank is preserved. This is expressed by the HeadLeEven predicate below.

Definition HeadLeEven l l´ := match l, l´ with
| [], [] ⇒ True
| k::_, k´::_ ⇒ ∃ p, k´ = k + 2×p
| _, _ ⇒ False
end.

Lemma norm_spec l :
 { l´ | sumfib l´ = sumfib l ∧
        (Delta 1 l → Delta 2 l´) ∧
        length l´ ≤ length l ∧
        HeadLeEven l l´ }.
Definition norm l := let (l´,_) := norm_spec l in l´.


Lemma norm_sum l : sumfib (norm l) = sumfib l.

Lemma norm_ok l : Delta 1 l → Delta 2 (norm l).

Lemma norm_ok´ l : Delta 1 (1::l) → Delta 2 (0::norm l).

Lemma norm_hd l : HeadLeEven l (norm l).

Lemma norm_le x l : Delta 1 (x::l) →
  ∀ y, In y (norm (x::l)) → x ≤ y.

Classification of Fibonacci decompositions

For a later theorem (g´_g), we'll need to classify the Fibonacci decompositions according to their lowest terms. Is the lowest rank 2, 3 or more ? Is it even or odd ?
In Low p n k:
  • p is the delta between ranks in the decomposition (usually 2)
  • n is the number we're decomposing
  • k is the lowest rank in the decomposition (we force 1<k).

Definition Low p n k :=
 ∃ l, n = sumfib (k::l) ∧ Delta p (k::l) ∧ 1<k.

Definition Two p n := Low p n 2.
Definition Three p n := Low p n 3.
Definition Four p n := Low p n 4.
Definition High p n := ∃ k, 3 < k ∧ Low p n k.

Definition Even p n := ∃ k, Low p n (2×k).
Definition Odd p n := ∃ k, Low p n (2×k+1).

Some properties of the Low predicate

Lemma Low_exists n : n≠0 → ∃ k, Low 2 n k.

Lemma Low_nz p n k : Low p n k → 1<k.

Lemma Low_unique n k k´ : Low 2 n k → Low 2 n k´ → k = k´.
Lemma Low_21 n k : Low 2 n k → Low 1 n k.

Lemma Low_12 n k : Low 1 n k → ∃ p, Low 2 n (k+2×p).

Lemma Low_le p n k : Low p n k → fib k ≤ n.

Properties specialized to Two, Three, etc

Lemma High_12 n : High 1 n ↔ High 2 n.

Lemma Two_21 n : Two 2 n → Two 1 n.

Lemma Two_12 n : Two 1 n → Two 2 n ∨ High 2 n.

Lemma Three_21 n : Three 2 n → Three 1 n.

Lemma Three_12 n : Three 1 n → Three 2 n ∨ High 2 n.

Lemma decomp_complete n : n≠0 → Two 2 n ∨ Three 2 n ∨ High 2 n.

Lemma Two_not_High n : Two 2 n → ¬High 2 n.

Lemma Two_not_Three n : Two 2 n → ¬Three 2 n.

Lemma High_not_Three n : High 2 n → ¬Three 2 n.

Lemma Two_not_Three´ n : Two 1 n → ¬Three 2 n.

Lemma Two_not_Three´´ n : Two 1 n → ¬Three 1 n.

Lemma High_not_Three´ n : High 1 n → ¬Three 2 n.

Special subdivisions of decompositions starting by 3.

Definition ThreeEven p n :=
 ∃ k l, n = sumfib (3::2×k::l) ∧ Delta p (3::2×k::l).
Definition ThreeOdd p n :=
 ∃ k l, n = sumfib (3::2×k+1::l) ∧ Delta p (3::2×k+1::l).

Lemma ThreeOdd_le n : ThreeOdd 2 n → 6 ≤ n.

Lemma ThreeEven_le n : ThreeEven 2 n → 7 ≤ n.

Lemma ThreeEven_Three p n : ThreeEven p n → Three p n.

Lemma ThreeOdd_Three p n : ThreeOdd p n → Three p n.
Hint Resolve ThreeOdd_Three ThreeEven_Three.

Lemma Three_split p n : 2<n → Three p n → ThreeEven p n ∨ ThreeOdd p n.

Lemma ThreeEven_not_ThreeOdd n : ThreeEven 2 n → ¬ThreeOdd 2 n.

Lemma decomp_complete´ n : 2<n →
 Two 2 n ∨ ThreeEven 2 n ∨ ThreeOdd 2 n ∨ High 2 n.

Lemma ThreeOdd_12 n : ThreeOdd 1 n ↔ ThreeOdd 2 n.

Lemma ThreeEven_21 n : ThreeEven 2 n → ThreeEven 1 n.

Lemma ThreeEven_12 n : ThreeEven 1 n → ThreeEven 2 n ∨ High 2 n.
Lemma Two_not_ThreeOdd n : Two 2 n → ¬ThreeOdd 2 n.

Lemma Two_not_ThreeOdd´ n : Two 1 n → ¬ThreeOdd 2 n.

Lemma High_not_ThreeOdd n : High 2 n → ¬ThreeOdd 2 n.

Lemma High_not_ThreeOdd´ n : High 1 n → ¬ThreeOdd 2 n.

Lemma ThreeEven_not_ThreeOdd´ n : ThreeEven 1 n → ¬ThreeOdd 2 n.

Hint Resolve Two_not_ThreeOdd ThreeEven_not_ThreeOdd High_not_ThreeOdd.
Hint Resolve Two_not_ThreeOdd´ ThreeEven_not_ThreeOdd´ High_not_ThreeOdd´.

Properties of Even and Odd

Lemma Even_or_Odd n : n≠0 → Even 2 n ∨ Odd 2 n.

Lemma Even_xor_Odd n : Even 2 n → Odd 2 n → False.

Lemma Even_12 n : Even 1 n ↔ Even 2 n.

Lemma Odd_12 n : Odd 1 n ↔ Odd 2 n.

Lemma Two_Even p n : Two p n → Even p n.

Lemma Three_Odd p n : Three p n → Odd p n.

Lemma Even_not_ThreeOdd n : Even 2 n → ¬ThreeOdd 2 n.
Hint Resolve Three_Odd Two_Even Even_not_ThreeOdd.

Decomposition of the predecessor of a Fibonacci number

We discriminate according to the parity of the rank:
So we explicitely builds these decompositions:

Definition evens k := map (fun x ⇒ 2×x) (seq 1 k).

Definition odds k := map (fun x ⇒ 2×x+1) (seq 1 k).

Lemma seq_S n k : seq (S n) k = map S (seq n k).

Lemma seq_end n k : seq n (S k) = seq n k ++ [n+k].

Lemma sumfib_evens k :
  sumfib (evens k) = pred (fib (2×k+1)).

Lemma sumfib_odds k :
  sumfib (odds k) = pred (fib (2*(S k))).

Lemma S_evens k : map S (evens k) = odds k.

Lemma evens_S k : evens (S k) = 2 :: map S (odds k).

Lemma evens_in k y : In y (evens k) → 2≤y≤2×k.

Lemma odds_in k y : In y (odds k) → 3≤y≤2×k+1.

Lemma Delta_evens k : Delta 2 (0::evens k).

Lemma Delta_odds k : Delta 2 (1::odds k).

Classification of successor's decomposition


Lemma Two_succ_Three n : Two 2 n → Three 1 (S n).

Lemma Two_succ_Odd n : Two 2 n ↔ Odd 2 (S n).

Lemma Three_succ_Four n : Three 2 n → Four 1 (S n).

Lemma Three_succ_EvenHigh n : Three 2 n → Even 2 (S n) ∧ High 2 (S n).

Lemma High_succ_Two n : High 2 n ↔ Two 2 (S n) ∧ 0<n.

Lemma Odd_succ_Even n : Odd 2 n → Even 2 (S n).

No general result for successor and Even n :

Classification of predecessor's decomposition


Lemma Odd_pred_Two n : Odd 2 n ↔ Two 2 (n-1).
Lemma EvenHigh_pred_Odd n : Even 2 n → High 2 n → Odd 2 (n-1).

Lemma Two_pred_High n : 1<n → Two 2 n → High 2 (n-1).

Lemma Three_pred_Two n : Three 2 n → Two 2 (n-1).

Lemma Four_pred_Three n : Four 2 n → Three 2 (n-1).

Lemma EvenHigh_pred_ThreeOdd n :
 Even 2 n → ¬Two 2 n → ¬Four 2 n → ThreeOdd 2 (n-1).

We can now prove alternate formulations for ThreeOdd and ThreeEven.

Lemma ThreeOdd_alt n :
  ThreeOdd 2 n ↔ Three 2 n ∧ Odd 2 (n-2).

Lemma ThreeEven_alt n :
  ThreeEven 2 n ↔ Three 2 n ∧ Even 2 (n-2).

Two consecutive ThreeOdd numbers are separated by 5 or 8


Lemma ThreeOdd_next n :
  ThreeOdd 2 n → ThreeOdd 2 (n+5) ∨ ThreeOdd 2 (n+8).
Lemma ThreeOdd_add_1 n : ThreeOdd 2 n → High 2 (n+1).

Lemma ThreeOdd_add_2 n : ThreeOdd 2 n → Two 2 (n+2).

Lemma ThreeOdd_add_3 n : ThreeOdd 2 n → ThreeEven 2 (n+3) ∨ High 2 (n+3).

Lemma ThreeOdd_add_4 n : ThreeOdd 2 n → Two 2 (n+4) ∨ High 2 (n+4).

Lemma ThreeOdd_add_6 n : ThreeOdd 2 n → High 2 (n+6).

Lemma ThreeOdd_add_7 n : ThreeOdd 2 n → Two 2 (n+7).

Lemma ThreeOdd_next_5_xor_8 n :
  ThreeOdd 2 (n+5) → ThreeOdd 2 (n+8) → False.

Lemma ThreeOdd_next5 n :
 ThreeOdd 2 n → ThreeOdd 2 (n+5) →
 ∀ m, n<m<n+5 → ¬ThreeOdd 2 m.

Lemma ThreeOdd_next8 n :
 ThreeOdd 2 n → ThreeOdd 2 (n+8) →
 ∀ m, n<m<n+8 → ¬ThreeOdd 2 m.

Lemma ThreeOdd_next_inv n m :
  ThreeOdd 2 n → ThreeOdd 2 m → n < m →
  (∀ p, n < p < m → ¬ThreeOdd 2 p) →
  m = n+5 ∨ m = n+8.