adjoining multiple elements notation

Stream: maths

[Thomas Browning]

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.

[Yakov Pechersky]

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⟮α,β⟯

[Thomas Browning]

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

[Reid Barton]

I would wonder which notation is getting used there.

[Reid Barton]

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

[Reid Barton]

er, rather only one doesn't have a comma

[Patrick Lutz]

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

[Patrick Lutz]

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

[Patrick Lutz]

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

[Thomas Browning]

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

[Yakov Pechersky]

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

[Thomas Browning]

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

[Patrick Lutz]

I think that was also a problem with the original notation

[Patrick Lutz]

but it would be good to fix

[Patrick Lutz]

maybe foldl instead of foldr?

[Patrick Lutz]

No, that doesn't make any difference actually

[Thomas Browning]

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

[Thomas Browning]

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

[Patrick Lutz]

Oh, good point

[Patrick Lutz]

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

[Patrick Lutz]

Is there some way of reversing a list in Lean?

[Thomas Browning]

list.reverse?

[Patrick Lutz]

we don't actually have a list though I guess

[Thomas Browning]

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

[Patrick Lutz]

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

[Thomas Browning]

might work

[Thomas Browning]

there might even be automatic coersion list -> set

[Patrick Lutz]

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}

[Thomas Browning]

doesn't seem like there's automatic coersion

[Thomas Browning]

but there should be a way

[Thomas Browning]

[Thomas Browning]

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 _)

[Patrick Lutz]

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?

[Patrick Lutz]

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

[Thomas Browning]

yeah, the coersion doesn't work

[Patrick Lutz]

oh

[Patrick Lutz]

why are the errors about decidable_eq?

[Thomas Browning]

no idea

[Thomas Browning]

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

[Patrick Lutz]

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?

[Yakov Pechersky]

Can you have a lemma that discusses adjoining a multiset?

[Yakov Pechersky]

Then you can use a list

[Kyle Miller]

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

[Kyle Miller]

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

[Thomas Browning]

Lovely! I think that works.