Mathlib.Data.Nat.Cast.Defs

Nat.unaryCast definition

[One R] [Zero R] [Add R] : ℕ → R

Full source

/-- The numeral `((0+1)+⋯)+1`. -/
protected def Nat.unaryCast [One R] [Zero R] [Add R] : ℕ → R
  | 0 => 0
  | n + 1 => Nat.unaryCast n + 1

Unary representation of natural numbers in an additive monoid with one

Informal description

The function `Nat.unaryCast` maps a natural number $n$ to its representation in a type `R` with operations `0`, `1`, and `+`, defined recursively as: - $0$ is mapped to $0 \in R$ - $n + 1$ is mapped to $\text{Nat.unaryCast}(n) + 1 \in R$

Nat.AtLeastTwo structure

(n : ℕ)

Full source

/-- A type class for natural numbers which are greater than or equal to `2`. -/
class Nat.AtLeastTwo (n : ℕ) : Prop where
  prop : n ≥ 2

Natural numbers at least two

Informal description

A structure `Nat.AtLeastTwo` is defined for natural numbers $ n $ that satisfy the property $ n \geq 2 $. This is used to represent natural numbers that are strictly greater than 1.

instNatAtLeastTwo instance

{n : ℕ} : Nat.AtLeastTwo (n + 2)

Full source

instance instNatAtLeastTwo {n : ℕ} : Nat.AtLeastTwo (n + 2) where
  prop := Nat.succ_le_succ <| Nat.succ_le_succ <| Nat.zero_le _

Natural Number Shift Preserves AtLeastTwo Property

Informal description

For any natural number $n$, the number $n + 2$ satisfies the property of being at least two.

Nat.AtLeastTwo.one_lt theorem

: 1 < n

Full source

lemma one_lt : 1 < n := prop

One is less than any natural number at least two

Informal description

For any natural number $n \geq 2$, we have $1 < n$.

Nat.AtLeastTwo.ne_one theorem

: n ≠ 1

Full source

lemma ne_one : n ≠ 1 := Nat.ne_of_gt one_lt

Natural numbers at least two are not one

Informal description

For any natural number $n \geq 2$, we have $n \neq 1$.

instOfNatAtLeastTwo instance

{n : ℕ} [NatCast R] [Nat.AtLeastTwo n] : OfNat R n

Full source

/-- Recognize numeric literals which are at least `2` as terms of `R` via `Nat.cast`. This
instance is what makes things like `37 : R` type check.  Note that `0` and `1` are not needed
because they are recognized as terms of `R` (at least when `R` is an `AddMonoidWithOne`) through
`Zero` and `One`, respectively. -/
@[nolint unusedArguments]
instance (priority := 100) instOfNatAtLeastTwo {n : ℕ} [NatCast R] [Nat.AtLeastTwo n] :
    OfNat R n where
  ofNat := n.cast

Interpretation of Numerals ≥ 2 via Natural Number Cast

Informal description

For any natural number $n \geq 2$ and any type $R$ with a canonical homomorphism from $\mathbb{N}$, the numeral $n$ can be interpreted as an element of $R$ via the `OfNat` instance.

Nat.cast_ofNat theorem

{n : ℕ} [NatCast R] [Nat.AtLeastTwo n] : (Nat.cast ofNat(n) : R) = ofNat(n)

Full source

@[simp, norm_cast] theorem Nat.cast_ofNat {n : ℕ} [NatCast R] [Nat.AtLeastTwo n] :
  (Nat.cast ofNat(n) : R) = ofNat(n) := rfl

Canonical Homomorphism Preserves Numerals $\geq 2$

Informal description

For any natural number $n \geq 2$ and any type $R$ with a canonical homomorphism from $\mathbb{N}$, the canonical homomorphism $\text{Nat.cast}$ applied to the numeral $n$ equals the interpretation of $n$ as an element of $R$ via the `OfNat` structure, i.e., $\text{Nat.cast}(n) = n$ (where the right-hand side is interpreted in $R$).

Nat.cast_eq_ofNat theorem

