coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Does Omega Support N?

From: Alexandre Pilkiewicz <alexandre.pilkiewicz AT polytechnique.org>
To: Gregory Malecha <gmalecha AT eecs.harvard.edu>
Cc: Coq Club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Does Omega Support N?
Date: Sun, 27 Mar 2011 16:31:42 +0200
Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:sender:in-reply-to:references:from:date :x-google-sender-auth:message-id:subject:to:cc:content-type; b=qufAN/L1fkS27965lwjc2q5NzwdWOja865+m+JCVE4KfsqsFZrqUTXo90mG5xlduit UCbw1g0wvCvVw8t3uY6BFOeZacwRGbifU/Os2Ai0sTxGXSVXJUE7JaiR2Y/5W4FWbO+n 1ylYp5N7Fq9ECN0Uyo3gaNsSz+6dp2DiDYDd0=

One solution is to use the slightly undocumented tactic "zify"

Require Import Omega.

Goal forall (n1 n2: N), (n1 + n2 >= n1)%N.
Proof.
intros. zify. omega.
Qed.

2011/3/27 Gregory Malecha
<gmalecha AT eecs.harvard.edu>:
> Does the omega tactic support reasoning about N and if so, what do I need to
> do to get this behavior? I noticed that the documentation mentions nat and
> Z, but not N.
> Thanks
> --
> gregory malecha
>

[Coq-Club] Does Omega Support N?, Gregory Malecha
- Re: [Coq-Club] Does Omega Support N?, Alexandre Pilkiewicz