Coq: Proof of list pair

Question

I have wrote this Inductive predicate and part of the proof for its (strong) specification:

Inductive SumPairs : (nat*nat) -> list (nat*nat) -> Prop :=
| sp_base : SumPairs (0,0) nil
| sp_step : forall (l0:list (nat*nat)) (n0 n1: nat) (y:(nat*nat)), SumPairs (n0,n1) l0 -> SumPairs ((n0+(fst y)),(n1+(snd y))) (cons y l0).

Theorem sumPairs_correct : forall (l:list (nat*nat)), { n: nat | SumPairs (n,n) l }.
Proof.
...

The thing is I don't think the theorem is correct because Coq doesn’t accept something like {n0 n1: nat | ...}. Is there a way to fix that or am I thinking wrong?

I think the predicate SumPairs is correct, but since I'm not sure, here's an example of how it should work: input [(1,2),(3,4)], expected output [3,7]

Answer 1

You could put a pair in the result, e.g.:

Inductive SumPairs : (nat*nat) -> list (nat*nat) -> Prop :=
| sp_base : SumPairs (0,0) nil
| sp_step : forall (l0:list (nat*nat)) (n0 n1: nat) (y:(nat*nat)), SumPairs (n0,n1) l0 -> SumPairs ((n0+(fst y)),(n1+(snd y))) (cons y l0).

Theorem sumPairs_correct : forall (l:list (nat*nat)), { p: nat * nat | SumPairs p l }.
Proof.
intros l.
induction l as [|p l [[x y] IH]].
- exists (0, 0); constructor.
- now exists (x + fst p, y + snd p); constructor.
Qed.

However, for this particular task, it is actually better to just use a plain functional program:

Require Import Coq.Lists.List.

Definition sum_list l := fold_left Nat.add l 0.

Definition sum_pairs l := (sum_list (map fst l), sum_list (map snd l)).

This definition is easier to read, to understand and to modify than the first version. Note that you can still use Coq to reason about the function:

Lemma sum_list_cat l1 l2 : 
  sum_pairs (l1 ++ l2) = 
  (fst (sum_pairs l1) + fst (sum_pairs l2),
   snd (sum_pairs l1) + snd (sum_pairs l2)).
(* Exercise! *)