Init.Data.Cast

Module docstring

{"# 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: lean 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. "}

NatCast structure

(R : Type u)

Full source

/--
The canonical homomorphism `Nat → R`. In most use cases, the target type will have a (semi)ring
structure, and this homomorphism should be a (semi)ring homomorphism.

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

The prototypical example is `Int.ofNat`.
-/
class NatCast (R : Type u) where
  /-- The canonical map `Nat → R`. -/
  protected natCast : Nat → R

Natural number coercion structure

Informal description

The structure `NatCast R` represents a type `R` equipped with a canonical homomorphism from the natural numbers to `R`. This homomorphism is typically a (semi)ring homomorphism when `R` has a (semi)ring structure. The purpose of this structure is to provide a uniform way to handle coercions from `Nat` to various types in a way that supports consistent simplification in proof assistants.

instNatCastNat instance

: NatCast Nat

Full source

instance : NatCast Nat where natCast n := n

Natural Numbers as a NatCast Structure

Informal description

The natural numbers $\mathbb{N}$ have a canonical natural number coercion structure, where the homomorphism from $\mathbb{N}$ to itself is the identity map.

Nat.cast definition

{R : Type u} [NatCast R] : Nat → R

Full source

@[coe, reducible, match_pattern, inherit_doc NatCast]
protected def Nat.cast {R : Type u} [NatCast R] : Nat → R :=
  NatCast.natCast

Canonical homomorphism from natural numbers to a type with natural number coercion

Informal description

The function `Nat.cast` maps a natural number $n$ to its canonical image in a type $R$ equipped with a `NatCast` structure. This function represents the canonical homomorphism from the natural numbers to $R$.

instCoeTailNatOfNatCast instance

[NatCast R] : CoeTail Nat R

Full source

instance [NatCast R] : CoeTail Nat R where coe := Nat.cast

Tail Coercion from Natural Numbers to a Type with Natural Number Coercion

Informal description

For any type $R$ with a natural number coercion structure (i.e., equipped with a canonical homomorphism from $\mathbb{N}$ to $R$), there exists a tail coercion from $\mathbb{N}$ to $R$. This means that natural numbers can be automatically cast to elements of $R$ when they appear at the end of a coercion chain.

instCoeHTCTNatOfNatCast instance

[NatCast R] : CoeHTCT Nat R

Full source

instance [NatCast R] : CoeHTCT Nat R where coe := Nat.cast

Head Coercion from Natural Numbers to a Type with Natural Number Coercion

Informal description

For any type $R$ with a natural number coercion structure, there exists a canonical coercion chain from $\mathbb{N}$ to $R$ that can be used in the head position of a coercion chain.