Generics

We've deployed a new version of the Acorn Prover, 0.0.5, with support for a commonly requested feature: generic types. For example, the standard library now has a Pair structure:

structure Pair<T, U> {
    first: T
    second: U
}

Generics allow defining functions, structures, or theorems with placeholders for types, so that proofs can be reused while maintaining type safety. Instead of specifying a concrete type, generics use type parameters that can be substituted with actual types when used.

Structures, function definitions, and theorems can all be expressed generically:

structure LatticePoint<T> {
    x: T
    y: T
}

class LatticePoint<T> {
    define swap(self) -> LatticePoint<T> {
        LatticePoint.new(self.y, self.x)
    }

    define on_main_diagonal(self) -> Bool {
        self.x = self.y
    }
}

theorem swap_is_involutive<T>(p: LatticePoint<T>) {
    p.swap.swap = p
} by {
    p.swap.x = p.y
    p.swap.y = p.x
}

define colinear<T>(a: LatticePoint<T>,
                   b: LatticePoint<T>) -> Bool {
    a.x = b.x or a.y = b.y
}

theorem swap_colinear_imp_main<T>(a: LatticePoint<T>) {
    colinear(a, a.swap) implies a.on_main_diagonal
} by {
    if a.x = a.swap.x {
        a.on_main_diagonal
    } else {
        a.y = a.swap.y
        a.on_main_diagonal
    }
}

We've updated the standard library to use generics where appropriate. If you have the Acorn Prover VS Code extension installed, updating your extension will automatically get you support for generics. Give it a try and let us know in Discord if you have any questions!