{n : ℕ} [NatCast R] [Nat.AtLeastTwo n] : (Nat.cast n : R) = OfNat.ofNat n

Full source

@[deprecated Nat.cast_ofNat (since := "2024-12-22")]
theorem Nat.cast_eq_ofNat {n : ℕ} [NatCast R] [Nat.AtLeastTwo n] :
    (Nat.cast n : R) = OfNat.ofNat n :=
  rfl

Canonical Homomorphism Equals Numeric Interpretation for $n \geq 2$

Informal description

For any natural number $n \geq 2$ and any type $R$ with a canonical homomorphism from $\mathbb{N}$, the canonical homomorphism $\text{Nat.cast}$ applied to $n$ equals the interpretation of $n$ as an element of $R$ via the `OfNat` structure, i.e., $\text{Nat.cast}(n) = n$ (where the right-hand side is interpreted in $R$).

AddMonoidWithOne structure

(R : Type*) extends NatCast R, AddMonoid R, One R

Full source

/-- An `AddMonoidWithOne` is an `AddMonoid` with a `1`.
It also contains data for the unique homomorphism `ℕ → R`. -/
class AddMonoidWithOne (R : Type*) extends NatCast R, AddMonoid R, One R where
  natCast := Nat.unaryCast
  /-- The canonical map `ℕ → R` sends `0 : ℕ` to `0 : R`. -/
  natCast_zero : natCast 0 = 0 := by intros; rfl
  /-- The canonical map `ℕ → R` is a homomorphism. -/
  natCast_succ : ∀ n, natCast (n + 1) = natCast n + 1 := by intros; rfl

Additive Monoid with One

Informal description

An `AddMonoidWithOne` is an additive monoid $R$ equipped with a distinguished element $1$ and a canonical homomorphism from the natural numbers to $R$. This structure ensures that the homomorphism $\mathbb{N} \to R$ is unique and preserves the additive monoid structure along with the multiplicative identity.

AddCommMonoidWithOne structure

(R : Type*) extends AddMonoidWithOne R, AddCommMonoid R

Full source

/-- An `AddCommMonoidWithOne` is an `AddMonoidWithOne` satisfying `a + b = b + a`. -/
class AddCommMonoidWithOne (R : Type*) extends AddMonoidWithOne R, AddCommMonoid R

Additive commutative monoid with one

Informal description

An additive commutative monoid with one is an additive monoid with one that additionally satisfies the commutative property $ a + b = b + a $ for all elements $ a, b $. This structure extends `AddMonoidWithOne` and `AddCommMonoid`, combining the properties of having a canonical homomorphism from the natural numbers (via `Nat.cast`), an additive identity, and a multiplicative identity, along with commutativity of addition.

Nat.cast_zero theorem

: ((0 : ℕ) : R) = 0

Full source

@[simp, norm_cast]
theorem cast_zero : ((0 : ℕ) : R) = 0 :=
  AddMonoidWithOne.natCast_zero

Canonical Homomorphism Preserves Zero: $\text{cast}(0) = 0$

Informal description

For any additive monoid with one $R$, the canonical homomorphism from the natural numbers to $R$ maps $0$ to the additive identity $0$ in $R$, i.e., $\text{cast}(0) = 0$.

Nat.cast_succ theorem

(n : ℕ) : ((succ n : ℕ) : R) = n + 1

Full source

@[norm_cast 500]
theorem cast_succ (n : ℕ) : ((succ n : ℕ) : R) = n + 1 :=
  AddMonoidWithOne.natCast_succ _

Canonical Homomorphism Preserves Successor: $\text{cast}(n+1) = \text{cast}(n) + 1$

Informal description

For any natural number $n$ and any additive monoid with one $R$, the canonical homomorphism $\mathbb{N} \to R$ satisfies $\text{cast}(\text{succ}(n)) = \text{cast}(n) + 1$, where $\text{succ}(n)$ denotes the successor of $n$.

Nat.cast_add_one theorem

(n : ℕ) : ((n + 1 : ℕ) : R) = n + 1

Full source

