The Coq mailing list

[Matthew Brecknell <matthew AT brecknell.net>]

Hi Babak,

You wrote:
> I have defined two functions in Coq: "add" and "mult" recursively.
> 
> they are functions for lists of pairs.  a pair is like (a,b), and a
> list of pairs is like 
> 
> (a_1,b_1)::(a_2,b_2):: ... ::(a_n, b_n)::nil
> 
> mult function multiplies each b_i by a constant m. 
> 
> (a_1,m*b_1)::(a_2,m*b_2):: ... ::(a_n, m*b_n)::nil
> 
> add function adds two lists in this way:
> suppose we have 
> 
> l1 = (a_1,b_1)::(a_2,b_2):: ... ::(a_n, b_n)::nil
> l2 = (a_1,b'_1)::(a'_2,b'_2):: ... ::(a'_n, b'_n)::nil
> 
> add function adds b_i's with a special rule and gives a new list of
> pairs.
> 
> now I want to prove that
> 
> mult m (add l1 l2) = add (mult m l1) (mult m l2)
> 
> but since both of my functions are recursively defined, I cannot prove
> it. Is there a special tactic for this?

Recursive functions must follow the structure of an inductive datatype,
so proofs of properties of those functions are usually by induction over
the respective inductive datatype, using the "induction" tactic:

http://www.lix.polytechnique.fr/coq/refman/Reference-Manual011.html

I guess your "mult" and "add" are structurally similar to "map" and
"combine" from the List library:

http://coq.inria.fr/stdlib/Coq.Lists.List.html

In that case, your proof should be structured something like this:

Require Import List.

Set Implicit Arguments.

Definition pairwise A B (f: A -> B) (p: A*A) : (B*B) :=
  let (a0,a1) := p in (f a0, f a1).

Lemma map_combine: forall A B (f: A -> B) (ps qs: list A),
  map (pairwise f) (combine ps qs) = combine (map f ps) (map f qs).
Proof.
  induction ps; destruct qs; simpl in *; try rewrite IHps; trivial.
Qed.

You might find it useful to express your "mult" and "add" in terms of
"map" and "combine", so you can make use of a lemma like this.

Regards,
Matthew