Zulip Chat Archive

Stream: general

Topic: Local notation in a lemma not working


view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Utensil Song (Jul 16 2020 at 09:11):

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

view this post on Zulip 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

view this post on Zulip Eric Wieser (Jul 16 2020 at 09:16):

Nice catch

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

-/

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Jul 16 2020 at 10:22):

I suspect this is an accident of the grammar

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Jul 16 2020 at 10:25):

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

view this post on Zulip 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

view this post on Zulip 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)

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

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

view this post on Zulip Mario Carneiro (Jul 16 2020 at 10:29):

yes, that's what I mean

view this post on Zulip Mario Carneiro (Jul 16 2020 at 10:29):

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

view this post on Zulip 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

view this post on Zulip Eric Wieser (Jul 16 2020 at 10:30):

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

view this post on Zulip Mario Carneiro (Jul 16 2020 at 10:30):

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

view this post on Zulip Mario Carneiro (Jul 16 2020 at 10:31):

But you can write structures with no fields

view this post on Zulip Mario Carneiro (Jul 16 2020 at 10:32):

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

view this post on Zulip Mario Carneiro (Jul 16 2020 at 10:33):

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

view this post on Zulip Mario Carneiro (Jul 16 2020 at 10:34):

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

view this post on Zulip Mario Carneiro (Jul 16 2020 at 10:35):

which means that

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

also works

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Jul 16 2020 at 10:36):

I sure hope they die

view this post on Zulip Utensil Song (Jul 16 2020 at 10:36):

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

view this post on Zulip 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

view this post on Zulip 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)

(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

view this post on Zulip Utensil Song (Jul 16 2020 at 10:38):

It's very useful

view this post on Zulip Mario Carneiro (Jul 16 2020 at 10:38):

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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Jul 16 2020 at 10:39):

fields with := are nothing special

view this post on Zulip Mario Carneiro (Jul 16 2020 at 10:39):

those are just sugar for opt_param

view this post on Zulip Eric Wieser (Jul 16 2020 at 10:41):

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

view this post on Zulip 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.

view this post on Zulip Utensil Song (Jul 16 2020 at 10:42):

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

view this post on Zulip Mario Carneiro (Jul 16 2020 at 10:44):

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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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)

view this post on Zulip Mario Carneiro (Jul 16 2020 at 10:47):

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

view this post on Zulip Mario Carneiro (Jul 16 2020 at 10:47):

rather than just something specific to binder sequences

view this post on Zulip Mario Carneiro (Jul 16 2020 at 10:48):

like there should be a let infix term constructor

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip Utensil Song (Jul 16 2020 at 10:55):

because the equality implied by := is only optional

view this post on Zulip Mario Carneiro (Jul 16 2020 at 10:55):

yep, the := is just a guideline

view this post on Zulip 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

view this post on Zulip Eric Wieser (Jul 16 2020 at 11:10):

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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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₂)
}

view this post on Zulip Mario Carneiro (Jul 31 2020 at 11:45):

oh wow that seems really hard to support

view this post on Zulip 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.

view this post on Zulip 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...

view this post on Zulip 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₁)

view this post on Zulip Sebastian Ullrich (Jul 31 2020 at 12:03):

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

view this post on Zulip Eric Wieser (Jul 31 2020 at 12:17):

mutual ... end certainly seems a lot nicer!


Last updated: May 16 2021 at 05:21 UTC