A Fibonacci word is a string of binary digits that follows specific rules.

The rules are:

• The first Fibonacci word $S_0=0S\_0\; =\; 0$.
• Each subsequent word is computed by mapping each symbol with $\varphi \backslash phi$, where:
  $\varphi (0)=01\varphi (1)=0\backslash phi(0)\; =\; 01\; \backslash \backslash \; \backslash phi(1)\; =\; 0$

Here are the first few Fibonacci words:

An interesting fact – which gives us the name "Fibonacci word" – is that each word is the concatenation of the previous two:

Prove that this is the case.

A note about Lean

In Lean, the symbols 0 and 1 are represented by ff and tt respectively.

Preloaded

import data.list
import data.stream.defs

def phi : bool → list bool
| ff := [ff, tt]
| tt := [ff]

def fword_aux (s : list bool) := list.bind s phi

def fword : ℕ → list bool := stream.iterate fword_aux [ff]

def SUBMISSION := ∀ n, fword (n + 2) = fword (n + 1) ++ fword n

From Coq Require Import Lists.List.
Import ListNotations.

Definition phi (b : bool) : list bool :=
  match b with
  | false => [false; true]
  | true => [false]
  end.

Definition fword_aux (l : list bool) : list bool :=
  flat_map phi l.

Definition fword (n : nat) : list bool :=
  Nat.iter n fword_aux [false].