cast vs coe

Stream: new members

[Damiano Testa]

Dear All,

I often struggle to know whether a lemma about coercions should have coe or cast in its name. My vague rule is that most of the time cast is for ℕ, while coe is for everything else.

Is there a stricter convention than this?

Thanks!

[Mario Carneiro]

The name of the coercion from nat -> A is nat.cast, and similarly for int.cast and rat.cast. Other coercions might have their own names but are usually referred to as coe

[Mario Carneiro]

In particular, there are two coercions declared for nat -> int, and the usual one does not resolve to nat.cast, it unfolds to int.of_nat. This one is referred to as coe when it is used via coe and of_nat when the int.of_nat function is used directly

[Damiano Testa]

Thanks Mario, this helps!

[Damiano Testa]

Just to make sure I understand, the "other" coercion ℕ →ℤ is the weird [-1-n] (or whatever the correct symbols are), right?

[Mario Carneiro]

The other one is nat.cast

[Mario Carneiro]

nat.cast : nat -> A where A is any monoid with one

[Mario Carneiro]

and int is a monoid with one so you can use nat.cast to coerce nat -> int

[Damiano Testa]

Ok, thanks. What I said above was nonsense.

[Mario Carneiro]

but there is another coercion which is defined specifically for nat -> int and overrides this blanket implementation

[Mario Carneiro]

using int.of_nat

[Mario Carneiro]

to get the nat.cast coercion you have to write it out like @coe nat int nat.cast_coe or so

[Mario Carneiro]

the only place this is done, more or less, is in the proof that this is equal to the preferred coe based on int.of_nat

[Mario Carneiro]

but this is a genuine diamond in the typeclass system that you have to watch out for since it's not a defeq

[Damiano Testa]

Ok, I get it now. In my mistaken comment above, I guess that I was using -1 as the has_one of ℤ.

[Mario Carneiro]

yeah that one's not a declared coe (it would probably be even more confusing)

[Mario Carneiro]

there's probably a way to get it using nat.cast : nat -> opposite int or something

[Damiano Testa]

There might be a way, but I'm not sure that I want to learn it, lest I get even more confused!

[Damiano Testa]

Thanks Mario! I have a better understanding now of this cast vs coe issue! And also I did not realize the subtlety of the two maps ℕ →ℤ.