Typing Rules

Reasoning
Exposition
Published

November 30, 2024

Tauber-Arp. *Composition* (1930)

Introduction

How can we tell if a term is well-typed? How can we tell if an environment is well-formed? We can be sure we have formed a proper term and environment (in the Calculus of Constructions) if we constructed the term and environment using the so-called typing rules.

There’s 16 typing rules in total, but many of the rules are analogous. I’ll go through them one-by-one.

Hypotheses

To start, we need some representation of a well-formed type. This class, Hypothesis, contains an environment, a term, and a type. Many of our typing rules will manipulate Hypothesis, either by using it as an input, or by returning Hypothesis as an output.

class Hypothesis:
    def __init__(self, environment:Environment, term_:Term, type_:Type):
        self.globalEnvironment = environment.globalEnvironment
        self.localContext = environment.localContext
        self.term_ = term_
        self.type_ = type_
    def __repr__(self):
        return f"{self.globalEnvironment.name}[{self.localContext.name}]⊢{self.term_}:{self.type_}"

There’s not much to the implementation. It just wraps up classes we’ve already seen.

Typing Rules

We read the typing rules from top-down. Given the conditions on the top of each rule, we can construct the term on the bottom.

Empty Environments

The first rule is W-Empty. This rule simply introduces an empty environment.
\[\small \begin{flalign} \frac{}{\text{W}([])[]} \end{flalign} \]

Here’s the code. We construct a local and global context, and then return the composite Environment object.

def w_empty(global_name='E', local_name='Gamma') -> Environment:
    global_env = GlobalEnvironment(global_name)
    local_context = LocalContext(local_name)
    return Environment(global_env, local_context)

Note that this function doesn’t require any arguments. We will call this at the beginning of every proof, to get the proof started.

Axioms for Sorts

The next set of rules lets us introduce various Sorts into an environment.

\[\small \begin{flalign} \frac{ W(E)[\Gamma] }{ E[\Gamma] \vdash \mathsf{SProp} : \mathsf{Type}(1) } \end{flalign} \]

\[\small \begin{flalign} \frac{ W(E)[\Gamma] }{ E[\Gamma] \vdash \mathsf{Prop} : \mathsf{Type}(1) } \end{flalign} \]

\[\small \begin{flalign} \frac{ W(E)[\Gamma] }{ E[\Gamma] \vdash \mathsf{Set} : \mathsf{Type}(1) } \end{flalign} \]

\[\small \begin{flalign} \frac{ W(E)[\Gamma] }{ E[\Gamma] \vdash \mathsf{Type}(i) : \mathsf{Type}(i+1) } \end{flalign} \]

There’s four different axioms: one for SProp, one for Prop, one for Set, and one for Type(i).

Below are the code implementations.

def ax_sprop(environment:Environment):
    return Hypothesis(environment, SProp(), Type())

def ax_prop(environment:Environment):
    return Hypothesis(environment, Prop(), Type()) 

def ax_set(environment:Environment):
    return Hypothesis(environment, Set(), Type())

def ax_type(environment:Environment, i: int):
    return Hypothesis(environment, Type(i), Type(i + 1))

There aren’t any checks here, so we can introduce our axioms about Sorts even in an empty environment.

Constants and Variables

The next four rules relate to adding variables and constants to the local and global contexts.

We can either assume a variable/constant, or define a variable/constant. We can assume a variable/constant so long as the name is fresh and it’s type is a Sort. Assumed variables go in the local context, assumed constants go in the global context.

Here’s W-Local-Assum and W-Global-Assum:

\[\small \begin{flalign} \frac{ \text{W}(\Gamma)[E] \quad s \in S \quad x \notin \Gamma }{ \text{W}(E)[\Gamma::(x:T)] } \end{flalign} \]

\[\small \begin{flalign} \frac{ E[] \vdash T:s \quad s \in S \quad c \notin \Gamma }{ \text{W}(E; c:T)[] } \end{flalign} \]

And here are the code implementations. The asserts check to make sure we do indeed have a sort, and that the variable/constant name doesn’t already exist1.

def w_local_assum(environment:Environment, variable:Variable, hyp:Hypothesis) -> Environment:
    assert variable.name not in environment.localContext.body() 
    assert variable.name not in environment.globalEnvironment.body()
    assert isinstance(hyp.type_, (Type, Prop, Set, SProp)) 
    newLocalContext = environment.localContext.assume_term(variable, hyp.term_)
    return Environment(environment.globalEnvironment, newLocalContext)

