Tactics with Types and Shapes

Tactics are programs that, given a context and a goal, return a new goal and context. As a fully stateful program, this view of tactics is rooted in the imperative programming paradigm, where program semantics can only be known after we run our programs. Our work at Glaive is to study tactics such that we do not have to guess what a tactic will do, we can infer that information directly from its type.

In the same way as you wouldn’t give a function String -> String a value of type Int, there is no sense in applying a tactic to a goal for which it cannot meaningfully make progress. So, what is the type of a tactic?

Proof Trees and Tactics

If we look at a statement such as $37 + (a × b) = 37 + (b × a)$ we can tell, as a human that it is true, but convincing a computer that it is takes some time and effort.

Given some tactics applying congruence, and symmetry, we can derive this proof:

def prob1 (a b : Nat) : 37 + a * b = 37 + b * a := by
  rw [Nat.mul_comm a b]

This is not the only proof! We can also write the following:

def prob2 (a b : Nat) : 37 + a * b = 37 + b * a := by
   congr 1
   exact Nat.mul_comm a b

Since there are multiple ways of proving the same thing, how do we know we are writing a “good” proof, what’s the difference between one that is longer and one that is shorter, how can we qualitatively evaluate different proof strategies? Until now, those questions are answered by social conventions where different challenges, like readability, maintenance, logical foundations, would inform what kind of proof is expected to be “good”.

Our approach focuses on the proof tree produced by a series of tactics. A good proof will produce a richly-typed proof tree with nodes carrying a lot of information about the current proof state and branches.

A Basic arithmetic Theorem prover

To demonstrate the capabilities of typed tactics, we implement a well-known logical system: Arithmetic on natural numbers.

This system has a very simple language to combine numbers via three constructors: successor, addition and multiplication. Along with two base terms, one for named variable and one for 0.

inductive Term where
  | Atom : String → Term
  | Zero : Term
  | Succ : Term → Term
  | Plus : Term → Term → Term
  | Mult : Term → Term → Term

We then define the basic building bloc for a proof system equating two Terms. A term is equal to itself, two equalities can be placed end-to-end if they share a common term, and equalities are symmetric.

inductive Equation : Term → Term → Type where
  /-- Every term is equal to itself. -/
  | Refl : Equation t t
  /-- Equality is transitive. -/
  | Trans : Equation r s → Equation s t → Equation r t
  /-- Equality is symmetric. -/
  | Sym : Equation t s → Equation s t

To this we add the equational theory of natural numbers we all expect, addition is symmetric, zero is a neutral element, etc¹.

  /-- Congruence for `Succ`. -/
  | CongS : Equation t s → Equation (Term.Succ t) (Term.Succ s)
  /-- Congruence for addition. -/
  | CongPlus : Equation t s → Equation x y → Equation (Term.Plus t x) (Term.Plus s y)
  /-- Plus is symmetric. -/
  | SymPlus : Equation (Term.Plus t s) (Term.Plus s t)
  /-- Mult is symmetric. -/
  | AssocPlus :
      Equation (Term.Plus t (Term.Plus r s))
               (Term.Plus (Term.Plus t r) s)
  /-- zero is neutral for + -/
  | ZeroPlusNeutral : Equation t s → Equation (Term.Plus t Term.Zero) s

Monad-typed tactics

Tactics historically can be seen as a function manipulating goals and theorems. First by splitting the goal into smaller subgoals, and then by reconstructing the proof of the original goal by combining the proofs collected by each sub-goal.

tactic : Type
tactic = goal → List goal × (List thm → thm)

The continuation List thm → thm combines sub-proof corresponding to each solved sub-goal into a bigger proof for the goal originally given in argument.

This approach has two shortcomings, first there is no way to handle errors when a goal cannot be split by the tactic into subgoals. Second, there is no relation between the list of subgoals generated and the list of theorems collected.

Viewing tactics as dependent lenses solve those problems by giving a precise type to a tactic.

tactic : Type
tactic = Eq =&> Any.Maybe (All.List Eq)

Expanding the definition of =&> give us a term that looks exactly like our traditional tactics but with a very precise relationship between inputs and output brought in by dependent types:

tactic : Type
tactic = (g : goal) → Σ Maybe (List goal) , Any All

This change is not fluff, it makes inconsistent states unrepresentable. If the tactic does not apply, then no theorems can be extracted or expected. If the tactic generates 3 sub-goals then 3 sub-theorems will be generated, always.

The Maybe and List functors on containers are monads, and their composition distribute, suggesting a more generic SubGoals monad on container such that failure is represented by a missing value, and a void proof, and success wraps a list of subgoal, for each of which we carry a proof.

