Zulip Chat Archive

Stream: general

Topic: notation question


view this post on Zulip Kevin Buzzard (May 06 2018 at 11:30):

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

view this post on Zulip Kevin Buzzard (May 06 2018 at 11:30):

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

view this post on Zulip Kevin Buzzard (May 06 2018 at 11:30):

(\heartsuit gives the heart, by the way)

view this post on Zulip Kevin Buzzard (May 06 2018 at 11:31):

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.

view this post on Zulip Kevin Buzzard (May 06 2018 at 11:31):

This has the following annoying-for-mathematicians consequence.

view this post on Zulip Kevin Buzzard (May 06 2018 at 11:32):

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

view this post on Zulip Kevin Buzzard (May 06 2018 at 11:32):

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

view this post on Zulip Kevin Buzzard (May 06 2018 at 11:32):

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

view this post on Zulip Kevin Buzzard (May 06 2018 at 11:33):

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.

view this post on Zulip Kevin Buzzard (May 06 2018 at 11:33):

My dream is

view this post on Zulip Kevin Buzzard (May 06 2018 at 11:34):

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

view this post on Zulip Kevin Buzzard (May 06 2018 at 11:34):

but of course that doesn't even typecheck

view this post on Zulip Kevin Buzzard (May 06 2018 at 11:34):

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

view this post on Zulip Kevin Buzzard (May 06 2018 at 11:34):

Actually I guess my dream is the impossible:

view this post on Zulip Kevin Buzzard (May 06 2018 at 11:34):

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

view this post on Zulip Kevin Buzzard (May 06 2018 at 11:36):

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.

view this post on Zulip Sebastian Ullrich (May 06 2018 at 11:51):

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

view this post on Zulip Kevin Buzzard (May 06 2018 at 12:01):

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.

view this post on Zulip Reid Barton (May 06 2018 at 13:44):

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

view this post on Zulip Kevin Buzzard (May 06 2018 at 14:45):

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


Last updated: May 14 2021 at 07:19 UTC