int

Int

data Int

The integers: pos n stands for n and negsucc n stands for -(n + 1).

Int.succ

def succ (n : Int) : Int

Integer successor: n + 1.

Int.pred

def pred (n : Int) : Int

Integer predecessor: n - 1.

Int.neg

def neg (n : Int) : Int

Integer negation: -n.

Int.abs

def abs (n : Int) : Nat

Absolute value of an integer, as a natural number.

Int.addNat

def addNat (m : Nat) (n : Int) : Int

Add a natural number to an integer by applying Int.succ m times.

Int.subNat

def subNat (m : Nat) (n : Int) : Int

Subtract a natural number from an integer by applying Int.pred m times.

Int.add

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

Integer addition, by recursion on the first argument.

Int.sub

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

Integer subtraction: m + (-n).

Int.mulNat

def mulNat (m : Nat) (n : Int) : Int

Multiply an integer by a natural number, as repeated addition.

Int.mul

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

Integer multiplication, by recursion on the first argument.

Int.beq

def beq (m : Int) (n : Int) : Bool

Boolean equality test on integers.

Int.blt

def blt (m : Int) (n : Int) : Bool

Boolean strict less-than test on integers.

Int.ble

def ble (m : Int) (n : Int) : Bool

Boolean less-than-or-equal test on integers.

Int.isPos

def isPos (n : Int) : Bool

Boolean test for whether an integer is strictly positive.

Int.isNeg

def isNeg (n : Int) : Bool

Boolean test for whether an integer is strictly negative.

Int.isZero

def isZero (n : Int) : Bool

Boolean test for whether an integer is zero.

Int.toNat

def toNat (n : Int) : Nat

Convert an integer to a natural number, sending negative integers to zero.

Int.ofNat

def ofNat (n : Nat) : Int

Embed a natural number into the integers.

Int.double

def double (n : Int) : Int

Double an integer: n + n.

Int.min

def min (m : Int) (n : Int) : Int

The smaller of two integers.

Int.max

def max (m : Int) (n : Int) : Int

The larger of two integers.

Int.sign

def sign (n : Int) : Int

Sign of an integer: 1, 0 or -1.

Int.pow

def pow (base : Int) (exp : Nat) : Int

Integer power with a natural-number exponent: base ^ exp.

Int.zero

def zero : Int

The integer 0.

Int.one

def one : Int

The integer 1.

Int.two

def two : Int

The integer 2.

Int.negOne

def negOne : Int

The integer -1.

Int.negTwo

def negTwo : Int

The integer -2.

Int.iterate

def iterate (f : Int -> Int) (n : Nat) (x : Int) : Int

Apply an integer function n times to x.

Int.lit

def lit (n : Nat) : Int

The integer literal for a natural number n.

Int.triple

def triple (n : Int) : Int

Triple an integer: n + (n + n).

Int.square

def square (n : Int) : Int

Square an integer: n * n.

Int.dist

def dist (m : Int) (n : Int) : Int

Distance between two integers: |m - n|, as an integer.

Int.addNatZero

def addNatZero (n : Int) : Int.addNat Nat.zero n = n

Adding zero by Int.addNat leaves an integer unchanged.

Int.subNatZero

def subNatZero (n : Int) : Int.subNat Nat.zero n = n

Subtracting zero by Int.subNat leaves an integer unchanged.

Int.addNatSucc

def addNatSucc (k : Nat) (n : Int) : Int.addNat (Nat.succ k) n = Int.succ (Int.addNat k n)

Unfolding of Int.addNat at a successor: Int.addNat (k + 1) n = Int.succ (Int.addNat k n).

Int.addPosSucc

def addPosSucc (k : Nat) (n : Int) : Int.add (pos (Nat.succ k)) n = Int.succ (Int.add (pos k) n)

Unfolding of integer addition at a positive successor: (k + 1) + n = Int.succ (k + n).

Int.addNatPosZero

