The Coq mailing list

[Judicael Courant <Judicael.Courant AT lri.fr>]

Dear Nicolas,

You wrote:

> One may wonder whether it is reasonable that the behavior of "Auto"
> relies on some external tactics (here Auto with arith relies on
> Omega);
> these external tactics are called when basic operations performed
> by Auto have failed to solve the goal(s).

I think the point is rather that automated tactic often have fuzzy 
(hence moving) specifications. When upgrading coq, you can reasonnably 
expect the new version to solve as many goals as the previous one, ... 
and possibly more!

In order to protect yourself against bad consequences of these 
improvements, you can of course try to avoid these tactics, but I think 
there are better ways: just never leave a failing "Auto" in your 
developments.

For instance, you can rewrite your proof of "test" in a more robust 
fashion as follows:

1) first way: avoid applying automated tactic to several goals at once
Apply A2.
Solve Auto with zarith. (* Solve is not needed but will tell you 
immediately if the next version of Coq fails to prove it *)
Clear H7;Omega.
Solve Auto with zarith.
Solve Auto with zarith.

Of course, this solution is a bit tedious

2) second way: when you apply an automated tactic to several goals, 
ensure it solves them
Apply A2 ; Solve [ Auto with zarith | Clear H7;Omega ]. (* again, Solve 
is not needed *)

A bit hacky though...

3) third way (and the best one IMHO). Since "Auto with zarith" generate 
a goal `0 <= [L]`, assert it first:
Assert `0 <= [L]`. Clear H7;Omega.
Apply A2; Solve Auto with zarith. (* again, Solve is not needed *)

This solution is quite readable and clearly robust.

NB: in V7.4, you can write things in a more uniform fashion like this:

Assert `0<= [L]`. Intuition.
Apply A2; Intuition.

Actually, there is an even shorter proof: "Intuition." or "Auto with 
*." I hope this reconciles you with automated tactics :-).

Sincerly yours,

Judicaël.
--
Judicael.Courant AT lri.fr,
 http://www.lri.fr/~jcourant/
Tel (+33) (0)1 69 15 64 85
GPG public key: 7C25 D439 9F60 BC68 A131  6267 98B9 98F6 7107 2457
When he realizes they own weapons of mass destruction,
will George demands for war on USA?