lean-rational

A pure, dependency-free Lean 4 library for exact rational arithmetic with machine-checked field axiom proofs.

Headline Theorems

All proven sorry-free with axioms [propext, Classical.choice, Quot.sound] only.

Theorem	Statement
add_comm	equiv (add a b) (add b a)
add_zero	equiv (add a zero) a
add_neg	equiv (add a (neg a)) zero
mul_comm	equiv (mul a b) (mul b a)
mul_one	equiv (mul a one) a
zero_ne_one	¬equiv zero one

API

import Rational.Defs
open Rational

-- Construction
def half  : Rat := reduce 1 2 (by omega)  -- 1/2
def third : Rat := reduce 1 3 (by omega)  -- 1/3

-- Arithmetic
#eval add half third    -- 5/6
#eval mul half third    -- 1/6
#eval neg half          -- -1/2
#eval sub half third    -- 1/6

-- Comparison
#eval eq half (reduce 2 4 (by omega))  -- true (2/4 = 1/2)
#eval le third half                    -- true (1/3 ≤ 1/2)

Demo Output

=== lean-rational Demo ===
1/2           = 1/2
1/3           = 1/3
1/2 + 1/3     = 5/6
1/2 - 1/3     = 1/6
1/2 * 1/3     = 1/6
2 * 1/2       = 1
-(1/2)        = -1/2
1/2 + (-(1/2))= 0
1/2 = 2/4?    = true
1/2 ≤ 1/3?    = false
1/4 ≤ 1/2?    = true

Verified field axioms (Proofs.lean):
  add_comm     : equiv (add a b) (add b a)
  add_zero     : equiv (add a zero) a
  add_neg      : equiv (add a (neg a)) zero
  mul_comm     : equiv (mul a b) (mul b a)
  mul_one      : equiv (mul a one) a
  zero_ne_one  : ¬equiv zero one

Build

# Requires elan (https://github.com/leanprover/elan)
lake build
lake exe test    # all tests green
lake exe demo    # demo output
lake env lean scripts/check_axioms.lean  # axiom audit

Layout

lean-rational/
  lakefile.toml              # build config
  lean-toolchain             # pinned: leanprover/lean4:v4.31.0
  Rational.lean              # root module
  Rational/
    Defs.lean                # data types + pure arithmetic functions
    Spec.lean                # field axiom statements (as Prop)
    Proofs.lean              # sorry-free, axiom-clean proofs
  TestVectors.lean           # #eval reference vectors
  TestMain.lean              # lake exe test driver
  DemoMain.lean              # lake exe demo
  scripts/check_axioms.lean  # #print axioms guard
  .github/workflows/ci.yml   # CI
  LICENSE

Proof Methodology

Rat represents p/q with q > 0. The reduce function normalizes by dividing by gcd. The key lemma reduce_cross proves that reduction preserves the equivalence class (r.num * q = p * r.den), enabling all field axiom proofs via cross-multiplication cancellation.

Equivalence (equiv a b ↔ a.num * b.den = b.num * a.den) is used throughout, following standard fraction equality.

License

MIT