def addNatPosZero (k : Nat) : Int.addNat k (pos Nat.zero) = pos k

Adding k to zero gives the integer k: Int.addNat k 0 = pos k.

Int.subNatNegZero

def subNatNegZero (k : Nat) : Int.subNat (Nat.succ k) (pos Nat.zero) = negsucc k

Subtracting k + 1 from zero gives -(k + 1): Int.subNat (k + 1) 0 = negsucc k.

Int.succAddNat

def succAddNat (k : Nat) (n : Int) : Int.succ (Int.addNat k n) = Int.addNat k (Int.succ n)

Successor commutes with adding a natural number: Int.succ (Int.addNat k n) = Int.addNat k (Int.succ n).

Int.addNatSuccL

def addNatSuccL (k : Nat) (n : Int) : Int.addNat (Nat.succ k) n = Int.addNat k (Int.succ n)

Adding k + 1 is adding k to the successor: Int.addNat (k + 1) n = Int.addNat k (Int.succ n).

Int.predSubNat

def predSubNat (k : Nat) (n : Int) : Int.pred (Int.subNat k n) = Int.subNat k (Int.pred n)

Predecessor commutes with subtracting a natural number: Int.pred (Int.subNat k n) = Int.subNat k (Int.pred n).

Int.negInvolPos

def negInvolPos (k : Nat) : Int.neg (Int.neg (pos k)) = pos k

Double negation of a non-negative integer is itself: -(-(pos k)) = pos k.

Int.negInvolNeg

def negInvolNeg (k : Nat) : Int.neg (Int.neg (negsucc k)) = negsucc k

Double negation of a negative integer is itself: -(-(negsucc k)) = negsucc k.

Int.negInvol

def negInvol (n : Int) : Int.neg (Int.neg n) = n

Integer negation is an involution: -(-n) = n.

Int.beqRefl

def beqRefl (n : Int) : Int.beq n n = true

Boolean integer equality is reflexive: Int.beq n n = true.

Int.sucPred

def sucPred (n : Int) : Int.succ (Int.pred n) = n

Successor undoes predecessor: Int.succ (Int.pred n) = n.

Int.predSucc

def predSucc (n : Int) : Int.pred (Int.succ n) = n

Predecessor undoes successor: Int.pred (Int.succ n) = n.

Int.mulZeroL

def mulZeroL (n : Int) : Int.mul (pos Nat.zero) n = pos Nat.zero

Zero absorbs integer multiplication on the left: 0 * n = 0.

Int.mulNatZero

def mulNatZero (n : Int) : Int.mulNat Nat.zero n = pos Nat.zero

Multiplying an integer by the natural number zero gives zero.

Int.mulNatOne

def mulNatOne (n : Int) : Int.mulNat (Nat.succ Nat.zero) n = Int.add n (pos Nat.zero)

Unfolding of multiplication by the natural number one: Int.mulNat 1 n = n + 0.

Int.succIsAddOne

def succIsAddOne (n : Int) : Int.succ n = Int.add (pos (Nat.succ Nat.zero)) n

The integer successor is adding one: Int.succ n = 1 + n.

Int.predIsAddNegOne

def predIsAddNegOne (n : Int) : Int.pred n = Int.add (negsucc Nat.zero) n

The integer predecessor is adding minus one: Int.pred n = -1 + n.

Int.absPos

def absPos (k : Nat) : Int.abs (pos k) = k

The absolute value of pos k is k.

Int.absNegsucc

def absNegsucc (k : Nat) : Int.abs (negsucc k) = Nat.succ k

The absolute value of negsucc k is k + 1.

Int.isZeroPos

def isZeroPos (k : Nat) : Int.isZero (pos (Nat.succ k)) = false

A positive integer is not zero: Int.isZero (pos (k + 1)) = false.

Int.isZeroNeg

def isZeroNeg (k : Nat) : Int.isZero (negsucc k) = false

A negative integer is not zero: Int.isZero (negsucc k) = false.

