has_coe_to_fun on iff

Stream: general

[Eric Wieser]

What would the opinion be on adding:

instance {P Q : Prop} : has_coe_to_fun (P ↔ Q) := ⟨_, iff.mp⟩

The argument would be twofold:

• It's consistent with how equiv decays to a function in the forward direction
• It would enable dot notation for things like and.comm:

variables {P Q : Prop} (h : P ∧ Q)
#check h.comm

[Eric Wieser]

(deleted)

[Eric Wieser]

/poll Is this a good idea?

[Patrick Massot]

For teaching that would be a disaster.

[Eric Wieser]

How so? The model only changes from "an iff is a pair of a forward and backward implication" to "an iff is a forward implication with an associated backward implication". That difference doesn't seem particularly troublesome.

[Mario Carneiro]

You can use and.symm instead of and.comm if you want the version that works with dot notation

[Mario Carneiro]

Also, has_coe_to_fun doesn't enable the use of dot notation like this

[Eric Wieser]

It does enable dot notation, the #check above works iff you also include the instance I start this thread with

[Eric Wieser]

and.symm is just an example, there are many other cases where the lack of this coercion makes us pick between a weak statement with dot notation, a strong statement without, or having to come up with two names for the same thing

[Patrick Massot]

Eric Wieser said:

How so? The model only changes from "an iff is a pair of a forward and backward implication" to "an iff is a forward implication with an associated backward implication". That difference doesn't seem particularly troublesome.

Students already have a lot of difficulties with the distinction between implication and equivalences. Anything that blurs this distinction would be awful.

[Bryan Gin-ge Chen]

For what it's worth, I still sometimes find the use of equivs as functions difficult to parse since the names are not what I intuitively expect. However, the inconsistency between equiv and iff here is a bit strange.

Lean 3 doesn't give us any way to disable instances once they've been declared, right? What about Lean 4?

[Eric Wieser]

Sure it does, local attribute [-instance]

[Patrick Massot]

Except in this case we need to go in the other direction. Have a def and let Eric use local attribute [instance] when he wants to use it.

[Kyle Miller]

I also have thought that the inconsistency between equiv and iff was odd. I wouldn't want mathlib to change the way it states theorems if this were a feature (so we would keep both and.symm and and.comm), but it would be nice being able to write foo a h rather than (foo a).mp h.

Maybe as a compromise, since for teaching you wouldn't want students to unwittingly use iffs in place of implications, we introduce a mathlib locale with fancy features such as this one.

[Violeta Hernández]

I like the idea because it means I don't have to write .1 everywhere

[Yaël Dillies]

This sounds like a terrible idea because has_coe_to_fun is quite fragile and our current use already breaks often enough. Further, iffs are usually quite polymorphic, so Lean will have an even harder time unifying.

[Gabriel Ebner]

In this case, has_coe_to_fun shouldn't be fragile at all afaict.

[Gabriel Ebner]

It should work just as well as writing .1 manually.

[Kyle Miller]

Yeah, that's my understanding -- when you syntactically have x y and x isn't obviously a function, then Lean will use a has_coe_to_fun instance for x.

[Eric Wieser]

Yaël Dillies said:

This sounds like a terrible idea because has_coe_to_fun is quite fragile and our current use already breaks often enough. Further, iffs are usually quite polymorphic, so Lean will have an even harder time unifying.

If you're describing what I think you are (the various breakage to dot notation in bundled homs every time someone adds a new typeclass in the hierarchy), that's not relevant here because:

• Almost no one is going to state or a theorem with iff.mp in the statement, whether it's spelt with coe_fn or otherwise
• iff has no typeclass arguments which can end up unified incorrectly