Skip to content
Cella Lang

nat

Nat.mulComm

Section titled “Nat.mulComm”
def Nat.mulComm (m : Nat) (n : Nat) : mul m n = mul n m

Commutativity of natural-number multiplication: m * n = n * m.

Nat.mulDistribL

Section titled “Nat.mulDistribL”
def Nat.mulDistribL (m : Nat) (n : Nat) (k : Nat) : mul (add m n) k = add (mul m k) (mul n k)

Multiplication distributes over addition on the left factor: (m + n) * k = m * k + n * k.

Nat.mulDistribR

Section titled “Nat.mulDistribR”
def Nat.mulDistribR (m : Nat) (n : Nat) (k : Nat) : mul m (add n k) = add (mul m n) (mul m k)

Multiplication distributes over addition on the right factor: m * (n + k) = m * n + m * k.

Nat.mulAssoc

Section titled “Nat.mulAssoc”
def Nat.mulAssoc (m : Nat) (n : Nat) (k : Nat) : mul (mul m n) k = mul m (mul n k)

Associativity of natural-number multiplication: (m * n) * k = m * (n * k).

Nat.mulTwoR

Section titled “Nat.mulTwoR”
def Nat.mulTwoR (n : Nat) : mul (succ (succ zero)) n = add n n

Doubling as multiplication: 2 * n = n + n.

Nat.mulOneLNat

Section titled “Nat.mulOneLNat”
def Nat.mulOneLNat (n : Nat) : mul (succ zero) n = n

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

Nat.subSelf

Section titled “Nat.subSelf”
def Nat.subSelf (n : Nat) : sub n n = zero

Truncated subtraction of a number from itself is zero: n - n = 0.

Nat.beqReflNat

Section titled “Nat.beqReflNat”
def Nat.beqReflNat (n : Nat) : Nat.beq n n = true

Boolean equality is reflexive: Nat.beq n n = true.

Nat.bltRefl

Section titled “Nat.bltRefl”
def Nat.bltRefl (n : Nat) : Nat.blt n n = false

Strict less-than is irreflexive as a boolean test: Nat.blt n n = false.

Nat.bltZeroSucc

Section titled “Nat.bltZeroSucc”
def Nat.bltZeroSucc (n : Nat) : Nat.blt zero (succ n) = true

Zero is strictly less than every successor: Nat.blt 0 (n + 1) = true.

Nat.maxZeroL

Section titled “Nat.maxZeroL”
def Nat.maxZeroL (n : Nat) : max zero n = n

Zero is a left identity for max: max 0 n = n.

Nat.minZeroL

Section titled “Nat.minZeroL”
def Nat.minZeroL (n : Nat) : min zero n = zero

Zero absorbs min on the left: min 0 n = 0.

Nat.subZeroL

Section titled “Nat.subZeroL”
def Nat.subZeroL (n : Nat) : sub zero n = zero

Truncated subtraction from zero is zero: 0 - n = 0.

Nat.addSuccRSym

Section titled “Nat.addSuccRSym”
def Nat.addSuccRSym (m : Nat) (n : Nat) : succ (add m n) = add m (succ n)

Moving succ out of the right summand, in reverse direction: succ (m + n) = m + succ n.

Nat.powSucc

Section titled “Nat.powSucc”
def Nat.powSucc (b : Nat) (n : Nat) : Nat.pow b (succ n) = mul b (Nat.pow b n)

Unfolding of power at a successor exponent: b ^ (n + 1) = b * b ^ n.

Nat.mulOneRNat

Section titled “Nat.mulOneRNat”
def Nat.mulOneRNat (n : Nat) : mul n (succ zero) = n

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

Nat.powOneBase

Section titled “Nat.powOneBase”
def Nat.powOneBase (n : Nat) : Nat.pow (succ zero) n = succ zero

Every power of one is one: 1 ^ n = 1.

Nat.triple

Section titled “Nat.triple”
def Nat.triple (n : Nat) : Nat

Triple a natural number: n + (n + n).

Nat.succPred

Section titled “Nat.succPred”
def Nat.succPred (n : Nat) : succ (pred (succ n)) = succ n

Taking the predecessor of a successor and then the successor gives it back: succ (pred (succ n)) = succ n.

Nat.predSucc

Section titled “Nat.predSucc”
def Nat.predSucc (n : Nat) : pred (succ n) = n

The predecessor of a successor: pred (succ n) = n.

Nat.addCommNat

Section titled “Nat.addCommNat”
def Nat.addCommNat (m : Nat) (n : Nat) : add m n = add n m

Commutativity of natural-number addition: m + n = n + m.

Nat.addRightSucc

Section titled “Nat.addRightSucc”
def Nat.addRightSucc (m : Nat) (n : Nat) : add m (succ n) = succ (add m n)

Moving succ out of the right summand: m + succ n = succ (m + n).

