The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

> 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