Zulip Chat Archive

Stream: general

Topic: iff vs eq


view this post on Zulip Yury G. Kudryashov (Jun 15 2020 at 01:46):

Do we have any guidelines on using p ↔ q vs p = q as the statement of a theorem? I see that mem_set_of_eq and some other set lemmas use = while many other lemmas use iff.

view this post on Zulip Jeremy Avigad (Jun 15 2020 at 15:29):

I don't think we do. The passage from iff to eq requires propositional extensionality. In early Lean history, we were worried about the effect of propext on computation, so when we could prove an equality without it (e.g. if the proof is refl), we favored that. But I don't know the effect of propext on computation is a big concern, and, if it isn't, it would be nice to standardize on iff.

view this post on Zulip Gabriel Ebner (Jun 15 2020 at 15:31):

A more practical issue is that dsimp does not use lemmas declared with iff, it can only use lemmas with eq where the proof is literally rfl. But this could be fixed.

view this post on Zulip Bryan Gin-ge Chen (Jun 15 2020 at 15:39):

Mario gave an example where the use of propext somewhere in factors was blocking computation here.

view this post on Zulip Johan Commelin (Jun 15 2020 at 16:12):

Gabriel Ebner said:

A more practical issue is that dsimp does not use lemmas declared with iff, it can only use lemmas with eq where the proof is literally rfl. But this could be fixed.

Sounds like a nice feature for lean-3.5.17 (-;

view this post on Zulip Sebastien Gouezel (Jun 15 2020 at 16:14):

Don't ask for more features for lean 3.5.17, it might delay it and I would be curious to see what lean#332 does to mathlib as soon as possible. I'm fine for 3.5.18, though!

view this post on Zulip Johan Commelin (Jun 15 2020 at 16:19):

Ok, 3.5.18 is a very nice version number as well (-;

view this post on Zulip Bhavik Mehta (Jun 15 2020 at 16:25):

Gabriel Ebner said:

A more practical issue is that dsimp does not use lemmas declared with iff, it can only use lemmas with eq where the proof is literally rfl. But this could be fixed.

Yeah I've been caught out by this a couple of times


Last updated: May 08 2021 at 03:17 UTC