Int.toNatPos

def toNatPos (k : Nat) : Int.toNat (pos k) = k

Converting pos k to a natural number gives k.

Int.toNatNeg

def toNatNeg (k : Nat) : Int.toNat (negsucc k) = Nat.zero

Converting a negative integer to a natural number gives zero.

Int.ofNatSucc

def ofNatSucc (k : Nat) : Int.ofNat (Nat.succ k) = pos (Nat.succ k)

Embedding a successor natural gives the positive integer pos (k + 1).

Int.mulNatZeroR

def mulNatZeroR (k : Nat) : Int.mulNat k (pos Nat.zero) = pos Nat.zero

Multiplying the integer zero by a natural number gives zero: k * 0 = 0.

Int.mulNatOneR

def mulNatOneR (k : Nat) : Int.mulNat k (pos (Nat.succ Nat.zero)) = pos k

Multiplying the integer one by a natural number k gives pos k.

Int.negSuc

def negSuc (n : Int) : Int.neg (Int.succ n) = Int.pred (Int.neg n)

Negation turns successor into predecessor: -(Int.succ n) = Int.pred (-n).

Int.negPred

def negPred (n : Int) : Int.neg (Int.pred n) = Int.succ (Int.neg n)

Negation turns predecessor into successor: -(Int.pred n) = Int.succ (-n).

Int.addNatSuccR

def addNatSuccR (k : Nat) (n : Int) : Int.addNat k (Int.succ n) = Int.succ (Int.addNat k n)

Adding a natural number commutes with successor: Int.addNat k (Int.succ n) = Int.succ (Int.addNat k n).

Int.subNatPred

def subNatPred (k : Nat) (n : Int) : Int.subNat k (Int.pred n) = Int.pred (Int.subNat k n)

Subtracting a natural number commutes with predecessor: Int.subNat k (Int.pred n) = Int.pred (Int.subNat k n).

Int.succSubNat

def succSubNat (k : Nat) (n : Int) : Int.succ (Int.subNat k n) = Int.subNat k (Int.succ n)

Successor commutes with subtracting a natural number: Int.succ (Int.subNat k n) = Int.subNat k (Int.succ n).

Int.predAddNat

def predAddNat (k : Nat) (n : Int) : Int.pred (Int.addNat k n) = Int.addNat k (Int.pred n)

Predecessor commutes with adding a natural number: Int.pred (Int.addNat k n) = Int.addNat k (Int.pred n).

Int.addNatComm

def addNatComm (k : Nat) (m : Nat) : Int.addNat k (pos m) = Int.addNat m (pos k)

Adding naturals onto non-negative integers is commutative: Int.addNat k (pos m) = Int.addNat m (pos k).

Int.addZeroL

def addZeroL (n : Int) : Int.add (pos Nat.zero) n = n

Zero is a left identity for integer addition: 0 + n = n.

Int.posCong

def posCong {m n : Nat} (p : m = n) : pos m = pos n

Congruence for pos: m = n implies pos m = pos n.

Int.negSuccCong

def negSuccCong {m n : Nat} (p : m = n) : negsucc m = negsucc n

Congruence for negsucc: m = n implies negsucc m = negsucc n.

Int.congNeg

def congNeg {m n : Int} (p : m = n) : Int.neg m = Int.neg n

Congruence for integer negation: m = n implies -m = -n.

Int.congAbs

def congAbs {m n : Int} (p : m = n) : Int.abs m = Int.abs n

Congruence for integer absolute value: m = n implies |m| = |n|.

Int.congSucc

def congSucc {m n : Int} (p : m = n) : Int.succ m = Int.succ n

Congruence for integer successor: m = n implies Int.succ m = Int.succ n.

Int.congPred

def congPred {m n : Int} (p : m = n) : Int.pred m = Int.pred n

Congruence for integer predecessor: m = n implies Int.pred m = Int.pred n.

Int.addZeroR

