The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

On 05/21/2015 03:03 PM, Jason Gross wrote:
> [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.

OK - the diagnosis was off, but the prognosis remains - auto isn't 
monotonic.  And that not-backtracking-across-solved-goals issue also is 
a pain - or, rather, is the primary pain - because full backtracking 
across solved goals would imply monotonicity.

I'm considering a way around this - it would involve using Print HintDb 
to dump hints to a file.  Then parse the file to create a new Coq script 
that would add the hints to a new db - but with all hints for the same 
head symbol ("hintlets") put into a single "+" hint, like so:

Hint Extern 1 (_ <= _) => (apply len_n + apply le_S) : newdb.

perhaps with the order of hintlets in each hint "+" tactical ordered by 
their original cost (or order in the original db if the same cost), with 
the overall hint cost being that of the lowest cost included hintlet.

I think the resulting db should fully backtrack across goals (and so 
also be monotonic) - at least for auto, which is currently the only 
automation tactic that can backtrack within a "+" tactical.

Sound promising?  (If this sounds desperate that's because it is. ;)

-- Jonathan