theorem cast_add_one (n : ℕ) : ((n + 1 : ℕ) : R) = n + 1 :=
  cast_succ _

Canonical Homomorphism Preserves Addition of One: $\text{cast}(n+1) = \text{cast}(n) + 1$

Informal description

For any natural number $n$ and any additive monoid with one $R$, the canonical homomorphism $\mathbb{N} \to R$ satisfies $\text{cast}(n + 1) = \text{cast}(n) + 1$, where $\text{cast}$ denotes the canonical embedding of natural numbers into $R$.

Nat.cast_ite theorem

(P : Prop) [Decidable P] (m n : ℕ) : ((ite P m n : ℕ) : R) = ite P (m : R) (n : R)

Full source

@[simp, norm_cast]
theorem cast_ite (P : Prop) [Decidable P] (m n : ℕ) :
    ((ite P m n : ℕ) : R) = ite P (m : R) (n : R) := by
  split_ifs <;> rfl

Canonical Homomorphism Preserves If-Then-Else for Natural Numbers

Informal description

Let $R$ be an additive monoid with one. For any proposition $P$ with a decision procedure, and for any natural numbers $m$ and $n$, the canonical homomorphism $\mathbb{N} \to R$ satisfies $\text{cast}(\text{ite}(P, m, n)) = \text{ite}(P, \text{cast}(m), \text{cast}(n))$, where $\text{ite}$ denotes the if-then-else operation.

Nat.cast_one theorem

[AddMonoidWithOne R] : ((1 : ℕ) : R) = 1

Full source

@[simp, norm_cast]
theorem cast_one [AddMonoidWithOne R] : ((1 : ℕ) : R) = 1 := by
  rw [cast_succ, Nat.cast_zero, zero_add]

Canonical Homomorphism Preserves One: $\text{cast}(1) = 1$

Informal description

For any additive monoid with one $R$, the canonical homomorphism from the natural numbers to $R$ maps the natural number $1$ to the multiplicative identity $1$ in $R$, i.e., $\text{cast}(1) = 1$.

Nat.cast_add theorem

[AddMonoidWithOne R] (m n : ℕ) : ((m + n : ℕ) : R) = m + n

Full source

@[simp, norm_cast]
theorem cast_add [AddMonoidWithOne R] (m n : ℕ) : ((m + n : ℕ) : R) = m + n := by
  induction n with
  | zero => simp
  | succ n ih => rw [add_succ, cast_succ, ih, cast_succ, add_assoc]

Canonical Homomorphism Preserves Addition: $\text{cast}(m + n) = \text{cast}(m) + \text{cast}(n)$

Informal description

For any additive monoid with one $R$ and any natural numbers $m$ and $n$, the canonical homomorphism $\mathbb{N} \to R$ satisfies $\text{cast}(m + n) = \text{cast}(m) + \text{cast}(n)$.

Nat.binCast definition

[Zero R] [One R] [Add R] : ℕ → R

Full source

/-- Computationally friendlier cast than `Nat.unaryCast`, using binary representation. -/
protected def binCast [Zero R] [One R] [Add R] : ℕ → R
  | 0 => 0
  | n + 1 => if (n + 1) % 2 = 0
    then (Nat.binCast ((n + 1) / 2)) + (Nat.binCast ((n + 1) / 2))
    else (Nat.binCast ((n + 1) / 2)) + (Nat.binCast ((n + 1) / 2)) + 1

Binary representation natural number cast

Informal description

The function `Nat.binCast` maps a natural number $n$ to an element of type $R$ (which has zero, one, and addition operations) using a binary representation. It is defined recursively as follows: - $0$ is mapped to $0 \in R$ - For $n+1$, if $(n+1)$ is even, it maps to $2 \cdot \text{binCast}((n+1)/2)$ - For $n+1$, if $(n+1)$ is odd, it maps to $2 \cdot \text{binCast}((n+1)/2) + 1$ This provides a computationally efficient alternative to the unary cast `Nat.unaryCast`.

Nat.binCast_eq theorem

[AddMonoidWithOne R] (n : ℕ) : (Nat.binCast n : R) = ((n : ℕ) : R)

