Zulip Chat Archive

Stream: general

Topic: simp-normal form for `b = some a`


Eric Wieser (Jun 24 2022 at 14:49):

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 (Jun 24 2022 at 14:51):

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

Anne Baanen (Jun 24 2022 at 15:47):

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 (Jun 24 2022 at 15:47):

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

Eric Wieser (Jun 24 2022 at 15:49):

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 (Jun 24 2022 at 16:12):

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

Eric Wieser (Jun 24 2022 at 16:16):

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 (Jun 24 2022 at 16:16):

But I guess the simp_nf linter will be the real test

Bhavik Mehta (Jun 24 2022 at 18:55):

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 (Jun 25 2022 at 00:46):

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

Violeta Hernández (Jun 25 2022 at 00:47):

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

Kyle Miller (Jun 25 2022 at 00:51):

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 (Jun 25 2022 at 19:04):

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 (Jun 25 2022 at 23:43):

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 (Jun 26 2022 at 01:44):

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


Last updated: Dec 20 2023 at 11:08 UTC