The Coq mailing list

[Jonathan <jonikelee AT gmail.com>]

On 07/29/2014 10:40 AM, coqcdp wrote:

Hi,
      Recently I want to prove associativity law in algebra ,I have proved that with 3 parameters,but I don't know how to prove that with arbitrary n parameters. for example I can prove  (a+b)+c = a +(b+c)  with coq , but  I don't know how to prove  or  formalize (a1+a2)+...+an=a1+(a2+a3)+...+an=...=a1+a2+...+(an-1+an). I hope you can give me some suggestions. Thank you .
    
        Yours Sincerely ,
                                   D.P.Chen

Once you have the basic associativity law proved, the rest are just repeated applications of that law.  For example:

Require Import Arith.

Goal forall (a b c d e : nat), a + (b + (c + d)) + e = (a + b) + (c + (d + e)).
intros.
repeat rewrite plus_assoc.
reflexivity.
Qed.

The rewrite plus_assoc is defined as an alias for Nat.add_assoc, which is defined as:

add_assoc : forall n m p : nat, n + (m + p) = n + m + p

So, there is no reason to prove more complex variations, as the single assoc law can handle all cases itself.

-- Jonathan