Guides

Prove a lemma about vectors

You will prove that if u ~ v then u + w ~ w + v for vectors, chaining three lemmas from src/rainbow/math/linear/vector/ as equivalence_transitivity.clj does. The module shape is explained in Prove a lemma about rationals.

A vector is a data/List of signed/SignedRational. vector/add stops at the end of the shorter list. vector/equivalent compares values component by component, so vectors of different lengths are not equivalent.

Find the lemmas you need

lein show vector/add-respects-equivalence rainbow.math.linear.vector.add-order
lein show vector/add-commutative rainbow.math.linear.vector.add-order
lein show vector/equivalent-transitive rainbow.math.linear.vector.equivalence-transitivity

vector/add-respects-equivalence :
  (left left-prime right right-prime : List ℚ)
  (left-same : vector/equivalent left left-prime)
  (right-same : vector/equivalent right right-prime)
  → vector/equivalent (vector/add left right) (vector/add left-prime right-prime)
  -- binder names: source
  -- List  data/List
  -- ℚ  signed/SignedRational
vector/add-commutative :
  (left right : List ℚ)
  → vector/equivalent (vector/add left right) (vector/add right left)
  -- binder names: source
  -- List  data/List
  -- ℚ  signed/SignedRational
vector/equivalent-transitive :
  (left middle right : List ℚ) (left-middle : vector/equivalent left middle)
  (middle-right : vector/equivalent middle right)
  → vector/equivalent left right
  -- binder names: source
  -- List  data/List
  -- ℚ  signed/SignedRational

Loading these modules also prints four WARNING: num already refers to: #'clojure.core/num ... lines. They are trimmed here and do not affect the result.

add-respects-equivalence with w ~ w from vector/equivalent-reflexive gives u + w ~ v + w, add-commutative gives v + w ~ w + v, and equivalent-transitive joins them.

Write the module

Save it as test/scratch/vector_add_swap.clj:

(ns scratch.vector-add-swap
  "If u ~ v then u + w ~ w + v, for signed-rational vectors: congruence of
  vector/add, then commutativity, joined by transitivity."
  (:require [rainbow.module :as module]
            [rainbow.math.logic.function :as function]
            [rainbow.math.milestone-support :as support]))

(def type-level [:succ [:zero]])
(def signed (function/const* 'signed/SignedRational []))
(def vector-type (function/app (function/const* 'data/List [type-level]) signed))

(defn- app [f & xs] (apply function/app f xs))
(defn- c [alias] (function/const* alias []))
(defn- vadd [a b] (app (c 'vector/add) a b))
(defn- veq [a b] (app (c 'vector/equivalent) a b))

(def add-swap-of-equivalent-spec
  {:name 'vector/add-swap-of-equivalent :universes []
   :type (function/forall
          [['u vector-type] ['v vector-type] ['w vector-type]
           ['same (veq 'u 'v)]]
          (veq (vadd 'u 'w) (vadd 'w 'v)))
   :value
   (function/lam
    [['u vector-type] ['v vector-type] ['w vector-type]
     ['same (veq 'u 'v)]]
    ;; u+w ~ v+w (congruence), v+w ~ w+v (commutativity), so u+w ~ w+v
    (app (c 'vector/equivalent-transitive)
         (vadd 'u 'w) (vadd 'v 'w) (vadd 'w 'v)
         (app (c 'vector/add-respects-equivalence)
              'u 'v 'w 'w 'same (app (c 'vector/equivalent-reflexive) 'w))
         (app (c 'vector/add-commutative) 'v 'w)))})

(def theorem-specs [add-swap-of-equivalent-spec])

(def deps
  "Modules this one installs on top of (see rainbow.module)."
  '[rainbow.math.linear.vector.add-reorder
    rainbow.math.linear.vector.equivalence-transitivity])

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

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

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

data/List takes a universe level, here [:succ [:zero]], the level of ordinary types. The hypothesis same is a binder like u, v and w, so the statement and the proof both take four arguments.

Verify it

lein verify scratch.vector-add-swap

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

About 55 seconds, with the WARNING lines trimmed.

When a dependency is missing

deps must bring in every declaration your proof names that the checkpoint lacks, and each dependency must find what it needs already installed. Put rainbow.math.linear.vector.equivalence-laws, which defines vector/equivalent-reflexive, first in deps and the module fails:

FAIL  scratch.vector-add-swap -- Milestone expression failed elaboration {:alias vector/equivalent, :error/category :elaborate/unknown-constant}

:elaborate/unknown-constant means the alias is not installed yet: equivalence-laws needs vector/equivalent first. rainbow.math.linear.vector.add-reorder uses vector/equivalent-reflexive itself and brings in what it needs. To fix this error, add to deps the module that installs the named alias, or one that depends on it.

Print the statement

lein show vector/add-swap-of-equivalent scratch.vector-add-swap

vector/add-swap-of-equivalent :
  (u v w : List ℚ) (same : vector/equivalent u v)
  → vector/equivalent (vector/add u w) (vector/add w v)
  -- binder names: source
  -- List  data/List
  -- ℚ  signed/SignedRational