Zulip Chat Archive

Stream: maths

Topic: adjoining multiple elements notation


view this post on Zulip Thomas Browning (Sep 02 2020 at 21:16):

So currently the notation for adjoining multiple elements to a field is
notation K`⟮`:std.prec.max_plus l:(foldr `, ` (h t, set.insert h t) ∅) `⟯` := adjoin K l
(from field_theory/adjoin.lean).
This definition is causing us a few headaches since F⟮α⟯ is not equal to adjoin F {α}, and F⟮α,β⟯ is not equal to adjoin F {α,β} (and so on).
Does anyone know how to change the definition of the notation to fix this problem?
I think that this requires treating the first element differently, so that we start off by applying set.insert to a singleton, rather than to the empty set.

view this post on Zulip Yakov Pechersky (Sep 02 2020 at 21:27):

Would something like this work?

notation K``:std.prec.max_plus l`` := adjoin K {l}
notation K``:std.prec.max_plus α`,`l:(foldr `, ` (h t, set.insert h t) {α}) `` := adjoin K l

variables (α β: E)
#check Fα
#check Fα,β

view this post on Zulip Thomas Browning (Sep 02 2020 at 21:43):

that looks promising, although it seems to sometimes require casting that wasn't previously necessary:

notation K``:std.prec.max_plus l`` := adjoin K {l}
notation K``:std.prec.max_plus α`,`l:(foldr `, ` (h t, set.insert h t) {α}) `` := adjoin K l

--this works
lemma mem_adjoin_simple_self : α  (Fα : subalgebra F E) := sorry

--but this worked with the old notation
lemma mem_adjoin_simple_self : α  Fα := sorry

view this post on Zulip Reid Barton (Sep 02 2020 at 21:45):

I would wonder which notation is getting used there.

view this post on Zulip Reid Barton (Sep 02 2020 at 21:46):

Oh wait, only one has a comma in it ...

view this post on Zulip Reid Barton (Sep 02 2020 at 21:46):

er, rather only one doesn't have a comma

view this post on Zulip Patrick Lutz (Sep 02 2020 at 21:47):

maybe you need adjoin K (@singleton _ _ set.has_singleton l) instead of adjoin K {l}

view this post on Zulip Patrick Lutz (Sep 02 2020 at 21:48):

I think it's the same issue we ran into before

view this post on Zulip Patrick Lutz (Sep 02 2020 at 21:48):

where for some reason Lean gets confused about the type of {l}

view this post on Zulip Thomas Browning (Sep 02 2020 at 21:49):

Ok, so it seems like this works:

notation K``:std.prec.max_plus l`` := adjoin K (@singleton _ _ set.has_singleton l)
notation K``:std.prec.max_plus α`,`l:(foldr `, ` (h t, set.insert h t) {α}) `` := adjoin K l

and I haven't noticed any problems yet

view this post on Zulip Yakov Pechersky (Sep 02 2020 at 22:17):

You might need to change whether whitespace is necessary between the commas

view this post on Zulip Thomas Browning (Sep 02 2020 at 22:22):

here's an potential issue: it seems to be inserting the wrong way: F⟮α,β⟯ equals adjoin F {β, α}, I think.

view this post on Zulip Patrick Lutz (Sep 02 2020 at 22:42):

I think that was also a problem with the original notation

view this post on Zulip Patrick Lutz (Sep 02 2020 at 22:42):

but it would be good to fix

view this post on Zulip Patrick Lutz (Sep 02 2020 at 22:42):

maybe foldl instead of foldr?

view this post on Zulip Patrick Lutz (Sep 02 2020 at 22:43):

No, that doesn't make any difference actually

view this post on Zulip Thomas Browning (Sep 02 2020 at 22:59):

the big problem seems to be that Yakov's code pick's off the first element and inserts into that singleton

view this post on Zulip Thomas Browning (Sep 02 2020 at 23:00):

I think that you would instead have to pick off the last element

view this post on Zulip Patrick Lutz (Sep 02 2020 at 23:00):

Oh, good point

view this post on Zulip Patrick Lutz (Sep 02 2020 at 23:03):

Patrick Lutz said:

maybe foldl instead of foldr?

Oh, wait, this makes it worse. It means the entire list is flipped rather than just the first element being in the wrong place

