Custom notation inside structures

Stream: new members

[Kuba]

Hi,
I have a structure whose constructor takes, among other things, a quaternary congruence relation and proofs of some of its properties as arguments. I would like to define a custom notation, so that I can write a b ≅ c d instead of congruence a b c d. However, if I use the notation command and then try to use the newly defined notation, I get an error.
My code:

structure space where
(point_t : Type)
(congruence : point_t → point_t → point_t → point_t → Prop)
notation a b " ≅ " c d => space.congruence a b c d
(symmetry_of_congruence : ∀ a b : point_t, a b ≅ b a)

Error message (relating to the congruence symbol on the last line):

expected token

[Chris Bailey]

The parser won't let you declare notation inside a structure declaration. You would want to declare the notation beforehand somewhere in the syntax/macro/notation hierarchy. One way of doing it (someone can probably give you a more clean implementation):

set_option hygiene false in
macro a:term b:term " ≅ " c:term:max d:term : term => `(congruence $a $b $c $d)

structure space where
(point_t : Type)
(congruence : point_t → point_t → point_t → point_t → Prop)
(symmetry_of_congruence : ∀ a b : point_t, a b ≅ b a)

#print space

[Eric Wieser]

Does putting the notation command in () help?

[Eric Wieser]

Oh nevermind, this is lean4

[Kuba]

Hmm, thanks for the answer, but I feel a bit queasy about disabling an option that has "hygiene" in its name. Does anyone know whether there is a cleaner way of doing this? I would have thought that my use case is a pretty common one. Or maybe the problem is with me using a lean structure here? What I am trying to achieve, is to describe a space made up of points and equipped with two relations that satisfy certain axioms. Both the points and the relations are primitive notions.

[Reid Barton]

Of course you can always manually expand the notation while defining the structure, and the worst that can happen is it may be hard to read/write.

[Reid Barton]

Sometimes it could also make sense to split the structure into two parts, and define the notation in between.

[Chris Bailey]

Kuba said:

Hmm, thanks for the answer, but I feel a bit queasy about disabling an option that has "hygiene" in its name. Does anyone know whether there is a cleaner way of doing this?

macro a:term b:term " ≅ " c:term:max d:term : term =>
  `($(mkIdent `congruence) $a $b $c $d)

(This produces pretty much identical code, but if it makes you feel better to not write the word hygiene, go for it)

[Kyle Miller]

"Hygienic macros" refers to making sure that identifiers in a macro expansion do not accidentally refer to local variables -- here, you do want congruence to refer to the local congruence. Think of it not that your macro is dirty, but that the hygiene system doesn't understand what you're trying to do.

Since congruence is the only literal identifier in your macro expansion, set_option hygiene false will only has affect on the handling of that one identifier.

[Kuba]

I see, that makes sense. What I ended up doing was separating out the two relations as separate type classes and then having the axioms as a structure. This is what I ended up with (the code has grown a bit since I started):

set_option autoImplicit false

class Congruence (point_t : Type) where
(congruence : point_t → point_t → point_t → point_t → Prop)
notation:37 a:38 b:38 " ≅ " c:max d:38 => Congruence.congruence a b c d

class Betweennes (point_t : Type) where
(betweennes : point_t → point_t → point_t → Prop)
notation:37 a:38 " B " b:max c:38 => Betweennes.betweennes a b c

-- Five Segment Configuration
def FSC {point_t : Type} [Congruence point_t] [Betweennes point_t]
(a b c d : point_t) (a' b' c' d' : point_t) : Prop :=
    b B a c ∧
    b' B a' c' ∧
    a b ≅ a' b' ∧
    b c ≅ b' c' ∧
    a d ≅ a' d' ∧
    b d ≅ b' d'

structure TarskisAxioms (point_t) [Congruence point_t] [Betweennes point_t] where
(congruence_of_reversed : ∀ a b : point_t, a b ≅ b a)
(transitivity_of_congruence :
    ∀ a b p q r s : point_t, a b ≅ p q ∧ a b ≅ r s → p q ≅ r s)
(identity_axiom_for_congruence : ∀ a b c : point_t, a b ≅ c c → a = b)
(segment_extension_axiom :
    ∀ o p a b : point_t, ∃ q : point_t, p B o q ∧ p q ≅ a b)
(five_segment_axiom :
    ∀ a b c d a' b' c' d' : point_t,
        FSC a b c d a' b' c' d' ∧ a ≠ b → c d ≅ c' d')
(identity_axiom_for_betweennes : ∀ a b : point_t, a B b b → a = b)

Does this approach make sense? I think this may be similar to how mathlib does it, but I only took a brief look. Also, how do you choose the precedence values? I think I managed to tune them by trial and error, but I am wondering if there is a recipe to follow.