def w_global_assum(environment:Environment, variable:Variable, hyp:Hypothesis) -> Environment: 
    assert variable.name not in environment.localContext.body() 
    assert variable.name not in environment.globalEnvironment.body()
    assert isinstance(hyp.type_, (Type, Prop, Set, SProp)) 
    newGlobalEnv = environment.globalEnvironment.assume_term(variable, hyp.term_)
    return Environment(newGlobalEnv, environment.localContext)

If we have some well-formed term \(t\) of type \(T\), we can also give it a new name by adding a definition to the local context (W-Local-Def) or global environment (W-Global-Def) using our local and global definition rules2.

\[\small \begin{flalign} \frac{ E[\Gamma] \vdash t:T \quad x \notin \Gamma }{ \text{W}(E)[\Gamma :: (x:=t:T)] } \end{flalign} \]

\[\small \begin{flalign} \frac{ E[] \vdash t:T \quad c \notin E }{ \text{W}(E; c:=t:T)[] } \end{flalign} \]

Here’s the associated code, complete with checks to ensure no duplicate names.

def w_local_def(environment:Environment, variable:Variable, hyp:Hypothesis) -> Environment:
    assert variable.name not in environment.localContext.body() 
    assert variable.name not in environment.globalEnvironment.body()
    newLocalContext = environment.localContext.define_term(variable, hyp.term_, hyp.type_)
    return Environment(environment.globalEnvironment, newLocalContext)

def w_global_def(environment:Environment, variable:Variable, hyp:Hypothesis) -> Environment:
    assert variable.name not in environment.localContext.body() 
    assert variable.name not in environment.globalEnvironment.body()
    newGlobalEnv = environment.globalEnvironment.define_term(variable, hyp.term_, hyp.type_)
    return Environment(newGlobalEnv, environment.localContext)

Now, assuming we have an environment, and either an assumed variable \(x\) of type \(T\) or a defined variable \(x\) defining \(t\) of type \(T\) in that environment, we can construct a hypothesis showing that that variable or constant is a well-formed term of type \(T\)3. These are the Var and Const rules:

\[\small \begin{flalign} \frac{ W(E)[\Gamma] \quad (x:T) \in \Gamma \text{ or } (x := t:T) \in \Gamma \text{ for some }t }{ E[\Gamma] \vdash x : T } \end{flalign} \]

\[\small \begin{flalign} \frac{ W(E)[\Gamma] \quad (c:T) \in E \text{ or } (c := t:T) \in E \text{ for some }t }{ E[\Gamma] \vdash c : T } \end{flalign} \]

The common pattern in proofs using the typing rules will be: 1. construct the appropriate type 2. assume or define variables/constants of that type 3. introduce the hypothesis showing that variable/constant is well-formed.

Here’s the code for var and const:

def var(environment: Environment, variable: Variable):
    if variable.name in environment.localContext.assumed_terms:
        term_type = environment.localContext.assumed_terms[variable.name]
        return Hypothesis(environment, variable, term_type)
    
    if variable.name in environment.localContext.defined_terms:
        term_type = environment.localContext.defined_terms[variable.name].type_
        return Hypothesis(environment, variable, term_type)
        
    raise Exception(f"No such variable of name {variable.name}.")

def const(environment: Environment, constant: Constant):
    if constant.name in environment.globalEnvironment.assumed_terms:
        term_type = environment.globalEnvironment.assumed_terms[constant.name]
        return Hypothesis(environment, constant, term_type)
    
    if constant.name in environment.globalEnvironment.defined_terms:
        term_type = environment.globalEnvironment.defined_terms[constant.name].type_
        return Hypothesis(environment, constant, term_type)
        
    raise Exception(f"No such constant of name {constant.name}.")

Note that, as in the definition, we have to check to make sure that the variable or constant does indeed exist in the environment.

Product Types

There’s four variations of the product type construction rules: one for each type of Sort (SProp, Prop, Set, Type). They’re called Prod-SProp, Prod-Prop, Prod-Set, and Prod-Type.

