Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Automatic finding false hypothesis

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Automatic finding false hypothesis


chronological Thread 
  • 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





Archive powered by MhonArc 2.6.16.

Top of Page