Match Construct

Introduction

In the Induction post, we were able to build some simple inductive types and write some (very simple proofs). However, the actual process of defining the inductive types and writing the proofs was clunky and difficult. Most theorem provers introduce a Match construct to simplify the process of defining and working complex inductive types. We can use Match constructions both as syntactic sugar to help define inductive types and to more easily define functions that manipulate inductive types by pattern matching against their constructors.

This post follows several other posts about implementing a theorem prover in Python. The first post is here. In this post I’ll attempt to get some basic Match functionality working in conjunction with the previous posts theorem prover implementation in Python. Match constructions can get quite complicated. This post will not implement the full functionality that you would find in a production proof assistant, but will try to get the base functionality working.

Elimination Principles vs Match

In our previous implementation of induction, we automatically generated elimination principles for inductive types. For example, with natural numbers, we created nat_rect, which has the following type:

∀P_nat:(Constant(nat)->Type(0)),((Var(P_nat) Constant(O))->((Constant(nat)->((Var(P_nat) Var(n))->(Var(P_nat) Constant(S))))->∀target_nat:Constant(nat),(Var(P_nat) Var(target_nat))))

This is very intimidating, and hard to parse, but it encodes the standard induction principle for natural numbers. To prove a property P for all natural numbers, you need to:

1. Prove \(P(0)\) (the base case).

2. Prove that for any \(n\), if \(P(n)\) holds, then \(P(S(n))\) also holds (the inductive step).

Here’s an intuitive look at what it would look like to define addition in terms of nat_rect:

def add(n, m):
    return nat_rect(
        lambda x: nat,  # The motive: the property we're defining
        m,              # Base case: 0 + m = m
        lambda k, rec: S(rec)  # Inductive case: S(k) + m = S(k + m)
    )(n)

In our current language, this gets pretty ugly:

def define_plus(env: Environment) -> Environment:
    # Type is: nat -> nat -> nat  
    plus_type = ProductType(
        Variable("n"), 
        Constant("nat"),
        ProductType(
            Variable("m"), 
            Constant("nat"),
            Constant("nat")
        )
    )

    n = Variable("n")
    m = Variable("m")

    # The function needs to do recursion on the first argument:
    # plus := λ n. λ m. nat_rect (λ _. nat) m (λ k rec. S rec) n
    plus_body = FunctionType(
        n, Constant("nat"),
        FunctionType(
            m, Constant("nat"),
            Application(
                Application(
                    Application(
                        Constant("nat_rect"),
                        # Motive: λ _. nat  
                        FunctionType(Variable("_"), Constant("nat"), Constant("nat"))
                    ),
                    # Base: m
                    m
                ),
                # Step: λ k rec. S rec
                FunctionType(
                    Variable("k"), Constant("nat"),
                    FunctionType(
                        Variable("rec"), Constant("nat"),
                        Application(Constant("S"), Variable("rec"))
                    )
                )
            )
        )
    )

    return w_global_def(
        env,
        Constant("plus"),
        Hypothesis(env, plus_body, plus_type) 
    )

Yikes¹. A more complex inductive type would be extremely unwieldy. We can use the Match construction to cut through some of the complexity using functional-programming-like pattern matching (this is pseudocode):

def add(n, m):
    match n with
    | O => m
    | S(k) => S(add(k, m))

We can also use match to handle “enum-like” definitions. For example, say we want to prove theorems about the days of the week. We can define an inductive type as follows:

def define_weekday(env: Environment) -> Environment:
    weekday_type = InductiveType(
        name="weekday",
        params=[],
        indices=[],
        returnType=Set(),
        constructors=[
            InductiveTypeConstructor(day, Constant("weekday"))
            for day in ["sunday", "monday", "tuesday", "wednesday", 
                       "thursday", "friday", "saturday"]
        ]
    )

    return define_inductive(env, weekday_type), weekday_type

You can imagine this (pseudocode) function implementation of is_weekend:

def is_weekend(day):
    return weekday_rect(
        lambda d: bool,                # Motive
        False,                         # Monday case
        False,                         # Tuesday case
        False,                         # Wednesday case
        False,                         # Thursday case  
        False,                         # Friday case
        True,                          # Saturday case
        True                           # Sunday case
    )(day)

with Match we can simplify this:

def is_weekend(day):
    match day with
    | Saturday => True
    | Sunday => True
    | _ => False

Ditto a function like “tomorrow”:

def tomorrow(day):
    match day with
    | Monday => Tuesday
    | Tuesday => Wednesday
    | Wednesday => Thursday
    | Thursday => Friday
    | Friday => Saturday
    | Saturday => Sunday
    | Sunday => Monday

So we have three use cases we might want out of Match²:

1. simplifying the definition of inductive types
2. handling case-by-case proofs (for inductive types)
3. simplifying the definition of functions on inductive types

We won’t handle 1 in this blog post (since we’ve got a perfectly good way of defining inductive types already) but we will try to handle 2 and 3.

