Proof language

The elaborator

rainbow.elaborate (source) is the surface language for terms and types, a “small deterministic surface-to-core elaborator for explicit function propositions”. Inductive blocks use their own syntax, which the kernel compiles (Inductive types). It turns names into de Bruijn indices and aliases into content ids. It sits outside the trusted base, and the kernel checks what it produces.

(type-expression surface) accepts Prop, bound names, :sort, :-> and :forall, enough for statements without constants such as pure logic over Prop. (core-expression environment surface) also accepts :nat, :const, :app, :fn and :let and resolves aliases in the environment. Proof modules built on rainbow.math.milestone-support elaborate every :type and :value with it. Both return :elaborated with the core term, or :rejected with an error:

{:status :elaborated
 :surface surface
 :term    core-term
 :trace   [{:operation :explicit-core-elaboration :input surface}]}  ; :surface-to-core from type-expression

{:status :rejected
 :error   {:error/category ... }
 :message "..."}

Surface forms

surface	core result
`Prop`	`[:sort [:zero]]`
a symbol `x`	`[:bound i]`, where `i` is the position of the nearest binder named `x`
`[:sort level]`	`[:sort level]`
`[:nat n]`	`[:nat n]`, for a natural number `n`
`[:const alias levels]`	`[:const id levels]`. `alias` is a symbol, resolved in the environment, or a string, used unchanged as the id without being looked up or validated.
`[:app f a b ...]`	`[:app [:app f a] b] ...`, at least one argument
`[:-> A B ... Z]`	non-dependent `:pi` from `A` to the arrow of the rest, at least two parts
`[:forall [binding ...] body]`	one `:pi` per binding
`[:fn [binding ...] body]`	one `:lam` per binding
`[:let name type value body]`	`[:let type value body]`, with `name` bound in `body`

A binding is [name type] or [name type mode], with mode :explicit (the default) or :implicit.

Levels are level vectors such as [:param u] or [:succ [:zero]]; a bare symbol u is rejected. A bare symbol in a term is only ever a bound name, never a constant: constants always need [:const ...]. Prop is matched before binder lookup, so a binder named Prop can never be referred to.

An inner binder shadows an outer one with the same name:

(elaborate/core-expression (environment/empty-environment)
                           '[:forall [[x Prop] [x [:-> x x]]] x])
;; :term
[:pi [:sort [:zero]]
     [:pi [:pi [:bound 0] [:bound 1] :explicit] [:bound 0] :explicit]
     :explicit]

The type of the second x refers to the first one, and the body refers to the second. An arrow’s binder has no name, so in [:-> A B] the type B cannot mention the argument. Use :forall when the codomain depends on it.

(elaborate/type-expression '[:forall [[P Prop] [Q Prop]] [:-> P Q P]])
;; :term
[:pi [:sort [:zero]]
     [:pi [:sort [:zero]]
          [:pi [:bound 1] [:pi [:bound 1] [:bound 3] :explicit] :explicit]
          :explicit]
     :explicit]

(elaborate/type-expression '[:forall [[P Prop :implicit]] [:-> P P]])
;; :term
[:pi [:sort [:zero]] [:pi [:bound 0] [:bound 1] :explicit] :implicit]

In the first, P is [:bound 1] under one binder and [:bound 3] under three: Q and the two arrow arguments.

Errors

category	cause
`:elaborate/unknown-name`	a symbol with no binder in scope. The error lists the names in scope.
`:elaborate/unknown-constant`	a symbol alias the environment does not know, or a malformed `:const` form
`:elaborate/invalid-forall`, `:elaborate/invalid-lambda`, `:elaborate/invalid-let`	a malformed binder form, including a binder name that is not a symbol
`:elaborate/invalid-sort`	`[:sort x]` where `x` is not a level
`:elaborate/invalid-literal`	`[:nat n]` where `n` is not a natural number
`:elaborate/arrow-arity`	an arrow with fewer than two parts
`:elaborate/application-arity`	`[:app f]` with no argument
`:elaborate/unsupported-form`	anything else, such as `:app`, `:const` or `:fn` in `type-expression`

(elaborate/type-expression 'y)
;=> {:status :rejected,
;    :error {:name y, :context [], :error/category :elaborate/unknown-name},
;    :message "Unknown surface name"}

You write every argument

The elaborator has no type inference, unification, overloading, notation or holes. :implicit is only a binder annotation, and the kernel requires a lambda’s mode to match its Pi’s. Nothing inserts implicit arguments: you write every argument, universe level and type annotation. An ill-typed term still comes back :elaborated, and the kernel rejects it when you check it.

For abbreviations, write Clojure functions that return surface vectors, such as (defn- accuracy [correct total] ...) in the accuracy module. Terms and binders lists the helpers the corpus shares.