Nat.mulZeroLNat

Section titled “Nat.mulZeroLNat”
def Nat.mulZeroLNat (n : Nat) : mul zero n = zero

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

Nat.powZeroBase

Section titled “Nat.powZeroBase”
def Nat.powZeroBase (n : Nat) : Nat.pow zero (succ n) = zero

Zero to any positive power is zero: 0 ^ (n + 1) = 0.

Nat.factorialSucc

Section titled “Nat.factorialSucc”
def Nat.factorialSucc (n : Nat) : factorial (succ n) = mul (succ n) (factorial n)

Unfolding of factorial at a successor: (n + 1)! = (n + 1) * n!.

Nat.isEvenB

Section titled “Nat.isEvenB”
def Nat.isEvenB (n : Nat) : Bool

Boolean test for whether a natural number is even.

Nat.addAssocNat

Section titled “Nat.addAssocNat”
def Nat.addAssocNat (m : Nat) (n : Nat) (o : Nat) : add m (add n o) = add (add m n) o

Associativity of natural-number addition, right-nested to left-nested: m + (n + o) = (m + n) + o.

Nat.sumTo

Section titled “Nat.sumTo”
def Nat.sumTo (n : Nat) : Nat

Sum of the natural numbers from 1 to n.

Nat.subSuccSucc

Section titled “Nat.subSuccSucc”
def Nat.subSuccSucc (m : Nat) (n : Nat) : sub (succ m) (succ n) = sub m n

Truncated subtraction cancels a common successor: (m + 1) - (n + 1) = m - n.

Nat.isOddB

Section titled “Nat.isOddB”
def Nat.isOddB (n : Nat) : Bool

Boolean test for whether a natural number is odd (the negation of isEvenB).

Nat.powOneExp

Section titled “Nat.powOneExp”
def Nat.powOneExp (n : Nat) : Nat.pow n (succ zero) = n

The first power of a number is the number itself: n ^ 1 = n.

Nat.addLeftCancelZero

Section titled “Nat.addLeftCancelZero”
def Nat.addLeftCancelZero (n : Nat) : add zero n = n

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

Nat.square

Section titled “Nat.square”
def Nat.square (n : Nat) : Nat

The square of a natural number: n * n.

Nat.cube

Section titled “Nat.cube”
def Nat.cube (n : Nat) : Nat

The cube of a natural number: n * (n * n).

Nat.predNat

Section titled “Nat.predNat”
def Nat.predNat (n : Nat) : Nat

Predecessor of a natural number, sending zero to zero.

Nat.absDiff

Section titled “Nat.absDiff”
def Nat.absDiff (m : Nat) (n : Nat) : Nat

Absolute difference of two naturals, |m - n|, computed as (m - n) + (n - m) with truncated subtraction.

Nat.predNatSucc

Section titled “Nat.predNatSucc”
def Nat.predNatSucc (n : Nat) : predNat (succ n) = n

The predecessor of a successor: predNat (n + 1) = n.

Nat.predNatZero

Section titled “Nat.predNatZero”
def Nat.predNatZero : predNat zero = zero

The predecessor of zero is zero.

Nat.powZero

Section titled “Nat.powZero”
def Nat.powZero (b : Nat) : pow b zero = succ zero

Any base to the exponent zero is one: pow b 0 = 1.

Nat.powOne

Section titled “Nat.powOne”
def Nat.powOne (b : Nat) : pow b (succ zero) = b

Any base to the exponent one is itself: pow b 1 = b.

Nat.absDiffSelf

Section titled “Nat.absDiffSelf”
def Nat.absDiffSelf (n : Nat) : absDiff n n = zero

The absolute difference of a number with itself is zero.

Nat.divMod

Section titled “Nat.divMod”
def Nat.divMod (m : Nat) (n : Nat) : Nat × Nat

Quotient and remainder of m divided by n, as a pair.

Nat.doubleNat

Section titled “Nat.doubleNat”
def Nat.doubleNat (n : Nat) : Nat

Double a natural number: n + n.

Nat.halve

Section titled “Nat.halve”
def Nat.halve (n : Nat) : Nat

Halve a natural number, rounding down (division by 2).

Nat.tripleNat

Section titled “Nat.tripleNat”
def Nat.tripleNat (n : Nat) : Nat

Triple a natural number: n + (n + n).

Nat.n0

Section titled “Nat.n0”
def Nat.n0 : Nat

The natural number 0, as a named constant.

Nat.n1

Section titled “Nat.n1”
def Nat.n1 : Nat

The natural number 1, as a named constant.

Nat.n2

Section titled “Nat.n2”
def Nat.n2 : Nat

The natural number 2, as a named constant.

Nat.n3

Section titled “Nat.n3”
def Nat.n3 : Nat

The natural number 3, as a named constant.

Nat.n4

