Pretty printing beta reduction

Stream: mathlib4

[Oliver Nash]

Separately, is there support for bumping this feature request: https://github.com/leanprover/lean4/issues/715 ?

[Eric Wieser]

Can you remind me what pretty-printer beta reduction support in lean 3 looked like?

[Oliver Nash]

From my point of view it meant that I saw things like α instead of (fun x ↦ α) a.

[Jireh Loreaux]

That could be annoying though right? Because then rw would randomly fail?

[Oliver Nash]

This is just for the pretty printer!

[Patrick Massot]

I had that in the tutorials project (coming from my teaching) but lots of people complained it led to incomprehensible failures

[Patrick Massot]

But I think we should still have the option.

[Oliver Nash]

@Jireh Loreaux and @Patrick Massot are you talking about the beta-reduction for pretty-printing? I don't understand how this could impact anything.

[Patrick Massot]

But resist the temptation to make it default.

[Jireh Loreaux]

Right, but Oliver, if you see c in the pretty printer and you try to rewrite with h : c = d, but it's really (fun x ↦ c) a, then you'll get a random failure of rw, no?

[Oliver Nash]

Oh I see.

[Eric Wieser]

Where here "random" means "the information you need to understand it has been hidden by the pretty printer"

[Yaël Dillies]

Jireh Loreaux said:

Right, but Oliver, if you see c in the pretty printer and you try to rewrite with h : c = d, but it's really (fun x ↦ c) a, then you'll get a random failure of rw, no?

Actually, rw will work here

[Jireh Loreaux]

??? I'm not saying I don't believe you, but I would swear that it would fail. Is there a similar situation in which it would fail?

[Eric Wieser]

I'm pretty sure there are situations in which it can fail

[Eric Wieser]

Certainly I can write a tactic that detects if there is a beta reduction available, and succeeds only if there is not

[Oliver Nash]

FWIW, I would be happy if we could have a limited version of pretty print beta-reduction which only applies for Type-valued functions.

[Jireh Loreaux]

Yaël is right though:

example {α β : Type} (c d : β) (a : α) (h : c = d) : (fun _ ↦ c) a = d := by rw [h] -- succeeds

[Patrick Massot]

I remember it caused linarith failures in the tutorials.

[Eric Wieser]

Anything that matches exprs rather than with Qq / unification would fail, and linarith is very guilty of expression matches in Lean 3

[Yaël Dillies]

To explain a bit further, the reason that rw doesn't "rewrite under binders" is because it generates (the equivalent of) an application of cast (congr_arg f), where f is called the motive. (docs#cast, docs#congr_arg)

When you rewrite ∀ a, a + 0 = a in ∑ i, i + 0 = ∑ i, i, there's no motive rw could possibly use. If such a f existed, it would somehow have access to the variable i from the outside context where i is bound, not free.

So the more accurate rule is "rw can't rewrite subexpressions that depend on a bound variable", because those are exactly the ones for which there's no motive (reference needed).

[Eric Wieser]

@Oliver Nash, I think it might be wise to split this thread, since you asked two questions and everyone is only answering the second one

[Yaël Dillies]

In fact, I think rewriting under binders might even be unprovable without function extensionality?

[Notification Bot]

23 messages were moved here from #mathlib4 > Pretty printing defaults by Oliver Nash.

[Yuyang Zhao]

I ran into this problem in the tutorials project when I was starting to learn Lean and even went here to ask a question.

[Kyle Miller]

@Oliver Nash While I don't support using pp.beta, here's a mathlib PR that implements it with a couple caveats (pp.analyze won't work, and you might see non-beta-reduced tooltips in the infoview): #7205 (@Heather Macbeth, this is from this from a thread of yours)

[Kyle Miller]

@Jireh Loreaux Here's a confusing example to support your thought about how it's annoying:

example {α β : Type} (f : α → β) (a : α) (b : β) (h : f a = b) :
    (fun x ↦ f x) a = b := by
  /-
  α β : Type
  f : α → β
  a : α
  b : β
  h : f a = b
  ⊢ f a = b
  -/
  rw [h] -- fails

It's possible to get that sort of term naturally.

When I was first learning Lean a few years ago, I almost gave up on it because of pp.beta. I managed to infer that I had an unreduced lambda term, and it was frustrating that there seemed to be no way to directly observe it -- I was thinking "if this is what people are willing to put up with, this can't be the end of it." Sorting this out was my first #new members question. (Other than that, I enjoyed Patrick's tutorial :-) It made sense why pp.beta was set, and amusingly the tutorial only ever seemed to trip up people who knew some lambda calculus, and always at a particular linarith exercise, 0079.)

[Oliver Nash]

Thanks @Kyle Miller both for #7205 and for the illustrative example.

I would add:

1. I'm persuaded that today the right call is for pp.beta to exist but switched off unless the user demands it (which IIUC is what you propose)
2. I'm a mathematician first and a type theorist only by necessity. So for me beta-reduction isn't really a thing. I regard the fact that rw can choke in this way as a failure of our tooling and thus see the fact that pp.beta cannot be on by default as a price we're paying for a deficiency of rw. (Of course I don't pretend I have a solution but I think it's important to keep this perspective in mind.)
3. Could we have a version of pp.beta for Type-valued functions? Could this be always on? I would like this because I often use the infoview to inspect the type of a term and it's annoying to have to do the beta-reduction in my head.
4. Failing 3, could we add a button to the infoview that I can click which prettifies things even further (e.g., applies beta reduction)?

[Kyle Miller]

Re 3: Could you give an example for how this occurs for Type-valued functions? I'm wondering if there's some other part of Lean that should be beta reducing something but it's not.

[Oliver Nash]

I couldn't quickly generate an example but I definitely encounter this fairly often --- I'll try to post an example later today when I have time for Lean again.

[Kyle Miller]

Re 1: Yes, I don't support it being a default, but I support your right to use it :smile: In that linked thread of Heather's, there was another feature we were exploring which would actually beta reduce the entire context after every tactic, and then pp.beta would be there to smooth over a few gaps in that (for example, I couldn't get the info view to show the beta reduced context if your cursor was in the whitespace before the first tactic in a by ... but it's safe to use pp.beta because by the time that tactic ran it'd all be beta reduced)

[Oliver Nash]

Kyle Miller said:

Re 3: Could you give an example for how this occurs for Type-valued functions? I'm wondering if there's some other part of Lean that should be beta reducing something but it's not.

Here is a simple example:

import Mathlib.LinearAlgebra.Basic

variable (R M : Type*) [CommRing R] [AddCommGroup M] [Module R M] (f : M →ₗ[R] R) (m : M)

#check f m -- Reports `(fun x ↦ R) m`, I would prefer it to say: `R`.

[Patrick Massot]

Yes, this kind of example is super annoying and I really feel it wasn't everywhere in Lean 3 as it is in Lean 4.

[Eric Wieser]

I suspect this is due to the coercion mechanism changing

[Eric Wieser]

Here's a smaller mwe:

import Mathlib.Data.FunLike.Basic
variable (F α β : Type*) [FunLike F α (fun _ => β)] (f : F) (a : α)
#check f a

[Eric Wieser]

Indeed there is no such problem in Lean 3:

import data.fun_like.basic
variables (F α β : Type*) [fun_like F α (fun _, β)] (f : F) (a : α)
#check f a