## Stream: general

### Topic: iff vs eq

#### 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.

#### 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.

#### 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.

#### 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.

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

#### 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!

#### Johan Commelin (Jun 15 2020 at 16:19):

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

#### 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