Full source

@[simp]
theorem binCast_eq [AddMonoidWithOne R] (n : ℕ) :
    (Nat.binCast n : R) = ((n : ℕ) : R) := by
  induction n using Nat.strongRecOn with | ind k hk => ?_
  cases k with
  | zero => rw [Nat.binCast, Nat.cast_zero]
  | succ k =>
      rw [Nat.binCast]
      by_cases h : (k + 1) % 2 = 0
      · conv => rhs; rw [← Nat.mod_add_div (k+1) 2]
        rw [if_pos h, hk _ <| Nat.div_lt_self (Nat.succ_pos k) (Nat.le_refl 2), ← Nat.cast_add]
        rw [h, Nat.zero_add, Nat.succ_mul, Nat.one_mul]
      · conv => rhs; rw [← Nat.mod_add_div (k+1) 2]
        rw [if_neg h, hk _ <| Nat.div_lt_self (Nat.succ_pos k) (Nat.le_refl 2), ← Nat.cast_add]
        have h1 := Or.resolve_left (Nat.mod_two_eq_zero_or_one (succ k)) h
        rw [h1, Nat.add_comm 1, Nat.succ_mul, Nat.one_mul]
        simp only [Nat.cast_add, Nat.cast_one]

Equivalence of Binary Cast and Canonical Homomorphism: $\text{binCast}(n) = \text{cast}(n)$

Informal description

For any additive monoid with one $R$ and any natural number $n$, the binary cast function `Nat.binCast` applied to $n$ yields the same element in $R$ as the canonical homomorphism from $\mathbb{N}$ to $R$, i.e., $\text{binCast}(n) = \text{cast}(n)$.

Nat.cast_two theorem

[NatCast R] : ((2 : ℕ) : R) = (2 : R)

Full source

theorem cast_two [NatCast R] : ((2 : ℕ) : R) = (2 : R) := rfl

Canonical Image of Two in Natural Number Cast

Informal description

For any type $R$ with a canonical homomorphism from the natural numbers, the canonical image of the natural number $2$ in $R$ is equal to the element $2$ in $R$.

Nat.cast_three theorem

[NatCast R] : ((3 : ℕ) : R) = (3 : R)

Full source

theorem cast_three [NatCast R] : ((3 : ℕ) : R) = (3 : R) := rfl

Canonical Image of Three in Natural Number Cast

Informal description

For any type $R$ with a canonical homomorphism from the natural numbers, the canonical image of the natural number $3$ in $R$ is equal to the element $3$ in $R$.

Nat.cast_four theorem

[NatCast R] : ((4 : ℕ) : R) = (4 : R)

Full source

theorem cast_four [NatCast R] : ((4 : ℕ) : R) = (4 : R) := rfl

Canonical Image of Four in Natural Number Cast

Informal description

For any type $R$ with a canonical homomorphism from the natural numbers, the canonical image of the natural number $4$ in $R$ is equal to the element $4$ in $R$.

AddMonoidWithOne.unary abbrev

[AddMonoid R] [One R] : AddMonoidWithOne R

Full source

/-- `AddMonoidWithOne` implementation using unary recursion. -/
protected abbrev AddMonoidWithOne.unary [AddMonoid R] [One R] : AddMonoidWithOne R :=
  { ‹One R›, ‹AddMonoid R› with }

Unary Recursion Construction of Additive Monoid with One

Informal description

Given an additive monoid $R$ with a distinguished element $1$, the structure `AddMonoidWithOne.unary` provides a canonical way to view $R$ as an additive monoid with one, where the natural number embedding is defined via unary recursion: - $0$ is mapped to $0 \in R$ - $n + 1$ is mapped to $\text{unaryCast}(n) + 1 \in R$

AddMonoidWithOne.binary abbrev

[AddMonoid R] [One R] : AddMonoidWithOne R

Full source

