simp-normal form for `b = some a`

Stream: general

[Eric Wieser]

docs#option.mem_def (a ∈ b ↔ b = option.some a) is already marked simp, but we have a lot of iff lemmas with a ∈ b on the LHS (eg docs#alist.mem_lookup_union). Should we change all of these to use the = spelling?

This comes up in #14930, as lean 3.44.0 is much more eager to apply option.mem_def than it used to be.

[Eric Wieser]

Alternatively, we could make option.mem_def not be a simp lemma

[Anne Baanen]

On the one hand, simping away all instances of a ∈ b seems weird to me, because why define that notation in the first place? On the other hand, b = some a is much more familiar/useful to me than a ∈ b so I'd rather keep mem_def.

[Anne Baanen]

So I'm going to cast a weak vote for the = spelling.

[Eric Wieser]

If we made option.mem_def not a simp lemma, we could replace it with docs#option.mem_some_iff being simp

[Yaël Dillies]

I agree that the has_mem instance is a bit weird and I certainly haven't used it myself.

[Eric Wieser]

It turns out that there's not quite as much fallout from this as I expected, so perhaps we don't need to decide before bumping to lean 3.44.0

[Eric Wieser]

But I guess the simp_nf linter will be the real test

[Bhavik Mehta]

The has_mem instance here is used a lot in finset.max and related, but in that case also I think it would be nicer to have the = some versoin

[Violeta Hernández]

Strong vote for the =, I find the ∈ notation to be very odd

[Violeta Hernández]

And we already have the simp lemma, so might as well use it

[Kyle Miller]

I've used the has_mem notation for option a few times, and it can be convenient in meta code.

I think what you're supposed to do is imagine that option could have been defined as lists of length at most 1.

[Violeta Hernández]

That logic makes sense, but
a) using set notation for things that aren't sets or very similar reeks of ZFC
b) we don't employ this logic in other places where it would make sense, like for α ⊕ β or Σ i, α i (with the appropriate instances)

[Kyle Miller]

Regarding (a), pretty much every mathlib data structure that contains elements in some sense has a has_mem instance. I mentioned list because it has the same computational properties (and there's a map of monads from option to list), but, except for issues of computational relevance, option could also have been defined as sets of cardinality at most 1. (Just for fun, the commit where this has_mem instance was introduced, five years ago.)

Regarding (b), I'm not sure I'm following; could you write out those instances?

[Yakov Pechersky]

An issue with the = based expressions is that = has two syntactically different yet propositionally equal forms, b = some a and some a = b. While the has_mem has only one