Section titled “Nat.n4”
def Nat.n4 : Nat

The natural number 4, as a named constant.

Nat.n5

Section titled “Nat.n5”
def Nat.n5 : Nat

The natural number 5, as a named constant.

Nat.n6

Section titled “Nat.n6”
def Nat.n6 : Nat

The natural number 6, as a named constant.

Nat.n7

Section titled “Nat.n7”
def Nat.n7 : Nat

The natural number 7, as a named constant.

Nat.n8

Section titled “Nat.n8”
def Nat.n8 : Nat

The natural number 8, as a named constant.

Nat.n9

Section titled “Nat.n9”
def Nat.n9 : Nat

The natural number 9, as a named constant.

Nat.n10

Section titled “Nat.n10”
def Nat.n10 : Nat

The natural number 10, as a named constant.

Nat.n11

Section titled “Nat.n11”
def Nat.n11 : Nat

The natural number 11, as a named constant.

Nat.n12

Section titled “Nat.n12”
def Nat.n12 : Nat

The natural number 12, as a named constant.

Nat.n13

Section titled “Nat.n13”
def Nat.n13 : Nat

The natural number 13, as a named constant.

Nat.n14

Section titled “Nat.n14”
def Nat.n14 : Nat

The natural number 14, as a named constant.

Nat.n15

Section titled “Nat.n15”
def Nat.n15 : Nat

The natural number 15, as a named constant.

Nat.n16

Section titled “Nat.n16”
def Nat.n16 : Nat

The natural number 16, as a named constant.

Nat.n17

Section titled “Nat.n17”
def Nat.n17 : Nat

The natural number 17, as a named constant.

Nat.n18

Section titled “Nat.n18”
def Nat.n18 : Nat

The natural number 18, as a named constant.

Nat.n19

Section titled “Nat.n19”
def Nat.n19 : Nat

The natural number 19, as a named constant.

Nat.n20

Section titled “Nat.n20”
def Nat.n20 : Nat

The natural number 20, as a named constant.

Nat.quadruple

Section titled “Nat.quadruple”
def Nat.quadruple (n : Nat) : Nat

Quadruple a natural number: (n + n) + (n + n).

Nat.quintuple

Section titled “Nat.quintuple”
def Nat.quintuple (n : Nat) : Nat

Quintuple a natural number: n + 4n.

Nat.isNonZero

Section titled “Nat.isNonZero”
def Nat.isNonZero (n : Nat) : Bool

Boolean test for whether a natural number is nonzero.

Nat.saturatingSub

Section titled “Nat.saturatingSub”
def Nat.saturatingSub (m : Nat) (n : Nat) : Nat

Saturating subtraction: m - n, or zero when n exceeds m (an explicit name for sub).

Nat.n24

Section titled “Nat.n24”
def Nat.n24 : Nat

The natural number 24, as a named constant.

Nat.n21

Section titled “Nat.n21”
def Nat.n21 : Nat

The natural number 21, as a named constant.

Nat.divAux

Section titled “Nat.divAux”
def Nat.divAux (fuel : Nat) (m : Nat) (n : Nat) : Nat

Division m / n by repeated subtraction, bounded by fuel; returns zero when n is zero or the fuel runs out.

Nat.div2

Section titled “Nat.div2”
def Nat.div2 (m : Nat) (n : Nat) : Nat

Division m / n by repeated subtraction, with enough fuel to finish; returns zero when n is zero.

Nat.n22

Section titled “Nat.n22”
def Nat.n22 : Nat

The natural number 22, as a named constant.

Nat.n25

Section titled “Nat.n25”
def Nat.n25 : Nat

The natural number 25, as a named constant.

Nat.n27

Section titled “Nat.n27”
def Nat.n27 : Nat

The natural number 27, as a named constant.

Nat.n28

Section titled “Nat.n28”
def Nat.n28 : Nat

The natural number 28, as a named constant.

Nat.simpAddZeroAddZero

Section titled “Nat.simpAddZeroAddZero”
-- T097: change proofs /-- Zero is a left identity for addition (proved with change): 0 + n = n. -/ -- =================================================================== -- Tactic 實戰驗證 (simp, injection, discriminate, conv, etc.) -- =================================================================== -- T009: simp with @[simp] lemma (NbE-solvable) /-- Adding zero twice on the left changes nothing: 0 + (0 + n) = n. -/ theorem Nat.simpAddZeroAddZero (n : Nat) : add zero (add zero n) = n

Zero is a left identity for addition, registered as a simp lemma: 0 + n = n.

Nat.simpAddZeroSuccN

Section titled “Nat.simpAddZeroSuccN”
theorem Nat.simpAddZeroSuccN (n : Nat) : add zero (succ n) = succ n

Zero is a left identity for addition at a successor: 0 + succ n = succ n.

Nat.zeroNeqSucc

