The Coq mailing list

[Pierre Courtieu <Pierre.Courtieu AT cnam.fr>]

The goal of eauto is precisely to leave some unsolved existentials
that should be instantiated by following tactics's side effects. This
is at the same time ugly and very useful sometimes. It breaks the nice
tree-likeness of proof scripts (see below my opinion on automatic
tactics anyway) but it sometimes avoids giving big and tedious
arguments to (e)apply.

Problem here is that there is no other goal because the only unsolved
existential is not detected as such. So no tactic side effect can
instantiate it. If this is not the consequence of a badly stated
lemma, you can instantiate it by yourselve like this (only tested on
trunk only):

Show Existentials.
Existential 1 := tt.

Or by going back and replacing eauto by an explicite apply. Actually
my opinion is that (e)auto (and other automatic tactics) should always
be used as proof search commands quickly replaced by the succeeding
tactics they found (side effect: faster scripts, no dependence on hint
databases). And yes interfaces should help with this, this is on my
todo list for proofgeneral.

Regards,
Pierre

2011/11/30 Paolo Herms 
<paolo.herms AT inria.fr>:
> Hello,
> I've got a real example which reduces to this one:
>
> Definition True2  := True.
> Definition def (u:unit) (P: Prop) := P.
> Lemma lem u: def u True -> True2.
>  auto.
> Save.
> Hint Unfold def.
> Hint Resolve lem.
> Goal True2.
>  eauto.
> Fail Save.
>
> I think the call to eauto shouldn't do anything here, as it cannot 
> completely
> solve the goal. Or are there situations where you want this behaviour?
>
> --
> Paolo Herms
> PhD Student - CEA Software Safety Lab. / INRIA ProVal Project
> Paris, France
>
>