The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

I think [auto] is implementing individual steps more like [simple apply] 
than [apply], so that definition unfolding isn't included, which can pay 
off in improved performance of checking which hints apply for each subgoal.

On 10/09/2016 01:27 PM, Klaus Ostermann wrote:
> I'm trying to understand the behavior of "auto".
>
> My understanding so far was that the following invariant holds:
>
> A proof that consists of a series of "apply" steps, where all applied
> terms are in the
> hints database, can also be solved by "auto" (with sufficient search depth).
>
> However, this doesn't seem to be the case. For instance, consider:
>
> Inductive foo : nat -> Prop :=
>    |  baz : forall n: nat, foo n -> foo (S n)
>    |  z : foo O.
>
> Hint Constructors foo.
>
> Now the following goal can be solved with "auto".
> Goal foo(2). auto. Qed.
>
> This small variant of the goal cannot be solved with "auto".
> But it can be solved by adding an "apply baz" - although "baz" is already
> in the hint database for "auto".
>
> Definition id{A: Set}(x: A) := x.
> Goal foo(id(2)). apply baz. auto.
>
> Does an explicit "apply" do more than an "apply" performed by "auto"?
> What is the explanation of this behavior? And how can I automate a proof
> like the one above such that I don't have to apply baz manually?
>
> Klaus