Section titled “Nat.zeroNeqSucc”
theorem Nat.zeroNeqSucc (n : Nat) (h : zero = succ n) : Empty

Zero is not a successor: a proof of zero = succ n yields Empty.

Nat.first_test

Section titled “Nat.first_test”
theorem Nat.first_test : Nat

A natural number built with the first tactic, which picks the first alternative that succeeds (here one).

Nat.gcdFuel

Section titled “Nat.gcdFuel”
def Nat.gcdFuel (fuel : Nat) (m : Nat) (n : Nat) : Nat

Greatest common divisor by the Euclidean algorithm, bounded by fuel.

Nat.gcdNat

Section titled “Nat.gcdNat”
def Nat.gcdNat (m : Nat) (n : Nat) : Nat

Greatest common divisor of two natural numbers.

Nat.lcmNat

Section titled “Nat.lcmNat”
def Nat.lcmNat (m : Nat) (n : Nat) : Nat

Least common multiple of two natural numbers: m * n / gcd m n.

Even

Section titled “Even”
data Even : Nat -> Type

Proof-relevant evenness predicate: zero is even, and n + 2 is even when n is.

Odd

Section titled “Odd”
data Odd : Nat -> Type

Proof-relevant oddness predicate: one is odd, and n + 2 is odd when n is.

Nat.even0

Section titled “Nat.even0”
def Nat.even0 : Even n0

Evidence that 0 is even.

Nat.even2

Section titled “Nat.even2”
def Nat.even2 : Even n2

Evidence that 2 is even.

Nat.even4

Section titled “Nat.even4”
def Nat.even4 : Even n4

Evidence that 4 is even.

Nat.even6

Section titled “Nat.even6”
def Nat.even6 : Even n6

Evidence that 6 is even.

Nat.even8

Section titled “Nat.even8”
def Nat.even8 : Even n8

Evidence that 8 is even.

Nat.even10

Section titled “Nat.even10”
def Nat.even10 : Even n10

Evidence that 10 is even.

Nat.odd1

Section titled “Nat.odd1”
def Nat.odd1 : Odd n1

Evidence that 1 is odd.

Nat.odd3

Section titled “Nat.odd3”
def Nat.odd3 : Odd n3

Evidence that 3 is odd.

Nat.odd5

Section titled “Nat.odd5”
def Nat.odd5 : Odd n5

Evidence that 5 is odd.

Nat.odd7

Section titled “Nat.odd7”
def Nat.odd7 : Odd n7

Evidence that 7 is odd.

Nat.odd9

Section titled “Nat.odd9”
def Nat.odd9 : Odd n9

Evidence that 9 is odd.

Nat.evenPlus2

Section titled “Nat.evenPlus2”
def Nat.evenPlus2 (n : Nat) (ev : Even n) : Even (succ (succ n))

If n is even then n + 2 is even.

Nat.oddPlus2

Section titled “Nat.oddPlus2”
def Nat.oddPlus2 (n : Nat) (od : Odd n) : Odd (succ (succ n))

If n is odd then n + 2 is odd.

Nat.bltSuccZero

Section titled “Nat.bltSuccZero”
def Nat.bltSuccZero (n : Nat) : Nat.blt (succ n) zero = false

No successor is strictly less than zero: Nat.blt (n + 1) 0 = false.

Nat.beqZeroSucc

Section titled “Nat.beqZeroSucc”
def Nat.beqZeroSucc (n : Nat) : Nat.beq zero (succ n) = false

Zero is not boolean-equal to any successor: Nat.beq 0 (n + 1) = false.

Nat.beqSuccZero

Section titled “Nat.beqSuccZero”
def Nat.beqSuccZero (n : Nat) : Nat.beq (succ n) zero = false

No successor is boolean-equal to zero: Nat.beq (n + 1) 0 = false.

Nat.maxZeroR

Section titled “Nat.maxZeroR”
def Nat.maxZeroR (n : Nat) : max n zero = n

Zero is a right identity for max: max n 0 = n.

Nat.minZeroR

Section titled “Nat.minZeroR”
def Nat.minZeroR (n : Nat) : min n zero = zero

Zero absorbs min on the right: min n 0 = 0.

Nat.succInjV2

Section titled “Nat.succInjV2”
theorem Nat.succInjV2 (a : Nat) (b : Nat) (h : succ a = succ b) : a = b

The successor constructor is injective: succ a = succ b implies a = b.

Nat.succSuccInj

Section titled “Nat.succSuccInj”
def Nat.succSuccInj (a : Nat) (b : Nat) (h : succ (succ a) = succ (succ b)) : a = b

Applying succ twice is injective: succ (succ a) = succ (succ b) implies a = b.

Nat.succNeqZero

Section titled “Nat.succNeqZero”
theorem Nat.succNeqZero (n : Nat) (h : succ n = zero) : Empty

