Local notation in a lemma not working

Stream: general

[Eric Wieser]

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]

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

[Rob Lewis]

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]

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

[Utensil Song]

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

[Eric Wieser]

Nice catch

[Eric Wieser]

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]

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]

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]

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]

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]

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]

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]

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]

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

[Mario Carneiro]

I suspect this is an accident of the grammar

[Utensil Song]

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]

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

[Mario Carneiro]

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

[Utensil Song]

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]

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

[Eric Wieser]

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]

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)

(from https://github.com/leanprover/lean/wiki/Refactoring-structures#other-goodies )

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

[Mario Carneiro]

yes, that's what I mean

[Mario Carneiro]

That's just a "binder sequence", and binder sequences appear elsewhere in the grammar as well

[Eric Wieser]

Yeah, I saw the notation for classes and wondered if I could get away with it for lemmas

[Eric Wieser]

Is there such a thing as an empty binder sequence in the grammar?

[Mario Carneiro]

Not directly. You can't write \forall, 2 = 2 for example

[Mario Carneiro]

But you can write structures with no fields

[Mario Carneiro]

structure unit' := mk
structure unit'' := mk ::

[Mario Carneiro]

you would think that structure unit''' := or structure unit''' := . or structure unit'''. would work but no

[Mario Carneiro]

bizarrely, structure unit'''' (x : ℕ) does work

[Mario Carneiro]

which means that

structure unit'''' (infix `*` := ℕ)

also works

[Utensil Song]

These are all interesting parsing edge cases that may or may not survive when Lean 4 comes.

[Mario Carneiro]

I sure hope they die

[Utensil Song]

But it's interesting to read the related C++ code

[Mario Carneiro]

I can tell it's a ball of hacks and I don't even need to read the code

[Utensil Song]

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)

(from https://github.com/leanprover/lean/wiki/Refactoring-structures#other-goodies )

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

But I do wish this one to survive

[Utensil Song]

It's very useful

[Mario Carneiro]

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

[Utensil Song]

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]

fields with := are nothing special

[Mario Carneiro]

those are just sugar for opt_param

[Eric Wieser]

What's the un-sugared syntax, and where can I read about it?

[Utensil Song]

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]

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

[Mario Carneiro]

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

[Mario Carneiro]

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]

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]

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]

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

[Mario Carneiro]

rather than just something specific to binder sequences

[Mario Carneiro]

like there should be a let infix term constructor

[Utensil Song]

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]

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]

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]

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]

because the equality implied by := is only optional

[Mario Carneiro]

yep, the := is just a guideline

[Mario Carneiro]

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

[Eric Wieser]

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

[Sebastian Ullrich]

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]

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]

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]

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]

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]

oh wow that seems really hard to support

[Eric Wieser]

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]

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]

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]

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

[Eric Wieser]

mutual ... end certainly seems a lot nicer!