The Coq mailing list

[AUGER Cédric <sedrikov AT gmail.com>]

Le Sat, 21 Sep 2013 02:37:07 +0000,
t x 
<txrev319 AT gmail.com>
 a écrit :

> Quoting the end of section 8.8.1,
> 
> 
> http://coq.inria.fr/refman/Reference-Manual010.html#hevea_command234
> 
> 
> Remark: auto either solves completely the goal or else leaves it
> intact. auto and trivial never fail.
> 
> 
> I can understand the motivation of this -- to avoid auto accidently
> making a provable state unprovable.

I do not think that is the motivation.

[intuition] tactic for instance does not leave the goal intact and
still does not change the provability of the goal (all operations
performed by induction can be reverted).

[easy] tactic also cannot make a goal unprovable but can fail.

For me the motivation is to provide a way to never fail, so some
progression can be achieved in scripts, and still have some control on
the predictability by never modifying the context (no new hypothesis
introduced, no hypothesis lost, no new goal to prove in a state you
have to guess why coq wanted you to prove it).

> 
> 
> However, suppose that I have designed my Hint Externs in such a way
> that they never go from provable state to unproable state, is there
> something like:
> 
> 
> "auto, try try to make progress; and if you get stuck, don't
> rollback" ?
> 
> Thanks!
> 
> (In particular, I have a situation that can not be completedly solved
> by auto, but I'd like to keep the progress it has made (by checking
> the Ltac debug)).