No successor is zero: a proof of succ n = zero yields Empty.

Nat.n23

Section titled “Nat.n23”
def Nat.n23 : Nat

The natural number 23, as a named constant.

Nat.n26

Section titled “Nat.n26”
def Nat.n26 : Nat

The natural number 26, as a named constant.

Nat.n29

Section titled “Nat.n29”
def Nat.n29 : Nat

The natural number 29, as a named constant.

Nat.n30

Section titled “Nat.n30”
def Nat.n30 : Nat

The natural number 30, as a named constant.

Nat.subZeroR

Section titled “Nat.subZeroR”
def Nat.subZeroR (n : Nat) : sub n zero = n

Zero is a right identity for truncated subtraction: n - 0 = n.

Nat.isEvenBSS

Section titled “Nat.isEvenBSS”
def Nat.isEvenBSS (n : Nat) : isEvenB (succ (succ n)) = isEvenB n

Adding two preserves evenness: isEvenB (n + 2) = isEvenB n.

Nat.isOddBSS

Section titled “Nat.isOddBSS”
def Nat.isOddBSS (n : Nat) : isOddB (succ (succ n)) = isOddB n

Adding two preserves oddness: isOddB (n + 2) = isOddB n.

Nat.even12

Section titled “Nat.even12”
def Nat.even12 : Even n12

Evidence that 12 is even.

Nat.even14

Section titled “Nat.even14”
def Nat.even14 : Even n14

Evidence that 14 is even.

Nat.even16

Section titled “Nat.even16”
def Nat.even16 : Even n16

Evidence that 16 is even.

Nat.even18

Section titled “Nat.even18”
def Nat.even18 : Even n18

Evidence that 18 is even.

Nat.even20

Section titled “Nat.even20”
def Nat.even20 : Even n20

Evidence that 20 is even.

Nat.odd11

Section titled “Nat.odd11”
def Nat.odd11 : Odd n11

Evidence that 11 is odd.

Nat.odd13

Section titled “Nat.odd13”
def Nat.odd13 : Odd n13

Evidence that 13 is odd.

Nat.odd15

Section titled “Nat.odd15”
def Nat.odd15 : Odd n15

Evidence that 15 is odd.

Nat.odd17

Section titled “Nat.odd17”
def Nat.odd17 : Odd n17

Evidence that 17 is odd.

Nat.odd19

Section titled “Nat.odd19”
def Nat.odd19 : Odd n19

Evidence that 19 is odd.

Nat.n36

Section titled “Nat.n36”
def Nat.n36 : Nat

The natural number 36, as 6 * 6.

Nat.n49

Section titled “Nat.n49”
def Nat.n49 : Nat

The natural number 49, as 7 * 7.

Nat.Divides

Section titled “Nat.Divides”
def Nat.Divides (m : Nat) (n : Nat) : Type

Divisibility: m divides n when m * k = n for some k.

Nat.dividesRefl

Section titled “Nat.dividesRefl”
def Nat.dividesRefl (n : Nat) : Divides n n

Every natural number divides itself.

Nat.onesDivides

Section titled “Nat.onesDivides”
def Nat.onesDivides (n : Nat) : Divides (succ zero) n

One divides every natural number.

Nat.dividesZero

Section titled “Nat.dividesZero”
def Nat.dividesZero (n : Nat) : Divides n zero

Every natural number divides zero.

Nat.prime2

Section titled “Nat.prime2”
def Nat.prime2 : Nat

The prime number 2, as a named constant.

Nat.prime3

Section titled “Nat.prime3”
def Nat.prime3 : Nat

The prime number 3, as a named constant.

Nat.prime5

Section titled “Nat.prime5”
def Nat.prime5 : Nat

The prime number 5, as a named constant.

Nat.prime7

Section titled “Nat.prime7”
def Nat.prime7 : Nat

The prime number 7, as a named constant.

Nat.zeroBle

Section titled “Nat.zeroBle”
def Nat.zeroBle (n : Nat) : Nat.ble zero n = true

Zero is below every natural number.

Nat.bleAddSelf

Section titled “Nat.bleAddSelf”
def Nat.bleAddSelf (x : Nat) (y : Nat) : Nat.ble x (add x y) = true

A number is at most itself plus anything: x <= x + y.

Nat.bleTrans

Section titled “Nat.bleTrans”
def Nat.bleTrans (a : Nat) (b : Nat) (c : Nat) : Nat.ble a b = true -> Nat.ble b c = true -> Nat.ble a c = true

Less-or-equal is transitive.

Nat.bleAddLeft

Section titled “Nat.bleAddLeft”
def Nat.bleAddLeft (k : Nat) (a : Nat) (b : Nat) (h : Nat.ble a b = true) : Nat.ble (add k a) (add k b) = true

Adding the same number on the left keeps the order: a <= b gives k + a <= k + b.

