coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] newbie question

From: "Balazs Vegvari" <balazs.vegvari AT gmail.com>
To: "Adam Chlipala" <adamc AT hcoop.net>
Cc: coq-club AT pauillac.inria.fr
Subject: Re: [Coq-Club] newbie question
Date: Thu, 28 Aug 2008 07:17:15 +0200
Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=message-id:date:from:to:subject:cc:in-reply-to:mime-version :content-type:content-transfer-encoding:content-disposition :references; b=i0IqSZ07YUO2Hf32hKx4ZdTF/9uS31fQmIO5gIKzc3tUS8TRG3sriRNsKavyMpXwFy ZH9UU1Mc+rPGemsh1vR95tsGujnlXyjau0P6wqZVuVeP10oNFlKlEZXL90JnI7r9gm5J 3Cmp4WykwB+EaY8J86cvX4viphHoe+wp1Y80s=
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

Hi Adam,

It worked, I really have to learn a lot.

thanks,
Balazs

On Thu, Aug 28, 2008 at 12:06 AM, Adam Chlipala
<adamc AT hcoop.net>
wrote:
> Balazs Vegvari wrote:
>>
>> I am just learning coq and I don't kow how to prove this:
>>
>> forall x y : Z, x <= y + 1 -> x <= y \/ x = y + 1
>>
>> Any suggestion is welcome.
>>
>
> Did you have a particular constraint on the proof technique in mind? Your
> theorem statement falls into the theory of "quantifier-free linear
> arithmetic," which is one of the most widely-used decidable theories. The
> [omega] tactic solves it instantly (after [intros]).
>

[Coq-Club] newbie question, Balazs Vegvari
- Re: [Coq-Club] newbie question, Adam Chlipala
  - Re: [Coq-Club] newbie question, Balazs Vegvari
    - Re: [Coq-Club] newbie question, Balazs Vegvari
      - Re: [Coq-Club] newbie question, Adam Chlipala
      - Re: [Coq-Club] newbie question, Yves Bertot
        
        Re: [Coq-Club] newbie question, Fr�d�ric Besson