Integer Type, Coercions, and Notation

This file defines the Int type as well as

• coercions, conversions, and compatibility with numeric literals,
• basic arithmetic operations add/sub/mul/div/mod/pow,
• a few Nat-related operations such as negOfNat and subNatNat,
• relations </≤/≥/>, the NonNeg property and min/max,
• decidability of equality, relations and NonNeg.

inductive Int : Type

The type of integers. It is defined as an inductive type based on the natural number type Nat featuring two constructors: "a natural number is an integer", and "the negation of a successor of a natural number is an integer". The former represents integers between 0 (inclusive) and ∞, and the latter integers between -∞ and -1 (inclusive).

This type is special-cased by the compiler. The runtime has a special representation for Int which stores "small" signed numbers directly, and larger numbers use an arbitrary precision "bignum" library (usually GMP). A "small number" is an integer that can be encoded with 63 bits (31 bits on 32-bits architectures).

• ofNat: Nat → Int

  A natural number is an integer (0 to ∞).

• negSucc: Nat → Int

  The negation of the successor of a natural number is an integer (-1 to -∞).

instance instNatCastInt : NatCast Int

Equations

• instNatCastInt = { natCast := fun (n : Nat) => Int.ofNat n }

instance instOfNat {n : Nat} : OfNat Int n

Equations

• instOfNat = { ofNat := Int.ofNat n }

def Int.«term-[_+1]» : Lean.ParserDescr

-[n+1] is suggestive notation for negSucc n, which is the second constructor of Int for making strictly negative numbers by mapping n : Nat to -(n + 1).

Equations

• One or more equations did not get rendered due to their size.

instance Int.instInhabited : Inhabited Int

Equations

• Int.instInhabited = { default := Int.ofNat 0 }

@[simp]

theorem Int.default_eq_zero : default = 0

theorem Int.zero_ne_one : 0 ≠ 1

Coercions

@[simp]

theorem Int.ofNat_eq_coe {n : Nat} : Int.ofNat n = ↑n

@[simp]

theorem Int.ofNat_zero : ↑0 = 0

@[simp]

theorem Int.ofNat_one : ↑1 = 1

theorem Int.ofNat_two : ↑2 = 2

def Int.negOfNat : Nat → Int

Negation of a natural number.

Equations

• Int.negOfNat 0 = 0
• Int.negOfNat m.succ = Int.negSucc m

@[extern lean_int_neg]

def Int.neg (n : Int) : Int

Negation of an integer.

Implemented by efficient native code.

Equations

• (Int.ofNat n_2).neg = Int.negOfNat n_2
• (Int.negSucc n_2).neg = ↑n_2.succ

@[defaultInstance 500]

instance Int.instNegInt : Neg Int

Equations

• Int.instNegInt = { neg := Int.neg }

def Int.subNatNat (m : Nat) (n : Nat) : Int

Subtraction of two natural numbers.

Equations

• Int.subNatNat m n = match n - m with | 0 => Int.ofNat (m - n) | k.succ => Int.negSucc k

@[extern lean_int_add]

def Int.add (m : Int) (n : Int) : Int

Addition of two integers.

#eval (7 : Int) + (6 : Int) -- 13
#eval (6 : Int) + (-6 : Int) -- 0

Implemented by efficient native code.

Equations

• (Int.ofNat m_2).add (Int.ofNat n_2) = Int.ofNat (m_2 + n_2)
• (Int.ofNat m_2).add (Int.negSucc n_2) = Int.subNatNat m_2 n_2.succ
• (Int.negSucc m_2).add (Int.ofNat n_2) = Int.subNatNat n_2 m_2.succ
• (Int.negSucc m_2).add (Int.negSucc n_2) = Int.negSucc (m_2 + n_2).succ

instance Int.instAdd : Add Int

Equations

• Int.instAdd = { add := Int.add }

@[extern lean_int_mul]

def Int.mul (m : Int) (n : Int) : Int

Multiplication of two integers.

#eval (63 : Int) * (6 : Int) -- 378
#eval (6 : Int) * (-6 : Int) -- -36
#eval (7 : Int) * (0 : Int) -- 0

Implemented by efficient native code.

Equations

• (Int.ofNat m_2).mul (Int.ofNat n_2) = Int.ofNat (m_2 * n_2)
• (Int.ofNat m_2).mul (Int.negSucc n_2) = Int.negOfNat (m_2 * n_2.succ)
• (Int.negSucc m_2).mul (Int.ofNat n_2) = Int.negOfNat (m_2.succ * n_2)
• (Int.negSucc m_2).mul (Int.negSucc n_2) = Int.ofNat (m_2.succ * n_2.succ)

instance Int.instMul : Mul Int

Equations

• Int.instMul = { mul := Int.mul }

@[extern lean_int_sub]

def Int.sub (m : Int) (n : Int) : Int

Subtraction of two integers.

#eval (63 : Int) - (6 : Int) -- 57
#eval (7 : Int) - (0 : Int) -- 7
#eval (0 : Int) - (7 : Int) -- -7

Implemented by efficient native code.

Equations

• m.sub n = m + -n

instance Int.instSub : Sub Int

Equations

• Int.instSub = { sub := Int.sub }

inductive Int.NonNeg : Int → Prop

A proof that an Int is non-negative.

• mk: ∀ (n : Nat), (Int.ofNat n).NonNeg

  Sole constructor, proving that ofNat n is positive.

def Int.le (a : Int) (b : Int) : Prop

Definition of a ≤ b, encoded as b - a ≥ 0.

Equations

• a.le b = (b - a).NonNeg

instance Int.instLEInt : LE Int

Equations

