The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

[auto] does not backtrack across solved goals.  Here is what's going on:*

When [le_n] has a lower cost than [le_S], it gets run immediately on the left goal.  [1 <= 0] is not solvable, so [auto] as a whole fails.

When [le_S] gets run before [le_n], [auto] will eat its stack trying to apply [le_S], notice, when its stack is gone, that the goal is not solved, backtrack to the next hint at the bottom, and apply [le_S].  So then the right side is provable, because it's [1 <= 3] if you use [auto with nocore mydb], or [1 <= 8] if you use [auto 10 with nocore mydb].

Here's what I ran:

Require Import Coq.Strings.String.

Ltac idtac_goal n :=

    match goal with |- ?G => idtac n G end;

    try match goal with H := ?T |- _ => idtac T end.

Hint Extern 1 (_ /\ _) => idtac_goal 0; apply conj; [ pose "left"%string | pose "right"%string ] : mydb.

Hint Extern 1 (_ <= _) => idtac_goal 1; apply le_n : mydb.

Hint Extern 1 (_ <= _) => idtac_goal 2; apply le_S : mydb.

Hint Extern 1 (_ = _) => idtac_goal 3; reflexivity : mydb.

Goal exists x, 0<=x /\ 1<=x.

eexists.

try auto 10 with nocore mydb.

On Thu, May 21, 2015 at 2:43 PM, Jonathan Leivent <jonikelee AT gmail.com> wrote:

Upon examining this more closely - it looks like auto is failing to be monotonic (at least) because it isn't backtracking 0-cost hints. For instance:

Hint Extern 1 (_ /\ _) => apply conj : mydb.
Hint Extern 1 (_ <= _) => apply le_n : mydb.
Hint Extern 1 (_ <= _) => apply le_S : mydb.
Hint Extern 1 (_ = _) => reflexivity : mydb.

Goal exists x, 0<=x /\ 1<=x.
eexists.
Fail solve [auto with mydb].
solve [auto with nocore mydb].
Undo.
Hint Extern 0 (_ <= _) => apply le_n : mydb.
Fail solve [auto with nocore mydb]. (*above 0-cost hint prevents solution*)
Abort.

Is this a bug in auto?

-- Jonathan

That's not quite right, either.  The above case where all costs are increased by any N - so that the costs of the initial 4 hints are N+1 and the cost of the blocking hint is H - also fails.  In other words, the non-monotonicity-inducing behavior is that auto won't backtrack a hint at cost N for a hint at cost >N.

I thought that costs were just to induce an order of proof search for performance reasons.

-- Jonathan