coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Sean Wilson <sean.wilson AT ed.ac.uk>
- To: Marko Malikovi� <marko AT ffri.hr>
- Cc: coq-club AT pauillac.inria.fr
- Subject: Re: [Coq-Club] Automatic finding false hypothesis
- Date: Sat, 24 Nov 2007 20:57:42 +0000
- List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
- Organization: School of Informatics, The University of Edinburgh
On Saturday 24 November 2007 17:51:29 Marko Malikoviæ wrote:
> Thanks for Sean and Edsko for solutions,
>
> Anyway, Sean asked me for example and here is one very simple:
>
> Coq < Parameter valid_prop : Prop.
> valid_prop is assumed
>
> Coq < Require Import Omega.
>
> Coq < Goal 2>100 -> valid_prop.
> 1 subgoal
>
> ============================
> 2 > 100 -> valid_prop
>
> Unnamed_thm < intro.
> 1 subgoal
>
> H : 2 > 100
> ============================
> valid_prop
>
> Unnamed_thm < omega.
> Toplevel input, characters 0-5
>
> > omega.
> > ^^^^^
>
> User error: Omega: Unrecognized atomic proposition: valid_prop
I've run into this problem too. It seems that if your conclusion is not a
statement about natural numbers, omega will just fail with the obscure
message that you see. You would expect it to look for a linear arithmetic
contradiction in the assumptions but it just fails. I used to do (absurd (0
<> 0);omega) to make omega find the contradiction but Edsko's snippet is more
efficient.
You could wrap up this trick in a tactic so omega works the way you expect it
to (i.e. solves the goal or finds a contradiction when it can):
Ltac omega2 := omega || (apply False_ind ; omega).
Regards,
Sean
- [Coq-Club] Automatic finding false hypothesis, Marko Malikoviæ
- Re: [Coq-Club] Automatic finding false hypothesis, Sean Wilson
- Re: [Coq-Club] Automatic finding false hypothesis,
Edsko de Vries
- Re: [Coq-Club] Automatic finding false hypothesis,
Marko Malikoviæ
- Re: [Coq-Club] Automatic finding false hypothesis, Sean Wilson
- Re: [Coq-Club] Automatic finding false hypothesis,
Marko Malikoviæ
Archive powered by MhonArc 2.6.16.