abbrev Subgoal a := Any.Maybe (Forall a)

By paring terms and equations we define the container of goals and proofs for our system.

def EqProblem : Container :=
  Container.mkC (Term × Term) (fun t => Equation t.π1 t.π2)

And the type of tactics is given by kleisli endomorphisms of the Subgoal monad.

abbrev Tactic : Type := EqProblem =&> Subgoals EqProblem

Using this one type we can define all the tactics in our theorem prover:

/-- The symmetry tactic: solving a problem reduces to solving its symmetric. Always applies. -/
def sym : Tactic :=
  !! fun x => some [(x.π2, x.π1)] ## fun (Aye (.Cons y _)) => .Sym y

/-- Equality is transitive. -/
def trans (t : Term) : Tactic :=
  !! fun x => some [(x.π1, t), (t, x.π2)]
  ## fun (Aye (.Cons y (.Cons z _))) => Equation.Trans y z

You will notice that trans is takes a Term in argument, this property turns it into a meta-tactic, a tactic that needs information from the context or the user to be run. As such, transitivity will be primarily used as a building block for more sophisticated tactics. Let’s start building those tactics!

/-- Associativity can be applied on the left of an equality
  a + (b + c) = t -> (a + b) + c = t -/
def assocLeftPlus : Tactic :=
  !! fun x =>
      match x with
        | (.Plus a (.Plus b c), t) =>
          some [(.Plus (.Plus a b) c, t)] ##
          fun (Aye x) => Equation.Trans Equation.AssocPlus x.head
        | (.Plus (.Plus a b) c, t) =>
          some [(.Plus a (.Plus b c), t)] ##
          fun (Aye x) => Equation.Trans (Equation.Sym Equation.AssocPlus) x.head
        | _ => none ## fun e => nomatch e

This tactic analysis the goal and if it has the shape a + (b + c) = t it will create a sub-goal (a + b) + c = t and combine the sub-proof using transitivity and associativity.

All other tactics can be written in this style, resulting in a list of Tactics that we can execute at each step of our theorem prover.

Running the prover

Each tactic gives us a function that will take a goal and return a new list of subgoals if it applies, or nothing if it does not apply. This decision procedure already help analyse a goal and give us the list of tactics that apply and their associated update subgoals. In this setting a proof state is characterised by the list of goals to solve and the context is given by the list of tactics that apply to the current goal.

Our initial state contains all goals and all tactics:

structure ProofState where
  goals : List Goal
  tactics : List Tactic

For a given goal, we can update the list of tactics in context by filtering the ones that do not apply:

def filterTactics (goal : Goal) (tactics : List (Named Tactic)) : List (Named (List Goal)) :=
  List.filterMap (fun t => match t.val.fn goal with
                                  | ⟨ some x , _ ⟩ => some ⟨ t.name, x ⟩
                                  | ⟨ none , _ ⟩ => none
                 ) tactics

Here we do two steps at once because we also recover the list of new goals resulting from applying the tactics. Not only we are able to show relevant tactics, we also get a preview of the next goal if it were to be applied².

result in the terminal.

    let filtered := filterTactics xs
        (p.primitives ++
          List.map (Functor.map tacticsFromAxioms) p.axioms
          ++ tacticsFromHighTactics p.axioms p.higher
          )

    let (newGoals, _) ← selectFromList toString filtered
    IO.println s!"new goal {toString newGoals}"

The basic proof loop takes the selected goal, display the available tactics to make progress toward a proof and once a tactic has been chosen, update the goal with the new subgoals generated by applying this tactic.

Here is an example of running the prover in the terminal:

current subGoal:

((37 + x) + q) = (37 + (q + x))
  [0] symmetry: [(37 + (q + x)) = ((37 + x) + q)]
  [1] sym+: [(q + (37 + x)) = (37 + (q + x))]
  [2] assoc+: [(37 + (x + q)) = (37 + (q + x))]
  [3] congruence+: [(37 + x) = 37, q = (q + x)]
> 2
new goal assoc+: [(37 + (x + q)) = (37 + (q + x))]
current subGoal:

(37 + (x + q)) = (37 + (q + x))
  [0] symmetry: [(37 + (q + x)) = (37 + (x + q))]
  [1] sym+: [((x + q) + 37) = (37 + (q + x))]
  [2] assoc+: [((37 + x) + q) = (37 + (q + x))]
  [3] congruence+: [37 = 37, (x + q) = (q + x)]
  [4] refl: [(x + q) = (q + x)]
> 4
new goal refl: [(x + q) = (q + x)]
current subGoal:

(x + q) = (q + x)
  [0] symmetry: [(q + x) = (x + q)]
  [1] sym+: [(q + x) = (q + x)]
  [2] congruence+: [x = q, q = x]
