OfNat.ofNat visible

Stream: mathlib4

[Yury G. Kudryashov]

Sometimes I get OfNat.ofNat 2 instead of 2 in the info view (failed to minimize so far). Does it mean that this 2 is different from a "normal" 2?

[Eric Wieser]

I think this is actually OfNat.ofNat (OfNat.ofNat <a raw 2 literal>)

[Eric Wieser]

Whereas a normal 2 is OfNat.ofNat <a raw 2 literal>

[Yury G. Kudryashov]

How can I test this?

[James Gallicchio]

#check OfNat.ofNat (nat_lit 1)                -- 1 : ℕ
#check OfNat.ofNat (OfNat.ofNat (nat_lit 1))  -- OfNat.ofNat 1 : ℕ

[Yury G. Kudryashov]

I mean test in the actual non-minimal example.

[Yury G. Kudryashov]

set_option ? ?

[Eric Wieser]

What's the tactic that makes it appear?

[Yury G. Kudryashov]

simp

[Yury G. Kudryashov]

But AFAIR (can test in an hour), set_option pp.all true doesn't show nested OfNat.ofNat.

[Kyle Miller]

Apparently set_option pp.coercions false should turn off hiding OfNat.ofNat

[Eric Wieser]

Can you squeeze the simp to find the bad lemma?

[Kyle Miller]

The source code is consistent with only the innermost OfNat.ofNat being hidden if they're nested.

[Eric Wieser]

Does the pretty-printer distinguish raw literals (which should never appear) from "regular" literals?

[Kyle Miller]

No, raw literals get printed in the same way: https://github.com/leanprover/lean4/blob/d37bbf4292c72798afdff8bf5488df09193fde58/src/Lean/PrettyPrinter/Delaborator/Builtins.lean#L592

[Kyle Miller]

The only difference would be what you see when you hover over it in the infoview (is it just a nat? or does it have an OfNat.ofNat?)

[Yury G. Kudryashov]

With pp.coercions false, it's just a usual OfNat.ofNat 2, not OfNat.ofNat (OfNat.ofNat 2).

[Yury G. Kudryashov]

The (very non-minimal) example is at the end of Mathlib/Geometry/Euclidean/Inversion/Calculus.lean in branch#YK-inversion-fderiv

[Kyle Miller]

Here's a little delaborator to help debug this:

section
open Lean PrettyPrinter Delaborator SubExpr

@[delab lit]
def delabLit : Delab := do
  let .lit (.natVal n) ← getExpr | failure
  `(nat_lit $(quote n))

end

It prints natural number literals as nat_lit 37 for example

[Kyle Miller]

I see what the issue is though: the OfNat.ofNat delaborator doesn't expect numbers to be functions, and in your example the number is a function that's being applied to an argument

[Kyle Miller]

So there's not really anything wrong with the expression, it's just not pretty printing right

[Kyle Miller]

Here's the offending expression: OfNat.ofNat 2 y

[Mario Carneiro]

The easiest way to determine whether you are looking at a double ofNat vs a single ofNat or a raw numeral is to hover over the expression in the infoview. Hovering over raw numeral 2 shows 2 in the hover, and hovering over a 2 ofNat expression shows ofNat 2 ... in the hover

[Mario Carneiro]

it would be nice if raw numerals were printed as nat_lit 2

[Kyle Miller]

Kyle Miller said:

The only difference would be what you see when you hover over it in the infoview (is it just a nat? or does it have an OfNat.ofNat?)

Yeah, I was doing that but wanted to be sure nothing weird was going on (and I got tired of hovering over all the numbers in the goal state), before I noticed the y argument

[Kyle Miller]

Mario Carneiro said:

it would be nice if raw numerals were printed as nat_lit 2

This line would just need to be | Literal.natVal n => `(nat_lit $(quote n)). Should that be behind a pp.nat_lit option?

[Eric Wieser]

Wouldn't that break the delaboration of ofNat (nat_lit 2) to print as nat_lit 2?

[Kyle Miller]

No, OfNat.ofNat isn't implemented as an app_unexpander, but as a delaborator

[Kyle Miller]

I linked the source code, but I'll paste it here. It does a pattern match on the Expr. Delaborators go outside-in and, for applications, app unexpanders go inside-out. This runs before the lit delaborator or the app delaborator.

@[builtin_delab app.OfNat.ofNat]
def delabOfNat : Delab := whenPPOption getPPCoercions do
  let .app (.app _ (.lit (.natVal n))) _ ← getExpr | failure
  return quote n