coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] question about a simple arithmetic theorem

From: Evgeny Makarov <emakarov AT gmail.com>
To: coq-club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] question about a simple arithmetic theorem
Date: Wed, 22 Jun 2011 20:10:02 +0200
Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:in-reply-to:references:date:message-id:subject:from:to :content-type; b=UJeub867aq9OqEiu2SGs1S9zIWGDpHld8jP33F6lMzpSdPM/nxAg2PcseVw3Xulxxe 4Ld1GYwV68K4t2aHZVR+qkks+Vmysn8mz5nQrVAG/nHlZBiJnKIK2YFe8kSdZK4Xguew 5fnTyezBDaPo+VoPZs0/Z9Gq7WCPKplqCmWIk=

Hi, Leo,

You have to do two things: (1) make le_plus_minus use n and m from the
current context as arguments and (2) say that you only need to rewrite
the first occurrence of m. Suppose the proof starts by

intros n m H.

Then (le_plus_minus n m H) or simply (le_plus_minus _ _ H) has the
type m = n + (m - n), The rewrite tactic accepts "at occurrences"
modifier which makes it rewrite only the specified occurrence of the
left-hand side. Occurrences are numbered left to right starting from
1. (See the reference manual.) So you can say

rewrite (le_plus_minus _ _ H) at 1.

Evgeny

[Coq-Club] question about a simple arithmetic theorem, leonardomatiasrodriguez
- Re: [Coq-Club] question about a simple arithmetic theorem, Evgeny Makarov
  - Re: [Coq-Club] question about a simple arithmetic theorem, Leonardo Rodriguez
- Re: [Coq-Club] question about a simple arithmetic theorem, Adam Chlipala
  - Re: [Coq-Club] question about a simple arithmetic theorem, Leonardo Rodriguez