## Stream: general

### Topic: Local notation in a lemma not working

#### Eric Wieser (Jul 16 2020 at 09:03):

Could anyone tell me why this doesn't work?

lemma op_comm {T : Type} (a b c : T) (op : T → T) (infix * := op) : a * b * c = a * (b * c) := sorry


#### Eric Wieser (Jul 16 2020 at 09:04):

It fails because it cannot find has_mul T, but my hope was it would use the local infix instead.

#### Rob Lewis (Jul 16 2020 at 09:07):

I've never seen local notation introduced in a lemma like this before. I think it's out of scope to the right of the : already.

#### Utensil Song (Jul 16 2020 at 09:11):

I'm looking at this and there seem to be 3 problems:

#### Utensil Song (Jul 16 2020 at 09:14):

1. op should be op : T → T → T
2. * will refer to the global has_mul and might not have been shadowed by the local one, to rule out this factor, better try another unicode
3. when 1&2 is fixed, Lean seems to be confused by the syntax and give another error

Nice catch

#### Eric Wieser (Jul 16 2020 at 09:17):

Lean is happy with

lemma op_comm {T : Type} (a b c : T) : ∀  (op : T → T → T)  (infix * := op), a * b * c = a * (b * c) := sorry


#### Utensil Song (Jul 16 2020 at 09:17):

lemma op_comm {T : Type} (a b c : T) (op : T → T → T) (infix ⬝ := op) :
a ⬝ b ⬝ c = a ⬝ (b ⬝ c) := sorry


gives

2:2: goal
T : Type,
a b c : T,
op : T → T → T
⊢ ⁇

2:2: error:
invalid definition, '|' or ':=' expected
2:0: error:
type expected at
a
term has type
T
2:2: error:
command expected


#### Eric Wieser (Jul 16 2020 at 09:19):

It would be nice if I could push op back to the LHS of the colon, but this syntax isn't valid:

lemma op_comm {T : Type} (a b c : T)  (op : T → T → T) : ∀ (infix * := op), a * b * c = a * (b * c) := sorry


Is there a way to create a binder of no variables, as I attempt to do here?

#### Utensil Song (Jul 16 2020 at 09:19):

Eric Wieser said:

Lean is happy with

lemma op_comm {T : Type} (a b c : T) : ∀  (op : T → T → T)  (infix * := op), a * b * c = a * (b * c) := sorry


Oh, something might not survive moving from the right side of :/∀ to the left side

#### Utensil Song (Jul 16 2020 at 09:51):

lemma op_comm {T : Type}  (op : T → T → T) :
∀ (a b c : T) (infix * := op), a * b * c = a * (b * c) := sorry


The above works. It seems that Lean need something that's not a definition to be after ∀ and it makes sense since without that, Lean can't form a pi type here.

#### Utensil Song (Jul 16 2020 at 10:16):

lemma op_comm {T : Type} (a b c : T) (op : T → T → T) (infix ⬝ := op) (n : ℕ := 1) :
a = a := begin
/-
T : Type,
a b c : T,
op : T → T → T,
n : opt_param ℕ 1
⊢ a = a

-/


#### Utensil Song (Jul 16 2020 at 10:18):

The case above reveal the truth. Lean parser accepts such syntax for specifying optional parameter, but semantically it didn't register the infix under such syntax.

#### Utensil Song (Jul 16 2020 at 10:20):

This would be even more obvious in the following example:

reserve infix ⬝

variables {T : Type} (a b c : T)

#check a ⬝ b -- Lean chokes as \cdot is not defined

lemma op_comm {T : Type} (a b c : T) (op : T → T → T) (infix ⬝ := op) :
a ⬝ b = a ⬝ b := sorry
-- Lean chokes with the same error message


#### Mario Carneiro (Jul 16 2020 at 10:21):

infix binders are primarily used for structures. I've never seen them used in lemmas or in foralls

#### Mario Carneiro (Jul 16 2020 at 10:22):

I suspect this is an accident of the grammar

#### Utensil Song (Jul 16 2020 at 10:22):

In forall, it works:

lemma op_comm {T : Type} (a b c : T) :
∀  (op : T → T → T)  (infix * := op), a * b * c = a * (b * c) :=
begin
/-
T : Type,
a b c : T
⊢ ∀ (op : T → T → T), op (op a b) c = op a (op b c)
-/
end


#### Mario Carneiro (Jul 16 2020 at 10:22):

They have no actual impact on the shape of the term, they are not really foralls at all

#### Mario Carneiro (Jul 16 2020 at 10:24):

plus lean doesn't even really have a concept of locally scoped notations, and the implementation here is kind of a hack

#### Utensil Song (Jul 16 2020 at 10:24):

It may be just an unintentional side effect of some Lean C++ code for the one in forall to work while lhs of : doesn't

#### Mario Carneiro (Jul 16 2020 at 10:25):

I'm curious to see what @Sebastian Ullrich thinks about these sort of local local notations

#### Eric Wieser (Jul 16 2020 at 10:26):

I can push all the binders out of the forall with a dummy unit argument:

