# Zulip Chat Archive

## Stream: new members

### Topic: notation

#### Michael Beeson (Sep 21 2020 at 21:07):

Section 6.6 of Theorem Proving in Lean says,

Lean’s core library declares the left-binding powers of a number of common symbols.

https://github.com/leanprover/lean/blob/master/library/init/core.lean

You are welcome to overload these symbols for your own use, but you cannot change their binding power.

That seems to be false--in my ignorance I declared binding powers for some of these operators

at the top of my first file. If I remove those lines there's no problem with the parsing, indicating that

infix is still ok, but my proofs no longer check, indicating that the binding powers I had declared

were in force, rather than the defaults, before I removed those lines. Put those lines back, of

course the project builds again.

#### Pedro Minicz (Sep 22 2020 at 00:59):

I also believe that to be false. You _can_ change the binding power. Maybe what the book means is that you _probably_ shouldn't.

#### Pedro Minicz (Sep 22 2020 at 01:00):

For reference, this is an thread where redefining the binding power of existing notation fixed a problem I was having: https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Substitution.20notation

#### Pedro Minicz (Sep 22 2020 at 01:00):

Also. It is always possible that it wasn't possible when the book was written.

#### Jeremy Avigad (Sep 22 2020 at 15:57):

The statement was probably true when it was first written. Lean changed a lot over the years, and I am guessing that this changed and nobody noticed (until now) that the documentation was out of date. I'll fix it.

#### tica (Mar 13 2023 at 14:54):

Hello,

How does infix and notation work with lean 3? I can't find a complete source.

Is it possible to do this (it doesn't work):

```
constant Cong : Point → Point → Point → Point → Prop
notation `[`a b ≡ c d`]` := Cong a b c d
```

#### Alex J. Best (Mar 13 2023 at 15:00):

I don't know if its possible with spaces only between a b

```
constant Point : Type
constant Cong : Point → Point → Point → Point → Prop
notation `[` a `,` b ` ≡ ` c `,` d `]` := Cong a b c d
variables (a b c d : Point)
#check [a, b ≡ c, d]
```

this works though

Be careful definition notations too similar to core ones (like list) though, you may end up with strange errors

#### tica (Mar 13 2023 at 15:16):

It works :grinning:

What should I replace the `[]`

with?

If I remove them it doesn't work anymore

#### tica (Mar 13 2023 at 21:12):

Any other ideas? I'm looking for a solution to stop writing Cong a b c d

#### Kevin Buzzard (Mar 13 2023 at 21:56):

Choose weird brackets which aren't being used for anything else (so not `[`

or `{`

or `(`

) and you'll be in much better shape. If you don't intend on using Lie Algebras then you could use the brackets which they use.

#### Kyle Miller (Mar 13 2023 at 22:06):

I haven't tested it, but this probably would work too:

```
notation `C[` a `,` b ` ≡ ` c `,` d `]` := Cong a b c d
```

#### tica (Mar 13 2023 at 22:09):

Thank you very much

#### Eric Wieser (Mar 13 2023 at 22:30):

What does `Cong`

mean here?

#### Eric Wieser (Mar 13 2023 at 22:30):

Is it congruence of two line segments?

#### tica (Mar 13 2023 at 22:41):

@Eric Wieser `Cong = Congruent`

#### tica (Mar 13 2023 at 22:41):

Eric Wieser said:

Is it congruence of two line segments?

Yes, but it is with the axioms of traski so there are 4 points and not 2 segments

#### Kevin Buzzard (Mar 13 2023 at 23:22):

It's modelling dist(a,b)=dist(c,d) without numbers.

#### Eric Wieser (Mar 13 2023 at 23:40):

The reason I ask, is that if you worked in terms of segments (or just pairs of points) you could write `(a, b) ≡ (c, d)`

where your axiom is`Cong' (a, b) (c, d)`

instead of `Cong a b c d`

#### tica (Mar 14 2023 at 12:51):

@Eric Wieser I tried to follow your advice and here is what I did:

```
-- basic.lean
import tactic.alias
structure segment (Point : Type*) := (a b : Point)
infix `⬝`:56 := segment.mk
class tarski_relation (Point : Type*) :=
--`B a b c` means that `c` is between `a` and `b`
(between : Point → segment Point → Prop)
--`C a b c d` means that `a b` and `c d` are congruent segments
(congruent : segment Point → segment Point → Prop)
infix ` ≅ `:50 := tarski_relation.congruent
variables {α : Type*}[tarski_relation α]
instance : has_mem α (segment α) := ⟨λ p s, tarski_relation.between p s⟩
class tarski (Point : Type*) extends tarski_relation Point:=
--A1
(cong_pseudo_reflexive : ∀ a b : Point, a⬝b ≅ b⬝a)
--A2
(cong_inner_transitivity : ∀ a b c d e f : Point, a⬝b ≅ c⬝d → a⬝b ≅ e⬝f → c⬝d ≅ e⬝f)
--A3
(cong_identity : ∀ a b c : Point, a⬝b ≅ c⬝c → a = b)
--A4
( segment_construction : ∀ a b c d : Point, ∃ e, b ∈ a⬝e ∧ b⬝e ≅ c⬝d)
--A5
( five_segment : ∀ a a' b b' c c' d d' : Point,
a⬝b ≅ a'⬝b' ∧ b⬝c ≅ b'⬝c' ∧ a⬝d ≅ a'⬝d' ∧ b⬝d ≅ b'⬝d' ∧
b ∈ a⬝c ∧ b' ∈ a'⬝c' ∧ a ≠ b → c⬝d ≅ c'⬝d')
--....
alias tarski_relation.between ← tarski.between
alias tarski_relation.congruent ← tarski.congruent
alias tarski.cong_inner_transitivity ← tarski.congruent.inner_transitivity
alias tarski.cong_pseudo_reflexive ← tarski.congruent.pseudo_reflexive
alias tarski.cong_identity ← tarski.congruent.identity
class tarski_2d (Point : Type*) extends tarski Point:=
-- A9
(upper_dim : ∀ a b c p q : Point, p ≠ q ∧ a⬝p ≅ a⬝q ∧ b⬝p ≅ b⬝q ∧ c⬝p ≅ c⬝q →
b ∈ a⬝c ∨ c ∈ b⬝a ∨ c ∈ a⬝b)
```

```
--cong.lean
import tactic
import basic
variables {Point : Type*} [tarski Point]
namespace tarski
@[refl] lemma congruent.refl {a b : Point} : a⬝b ≅ a⬝b :=
begin
apply cong_inner_transitivity,
apply cong_pseudo_reflexive,
apply cong_pseudo_reflexive,
end
@[symm]lemma congruent.symm {a b c d : Point} : a⬝b ≅ c⬝d → c⬝d ≅ a⬝b :=
begin
intro h,
apply cong_inner_transitivity,
apply h,
refl,
end
end tarski
example {a b c d : Point} : a⬝b ≅ c⬝d → c⬝d ≅ a⬝b :=
begin
intro h,
apply tarski.congruent.symm h,
end
```

Is this a good way to do it?

I also have an error that I don't understand.

That works:

```
example {a b c d : Point} : a⬝b ≅ c⬝d → c⬝d ≅ a⬝b :=
begin
intro h,
apply tarski.congruent.symm h,
end
```

It does not work :

```
example {a b c d : Point} : a⬝b ≅ c⬝d → c⬝d ≅ a⬝b :=
begin
intro h,
apply h.symm,
end
```

```
invalid field notation, 'symm' is not a valid "field" because environment does not contain 'tarski_relation.congruent.symm'
h
which has type
a⬝b ≅ c⬝d
Additional information:
src\geometry.lean: context: invalid field notation, 'symm' is not a valid "field" because environment does not contain 'tarski_relation.rec.symm'
h
which has type
tarski_relation.rec
(λ (between : Point → segment Point → Prop) (congruent : segment Point → segment Point → Prop), congruent)
tarski.to_tarski_relation
(a⬝b)
(c⬝d)
state:
Point : Type u_1,
_inst_1 : tarski Point,
a b c d : Point,
h : a⬝b ≅ c⬝d
⊢ c⬝d ≅ a⬝b
```

I thought the alias would make it work.

#### Eric Wieser (Mar 14 2023 at 12:54):

The alias doesn't work because the `a⬝b ≅ c⬝d`

notation refers to `tarski_relation.congruent`

not `tarski.congruent `

#### Eric Wieser (Mar 14 2023 at 12:54):

```
alias tarski_relation.congruent ← tarski.congruent
infix ` ≅ `:50 := tarski.congruent
```

should work

#### tica (Mar 14 2023 at 13:09):

@Eric Wieser I had thought about it but I wanted to be able to use the new notations in the 'tarski' class.

In this case my class 'tarski_relation' is no longer useful

#### Eric Wieser (Mar 14 2023 at 13:10):

`tarski`

doesn't need to exist yet when you define that alias

#### Eric Wieser (Mar 14 2023 at 13:10):

There's no rule that prevents you defining `foo.bar`

before defining `foo`

.

#### tica (Mar 14 2023 at 13:12):

Eric Wieser said:

`tarski`

doesn't need to exist yet wen you define that alias

Oh great I didn't know! Thanks

#### Eric Wieser (Mar 14 2023 at 13:13):

Note that

```
(cong_inner_transitivity : ∀ a b c d e f : Point, a⬝b ≅ c⬝d → a⬝b ≅ e⬝f → c⬝d ≅ e⬝f)
```

will be more convenient to use as

```
(cong_inner_transitivity : ∀ ab cd ef : segment Point, ab ≅ cd → ab ≅ ef → cd ≅ ef)
```

#### tica (Mar 14 2023 at 13:19):

Eric Wieser said:

Note that

`(cong_inner_transitivity : ∀ a b c d e f : Point, a⬝b ≅ c⬝d → a⬝b ≅ e⬝f → c⬝d ≅ e⬝f)`

will be more convenient to use as

`(cong_inner_transitivity : ∀ ab cd ef : segment Point, ab ≅ cd → ab ≅ ef → cd ≅ ef)`

Indeed, I remained in the 'style' of tarski but I can go further.

Last updated: Dec 20 2023 at 11:08 UTC