Verify a module

Re-check two corpus modules in one run and find out which axioms they use. Two theorems in rainbow.math.finite.set-union use classical axioms; rainbow.algorithms.proofs.ahof.christofides has worked instances. Run the commands from the root of a v1.4.1 clone (see Install).

Verify

lein verify rainbow.math.finite.set-union rainbow.algorithms.proofs.ahof.christofides; echo $?

checkpoint artifacts/ahof/d63-eligibility-traces/checkpoint.edn.gz replayed
OK    rainbow.math.finite.set-union (5 theorems: 5 for all inputs, 0 definitional unfoldings, 0 worked instances)
       checked   for-all   set/finite-singleton-equivalence  axiom-free
       checked   for-all   set/finite-singleton-proposition-equality  axioms: ("sha256:b3f5d5a15f123b8edd7a1003cd1d1122dde6d8476e8b905d58034f999a1c3088")
       checked   for-all   set/infinite-indexed-union-member  axiom-free
       checked   for-all   set/infinite-indexed-union2-member  axiom-free
       checked   for-all   set/infinite-union-equivalence  axioms: ("sha256:2756c280e97f5c73b7f8ed1cdae9b3e0f2871720be7d82785b6b81ef1fb84366")
OK    rainbow.algorithms.proofs.ahof.christofides (3 theorems: 0 for all inputs, 0 definitional unfoldings, 3 worked instances)
       checked   instance  christofides/tour-at-most-bound  axiom-free
       checked   instance  christofides/tour-over-bound-rejected  axiom-free
       checked   instance  christofides/tour-within-guarantee  axiom-free
0

About 20 seconds, mostly the checkpoint replay. It runs once however many namespaces you name, so name them all in one command.

Read the result

The first line says the base checkpoint replayed through the kernel. If it does not, the command prints FAIL checkpoint ... did not replay and stops.

OK means the module installed, named at least one theorem, and every theorem checked. On a theorem line, checked means the kernel accepted the proof once more; any other status fails the module. The scope is for-all when the statement quantifies over data, unfolding when it does but the proof is reflexivity, and instance for specific values. christofides/tour-at-most-bound states 13 <= 15 for one tour, not the algorithm’s 3/2 guarantee (What “proved” means). The last column is axiom-free or the content ids of the axioms the kernel found.

The exit code is 0 when every namespace is OK and 1 otherwise, so the command works as a CI gate. A module that does not install prints FAIL, the namespace and the reason; Prove a lemma about rationals shows how to get the kernel’s own reason.

Name the axioms

Resolve the aliases you suspect in the default checkpoint. Save this as /tmp/axiom-ids.clj:

(require '[rainbow.checkpoint :as checkpoint]
         '[rainbow.environment :as environment]
         '[rainbow.main :as main])
(let [env (:environment (checkpoint/load-checkpoint main/default-checkpoint))]
  (doseq [alias '[logic/excluded-middle logic/proposition-extensionality]]
    (println alias (environment/resolve-id env alias))))

lein run -m clojure.main /tmp/axiom-ids.clj

logic/excluded-middle sha256:2756c280e97f5c73b7f8ed1cdae9b3e0f2871720be7d82785b6b81ef1fb84366
logic/proposition-extensionality sha256:b3f5d5a15f123b8edd7a1003cd1d1122dde6d8476e8b905d58034f999a1c3088

So set/infinite-union-equivalence uses excluded middle and set/finite-singleton-proposition-equality uses propositional extensionality. lein show prints an axiom’s statement:

lein show logic/excluded-middle

logic/excluded-middle :
  (x₁ : Prop)
  → proposition/disjunction x₁ (x₁ → proposition/falsity)
  -- binder names: generated

According to doc/claims.md, the theorems in set_union.clj and set_boundary.clj are the only eight in the corpus that depend on an axiom. A logical principle enters Rainbow only as an explicit axiom declaration, so the kernel can always list it.

Next

• Commands: lein verify options, including --checkpoint
• What “proved” means, The trusted base
• Reference: rainbow.math.finite.set-union, rainbow.algorithms.proofs.ahof.christofides