Number Theory

Proving properties of integer arithmetic — the kind of reasoning that underlies correct numerical algorithms.

import logos
import logos.tactics as t

Basic Identities

Let’s build a small library of arithmetic identities, each proved formally.

x, y, z = logos.vars("x y z", int)

# Commutativity
@logos.theorem
def add_comm(x: int, y: int):
    return x + y == y + x

@logos.theorem
def mul_comm(x: int, y: int):
    return x * y == y * x

# Associativity
@logos.theorem
def add_assoc(x: int, y: int, z: int):
    return (x + y) + z == x + (y + z)

@logos.theorem
def mul_assoc(x: int, y: int, z: int):
    return (x * y) * z == x * (y * z)

# Distributivity
@logos.theorem
def distrib(x: int, y: int, z: int):
    return x * (y + z) == x * y + x * z

logos.check(add_comm.proof(t.intro("x", "y"), t.ring()))
logos.check(mul_comm.proof(t.intro("x", "y"), t.ring()))
logos.check(add_assoc.proof(t.intro("x", "y", "z"), t.ring()))
logos.check(mul_assoc.proof(t.intro("x", "y", "z"), t.ring()))
logos.check(distrib.proof(t.intro("x", "y", "z"), t.ring()))

print("Core arithmetic library: ✓")
Core arithmetic library: ✓

Parity

@logos.define
def double(n: int):
    return n + n

# double(n) = 2*n
@logos.theorem
def double_is_2n(n: int):
    return double(n) == logos.lit(2) * n

logos.check(double_is_2n.proof(t.intro("n"), t.unfold(double), t.ring()))
print("double(n) = 2n ✓")

# double is non-negative for non-negative inputs
@logos.theorem
def double_nonneg(n: int):
    return (n >= logos.lit(0)) >> (double(n) >= logos.lit(0))

logos.check(double_nonneg.proof(t.intro("n", "h"), t.unfold(double), t.linarith()))
print("n ≥ 0 → double(n) ≥ 0 ✓")

# double of a sum: double(x + y) = double(x) + double(y)
@logos.theorem
def double_additive(x: int, y: int):
    return double(x + y) == double(x) + double(y)

logos.check(double_additive.proof(t.intro("x", "y"), t.unfold(double), t.ring()))
print("double(x + y) = double(x) + double(y) ✓")
double(n) = 2n ✓
n ≥ 0 → double(n) ≥ 0 ✓
double(x + y) = double(x) + double(y) ✓

Difference of Squares

A classic identity used in factoring and cryptography:

@logos.define
def square(n: int):
    return n * n

@logos.theorem
def diff_of_squares(a: int, b: int):
    return (a + b) * (a - b) == square(a) - square(b)

logos.check(diff_of_squares.proof(t.intro("a", "b"), t.unfold(square), t.ring()))
print("(a+b)(a-b) = a² - b² ✓")

@logos.theorem
def square_of_sum(a: int, b: int):
    return square(a + b) == square(a) + logos.lit(2)*a*b + square(b)

logos.check(square_of_sum.proof(t.intro("a", "b"), t.unfold(square), t.ring()))
print("(a+b)² = a² + 2ab + b² ✓")
(a+b)(a-b) = a² - b² ✓
(a+b)² = a² + 2ab + b² ✓

Linear Inequalities

Reasoning about bounds — essential for algorithm correctness:

x, y = logos.vars("x y", int)

# Additive monotonicity
@logos.theorem
def add_mono(x: int, y: int, z: int):
    return (x <= y) >> (x + z <= y + z)

logos.check(add_mono.proof(t.intro("x", "y", "z", "h"), t.linarith()))
print("x ≤ y → x+z ≤ y+z ✓")

# Transitivity
@logos.theorem
def lt_trans(x: int, y: int, z: int):
    return (x < y) >> ((y < z) >> (x < z))

logos.check(lt_trans.proof(t.intro("x", "y", "z", "hxy", "hyz"), t.linarith()))
print("x < y ∧ y < z → x < z ✓")

# Sum of non-positives is non-positive
@logos.theorem
def neg_add_neg(x: int, y: int):
    return (x <= logos.lit(0)) >> ((y <= logos.lit(0)) >> (x + y <= logos.lit(0)))

logos.check(neg_add_neg.proof(t.intro("x", "y", "hx", "hy"), t.linarith()))
print("x ≤ 0 ∧ y ≤ 0 → x + y ≤ 0 ✓")
x ≤ y → x+z ≤ y+z ✓
x < y ∧ y < z → x < z ✓
x ≤ 0 ∧ y ≤ 0 → x + y ≤ 0 ✓

Triangle Inequality

Proving |a + b| ≤ |a| + |b| requires case analysis. Here’s a simplified version for non-negatives:

# For non-negative integers: (a + b) ≤ (a + b) — trivial base case
# Full triangle inequality needs case splits; here we show the setup:

@logos.theorem
def abs_nonneg(n: int):
    return (n >= logos.lit(0)) >> (n >= logos.lit(0))

logos.check(abs_nonneg.proof(t.intro("n", "h"), t.assumption()))
print("n ≥ 0 → n ≥ 0 (trivial, shows case intro works) ✓")
n ≥ 0 → n ≥ 0 (trivial, shows case intro works) ✓

Arithmetic Progressions

Sum of first n natural numbers using Gauss’s formula (as an axiom — logos doesn’t have induction in v0.2):

# Declare gauss_sum as an external function and axiomatize it
gauss_sum = logos.extern("gauss_sum", [int], int)

n = logos.var("n", int)

# Axiom: gauss_sum(n) * 2 = n * (n + 1)
@logos.axiom
def gauss_formula(n: int):
    return gauss_sum(n) * logos.lit(2) == n * (n + logos.lit(1))

# Use the axiom: from it and n > 0, we can derive gauss_sum(n) * 2 == n*(n+1)
# Here we show applying the axiom in a forall proof
logos.check(logos.prove(
    logos.forall(int, lambda n: gauss_sum(n) * logos.lit(2) == n * (n + logos.lit(1))),
    [t.intro("n"), t.apply(gauss_formula)],
))
print("gauss_sum(n) * 2 = n*(n+1) ✓")
gauss_sum(n) * 2 = n*(n+1) ✓

Modular Arithmetic

# Basic mod property: (a * b) mod m = ((a mod m) * (b mod m)) mod m
# We'll prove a specific case

logos.check(logos.prove(
    logos.lit(7) * logos.lit(8) % logos.lit(5) == (logos.lit(7) % logos.lit(5)) * (logos.lit(8) % logos.lit(5)) % logos.lit(5),
    [t.norm_num()],
))
print("(7 * 8) mod 5 = (7 mod 5)(8 mod 5) mod 5 ✓")
(7 * 8) mod 5 = (7 mod 5)(8 mod 5) mod 5 ✓