Zulip Chat Archive

Stream: maths

Topic: Lean can't figure out type of {a}


view this post on Zulip Thomas Browning (Aug 21 2020 at 20:29):

So we've been working with adjoining elements to fields:

import field_theory.subfield
import ring_theory.algebra

variables (F : Type*) [field F] {E : Type*} [field E] [algebra F E] (S : set E)

def adjoin : set E := field.closure (set.range (algebra_map F E)  S)

def adjoin_simple (α : E) : set E := adjoin F {α}

--this is fine
example (α : E) (x : F) : algebra_map F E x  (adjoin_simple F α) := sorry

--this is also fine
example (α : E) (x : F) : algebra_map F E x  adjoin F ({α} : set E) := sorry

--this doesn't work
example (α : E) (x : F) : algebra_map F E x  adjoin F {α} := sorry

but lean sometimes has trouble figuring out that if α : E then {α} : set E

How can we fix this?

view this post on Zulip Adam Topaz (Aug 21 2020 at 20:30):

You can always tell lean explicitly ({a} : set E).

view this post on Zulip Thomas Browning (Aug 21 2020 at 20:31):

The problem is when we try to define notation (give me a sec)

view this post on Zulip Thomas Browning (Aug 21 2020 at 20:31):

(deleted)

view this post on Zulip Thomas Browning (Aug 21 2020 at 20:31):

We would really like to get notation F[alpha] to work

view this post on Zulip Thomas Browning (Aug 21 2020 at 20:32):

(deleted)

view this post on Zulip Thomas Browning (Aug 21 2020 at 20:32):

import field_theory.subfield
import ring_theory.algebra

variables (F : Type*) [field F] {E : Type*} [field E] [algebra F E] (S : set E)

def adjoin : set E := field.closure (set.range (algebra_map F E)  S)

def adjoin_simple (α : E) : set E := adjoin F {α}

--this is fine
example (α : E) (x : F) : algebra_map F E x  (adjoin_simple F α) := sorry

--this is also fine
example (α : E) (x : F) : algebra_map F E x  adjoin F ({α} : set E) := sorry

--this doesn't work
example (α : E) (x : F) : algebra_map F E x  adjoin F {α} := sorry

notation K`[`:std.prec.max_plus β`]` := adjoin K {β}

--how can we get this to work?
example (α : E) (x : F) : algebra_map F E x  F[α] := sorry

--this works because it knows that F[α] is supposed to be in set E
example (α : E) (x : F) : F[α] = adjoin_simple F α := sorry

view this post on Zulip Thomas Browning (Aug 21 2020 at 20:34):

so the notation sometimes works when it already knows that F[α] is supposed to be in set E, but we would like this sort of notation to work more generally

view this post on Zulip Adam Topaz (Aug 21 2020 at 20:34):

It's a hack:

notation K`[`:std.prec.max_plus β`]` := adjoin K {x | x = β}

view this post on Zulip Thomas Browning (Aug 21 2020 at 20:34):

(deleted)

view this post on Zulip Thomas Browning (Aug 21 2020 at 20:34):

Oh, it looks like that works!

view this post on Zulip Thomas Browning (Aug 21 2020 at 20:35):

Is there any downside or is that hack as good as it looks?

view this post on Zulip Adam Topaz (Aug 21 2020 at 20:35):

Yeah, but someone who actually know how to write notation would give you a better answer :)

view this post on Zulip Adam Topaz (Aug 21 2020 at 20:37):

@Mario Carneiro Do you have any suggestions?

view this post on Zulip Mario Carneiro (Aug 21 2020 at 20:38):

Have you tried notation K`[`:std.prec.max_plus β`]` := adjoin K ({β} : set _)?

view this post on Zulip Thomas Browning (Aug 21 2020 at 20:38):

I think that I tried that

view this post on Zulip Thomas Browning (Aug 21 2020 at 20:39):

Yeah, that doesn't work unfortunately

view this post on Zulip Mario Carneiro (Aug 21 2020 at 20:40):

Oh, I see the problem now. Yeah you should make the notation unfold to adjoin_simple

view this post on Zulip Mario Carneiro (Aug 21 2020 at 20:42):

it's generally a bad idea to have notations unfold to things other than constant applied to variables

view this post on Zulip Patrick Lutz (Aug 21 2020 at 20:42):

Mario Carneiro said:

Oh, I see the problem now. Yeah you should make the notation unfold to adjoin_simple

We want to remove adjoin_simple

view this post on Zulip Adam Topaz (Aug 21 2020 at 20:42):

import field_theory.subfield
import ring_theory.algebra

variables (F : Type*) [field F] {E : Type*} [field E] [algebra F E] (S : set E)

def adjoin : set E := field.closure (set.range (algebra_map F E)  S)

def adjoin_simple (α : E) : set E := adjoin F ({α} : set _)

notation K`[`:std.prec.max_plus β`]` := adjoin_simple K β

--how can we get this to work?
example (α : E) (x : F) : algebra_map F E x  F[α] := sorry

view this post on Zulip Adam Topaz (Aug 21 2020 at 20:42):

Is that safe?

view this post on Zulip Mario Carneiro (Aug 21 2020 at 20:42):

Unfortunately lean has limited capacity to perform rewriting as part of notation expansion