Nat.bltFalseOfBle

Section titled “Nat.bltFalseOfBle”
def Nat.bltFalseOfBle (a : Nat) (b : Nat) : Nat.ble a b = true -> Nat.blt b a = false

Less-or-equal rules out strictly greater: a <= b gives not (b < a).

Nat.bleMulLeft

Section titled “Nat.bleMulLeft”
def Nat.bleMulLeft (c : Nat) (a : Nat) (b : Nat) (h : Nat.ble a b = true) : Nat.ble (mul c a) (mul c b) = true

Multiplying on the left keeps the order: a <= b gives c * a <= c * b.

Nat.bleMulRight

Section titled “Nat.bleMulRight”
def Nat.bleMulRight (c : Nat) (a : Nat) (b : Nat) (h : Nat.ble a b = true) : Nat.ble (mul a c) (mul b c) = true

Multiplying on the right keeps the order: a <= b gives a * c <= b * c.

Nat.bleMulBoth

Section titled “Nat.bleMulBoth”
def Nat.bleMulBoth (a : Nat) (b : Nat) (c : Nat) (d : Nat) (hab : Nat.ble a b = true) (hcd : Nat.ble c d = true) : Nat.ble (mul a c) (mul b d) = true

Products are monotone in both factors: a <= b and c <= d give a * c <= b * d.

Nat.squareDouble

Section titled “Nat.squareDouble”
def Nat.squareDouble (x : Nat) : mul (mul 2 x) (mul 2 x) = mul 4 (mul x x)

The square of a double is four times the square: (2x)(2x) = 4(x x).

Nat.bltAddLeft

Section titled “Nat.bltAddLeft”
def Nat.bltAddLeft (k : Nat) (a : Nat) (b : Nat) (h : Nat.blt a b = true) : Nat.blt (add k a) (add k b) = true

Adding the same number on the left keeps a strict order.

Nat.bltBleTrans

Section titled “Nat.bltBleTrans”
def Nat.bltBleTrans (a : Nat) (b : Nat) (c : Nat) : Nat.blt a b = true -> Nat.ble b c = true -> Nat.blt a c = true

A strict order followed by an order is strict: a < b <= c gives a < c.

Nat.bltOfBleFalse

Section titled “Nat.bltOfBleFalse”
def Nat.bltOfBleFalse (a : Nat) (b : Nat) : Nat.ble a b = false -> Nat.blt b a = true

Not at most means strictly above: not (a <= b) gives b < a.

Nat.sqrtStep

Section titled “Nat.sqrtStep”
def Nat.sqrtStep (n : Nat) (r : Nat) : Nat

One digit of the square root: given 2 * sqrt (n / 4), take one more when it still fits.

Nat.sqrtFuel

Section titled “Nat.sqrtFuel”
def Nat.sqrtFuel (fuel : Nat) (n : Nat) : Nat

The square root by halving in base 4, with fuel bounding the depth (n itself is enough); stops at zero.

Nat.sqrtDigits

Section titled “Nat.sqrtDigits”
def Nat.sqrtDigits (n : Nat) : Nat

The integer square root digit by digit (the version the proofs are about).

Nat.mulFourQuarterBle

Section titled “Nat.mulFourQuarterBle”
def Nat.mulFourQuarterBle (n : Nat) : Nat.ble (mul 4 (Nat.div n 4)) n = true

Four times a quarter is at most the number: 4 * (n / 4) <= n.

Nat.sqrtDoubleSquareLe

Section titled “Nat.sqrtDoubleSquareLe”
def Nat.sqrtDoubleSquareLe (n : Nat) (r0 : Nat) (h : Nat.ble (mul r0 r0) (Nat.div n 4) = true) : Nat.ble (mul (mul 2 r0) (mul 2 r0)) n = true

Twice the square root of the quarter squares to at most n.

Nat.sqrtStepSquareLeAt

Section titled “Nat.sqrtStepSquareLeAt”
def Nat.sqrtStepSquareLeAt (n : Nat) (r : Nat) (b : Bool) (e : Nat.ble (mul (succ r) (succ r)) n = b) (low : Nat.ble (mul r r) n = true) : Nat.ble (mul (match b with | true => succ r | false => r) (match b with | true => succ r | false => r)) n = true

The step keeps the lower bound: either the candidate fits, or the doubled root does.

Nat.sqrtFuelSquareLe

Section titled “Nat.sqrtFuelSquareLe”
def Nat.sqrtFuelSquareLe (fuel : Nat) (n : Nat) : Nat.ble (mul (Nat.sqrtFuel fuel n) (Nat.sqrtFuel fuel n)) n = true

The fueled square root never overshoots: s * s <= n.

Nat.bleSuccOfBlt

Section titled “Nat.bleSuccOfBlt”
def Nat.bleSuccOfBlt (a : Nat) (b : Nat) : Nat.blt a b = true -> Nat.ble (succ a) b = true