\[\small \begin{flalign} \frac{ E[\Gamma] \vdash T : s \quad s \in S \quad E[\Gamma :: (x:T)] \vdash U : \mathsf{SProp} }{ E[\Gamma] \vdash \forall x:T,U : \mathsf{SProp} } \end{flalign} \]

\[\small \begin{flalign} \frac{ E[\Gamma] \vdash T : s \quad s \in S \quad E[\Gamma :: (x:T)] \vdash U : \mathsf{Prop} }{ E[\Gamma] \vdash \forall x:T,U : \mathsf{Prop} } \end{flalign} \]

\[\small \begin{flalign} \frac{ E[\Gamma] \vdash T : s \quad s \in \{\mathsf{Prop}, \mathsf{Set}\} \quad E[\Gamma :: (x:T)] \vdash U : \mathsf{Set} }{ E[\Gamma] \vdash \forall x:T,U : \mathsf{Set} } \end{flalign} \]

\[\small \begin{flalign} \frac{ E[\Gamma] \vdash T : s \quad s \in \{\mathsf{SProp}, \mathsf{Type(i)}\} \quad E[\Gamma :: (x:T)] \vdash U : \mathsf{Type(i)} }{ E[\Gamma] \vdash \forall x:T,U : \mathsf{Set} } \end{flalign} \]

There’s a fair amount going on in the above rules, but they are all pretty similar. We need (a) a hypothesis representing a well-formed term \(T:s\), where \(s\) is of the appropriate Sorts (depending on the Prod rule), and (b) a hypothesis representing a well-formed term \(U\).

If we have those inputs, we can produce a hypothesis of a product type:

def prod_sprop(environment: Environment, x: Variable, hyp_sort_type: Hypothesis, hyp_sprop_type: Hypothesis) -> Hypothesis:
    T1 = hyp_sprop_type.localContext.body()[x.name]
    assert terms_equal(environment, hyp_sort_type.term_, T1) 

    term_is_sprop = terms_equal(environment, hyp_sort_type.type_, SProp())
    term_is_prop = terms_equal(environment, hyp_sort_type.type_, Prop())
    term_is_set = terms_equal(environment, hyp_sort_type.type_, Set())
    term_is_type = isinstance(hyp_sort_type.type_, Type)
    assert term_is_sprop or term_is_prop or term_is_set or term_is_type 

    assert terms_equal(environment, hyp_sprop_type.type_, SProp())

    assert x.name in hyp_sprop_type.localContext.body() 
    assert x.name not in hyp_sort_type.localContext.body()

    T2 = hyp_sort_type.term_
    assert terms_equal(environment, T1, T2)
    product = ProductType(x, T1, hyp_sprop_type.term_)
    return Hypothesis(environment, product, SProp())

def prod_prop(environment: Environment, x: Variable, hyp_sort_type: Hypothesis, hyp_prop_type: Hypothesis) -> Hypothesis:
    T1 = hyp_prop_type.localContext.body()[x.name]
    assert terms_equal(environment, hyp_sort_type.term_, T1) 

    term_is_sprop = terms_equal(environment, hyp_sort_type.type_, SProp())
    term_is_prop = terms_equal(environment, hyp_sort_type.type_, Prop())
    term_is_set = terms_equal(environment, hyp_sort_type.type_, Set())
    term_is_type = isinstance(hyp_sort_type.type_, Type)
    assert term_is_sprop or term_is_prop or term_is_set or term_is_type 

    assert terms_equal(environment, hyp_prop_type.type_, Prop())

    assert x.name in hyp_prop_type.localContext.body() 
    assert x.name not in hyp_sort_type.localContext.body()

    T2 = hyp_sort_type.term_
    assert terms_equal(environment, T1, T2)

    product = ProductType(x, T1, hyp_prop_type.term_)
    return Hypothesis(environment, product, Prop())

def prod_set(environment: Environment, x: Variable, hyp_sort_type: Hypothesis, hyp_set_type: Hypothesis) -> Hypothesis:
    T1 = hyp_set_type.localContext.body()[x.name]
    assert terms_equal(environment, hyp_sort_type.term_, T1) 
    
    term_is_sprop = terms_equal(environment, hyp_sort_type.type_, SProp())
    term_is_prop = terms_equal(environment, hyp_sort_type.type_, Prop())
    term_is_set = terms_equal(environment, hyp_sort_type.type_, Set())
    assert term_is_set or term_is_prop or term_is_sprop 

    assert terms_equal(environment, hyp_set_type.type_, Set())

    assert x.name in hyp_set_type.localContext.body() 
    assert x.name not in hyp_sort_type.localContext.body()

    T2 = hyp_sort_type.term_
    assert terms_equal(environment, T1, T2)
    product = ProductType(x, T1, hyp_set_type.term_)

    return Hypothesis(environment, product, Set())