def addZeroR (n : Int) : Int.add n (pos Nat.zero) = n

Zero is a right identity for integer addition: m + 0 = m.

Int.mulNatOneV2

def mulNatOneV2 (n : Int) : Int.mulNat (Nat.succ Nat.zero) n = n

Multiplying an integer by the natural number one gives it back: Int.mulNat 1 n = n.

Int.absNegPos

def absNegPos (k : Nat) : Int.abs (Int.neg (pos k)) = Int.abs (pos k)

Negating a non-negative integer keeps its absolute value: |-(pos k)| = |pos k|.

Int.absNegNegsucc

def absNegNegsucc (k : Nat) : Int.abs (Int.neg (negsucc k)) = Int.abs (negsucc k)

Negating a negative integer keeps its absolute value: |-(negsucc k)| = |negsucc k|.

Int.absNeg

def absNeg (n : Int) : Int.abs (Int.neg n) = Int.abs n

Negation preserves absolute value: |-n| = |n|.

Int.mulZeroR

def mulZeroR (n : Int) : Int.mul n (pos Nat.zero) = pos Nat.zero

Zero absorbs integer multiplication on the right: m * 0 = 0.

Int.mulOneL

def mulOneL (n : Int) : Int.mul (pos (Nat.succ Nat.zero)) n = n

One is a left identity for integer multiplication: 1 * m = m.

Int.mulOneR

def mulOneR (n : Int) : Int.mul n (pos (Nat.succ Nat.zero)) = n

One is a right identity for integer multiplication: m * 1 = m.

Int.powZero

def powZero (n : Int) : Int.pow n Nat.zero = pos (Nat.succ Nat.zero)

Any integer to the power zero is one: n ^ 0 = 1.

Int.powOne

def powOne (n : Int) : Int.pow n (Nat.succ Nat.zero) = n

Any integer to the power one is itself: n ^ 1 = n.

Int.powOneBase

def powOneBase (k : Nat) : Int.pow (pos (Nat.succ Nat.zero)) k = pos (Nat.succ Nat.zero)

Every power of the integer one is one: 1 ^ k = 1.

Int.doubleIsAdd

def doubleIsAdd (n : Int) : Int.double n = Int.add n n

Int.double n unfolds to n + n.

Int.squareIsMul

def squareIsMul (n : Int) : Int.square n = Int.mul n n

Int.square n unfolds to n * n.

Int.ofNatToNatPos

def ofNatToNatPos (k : Nat) : Int.ofNat (Int.toNat (pos k)) = pos k

Round-tripping a non-negative integer through Nat gives it back: Int.ofNat (Int.toNat (pos k)) = pos k.

Int.intToOfNat

def intToOfNat (k : Nat) : Int.toNat (Int.ofNat k) = k

Round-tripping a natural number through Int gives it back: Int.toNat (Int.ofNat k) = k.

Int.five

def five : Int

The integer 5.

Int.negFive

def negFive : Int

The integer -5.

Int.cube

def cube (n : Int) : Int

Cube an integer: n * (n * n).

Int.absAs

def absAs (n : Int) : Int

Absolute value of an integer, as a non-negative integer.

Int.clamp

def clamp (lo : Int) (hi : Int) (n : Int) : Int

Clamp an integer into the range [lo, hi].

Int.eqDec

def eqDec (m : Int) (n : Int) : Bool

Boolean equality test on integers (an alias for Int.beq).

Int.litNeg

def litNeg (n : Nat) : Int

The negative integer -(n + 1), as a literal shorthand for negsucc n.

Int.succN

def succN (n : Nat) (x : Int) : Int

Apply Int.succ n times to x: x + n.

Int.predN

def predN (n : Nat) (x : Int) : Int

Apply Int.pred n times to x: x - n.

Int.three

def three : Int

The integer 3.

Int.four

def four : Int

The integer 4.

Int.ten

def ten : Int

The integer 10.

Int.negThree

