Writing theorems

The theorem keyword

theorem is syntactically identical to fn. It declares that the signature is a proposition and the body its proof:

theorem zero_eq_zero() -> Eq<Nat, 0, 0> {
    refl
}

The difference is one of intent rather than mechanism — a fn returning a proof would be checked exactly the same way. Use theorem when the point of the declaration is the claim rather than the value, so a reader can tell at a glance which is which.

Proof by exhaustive checking

Where a type has few enough values, you can prove a property by checking every one. For Bool, with two values, this is a complete proof rather than a sampling:

pub fn not(x: Bool) -> Bool {
    if x { false } else { true }
}

pub fn and(a: Bool, b: Bool) -> Bool {
    if a { b } else { false }
}

// not is self-inverse — both cases checked, so this is exhaustive.
theorem double_negation() -> Bool {
    not(not(true)) == true && not(not(false)) == false
}

This technique carries the boolean algebra proofs in examples/proofs_boolean.tg — De Morgan’s laws, distributivity, associativity — and it is honest, because enumerating both booleans really does settle a claim about all booleans.

Be clear about what it does not do. The proposition proved is double_negation() -> Bool: that the body evaluates to a Bool. That the body happens to be a conjunction of true things is checked by evaluation, not recorded in the type. Compare with Eq<Nat, 2 + 2, 4>, where the claim is in the signature and the checker verifies it.

The distinction matters at the point where the technique stops scaling.

Where it stops

Nat has no small set of values, so exhaustive checking cannot prove anything about all naturals. What the examples do instead is verify small cases:

// From examples/proofs_natural.tg — Peano naturals, since Nat is built in.
pub type Peano = Zero | Succ(Peano)

pub fn add(m: Peano, n: Peano) -> Peano {
    match m {
        Zero => n,
        Succ(pred) => Succ(add(pred, n)),
    }
}

// Verifies commutativity for particular small values — not for all Peano.
fn test_add_commutative() -> Bool {
    nat_eq(add(one(), two()), add(two(), one())) &&
    nat_eq(add(two(), three()), add(three(), two()))
}

nat_eq, defined in the same file, takes both arguments apart at once, so it carries #[decreasing(m)] to tell the termination checker which one to measure — see Recursion the compiler can see ends.

Calling this a proof of commutativity would be wrong, and the examples do not: it is a test with a proof-shaped signature. A statement about every natural needs induction, which is the next page.

Honest positioning

Albite’s proof surface is real and small. Propositional equality, the combinators, and induction over naturals are available as terms, and since 2.0-beta a small tactic language — induction, cases, rewrite, bounded simp, ring, omega — builds those terms step by step. Every proof, however it was written, is re-checked by the kernel. It is far from the libraries a Lean user expects; see the 2.0-beta release notes.