Bringing back ⇑

Stream: mathlib4

[Eric Wieser]

In Lean4, core only supports ↑. We added a custom elaborator in mathlib that lets us write ⇑ and ↥ (though it's buggy until #8297). Kyle Miller added support for delaboration of ↥ for pretty much all the cases we care about.

Do we want ⇑ to appear in the goal view instead of ↑ for functions? Should this be a mathlib-only feature or in Std?

[Eric Wieser]

/poll What do you prefer to see in your goal view

• ↑f (x + y) = ↑f x + ↑f y (the status quo)
• ⇑f (x + y) = ⇑f x + ⇑f y

[Eric Wieser]

Arguments in favor of ⇑:

• It should round-trip better
• It allows use of the heuristic "⇑s are always boring, ↑s could be hiding something unexpected"

[Eric Wieser]

Arguments against:

• It's one more magic arrow to teach new users

[Alex J. Best]

Do we have actual examples of situations where round tripping is better? Those would be helpful to know when deciding

[Eric Wieser]

Sure, here's an example:

import Mathlib.Algebra.Group.Hom.Basic
import Mathlib.Tactic.Coe

example {M N : Type*} [Monoid M] [Monoid N] (f : M →* N) (x y : M) : f x = f y := by
  show (⇑f) x = (⇑f) y -- works
  show ↑f x = ↑f y -- fails
  sorry

[Eric Wieser]

(the extra parens will go away after #8297)

[Patrick Massot]

In Lean 3, you needed to remove all ⇑ as a very first step when trying to get round-tripping.

[Patrick Massot]

And #8297 doesn't build.

[Eric Wieser]

Yes, and the status quo in mathlib 4 is that you have to do the same thing with removing all the ↑, which is even worse because you can't tell which ones you need to remove!

[Floris van Doorn]

I would like to not see ⇑f x in my goal view at all. f x is unambiguous and (almost?) always parses correctly anyway. So it's just noise. (Ideally clicking on f in the goal view would show that there is a coercion.)
If ⇑f is not applied to an argument (e.g. ⇑f = ⇑g or F (⇑f)), then the ⇑ would be nice to see.

[Floris van Doorn]

The same applies to sorts, but they are a lot less frequent (in the formalizations I do), so I care less about that.

[Eric Wieser]

As an example of where you do need ⇑, consider the goal state ⇑f + ⇑g = ⇑(f + g)

[Eric Wieser]

It's not immediately clear to me what the heuristic here is; the problem in general is when you have some polymorphic function h (here HAdd.hAdd) such that both h ⇑f ⇑g and ⇑(h f g) are well-typed.

[Floris van Doorn]

I covered that case in my message, and I do want to see the ⇑ (or ↑) there, indeed.

[Eric Wieser]

I'm not sure that helps with (⇑f + ⇑g) x = ⇑(f + g) x

[Eric Wieser]

Ah yes, that sounds sufficient, you'd see (⇑f + ⇑g) x = (f + g) x

[Floris van Doorn]

The heuristic I was thinking of: is the ⇑f applied to another argument. There might be a few cases where the ⇑ is still superfluous, like Function.curry ⇑f, but I'm happy to accept those.

[Eric Wieser]

std4#354 implements that heuristic

[Floris van Doorn]

Eric Wieser said:

std4#354 implements that heuristic

Did you forget to push new commits?

/-- info: ⇑f 1 : Nat-/

[Eric Wieser]

$ git commt -m "implement Floris' heuristic"
git: 'commt' is not a git command. See 'git --help'.

Whoops, yes

[Eric Wieser]

I guess we need to settle the precedence discussion before that it safe to merge; I don't really care much about the outcome of #8297, and was just following Mario's advice

[Floris van Doorn]

I understand. I also don't care too much in #8297, and would definitely not block it, but when looking at the changes I was wondering whether it was actually a regression.
It's counterintuitive that ↑ and ⇑ have different precedences, and maybe that weighs stronger than a few extra parentheses.

[Eric Wieser]

Hot take: ↑ has the wrong precedence, and should be just shy of = so that (↑a + b : X) means "coerce a + b to X", since that's nicer than the (↑(a + b) : X) we currently have to write

[Floris van Doorn]

Thinking seriously about your message makes me agree with Mario's suggestion. :sweat_smile:
Yes, low-precedence ↑ would probably lead to fewer parentheses, but a prefix operation with such a low precedence is just evil.

[Mario Carneiro]

Unfortunately, we have very many low precedence prefix operators because most macros are like that. Another one with an evil precedence is !:

example (f : Bool → Bool → Bool) (x : Bool) : (f x !x = x) = (f x !(x = x)) := rfl

[Eric Wieser]

That's surely a bug, right?

[Jireh Loreaux]

eww, gross.

[Martin Dvořák]

Eric Wieser said:

Hot take: ↑ has the wrong precedence, and should be just shy of = so that (↑a + b : X) means "coerce a + b to X", since that's nicer than the (↑(a + b) : X) we currently have to write

Your suggestion would essentially guarantee that my brain would experience a parse error every time ↑a + b appears in front of me. I understand your desire to do coërcion as the last step, but the syntax would have to be something like (a + b ↑: X) to preserve the last drops of my sanity. A prefix operator, especially one that is typically written without a space, must bind tightly.

[Martin Dvořák]

Mario Carneiro said:

Unfortunately, we have very many low precedence prefix operators because most macros are like that. Another one with an evil precedence is !:

example (f : Bool → Bool → Bool) (x : Bool) : (f x !x = x) = (f x !(x = x)) := rfl

My disgust is immeasurable, and my day is ruined. Please somebody PR a fix asap.

[Eric Wieser]

Eric Wieser said:

std4#354 implements that heuristic

Just to be explicit, the behavior in that PR is now:

variable (f : WrappedFun Nat) (g : Nat → WrappedFun Nat) (h : WrappedFun (WrappedFun Nat))

/-- info: ⇑f : Nat → Nat -/
#guard_msgs in #check f.fn
/-- info: ⇑f : Nat → Nat -/
#guard_msgs in #check ⇑f
-- applied functions do not need the `⇑`
/-- info: f 1 : Nat -/
#guard_msgs in #check ⇑f 1

/-- info: ⇑(g 1) : Nat → Nat -/
#guard_msgs in #check ⇑(g 1)
/-- info: (g 1) 2 : Nat -/
#guard_msgs in #check g 1 2

/-- info: ⇑h : Nat → WrappedFun Nat -/
#guard_msgs in #check ⇑h
/-- info: h 1 : WrappedFun Nat -/
#guard_msgs in #check h 1
/-- info: ⇑(h 1) : Nat → Nat -/
#guard_msgs in #check ⇑(h 1)
/-- info: (h 1) 2 : Nat -/
#guard_msgs in #check h 1 2

[Eric Wieser]

This is now live, see docs#FunLike.coe_injective for a place where the new arrow appears in place of the old one, and docs#FunLike.ext_iff for a place where it now is eliminated.

[Eric Wieser]

(hmm, this doesn't seem to have affected the docs)