feature request: unfold n steps of definition

Stream: lean4

[Kenny Lau]

From #new members > How to determine the intended API of an object we ran into the problem that it can be hard for a beginner to find out the underlying definition of (· ≤ · : Subgroup _ → Subgroup _ → Prop) (sorry for using mathlib), and I proposed a command/tactic to repeatedly unfold definition for n steps (n is numeral input)...

and right in the middle of typing this I realised that maybe I can try to write the code as well

[Henrik Böving]

What does "unfold for n steps" mean if the head symbol of the definition is not a constant?

[Kenny Lau]

nothing

[Henrik Böving]

Aren't you going to run into issues pretty quickly then because LE.le is just a projection and as such not unfoldable

[Kenny Lau]

well unfold LE.le works

[Kenny Lau]

import Mathlib

variable (G : Type*) [Group G]

example : (· ≤ · : Subgroup G → Subgroup G → Prop) = sorry := by
  unfold LE.le
  -- ⊢ (fun x1 x2 => CompleteLattice.toCompletePartialOrder.toLE.1 x1 x2) = sorry

[Henrik Böving]

Yeah and now youa re left in another state where the head symbol is not a constant, so what do you want to unfold next, my point is that it's not trivial to figure out what the symbol you actually want to unfold is when you go recursively without human assistance

[Kenny Lau]

the head is Preorder.toLE which is a constant

[Kenny Lau]

oh wait, it's the .1

[Henrik Böving]

Exactly^^

[Kenny Lau]

but after the .1 the head is Preorder.toLE

[Henrik Böving]

But Preorder.toLE is also just an abbrevation for a projection

[Kenny Lau]

how would you solve this problem then?

[Henrik Böving]

I don't know, that's why I asked :)

[Kenny Lau]

well you can go one step deeper if you see .n

[Henrik Böving]

Sure you can try many tricks, there is also the question of what you do once there is more than one potential constant that you could unfold in your term around, do you go for all of them? just one? which one?. My point is that it is probably not easy to figure out something that will present a beginner with an output that is generally helpful, especially when there are large towers of definitions like in Mathlib that, when just naively unfolded, don't look helpful at all.

[Kyle Miller]

Hmm, maybe mathlib's whnf tactic could take a numeric argument for how many head definition unfoldings to do. In the given example, it could be used along with conv mode to get into a particular position.

It'll probably unfold too much still, since the projection will force unfolding, even of definitions. Plus, it won't use equation lemmas, so the results might not be good.

[Kyle Miller]

Something that might work as a heuristic for Kenny's idea is "to find the next definition to unfold, take all the constants appearing in explicit arguments, and unfold the one with the largest definitional height".

"Definitional height" is already a heuristic used in the system. The definitional height is one more than the maximum of definitional heights of constants appearing in a declaration. (Abbreviations don't have a definitional height though. They sort of have infinite height and could be unfolded first.)