coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Beginner's question: how to prove m+n = n+m

From: Adam Koprowski <adam.koprowski AT gmail.com>
To: "Zhoulai.FU AT X.org" <zhoulai.fu AT polytechnique.org>
Cc: coq-club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Beginner's question: how to prove m+n = n+m
Date: Mon, 1 Mar 2010 17:33:26 +0100
Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:in-reply-to:references:from:date:message-id:subject:to :cc:content-type; b=vsT6AoKcY3oLO3fCRLAjSZyNSZELfgyurj/iqL2MbqVnXoiYC1nbp3/lemt1XfVSMz tj1cuQPsO5iHm8yPRQ5ed5vkLJjU+keg9KUo0cfMrzt3xTKLp8A2eUw7pge60BuDEfGV edI0aQrlhsBUlP99aN+nj5414URhchdOYeh3o=

��Dear Zhoulai,�

I agree that it is not a hard work if we introduce a lemma as you said. However to do that,� if I understand well , you may probably have to use something like this
**************
[rewrite] [lemma_name]
**************
But the "rewrite" learned till now does not have that syntax. It can only rewrite
syntactically something following a rule indicated by a hypothesis.

��There is no new syntax involved. In fact you can use any lemma in pretty much the same way as you can use any of your local hypotheses. As an analogy you can think of calling a locally bound function VS calling a top-level function in a functional programming language of your choice.�

��More importantly: recognizing and abstracting away crucial lemmas in your proofs is one of the most important things needed to have clean & well-structured theories. This theorem naturally asks for such a separate lemma so why not having it?

��Best,

��Adam

--
Adam Koprowski � [http://www.cs.ru.nl/~Adam.Koprowski]
R&D @ MLstate � �[http://mlstate.com, 15 rue Berlier, 75013 Paris, France]

[Coq-Club] Beginner's question: how to prove m+n = n+m, zell08v
- Re: [Coq-Club] Beginner's question: how to prove m+n = n+m, Adam Koprowski
  - Re: [Coq-Club] Beginner's question: how to prove m+n = n+m, Zhoulai.FU AT X.org
    - Re: [Coq-Club] Beginner's question: how to prove m+n = n+m, gallais @ EnsL
      - Re: [Coq-Club] Beginner's question: how to prove m+n = n+m, Zhoulai.FU AT X.org
        
        Re: [Coq-Club] Beginner's question: how to prove m+n = n+m, Guilhem Moulin
        
        Re: [Coq-Club] Beginner's question: how to prove m+n = n+m, Adam Koprowski
- Re: [Coq-Club] Beginner's question: how to prove m+n = n+m, Jean-Marc Notin