def negThree : Int

The integer -3.

Int.negFour

def negFour : Int

The integer -4.

Int.congAdd

def congAdd {m1 m2 n1 n2 : Int} (p : m1 = m2) (q : n1 = n2) : Int.add m1 n1 = Int.add m2 n2

Congruence for integer addition in both arguments.

Int.congSub

def congSub {m1 m2 n1 n2 : Int} (p : m1 = m2) (q : n1 = n2) : Int.sub m1 n1 = Int.sub m2 n2

Congruence for integer subtraction in both arguments.

Int.congMul

def congMul {m1 m2 n1 n2 : Int} (p : m1 = m2) (q : n1 = n2) : Int.mul m1 n1 = Int.mul m2 n2

Congruence for integer multiplication in both arguments.

Int.congBeq

def congBeq {m1 m2 n1 n2 : Int} (p : m1 = m2) (q : n1 = n2) : Int.beq m1 n1 = Int.beq m2 n2

Congruence for boolean integer equality in both arguments.

Int.congBlt

def congBlt {m1 m2 n1 n2 : Int} (p : m1 = m2) (q : n1 = n2) : Int.blt m1 n1 = Int.blt m2 n2

Congruence for boolean integer less-than in both arguments.

Int.congSign

def congSign {m n : Int} (p : m = n) : Int.sign m = Int.sign n

Congruence for the integer sign function.

Int.congAbsAs

def congAbsAs {m n : Int} (p : m = n) : Int.absAs m = Int.absAs n

Congruence for Int.absAs.

Int.indPos

def indPos (P : Int -> Type) (z : P (pos Nat.zero)) (s : (m : Int) -> P m -> P (Int.succ m)) (k : Nat) : P (pos k)

Integer induction on the non-negative part: from P 0 and a successor step, P holds at every pos k.

Int.indNeg

def indNeg (P : Int -> Type) (z : P (pos Nat.zero)) (p : (m : Int) -> P m -> P (Int.pred m)) (k : Nat) : P (negsucc k)

Integer induction on the negative part: from P 0 and a predecessor step, P holds at every negsucc k.

Int.ind

def ind (P : Int -> Type) (z : P (pos Nat.zero)) (s : (m : Int) -> P m -> P (Int.succ m)) (p : (m : Int) -> P m -> P (Int.pred m)) (m : Int) : P m

Integer induction: from P 0, a successor step and a predecessor step, P holds at every integer.

Int.addNatPred

def addNatPred (k : Nat) (n : Int) : Int.addNat k (Int.pred n) = Int.pred (Int.addNat k n)

Adding a natural number commutes with predecessor: Int.addNat k (Int.pred n) = Int.pred (Int.addNat k n).

Int.subNatSuc

def subNatSuc (k : Nat) (n : Int) : Int.subNat k (Int.succ n) = Int.succ (Int.subNat k n)

Subtracting a natural number commutes with successor: Int.subNat k (Int.succ n) = Int.succ (Int.subNat k n).

Int.addSucR

def addSucR (m : Int) (n : Int) : Int.add m (Int.succ n) = Int.succ (Int.add m n)

Successor in the right summand moves outside: m + Int.succ n = Int.succ (m + n).

Int.addPredR

def addPredR (m : Int) (n : Int) : Int.add m (Int.pred n) = Int.pred (Int.add m n)

Predecessor in the right summand moves outside: m + Int.pred n = Int.pred (m + n).

Int.addSucL

def addSucL (m : Int) (n : Int) : Int.add (Int.succ m) n = Int.succ (Int.add m n)

Successor in the left summand moves outside: Int.succ m + n = Int.succ (m + n).

Int.addPredL

def addPredL (m : Int) (n : Int) : Int.add (Int.pred m) n = Int.pred (Int.add m n)

Predecessor in the left summand moves outside: Int.pred m + n = Int.pred (m + n).

Int.addComm

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

Commutativity of integer addition: m + n = n + m.

