Library examples.fibonacci

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

Fixpoint fibonacci n :=
  match n with
  | 0 ⇒
      0
  | S n ⇒
      match n with
      | 0 ⇒
          1
      | S 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).