def prod_type(environment: Environment, x: Variable, hyp_sort_type: Hypothesis, hyp_type_type: Hypothesis) -> Hypothesis:
    T1 = hyp_type_type.localContext.body()[x.name]
    assert terms_equal(environment, hyp_sort_type.term_, T1)
    
    equals_sprop = terms_equal(environment, hyp_sort_type.type_, SProp())
    equals_type_i = terms_equal(environment, hyp_sort_type.type_, Type(hyp_type_type.type_.n))
    assert equals_sprop or equals_type_i

    assert terms_equal(environment, hyp_type_type.type_, Type(hyp_type_type.type_.n))

    assert x.name in hyp_type_type.localContext.body() 
    assert x.name not in hyp_sort_type.localContext.body()

    T2 = hyp_sort_type.term_
    assert terms_equal(environment, T1, T2)

    product = ProductType(x, T1, hyp_type_type.term_)
    return Hypothesis(environment, product, Type(hyp_type_type.type_.n))

There’s several asserts in there to make sure everything is in order.

Lambda

Next up is forming lambdas, to bind variables.

\[\small \begin{flalign} \frac{ E[\Gamma] \vdash \forall x : T, U : s \quad E[\Gamma :: (x:T)] \vdash t : U }{ E[\Gamma] \vdash \lambda x:T.t : \forall x: T, U } \end{flalign} \]

That’s the Lam rule. We need a product type, and a term of the second element of said product type. Then we can form a hypothesis of lambda type.

def lam(environment: Environment, x: Variable, hyp1: Hypothesis, hyp2: Hypothesis) -> Hypothesis:

    assert isinstance(hyp1.term_, ProductType)
    assert hyp1.term_.variable.name == x.name

    assert x.name in hyp2.localContext.body()
    assert terms_equal(environment, hyp1.term_.term1, hyp2.localContext.body()[x.name]) 
    assert terms_equal(environment, hyp1.term_.term2, hyp2.type_)

    function = FunctionType(x, hyp1.term_.term1, hyp2.term_)
    return Hypothesis(environment, function, hyp1.term_)

Application

Application takes a (hypothesis representing) a term of a product type and a (hypothesis representing) an element of the first type of that product type, and produces the application of the first term to the second term. The intuition here is that you are “plugging in” an input to a function.

\[\small \begin{flalign} \frac{ E[\Gamma] \vdash t : \forall x: U,T \quad\quad E[\Gamma] \vdash u : U }{ E[\Gamma] \vdash (t\ u) : T[x/u] } \end{flalign} \]

Here’s the code. Note the checks on terms_equal, and the use of substitute.

def app(environment: Environment, hyp1: Hypothesis, hyp2: Hypothesis) -> Hypothesis:
    assert isinstance(hyp1.type_, ProductType)
    x = hyp1.type_.variable
    T1 = hyp1.type_.term1
    T2 = hyp1.type_.term2

    assert terms_equal(environment, hyp2.type_, T1)
    
    app_term = Application(hyp1.term_, hyp2.term_)
    result_type = substitute(T2, hyp2.term_, x)
    
    return Hypothesis(environment, app_term, result_type)

Let

The last typing rule lets us introduce let terms.

\[\small \begin{flalign} \frac{ E[\Gamma] \vdash t : T \quad E[\Gamma :: (x := t:T)] \vdash u : U }{ \Gamma \vdash \mathsf{let}\ x:=t : T\ \mathsf{in}\ u : U[x/t] }\ \end{flalign} \]

We need two hypotheses, representing \(t:T\) and \(u:U\). The second hypothesis has an additional variable defined within, matching the first hypothesis. Given those two objects, you can construct a hypothesis representing the let construct.

