The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

I've had similar issues in the past with omega and ring. However, I 
haven't seen a case like this, where the evar is just in a local def 
that isn't used - in fact I was relying on such cases to not fail as I 
typically "factor out evars" (into local defs) before trying omega or ring.

-- Jonathan


On 09/22/2016 08:32 AM, Soegtrop, Michael wrote:
> 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