What's Isabelle's "auto"?

Stream: concrete semantics

[Kevin Buzzard]

inductive mynat
| zero : mynat
| S : mynat → mynat

namespace mynat

def add : mynat → mynat → mynat
| zero n := n
| (S x) n := S (add x n)

lemma add_zero (m : mynat) :
add m zero = m :=
begin
  induction m with d Hd,
-- Isabelle can now finish this with
-- apply(auto)
    refl,
  exact congr_arg S Hd,
end

end mynat

Looking at p8 of the book (p18 of the pdf). What is this auto wizardry?

[Sebastien Gouezel]

auto is the main Isabelle tactic. It applies simp, but it also tries to apply recursively some rules named with the attribute intro in the library, to see if it proves the goal, with a controlled amount of backtracking (like the upcoming back in Lean, but more involved). And it is rather clever, trying to combine available facts to see what it can prove from them and if it helps solve the goal. I never really understood how it works (much more complicated than simp!), but most of the time it does what you would like schoolkid to do. For instance, there is a linarith tactic in Isabelle, but it is seldom used since auto will close your goal involving linear inequalities, say, 95% of the time.

[Jesse Michael Han]

is auto (and any of the features you just described) documented anywhere?

[Jesse Michael Han]

i suppose for now, we have tidy, which is not as intelligent (but suffices to finish the lemma above with by induction m; tidy)

[Kevin Buzzard]

Oh thanks Jesse! That's the first time I've ever used tidy! I tried all my usual suspects and none of them worked.

Here are two statements: Isabelle has some cool tactics which Lean doesn't have; Isabelle only uses simple type theory and not dependent type theory. Are these things related in any way, or is it just a matter of time before Lean gets some cool tactics which are as intelligent as Isabelle's?

[Simon Hudon]

My personal belief is that for the fragment of Lean code where you don't use dependent types, you should be able to get tactics as smart as those of Isabelle but I might be missing something important

[Sebastien Gouezel]

For documentation of Isabelle tactics, see for instance https://isabelle.in.tum.de/doc/isar-ref.pdf, page 232 (mainly blast, auto and force). Probably https://www.cl.cam.ac.uk/~lp15/papers/Isabelle/blast.pdf is also relevant.

[Jasmin Blanchette]

@Simon Hudon: Isabelle's inductive predicates correspond in Lean to inductive predicates, i.e. dependent inductive types. An inductive predicate like "even" is about as evil as "vector"-as-a-dependent-inductive-type. Same of course for big- and small-step operational semantics (in Concrete Semantics).

I'm not sure what it means for automation of Lean, but my point is that unless you're willing to build your own inductive predicates using Knaster-Tarski in Lean, you're going to need dependent types where Isabelle remains simply typed.