> 1
new goal sym+: [(q + x) = (q + x)]
current subGoal:

(q + x) = (q + x)
  [0] symmetry: [(q + x) = (q + x)]
  [1] sym+: [(x + q) = (q + x)]
  [2] reflPrim: []
  [3] congruence+: [q = q, x = x]
  [4] refl: []
  [5] refl: [x = x]
> 4
new goal refl: []
QED

At each step the list of tactics is inferred by pre-computing the next goal and keeping only the tactics that match. Tactics that fail return none in their forward part, which breaks down the goal. Tactics that succeed and entirely solve the goal return some [] which is what we see with the last use of refl. Tactics that succeed but return multiple subgoals return some [ x, y ] and each subgoal x and y is shown in the output, this is why congruence+ has two elements in the list of output goals.

So far the types we gave are pretty uniform, everything is a Tactic, but we can give even more precise types.

Monoid-typed tactics

The Tactic monad gives us a very expressive way to compose tactics accurately but we can do better. By describing exactly how many subgoals a tactic produces we can wire together tactics and clearly see how the proof tree is built from smaller more primitive tactics.

We implemented a basic tactical theorem prover using the Subgoal monad but we haven’t really shown the benefits of containers in terms of how they help give more precise type to tactics, right now, all our tactics have the same type, a lens EqProblem =&> Subgoal EqProblem, but we can do better.

The first distinction to make is between tactics that can fail and tactics that can never fail. There are tactics that are always available because their application do not depend on the current goal. Sym is one of them, it never fails because the goal a = b can always be flipped to become b = a

applySym : EqProblem =&> EqProblem

If you are familiar with reversible rules in sequent calculus this is one exmaple of the type of a reversible rule. It can never fail, and it can always be undone.

Another tactic with a more precise type is reflexivity. A proof by reflexivity never creates any additional subgoals. Either it succeeds and finishes, or it does not apply at all. Its type is therefore:

applyRefl : EqProblem =&> Maybe I

We use I, the tensor unit, to indicate a leaf-tactic with no further subgoal, this is isomorphic to an empty list of subgoals.

Finally, a third kind of tactic is one that generates multiple subgoals, in our system, transitivity generates 2 subgoals, it also never fails, type is therefore:

applyTrans : (t : Term) -> EqProblem =&> EqProblem ⊗ EqProblem

We now see why the All.List monad is the correct monad for representing all subgoals

Type	List Term
I	[]
Eq	[ x ]
Eq ⊗ Eq	[ x , y ]

Giving types to tactics reveals the structure of the proof tree that we are building in a way that using lists of subgoals cannot represent. Lists of subgoals are useful to building a theorem prover by giving a uniform type to each tactic and treating them all the same. But we want to recover the rich structure of tactics to help the user drive the proof in a productive direction.

Tactics and Goal Shapes

We can further refine the type of tactics by parameterising them by a predicate indicating what shape the goal. Most goals will have multiple shapes such that multiple tactics that can be applied. Typically a goal a + b = c + d is shaped like a congruence, a goal a + (b + c) = (a' + b') + c' is shaped both like a congruence and an associativity tactic.

In addition to give the type of a tactic in term of proof-tree or sub-goal generation, we also want to infer the shape of the goal and use that information to further help with tactic selection. A goal that is symmetry-shaped can have the symmetry tactic applied to it. Each goal can have multiple compatible shapes, those shapes emerge from the head of the expression tree of the goal. For example the goal a + (b + c) = (a + c) + b expression has trees

┌─(+)─┐           ┌─(+)─┐
│     │           │     │
a  ┌─(+)─┐  =  ┌─(+)─┐  b
   │     │     │     │
   b     c     a     c

Anything that has head shape:

┌─(+)─┐     =     ┌─(+)─┐

is “congruence-shaped”.

Similarly anything with a left tree

┌─(+)─┐
│     │
a  ┌─(+)─┐  =  x
   │     │
   b     c

is “associative-shaped”.

This is how we can infer that the goal a + (b + c) = (a + c) + b has shapes congruence ∧ assoc+ ∧ assoc1+ ∧ flip. In fact we’re built a demo that will, given a list of shapes deciders provide the type and shape of the prover’s goal and then propose tactics that match the shape of the goal.

The shapes of a tactic form a lattice where the top of the lattice contains the most general shape and its children contain more and more sophisticated shapes

