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

• 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 -∞).

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

instance instCoeNatInt : Coe Nat Int

instance instOfNatInt {n : Nat} : OfNat Int n

instance Int.instInhabitedInt : Inhabited Int

def Int.negOfNat : Nat → Int

Negation of a natural number.

@[extern lean_int_neg]

def Int.neg (n : Int) : Int

Negation of an integer.

Implemented by efficient native code.

@[defaultInstance 500]

instance Int.instNegInt : Neg Int

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

Subtraction of two natural numbers.

@[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.

instance Int.instAddInt : Add Int

@[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.

instance Int.instMulInt : Mul Int

@[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.

instance Int.instSubInt : Sub Int

inductive Int.NonNeg : Int → Prop

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

  Sole constructor, proving that ofNat n is positive.

A proof that an Int is non-negative.

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

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

instance Int.instLEInt : LE Int

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

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

instance Int.instLTInt : LT Int

@[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.

instance Int.instDecidableEqInt : DecidableEq Int

@[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.

@[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.

@[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.

@[extern lean_int_div]

def Int.div : Int → Int → Int

Integer division. This function uses the "T-rounding" (Truncation-rounding) convention, meaning that it rounds toward zero. Also note that division by zero is defined to equal zero.

The relation between integer division and modulo is found in the Int.mod_add_div theorem in std which states that a % b + b * (a / b) = a, unconditionally.

Examples:

#eval (7 : Int) / (0 : Int) -- 0
#eval (0 : Int) / (7 : Int) -- 0

#eval (12 : Int) / (6 : Int) -- 2
#eval (12 : Int) / (-6 : Int) -- -2
#eval (-12 : Int) / (6 : Int) -- -2
#eval (-12 : Int) / (-6 : Int) -- 2

#eval (12 : Int) / (7 : Int) -- 1
#eval (12 : Int) / (-7 : Int) -- -1
#eval (-12 : Int) / (7 : Int) -- -1
#eval (-12 : Int) / (-7 : Int) -- 1

Implemented by efficient native code.

instance Int.instDivInt : Div Int

@[extern lean_int_mod]

def Int.mod : Int → Int → Int

Integer modulo. This function uses the "T-rounding" (Truncation-rounding) convention to pair with Int.div, meaning that a % b + b * (a / b) = a unconditionally (see Int.mod_add_div). In particular, a % 0 = a.

Examples:

#eval (7 : Int) % (0 : Int) -- 7
#eval (0 : Int) % (7 : Int) -- 0

#eval (12 : Int) % (6 : Int) -- 0
#eval (12 : Int) % (-6 : Int) -- 0
#eval (-12 : Int) % (6 : Int) -- 0
#eval (-12 : Int) % (-6 : Int) -- 0

#eval (12 : Int) % (7 : Int) -- 5
#eval (12 : Int) % (-7 : Int) -- 5
#eval (-12 : Int) % (7 : Int) -- 2
#eval (-12 : Int) % (-7 : Int) -- 2

Implemented by efficient native code.

instance Int.instModInt : Mod Int

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

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

• Int.pow m 0 = 1
• Int.pow m (Nat.succ m_1) = Int.pow m m_1 * m

instance Int.instHPowIntNat : HPow Int Nat Int

instance Int.instLawfulBEqIntInstBEqInstDecidableEqInt : LawfulBEq Int

instance Int.instMinInt : Min Int

instance Int.instMaxInt : Max Int