## Stream: maths

### Topic: adjoining multiple elements notation

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


#### 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


#### Reid Barton (Sep 02 2020 at 21:45):

I would wonder which notation is getting used there.

#### Reid Barton (Sep 02 2020 at 21:46):

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

#### Reid Barton (Sep 02 2020 at 21:46):

er, rather only one doesn't have a comma

#### Patrick Lutz (Sep 02 2020 at 21:47):

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

#### Patrick Lutz (Sep 02 2020 at 21:48):

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

#### Patrick Lutz (Sep 02 2020 at 21:48):

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

#### 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

#### Yakov Pechersky (Sep 02 2020 at 22:17):

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

#### 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.

#### Patrick Lutz (Sep 02 2020 at 22:42):

I think that was also a problem with the original notation

#### Patrick Lutz (Sep 02 2020 at 22:42):

but it would be good to fix

#### Patrick Lutz (Sep 02 2020 at 22:42):

maybe foldl instead of foldr?

#### Patrick Lutz (Sep 02 2020 at 22:43):

No, that doesn't make any difference actually

#### 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

#### Thomas Browning (Sep 02 2020 at 23:00):

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

Oh, good point

#### 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

#### Patrick Lutz (Sep 02 2020 at 23:10):

Is there some way of reversing a list in Lean?

list.reverse?

#### Patrick Lutz (Sep 02 2020 at 23:12):

we don't actually have a list though I guess

#### 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

#### Patrick Lutz (Sep 02 2020 at 23:12):

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

might work

#### Thomas Browning (Sep 02 2020 at 23:13):

there might even be automatic coersion list -> set

#### 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}

#### Thomas Browning (Sep 02 2020 at 23:14):

doesn't seem like there's automatic coersion

#### Thomas Browning (Sep 02 2020 at 23:14):

but there should be a way

#### Thomas Browning (Sep 02 2020 at 23:14):




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


#### 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?

#### 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

#### Thomas Browning (Sep 02 2020 at 23:16):

yeah, the coersion doesn't work

oh

#### Patrick Lutz (Sep 02 2020 at 23:16):

why are the errors about decidable_eq?

no idea

#### Thomas Browning (Sep 02 2020 at 23:17):

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

#### 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?

#### Yakov Pechersky (Sep 02 2020 at 23:23):

Can you have a lemma that discusses adjoining a multiset?

#### Yakov Pechersky (Sep 02 2020 at 23:23):

Then you can use a list

#### 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


#### Kyle Miller (Sep 02 2020 at 23:44):

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

#### Thomas Browning (Sep 02 2020 at 23:46):

Lovely! I think that works.

Last updated: May 10 2021 at 08:14 UTC