view this post on Zulip Patrick Lutz (Sep 02 2020 at 23:10):

Is there some way of reversing a list in Lean?

view this post on Zulip Thomas Browning (Sep 02 2020 at 23:12):

list.reverse?

view this post on Zulip Patrick Lutz (Sep 02 2020 at 23:12):

we don't actually have a list though I guess

view this post on Zulip Thomas Browning (Sep 02 2020 at 23:12):

yeah, l is a set so you can't just add a reverse on the right hand side

view this post on Zulip Patrick Lutz (Sep 02 2020 at 23:12):

maybe we could first form a list then reverse it then turn it into a set

view this post on Zulip Thomas Browning (Sep 02 2020 at 23:13):

might work

view this post on Zulip Thomas Browning (Sep 02 2020 at 23:13):

there might even be automatic coersion list -> set

view this post on Zulip Patrick Lutz (Sep 02 2020 at 23:14):

Thomas Browning said:

there might even be automatic coersion list -> set

although we want the set we get to be definitionally equal to {a, b, c}

view this post on Zulip Thomas Browning (Sep 02 2020 at 23:14):

doesn't seem like there's automatic coersion

view this post on Zulip Thomas Browning (Sep 02 2020 at 23:14):

but there should be a way

view this post on Zulip Thomas Browning (Sep 02 2020 at 23:14):


view this post on Zulip Thomas Browning (Sep 02 2020 at 23:14):

notation K``:std.prec.max_plus l`` := adjoin K (@singleton _ _ set.has_singleton l)
notation K``:std.prec.max_plus α`,`l:(foldl `, ` (h t, list.insert h t) {α}) `` := adjoin K ((l.reverse) : set _)

view this post on Zulip Patrick Lutz (Sep 02 2020 at 23:14):

Patrick Lutz said:

maybe we could first form a list then reverse it then turn it into a set

why can't I give emoji reacts to my own messages?

view this post on Zulip Patrick Lutz (Sep 02 2020 at 23:16):

Thomas Browning said:

notation K``:std.prec.max_plus l`` := adjoin K (@singleton _ _ set.has_singleton l)
notation K``:std.prec.max_plus α`,`l:(foldl `, ` (h t, list.insert h t) {α}) `` := adjoin K ((l.reverse) : set _)

this seems to cause some problems

view this post on Zulip Thomas Browning (Sep 02 2020 at 23:16):

yeah, the coersion doesn't work

view this post on Zulip Patrick Lutz (Sep 02 2020 at 23:16):

oh

view this post on Zulip Patrick Lutz (Sep 02 2020 at 23:16):

why are the errors about decidable_eq?

view this post on Zulip Thomas Browning (Sep 02 2020 at 23:17):

no idea

view this post on Zulip Thomas Browning (Sep 02 2020 at 23:17):

if you add in a hypothesis about decidable_eq then it gives a coersion error

view this post on Zulip Patrick Lutz (Sep 02 2020 at 23:17):

I guess it has something to do with the elements of a list being allowed to be different but not the elements of a set?

view this post on Zulip Yakov Pechersky (Sep 02 2020 at 23:23):

Can you have a lemma that discusses adjoining a multiset?

view this post on Zulip Yakov Pechersky (Sep 02 2020 at 23:23):

Then you can use a list

view this post on Zulip Kyle Miller (Sep 02 2020 at 23:42):

This seems to work...

class fancy_insert {α : Type*} (s : set α) :=
(insert : α  set α)

@[priority 1000]
instance fancy_insert_empty {α : Type*} : fancy_insert ( : set α) :=
{ insert := λ x, @singleton _ _ set.has_singleton x }

@[priority 900]
instance fancy_insert_nonempty {α : Type*} (s : set α) : fancy_insert s :=
{ insert := λ x, set.insert x s }

notation K``:std.prec.max_plus l:(foldr `, ` (h t, fancy_insert.insert t h) ) `` := adjoin K l

view this post on Zulip Kyle Miller (Sep 02 2020 at 23:44):

(assuming I'm following what you're trying to accomplish)

view this post on Zulip Thomas Browning (Sep 02 2020 at 23:46):

Lovely! I think that works.


Last updated: May 10 2021 at 08:14 UTC