can coercions be abused?

Stream: general

[Edward Ayers]

I've added some questionable coercions to a lean file I am working on:

instance [partial_order α] : has_coe (a = b) (a ≤ b) := ⟨le_of_eq⟩
instance : has_coe (a = b) (b = a) := ⟨eq.symm⟩

They work great in the file that I am working on because it means I can now do things like

lemma (p :a ≤ b) (q:c = b) :a ≤ c  := le_trans p q

Within a bigger proof and I don't have to use any tactics or faff around making sure equalities match up.
Are there any pitfalls to this approach or is it good practice?

[Kenny Lau]

wow

[Edward Ayers]

In particular I am worried that stuff like has_coe (a = b) (b = a) will cause a loop of doom in the elaborator.

[Mario Carneiro]

it will

[Mario Carneiro]

you will probably get a timeout coercing a = b to a = c

[Edward Ayers]

example (p : a = c) : a = b := p

doesn't loop forever with the above coercion. How can I get the bad behaviour?

[Mario Carneiro]

hm, not sure in that case. I will downgrade from "bad" to "highly suspicious"

[Edward Ayers]

I will leave it in and keep coding and see if it explodes anywhere.

[Mario Carneiro]

seems reasonable

[Edward Ayers]

It has saved me a lot of typing.

[Mario Carneiro]

I can believe it

[Patrick Massot]

Ed, have you tried Simon's mono tactic, from https://github.com/leanprover-community/mathlib-nursery/blob/master/src/tactic/monotonicity/interactive.lean (see also https://github.com/leanprover-community/mathlib-nursery/blob/master/docs/monotonicity.md)

[Edward Ayers]

That's a nice tactic. I am now thinking that it is bad practice to use coercions to do reasoning because your code now depends directly on the minutiae of how the elaborator works, which is somewhat opaque and subject to change. Whereas the tactics have well-defined behaviour and can be tuned.
However it is cool that the elaborator was able deal with my coercion abuse nicely. Are there any docs which specify precisely what the elaborator is doing when it looks for coercions?

[Patrick Massot]

source code?