Match Construct

Let’s start to implement our Match construct. We’ll start with the extension to our grammar

class MatchBranch:
    __match_args__ = ('constructor', 'bound_vars', 'body')
    def __init__(self, constructor: Constant, bound_vars: List[Variable], body: Term):
        self.constructor = constructor
        self.bound_vars = bound_vars 
        self.body = body
    def __repr__(self):
        return f"MatchBranch({self.constructor}->{self.body})"

class Match:
    __match_args__ = ('name', 'scrutinee', 'motive', 'branches')
    def __init__(self, name:str, scrutinee: Term, motive: Term, branches: List[MatchBranch]):
        self.name = name
        self.scrutinee = scrutinee
        self.motive = motive
        self.branches = branches

    def __repr__(self):
        branches_str = '\n'.join(
            f"| {b.constructor} {' '.join(str(v) for v in b.bound_vars)} => {b.body}"
            for b in self.branches
        )
        return f"match {self.scrutinee} return {self.motive} with\n{branches_str}\nend"

There’s two main classes. The first is for each branch of a Match construct. This has three components:

• constructor: A Constant representing the constructor pattern being matched (like O or S for natural numbers)
• bound_vars: A list of Variables that will be bound to the constructor’s arguments
• body: A Term representing the result expression when this branch matches

The Match construct follows. Here, the constructor takes four parameters:

• name: A string identifier for the match expression
• scrutinee: The term being matched against (the value we’re examining) motive: The return type of the match - expression (similar to the motive in elimination principles)
• branches: A list of MatchBranch objects representing the different cases

Proofs of Inductive Types with Match

Next, let’s try to handle case-by-case proofs for inductive types using the match construct.

Match Rule

Given a valid match object, to view the theorem as “proven” we need to produce a valid hypothesis out of the elimination rules. Let’s take a look at how to do this:

def match_rule(env: Environment, match_: Match, inductive_type: InductiveType) -> Term:
    # Find the elimination principle for this inductive type
    eliminator_name = f"{inductive_type.name}_rect"
    
    # Apply eliminator applied to motive, branches, and scrutinee
    result = Constant(eliminator_name)
    result = Application(result, match_.motive)
    for branch in match_.branches:
        result = Application(result, branch.body.term_)
    result = Application(result, match_.scrutinee)
    
    # Return type (motive applied to scrutinee)
    return_type = Application(match_.motive, match_.scrutinee)
    return Hypothesis(env, result, beta_reduce(return_type))

The match_rule function builds the correct expression using elimination principles. We take the appropriate eliminator (nat_rect in this case), then systematically apply it to the motive, each branch implementation, and the scrutinee value being matched against³.

Proof Example

Let’s now look at a proof example using match. This is a proof we previously handled in the induction post. Here, we will prove it using Match:

def prove_plus_zero_via_match():
    env = w_empty()
    env, nat_type = define_nat(env)
    env = define_plus(env)  
    env, _ = define_equality(env, Set())
    
    zero = const(env, Constant("O"))
    plus = const(env, Constant("plus"))
    eq = const(env, Constant("eq"))
    nat = const(env, Constant("nat"))
    
    n = Variable("n")
    env = w_local_assum(env, n, nat)
    hyp_n = var(env, n)
    
    # n + 0 = n
    n_plus_zero = app(env, app(env, plus, hyp_n), zero)
    
    eq_nat = app(env, eq, nat)
    eq_n = app(env, eq_nat, n_plus_zero)
    eq_type = app(env, eq_n, hyp_n)

    # 0 + 0 = 0
    eq_0 = app(env, eq_nat, zero)
    eq_0_0 = app(env, eq_0, zero)

    # Zero branch
    zero_branch = MatchBranch(
        constructor=Constant("O"),
        bound_vars=[],
        body=eq_0_0
    )
    
    s = Variable("s")
    env = w_local_assum(env, s, nat)
    succ = const(env, Constant("S"))
    s_term = var(env, s)
    succ_s = app(env, succ, s_term)
    succ_s_plus_zero = app(env, app(env, plus, succ_s), zero)
    
    eq_succ_s = app(env, eq_nat, succ_s_plus_zero)
    eq_succ_s_succ_s = app(env, eq_succ_s, succ_s)
    
    succ_branch = MatchBranch(
        constructor=Constant("S"),
        bound_vars=[s],
        body=eq_succ_s_succ_s
    )

    m = Variable('m')
    env = w_local_assum(env, m, nat)
    motive = FunctionType(n, nat.term_, eq_type.term_)

    # Create match expression with name related to the type
    match_expr = Match(
        name="nat_match",
        scrutinee=m,
        motive=motive,
        branches=[zero_branch, succ_branch]
    )
    
    theorem = match_rule(env, n, match_expr, nat_type)
    return theorem

How does it work?

If we look at the output of this:

