pp.beta

Stream: mathlib4

[Heather Macbeth]

Is there a Lean 4 analogue of the Lean 3 pp.beta, the option to pretty-print (fun x => x ^ 2) a as a ^ 2? I remember this came up in the tutorials project in hiding a pain point for newbies
https://github.com/leanprover-community/tutorials/blob/79a6872a755c4ae0c2aca57e1adfdac38b1d8bb1/src/exercises/03_forall_or.lean#L4
and I've also encountered it in teaching.

[Kevin Buzzard]

Yes I run into this too with teaching -- I tell the students that whenever they see a lambda they should try dsimp

[Yaël Dillies]

Is it better to hide it or to automatically simp it away at every tactic step? Hiding has the downside of creating unexpected errors.

[Heather Macbeth]

Perhaps you misunderstood my question, I asked if there was an option to hide it.

[Yaël Dillies]

Oh no, I just thought I would mention another (imo better) solution in case the option doesn't exist :smile:

[Heather Macbeth]

Yaël Dillies said:

Is it better to hide it or to automatically simp it away at every tactic step? Hiding has the downside of creating unexpected errors.

For various reasons, I don't think this would work for me. Consider

import Mathlib.Init.Function

example : Function.Injective (fun (x : Int) ↦ x - 12) := by
  intro x1 x2 h -- `h` displays as `h: (fun x => x - 12) x1 = (fun x => x - 12) x2`

Are you seriously proposing that I write my own intro variant to perform beta reduction?

Anyway, let's not derail the thread. This is an existing option from Lean 3 and the question is simply whether it's a "we'll get around to it someday" in Lean 4 or a "we've deliberately left it out."

[Patrick Massot]

I think that using a custom intro is actually a better suggestion, whatever the answer to your actual question.

[Kyle Miller]

I hope you don't mind if I derail the thread a little more, but I do want to mention that in Patrick's tutorials, number 0079 is a source of periodic questions since pp.beta is set to true but it's easy to get lambdas in this exercise, and these cause linarith to mysteriously fail.

It led to my first Zulip question as well.

[Heather Macbeth]

OK, OK .... next question, will the devs let us make such a custom intro tactic available as

set_option intro.beta true

?

[Notification Bot]

17 messages were moved from this topic to #mathlib4 > dsimp only for universal cleanup by Heather Macbeth.

[Sebastian Ullrich]

Heather Macbeth said:

This is an existing option from Lean 3 and the question is simply whether it's a "we'll get around to it someday" in Lean 4 or a "we've deliberately left it out."

This I can answer: the option did not make the cut in my initial implementation of the pretty printer together with a few more options and I never came back to implementing the rest of them (did anyone miss the other ones so far?), but there was no conscious decision to drop them forever https://github.com/leanprover/lean4/blob/f9da1d8b55ca6989297fb952985b7d8d6c77e14b/src/Lean/PrettyPrinter/Delaborator/Options.lean#L138-L180

[Eric Rodriguez]

[Quoting…]

Is this also the case in the new thread that just got posted in #new members > Unexpected behaviour of linarith?

[Eric Rodriguez]

(I think my quote didn't work, tube WiFi, but it was @Kyle Miller's comment about the exercises by Patrick

[Yaël Dillies]

Yes, absolutely.