Introduction

The “reverse-chaining” style proofs (working backward from some desired theorem using out tactics engine) ought to be convertible to “forward-chaining” style proofs (working forward from the typing rules).

In this post, I will attempt to implement the elaboration¹ function in the proof engine from the previous post.

This post follows several other posts about implementing a theorem prover in Python. The first post is here or view the links to the complete set.

Strategy

Let’s take a look at our proof engine code:

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:  
            self.elaborate_proof()
            # self.state.proof_term = self.elaborate_proof()

The function of interest is the elaborate_proof function. What we’ll do is contruct a proof using backward-chaining. While we do this, we track each tactic used in the proof. When the final goal is empty, we iterate through each tactic in reverse order. This should construct the forward-chaining style proof.

To accomplish this, we’ll need to implement the “reverse-mode” version of each tactic in the typing rules.

class ProofEngine:
    def __init__(self, initial_goal: Goal):
        self.state = ProofState([initial_goal])
    
    def elaborate_proof(self):
        if self.state.goals:  
            raise Exception("Incomplete proof cannot be elaborated")

        environment = w_empty()
        self.proof_term = None
        goal_to_proof_terms = {}
        goal_to_environment = {}

        # Process tactics in reverse order (from leaves to root)
        for tactic, goal, subgoals in reversed(self.state.tactics_applied):
            print("Elaborating:", tactic, goal, subgoals)
            subgoal_terms = [goal_to_proof_terms.get(sg) for sg in subgoals] if subgoals else None
            term, environment = tactic.elaborate(environment, goal, subgoals, subgoal_terms)
            goal_to_proof_terms[goal] = term
            goal_to_environment[goal] = environment
            self.proof_term = term
        
        return self.proof_term 
    
    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:  
            self.elaborate_proof()

Now elaborate_proof calls elaborate on each tactic in reverse order. But we need to implement the elaborate functions for the tactics themselves.

Tactic Elaboration

Now we’ll implement the elaborate method for a few of our tactics (just the ones we are going to use for an example²).

Intro

   def elaborate(self, env: Environment, goal: Goal, subgoals, subgoal_terms):
        if not isinstance(goal.conclusion, ProductType):
            raise Exception("Can't elaborate intro on non-product type")
            
        var_name = goal.conclusion.variable.name
        var_type = goal.conclusion.term1
        var_obj = Variable(var_name)
        
        # For propositions like "P: Prop", we need to use ax_prop
        if isinstance(var_type, Prop) or terms_equal(env, var_type, Prop()) and (var_type not in env.localContext.body()):
            hyp_type = ax_prop(env)
        elif isinstance(var_type, Set) or terms_equal(env, var_type, Set()) and (var_type not in env.localContext.body()):
            hyp_type = ax_set(env)
        elif isinstance(var_type, Type) and (var_type not in env.localContext.body()):
            hyp_type = ax_type(env, var_type.n)
        elif var_type not in env.localContext.body():
            # Default to prop
            env = w_local_assum(env, var_type, ax_prop(env))
            # Simplification - call Hypothesis
            hyp_type = Hypothesis(env, var_type, env.localContext.body()[var_type.name])

        new_env = w_local_assum(env, var_obj, hyp_type)
        body_term = subgoal_terms[0] if subgoal_terms else None
        
        if not body_term:
            raise Exception("Missing body term for lambda abstraction")
        
        # Create the product type (a simplification, replaces prod_prop)
        prod_type = Hypothesis(new_env, ProductType(var_obj, hyp_type.term_, body_term.type_), hyp_type.type_)
        body_term.localContext = body_term.localContext.assume_term(var_obj, body_term.type_)
        lambda_term = lam(env, var_obj, prod_type, body_term)
        return lambda_term, new_env

This is somewhat simplified, but essentially for each Intro, we run Intro in reverse. Intro usually introduces a variable from the goal into the context. Here we add the variable back into the goal using a combination of product introduction and lam.

Exact

