Stream: concrete semantics
Topic: What's Isabelle's "auto"?
Kevin Buzzard (Mar 01 2019 at 19:17):
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
Sebastien Gouezel (Mar 01 2019 at 19:29):
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 (Mar 01 2019 at 19:33):
auto (and any of the features you just described) documented anywhere?
Jesse Michael Han (Mar 01 2019 at 19:35):
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 (Mar 01 2019 at 20:01):
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 (Mar 01 2019 at 20:07):
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 (Mar 01 2019 at 20:09):
For documentation of Isabelle tactics, see for instance https://isabelle.in.tum.de/doc/isar-ref.pdf, page 232 (mainly
force). Probably https://www.cl.cam.ac.uk/~lp15/papers/Isabelle/blast.pdf is also relevant.
Jasmin Blanchette (Mar 25 2020 at 13:33):
@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.
Last updated: May 18 2021 at 11:11 UTC