def let(environment: Environment, x: Variable, hyp1: Hypothesis, hyp2: Hypothesis) -> Hypothesis:
    assert x.name in hyp2.localContext.defined_terms
    defined_x = hyp2.localContext.defined_terms[x.name]
    assert terms_equal(environment, defined_x.term_, hyp1.term_)
    assert terms_equal(environment, defined_x.type_, hyp1.type_)
    
    assert x.name in hyp2.localContext.body()
    assert x.name not in hyp1.localContext.body()
    
    let_term = Let(x, hyp1.term_, hyp1.type_, hyp2.term_)
    result_type = substitute(hyp2.type_, hyp1.term_, x)
    
    return Hypothesis(environment, let_term, result_type)

Simple Proofs

Now that we’ve introduced all the rules, let’s see some examples of how they combine.

Identity Implication

This is maybe the simplest possibly theorem we can look at. Given a Prop \(P\), we should be able to prove that \(P \to P\).

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

What’s happening in the above code? Let’s break it down.

Initial Setup

# Create variables (no types yet)
p = Variable(term_name)  
P = Variable(prop_name)  

# Create empty environment
# Type: Environment
env = w_empty()

First, we create an empty environment.

Create and Introduce Proposition Type

# Hypothesis(env, Prop, Type(1))
hyp_prop = ax_prop(env)                  

# Since Type(1) is a sort, add P:Prop to the environment
env = w_local_assum(env, P, hyp_prop)

At this point, our environment contains the assumption that \(P:\mathsf{Prop}\).

Create p:P and Add to Environment

# Hypothesis(env, P, Prop)
hyp_P = var(env, P)                      

# Since Prop is a Sort, add p:P to the environment
env_with_p = w_local_assum(env, p, hyp_P)

Now our environment also contains the assumption that \(p:P\).

Build P → P Type

# Hypothesis(env_with_p, P, Prop)
hyp_with_p_P = var(env_with_p, P)        

# Hypothesis(env, ∀p:P.P, Prop)
P_implies_P = prod_prop(env, p, hyp_P, hyp_with_p_P)

This constructs the type \(P \to P\), which is written as \(\forall p:P.P\). Note the introduction of a separate environment, since the rules dictate that the newly quantified variable can only be in the second hypothesis for prod-prop.

Create Function Body

# Hypothesis(env_with_p, p, P)
hyp_p = var(env_with_p, p)               

# Hypothesis(env, λp:P.p, ∀p:P.P)
p_implies_p = lam(env, p, P_implies_P, hyp_p)

This creates the identity function \(\lambda p:P.p\) of type \(P \to P\).

Polymorphism Over P

# Hypothesis(env, ∀P:Prop.(P→P), Prop)
p_implies_p_is_prop = prod_prop(env, P, hyp_prop, P_implies_P)  

# Hypothesis(env, λP:Prop.λp:P.p, ∀P:Prop.(P→P))
theorem = lam(env, P, p_implies_p_is_prop, p_implies_p)

The final theorem has type \(\forall P:\mathsf{Prop}.(P \to P)\), meaning it works for any proposition \(P\).

Understanding the Proof

Let’s break down what this proof means logically:

  1. We start by assuming we have some arbitrary proposition \(P:\mathsf{Prop}\)
  2. We then construct a function that:
    • Takes an input \(p:P\)
    • Returns that same \(p:P\) as output
  3. This function has type \(P \to P\)
  4. Since this works for any proposition \(P\), we wrap it in a \(\forall P:\mathsf{Prop}\) quantifier

The result is a proof that for any proposition \(P\), we can construct a function that maps \(P\) to itself, proving \(P \to P\). This is the identity function at the propositional level.

If we print the output of the above code, we see the following expression:

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

Note that all of the variables, \(P\) and \(p\), are bound in the expression4.

Implication Transitivity

Here’s a slightly more complex theorem. Give Props \(P\), \(Q\), \(R\), we should have transitivity of implication. That is:

\[ \forall P:\mathsf{Prop}, \forall Q:\mathsf{Prop}, \forall R:\mathsf{Prop}, (P \to Q) \to (Q \to R) \to (P \to R) \]

The proof is below.

