Introduction

Commonly used proof assistants like Coq and Lean don’t prove theorems directly using the typing rules. Rather, they use tactics to reason backwards from some goal to the core set of axioms. In this post, I’ll build a (very simplified) tactics engine, implement some simple tactics, and prove some (basic) proofs.

This post is a sequel to several earlier posts about proofs and reasoning. I recommend reading those posts first.

Forward Chaining

Rule-based AI system usually distinguish between two main types of reasoning, “forward chaining” and “backward chaining”. In “forward chaining” you start from known facts, rules, or data and then derive new facts (often searching for a goal). For example, suppose we know:

Socrates is a man
All men are mortal

By following the rules of logic, we can extend our set of facts with a new fact:

Socrates is a man
All men are mortal
Socrates is mortal

The typing rules approach so far has been a sort of “forward” chaining: we’ve started from the simplest axions (usually introducing environments, variables and constants) then building up to more complex theories with sequences of function compositions.

Forward chaining might be better for exploration (when you don’t know what “theorem” you want to choose beforehand) as you can keep running the system and adding new “facts” to it. On the other hand, forward chaining can be computationally expensive. Depending on the reasoning system, any combination or permutation of the input facts and rules could lead to a new fact or rule, and the number of rules could grow very large if you are operating in a complex domain.

And besides, what if you just care about a making a decision about a single theorem?

Backward Chaining

Some of the proofs, especially using induction, have been long or difficult to get right. Most proof assistants (like Coq and Lean) start from the “goal” and then work backwards, trying to reduce the goal to known facts.

class Goal:
    def __init__(self, environment: Environment, conclusion: Term):
        self.environment = environment
        self.conclusion = conclusion
    def __repr__(self):
        return str(self.conclusion)

The idea is you reduce the “goal” type to tautologies or known proofs using “tactics”. Each tactic corresponds (in theory) to some set of typing rules run “in reverse”. At each step, we declare a tactic, which transforms the current goal and then reduces it to a new goal (or goals).

class Tactic:
    def apply(self, goal: Goal):
        raise NotImplementedError()
    
    def elaborate(self, subterm: Term) -> Term:
        raise NotImplementedError()

    def __repr__(self):
        return self.__class__.__name__

If you can completely reduce the the entire goal type to trivialities, then running those steps “in reverse” would generate the proof¹.

The ProofState below will be used to track the tactics used so far and the goals.

class ProofState:
    def __init__(self, goals):
        self.goals = goals 
        self.tactics_applied = [] 

    def __repr__(self):
        return str(self.goals)

Next we will need an engine to run the tactics, then a few example tactics.

Proof Engine

class ProofEngine:
    def __init__(self, initial_goal: Goal):
        self.state = ProofState([initial_goal])
    
    def elaborate_proof(self):
        pprint(self.state.tactics_applied)
    
    def run_tactic(self, tactic: Tactic):
        current_goal = self.state.goals.pop()
        new_goals = tactic.apply(current_goal)
        self.state.goals.extend(new_goals)

        self.state.tactics_applied.append((tactic, current_goal, new_goals))
        
        if not self.state.goals:  
            # Convert tactical proof into explicit term - not yet implemented
            self.elaborate_proof()
            # self.state.proof_term = self.elaborate_proof()

This is straightforward so far. We start with an initial goal. Given a tactic, we apply it to the goal, then record what happened. When our goal is reduced to nothing, we are done. We print the log as a record of the proof.

In this post, elaborate_proof just prints out the log of tactics. Hopefully in a future post we will be able to construct the proof from the typing rules using this data.

Some Basic Tactics

Let’s look at some basic tactics. These should roughly match tactics used in languages like lean ².

I won’t belabor the explanations. I recommended some better resources for learning to use proof assistants in this post: they will provide much better tutorials than I will.

Intro

The Intro tactic is a basic and frequently used tactic. Given a goal with a product type(universal quantification or function types in our type theory), say of form:

\[ \forall x:A, B \]

Then if you add \(x:A\) to the context and reduce the goal to \(B\)³.

class IntroTactic(Tactic):
    def apply(self, goal: Goal):
        if not isinstance(goal.conclusion, ProductType):
            raise Exception("Can't intro on non-product type")
            
        # Add the variable to our context
        newLocalContext = goal.environment.localContext.assume_term(
            goal.conclusion.variable, 
            goal.conclusion.term1
        )
        newEnv = Environment(goal.environment.globalEnvironment, newLocalContext)
        
        # Return new goal with the body of the product type
        return [Goal(newEnv, goal.conclusion.term2)]

