sum'.v

Fixpoint sum (l : list nat) : nat :=
  match l with
  | nil => 0
  | cons x xs => x + sum xs
  end.

Fixpoint sum_tail' (l : list nat) (acc : nat) : nat :=
  match l with
  | nil => acc
  | cons x xs => sum_tail' xs (x + acc)
  end.

Definition sum_tail (l : list nat) : nat :=
  sum_tail' l 0.

Fixpoint sum' (l : list nat) (acc: nat) : nat :=
  match l with
  | nil => acc
  | cons x xs => x + sum' xs acc
  end.

Lemma sum_sum':
  forall l, sum l = sum' l 0.
Proof.
  induction l; auto.
  simpl. rewrite IHl; auto.
Qed.

Lemma sum'_equation:
  forall l x acc,
    sum' (cons x l) acc = sum' l (x + acc).
Proof.
  induction l; intros; auto.
  simpl. rewrite <- IHl; simpl. omega.
Qed.

Lemma sum_tail_sum':
  forall l acc,
    sum_tail' l acc = sum' l acc.
Proof.
  induction l; intros; auto.
  rewrite sum'_equation. simpl. auto.
Qed.

Theorem sum_tail_correct:
  forall l, sum_tail l = sum l.
Proof.
  intros; unfold sum_tail; rewrite sum_tail_sum'.
  symmetry; apply sum_sum'.
Qed.