Askar Safin implemented insertion for a simplified red-black tree in Lean 4, a dependently typed theorem prover and programming language. He proved all key properties, including that the output tree remains sorted. This covers the core invariants: no two consecutive red nodes, equal black heights on every path, and binary search tree ordering. Insertion runs in amortized O(log n) time, as expected for red-black trees.
Safin’s code assumes the input tree consists entirely of black nodes, skipping full balancing for deletions or rotations on arbitrary trees. He targets a minimal viable example: one operation, fully verified. The codebase spans about 200 lines, including proofs. Lean 4 checks these proofs mechanically, eliminating human error in verification.
Red-black trees power balanced binary search trees in languages like Java’s TreeMap and Rust’s BTreeMap alternatives. They maintain logarithmic height by coloring nodes red or black and enforcing four invariants during inserts and deletes. Violations trigger rotations and recoloring. Bugs here could degrade performance to O(n) in worst cases, as seen in historical set implementations.
Core Implementation
Safin defines two mutual inductive types: Black for black subtrees (either null or a node with left/right as Node) and Node (black-wrapped black or red with black children).
mutual
inductive Black where
| null : Black
| some (left : Node) (val : Nat) (right : Node) : Black
inductive Node where
| black : Black -> Node
| red (left : Black) (val : Nat) (right : Black) : Node
endThe join function handles three-node cases during insertion, resolving consecutive reds via rotations:
def join (n11 : Node) (n12 : Nat) (n13 : Black) (n2 : Nat) (n3 : Node) : Node :=
match n11 with
| .black n11 => .black (.some (.red n11 n12 n13) n2 n3)
| .red _ _ _ => match n3 with
| .black n3 => .black (.some n11 n12 (.red n13 n2 n3))
| .red n31 n32 n33 => .red (.some n11 n12 (.black n13)) n2 (.some (.black n31) n32 (.black n33))
Insertion recurses down the tree, flips colors, and calls join on reds. It returns a Node, which callers wrap black if needed. The full insert matches on paths for left/right subtrees, handling color cases explicitly. No deletions or searches yet—keeps it under 100 lines of core logic.
Proofs and Limitations
Safin proves insert_sorted: if input is sorted, output is too. This induction spans dozens of cases, matching Lean’s pattern-matching proofs. He also verifies black-height preservation and no-red-parent rules post-insert. Total proofs fill half the repo.
Trade-offs show: assuming all-black inputs dodges delete complexities, where black-height can drop. Full red-black needs 20-30 lemmas for balance. Safin notes insert_sorted grew large—Lean 4’s mathlib offers tactics like simp or rw that could shrink it by 50%, pulling in sorted lemmas.
Repo lives at types.pl/@safinaskar. Run it via lake exe cache get then lake build in Lean 4. Tests insert sequences like 5,3,7 and check outputs.
This matters because formal verification catches subtle bugs unproven code misses. Red-black flaws hit production: Java’s early TreeMap had quadratic inserts under attack. In security, verified structures block side-channels or DoS via imbalance. Crypto libs like libsodium use balanced trees for key stores; Lean proves them immune to adversarial inputs.
For finance, sorted maps underpin order books—O(n) degrades high-frequency trading. Safin’s work proves Lean 4 handles real algos without Rust-like unsafe escapes. Skeptical note: it’s a toy (no deletes, Nat-only keys). Yet it extracts to efficient code via Lean’s compiler. Scale to full trees? Mathlib’s Data.RBTree already does, with 10k+ lines proved. This minimal version teaches why: invariants chain tightly, proofs expose gaps early.
Implication: Teams building secure software—wallets, exchanges—should verify core data structures. Lean lowers the bar versus Coq; extract to C/Rust. Safin invites mathlib tweaks—expect cleaner proofs soon. At 200 lines fully proved, it’s a benchmark for “simple but complete” verification.
