notation

Stream: new members

[Michael Beeson]

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]

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]

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]

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

[Jeremy Avigad]

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]

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]

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]

It works :grinning:
What should I replace the [] with?
If I remove them it doesn't work anymore

[tica]

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

[Kevin Buzzard]

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]

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

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

[tica]

Thank you very much

[Eric Wieser]

What does Cong mean here?

[Eric Wieser]

Is it congruence of two line segments?

[tica]

@Eric Wieser Cong = Congruent

[tica]

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]

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

[Eric Wieser]

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 isCong' (a, b) (c, d) instead of Cong a b c d

[tica]

@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]

The alias doesn't work because the a⬝b ≅ c⬝d notation refers to tarski_relation.congruent not tarski.congruent

[Eric Wieser]

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

should work

[tica]

@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]

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

[Eric Wieser]

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

[tica]

Eric Wieser said:

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

Oh great I didn't know! Thanks

[Eric Wieser]

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]

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.