The Coq mailing list

[Brian Emre Aydemir <baydemir AT cis.upenn.edu>]

Hi,

I have noticed the following behavior about the Omega module.  
Sometimes I have a subgoal where the equality is a conclusion on 
something other than terms of type nat or Z, and where the hypotheses 
include (n < k) and (n >= k) for n and k arbitrary natural numbers (a 
contradiction that makes the subgoal trivially true).

"auto with *" fails to do anything.  So then I try including the Omega 
module.  "omega" fails to solve the subgoal (it complains about the 
equality).  However, now "auto with *" will solve it!  It seems that 
the Omega module modifies the resources used by the auto tactic.  I 
discovered this by accident.  Is this behavior documented anywhere?  I 
couldn't find anything after looking in the Coq reference manual, 
specifically Chapter 17, for information on Omega.

Cheers,
Brian

--
Brian Emre Aydemir
http://www.cis.upenn.edu/~baydemir/