Int.addAssoc

def addAssoc (m : Int) (n : Int) (o : Int) : Int.add (Int.add m n) o = Int.add m (Int.add n o)

Associativity of integer addition: (m + n) + o = m + (n + o).

Int.negAdd

def negAdd (m : Int) (n : Int) : Int.neg (Int.add m n) = Int.add (Int.neg m) (Int.neg n)

Negation distributes over integer addition: -(m + n) = -m + -n.

Int.addNegR

def addNegR (m : Int) : Int.add m (Int.neg m) = pos Nat.zero

An integer plus its negation is zero: m + (-m) = 0.

Int.addNegL

def addNegL (m : Int) : Int.add (Int.neg m) m = pos Nat.zero

The negation of an integer plus the integer is zero: -m + m = 0.

Int.addSwap

def addSwap (a : Int) (b : Int) (c : Int) : Int.add a (Int.add b c) = Int.add b (Int.add a c)

Swap the first two summands of a right-nested sum: a + (b + c) = b + (a + c).

Int.mulSucL

def mulSucL (m : Int) (n : Int) : Int.mul (Int.succ m) n = Int.add n (Int.mul m n)

Successor in the left factor adds one copy: Int.succ m * n = n + m * n.

Int.mulPredL

def mulPredL (m : Int) (n : Int) : Int.mul (Int.pred m) n = Int.add (Int.neg n) (Int.mul m n)

Predecessor in the left factor subtracts one copy: Int.pred m * n = -n + m * n.

Int.mulDistribR

def mulDistribR (m : Int) (n : Int) (o : Int) : Int.mul (Int.add m n) o = Int.add (Int.mul m o) (Int.mul n o)

Integer multiplication distributes over addition on the left factor: (m + n) * o = m * o + n * o.

Int.mulSucR

def mulSucR (m : Int) (n : Int) : Int.mul m (Int.succ n) = Int.add m (Int.mul m n)

Successor in the right factor adds one copy: m * Int.succ n = m + m * n.

Int.mulPredR

def mulPredR (m : Int) (n : Int) : Int.mul m (Int.pred n) = Int.add (Int.neg m) (Int.mul m n)

Predecessor in the right factor subtracts one copy: m * Int.pred n = -m + m * n.

Int.mulComm

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

Commutativity of integer multiplication: m * n = n * m.

Int.mulDistribL

def mulDistribL (m : Int) (n : Int) (o : Int) : Int.mul m (Int.add n o) = Int.add (Int.mul m n) (Int.mul m o)

Integer multiplication distributes over addition on the right factor: m * (n + o) = m * n + m * o.

Int.mulNegL

def mulNegL (m : Int) (n : Int) : Int.mul (Int.neg m) n = Int.neg (Int.mul m n)

Negation of the left factor negates the product: (-m) * n = -(m * n).

Int.mulAssoc

def mulAssoc (m : Int) (n : Int) (o : Int) : Int.mul (Int.mul m n) o = Int.mul m (Int.mul n o)

Associativity of integer multiplication: (m * n) * o = m * (n * o).

Int.addNatPos

def addNatPos (k : Nat) (m : Nat) : Int.addNat k (pos m) = pos (Nat.add k m)

Adding a natural to a non-negative integer stays non-negative: Int.addNat k (pos m) = pos (k + m).

Int.mulNatPos

def mulNatPos (n : Nat) (m : Nat) : Int.mulNat n (pos m) = pos (Nat.mul n m)

Multiplying a non-negative integer by a natural stays non-negative: Int.mulNat n (pos m) = pos (n * m).

Int.quot

def quot (a : Int) (b : Int) : Int

Truncating integer division (C++ semantics): divides the absolute values and gives the quotient the product of the signs; division by zero gives zero.

Int.rem

def rem (a : Int) (b : Int) : Int

Integer remainder matching truncating division (C++ semantics): takes the sign of the dividend; division by zero returns the dividend.

