The Coq mailing list

[Marko Malikovi� <marko AT ffri.hr>]

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
-------------------------