coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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
- [Coq-Club] problem to prove associativity law with n parameters, coqcdp, 07/29/2014
- Re: [Coq-Club] problem to prove associativity law with n parameters, Jonathan, 07/29/2014
- Re: [Coq-Club] problem to prove associativity law with n parameters, Cedric Auger, 07/29/2014
Archive powered by MHonArc 2.6.18.