pretty print of Nat

Stream: Is there code for X?

[Asei Inoue]

Is there a way to replace the combination of Nat.zero and Nat.succ appearing in infoview with "0, 1, 2, 3, ..." ?

import Mathlib.Tactic

/-
![1, 2, 3] : Fin (Nat.succ (Nat.succ (Nat.succ 0))) → ℕ
-/
#check ![1, 2, 3]

[Kyle Miller]

Related question: https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/.E2.9C.94.20More.20convenient.20notation.20for.20.23check.20a.20FinVec/near/434055374

The answer is that there's no pretty printer option for this. It's possible for you to write your own delaborator to pretty print these expressions in the way you want though.

[Asei Inoue]

Thank you!

[Asei Inoue]

I will learn Lean more to understand this fantastic language…

[Filippo A. E. Nuccio]

While doing some exercises from the "Metaprogramming in Lean" book, I clicked on the solutions and got the following code

import Mathlib
import Init.Prelude

open Lean Lean.Expr Lean.Meta

elab "explore" : tactic => do
  let mvarId : MVarId ← Lean.Elab.Tactic.getMainGoal
  let metavarDecl : MetavarDecl ← mvarId.getDecl

  IO.println "Our metavariable"
  -- [anonymous] : 2 = 2
  IO.println s!"\n{metavarDecl.userName} : {metavarDecl.type}"

  IO.println "\nAll of its local declarations"
  let localContext : LocalContext := metavarDecl.lctx
  for (localDecl : LocalDecl) in localContext do
    if localDecl.isImplementationDetail then
      -- (implementation detail) red : 1 = 1 → 2 = 2 → 2 = 2
      IO.println s!"\n(implementation detail) {localDecl.userName} : {localDecl.type}"
    else
      -- hA : 1 = 1
      -- hB : 2 = 2
      IO.println s!"\n{localDecl.userName} : {localDecl.type}"

theorem red (hA : 1 = 1) (hB : 2 = 2) : 2 = 2 := by
  explore
  sorry

but in the infoview I have a bunch of (OfNat.ofNat.{0} Nat 1 (instOfNatNat 1)) (OfNat.ofNat.{0} Nat 1 (instOfNatNat 1))) instead of 1. Is there a pretty printer to call so that this gets bettered rendered?

[Aaron Liu]

Use docs#Lean.logInfo instead:

import Lean

open Lean Lean.Expr Lean.Meta

elab "explore" : tactic => do
  let mvarId : MVarId ← Lean.Elab.Tactic.getMainGoal
  let metavarDecl : MetavarDecl ← mvarId.getDecl

  logInfo "Our metavariable"
  -- hA : 1 = 1
  -- hB : 2 = 2
  -- ⊢ 2 = 2
  logInfo mvarId

  logInfo "All of its local declarations"
  let localContext : LocalContext := metavarDecl.lctx
  for (localDecl : LocalDecl) in localContext do
    if localDecl.isImplementationDetail then
      -- (implementation detail) red : 1 = 1 → 2 = 2 → 2 = 2
      logInfo m!"(implementation detail) {localDecl.userName} : {localDecl.type}"
    else
      -- hA : 1 = 1
      -- hB : 2 = 2
      logInfo m!"{localDecl.userName} : {localDecl.type}"

theorem red (hA : 1 = 1) (hB : 2 = 2) : 2 = 2 := by
  explore
  sorry

[Filippo A. E. Nuccio]

Thanks!

[Filippo A. E. Nuccio]

I realise that this is still not exactly what I needed: for pedagogical purposes I am defining a tactic that add the double of any natural in scope:

import Lean.Elab
import Mathlib.Tactic

open Lean Elab Tactic

