Library examples.fibonacci

Require Import zoo.prelude.
Require Import zoo.options.

Fixpoint fibonacci n :=
  match n with
  | 0 ⇒
      0
  | ˖n ⇒
      match n with
      | 0 ⇒
          1
      | ˖m ⇒
          fibonacci n + fibonacci m
      end
  end.
#[global] Arguments fibonacci !_ /.

Lemma fibonacciｰspec n :
  fibonacci n =
    if decide (n ≤ 1) then
      n
    else
      fibonacci (n - 1) + fibonacci (n - 2).
Lemma fibonacciｰspecｰZ n :
  (0 ≤ n)%Z →
  fibonacci ₊n =
    if decide (n ≤ 1)%Z then
      ₊n
    else
      fibonacci ₊(n - 1) + fibonacci ₊(n - 2).

Lemma fibonacciｰbase n :
  n ≤ 1 →
  fibonacci n = n.
Lemma fibonacciｰrecursive n :
  1 < n →
  fibonacci n = fibonacci (n - 1) + fibonacci (n - 2).