Declarations and modules

You write statements and proofs as Clojure data. rainbow.elaborate turns that data into kernel terms, and the kernel checks them. The examples come from rainbow.algorithms.proofs.ahof.accuracy (source, reference). It defines classification accuracy as correct predictions divided by the total and proves two worked instances.

Write a spec

accuracy/accuracy takes two non-negative rationals and divides the first by the second (line 57):

(def nnrat (function/const* 'nnrat/NonnegativeRational []))

;; accuracy correct total = correct / total
(def accuracy-spec
  {:name 'accuracy/accuracy :kind :definition :universes []
   :type (function/arrow nnrat nnrat nnrat)
   :value (function/lam [['correct nnrat] ['total nnrat]]
                        (nnrat-divide 'correct 'total))})

(def definition-specs [accuracy-spec])

function/arrow, function/lam and function/const* come from rainbow.math.logic.function and return plain vectors: (function/arrow nnrat nnrat nnrat) is [:-> nnrat nnrat nnrat]. Terms and binders lists every helper.

A theorem has the same shape without :kind. :type is the statement and :value its proof:

;; 3 correct of 4 -> accuracy 3/4.
(def accuracy-example-spec
  {:name 'accuracy/accuracy-example :universes []
   :type (nnrat-equivalent (accuracy (whole 3) (whole 4)) (fraction 3 3))
   :value (equivalent-proof (accuracy (whole 3) (whole 4)) (fraction 3 3))})

(def theorem-specs [accuracy-example-spec perfect-classifier-accuracy-one-spec])

fraction calls nnrat/make, which takes the numerator and the denominator minus one, so (fraction 3 3) is 3/4 and (whole 4) is 4/1. nnrat/equivalent compares two fractions by cross-multiplication. equivalent-proof applies equality/reflexive to one side of that equation, and the kernel accepts it because both sides reduce to the same natural number.

nnrat-divide, accuracy, whole and fraction are private functions that return vectors. Build statements with any Clojure you like. Only the returned data reaches the kernel.

From spec to declaration

A module passes its specs to rainbow.math.milestone-support/extend-with, which calls add-spec on each one (source). add-spec elaborates :type and :value with rainbow.elaborate/core-expression and builds the kernel’s declaration map:

(kernel/add-declaration
 checked-environment
 {:rainbow/kind (if definition? :definition :theorem)
  :rainbow/aliases #{(:name spec)}
  :rainbow/universes (:universes spec)
  :rainbow/type type :rainbow/value value
  :rainbow/transparency (if definition? :reducible :opaque)
  :rainbow/dependencies (into (term/constants type)
                              (term/constants value))
  :rainbow/provenance {:origin :native :producer producer}
  :rainbow/schema-version 1})

If the elaborator or the kernel rejects a spec, add-spec throws an ex-info with the rejected result and the install stops.

kernel/add-declaration (source) is the only way into an environment. Besides the values above, :rainbow/kind can be :axiom (with a nil value) and :rainbow/transparency can be :semireducible. Missing keys default to no universes, no value, :opaque, no dependencies, no aliases and schema 1. The kinds :inductive, :constructor and :recursor come only from add-inductive-block (see Inductive types).

It checks the declaration against the rules in The calculus (validate-declaration!, source), computes its axioms and its id, and returns {:status :accepted :declaration ... :environment ...} or {:status :rejected :error ... :message ...}. The :error has an :error/category such as :kernel/type-mismatch or :kernel/dependency-mismatch. Your input environment stays as it was. You get a new one back.

The id is the SHA-256 hash of the canonical encoding of the map except aliases and provenance (environment/declaration-id, source), for example "sha256:a5d13ae2...". Terms refer to constants by this id. A second alias for the same content joins the existing declaration, and an alias already taken by a different id fails with :kernel/alias-conflict. More in Content addressing.

Transparency and axioms

The kernel unfolds :reducible and :semireducible constants when it compares terms, and never unfolds :opaque ones. add-spec makes definitions :reducible and theorems :opaque, so a definition computes and a theorem is used only through its type. The accuracy theorems go through by reflexivity because accuracy/accuracy, nnrat/divide and nnrat/equivalent unfold down to arithmetic on natural numbers.

An axiom has :rainbow/kind :axiom and no value. kernel/axioms returns the axioms a declaration depends on, directly or through others, for an id or an alias. The open core declares excluded middle, propositional extensionality, proof irrelevance, function extensionality and choice as axioms in rainbow.math.profile (source). The accuracy theorems use none.

The module around the specs

The rest of the module is the same in every proof module (line 83):

(def deps
  "Modules this one installs on top of (see rainbow.module)."
  '[rainbow.math.rational.division])

(defn install
  "Adds this module's own declarations."
  [checked-environment]
  (-> checked-environment (support/extend-with :ahof-accuracy (concat definition-specs theorem-specs))))

(defn extend-environment [checked-environment]
  (module/install-module checked-environment 'rainbow.algorithms.proofs.ahof.accuracy))
(defn definition-ids [checked-environment]
  (support/spec-ids checked-environment definition-specs))

(defn theorem-ids [checked-environment]
  (support/spec-ids checked-environment theorem-specs))

Definitions go before theorems in the install because the theorems use them. deps lists the modules this one refers to. install adds only this module’s declarations, with :ahof-accuracy in their provenance. Callers use extend-environment, which goes through rainbow.module/install-module (source) and installs each dependency once, before the module. definition-ids and theorem-ids map spec names to content ids. Forget an entry in deps and the kernel rejects the first declaration that names the missing constant. Modules covers the rest.

Check it

lein verify rainbow.algorithms.proofs.ahof.accuracy

lein verify installs the module through the kernel, re-checks both theorems and prints each one’s scope (for all inputs, definitional unfolding or worked instance) and its axioms. For this module: 2 worked instances, statements about specific values.