Int.negOfNat

def negOfNat (k : Nat) : Int

The negation of a natural number, as an integer: -k.

Int.subNatNat

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

Subtract two naturals into an integer, m - n, using fast natural-number subtraction instead of step-by-step recursion.

Int.addFast

def addFast (a : Int) (b : Int) : Int

Fast integer addition built on accelerated natural-number operations; provably equal to Int.add.

Int.subFast

def subFast (a : Int) (b : Int) : Int

Fast integer subtraction built on Int.addFast; provably equal to Int.sub.

Int.mulFast

def mulFast (a : Int) (b : Int) : Int

Fast integer multiplication built on accelerated natural-number operations; provably equal to Int.mul.

Int.subNatSlow

def subNatSlow (m : Nat) (n : Nat) : Int

Natural subtraction m - n into an integer, peeling both arguments in step; a proof intermediate for Int.subNatNat.

Int.subNatNatSlow

def subNatNatSlow (m : Nat) (n : Nat) : Int.subNatNat m n = Int.subNatSlow m n

The fast and the step-by-step natural subtraction agree: Int.subNatNat m n = Int.subNatSlow m n.

Int.subNatSlowZero

def subNatSlowZero (a : Nat) : Int.subNatSlow a Nat.zero = pos a

Subtracting zero gives the non-negative integer itself: Int.subNatSlow a 0 = pos a.

Int.succSubNatSlow

def succSubNatSlow (j : Nat) (n : Nat) : Int.succ (Int.subNatSlow j (Nat.succ n)) = Int.subNatSlow j n

Successor of j - (n + 1) is j - n, for natural subtraction into the integers.

Int.predSubNatSlow

def predSubNatSlow (n : Nat) (j : Nat) : Int.pred (Int.subNatSlow n j) = Int.subNatSlow n (Nat.succ j)

Predecessor of n - j is n - (j + 1), for natural subtraction into the integers.

Int.addNatNegsucc

def addNatNegsucc (m : Nat) (n : Nat) : Int.addNat m (negsucc n) = Int.subNatSlow m (Nat.succ n)

Adding m to -(n + 1) is m - (n + 1): Int.addNat m (negsucc n) = Int.subNatSlow m (n + 1).

Int.subNatPos

def subNatPos (k : Nat) (n : Nat) : Int.subNat k (pos n) = Int.subNatSlow n k

Subtracting k from a non-negative integer n is n - k: Int.subNat k (pos n) = Int.subNatSlow n k.

Int.subNatNegsucc

def subNatNegsucc (k : Nat) (n : Nat) : Int.subNat k (negsucc n) = negsucc (Nat.add k n)

Subtracting k from -(n + 1) gives -(k + n + 1): Int.subNat k (negsucc n) = negsucc (k + n).

Int.addEqAddFast

def addEqAddFast (a : Int) (b : Int) : Int.add a b = Int.addFast a b

The fast integer addition agrees with integer addition: Int.add a b = Int.addFast a b.

Int.subEqSubFast

def subEqSubFast (a : Int) (b : Int) : Int.sub a b = Int.subFast a b

The fast integer subtraction agrees with integer subtraction: Int.sub a b = Int.subFast a b.

Int.addNegsuccNegOfNat

def addNegsuccNegOfNat (n : Nat) (k : Nat) : Int.add (negsucc n) (Int.negOfNat k) = Int.negOfNat (Nat.add (Nat.succ n) k)

Adding two negative quantities: -(n + 1) + (-k) = -((n + 1) + k).

Int.mulNatNegsucc

def mulNatNegsucc (m : Nat) (n : Nat) : Int.mulNat m (negsucc n) = Int.negOfNat (Nat.mul m (Nat.succ n))

Multiplying a negative integer by a natural: Int.mulNat m (negsucc n) = -(m * (n + 1)).

Int.mulEqMulFast

def mulEqMulFast (a : Int) (b : Int) : Int.mul a b = Int.mulFast a b