E[Gamma]⊢((((Constant(nat_rect) λn:Constant(nat).(((Constant(eq) Constant(nat)) ((Constant(plus) Var(n)) Constant(O))) Var(n))) (((Constant(eq) Constant(nat)) Constant(O)) Constant(O))) (((Constant(eq) Constant(nat)) ((Constant(plus) (Constant(S) Var(s))) Constant(O))) (Constant(S) Var(s)))) Var(m)):(((Constant(eq) Constant(nat)) ((Constant(plus) Var(m)) Constant(O))) Var(m))

It’s almost the same⁴ as the output of the example from the induction post.

Defining Functions Using Match

Weekday

I alluded to this earlier. Let’s say we have a weekday enum defined as an inductive type:

def define_weekday(env: Environment) -> Environment:
    weekday_type = InductiveType(
        name="weekday",
        params=[],
        indices=[],
        returnType=Set(),
        constructors=[
            InductiveTypeConstructor(day, Constant("weekday"))
            for day in ["sunday", "monday", "tuesday", "wednesday", 
                       "thursday", "friday", "saturday"]
        ]
    )

    return define_inductive(env, weekday_type), weekday_type

Now let’s define functions on top of weekday. This function adds yesterday and tomorrow to our global environment.

def define_weekday_operations(env: Environment, weekday:InductiveType) -> Environment:
    days = ["sunday", "monday", "tuesday", "wednesday", "thursday", "friday", "saturday"]
    
    # Get the weekday type from environment
    w_weekday = Variable("w_weekday")
    ind_weekday = const(env, weekday)

    d_tomorrow = Variable("d_tomorrow")
    d_yesterday = Variable("d_yesterday")
    env = w_local_assum(env, d_tomorrow, ind_weekday)
    env = w_local_assum(env, d_yesterday, ind_weekday)
    
    # Create motive - maps weekday to weekday
    motive = ProductType(
        w_weekday,
        weekday,
        weekday
    )
    
    # Create branches for tomorrow
    branches_tomorrow = []
    for ind, day in enumerate(days):
        tomorrow_day = days[(ind + 1) % 7]
        branches_tomorrow.append(
            MatchBranch(
                constructor=Constant(day),
                bound_vars=[],
                body=Constant(tomorrow_day)
            )
        )

    # Create branches for yesterday
    branches_yesterday = []
    for ind, day in enumerate(days):
        yesterday_day = days[(ind - 1) % 7]
        branches_yesterday.append(
            MatchBranch(
                constructor=Constant(day),
                bound_vars=[],
                body=Constant(yesterday_day)
            )
        )

    # Create match expressions
    tomorrow = Match(
        name="tomorrow",
        scrutinee=d_tomorrow,  
        motive=motive,     
        branches=branches_tomorrow
    )

    yesterday = Match(
        name="yesterday",
        scrutinee=d_yesterday,  
        motive=motive,   
        branches=branches_yesterday
    )

    # Add functions to environment
    env = w_global_def(
        env,
        Constant("tomorrow"),
        Hypothesis(env, tomorrow, tomorrow) 
    )
    env = w_global_def(
        env,
        Constant("yesterday"),
        Hypothesis(env, yesterday, yesterday) 
    )

    return env

Reduce Match

Now, say we have Application of yesterday to a day of the week. We need a way to reduce it:

def reduce_match(term: Term) -> Term:
    if isinstance(term, Application) and isinstance(term.first, Match):
        match_expr = term.first
        arg = term.second
        
        for branch in match_expr.branches:
            if isinstance(arg, Constant) and arg.name == branch.constructor.name:
                return branch.body
    
    return term

This is a pretty naive implementation, but it reduces an application of Match by running through all the branches.

At this point, in theory, you could add reduce_match (or similar rules) to our other conversion rules, which would let us prove theorems like \(\forall \text{day}: \text{weekday}, \text{yesterday}(\text{tomorrow}(\text{day})) = \text{day}\).

Conclusion and Next Steps

In this post, we’ve implemented a basic Match construct that provides a more intuitive interface to the elimination principles. Though this implementation covers only the essentials it does demonstrate the core principles for handling Match.

We’re pretty far along in terms of a proof assistant. There is more that can be done with Match, but it’s out of scope of this post

In the game plan this post is the second half of step five. I’ve now implemented at least toy versions for most of the major aspects of a theorem prover, and proved a fair number of (trivial) theorems.

Probably I will have one more post on this Python implementation (the second half of step six, where I will attempt to tie our tactics back to the typing rules) and then a retrospective.

Footnotes

1. In general, this post is where the wheels started to fall off of this codebase. I’ll get into this in my proof assistant retrospective post.

2. At least. Presumably there are many tactics that can use matching, but that’s outside the scope of this post.

3. Note that I’ve fudged this a bit: we are getting away from the typing rules and just constructing the appropriate term. More on this in the next two posts.

4. I flipped the equal sign, so this proves \(n + 0 = n\) whereas the other proves \(n = n + 0\).