• Int.instLEInt = { le := Int.le }

def Int.lt (a : Int) (b : Int) : Prop

Definition of a < b, encoded as a + 1 ≤ b.

Equations

• a.lt b = (a + 1 ≤ b)

instance Int.instLTInt : LT Int

Equations

• Int.instLTInt = { lt := Int.lt }

@[extern lean_int_dec_eq]

def Int.decEq (a : Int) (b : Int) : Decidable (a = b)

Decides equality between two Ints.

#eval (7 : Int) = (3 : Int) + (4 : Int) -- true
#eval (6 : Int) = (3 : Int) * (2 : Int) -- true
#eval ¬ (6 : Int) = (3 : Int) -- true

Implemented by efficient native code.

Equations

• (Int.ofNat m_1).decEq (Int.ofNat n_1) = match decEq m_1 n_1 with | isTrue h => isTrue ⋯ | isFalse h => isFalse ⋯
• (Int.ofNat m_1).decEq (Int.negSucc n_1) = isFalse ⋯
• (Int.negSucc m_1).decEq (Int.ofNat n_1) = isFalse ⋯
• (Int.negSucc m_1).decEq (Int.negSucc n_1) = match decEq m_1 n_1 with | isTrue h => isTrue ⋯ | isFalse h => isFalse ⋯

instance Int.instDecidableEq : DecidableEq Int

Equations

• Int.instDecidableEq = Int.decEq

@[extern lean_int_dec_le]

instance Int.decLe (a : Int) (b : Int) : Decidable (a ≤ b)

Decides whether a ≤ b.

#eval ¬ ( (7 : Int) ≤ (0 : Int) ) -- true
#eval (0 : Int) ≤ (0 : Int) -- true
#eval (7 : Int) ≤ (10 : Int) -- true

Implemented by efficient native code.

Equations

• a.decLe b = Int.decNonneg (b - a)

@[extern lean_int_dec_lt]

instance Int.decLt (a : Int) (b : Int) : Decidable (a < b)

Decides whether a < b.

#eval `¬ ( (7 : Int) < 0 )` -- true
#eval `¬ ( (0 : Int) < 0 )` -- true
#eval `(7 : Int) < 10` -- true

Implemented by efficient native code.

Equations

• a.decLt b = Int.decNonneg (b - (a + 1))

@[extern lean_nat_abs]

def Int.natAbs (m : Int) : Nat

Absolute value (Nat) of an integer.

#eval (7 : Int).natAbs -- 7
#eval (0 : Int).natAbs -- 0
#eval (-11 : Int).natAbs -- 11

Implemented by efficient native code.

Equations

• (Int.ofNat n_1).natAbs = n_1
• (Int.negSucc n_1).natAbs = n_1.succ

sign

def Int.sign : Int → Int

Returns the "sign" of the integer as another integer: 1 for positive numbers, -1 for negative numbers, and 0 for 0.

Equations

• (Int.ofNat n.succ).sign = 1
• (Int.ofNat 0).sign = 0
• (Int.negSucc a).sign = -1

Conversion

def Int.toNat : Int → Nat

Turns an integer into a natural number, negative numbers become 0.

#eval (7 : Int).toNat -- 7
#eval (0 : Int).toNat -- 0
#eval (-7 : Int).toNat -- 0

Equations

• (Int.ofNat n).toNat = n
• (Int.negSucc a).toNat = 0

def Int.toNat' : Int → Option Nat

• If n : Nat, then int.toNat' n = some n
• If n : Int is negative, then int.toNat' n = none.

Equations

• (Int.ofNat n).toNat' = some n
• (Int.negSucc a).toNat' = none

divisibility

instance Int.instDvd : Dvd Int

Divisibility of integers. a ∣ b (typed as \|) says that there is some c such that b = a * c.

Equations

• Int.instDvd = { dvd := fun (a b : Int) => ∃ (c : Int), b = a * c }

Powers

def Int.pow (m : Int) : Nat → Int

Power of an integer to some natural number.

#eval (2 : Int) ^ 4 -- 16
#eval (10 : Int) ^ 0 -- 1
#eval (0 : Int) ^ 10 -- 0
#eval (-7 : Int) ^ 3 -- -343

Equations

• m.pow 0 = 1
• m.pow m_1.succ = m.pow m_1 * m

instance Int.instNatPow : NatPow Int

Equations

• Int.instNatPow = { pow := Int.pow }

instance Int.instLawfulBEq : LawfulBEq Int

Equations

• Int.instLawfulBEq = ⋯

instance Int.instMin : Min Int

Equations

• Int.instMin = minOfLe

instance Int.instMax : Max Int

Equations

• Int.instMax = maxOfLe

class IntCast (R : Type u) : Type u

The canonical homomorphism Int → R. In most use cases R will have a ring structure and this will be a ring homomorphism.

• intCast : Int → R

  The canonical map Int → R.

instance instIntCastInt : IntCast Int

Equations

• instIntCastInt = { intCast := fun (n : Int) => n }

@[reducible, match_pattern]

def Int.cast {R : Type u} [IntCast R] : Int → R

Apply the canonical homomorphism from Int to a type R from an IntCast R instance.

In Mathlib there will be such a homomorphism whenever R is an additive group with a 1.

Equations

• Int.cast = IntCast.intCast

instance instCoeTailIntOfIntCast {R : Type u_1} [IntCast R] : CoeTail Int R

Equations

• instCoeTailIntOfIntCast = { coe := Int.cast }

instance instCoeHTCTIntOfIntCast {R : Type u_1} [IntCast R] : CoeHTCT Int R

Equations

• instCoeHTCTIntOfIntCast = { coe := Int.cast }