Zulip Chat Archive

Stream: general

Topic: mem_preimage_eq

Patrick Massot (Jul 03 2019 at 13:59):

Is there any reason why mem_preimage_eq is stated as an equality rather than an iff? It seems contrary to the mathlib way

Chris Hughes (Jul 03 2019 at 14:02):

My guess is because it's stronger in the world without propext.

Kenny Lau (Jul 03 2019 at 14:04):

you can blame it on commit 8f4327a by digama0 on 15 Oct 2017:
https://github.com/leanprover-community/mathlib/commit/8f4327ae0c45ed36037beb1449f8285cae1ebe9c#diff-d076c0ad9beb03e207eb6ed5d354f5d5R497

Kenny Lau (Jul 03 2019 at 14:04):

or, in other words, it's because the code is 2 years old

Chris Hughes (Jul 03 2019 at 14:07):

I guess it means dsimp will use it.

Chris Hughes (Jul 03 2019 at 14:07):

Which is handy

Patrick Massot (Jul 03 2019 at 14:07):

@Mario Carneiro?

Mario Carneiro (Jul 03 2019 at 14:14):

I think it just predates the mathlib convention

Patrick Massot (Jul 03 2019 at 14:15):

Would you merge a PR changing this?

Mario Carneiro (Jul 03 2019 at 14:15):

also dsimp doesn't use iff.rfl lemmas unfortunately

Patrick Massot (Jul 03 2019 at 14:16):

Or maybe adding a mem_preimage_iff lemma if that dsimp thing is important?

Mario Carneiro (Jul 03 2019 at 14:16):

@Kenny Lau Actually that's not the origin; you can see it got moved in that commit but predates it

Mario Carneiro (Jul 03 2019 at 14:17):

I would merge such a PR

Mario Carneiro (Jul 03 2019 at 14:17):

I don't think the dsimp thing is a very big deal

Patrick Massot (Jul 03 2019 at 14:17):

Which version? Changing the lemma or adding a new one?

Mario Carneiro (Jul 03 2019 at 14:19):

changing the lemma

Patrick Massot (Jul 03 2019 at 14:22):

Should the new name be mem_preimage or mem_preimage_iff?

Mario Carneiro (Jul 03 2019 at 14:25):

I like mem_preimage if it's not already taken

Patrick Massot (Jul 03 2019 at 14:27):

It seems to exists in many namespaces but not the root one

Mario Carneiro (Jul 03 2019 at 14:27):

this one should be in the set namespace

Patrick Massot (Jul 03 2019 at 14:28):

actually it is

Patrick Massot (Jul 03 2019 at 14:28):

I didn't pay attention but this lemma is in the set namespace

Patrick Massot (Jul 03 2019 at 14:30):

Ok, let's see what Travis thinks about https://github.com/leanprover-community/mathlib/pull/1174

Last updated: Dec 20 2023 at 11:08 UTC