The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

On 02/27/2015 12:27 PM, Soegtrop, Michael wrote:
> 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.

What you need is the "new_evars_as_subgoals" part of enhancement request 
3872.

> 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.

I've tried "Declare Implicit Tactic", but have not managed to get it to 
work in such cases.  I think that's because the arguments in question 
are not implicit, just shelved by the choice of tactics within eauto.

Note that the problem is actually with the hypothesis H.  When eauto 
applies it, it effectively does [eapply H] instead of something more 
controlled like [refine (H _)].

Maybe if you write an extern hint with low enough cost to find 
hypotheses and try refining them with the right number of holes, that 
will fire prior to eauto's automatic use of eapply:

If you want a way to use refine when you don't know the right number of 
holes:

Ltac Refine_limit := constr:(100).
Ltac Refine term :=
  let RL:=Refine_limit in
  let rec f x n :=
      tryif constr_eq n RL
      then fail "Refine exceeded" RL "_'s"
      else tryif refine x then idtac else f uconstr:(x _) (S n)
  in f term 0.

This allows one to write [Refine f] without knowing in advance how many 
"_"'s to use for f.

So, the hint would be something like:

Hint Extern 0 => match goal with H:_ |- _ => Refine H end.

Nope - that doesn't work - probably because the tendency for eauto is to 
eapply local hyps is at lower than 0 cost.

Oh - but as has been pointed out - Coq has three (at last count) 
different automation routines!  In this case, this is fortunate, as:

  Hint Resolve Lemma1.
  typeclasses eauto with core.

works without anything left on the shelf.

-- Jonathan