Guides

Prove a lemma about rationals

You will prove b ≤ a + b for non-negative rationals, following the mirror lemma a ≤ a + b in src/rainbow/math/rational/nnrat/add_upper.clj. Run the commands from the root of a v1.4.1 clone.

Find the lemmas you need

To print a lemma, name the module that installs it after the alias:

lein show nnrat/at-most-add-right rainbow.math.rational.nnrat.add-upper

nnrat/at-most-add-right :
  (a b : ℚ≥0)
  → a ≤ a + b
  -- binder names: source
  -- +  nnrat/add
  -- ℚ≥0  nnrat/NonnegativeRational
  -- ≤  nnrat/at-most

Without the module, lein show looks only in the default checkpoint:

lein show nnrat/add-commutative

unknown declaration nnrat/add-commutative -- name the module that installs it

lein show nnrat/add-commutative rainbow.math.rational.nnrat.add-monotone

nnrat/add-commutative :
  (a b : ℚ≥0)
  → a + b = b + a
  -- binder names: source
  -- +  nnrat/add
  -- =  nnrat/equivalent: equality of rational values
  -- ℚ≥0  nnrat/NonnegativeRational

Here = is nnrat/equivalent, equality of values. A lemma in the checkpoint moves ≤ across it:

lein show nnrat/at-most-respects-equivalence

nnrat/at-most-respects-equivalence :
  (x₁ x₂ x₃ x₄ : ℚ≥0)
  (h₁ : x₁ = x₂)
  (h₂ : x₃ = x₄)
  (h₃ : x₂ ≤ x₄)
  → x₁ ≤ x₃
  -- binder names: generated
  -- =  nnrat/equivalent: equality of rational values
  -- ℚ≥0  nnrat/NonnegativeRational
  -- ≤  nnrat/at-most

With x₁ = b, x₂ = b, x₃ = a + b and x₄ = b + a, it turns b = b (nnrat/equivalent-reflexive), a + b = b + a and b ≤ b + a into b ≤ a + b.

Write the module

lein verify has test/ on the classpath. Save the module as test/scratch/nnrat_add_left.clj:

(ns scratch.nnrat-add-left
  "b <= a + b for non-negative rationals, from nnrat/at-most-add-right (b <= b + a)
  and nnrat/add-commutative."
  (:require [rainbow.module :as module]
            [rainbow.math.logic.function :as function]
            [rainbow.math.milestone-support :as support]))

(def nnrat (function/const* 'nnrat/NonnegativeRational []))
(defn- app [f & xs] (apply function/app f xs))
(defn- c [alias] (function/const* alias []))
(defn- radd [a b] (app (c 'nnrat/add) a b))
(defn- rle [a b] (app (c 'nnrat/at-most) a b))

(def at-most-add-left-spec
  {:name 'nnrat/at-most-add-left :universes []
   :type (function/forall [['a nnrat] ['b nnrat]] (rle 'b (radd 'a 'b)))
   :value
   (function/lam
    [['a nnrat] ['b nnrat]]
    ;; b ~ b, a+b ~ b+a, b <= b+a  ==>  b <= a+b
    (app (c 'nnrat/at-most-respects-equivalence)
         'b 'b (radd 'a 'b) (radd 'b 'a)
         (app (c 'nnrat/equivalent-reflexive) 'b)
         (app (c 'nnrat/add-commutative) 'a 'b)
         (app (c 'nnrat/at-most-add-right) 'b 'a)))})

(def theorem-specs [at-most-add-left-spec])

(def deps
  "Modules this one installs on top of (see rainbow.module)."
  '[rainbow.math.rational.nnrat.add-monotone rainbow.math.rational.nnrat.add-upper])

(defn install [env]
  (support/extend-with env :scratch-nnrat-add-left theorem-specs))

(defn extend-environment [env]
  (module/install-module env 'scratch.nnrat-add-left))

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

:type is the statement and :value the proof term: the lemma applied to four values and three proofs. function/forall builds a Pi type, function/lam a function, function/const* a reference by alias.
deps installs the modules for nnrat/add-commutative and nnrat/at-most-add-right. The other two lemmas are in the checkpoint.
install hands the spec to support/extend-with, which elaborates it and calls kernel/add-declaration, where the kernel checks :value against :type.
lein verify calls extend-environment, which installs the dependencies and the module once each, and re-checks the theorems theorem-ids lists.

Verify it

lein verify scratch.nnrat-add-left

checkpoint artifacts/ahof/d63-eligibility-traces/checkpoint.edn.gz replayed
OK    scratch.nnrat-add-left (1 theorems: 1 for all inputs, 0 definitional unfoldings, 0 worked instances)
       checked   for-all   nnrat/at-most-add-left  axiom-free

About 25 seconds. The theorem holds for all inputs and uses no axioms.

Read a rejection

Swap the last lemma’s arguments to 'a 'b and verify again:

checkpoint artifacts/ahof/d63-eligibility-traces/checkpoint.edn.gz replayed
FAIL  scratch.nnrat-add-left -- Milestone declaration rejected #:error{:category :kernel/invalid-declaration-value}

The exit code is 1. To get the kernel’s reason, save this as /tmp/why.clj:

(require '[rainbow.checkpoint :as checkpoint]
         '[rainbow.main :as main]
         'scratch.nnrat-add-left)
(let [env (:environment (checkpoint/load-checkpoint main/default-checkpoint))]
  (try (scratch.nnrat-add-left/extend-environment env)
       (catch Exception e
         (binding [*print-level* 5]
           (prn (-> e ex-data :result :error :cause :error))))))

lein run -m clojure.main /tmp/why.clj

{:expected [:app [:app [:const "sha256:47647b2c8768d200717fbe6fa0133a9b9151aa562ac9acdc7cdec251f6ceb1eb" []] [:bound 0]] [:app [:app [:const "sha256:11694b140ea13ccef3386121702ec9e2483cb1c97cbb9d469e934e6dbe736c77" #] [:bound 0]] [:bound 1]]], :actual [:app [:app [:const "sha256:47647b2c8768d200717fbe6fa0133a9b9151aa562ac9acdc7cdec251f6ceb1eb" []] [:bound 1]] [:app [:app [:const "sha256:11694b140ea13ccef3386121702ec9e2483cb1c97cbb9d469e934e6dbe736c77" #] [:bound 1]] [:bound 0]]], :term [:app [:app [:const "sha256:b25fb63220a954f0e9390a9b068b26520c39599a6172e82708e01a08e16395a2" []] [:bound 1]] [:bound 0]], :error/category :kernel/type-mismatch}

Binders are de Bruijn indices: [:bound 0] is b, the nearest binder, and [:bound 1] is a. Constants are content ids: sha256:47647b… is nnrat/at-most, sha256:11694b… is nnrat/add. So the third proof argument should prove b ≤ b + a and proves a ≤ a + b. # marks parts cut by *print-level*.

Print the statement

lein show nnrat/at-most-add-left scratch.nnrat-add-left

nnrat/at-most-add-left :
  (a b : ℚ≥0)
  → b ≤ a + b
  -- binder names: source
  -- +  nnrat/add
  -- ℚ≥0  nnrat/NonnegativeRational
  -- ≤  nnrat/at-most

binder names: source means the names come from your spec, and elaboration gave exactly the kernel’s type.