Generate explanation for expressions

Stream: Is there code for X?

[Tsuru]

I want to generate natural language explanation for Lean expressions (expr).
I think doc strings are useful for this purpose, but there is problem with expressions which involve type (class) inferences.
In short, I need some_function like this:

class has_add2 (α : Type*) := (add : α → α → α)
instance : has_add2 ℚ := ⟨λ x y, x+y⟩
instance : has_add2 ℕ := ⟨λ x y, x+x+y⟩
infix `++++` : 100 := has_add2.add
#eval 4 ++++ 5 --13
#eval (4 ++++ (5 : ℚ)) --9
meta def some_function (e: expr) := (some definition here)
#eval some_function `(4 ++++ 5) -- "addition (ℕ) of 4 and 5"
#eval some_function `(4 ++++ (5 : ℚ)) -- "addition (ℚ) of 4 and 5"

expr.to_string seems not suitable, because it gives too much complicated results (it displays 4 as something like "the successor of the successor of the successor of the successor of 0").
Is there any idea?

[Yakov Pechersky]

Take a look at how something like the norm_fin code deals with instances and numerals

[Tsuru]

Thank you! I looked over the code and found some pattern matching (in match_fin).
This seems effective for my example, but can this be more "general" solution?
We don't want to write a lot of pattern for every possible expression, but get the "surface" structure of expression and the names of its components (which can be used to collect doc strings).
(If I should study the code more, please say so.)

[Scott Morrison]

I suspect people are having trouble helping you because we don't really understand what you want to do. What is the "surface structure" of an expression? How generally are you hoping to convert Lean expressions into natural language? (Surely not arbitrary expressions?)

[Tsuru]

Yeah, actually I suspect so too, sorry...
My assumption is roughly that

1. every definition (name) can have doc strings (by tactic.add_doc_string)
2. expressions are composed of names (and application?)
3. I can combine doc strings into natural language

In short, I want to get nat.has_add2.add from `(4 ++++ 5). I suspect that I should throw away the second assumption (I may not need natural language representation of let x := e in y or lambda abstraction).
Current problem is that I got only too much decomposed representations of exprs (for example, "has_add2.add.{0} nat nat.has_add2 (bit0.{0} nat ...")
...Am I making sense? Thanks for your kind support.

[Chris B]

You can get close with the pretty-printer using the right set of options:

set_option pp.implicit true
set_option pp.notation false
-- there's also `set_option pp.numerals true` for the bit0 bit1 ... problem
def add2_ := 4 ++++ 5 --13
#print add2_
-- @has_add2.add nat nat.has_add2 4 5

Are you just trying to get this intermediate output as a string, or do you want to do more stuff with it in a tactic?

[Chris B]

If you don't need mathlib and don't mind experimenting, Lean 4 gives a lot more user-level control over pretty printing, elaboration, and delaboration.

[Tsuru]

Thank you.
I don't have courage to try Lean 4 now, but I'll do so if necessary, in future.
(I think I want to "do more stuff with it in a tactic")

[Chris B]

It seems in that case like you just want to reduction/unfolding of definitions to be more conservative. There are tactics for doing more exact unfolding, like tactic.delta, but you need to know the name(s) of the definitions you want to unfold:

meta def some_function (e: expr) : tactic unit :=
let e' := tactic.delta [`has_add2.add] e
in tactic.trace e'

#eval some_function `(4 ++++ 5) -- [has_add2.add nat.has_add2] 4 5

I'm not an expert on lean 3's meta programming; @Mario Carneiro is though, maybe he has some words of wisdom?

[Tsuru]

Thank you, this is also helpful.
Do you mean by "need to know the name(s) of the definitions" that we need to "hard-code" the name? Or is there a way to do the same thing with string data of "has_add2.add"?

[Chris B]

You can get an arbitrary string somewhere and turn it into a name, then pass it as an argument. Your tactic can also walk the actual expr itself to figure out what names it wants to unfold.

meta def some_function2 (ns : list string) (e: expr) :=
let e' := tactic.delta (ns.map name.from_string) e
in tactic.trace e'

#eval some_function2 ["has_add2.add", "nat.has_add2"] `(4 ++++ (5 : ℚ))

meta def some_function (ns : list name) (e: expr) :=
let e' := tactic.delta ns e
in tactic.trace e'

#eval some_function [`has_add2.add] `(4 ++++ 5)

There's also dsimplify for other kinds of reduction (delta is replacing a constant with its definition); both of them are configurable with a set of options. Aside from the mathlib docs, Rob Lewis made a video series about doing metaprogramming in Lean 3; https://www.youtube.com/watch?v=o6oUjcE6Nz4.