lemma op_comm {T : Type} (a b c : T) (op : T → T → T) :
∀ {_ : unit} (infix * := op), a * b * c = a * (b * c) := sorry


which feels like a nasty hack

#### Utensil Song (Jul 16 2020 at 10:27):

It seems to be the same mechanism why the following works:

universes u v

class functor'' (f : Type u → Type v) :=
(map : Π {α β : Type u}, (α → β) → f α → f β)
(infixr <$> := map)  Lean seems to be able to pick the notation up in general. #### Mario Carneiro (Jul 16 2020 at 10:29): yes, that's what I mean #### Mario Carneiro (Jul 16 2020 at 10:29): That's just a "binder sequence", and binder sequences appear elsewhere in the grammar as well #### Eric Wieser (Jul 16 2020 at 10:29): Yeah, I saw the notation for classes and wondered if I could get away with it for lemmas #### Eric Wieser (Jul 16 2020 at 10:30): Is there such a thing as an empty binder sequence in the grammar? #### Mario Carneiro (Jul 16 2020 at 10:30): Not directly. You can't write \forall, 2 = 2 for example #### Mario Carneiro (Jul 16 2020 at 10:31): But you can write structures with no fields #### Mario Carneiro (Jul 16 2020 at 10:32): structure unit' := mk structure unit'' := mk ::  #### Mario Carneiro (Jul 16 2020 at 10:33): you would think that structure unit''' :=  or structure unit''' := . or structure unit'''. would work but no #### Mario Carneiro (Jul 16 2020 at 10:34): bizarrely, structure unit'''' (x : ℕ) does work #### Mario Carneiro (Jul 16 2020 at 10:35): which means that structure unit'''' (infix * := ℕ)  also works #### Utensil Song (Jul 16 2020 at 10:35): These are all interesting parsing edge cases that may or may not survive when Lean 4 comes. #### Mario Carneiro (Jul 16 2020 at 10:36): I sure hope they die #### Utensil Song (Jul 16 2020 at 10:36): But it's interesting to read the related C++ code #### Mario Carneiro (Jul 16 2020 at 10:36): I can tell it's a ball of hacks and I don't even need to read the code #### Utensil Song (Jul 16 2020 at 10:37): Utensil Song said: It seems to be the same mechanism why the following works: universes u v class functor'' (f : Type u → Type v) := (map : Π {α β : Type u}, (α → β) → f α → f β) (infixr <$> := map)


Lean seems to be able to pick the notation up in general.

But I do wish this one to survive

It's very useful

#### Mario Carneiro (Jul 16 2020 at 10:38):

I would prefer to see it replaced by a proper notation scoping system

#### Utensil Song (Jul 16 2020 at 10:38):

Otherwise, I don't know how to express this: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/unbundled.20v.2Es.2E.20%28semi-%29bundled/near/204051388

#### Mario Carneiro (Jul 16 2020 at 10:39):

fields with := are nothing special

#### Mario Carneiro (Jul 16 2020 at 10:39):

those are just sugar for opt_param

#### Utensil Song (Jul 16 2020 at 10:41):

Unable to define notations in the process of defining a new structure/class, will make me break a structure/class into a few classes, with notations defined between them.

#### Utensil Song (Jul 16 2020 at 10:42):

Or I can't use notations to express Props using the operations defined for the class

#### Mario Carneiro (Jul 16 2020 at 10:44):

(x : A := a) is sugar for (x : opt_param A a)

#### Mario Carneiro (Jul 16 2020 at 10:45):

note that opt_param A a is defeq to A so this doesn't cause any typing problems, but the tag is used by lean as an elaboration hint

#### Utensil Song (Jul 16 2020 at 10:45):

Think

universes u v

class semigroup (G : Type u)
:=
(mul : G → G → G)
(infix ⬝ := mul)
(mul_assoc : ∀ a b c : G, a ⬝ b ⬝ c = a ⬝ (b ⬝ c))


for more complicated cases.

#### Mario Carneiro (Jul 16 2020 at 10:46):

I don't object to notations local to a structure at all (although I think that the gain is largely illusory since it doesn't survive parsing)

#### Mario Carneiro (Jul 16 2020 at 10:47):

I think that it should be part of an actual scoping system though

#### Mario Carneiro (Jul 16 2020 at 10:47):

rather than just something specific to binder sequences

#### Mario Carneiro (Jul 16 2020 at 10:48):

like there should be a let infix term constructor

#### Utensil Song (Jul 16 2020 at 10:48):

it doesn't survive parsing

Oh, that's true. I was already using the break-into-a-few-classes-and-define-notations-in-between way before I learned the existence of such a syntax. So I didn't notice it.

#### Mario Carneiro (Jul 16 2020 at 10:50):

if you just write one mega structure with 50 fields and several notation-worthy fields, and don't try to prove anything about the structure, then you will think this trick is great

#### Mario Carneiro (Jul 16 2020 at 10:50):

but once you try to inhabit the structure you will find it isn't very easy to work with the resulting structure definition

#### Utensil Song (Jul 16 2020 at 10:54):

Yes, for one, I noticed I still have to add

(fᵣ_defeq: fᵣ = algebra_map R G)


even after I have

