changing default coercion

Stream: general

[Chris Hughes]

I've just defined the integers mod n, and since they are a comm_ring there is a default coercion from int. However rather than using the default coercion, it would be nicer to have quotient.mk as the coercion. Is there a way to change this?

[Simon Hudon]

I think if you declare the has_coe instance, it will use your instance whenever applicable before even trying the coercion from int to arbitrary comm_ring

[Kevin Buzzard]

Is there a risk of a diamond here though?

[Simon Hudon]

You mean like when you have multiple inheritance?

[Chris Hughes]

Is there a risk of a diamond here though?

What's the diamond? I think that the same idea has been used for coercions from nat to int. The only risk is if I make a coe from Zmod to int

[Kevin Buzzard]

the diamond occurs in 5 years' time when someone else imports your code and then writes down some innocuous-looking coe and stuff doesn't work. My question is whether this is a possibility

[Simon Hudon]

Not for any notion of diamond that I've worked with

[Kevin Buzzard]

Somehow what I was concerned about is that if someone one day writes down a coercion from the integers mod n to another comm_ring then they will have to deal with the issue that they now have two coercions from int to the other comm_ring which may not be defeq.

[Patrick Massot]

You could define a local instance

[Patrick Massot]

That way only people editing your file would have to deal with this

[Chris Hughes]

@Kevin Buzzard I don't think coercions are transitive, so if something is coerced from integers to integers mod n to R, then it will appear as two up arrows. I think these issues happen anyway with int to rat to real etc, and there are a load of lemmas proving equivalence of different permutations of coercions. I don't want a local coercion, because the quotient coercion is the most useful for everyone.

[Mario Carneiro]

There is definitely a "diamond risk", but of an even more trivial variety than an actual diamond: you are talking about two arrows from A to B in the category of typeclass instances, which is only acceptable (by my rule of thumb) if they are defeq, which presumably defeats the purpose of having a second coercion.

That said, in the specific case of replacing the default coercion, you can do it by similar methods to the ones used for int.of_nat, as Simon mentions, although you will have to prove lots of lemmas to replace the ones that int.cast gives you, and users will need to know that you are doing this since they have to refer to different lemmas.

Coercions are transitive, in the sense that if there is has_coe A B and has_coe B C and a C is needed where A is given, Lean will insert a single coe up-arrow with a composite typeclass instance. However, mathlib has a simp lemma explicitly to break these composite arrows up, because they work poorly with other simp lemmas that are all keyed to single coercions.