Strictly below means one more is at most: a < b gives a + 1 <= b.

Nat.bleOfMulFourBleSucc

Section titled “Nat.bleOfMulFourBleSucc”
def Nat.bleOfMulFourBleSucc (q : Nat) (m : Nat) : Nat.ble (mul q 4) (succ m) = true -> Nat.ble q m = true

Four times q at most m + 1 gives q at most m.

Nat.quarterBleFuel

Section titled “Nat.quarterBleFuel”
def Nat.quarterBleFuel (m : Nat) (f : Nat) (h : Nat.ble m f = true) : Nat.ble (Nat.div (succ m) 4) f = true

The quarter of a positive number within the fuel fits the remaining fuel.

Nat.bltMulFourSuccQuarter

Section titled “Nat.bltMulFourSuccQuarter”
def Nat.bltMulFourSuccQuarter (n : Nat) : Nat.blt n (mul 4 (succ (Nat.div n 4))) = true

A number is below four times one more than its quarter: n < 4 * (n / 4 + 1).

Nat.ltSuccSqrtStepSquareAt

Section titled “Nat.ltSuccSqrtStepSquareAt”
def Nat.ltSuccSqrtStepSquareAt (n : Nat) (r : Nat) (b : Bool) (e : Nat.ble (mul (succ r) (succ r)) n = b) (top : Nat.blt n (mul (succ (succ r)) (succ (succ r))) = true) : Nat.blt n (mul (succ (match b with | true => succ r | false => r)) (succ (match b with | true => succ r | false => r))) = true

The step keeps the upper bound: either the candidate fits and the next one does not, or it does not fit.

Nat.ltSuccSuccSqrtDoubleSquare

Section titled “Nat.ltSuccSuccSqrtDoubleSquare”
def Nat.ltSuccSuccSqrtDoubleSquare (n : Nat) (r0 : Nat) (h : Nat.blt (Nat.div n 4) (mul (succ r0) (succ r0)) = true) : Nat.blt n (mul (succ (succ (mul 2 r0))) (succ (succ (mul 2 r0)))) = true

Twice the root of the quarter, plus two, squares above n.

Nat.ltSuccSqrtFuelSquare

Section titled “Nat.ltSuccSqrtFuelSquare”
def Nat.ltSuccSqrtFuelSquare (fuel : Nat) (n : Nat) : Nat.ble n fuel = true -> Nat.blt n (mul (succ (Nat.sqrtFuel fuel n)) (succ (Nat.sqrtFuel fuel n))) = true

The fueled square root is the largest such: n < (s + 1) * (s + 1), while n is within the fuel.

Nat.sqrtDigitsSquareLe

Section titled “Nat.sqrtDigitsSquareLe”
def Nat.sqrtDigitsSquareLe (n : Nat) : Nat.ble (mul (Nat.sqrtDigits n) (Nat.sqrtDigits n)) n = true

The digit-by-digit square root does not overshoot.

Nat.ltSuccSqrtDigitsSquare

Section titled “Nat.ltSuccSqrtDigitsSquare”
def Nat.ltSuccSqrtDigitsSquare (n : Nat) : Nat.blt n (mul (succ (Nat.sqrtDigits n)) (succ (Nat.sqrtDigits n))) = true

The digit-by-digit square root is the largest such.

Nat.sqrtNewtonGo

Section titled “Nat.sqrtNewtonGo”
def Nat.sqrtNewtonGo (n : Nat) (x : Nat) (fuel : Nat) : Nat

Newton’s method for the square root from a start above the root; fuel bounds the iterations.

Nat.sqrtNewton

Section titled “Nat.sqrtNewton”
def Nat.sqrtNewton (n : Nat) : Nat

A fast guess for the square root: Newton’s method from 2 to the half bit length (a few iterations).

Nat.isSqrtOf

Section titled “Nat.isSqrtOf”
def Nat.isSqrtOf (n : Nat) (r : Nat) : Bool

Whether r is the integer square root of n: r * r <= n < (r + 1) * (r + 1).

Nat.sqrt

Section titled “Nat.sqrt”
def Nat.sqrt (n : Nat) : Nat

The integer square root: the largest s with s * s <= n. Runs Newton’s method and checks the answer; the digit-by-digit version is the fallback, so the specification holds without proving that Newton converges.

Nat.sqrtChecked

Section titled “Nat.sqrtChecked”
def Nat.sqrtChecked (n : Nat) (r : Nat) : Nat

The candidate r when it is the square root of n, otherwise the digit-by-digit answer.

Nat.sqrtSquareLeAt

Section titled “Nat.sqrtSquareLeAt”
def Nat.sqrtSquareLeAt (n : Nat) (r : Nat) (b : Bool) (e : Nat.isSqrtOf n r = b) : Nat.ble (mul (match b with | true => r | false => Nat.sqrtDigits n) (match b with | true => r | false => Nat.sqrtDigits n)) n = true