view this post on Zulip Patrick Lutz (Aug 21 2020 at 20:43):

Adam Topaz said:

import field_theory.subfield
import ring_theory.algebra

variables (F : Type*) [field F] {E : Type*} [field E] [algebra F E] (S : set E)

def adjoin : set E := field.closure (set.range (algebra_map F E)  S)

def adjoin_simple (α : E) : set E := adjoin F ({α} : set _)

notation K`[`:std.prec.max_plus β`]` := adjoin_simple K β

--how can we get this to work?
example (α : E) (x : F) : algebra_map F E x  F[α] := sorry

Yeah, that's what we were doing before. But we kind of want to remove adjoin_simple

view this post on Zulip Mario Carneiro (Aug 21 2020 at 20:43):

You can make adjoin_simple reducible

view this post on Zulip Mario Carneiro (Aug 21 2020 at 20:43):

Or you can notate the type of α

view this post on Zulip Patrick Lutz (Aug 21 2020 at 20:43):

What do you mean?

view this post on Zulip Adam Topaz (Aug 21 2020 at 20:44):

import field_theory.subfield
import ring_theory.algebra

variables (F : Type*) [field F] {E : Type*} [field E] [algebra F E] (S : set E)

def adjoin : set E := field.closure (set.range (algebra_map F E)  S)

@[reducible]
def adjoin_simple (α : E) : set E := adjoin F ({α} : set _)

notation K`[`:std.prec.max_plus β`]` := adjoin_simple K β

--how can we get this to work?
example (α : E) (x : F) : algebra_map F E x  F[α] := sorry

view this post on Zulip Mario Carneiro (Aug 21 2020 at 20:45):

or

notation K`[`:std.prec.max_plus β`:`E`]` := adjoin K ({β} : set E)

example (α : E) (x : F) : algebra_map F E x  F[α:E] := sorry

view this post on Zulip Adam Topaz (Aug 21 2020 at 20:46):

By the way, from a mathematical point of view, this is confusing notation since K[α]K[\alpha] usually denotes the algebra generated by α\alpha and not the field generated by α\alpha, but I guess (...) doesn't work with notation?

view this post on Zulip Mario Carneiro (Aug 21 2020 at 20:47):

aha:

notation K`[`:std.prec.max_plus β`]` :=
adjoin K (@singleton _ _ set.has_singleton β)

example (α : E) (x : F) : algebra_map F E x  F[α] := sorry

view this post on Zulip Adam Topaz (Aug 21 2020 at 20:48):

Now how can we change [..] to (..)?

view this post on Zulip Patrick Lutz (Aug 21 2020 at 20:48):

Adam Topaz said:

By the way, from a mathematical point of view, this is confusing notation since K[α]K[\alpha] usually denotes the algebra generated by α\alpha and not the field generated by α\alpha, but I guess (...) doesn't work with notation?

Yeah, parentheses don't seem to work well in notation for some reason

view this post on Zulip Patrick Lutz (Aug 21 2020 at 20:48):

We're open to other suggestions for notation though (besides square brackets)

view this post on Zulip Mario Carneiro (Aug 21 2020 at 20:49):

how about F[(α)]

view this post on Zulip Mario Carneiro (Aug 21 2020 at 20:50):

you can also do funny things like F-(α)- as long as it doesn't begin with ( or end with )

view this post on Zulip Adam Topaz (Aug 21 2020 at 20:50):

Mario Carneiro said:

you can also do funny things like F-(α)- as long as it doesn't begin with ( or end with )

That looks awful!

view this post on Zulip Mario Carneiro (Aug 21 2020 at 20:51):

with unicode the Possibilities are Endless (TM)

view this post on Zulip Patrick Massot (Aug 21 2020 at 20:51):

Where are those zero-width unicode characters again?

view this post on Zulip Mario Carneiro (Aug 21 2020 at 20:51):

I recall seeing a talk about the mongolian vowel separator

view this post on Zulip Patrick Massot (Aug 21 2020 at 20:51):

In the perfectoid project we also used fancy parentheses.

view this post on Zulip Mario Carneiro (Aug 21 2020 at 20:52):

which is one of the few space characters that went through multiple character classes over the different unicode standards

view this post on Zulip Patrick Massot (Aug 21 2020 at 20:52):

https://github.com/leanprover-community/lean-perfectoid-spaces/blob/master/src/Spa/localization_Huber.lean#L28

view this post on Zulip Patrick Massot (Aug 21 2020 at 20:53):

Those are not actual parentheses.

view this post on Zulip Adam Topaz (Aug 21 2020 at 20:53):

My vscode doesn't like that (I think I'm missing some fonts :( )

view this post on Zulip Patrick Massot (Aug 21 2020 at 20:55):

That's one of the many reason why this isn't such a great idea (and it would probably not go through mathlib review).

view this post on Zulip Mario Carneiro (Aug 21 2020 at 20:55):

personally I greatly prefer "ascii art" to this kind of thing

view this post on Zulip Adam Topaz (Aug 21 2020 at 20:56):

F>>= a <<=?

view this post on Zulip Kevin Buzzard (Aug 21 2020 at 21:18):

I think those might already be used for monads

view this post on Zulip Kevin Buzzard (Aug 21 2020 at 21:19):

I would use four characters, then you'll be fine


Last updated: May 10 2021 at 06:13 UTC