Skip to Content.
Sympa Menu

coq-club - [Coq-Club] problem to prove associativity law with n parameters

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] problem to prove associativity law with n parameters


Chronological Thread 
  • From: coqcdp <coqcdpnxj AT 163.com>
  • To: coq-club <coq-club AT inria.fr>
  • Subject: [Coq-Club] problem to prove associativity law with n parameters
  • Date: Tue, 29 Jul 2014 22:40:08 +0800 (CST)

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





Archive powered by MHonArc 2.6.18.

Top of Page