# Zulip Chat Archive

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