The Coq mailing list

[Claude Marche <Claude.Marche AT lri.fr>]

Hi,

I guess the Omega module adds some new hints in the zarith hint base,
and as for any other module, it may or may not be clearly documented.

Anyway, to make the omega tactic solve your goal when hypotheses are
inconsistant, you could do 

casetype False; omega.

- Claude

>>>>> "Brian" == Brian Emre Aydemir 
>>>>>Â <baydemir AT cis.upenn.edu>
>>>>>  writes:

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

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

    Brian> Cheers,
    Brian> Brian

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

    Brian> --------------------------------------------------------
    Brian> Bug reports: http://coq.inria.fr/bin/coq-bugs
    Brian> Archives: http://pauillac.inria.fr/pipermail/coq-club
    Brian>           http://pauillac.inria.fr/bin/wilma/coq-club
    Brian> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club

-- 
| Claude Marché           | 
mailto:Claude.Marche AT lri.fr
 |
| LRI - Bât. 490          | http://www.lri.fr/~marche/  ;|
| Université de Paris-Sud | phoneto: +33 1 69 15 64 85  |
| F-91405 ORSAY Cedex     | faxto: +33 1 69 15 65 86    |