The checked answer does not overshoot, whichever way the check went.

Nat.ltSuccSqrtSquareAt

Section titled “Nat.ltSuccSqrtSquareAt”
def Nat.ltSuccSqrtSquareAt (n : Nat) (r : Nat) (b : Bool) (e : Nat.isSqrtOf n r = b) : Nat.blt n (mul (succ (match b with | true => r | false => Nat.sqrtDigits n)) (succ (match b with | true => r | false => Nat.sqrtDigits n))) = true

The checked answer is the largest such, whichever way the check went.

Nat.sqrtSquareLe

Section titled “Nat.sqrtSquareLe”
def Nat.sqrtSquareLe (n : Nat) : Nat.ble (mul (Nat.sqrt n) (Nat.sqrt n)) n = true

The square root does not overshoot: sqrt n * sqrt n <= n.

Nat.ltSuccSqrtSquare

Section titled “Nat.ltSuccSqrtSquare”
def Nat.ltSuccSqrtSquare (n : Nat) : Nat.blt n (mul (succ (Nat.sqrt n)) (succ (Nat.sqrt n))) = true

The square root is the largest such: n < (sqrt n + 1) * (sqrt n + 1).

Nat.bitLengthFuel

Section titled “Nat.bitLengthFuel”
def Nat.bitLengthFuel (fuel : Nat) (n : Nat) : Nat

The number of binary digits, counting from the highest set bit; with fuel bounding the depth, stops at zero.

Nat.bitLength

Section titled “Nat.bitLength”
def Nat.bitLength (n : Nat) : Nat

The number of binary digits of n (zero has none).

Nat.bltZeroFalse

Section titled “Nat.bltZeroFalse”
def Nat.bltZeroFalse (m : Nat) : Nat.blt m zero = false

Nothing is below zero, as a boolean: m < 0 is false.

Nat.halveStep

Section titled “Nat.halveStep”
def Nat.halveStep (fuel : Nat) (q : Nat) (m : Nat) (b : Bool) : Nat

One step of halving: the division loop at m + 2 with m < 2 decided by b.

Nat.halveDoubleAux

Section titled “Nat.halveDoubleAux”
def Nat.halveDoubleAux (p : Nat) (fuel : Nat) (q : Nat) : Nat.ble (succ p) fuel = true -> Nat.divAuxFuel fuel q (add p p) 2 = add q p

The halving loop on p + p with enough fuel returns q + p.

Nat.bleSuccSuccAdd

Section titled “Nat.bleSuccSuccAdd”
def Nat.bleSuccSuccAdd (p : Nat) (r : Nat) : Nat.ble (succ p) (succ (add p r)) = true

One more than p is at most one more than p plus anything.

Nat.halfDouble

Section titled “Nat.halfDouble”
def Nat.halfDouble (p : Nat) : Nat.div (add p p) 2 = p

Half of a double is the number: (p + p) / 2 = p.

Nat.halfPowTwo

Section titled “Nat.halfPowTwo”
def Nat.halfPowTwo (k : Nat) : Nat.div (Nat.pow 2 (succ k)) 2 = Nat.pow 2 k

Half of a power of two is the next lower power: 2^(k+1) / 2 = 2^k.

Nat.bltSubOfBltAdd

Section titled “Nat.bltSubOfBltAdd”
def Nat.bltSubOfBltAdd (p : Nat) (q : Nat) (i : Nat) : Nat.blt i (add p q) = true -> Nat.blt i p = false -> Nat.blt (sub i p) q = true

Past the first part of a sum, the rest is below the second part: i < p + q and not i < p give i - p < q.

Nat.bltDoubleOfBltPowSucc

Section titled “Nat.bltDoubleOfBltPowSucc”
def Nat.bltDoubleOfBltPowSucc (k : Nat) (i : Nat) (h : Nat.blt i (Nat.pow 2 (succ k)) = true) : Nat.blt i (add (Nat.pow 2 k) (Nat.pow 2 k)) = true

Below the next power of two means below twice this one: i < 2^(k+1) gives i < 2^k + 2^k.

Nat.bltSelfAddOfPos

Section titled “Nat.bltSelfAddOfPos”
def Nat.bltSelfAddOfPos (p : Nat) (q : Nat) (h : Nat.blt zero q = true) : Nat.blt p (add p q) = true

A number is below itself plus something positive.

Nat.bleBltTrans

Section titled “Nat.bleBltTrans”
def Nat.bleBltTrans (a : Nat) (b : Nat) (c : Nat) (h1 : Nat.ble a b = true) (h2 : Nat.blt b c = true) : Nat.blt a c = true

An order followed by a strict order is strict: a <= b < c gives a < c.