Adam Dingle (Mar 29 2026 at 11:19): Adam Dingle (Mar 29 2026 at 11:19):Continuing my saga of proving facts about the naturals, in the middle of a proof I have this:
...
have "x + (u + v) = z" using b by auto
hence "∃a. x + a = z" by blast
...
It works, but if I change "by blast" to "by auto" it fails. That surprised me, since I thought that "auto" calls "blast". Specifically, the reference manual says
auto combines classical reasoning with simplification. It is intended for situations where there are a lot of mostly trivial subgoals; it proves all the easy ones, leaving the ones it cannot prove. Occasionally, attempting to prove the hard ones may take a long time. The optional depth arguments in (auto m n) refer to its builtin classical reasoning procedures: m (default 4) is for blast, which is tried first...
I thought maybe "auto" was failing because it searches by default to depth 4, but "blast" searches by default to depth 20. However if I change "by blast" to "by (blast 4)" it still works, so a search depth of 4 should be adequate.
So what am I missing? Does "auto" not actually try "blast" as the documentation seems to say?
Kevin Kappelmann (Mar 29 2026 at 11:31):One can't tell because your message does not include sufficient context. In particular, this works in Isabelle 2025-2:
theory Scratch
imports Main
begin
notepad
begin
fix x u v z :: nat
have "x + (u + v) = z" sorry
hence "∃a. x + a = z" by auto
end
end
In general: auto does more than blast. In particular, it uses the simplifier. So maybe you have a bad setup for the simplifier in your background theory.
Adam Dingle (Mar 29 2026 at 11:37):OK - I've attached my theory file. If I change "by blast" to "by auto" in the last proof, it fails.
Kevin Kappelmann (Mar 29 2026 at 11:40):Try (auto simp del: add_assoc)
Adam Dingle (Mar 29 2026 at 11:46):Aha, I see - my associative simplification rule was causing trouble:
theorem add_assoc [simp]: "x + (y + z) = (x + y) + z"
by (induct z) auto
When I wrote that theorem, I wasn't sure whether to add "[simp]" or not. Now I realize maybe that wasn't a great idea, since there are situations where this rewrite can be harmful.
However, I'm still a bit puzzled as to why "auto" fails with this rule in place, because the documentation says that "blast is tried first". I thought that "auto" would invoke "blast" before applying any rewrite rules. But maybe I was wrong about that.
Kevin Kappelmann (Mar 29 2026 at 11:51):You are misreading that part of the manual (and quoting it without sufficient context). The full context is:
The optional depth arguments in (auto m n) refer to its builtin classical
reasoning procedures: m (default 4) is for blast, which is tried first...
So "first" here just refers to its classical reasoning component. And indeed, that is true if you check the implementation (Provers/clasimp.ML):
fun mk_auto_tac ctxt m n =
let
val main_tac =
Blast.depth_tac ctxt m (* fast but can't use wrappers *)
ORELSE'
(CHANGED o nodup_depth_tac (addss ctxt) n); (* slower but more general *)
in
PARALLEL_ALLGOALS (Simplifier.asm_full_simp_tac ctxt) THEN
TRY (Classical.safe_tac ctxt) THEN
REPEAT_DETERM (FIRSTGOAL main_tac) THEN
TRY (Classical.safe_tac (addSss ctxt)) THEN
Simplifier.prune_params_tac ctxt
end
(you don't have to understand the code, I just put it here so you can see by syntactic pattern matching that the simplifier is applied before calling main_tac, which contains blast)
Adam Dingle (Mar 29 2026 at 11:55):The code is illuminating. Thanks for the helpful reply!
Notification Bot (Mar 29 2026 at 11:55):Adam Dingle has marked this topic as resolved.
Last updated: Apr 14 2026 at 09:21 UTC