class ExactTactic(Tactic):    
    ...

    def elaborate(self, env, goal, subgoals, subgoal_terms):
        # Basically, if we used p to exact P, we know p:P must have existed. So introduce it.
        hypothesis_name = self.hypothesis_name
        hyp_var = Variable(hypothesis_name)
        hyp_type = Hypothesis(env, Variable(goal.conclusion.name), Prop()) # Simplified to assume Prop
        env = w_local_assum(env, hyp_var, hyp_type)
        goal_hyp = var(env, hyp_var)
        return goal_hyp, env

To use Exact as a tactic, we must have some specific witness in the environment for the last step of the goal. In reverse, we are introducing that witness into the environment.

Proof Example

Let’s look at a proof we already had. Here’s the proof with typing rules:

def prove_identity_implication(term_name='p', prop_name="P"):
    p = Variable(term_name)
    P = Variable(prop_name)
    
    env = w_empty()

    hyp_prop = ax_prop(env)

    env = w_local_assum(env, P, hyp_prop)

    hyp_P = var(env, P)
    env_with_p = w_local_assum(env, p, hyp_P)

    hyp_with_p_P = var(env_with_p, P)

    P_implies_P = prod_prop(env, p, hyp_P, hyp_with_p_P)

    hyp_p = var(env_with_p, p)

    p_implies_p = lam(env, p, P_implies_P, hyp_p)

    p_implies_p_is_prop = prod_prop(env, P, hyp_prop, P_implies_P)
    theorem = lam(env, P, p_implies_p_is_prop, p_implies_p)
    return theorem

And here’s the tactics version:

def prove_p_implies_p_with_elab():
    P = Variable("P")
    p = Variable("p")
    
    conclusion = ProductType(p, P, P)
    conclusion = ProductType(P, Prop(), conclusion)
    
    globalEnv = GlobalEnvironment("E")
    localContext = LocalContext("Gamma")
    env = Environment(globalEnv, localContext)
    goal = Goal(env, conclusion)
    
    # Proof strategy:
    # 1. Introduce P (a proposition)
    # 2. Introduce p (a proof/evidence of P)
    # 3. Return p as the proof of P
    
    pe = ProofEngine(goal)
    pe.run_tactic(IntroTactic())  # Introduce P: Prop
    pe.run_tactic(IntroTactic())  # Introduce p: P
    pe.run_tactic(ExactTactic("p"))  # Return p as the proof
    
    pe.print_applied_tactics()
    lambda_term = pe.elaborate_proof()
    return lambda_term

Looks the same as our proof from before, but now we elaborate proof at the end. This produces a token of the desired type at the end of the proof using the typing rules.

What happens when we elaborate? We iterate through the tactics in reverse order:

In elaborate_proof, we run w_empty.
Then we elaborate ExactTactic("p"). This creates a variable and runs ax_prop.
Then we elaborate Intro. This runs prod_prop and lam.
Then we elaborate Intro again. Once again, we run prod_prop and lam.

If you look back the original typing rules proof of the theorem, you’ll note that it consists of the same steps that we just showed.

Also, both proofs return the same term:

E[Gamma]⊢λP:Prop.λp:Var(P).Var(p):∀P:Prop,(Var(P)->Var(P))

Conclusion and Next Steps

This is the second half of the sixth step in the game plan from the beginning of the post series. Step seven was “automatically searching the space of proofs”. However, now that I’ve come this far I think the next post will be a retrospective on the posts and code so far. I’ve learned a lot building this proof assistant but it may be wiser to move towards a real system if I want to investigate this area further.

Footnotes

Elaboration in dependently typed programming languages refers to the process of transforming high-level source code into a fully explicit core language that the type checker can verify. Here I’m using it to refer to breaking down the tactics into the relevant typing rules.↩︎
I attempted to implement some of the other tactics to handle more complex proofs. I convinced myself that it was possible, but in practice this was pretty difficult and I’m unsure about the results (even the ones here). Based on the complexity, I don’t think this is a good approach for a full-blown theorem prover. I’m also skating over many details (like multiple subgoals) that would arise in production system.↩︎