flowchart TD
    A --> Cong1P["Cong1+\na+b=c"]
    A["Sym\na=b"] --> B["Refl\na=a"]
    A --> Cong1M["Cong1×\na×b=c"]
    Cong1P --> AssocPL["assocR+\na+(b+c)=d"]
    Cong1P --> AssocPR["assocL+\n(a+b)+c=d"]
    AssocPR --> AssocP["assoc+\na+(b+c)=(a+b)+c"]
    AssocPL --> AssocP
    Cong1P --> DistribP["distrib+\n(a×b)+(a×c)=d"]
    Cong1M -->DistribM["distrib×\na×(b+c)=d"]
    DistribM --> Distrib["distrib\n(a×b)+(a×c)=a×(b+c)"]
    DistribP --> Distrib
    Cong1M --> AssocMR["assocR×\na×(b×c)=d"]
    Cong1M --> AssocML["assocL×\n(a×b)×c=d"]
    AssocMR --> AssocM["assocR×\na×(b×c)=(a×b)×c"]
    AssocML --> AssocM

This lattice suggest a subtyping relation between tactic shapes, an area of research we plan to explore in the coming months.

Finally, once a shape has been identified, we obtain a deterministic tactic that can never fail. The shape already provides all the information necessary to run the tactic, there is no more guessing or error handling.

The congruence tactic for example takes evidence that the goal is congruence-shaped and return the appropriate list of subgoals:

applyCong : IsCong g -> EqShape g =&> All.List EqGen

In general a tactic with shapes is given by a shape predicate Goal -> Type and a lens EqShape g =&> All.List EqGen. Where EqShape g is a container with a singleton g in the base.

Running the prover

Our implementation is based on a prover’s state carrying the set of shapes any goal can have, for each shape, a tactic that will reduce the goal, and the list of goals left to solve.

The theorem prover then analyses the shape of the goal and displays it, along with the tactics that will make progress for this goal.

Here is an example where the goal is given by the expression a + (b + c) = (a + c) + b.

current goal (a + (b + c)) = ((a + c) + b)
goal shape : congruence ∧ assoc+ ∧ assoc1+ ∧ flip
candidate tactics:
[0]: congruence: ["a = (a + c)", "(b + c) = b"]
[1]: assoc+: ["a = a", "b = c", "c = b"]
[2]: assoc1+: ["((a + b) + c) = ((a + c) + b)"]
[3]: flip: ["((a + c) + b) = (a + (b + c))"]

By picking flip we make use of symmetry of equality proofs.

current goal ((a + c) + b) = (a + (b + c))
goal shape : congruence ∧ assoc+ ∧ assoc1+ ∧ flip
candidate tactics:
[0]: congruence: ["(a + c) = a", "b = (b + c)"]
[1]: assoc+: ["a = a", "b = c", "c = b"]
[2]: assoc1+: ["(a + (c + b)) = (a + (b + c))"]
[3]: flip: ["(a + (b + c)) = ((a + c) + b)"]

This step is necessary to apply assoc1+ to the expression (a + c) + b which results in a + (c + b).

current goal (a + (c + b)) = (a + (b + c))
goal shape : congruence ∧ assoc1+ ∧ flip
candidate tactics:
[0]: congruence: ["(c + b) = (b + c)"]
[1]: assoc1+: ["((a + c) + b) = (a + (b + c))"]
[2]: flip: ["(a + (b + c)) = (a + (c + b))"]

We can now eliminate a + by congruence which is identified by the congruence shape

current goal (c + b) = (b + c)
goal shape : congruence ∧ symmetry+ ∧ flip
candidate tactics:
[0]: congruence: ["c = b", "b = c"]
[1]: symmetry+: []
[2]: flip: ["(b + c) = (c + b)"]

1
QED

The final step is an application of symmetry of + which resolves the goal and completes the proof.

AI for Maths

We haven’t said anything about AI yet, our mission is to further the understanding of mathematics & formal systems through the lens of AI capabilities. We are seeing a mutually beneficial relationship between AI understanding and human understanding of mathematics. In the last few months, we have been deeply focused on how the two relate and how we can help both human and AI interact with more sophisticated tools to write and understand mathematics.

Giving types to tactics greatly reduces the search space for a human to study and pick the next tactic to use. This feature grealy benefits machines too as we can mechanically constrain their input to known-good interactions via Stellar. What is more, our analysis of tactics can generate well-typed traces (proof trees) which contain vastly more semantic information than the purely syntactic data that a lean file contains.

Our experiments with AI go much deeper than merely training or connecting an existing model to our lens-based proof infrastructure. By using structured generation we expect to obtain a model that can directly think and speak in terms of tactics and proof state manipulation, without the overhead of post-hoc parsing or probabilistic conditionning. An area of research we’re excited to take further.

1. In this post, we skip the equations for multiplication for brevity but they are present in the code. ↩

2. Named is merely a structure that adds a String label, this is used for printing the ↩