`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.

source

class NatCast (R : Type u) :

Type u

Type class for the canonical homomorphism Nat → R.

natCast : Nat → R
The canonical map Nat → R.

Instances

source

instance instNatCastNat :

NatCast Nat

Equations

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

source

@[match_pattern, reducible]

def Nat.cast {R : Type u} [NatCast R] :

Nat → R

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