(fᵣ : R →+* G := algebra_map R G)


#### Utensil Song (Jul 16 2020 at 10:55):

because the equality implied by := is only optional

#### Mario Carneiro (Jul 16 2020 at 10:55):

yep, the := is just a guideline

#### Mario Carneiro (Jul 16 2020 at 10:56):

it would be nice if structures actually supported let binders in the constructor. I think Coq does

#### Eric Wieser (Jul 16 2020 at 11:10):

Do you want (notation fᵣ := (algebra_map R G : R →+* G))?

#### Sebastian Ullrich (Jul 16 2020 at 14:48):

Mario Carneiro said:

like there should be a let infix term constructor

But there is.

#check let infix * := nat.mul in 1 * 2


Don't get too attached to it, however; since no-one has ever used - or apparently needed - it as far as we know, we will drop that one in Lean 4 since it complicates hygiene quite a bit. I think the introduction of proper namespace-scoped notations should more than offset that.

#### Eric Wieser (Jul 31 2020 at 10:38):

I've found that syntax quite useful for introducing notation in a recursive definition like

reserve infix  ⋏ :70
def wedge : Π {n}, Gₙ α n → Gₙ α n → Gₙ α n
| 0 x y := (x * y : α)
| (n + 1) ⟨x₁, x₂⟩ ⟨y₁, y₂⟩ := let infix  ⋏  := wedge in
(x₂ ⋏ y₂, x₁ ⋏ y₂ + x₂ ⋏ ̅y₁ᵈ)
infix  ⋏  := wedge


It still feels clumsy, but it would be great if whatever replaces let infix enables a similar approach

#### Utensil Song (Jul 31 2020 at 11:16):

What about declaring has_wedge.wedge first, then notation, then make an instance and implement wedge in it? This way would survive Lean 4 and the storyline is still clear?

#### Sebastian Ullrich (Jul 31 2020 at 11:27):

That issue is quite similar to the common pattern of declaring a structure/class with a notation, which is a bit awkward as well (having to redeclare the notation outside). I'd like to improve that one in Lean 4, so it would make sense to find a general solution that also works for def etc.

#### Utensil Song (Jul 31 2020 at 11:42):

Ah, my idea doesn't seem to work, Lean doesn't accept equation compiler in structure (not an #mwe , a sketch of the syntax idea):

universe u

variables (α : Type u) [field α]

-- multivectors
def Gₙ : ℕ → Type
| 0 := α
| (n + 1) := Gₙ n × Gₙ n

class has_wedge (α : Type u) := (wedge : α → α → α)
class has_vee   (α : Type u) := (vee : α → α → α)

infix  ⋏ :70 := has_wedge.wedge
infix  ⋎ :70 := has_vee.vee

class has_ga_ops (α : Type u) extends has_wedge α, has_vee α

instance ga_ops : has_ga_ops (Π {n}, Gₙ α n) := {
wedge
| 0 x y := (x * y : α)
| (n + 1) ⟨x₁, x₂⟩ ⟨y₁, y₂⟩ := (x₂ ⋏ y₂, x₁ ⋏ y₂ + x₂ ⋏ ̅y₁ᵈ),
vee
| 0 x y := (x * y : α)
| (n + 1) ⟨x₁, x₂⟩ ⟨y₁, y₂⟩ :=  (x₁ ⋎ y₂ + ̅x₂ ⋎ y₁, x₂ ⋎ y₂)
}


#### Mario Carneiro (Jul 31 2020 at 11:45):

oh wow that seems really hard to support

#### Eric Wieser (Jul 31 2020 at 11:55):

Is the solution to allow forward declarations? If I could forward declare def wedge : the_type := by patience, I could then associate a notation with it, and then fill out the definition later. Of course, this is still difficult in the equation compiler, where the local wedge isn't quite the global one.

#### Sebastian Ullrich (Jul 31 2020 at 11:56):

It really should be

mutual
infix  ⋏ :70 => wedge
def wedge : {n : _} → Gₙ α n → Gₙ α n → Gₙ α n
| 0, x, y => (x * y : α)
| n + 1, ⟨x₁, x₂⟩ ⟨y₁, y₂⟩ => (x₂ ⋏ y₂, x₁ ⋏ y₂ + x₂ ⋏ ̅y₁ᵈ)
end


Just have to implement that somehow...

#### Eric Wieser (Jul 31 2020 at 12:01):

The current syntax would make that more like the following, wouldn't it?

mutual def wedge, infix  ⋏ :70
with   ⋏  := wedge
with wedge : {n : _} → Gₙ α n → Gₙ α n → Gₙ α n
| 0, x, y := (x * y : α)
| n + 1, ⟨x₁, x₂⟩ ⟨y₁, y₂⟩ => (x₂ ⋏ y₂, x₁ ⋏ y₂ + x₂ ⋏ ̅y₁ᵈ)


#### Sebastian Ullrich (Jul 31 2020 at 12:03):

Well, I only know that I won't implement that one!

#### Eric Wieser (Jul 31 2020 at 12:17):

mutual ... end certainly seems a lot nicer!

Last updated: May 16 2021 at 05:21 UTC