Zulip Chat Archive

Stream: general

Topic: Infix operators in structure

Lime Sublime (Jan 20 2021 at 19:14):

Is it possible to define infix functions in a structure that act on other fields.

For example, if I have:

universe l
structure Preorder : Type (l + 1) :=
  (Obj : Type l)
  (Arr : Obj -> Obj -> Prop)

can I somehow define ~> as a synonym for Arr, such that I can have forall {A : Preorder} {a b : A.Obj}, a ~> b? The issue with adding an infix declaration in the namespace is that Lean wants it to be accessed on a Preorder like A, rather than on an element of its object set (like a)

Yakov Pechersky (Jan 20 2021 at 19:16):

How would ~> infer which A : Preorder you're talking about?

Eric Wieser (Jan 20 2021 at 19:17):

This is legal:

universe l
structure Preorder : Type (l + 1) :=
  (Obj : Type l)
  (Arr : Obj -> Obj -> Prop)
  (infixr `~>`:25 := Arr)
  (Some_prop : ∀ a b, a ~> b)

Eric Wieser (Jan 20 2021 at 19:19):

Ah, it sounds like you're not actually asking how to define notation to use within the structure definition though

Lime Sublime (Jan 20 2021 at 19:23):

Good point, Yakov. Is there a way to get something like a A.~> b? As you say, Eric, I'm trying to reference it not only in futher field definitions

Yakov Pechersky (Jan 20 2021 at 19:26):

universe l
structure Preorder : Type (l + 1) :=
  (Obj : Type l)
  (Arr : Obj -> Obj -> Prop)

local notation a `~>[` A `]` := A.Arr a

variables {A : Preorder} {a b : A.Obj}

#check a ~>[A] b

Yakov Pechersky (Jan 20 2021 at 19:29):

I edited to make it a little cleaner

Lime Sublime (Jan 20 2021 at 19:30):

Thanks! One thing I'd hope to be able to get is an arrow on many structures (Preorder, Category, 2-category ...). Can I get a notation that overloads based on the type of A?

Johan Commelin (Jan 20 2021 at 19:30):

yes, use typeclasses... see how + works on natural numbers, integers, and reals, etc...

Reid Barton (Jan 20 2021 at 19:31):

I think you can just write something like local notation a `~>` b := Preorder.Arr _ a b

Reid Barton (Jan 20 2021 at 19:32):

it will work as long as a and b have types already of the form Preorder.Obj _

Yakov Pechersky (Jan 20 2021 at 19:33):

Reid Barton said:

I think you can just write something like local notation a `~>` b := Preorder.Arr _ a b

Do you think it is better to make the notation "fully applied" as opposed to local notation a `~>` := Preorder.Arr _ a?

Reid Barton (Jan 20 2021 at 19:34):

I don't know, it just seems like a normal human way to write it

Reid Barton (Jan 20 2021 at 19:35):

in one project, I used the precedence values notation a ` ⟶ `:10 b:10 := Graph.hom _ a b

Lime Sublime (Jan 20 2021 at 19:35):

Wow, excellent!

Lime Sublime (Jan 20 2021 at 19:37):

Thanks for the help. The final thing I'm trying to figure out is if I can also overload ~> to be a synonym for Preorder homomorphisms (still trying to get my parameterised records working to give an example here)

Lime Sublime (Jan 20 2021 at 19:39):

Seems to work! Thanks all. Really happy I was able to get the notation I wanted

Reid Barton (Jan 20 2021 at 19:40):

Well preorders don't form a preorder, and overloading notation doesn't really work

Lime Sublime (Jan 20 2021 at 19:43):

Could you say more about how overloading notation doesn't work?

Reid Barton (Jan 20 2021 at 19:47):

I actually don't know much about how it doesn't work

Lime Sublime (Jan 20 2021 at 19:48):

Cool. I'll remain vigilant

Reid Barton (Jan 20 2021 at 19:50):

I've never tried it myself since ... my understanding is it doesn't really work :upside_down:

Lime Sublime (Jan 20 2021 at 19:52):

It's working so far!

Last updated: Dec 20 2023 at 11:08 UTC