The Coq mailing list

[Klaus Ostermann <klaus.ostermann AT uni-tuebingen.de>]

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