`NatCast`

#

We introduce the typeclass `NatCast R`

for a type `R`

with a "canonical
homomorphism" `Nat → R`

. The typeclass carries the data of the function,
but no required axioms.

This typeclass was introduced to support a uniform `simp`

normal form
for such morphisms.

Without such a typeclass, we would have specific coercions such as
`Int.ofNat`

, but also later the generic coercion from `Nat`

into any
Mathlib semiring (including `Int`

), and we would need to use `simp`

to
move between them. However `simp`

lemmas expressed using a non-normal
form on the LHS would then not fire.

Typically different instances of this class for the same target type `R`

are definitionally equal, and so differences in the instance do not
block `simp`

or `rw`

.

This logic also applies to `Int`

and so we also introduce `IntCast`

alongside
`Int.

## Note about coercions into arbitrary types: #

Coercions such as `Nat.cast`

that go from a concrete structure such as
`Nat`

to an arbitrary type `R`

should be set up as follows:

```
instance : CoeTail Nat R where coe := ...
instance : CoeHTCT Nat R where coe := ...
```

It needs to be `CoeTail`

instead of `Coe`

because otherwise type-class
inference would loop when constructing the transitive coercion `Nat → Nat → Nat → ...`

. Sometimes we also need to declare the `CoeHTCT`

instance if we need to shadow another coercion.

## Equations

- instNatCastNat = { natCast := fun (n : Nat) => n }

Canonical homomorphism from `Nat`

to a type `R`

.

It contains just the function, with no axioms. In practice, the target type will likely have a (semi)ring structure, and this homomorphism should be a ring homomorphism.

The prototypical example is `Int.ofNat`

.

This class and `IntCast`

exist to allow different libraries with their own types that can be notated as natural numbers to have consistent `simp`

normal forms without needing to create coercion simplification sets that are aware of all combinations. Libraries should make it easy to work with `NatCast`

where possible. For instance, in Mathlib there will be such a homomorphism (and thus a `NatCast R`

instance) whenever `R`

is an additive monoid with a `1`

.

## Equations

- Nat.cast = NatCast.natCast