Sum.v

Require Import ZArith.
Require Import Coq.Lists.List.
Require Import Omega.
Import ListNotations.
Local Open Scope Z_scope.

Inductive is_sum : list Z -> Z -> Prop :=
| is_sum_nil : is_sum [] 0
| is_sum_cons : forall y n ns, is_sum ns y -> is_sum (n::ns) (n + y).

Example is_sum_ex1 :
  is_sum [1;2;3] 6.
Proof.
  replace 6 with (1 + (2 + (3 + 0))) by reflexivity.
  repeat constructor.
Qed.

Fixpoint sum_loop acc ns :=
  match ns with
  | [] => acc
  | n::ns' => sum_loop (n + acc) ns'
  end.

Definition sum := sum_loop 0.

Example sum_ex1 :
  sum [1;2;3] = 6.
Proof.
  unfold sum.
  simpl.
  reflexivity.
Qed.

Lemma exists_add :
  forall x y, exists z, x = y + z.
Proof.
  intros x y.
  exists (x - y).
  ring.
Qed.

Lemma is_sum_step :
  forall ns y n, is_sum ns (y - n) -> is_sum (n :: ns) y.
Proof.
  intros.
  assert (exists z, y = n + z) by apply exists_add.
  inversion H0.
  subst.
  constructor.
  replace (n + x - n) with x in H by ring.
  assumption.
Qed.

Lemma sum_loop_is_sum :
  forall ns acc y, sum_loop acc ns = y + acc -> is_sum ns y.
Proof.
  intros ns.
  induction ns; intros acc y H.
  simpl in H.
  replace y with 0 by omega.
  constructor.
  simpl in H.
  specialize (IHns (a + acc) (y - a)).
  replace (y - a + (a + acc)) with (y + acc) in IHns by ring.
  apply IHns in H.
  apply is_sum_step.
  assumption.
Qed.