The Coq mailing list

[Sean Wilson <sean.wilson AT ed.ac.uk>]

On Saturday 24 November 2007 15:42:25 you 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.

You can use "inversion Hyp1." to show a contradiction. This will reason that 
there is no possible way that the assumption you have can be constructed 
given the type constructors available.

You can write a quick Ltac tactic to try this on all assumptions:

Ltac absurd_inversion :=
 match goal with
  H:_ |- _ => inversion H; fail
 end.

> If it is just a "omega" tactic, can somebody explain me this error:
>
> User error: Omega: Unrecognized atomic proposition: my_proposition

Can you give an example script that produces this error?

Regards,

Sean