The Coq mailing list

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

Dear Coq users,

sometimes when I run eauto, I end up with a few shelved evars, which are 
trivial to solve, e.g. just a nat. This happens e.g. in the following 
simplified use case:

        Parameter f : nat -> nat.
        Parameter Lemma1 : forall m n : nat, f m <> 0 -> f n <> 0.

        Lemma Test1: (forall m : nat, f (S m) <> 0) -> (forall n : nat, f n 
<> 0).
        Proof.
          intros H n.
          eauto using Lemma1.

At the end of the proof I have to do 

        Unshelve.
          exact 0.

This is a bit inconvenient because Unshelve is a vernacular command, not 
Ltac, so it cannot be embedded in a scripts and automated.

The only automated method I came up with is to initially create an artificial 
extra goal and when solving this goal search for evars and instantiate them, 
but this is bit complicated.

Is there some elegant way to say "if you need a nat, take 0"? I tried 
"Declare Implicit Tactic assumption" but this doesn't work, although a nat is 
among the Hypothesis. 

Thanks & best regards,

Michael