PeanoScript reference

This is a reference page/cheat sheet for PeanoScript, the TypeScript-like theorem prover. For an in-depth explanation, see the tutorial.

Axioms

The following functions are built in (with implementations):

Assignment

Permanently assigns a value to a name. Optionally uses a type annotation.

Arithmetic

Arithmetic expressions are built from 0, natural number variables introduced as function arguments, and the operationssucc(a), a * b, a + b. Arabic numerals can be used as syntax sugar, for example 2 is the same as succ(succ(0)).

The type of an arithmetic expression looks the same as the expression.

Equality

Given arithmetic expressions A and B, A == B is a type.

Given arithmetic expressions A, B, C, terms eqAB : A == B and eqBC : B == C, and f a function that returns arithmetic expressions:

• eqAB.symm() is of type B == A.
• eqAB.trans(eqBC) is of type A == C.
• eqAB.map(f) is of type f(A) == f(B).

Functions

Functions follow the TypeScript syntax, including function types, arrow functions, and function statements, but not including function expressions.

Functions are automatically curried, so (a: T, b: T) => e desugars to (a: T) => (b: T) => e and f(a, b) desugars to f(a)(b).

Function parameters can have a proposition type or the type N. The latter case introduces a new natural number variable, the return type of the function can use this variable.

For loop

The for loop expression is how PeanoScript does induction. It has the following syntax*:

Where:

1. i and acc are identifiers.
2. accType is a type that might depend on i.
3. base, bound, and updatedAcc are expressions.

We will use the notation expr[var:=val] for the expression expr but with all instances of the name var replaced with val. A for loop is well-typed if:

1. base is of type accType[i:=0].
2. bound is an arithmetic expression.
3. Given the context of the for loop with the added variables i (natural number) and acc: accType, the type of updatedAccis accType[i:=succ(i)].

In this case, the type of the for expression is accType[i:=bound].

If there is no type annotation on acc, but the for expression has a required type retType and bound is a variable, accType will be guessed as retType[bound:=i]

(*): The continue statement can also be inside a match statement.

And types (&&)

Given types A and B, A && B is a type. Given terms a : A and b : B, a && b has type A && B. Given a term ab: A && B, ab.left has type A and ab.right has type B.

Exists types

An exists type is written {x: N; prop: T} where x and prop are identifiers, and T is a type that may depend on x.

A value of this type can be created as {x: NumExpr, prop: PropExpr} where NumExpr is an arithmetic expression and PropExpr is of type T[x:=NumExpr].

Hack note: while the property names in an Exists type are meaningful for interpreting object expressions and destructuring assignment, the compiler will accept a conversion between Exists types as long as they're logically equivalent. That is, the second property's name doesn't matter and the first property can be renamed. Without this feature, it would be difficult to work with generic Exists types, as the property names sometimes need to be renamed in a nested generic to not shadow generic parameters.

Destructuring assignment

To use a value of an exists type, we use destructuring assignment. We can optionally rename one or both of the properties using from: to syntax.

Or types (||)

Given types A and B, A || B is a type. Given a: A and b: B we can create a value of type A || B as{left: a} or {right: b}.

Match statement/expression

A match expression is written:

Where:

1. l and r are identifiers.
2. aOrB, leftReturn, and rightReturn are expressions.

It's well-typed if:

1. aOrB has type A || B
2. There is a type R such that:
• Given l: A in the context, leftReturn has type R.
• Given r: B in the context, rightReturn has type R.

Then the type of the match expression is R.

Match can also be used as a statement. Then it's basically equivalent to a return/continue/break statement with a match expression as the value, except that instead of ending cases with break, we end them with return/continue/break respectively.

Type "never"

never is a type representing logical contradiction. Given x: never, neverElim<T>(x) has type T. The generic argument can also be inferred.

Type definitions

You can define a shorthand for a type like in TypeScript:

Generic types

Defined types can take zero or more generic arguments. These have to be declared as either extends N for arithmetic expression arguments or extends Prop for proposition type arguments.

Operator "as"

Given an expression expr and a type T, expr as T has type T if exprcan be interpreted as type T. This is the same as type annotations, but can be used in expression context.

Magic built-ins

The following compiler magic is available:

1. For a type T, the expression excludedMiddle<T> has type T || !T.
2. The placeholder value sorry has type any. This type can be converted into anything.
3. For eq: A == B, ring(eq) has type rung<A == B>. This type can be converted to C == D if A - B equals C - D or D - C, considering them as polynomials.
4. For prop: T and eq: x == B where x is a variable and Bis an expression, replaceAll(prop, eq) has type T[x:=B].
5. If GT is the name of a generic type with a single argument of kind N, replace<GT> has type (L: N, R: N, eqLR: L == R, propOfL: GT<L>) => GT<R>.