Allowing for φ(g * h) = φ(g) * φ(h) in Lean

Stream: new members

[Isak Colboubrani]

A textbook would describe a group homomorphism as a function φ : G → H such that φ(g * h) = φ(g) * φ(h) for all g, h ∈ G.

Expressing φ(g * h) = φ(g) * φ(h) for all g, h ∈ G in Lean might look like this:

example (φ : G →* H) (g h : G) : φ (g * h) = φ g * φ h := by simp # Works.

Beginners who might worry about operator precedence sometimes add extra parentheses to be extra clear, which Lean accepts:

example (φ : G →* H) (g h : G) : φ (g * h) = φ (g) * φ (h) := by simp # Works.

However, writing it exactly like we're used to from textbooks, with parentheses and without spaces, does not work:

example (φ : G →* H) (g h : G) : φ(g * h) = φ(g) * φ(h) := by simp # Does not work.

Why is whitespace significant here? What would break if it wasn't?

[Julian Berman]

Doesn't your question apply equally to any function application? Is there a reason f(12) is any more or less mathematically natural looking when f isn't a group homomorphism?

[Vlad Tsyrklevich]

φ (g) * φ (h) does not ensure the operator precedence you want--what you actually want to ensure it is (φ g) * (φ h)

[Isak Colboubrani]

@Julian Berman Indeed, I just started considering it in the context of group homomorphisms.

@Vlad Tsyrklevich That's true! I suppose a beginner concerned about precedence might fully parenthesize everything like this …

example (φ : G →* H) (g h : G) : φ (g * h) = (φ (g)) * (φ (h)) := by simp # Works.

… which Lean accepts, whereas this …

example (φ : G →* H) (g h : G) : φ(g * h) = (φ(g)) * (φ(h)) := by simp # Does not work.

… is not accepted.

[Etienne Marion]

It is just the way it works. Function application has a high level of precedence, so that white spaces play the role played by parentheses in paper maths, so the parentheses are useless, and once you are used to it they just damage readability in my opinion. Anyway as you see this is not authorized.

[Vlad Tsyrklevich]

It could also introduce parser ambiguity, I mean this is a contrived example, but:

infix:50 ")(" => fun a b => a + b
#eval 1)(2
#eval f(1)(2)

Is this f 3 or (f 1) 2

[Edward van de Meent]

Vlad Tsyrklevich said:

It could also introduce parser ambiguity, I mean this is a contrived example, but:

infix:50 ")(" => fun a b => a + b
#eval 1)(2
#eval f(1)(2)

Is this f 3 or (f 1) 2

this just highlights an issue with introducing unmatching bracket notation when usually all bracket notation matches, not an issue with the bracket function application itself.

[Isak Colboubrani]

I'm trying to think of a way to explain to a fellow undergraduate mathematics student how φ (g * h) = φ (g) * φ (h) is materially different from φ(g * h) = φ(g) * φ(h).

[Damiano Testa]

Why is "there are spaces missing", not a valid explanation?

[Isak Colboubrani]

While that response is certainly technically accurate I would expect -- right or wrong -- him/her to simply respond with: "Why does formalization force me to insert spaces, and exactly where should they go? Isn't this a problem that can be resolved?".

I'm trying to figure out how to best answer those questions in a way that is meaningful to an undergraduate mathematics student.

[Damiano Testa]

I do not know the details of parsing, but the parser needs to have some assurances that certain things will be of a given form. I do not think that it is impossible for formalization to remove the spaces, but it would likely be a lot of work to redesign the Lean parsers to accept the syntax that you propose.

[Riccardo Brasca]

If you are happy to explain to students the Lean convention just say that you have to put a space after the name of the function.

[Riccardo Brasca]

if they ask why you can just say that formalization is very rigid sometimes, it's not like writing math on paper. This sooner or later will happen anyway

[Isak Colboubrani]

I understand—so the correct answer is more along the lines of "that would require a lot of work (and probably isn't worth it)" rather than "that would break A, B, and C (which we are unwilling to do)"?

[Damiano Testa]

I am pretty sure that a lot of things would break if you allowed that and the "work" would be to fix those other things.

[Eric Wieser]

I don't think "it would be lots of work" is the answer. It was an active decision to not allow this syntax

[Isak Colboubrani]

Would you mind elaborating on the reasoning behind this design decision? I'm interested in understanding the factors that led to disallowing that syntax (I'm not questioning the decision, just looking to understand it more fully).

[Eric Wieser]

I think one argument is that forbidding the notation for function application lets it be used for custom notation instead

[Eric Wieser]

eg congr(), ofNat(), and other "magic" notation that is doing something at compile-time

[Kevin Buzzard]

I just tell my students "this is how functional programming languages work, turns out mathematicians put too many brackets"

[Philippe Duchon]

Turns out, not all functional languages work this way - some are worse than mathematicians.

But essentially, I tell my students the same thing - except, since they are computer science students, I can blame the mathematicians.

[Daniel Weber]

You can try defining

macro a:term:max"("b:term")":term => `($a $b)

and seeing what breaks