/-- `AddMonoidWithOne` implementation using binary recursion. -/
protected abbrev AddMonoidWithOne.binary [AddMonoid R] [One R] : AddMonoidWithOne R :=
  { ‹One R›, ‹AddMonoid R› with
    natCast := Nat.binCast,
    natCast_zero := by simp only [Nat.binCast, Nat.cast],
    natCast_succ := fun n => by
      letI : AddMonoidWithOne R := AddMonoidWithOne.unary
      rw [Nat.binCast_eq, Nat.binCast_eq, Nat.cast_succ] }

Binary Recursion Construction of Additive Monoid with One

Informal description

Given an additive monoid $R$ with a distinguished element $1$, the structure `AddMonoidWithOne.binary` provides a canonical way to view $R$ as an additive monoid with one, where the natural number embedding is defined via binary recursion: - $0$ is mapped to $0 \in R$ - For $n+1$, if $(n+1)$ is even, it maps to $2 \cdot \text{binCast}((n+1)/2)$ - For $n+1$, if $(n+1)$ is odd, it maps to $2 \cdot \text{binCast}((n+1)/2) + 1$

one_add_one_eq_two theorem

[AddMonoidWithOne R] : 1 + 1 = (2 : R)

Full source

theorem one_add_one_eq_two [AddMonoidWithOne R] : 1 + 1 = (2 : R) := by
  rw [← Nat.cast_one, ← Nat.cast_add]
  apply congrArg
  decide

Identity Sum Equals Two: $1 + 1 = 2$ in Additive Monoids with One

Informal description

For any additive monoid with one $R$, the sum of the multiplicative identity $1$ with itself equals the canonical image of the natural number $2$ in $R$, i.e., $1 + 1 = 2$.

two_add_one_eq_three theorem

[AddMonoidWithOne R] : 2 + 1 = (3 : R)

Full source

theorem two_add_one_eq_three [AddMonoidWithOne R] : 2 + 1 = (3 : R) := by
  rw [← one_add_one_eq_two, ← Nat.cast_one, ← Nat.cast_add, ← Nat.cast_add]
  apply congrArg
  decide

Sum Identity: $2 + 1 = 3$ in Additive Monoids with One

Informal description

For any additive monoid with one $R$, the sum of the elements $2$ and $1$ equals the element $3$, i.e., $2 + 1 = 3$.

three_add_one_eq_four theorem

[AddMonoidWithOne R] : 3 + 1 = (4 : R)

Full source

theorem three_add_one_eq_four [AddMonoidWithOne R] : 3 + 1 = (4 : R) := by
  rw [← two_add_one_eq_three, ← one_add_one_eq_two, ← Nat.cast_one,
    ← Nat.cast_add, ← Nat.cast_add, ← Nat.cast_add]
  apply congrArg
  decide

Sum Identity: $3 + 1 = 4$ in Additive Monoids with One

Informal description

For any additive monoid with one $R$, the sum of the elements $3$ and $1$ equals the element $4$, i.e., $3 + 1 = 4$.

two_add_two_eq_four theorem

[AddMonoidWithOne R] : 2 + 2 = (4 : R)

Full source

theorem two_add_two_eq_four [AddMonoidWithOne R] : 2 + 2 = (4 : R) := by
  simp [← one_add_one_eq_two, ← Nat.cast_one, ← three_add_one_eq_four,
    ← two_add_one_eq_three, add_assoc]

Sum of Twos Equals Four in Additive Monoid with One

Informal description

In any additive monoid with one $R$, the sum of the elements $2$ and $2$ equals the element $4$, i.e., $2 + 2 = 4$.

nsmul_one theorem

{A} [AddMonoidWithOne A] : ∀ n : ℕ, n • (1 : A) = n

Full source

@[simp] lemma nsmul_one {A} [AddMonoidWithOne A] : ∀ n : ℕ, n • (1 : A) = n
  | 0 => by simp [zero_nsmul]
  | n + 1 => by simp [succ_nsmul, nsmul_one n]

Additive Iteration of One: $n \cdot 1 = n$

Informal description

For any additive monoid with one $A$ and any natural number $n$, the $n$-th additive iteration of the multiplicative identity $1$ in $A$ equals $n$, i.e., $n \cdot 1 = n$.

Main declarations