The Coq mailing list

["Soegtrop, Michael" <michael.soegtrop AT intel.com>]

Dear Coq Users,

 

I have the issue that omega sometimes tries to instantiate evars and fails. See the following example:

 

Require Import Omega.

Require Import ZArith.

 

Open Scope Z_scope.

 

Example Ex1 : forall x:Z, 0<x -> 0<=x.

  intros  x H.

  evar( result : Z ).

  (* works, does not use hypothesis H *)

  let test := constr:( ltac:(omega) : x=x ) in idtac test.

  (* fails, does use hypothesis H *)

  Fail let test := constr:( ltac:(omega) : 0<=x ) in idtac test.

  (* works *)

  omega.

 

What I don’t understand here is why the direct omega at the end works, but trying to solve an identical intermediate goal fails with:

 

The command has indeed failed with message:

Cannot infer an existential variable of type "Z" in environment:

x : Z

 

Can someone shed some light on this mystery?

 

Does someone have a similar construct (without creating a hypothesis like assert does) that works?

 

Thanks & best regards,

 

Michael

Intel Deutschland GmbH
Registered Address: Am Campeon 10-12, 85579 Neubiberg, Germany
Tel: +49 89 99 8853-0, www.intel.de
Managing Directors: Christin Eisenschmid, Christian Lamprechter
Chairperson of the Supervisory Board: Nicole Lau
Registered Office: Munich
Commercial Register: Amtsgericht Muenchen HRB 186928