def SuccNat : TacticM Unit :=
  withMainContext do
  let lctx ← getLCtx
  for h in lctx do
  if h.type == .const ``Nat [] then
    liftMetaTactic fun mv => do
      let mv ← mv.define s!"double_{h.userName.toString}".toName (.const ``Nat [])
        (Lean.mkAppN (.const ``Nat.mul []) #[mkNatLit 2, h.toExpr])
      let (_, mv) ← mv.intro1P
      return [mv]

elab "succNat" : tactic => SuccNat

but when I do

example (n m k : ℕ) (H : n = 3 + 1) : True := by
  succNat
  sorry

I have in my infoview

double_n : ℕ := Nat.mul 2 n
double_m : ℕ := Nat.mul 2 m
double_k : ℕ := Nat.mul 2 k

whereas I would like them rendered as 2 * n, 2 * m, etc...

[Damiano Testa]

Here is one way:

def SuccNat : TacticM Unit := withMainContext do
  let lctx ← getLCtx
  for h in lctx do
    if h.type == .const ``Nat [] then
      let hval := h.toExpr
      let hstx ← Expr.toSyntax hval
      let tm ← `(term| 2 * $hstx)
      let tme ← elabTerm tm h.type
      liftMetaTactic fun mv => do
        let mv ← mv.define s!"double_{h.userName.toString}".toName h.type tme
        let (_, mv) ← mv.intro1P
        return [mv]

[Filippo A. E. Nuccio]

Nice! Can you explain what these lines

    let tm ← `(term| 2 * $hstx)
    let tme ← elabTerm tm (some h.type)

are (in paticular the term| and the elabTerm) and why this works (or, equivalently, why the previous did not)?

[Damiano Testa]

The first one, is generating a Syntax object (in fact, a Term) that represents 2 * <the other>.

[Damiano Testa]

Now that you have a Syntax, you can elaborate it and produce an expression: this is what the other line does.

[Filippo A. E. Nuccio]

Oh, so I was roughly working at the Expr level, and you are somewhat deeper?

[Damiano Testa]

The main takeaway is that Lean is generating the expr for you, so you do not have to worry about what mkApp you should use.

[Filippo A. E. Nuccio]

(Apologies for the dummy question, I am moving my first steps in this)

[Damiano Testa]

I would actually say that my code is more shallow.

[Damiano Testa]

I view "depth" as follows:

• text that you type -- very much on the surface;
• Lean converts it to syntax -- a little bit deeper;
• eventually, from the syntax lean produces an expr -- deep here!

[Filippo A. E. Nuccio]

Oh, I got syntax <-> expr in the wrong order. Thanks!

[Damiano Testa]

Right: I mostly view Syntax as a step towards producing an Expr, rather than the other way round.

[Filippo A. E. Nuccio]

So, is it roughly correct that you try to work with syntax as much as possible and revert to Expr only when needed?

[Filippo A. E. Nuccio]

(I am a bit confused because studying the Metaprogramming book, I feel more emphasis on Expr than on Stx)

[Damiano Testa]

I am not sure if that is always the case: eventually, you want the Expr to line up, but if you can make Lean do the conversion/elaboration, that is more stable than doing it yourself.

[Filippo A. E. Nuccio]

I see

[Damiano Testa]

I would view writing directly the Expr as "unfolding all the way".

[Damiano Testa]

Sometimes, there is no way around it and ultimately, you should be able to do things like that.

[Damiano Testa]

In practice, though, if you can leverage some intermediate representations that takes care of the conversion for you, you are better off using them.

[Filippo A. E. Nuccio]

OK, very nice. But this means in particular that the infoview is really affected by the way I produce things, and does nothing "on its own" like translating expressions back and forth when notation is in force?

[Damiano Testa]

I would say that pretty-printing is very susceptible of what exactly you use. This is why, if you have syntax for something, you should use it, since otherwise it will "mean the same", but nothing will pick it up.

[Damiano Testa]

In the case above, you want Lean to latch onto whatever it is that uses the * notation.

[Damiano Testa]

I think that this is the HMul typeclass, that, for Nat, is highjacked... maybe the Nat.mul that you were using, I am not sure.

[Filippo A. E. Nuccio]

I see, I certainly need to get more experience, but little by little it will improve. I had indeed tried with the HMul, but at the Expr-level it is a nightmare, because it needs to be filled with all the arguments (the three types) and with the HMul instance, itselft having several arguments (and coming from Mul for Nat, that again needs arguments...)

[Aaron Liu]

If you turn off notation, 2 * n is printed as HMul.hMul 2 n

[Filippo A. E. Nuccio]

Aaron Liu said:

If you turn off notation, 2 * n is printed as HMul.hMul 2 n

But my point was to turn it on

[Damiano Testa]

Right, if you use

        (← Meta.mkAppM ``HMul.hMul #[mkNatLit 2, h.toExpr])

in the appropriate line of your code, you will see that it "works" as is.

[Damiano Testa]

Filippo A. E. Nuccio said:

I see, I certainly need to get more experience, but little by little it will improve. I had indeed tried with the HMul, but at the Expr-level it is a nightmare, because it needs to be filled with all the arguments (the three types) and with the HMul instance, itselft having several arguments (and coming from Mul for Nat, that again needs arguments...)

Note that I used the helper Meta.mkAppM that have a better UX.

[Filippo A. E. Nuccio]

Yes, because mkAppM is more clever wrt implicit arguments, right?

[Aaron Liu]

Nat.mul does not have notation, and is not the same as @HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat)

[Damiano Testa]

Using Lean.mkAppN directly is really hardcore (and really brittle).

[Aaron Liu]

For this I would use docs#Lean.mkNatMul, since it is specialized to this use case.

[Damiano Testa]

So, `(syntax) and Meta.mkAppN are more user-friendly than constructing the inductive Syntax and Expr directly.

[Aaron Liu]

Usually

[Damiano Testa]

In general, you should always prefer them over anything else and use the constructors only as a last resort.

[Damiano Testa]

Ah, if there is a dedicated function, then great!

[Filippo A. E. Nuccio]

Aaron Liu said:

For this I would use docs#Lean.mkNatMul, since it is specialized to this use case.

And this brings me to the ancillary question... how to survive the enormous zoo of functions around? I understand it is probably the same question one could ask for Mathlib, but for me the Lean.Elab zoo seems much wilder :lion: :tiger: I mean, should I hope to eventually learn everything that is in there? Are there guide(line)s? General principles to browse the library?

[Filippo A. E. Nuccio]

At any rate, thank you both for your answers ! :pray:

[Damiano Testa]

I think that yes, it is like with mathlib: you ask questions, you browse a little...

[Damiano Testa]

In the case of metaprogramming, "proofs", i.e. reading after the :=, is probably more informative than doing it in mathlib.

[Kyle Miller]

You could also take more advantage of evalTactic here. It feels less robust in some ways, but the positive to the tradeoff is that the code is a lot simpler to understand:

def SuccNat : TacticM Unit := withoutRecover <| withMainContext do
  let lctx ← getLCtx
  for h in lctx do
    if h.type.isConstOf ``Nat then
      let doubleIdent := mkIdent <| Name.mkSimple s!"double_{h.userName.toString}"
      let hstx ← exprToSyntax h.toExpr
      evalTactic <| ← `(tactic| let $doubleIdent : Nat := 2 * $hstx)

elab "double_nats" : tactic => SuccNat

example (a b c : Nat) (d : Int) : True := by
  double_nats
/-
a b c : Nat
d : Int
double_a : Nat := 2 * a
double_b : Nat := 2 * b
double_c : Nat := 2 * c
⊢ True
-/

[Filippo A. E. Nuccio]

Is evalTactic explained somewhere (perhaps in the Metaprogramming book, or elsewhere)?

[Kyle Miller]

I don't know whether it is or not, but it ought to be. It's one of the easiest ways to manipulate the tactic state, since it lets you run tactic scripts directly. It lets you make macros that depend on the details of the current state (here, we can't use a macro because we need the current local context).

[Filippo A. E. Nuccio]

Ok, thanks, I'll try to study/understand it and how it works.

[Kyle Miller]

I made a small modification: the additional withoutRecover makes sure the tactic in evalTactic is being run in a mode where it doesn't try to do any error recovery. For example, inserting sorry when there are type errors.

In the automated parts of a tactic, you want recovery disabled, since you expect them to be error-free. If anything goes wrong, you want the tactic to stop with an error so you can debug it.

(You can experiment with the effects of withoutRecover by changing the evalTactic line to do something bogus, like let $doubleIdent : Nat := true * $hstx)

[Kyle Miller]

I think the fact it was easy to forget to include withoutRecover proves the thesis that the Lean 4 metaprogramming interface is very large and difficult to keep track of.

I try to keep Metaprogramming gotchas updated. Just added withoutRecover at the end.

[Filippo A. E. Nuccio]

Thanks! If you feel like adding a paragraph about evalTactic (or more about EvalM in general... :smile: ) it would be very much appreciated!

[Damiano Testa]

Also, for pedagogical purposes, I find the exact checking that the type of your local declarations is Nat very strong. If this were a "real" tactic, I think that it would probably try a little harder to unify h.type with Nat, probably using Meta.whnfR.

[Damiano Testa]

E.g., if you had abbrev N := Nat and then you had an s : N in your context, it may not be unreasonable to want to double s as well.

[Kyle Miller]

In fact, that points to how the tactic is afflicted by one of the gotchas :-)

example (a b c : Nat) (d : Int) : True := by
  let e := 2
  double_nats
  -- e is not doubled

[Kyle Miller]

Quiz: which gotcha is it?

[Damiano Testa]

This is one of the most common issues!! :smile:

[Filippo A. E. Nuccio]

Kyle Miller said:

Quiz: which gotcha is it?

Oh nice! I'll try to do the exercise tonight :smirk: Thanks.

[Damiano Testa]

(And I still consider this kind of "action at a distance" very confusing, btw.)

[Filippo A. E. Nuccio]

Filippo A. E. Nuccio said:

Kyle Miller said:

Quiz: which gotcha is it?

Oh nice! I'll try to do the exercise tonight :smirk: Thanks.

Is it in some sense thinking that e must be an integer (although it shows as a Nat in the infoview) perhaps?

[Damiano Testa]

I think that even without d, it would still not work.

[Damiano Testa]

But I also consider the d a hint for figuring out what is going on.

[Kyle Miller]

I'm not sure d is related at all. It's not a metadata bug, if that's what you're thinking. (E.g., one solved by consumeMData on the goal type.)

[Damiano Testa]

No, I was not thinking of a metadata issue (although it is the first thing that I thought when I saw your example).

[Damiano Testa]

I was thinking more of getting into the mind-set of thinking that there is something unspecified about the type of e.

[Aaron Liu]

Kyle Miller said:

Quiz: which gotcha is it?

Is it

spoiler

uninstantiated mvars

[Filippo A. E. Nuccio]

Aaron Liu said:

Kyle Miller said:

Quiz: which gotcha is it?

Is it

spoiler

uninstantiated mvars

Oh, and why so!?! Is the let clause creating a mvar for the type of e or something?

[Kyle Miller]

let e := 2 is basically shorthand for let e : _ := 2, and so, yes, the type of e is a metavariable. The metavariable is assigned very soon after it is created, but it's still there.

One fix is to do

def SuccNat : TacticM Unit := withoutRecover <| withMainContext do
  let lctx ← getLCtx
  for h in lctx do
    let htype ← instantiateMVars h.type
    if htype.isConstOf ``Nat then
      let doubleIdent := mkIdent <| Name.mkSimple s!"double_{h.userName.toString}"
      let hstx ← exprToSyntax h.toExpr
      evalTactic <| ← `(tactic| let $doubleIdent : Nat := 2 * $hstx)

Another is to put it into whnf as Damiano suggested:

def SuccNat : TacticM Unit := withoutRecover <| withMainContext do
  let lctx ← getLCtx
  for h in lctx do
    if (← whnfR h.type).isConstOf ``Nat then
      let doubleIdent := mkIdent <| Name.mkSimple s!"double_{h.userName.toString}"
      let hstx ← exprToSyntax h.toExpr
      evalTactic <| ← `(tactic| let $doubleIdent : Nat := 2 * $hstx)

[Filippo A. E. Nuccio]

While I understand why the first solution works, I do not for Damiano's. Is whnfR instantiating mvars under the hood? I would have imagined it only to be able to fix problems related to Nat being "locally presented" not as .const ``Nat [], not to be able to manage this kind of uninstantiated mvars.

[Kyle Miller]

Yes, part of the definition of weak-head normal form is that there are no head metavariables that have been assigned. That is, if you have ?m a1 a2 ... an with ?m an assigned metavariable, it will instantiate it.

[Filippo A. E. Nuccio]

Awesome! Thanks (this probably is also worth mentioning in the relevant chapter, no?)

[Kyle Miller]

It looks like they briefly mention it, a bit indirectly:

?x 0 1  -- Assuming the metavariable `?x` is unassigned, it is in WHNF.

?x 0 1 -- Assuming `?x` is assigned (e.g. to `Nat.add`), its application is not
          in WHNF.

[Damiano Testa]

In terms of "standard tactic expectation", I would say that mathlib tactics would normally expect using whnfR for normalization, than just instantiating metavariables.