Rewrite

The Rewrite tactic is used for equational reasoning when we have an equality in our context and want to replace one side of it with the other in our goal.

That is, given a hypothesis \(h: a = b\) and a goal containing \(a\), the Rewrite tactic will replace some or all occurrences of \(a\) with \(b\) (or vice-versa).

class RewriteTactic(Tactic):
    def __init__(self, hypothesis_name = None):
        self.hypothesis_name = hypothesis_name

    def apply(self, goal: Goal):
        hypothesis_name = self.hypothesis_name
        if hypothesis_name is None:
            hypothesis_name = next(iter(goal.environment.localContext.assumed_terms))
            equality_proof = goal.environment.localContext.body()[hypothesis_name]
        else:
            if hypothesis_name not in goal.environment.localContext.assumed_terms:
                raise Exception(f"Hypothesis {hypothesis_name} not found in context")
            equality_proof = goal.environment.localContext.body()[hypothesis_name]

        norm_proof = strong_normalize(equality_proof, goal.environment)
        if not isinstance(norm_proof, Application):
            raise Exception("Equality proof has invalid form")

        rhs = norm_proof.second
        lhs_app = norm_proof.first 
        if not isinstance(lhs_app, Application):
            raise Exception("Invalid equality proof structure")
            
        lhs = lhs_app.second
        type_app = lhs_app.first
        if not isinstance(type_app, Application):
            raise Exception("Invalid equality proof structure")
            
        new_conclusion = substitute(goal.conclusion, rhs, lhs)
        return [Goal(goal.environment, new_conclusion)]

Reflexivity

Reflexivity is used to prove that something equals itself. It’s often the final step in an equational reasoning chain. If our goal is to prove \(t = t\), Reflexivity will complete the proof immediately.

class ReflexivityTactic(Tactic):
    def apply(self, goal: Goal):
        conclusion = goal.conclusion
        rhs = conclusion.second
        eq_a_x = conclusion.first
        if not isinstance(eq_a_x, Application):
            raise Exception("Goal not an equality") 
            
        lhs = eq_a_x.second
        eq_a = eq_a_x.first

        if not isinstance(eq_a, Application):
            raise Exception("Goal not an equality")
        if not terms_equal(goal.environment, lhs, rhs):
            raise Exception("Terms not convertible")
            
        return []

Apply

Let’s you apply one equation to another.

The Apply tactic uses a hypothesis or lemma whose conclusion matches our current goal. If we have a hypothesis \(h: A \to B\) and our goal is \(B\), then Apply \(h\) will change our goal to proving \(A\)⁴.

class ApplyTactic(Tactic):    
    def __init__(self, term):
        self.term = term

    def apply(self, goal: Goal):
        lemma_type = goal.environment.localContext.assumed_terms[self.term]
        
        if not isinstance(lemma_type, ProductType):
            raise Exception("Lemma must be function type")
            
        normalized_lemma = strong_normalize(lemma_type, goal.environment)
        normalized_goal = strong_normalize(goal.conclusion, goal.environment)
        
        if not terms_equal(goal.environment, normalized_lemma.term2, normalized_goal):
            raise Exception("Lemma conclusion doesn't match goal")
        return [Goal(goal.environment, normalized_lemma.term1)]

Exact

The Exact tactic is used when we have exactly what we need to prove in our context. If we’re trying to prove \(P\) and we have a hypothesis \(h: P\), then Exact \(h\) completes the proof.

class ExactTactic(Tactic):    
    def __init__(self, hypothesis_name: str):
        self.hypothesis_name = hypothesis_name
        
    def apply(self, goal: Goal):
        if self.hypothesis_name not in goal.environment.localContext.assumed_terms:
            raise Exception(f"Hypothesis {self.hypothesis_name} not found")
            
        h_type = goal.environment.localContext.assumed_terms[self.hypothesis_name]
        
        if not terms_equal(goal.environment, h_type, goal.conclusion):
            raise Exception("Hypothesis type doesn't match goal")
            
        return []

Basic Proofs

Let’s look at some proofs.

Transitivity of Equality

Here we prove the basic theorem:

\[ \forall A: \text{Type}, \forall x, y, z : A, x = y \to y = z \to x = z \]

How will we proceed? The first part of the code just defines the goal. Then, we will use intros six times to reduce the context and goal to:

Context: \[ \begin{align*} A &: \text{Type} \\ x &: A \\ y &: A \\ z &: A \\ h &: x = y \\ h2 &: y = z \end{align*} \]

Goal: \[ x = z \]

