notation question

Stream: general

[Kevin Buzzard]

The following might be impossible in Lean but I thought I'd ask. It's just an issue with notation.

[Kevin Buzzard]

variables {S : Type} (R : S → S → Prop)
local infix `♥` : 50 := R

definition euclidean₁ := ∀ {{x y z : S}}, x ♥ y → x ♥ z → y ♥ z
definition euclidean₂ (R : S → S → Prop) := ∀ {{x y z : S}}, R x y → R x z → R y z
definition euclidean₃ (R : S → S → Prop) := ∀ {{x y z : S}}, x ♥ y → x ♥ z → y ♥ z

[Kevin Buzzard]

(\heartsuit gives the heart, by the way)

[Kevin Buzzard]

So mathematicians would normally _define_ a new relation with the infix notation, in contrast to functional programmers who want to define R first and then set up infix notation for it.

[Kevin Buzzard]

This has the following annoying-for-mathematicians consequence.

[Kevin Buzzard]

Definition 1 above is not so great because you can't see what you are defining -- it should say "euclidean1 heartsuit" or something.

[Kevin Buzzard]

Definition 2 is correct, but doesn't use the notation, so mathematicians are left wondering why we have R x y instead of x R y or x heartsuit y

[Kevin Buzzard]

(infix notation is more normal in mathematics than CS perhaps)

[Kevin Buzzard]

And definition 3 is wrong because the heart in the definition is unrelated to the R -- the heart is attached to the variable R and definition 3 introduces a new one.

[Kevin Buzzard]

My dream is

[Kevin Buzzard]

definition euclidean_dream (R) := ∀ {{x y z : S}}, x ♥ y → x ♥ z → y ♥ z

[Kevin Buzzard]

but of course that doesn't even typecheck

[Kevin Buzzard]

Is there any way I can make my dream definition typecheck?

[Kevin Buzzard]

Actually I guess my dream is the impossible:

[Kevin Buzzard]

definition euclidean_dream ♥ := ∀ {{x y z : S}}, x ♥ y → x ♥ z → y ♥ z

[Kevin Buzzard]

I don't mind a few incomprehensible lines with set-up beforehand, my question I guess is simply whether I can introduce a local variable in a definition and instantly have access to notation for it.

[Sebastian Ullrich]

@Kevin Buzzard Something like this proposal? https://github.com/leanprover/lean/issues/1522#issuecomment-294872715

[Kevin Buzzard]

Yes! I didn't mention it in my posts above but I did try to do this with the type class notation types (indeed I wrote has_heart :-) ) but I couldn't get that to work either because definition blah (S : Type) (R : S -> S -> Prop) [has_heart S] wouldn't attach the heart to R and I couldn't figure out how to make the attachment whilst keeping it all looking clean and uncluttered. I am currently thinking a lot about trying to write code which looks really clean to mathematicians, who we can think of here as people who know exactly what a transitive binary relation is but have no idea what a typeclass is and don't want to see clutter when they are actually doing or reading mathematics in Lean.

[Reid Barton]

In Haskell you can convert an infix operator to an ordinary (prefix) function by surrounding the operator in parentheses. You can also use this notation at a binding site.
The hypothetical Lean equivalent would be

definition euclidean {S : Type} ((♥) : S → S → Prop) := ∀ {{x y z : S}}, x ♥ y → x ♥ z → y ♥ z

[Kevin Buzzard]

Lean would need to be told the associativity and left binding power, or at least default options for such things.