iff vs eq

Stream: general

[Yury G. Kudryashov]

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.

[Jeremy Avigad]

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.

[Gabriel Ebner]

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.

[Bryan Gin-ge Chen]

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

[Johan Commelin]

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 (-;

[Sebastien Gouezel]

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!

[Johan Commelin]

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

[Bhavik Mehta]

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