Them we rewrite twice using \(h\) and \(h2\):

\[ z = z \]

At which point we call Reflexivity and the goal is empty.

Here’s the full code:

def prove_trans_eq():
    A = Variable("A")
    x = Variable("x")
    y = Variable("y")
    z = Variable("z")
    h = Variable("h")
    h2 = Variable("h2")
    eq = Constant("eq")

    final_eq = Application(Application(eq, A), x)
    final_eq = Application(final_eq, z)

    h_type = Application(Application(eq, A), x)
    h_type = Application(h_type, y)

    h2_type = Application(Application(eq, A), y)
    h2_type = Application(h2_type, z)

    conclusion = ProductType(h2, h2_type, final_eq)
    conclusion = ProductType(h, h_type, conclusion)
    conclusion = ProductType(z, A, conclusion)
    conclusion = ProductType(y, A, conclusion)
    conclusion = ProductType(x, A, conclusion)
    conclusion = ProductType(A, Type(0), conclusion)

    globalEnv = GlobalEnvironment("E")
    localContext = LocalContext("Gamma")
    env = Environment(globalEnv, localContext)
    goal = Goal(env, conclusion)

    # goal: forall (A: Type) (x y z: A) (h: x = y) (h2: y = z), x = z
    # intros A x y z h h2     # Introduce all variables into context
    # rewrite h              # Change x to y
    # rewrite h2             # Change y to z
    # reflexivity            # Now we have z = z

    pe = ProofEngine(goal)
    pe.run_tactic(IntroTactic())
    pe.run_tactic(IntroTactic())
    pe.run_tactic(IntroTactic())
    pe.run_tactic(IntroTactic())
    pe.run_tactic(IntroTactic())
    pe.run_tactic(IntroTactic())
    pe.run_tactic(RewriteTactic("h"))
    pe.run_tactic(RewriteTactic("h2"))
    pe.run_tactic(ReflexivityTactic())

    return

One minor convenience: we run the IntroTactic six times in a row in the above proof. We can create a new tactic, IntrosTactic, that calls IntroTactic until it can’t anymore.

class IntrosTactic(Tactic):
    def apply(self, goal: Goal):
        current_goal = goal
        intro = IntroTactic()
        
        while isinstance(current_goal.conclusion, ProductType):
            try:
                current_goal = intro.apply(current_goal)[0]
            except Exception:
                break
                
        return [current_goal]

Modus Ponens

Here we prove the basic theorem: \[ \forall P, Q: \text{Prop}, (P \to Q) \to P \to Q \] First, we use intros to bring everything into our context. The result would look like:

\[ \begin{align*} P &: \text{Prop} \\ Q &: \text{Prop} \\ H &: P \to Q \\ p &: P \end{align*} \]

Goal: \[ Q \] Then we can use two simple steps:

Apply \(H\) which changes our goal to \(P\)

Use Exact on \(p\) since we have \(p:P\) in our context. This reduces the goal to nothing.

def prove_modus_ponens():
    P = Variable("P")
    Q = Variable("Q")
    H = Variable("H") 
    p = Variable("p")

    # forall (P Q: Prop), (P -> Q) -> P -> Q
    h_type = ProductType(P, P, Q) 

    conclusion = ProductType(p, P, Q)  
    conclusion = ProductType(H, h_type, conclusion)  
    conclusion = ProductType(Q, Prop(), conclusion)  
    conclusion = ProductType(P, Prop(), conclusion)

    goal = Goal(Environment(GlobalEnvironment("E"), LocalContext("Gamma")), conclusion)

    pe = ProofEngine(goal)
    pe.run_tactic(IntrosTactic())
    pe.run_tactic(ApplyTactic("H"))  
    pe.run_tactic(ExactTactic("p"))
    print(pe.state)

Next Steps

We built a simple tactics engine and proved some (trivial) theorems. We should be able to add new tactics reasonably frequently as we need them.

In the game plan, this is the first part of step 6.

If you’ve been following along, we still have some more work to do on induction, mostly adding match terms, and we will need to link together the tactics with the typing rules (assuming I can figure out how to do that). We may also extend some of the hierarchies, as needed.

Footnotes

One of my main goals for this project was to understand how this all works (using code), so take what I say with a grain of salt. Getting closer, though!↩︎
At least in terms of function. Not yet sure how Lean or Coq implements the logic for these tactics under-the-hood. My versions are VERY simplified.↩︎
I’ve been thinking of this as “reverse lam” (which may or may not be correct). Rather than binding a variable, we “unbind” it.↩︎
I think of this as “reverse app”.↩︎