How does Lean name new variables?

Stream: general

[É Olive]

Lean produces some rather odd variable names when you let it name them. Often they seem to include the character ᾰ, but sometimes not. For example I have seen it generate the variable name s_ᾰ_1 in one proof and then moments later it in the same proof it generates the the much nicer name of ih for something else. For code-golf I would like to be able to predict these somewhat so I can make informed decisions, and try to steer them towards shorter names without the unweildy with statements. How does it generate these? And why does it sometimes generate nice names and sometimes not?

[Yaël Dillies]

Eh, I think you're in for some trouble because Lean names variables weirdly to avoid clashing. When it names "nicely", it's because it's using some recursor/ext lemma under the hood where the introduced variable is named, in which case that name is used.

[Yaël Dillies]

For example, when the goal has an outer forall, intros will introduce the variable and give it the name of the variable in the binder.

[Yakov Pechersky]

For code golf, you can use french quoted underscore to have a short way of saying "by assumption"

[Patrick Massot]

The ᾰ is not only trying to avoid clashing with things you named yourself, it is also explicitly trying to discourage you from using it. If you need to refer to it then you should provide a name.

[É Olive]

Yaël Dillies said:

Eh, I think you're in for some trouble because Lean names variables weirdly to avoid clashing. When it names "nicely", it's because it's using some recursor/ext lemma under the hood where the introduced variable is named, in which case that name is used.

The forall and intro/intros makes sense to me, but I have this code:

def r:∀s,rev(@rev A s)=s
| [] :=
  rfl
| (x::t) :=
  by
    { conv
      { to_rhs
      , rw<-r t
      }
    ; simp
    ; induction rev t
    ; simp
    ; simp [ih]
    }

Full mwe

Here the nice name ih comes out of the induction, but most the time the inductive hypothesis is named some jibberish like s_ᾰ_ih. I can't quite figure out what is causing the nice name here.

[Eric Wieser]

Can you provide an mwe that produces the gibberish name?

[É Olive]

Eric Wieser said:

Can you provide an mwe that produces the gibberish name?

Sure, here's a really short example where I introduce a variable without supplying a name and it becomes ᾰ, which seems to be the preferred default

universe u
theorem f{A:Type u}:A->A:=by intro;exact ᾰ

[Yury G. Kudryashov]

If you're going to use a name, then you should do intro h.

[É Olive]

Yes, but that would make it no longer a mwe.

[Yury G. Kudryashov]

If you do intro without supplying a name, then you should not refer introduced variables by names.

[Yury G. Kudryashov]

Consider this to be our way to enforce a coding style.

[É Olive]

Alright, here's a mwe in which I do not refer to the variable. I think this makes it harder to see what is going on, but here it is.

universe u
theorem f{A:Type u}:A->nat:=by intro;exact 0

[Yury G. Kudryashov]

Lean (more precisely, Lean 3 community edition) uses strange characters for autogenerated variable names in order to avoid possible name clash. As a side effect, some definitions have funny variable names in #print/#check output.

[Yakov Pechersky]

In your A to A mwe, by assumption will work. So if you're trying to golf, use the French quoted underscore.

[Yury G. Kudryashov]

And you have to name any introduced variable if you're going to use its name in the proof.

[É Olive]

É Olive said:

Eric Wieser said:

Can you provide an mwe that produces the gibberish name?

Sure, here's a really short example where I introduce a variable without supplying a name and it becomes ᾰ, which seems to be the preferred default

universe u
theorem f{A:Type u}:A->A:=by intro;exact ᾰ

Here's a mwe where I get the precise jibberish name I made up earlier of s_ᾰ_ih. Notably it seems that the default naming works different on my new lists vs. the ones in the prelude, so you have to use my lists to get this name.

universe u

inductive mylist (A : Type u) : Type u
| nil : mylist
| cons : A → mylist → mylist

@[simp]def f{A:Type u}:mylist A→mylist A:=λx,x

theorem q{A:Type u}:∀ s:mylist(mylist A),s=f(s):=by{intro,induction s,simp,induction s_ᾰ;simp}

[Yury G. Kudryashov]

Coding style says to name variables in intro and induction.

[Yury G. Kudryashov]

For induction you can also use case nil : { }, case cons : a l ihl { }

[Yakov Pechersky]

If you're really trying to golf here, you can directly say "apply mylist.rec_on" or some variant of that, instead of using the induction tactic. But you should also remember that the whole language is set up to be expressive and to avoid ambiguitity, which is pretty counter to syntax-style golfing.

[É Olive]

That's very interesting, and yes will probably be very useful to me. Is there any sort of documentation for the function? It's a little mystical to me.

[Yury G. Kudryashov]

For each new inductive type (incl. structures), Lean generates typename.rec_on and a few other functions. I don't know if they're documented somewhere. You can alway #print prefix mylist to list them, then #check mylist.rec_on or #print mylist.rec_on to see what they do.

[Yaël Dillies]

To be fair, a much better golfing metric would be the size of the underlying generated term.

[É Olive]

Is that measurable?

[Yaël Dillies]

Definitely! I don't personally know how to access it, but it's perfectly possible.

[É Olive]

Well, if anyone finds out I'd be interested in giving it a spin, but until then I will probably live with bytes on disc, since that's easy for me to measure.