The REPL and tactics

Proof modules write proof terms by hand. From a REPL you can build them in steps. rainbow.repl (source) sits over rainbow.proof (proof states), rainbow.tactic (steps) and rainbow.search (automatic search). Tactics are untrusted. They propose pieces of a term, and when the last goal closes, the kernel checks the whole term.

A session

Run lein repl in the repository. Outputs are from v1.4.1.

(require '[rainbow.repl :as repl]
         '[rainbow.tactic :as tactic]
         '[rainbow.environment :as environment])

(def env (environment/empty-environment))

(def started
  (repl/surface-goal env '[:forall [[A [:sort [:param u]]] [x A]] A]
                     {:universes ['u]}))

(:status started)
;=> :ready

(repl/goals (repl/proof-state started))
;=> [#:goal{:id "g-0",
;           :context [],
;           :target [:pi [:sort [:param u]] [:pi [:bound 0] [:bound 1] :explicit] :explicit],
;           :path []}]

The goal asks for an A, given any type A in universe u and any x : A. :universes declares u.

(def s1 (repl/try! (repl/proof-state started) (tactic/intro 'A)))
(def s2 (repl/try! (repl/proof-state s1) (tactic/intro 'x)))

(repl/goals (repl/proof-state s2))
;=> [#:goal{:id "g-2",
;           :context [#:goal{:name x, :type [:bound 0], :mode :explicit}
;                     #:goal{:name A, :type [:sort [:param u]], :mode :explicit}],
;           :target [:bound 1],
;           :path [0 0]}]

Locals are listed innermost first: x is [:bound 0], and A is [:bound 1], the target.

A wrong step fails and leaves the state unchanged:

(def bad (repl/try! (repl/proof-state s2) (tactic/exact [:bound 1])))

(:status bad)
;=> :failure

(repl/why bad)
;=> #:failure{:category :tactic/type-mismatch,
;             :tactic :exact,
;             :detail {:term [:bound 1],
;                      :kernel {:status :rejected,
;                               :error {:expected [:bound 1], :actual [:sort [:param u]], ...},
;                               :message "Term does not inhabit expected type"}}}

(= (:state bad) (repl/proof-state s2))
;=> true

[:bound 1] is the type A itself, and the goal wants an element of A. The local x fits:

(def done (repl/try! (repl/proof-state s2) (tactic/assumption)))

(:status done)
;=> :proved

(:proof done)
;=> {:rainbow/kind :checked-proof,
;    :proof/term [:lam [:sort [:param u]] [:lam [:bound 0] [:bound 0] :explicit] :explicit],
;    :proof/type [:pi [:sort [:param u]] [:pi [:bound 0] [:bound 1] :explicit] :explicit],
;    :proof/environment-id "sha256:...",
;    :proof/axioms #{},
;    :proof/history [#:event{:tactic :intro, :name A}
;                    #:event{:tactic :intro, :name x}
;                    #:event{:tactic :exact, :term [:bound 0]}]}

assumption closed the goal with exact. With no goals left, rainbow.proof/progress assembled the term and called kernel/check, and the result also holds :kernel {:status :checked ...}.

Functions

A state is a map with :proof/goals, :proof/partial-term (the proof so far, [:hole "g-n"] for open goals), :proof/history, :proof/root-goal and :proof/environment. Keep a state in a var to go back to it.

A tactic result has :status :progress (new state in :state, open goals in :goals, the step in :event), :proved (the kernel accepted the term, results in :proof and :kernel) or :failure (:state is the unchanged input, :failure says why). repeat and all-goals can also return :no-progress.

Tactics

Tactics in rainbow.tactic (source) map a state to a result. They work on the focused goal and take core terms in its context.

reflexivity, rewrite, calc and simplify need equality/Eq, equality/reflexive, equality/symmetric and equality/transitive in the environment.

Induction

rainbow.history.nat-induction (source) proves (n : Nat) -> n = n. It loads artifacts/day7/environment.edn, so run it from the repository root.

(defn prove-reflexive-induction [environment terms]
  (let [{:keys [nat]} terms
        target (term/pi-term nat (equality-type terms (term/bound 0) (term/bound 0)))
        introduced (tactic/run (:state (proof/start environment target)) (tactic/intro 'n))
        induced (tactic/run (:state introduced) (tactic/induction [:bound 0]))
        base (tactic/run (:state induced) (tactic/reflexivity))
        predecessor (tactic/run (:state base) (tactic/intro 'predecessor))
        hypothesis (tactic/run (:state predecessor) (tactic/intro 'induction-hypothesis))]
    (tactic/run (:state hypothesis) (tactic/reflexivity))))

(tactic/induction [:bound 0]) leaves two goals:

(:event induced)
;=> #:event{:tactic :induction, :expression [:bound 0], :cases 2}

(mapv :goal/path (:goals induced))
;=> [[0 0] [0 1]]

Goal g-2 is the motive at data/zero. Goal g-3 says the motive at predecessor implies the motive at succ predecessor. The motive (fn [n] (Eq Nat n n)) comes from abstracting [:bound 0] out of the target and stays unreduced in the case targets. reflexivity reduces the head of the target before it looks for equality/Eq, so it closes both cases. The proof is axiom-free. induction passes the goal’s universe level to the recursor as the motive universe (see Inductive types).

Search

search! runs a deterministic, bounded, breadth-first search over proof states. The default budget is 1,000 states, depth 32 and 10 seconds, and your map is merged over it. It proves transitivity of implication by itself:

(def s (repl/surface-goal env '[:forall [[A Prop] [B Prop] [C Prop]]
                                 [:-> [:-> A B] [:-> B C] A C]]))
(def r (repl/search! (repl/proof-state s) {:states 100}))

(:status r)
;=> :proved

(get-in r [:proof :proof/history])
;=> [#:event{:tactic :intro, :name h1} ... #:event{:tactic :intro, :name h6}
;    #:event{:tactic :apply, :term [:bound 1], :subgoals 1}
;    #:event{:tactic :apply, :term [:bound 2], :subgoals 1}
;    #:event{:tactic :exact, :term [:bound 0]}]

A search that cannot finish reports where it stopped:

(repl/search! (repl/proof-state (repl/surface-goal env '[:forall [[A Prop] [B Prop]] [:-> A B]]))
              {:states 50})
;=> {:status :blocked,
;    :reason :frontier-exhausted,
;    :remaining [{:goal-hash "sha256:...", :target [:bound 1], :context [...]}],
;    :dominant-failures [{:class :tactic/conclusion-mismatch, :count 6}
;                        {:class :tactic/no-matching-assumption, :count 4}],
;    :telemetry {...}}

Tactic programs

(repl/run-program started '[[:intro A] [:intro x] [:assumption]]) runs a vector of steps on a started proof. Steps are [:intro name], [:exact term], [:apply term], [:assumption], [:refine template targets], [:rewrite proof options], [:simplify equalities options], [:calc proofs], [:induction term] and [:search budget]. The program stops at the first result that is neither :ready nor :progress and returns it. An unknown step throws with :repl/unsupported-step.

declare-theorem elaborates the statement, runs the proof and adds the theorem through kernel/add-declaration:

(repl/declare-theorem env 'example/identity {:universes ['u]}
                      '[:forall [[A [:sort [:param u]]] [x A]] A]
                      '[:by [[:intro A] [:intro x] [:assumption]]])
;=> {:status :accepted,
;    :declaration #:rainbow{:kind :theorem, :aliases #{example/identity}, :universes [u],
;                           :id "sha256:e8cf6058...", ...},
;    :environment {...}}

The proof form is [:by steps] or [:core term]. Steps are data, and no Clojure code in them runs. declare-theorem elaborates with type-expression and records no dependencies, so it only takes statements and proofs without constants. For anything that uses the library, write a spec in a module, as in Declarations and modules.