Require Import PeanoNat Nat.

From Typonomikon Require Import D5a.

Module Fib.

Fixpoint fib (n : nat) : nat :=
match n with
| 0 => 0
| 1 => 1
| S (S n' as n'') => fib n'' + fib n'
end.

Fixpoint fib_tailrec_aux (n : nat) (a b : nat) : nat :=
match n with
| 0 => a
| S n' => fib_tailrec_aux n' b (a + b)
end.

Lemma fib_tailrec_aux_S :
  forall n a b : nat,
    fib_tailrec_aux (S n) a b = fib_tailrec_aux n b (a + b).

Compute fib_tailrec_aux 7 1 2.

Lemma fib_SS :
  forall n : nat,
    fib (S (S n)) = fib (S n) + fib n.

Definition fib_tailrec (n : nat) := fib_tailrec_aux n 0 1.

Lemma fib_tailrec_aux_spec :
  forall n k : nat,
    fib_tailrec_aux k (fib n) (fib (1 + n)) = fib (k + n).

Lemma fib_tailrec_spec :
  forall n : nat, fib_tailrec n = fib n.

End Fib.

Fixpoint app_tailrec_aux {A : Type} (l acc : list A) : list A :=
match l with
| [] => acc
| h :: t => app_tailrec_aux t (h :: acc)
end.

Definition app' {A : Type} (l1 l2 : list A) : list A :=
  app_tailrec_aux (app_tailrec_aux l1 []) l2.

Lemma app_tailrec_aux_spec :
  forall (A : Type) (l1 l2 : list A),
    app_tailrec_aux l1 l2 = rev l1 ++ l2.

Lemma app'_spec :
  forall (A : Type) (l1 l2 : list A),
    app' l1 l2 = l1 ++ l2.

Definition rev' {A : Type} (l : list A) : list A :=
  app_tailrec_aux l [].

Lemma rev'_spec :
  forall {A : Type} (l : list A),
    rev' l = rev l.