The Coq mailing list

[Edsko de Vries <devriese AT cs.tcd.ie>]

On Sat, Nov 24, 2007 at 04:42:25PM +0100, Marko Malikovi? wrote:
> Greetings,
> 
> is there some another tactic (except "omega") which can automatically find
> false hypothesis in form of inequality and solve the goal, for example:
> 
> Hyp1 : 5>6
> 
> I know just ident of hypothesis ("Hyp1") but not his statement (we don't
> know is it 5>6 or 100<=50). So, "absurd" tactic is not enough.
> 
> If it is just a "omega" tactic, can somebody explain me this error:
> 
> User error: Omega: Unrecognized atomic proposition: my_proposition

You can use Omega for this if you use 'apply False_ind' first:

  Require Import Omega.
  
  Section test.
  
  Variable P : Prop.
  
  Hypothesis H : 5 > 6.
  
  Lemma p : P.
  apply False_ind ; omega.
  Qed.
  
  End test.

Hope that helps,

Edsko