The fast integer multiplication agrees with integer multiplication: Int.mul a b = Int.mulFast a b.

Int.andTrueI

def andTrueI (b : Bool) (c : Bool) (hb : b = true) (hc : c = true) : and b c = true

Boolean conjunction introduction: if b = true and c = true then and b c = true.

Int.emod

def emod (v : Int) (m : Nat) : Nat

Euclidean remainder of an integer modulo m + 1, always in [0, m].

Int.emodLt

def emodLt (v : Int) (m : Nat) : Nat.blt (Int.emod v m) (Nat.succ m) = true

The Euclidean remainder is in range: Int.emod v m < m + 1.

Int.bleZeroPos

def bleZeroPos (e : Nat) : Int.ble (pos 0) (pos e) = true

Zero is at most every non-negative integer: 0 <= pos e.

Int.bleOfLtSucc

def bleOfLtSucc (e : Nat) (m : Nat) (h : Nat.blt e (Nat.succ m) = true) : Int.ble (pos e) (pos m) = true

A strict bound by a successor gives a non-strict bound: e < m + 1 implies pos e <= pos m.

Int.bleNegOfLt

def bleNegOfLt (k : Nat) (a : Nat) (h : Nat.blt k (Nat.succ a) = true) : Int.ble (negsucc a) (negsucc k) = true

Ordering of negative integers reverses: k < a + 1 implies -(a + 1) <= -(k + 1).

Int.subAddLt

def subAddLt (a : Nat) (b : Nat) (e : Nat) (h : Nat.blt e (Nat.succ a) = false) : Nat.blt (Nat.sub (Nat.add a (Nat.succ b)) e) (Nat.succ b) = true

If e ≥ a + 1 then (a + (b + 1)) - e < b + 1, with truncated subtraction.

Int.twos

def twos (h : Nat) (e : Nat) : Int

Two’s-complement reading of an unsigned value e modulo 2h, where h = 2^(w-1): e itself when e < h, otherwise e - 2h.

Int.twosStep

def twosStep (h0 : Nat) (e : Nat) (c : Bool) : Int

One branch step of Int.twos, chosen by the boolean c (the result of e < h0 + 1); a proof helper for Int.twosIn.

Int.twosIn

def twosIn (h0 : Nat) (e : Nat) : and (Int.ble (negsucc h0) (Int.twos (Nat.succ h0) e)) (Int.ble (Int.twos (Nat.succ h0) e) (pos h0)) = true

The two’s-complement reading for h = h0 + 1 lies in [-(h0 + 1), h0].

Int.signedRange

def signedRange (h : Nat) (hp : Nat.blt 0 h = true) (e : Nat) : and (Int.ble (Int.negOfNat h) (Int.twos h e)) (Int.ble (Int.twos h e) (pos (Nat.pred h))) = true

For positive h, the two’s-complement reading Int.twos h e lies in [-h, h - 1].

Int.twosMod

def twosMod (h : Nat) (v : Int) : Int

Wrap an integer into two’s-complement range: the representative of v modulo 2h in [-h, h - 1].

Int.twosModRange

def twosModRange (h : Nat) (hp : Nat.blt 0 h = true) (v : Int) : and (Int.ble (Int.negOfNat h) (Int.twosMod h v)) (Int.ble (Int.twosMod h v) (pos (Nat.pred h))) = true

For positive h, Int.twosMod h v lies in [-h, h - 1].

Int.toString

def toString (v : Int) : String

Decimal string representation of an integer, with a leading minus sign when negative.

Int.toStringInt

instance toStringInt : ToString Int

Decimal rendering of integers, with a leading - for negatives.

Int.parse

def parse (s : String) : Option Int

Parse a decimal integer with an optional leading minus sign, returning nothing for anything else.

Int.floorDiv

def floorDiv (v : Int) (d : Nat) : Int

Division by a positive natural number rounded toward negative infinity; dividing by zero gives zero.