The Coq mailing list

[Georgi Guninski <guninski AT guninski.com>]

Possible workaround is to manually add
pose proof A.
before omega.

-- 
joro

On Sat, Jul 30, 2011 at 10:12:20AM +0200, Marko Maliković wrote:
> Greetings,
> 
> Can someone explain to me whether is the standard that omega does not take
> the axioms into account (or there is another problem in the example
> Test1):
> 
> Section Test1.
> Require Import Omega.
> Parameter x : nat.
> Axiom A : x < 2 \/ x > 5.
> Hypothesis H1 : x <> 0.
> Hypothesis H2 : x < 6.
> Goal x = 1.
> omega.
> Error: Omega can't solve this system
> 
> But, if I introduce axiom A as an hypothesis then omega solve this problem:
> 
> Section Test2.
> Require Import Omega.
> Parameter x : nat.
> Hypothesis A : x < 2 \/ x > 5.
> Hypothesis H1 : x <> 0.
> Hypothesis H2 : x < 6.
> Goal x = 1.
> omega.
> Proof completed.
> 
> Thank you,
> 
> Marko Maliković
> 
> -----------------------
> Dr. Sc. Marko Maliković
> Filozofski fakultet
> Sveučilište u Rijeci
> ---------------------
> Ph.D. Marko Maliković
> Faculty of Humanities and Social Sciences
> University of Rijeka, Croatia
> -----------------------------
> marko AT ffri.hr
> http://www.ffri.hr/~marko
> -------------------------