Zulip Chat Archive

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 :=
  induction m with d Hd,
-- Isabelle can now finish this with
-- apply(auto)
  exact congr_arg S Hd,

end mynat

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

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):

is 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 blast, auto and 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: Dec 20 2023 at 11:08 UTC