def prove_implication_transitivity(names=["p","q","P","Q","R","f","g"]):
    p = Variable(names[0])
    q = Variable(names[1])
    P = Variable(names[2])
    Q = Variable(names[3])
    R = Variable(names[4])
    f = Variable(names[5])
    g = Variable(names[6])

    env = w_empty()

    hyp_prop = ax_prop(env)

    env = w_local_assum(env, P, hyp_prop)
    env = w_local_assum(env, Q, hyp_prop)
    env = w_local_assum(env, R, hyp_prop)

    hyp_P = var(env, P)
    hyp_Q = var(env, Q)

    env_with_p = w_local_assum(env, p, hyp_P)
    env_with_q = w_local_assum(env, q, hyp_Q)

    hyp_p_Q = var(env_with_p, Q)
    hyp_q_R = var(env_with_q, R)
    hyp_p_R = var(env_with_p, R)

    P_implies_Q = prod_prop(env, p, hyp_P, hyp_p_Q)
    Q_implies_R = prod_prop(env, q, hyp_Q, hyp_q_R)
    P_implies_R = prod_prop(env, p, hyp_P, hyp_p_R)

    env = w_local_assum(env, f, P_implies_Q)
    env = w_local_assum(env, g, Q_implies_R)

    hyp_f = var(env, f)
    hyp_g = var(env, g)
    hyp_p = var(env_with_p, p)

    f_p = app(env, hyp_f, hyp_p)    
    g_f_p = app(env_with_p, hyp_g, f_p)

    p_to_r_hyp = lam(env, p, P_implies_R, g_f_p)

    env_with_p = w_local_assum(env_with_p, g, Q_implies_R)
    env_with_p = w_local_assum(env_with_p, f, P_implies_Q)
    hyp_pg_R = var(env_with_p, R)
    
    P_implies_R_g = prod_prop(env_with_p, p, hyp_P, hyp_pg_R)
    Q_to_R_to_P_to_R = prod_prop(env_with_p, g, Q_implies_R, P_implies_R_g)

    hyp_qr_pr = lam(env_with_p, g, Q_to_R_to_P_to_R, p_to_r_hyp)

    P_to_Q__Q_to_R__P_to_R = prod_prop(env, f, P_implies_Q, Q_to_R_to_P_to_R)
    hyp_pq_qr_pr  = lam(env_with_p, f, P_to_Q__Q_to_R__P_to_R, hyp_qr_pr)

    P_to_Q__Q_to_R__P_to_R_prop = prod_prop(env, R, hyp_prop, P_to_Q__Q_to_R__P_to_R)
    prop__P_to_Q__Q_to_R__P_to_R_prop = prod_prop(env, Q, hyp_prop, P_to_Q__Q_to_R__P_to_R_prop)
    prop_prop__P_to_Q__Q_to_R__P_to_R_prop = prod_prop(env, P, hyp_prop, prop__P_to_Q__Q_to_R__P_to_R_prop)

    theorem_R_bound = lam(env, R, P_to_Q__Q_to_R__P_to_R_prop, hyp_pq_qr_pr)
    theorem_Q_bound = lam(env, Q, prop__P_to_Q__Q_to_R__P_to_R_prop, theorem_R_bound)
    theorem = lam(env, P, prop_prop__P_to_Q__Q_to_R__P_to_R_prop, theorem_Q_bound)
    
    assert theorem.type_.variable.name == "P"
    assert theorem.type_.term2.variable.name == "Q"
    return theorem

Despite the simplicity of the theorem, the proof is rather lengthy. I won’t analyze it in detail, but printing the theorem returns the following:

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

The type representation appears correct5.

Next Steps

We’ve proved some theorems! Unfortunately, (a) these theorems are borderline trivial, and (b) despite their simplicity, it took quite a lot of code to get to the proof.

This will motivate our next two posts. First, we will handle induction, which will allow us to prove more interesting theorems. For example, we will need induction to prove theorems about the natural numbers (\(\mathbb{N}\)).

Then, we will have to build some tactics, which will help us prove theorems more easily.

If you’re following the game plan, we are through the first four steps.

Footnotes

  1. The global assumption and definition rules show an empty local context. I’m not sure if this means (a) the context must actually by empty when you use these rules or (b) ignore the local context. I’ve chosen to ignore the local context. Hopefully this won’t be important in practice.↩︎

  2. Which can then be delta-reduced.↩︎

  3. Var and Const are the same: just replace variables with constants and \(x\) with \(c\).↩︎

  4. A theorem must have no free variables - all variables must be bound by quantifiers.↩︎

  5. The __repr__ calls look a bit weird for the type here, but the last two asserts in our code proof show that the variables of those Props are indeed \(P\) and \(Q\). I may clean this up in the future.↩︎