The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

This statement appears in Adam Chlipala's CPDT, in the Proof Search by 
Logic Programming section:

> This "non-monotonicity" of rewrite hints contrasts with the situation 
> for auto, where new hints may slow down proof search but can never 
> "break" old proofs.

However, this isn't the case, as illustrated here (using 8.5):

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]. (*some hint in the core db prevents 
solution here*)
auto with nocore mydb.
Qed.


The question is - which should be right?  Should auto (but not eauto) 
have the monotonicity of hints property, or not?  That property would 
certainly be nice to have in many cases, as it would make the 
introduction of new hints less dangerous with respect to maintainability 
and modularity.

-- Jonathan