Correct By Construction First Order Logic

Idris is basically just Haskell with dependent types, so if you are familiar with Haskell, you should be able to follow along. We’ll just quickly go over some examples to get you familiar with Idris. The biggest, or at least most common, syntactic difference between Haskell and Idris is that Haskell uses :: for type annotations and (:) for the cons operator, while Idris does it the correct way.

First, let’s look at lists.

data List : Type -> Type where
  Nil  : List a
  (::) : a -> List a -> List a

This is the GADT way to define this type, but this is just a more explicit version of the usual definition³.

data List a = Nil | (::) a (List a)

Lists are great, but there is a fundamental problem with them that happens when we try to write a function to index into a list.

index : List a -> Nat -> a
index []        i     = ?uh_oh
index (x :: xs) 0     = x
index (x :: xs) (S i) = index xs i

We can write most of the function without issue, but, since we can’t guarantee that the index is in range, we have to decide what to do if the index is out of bounds. There are generally two approaches:

1. Crash. This is the approach taken by head and tail in Haskell’s standard library, though it is generally disfavored in Haskell now, since it is very easy to ignore the possibility of an error.
2. Rather than return an a, return a Maybe a. This forces the caller to handle the possibility of an error, which is a both a pro since it means that the potential error will be handled, but is also a con because it’s annoying and there can be situations where you have already verified that an error is impossible, but still have to deal with an impossible error anyway.

Dependent types allow for a third approach, namely require the caller to prove ahead of time that errors are impossible. This is not strictly better than the other approaches, but can sometimes be a life-saver. Let’s see how we can use dependent types to fix this problem.

Here’s our definition of Vect.

data Vect : Nat -> Type -> Type
  Nil  : Vect 0 a
  (::) : a -> Vect n a -> Vect (S n) a

There’s a lot to digest here. Let’s go line by line. First, the type of Vect is Nat -> Type -> Type. This means it is a type depending on a natural number and another type. The natural number represents the length of the vector, and the type is the type of the contents of the vector.

Then, we have Nil : Vect 0 a. Remember that this is shorthand for Nil : {a : Type} -> Vect 0 a. So whenever you use Nil, Idris will try to figure out what a is from the context. Furthermore, note that we need GADTs here, since the type of Nil involves specializing the Nat argument.

Finally, we have (::) : a -> Vect n a -> Vect (S n) a. This introduces a constructor (::), which is an infix operator. It takes on its left an argument of type a, where a is again inferred from context. On its right, it takes an argument of type Vect n a. Note that n is a lower case identifier, so it is also an implicit argument, even though n is a Nat, not a type⁴. Then the resulting Vect is length S n and still holds values of type a.

Let’s type check the term [1, 2, 3], which desugars to 1 :: 2 :: 3 :: Nil as an example³. We begin with Nil, which is type Vect 0 a. Idris can’t figure out what a is quite yet. Then we get to 3 :: Nil. The relevant types are:

• 3 : Nat
• (::) : a -> Vect n a -> Vect (S n) a
• Nil : Vect 0 a.

By matching these up, Idris is able to see that a must be Nat. Idris can also see that n must be 0, even though n is a value of type Nat, rather than a type. With n = 0 and a = Nat, we then have 3 :: Nil : Vect (S 0) Nat, and S 0 = 1, so 3 :: Nil : Vect 1 Nat. Then we have

• 2 : Nat
• (::) : a -> Vect n a -> Vect (S n) a
• Nil : Vect 1 a=.

Idris is again able to match these types and conclude that a = Nat and n = 1. This means that 2 :: 3 :: Nil must be type Vect (S 1) Nat = Vect 2 Nat.

Finally, Idris can do this one more time to conclude that 1 :: 2 :: 3 :: Nil : Vect 3 Nat.

We can write normal functions on vectors without much issue. One easy one is map : (a -> b) -> Vect n a -> Vect n b.

map : (a -> b) -> Vect n a -> Vect n b
map f []        = []
map f (x :: xs) = f x :: map f xs

Note that we are casually proving that mapping a function over a list doesn’t change its length. By the way, implementing this interactively is quite the experience. Since this function is actually the only possible function with this type signature⁵, Idris is able to write almost the entire function by itself.

Incidentally, better tooling is another good argument for stronger types, since stronger types means the compiler understands your program better and can help you out more.

One standard function that works, but is much more complicated than it first appears is append.

(++) : Vect n a -> Vect m a -> Vect (n + m) a
[]        ++ ys = ys
(x :: xs) ++ ys = x :: (xs ++ ys)

The standard definition seems to work just fine. However, this is incredibly fragile, and we are really quite lucky that this works out. You might rightly wonder how Idris can tell that the output is length n + m. It turns out that this works because we exactly follow the definition of addition. One major downside to dependent types is that, since values can appear in types, implementation can become part of the interface. Here is how addition is defined.

(+) : Nat -> Nat -> Nat
0     + y = y
(S x) + y = S (x + y)

If addition had been defined as follows instead, then the previous definition of append would no longer type check.

(+) : Nat -> Nat -> Nat
x + 0     = x
x + (S y) = S (x + y)

Let’s look closely at the lengths of the vectors in the implementation of append. In the first clause we have [] ++ ys = ys. [] is just shorthand for Nil, which we know is type Vect 0 a. All we know about ys is that it is type Vect m a. The return value in this situation is ys, which again is type Vect m a. What Idris does to type check in this situation is it attempts to unify the actual return type, Vect m a, with the declared return type, Vect (n + m) a. But since n = 0, we have Vect (0 + m) a. It can immediately see from the first clause of the definition of addition that 0 + m = m, so Vect m a unifies with Vect (n + m) a.

The second clause is more complicated. Here are the relevant types:

• x : a
• xs : Vect k a
• x :​: xs : Vect (S k) a
• ys : Vect m a
• xs ++ ys : Vect (k + m) a (since xs : Vect k a and ys : Vect m a, inductively assuming append to be well-typed yields Vect (k + m) a for the type of xs ++ ys)
• x :​: (xs ++ ys) : Vect (S (k + m)) a

In this situation, n = S k. Our final return value was type Vect (S (k + m)) a. The declared return value is Vect (n + m) a = Vect (S k + m) a. Looking at the second clause in the definition of addition, we see S k + m = S (k + m), so these two types do in fact unify.

The specific implementation of addition ends up impacting whether or not append type checks. This is what I mean when I say that, with dependent types, the implementation is part of the interface⁶. This is so tricky, in fact, that in Idris there are three levels of exporting something:

1. private. The default. This means that the function/type/interface/etc. is not exported at all.
2. export. This means that the type of the definition is exported, but only the type, not the implementation.
3. public export. This means that both the type and implementation are exported. This is longer and more cumbersome to type on purpose, and should only be reserved for definitions that are intended to occur in types.

That was tricky, but things get even trickier with reverse.

reverse : Vect n a -> Vect n a
reverse []        = []
reverse (x :: xs) = reverse xs ++ [x]

This standard definition seems like it would be fine, but doesn’t actually type check. Instead we get the error message

While processing right hand side of reverse. Can’t solve constraint between: plus n 1 and S n.

with reverse xs ++ [x] highlighted. The problem here is that reverse xs ++ [x] is type Vect (n + 1) a, while the return type should be Vect (S n) a. While S n is obviously equal to n + 1, Idris can’t see that. Recall that, in the definition of addition, we recurred on the first argument. In n + 1, we can’t further simplify, since we can’t tell whether n = 0 or n = S k for some k. We would have to somehow convince Idris that these two types are the same. It is possible to do this, but it’s a pretty significant diversion, and doesn’t really come up later. Look here for a brief overview of how to solve this, and here for a lot more detail.

reverse and append were tricky, but let’s finally look at indexing into a vector. We know that a vector of type Vect k a has k elements, but how can we restrict the index to be less than k?

A first order language \(\mathcal{L}\) has some specified function and relation symbols, with specified arities. For example, the language \(\mathcal{L}_{\mathrm{NT}}\) of number theory might have binary function symbols \(+\) and \(\cdot\), a unary function symbol \(S\), a nullary function symbol (constant symbol) \(0\), and a binary relation symbol \(\leq\). Some example terms in this language might include \(S S S 0 + S S 0\), or \(S(S(0 + S 0 \cdot S 0) \cdot S S S 0)\), or \(x + S y\) (since we have variables for free). Importantly, terms like \(+(0(S(x, y)), 0)\) are not correct, since the arities are incorrect; the function symbols are not given the correct number of arguments.

We can relate terms via the relation symbols, as well as equality, which we always assume to have for free. So some example simple formulas of \(\mathcal{L}_{\mathrm{NT}}\) are \(x + y = y + x\), \(S x \leq x \cdot 2\), \(x \cdot y = S(0 + S S y)\) (these formulas don’t need to be true). We can also combine formulas together with the standard connectives \(\wedge\) (and), \(\vee\) (or), \(\to\) (implies), and \(\neg\) (not). We can also use the quantifiers \(\forall\) and \(\exists\), meaning “for all” and “there exists” respectively. So \[ \forall x\, \forall y\, [x \leq y \wedge \neg (x = y) \to y \leq x] \] states that for every \(x\) and \(y\), if \(x \leq y\) but \(x \neq y\), then \(y \leq x\).

We might also have the language of group theory \(\mathcal{L}_{\mathrm{G}} = \{\cdot,\,e\}\). We can then state the group axioms as:

1. \(\forall x\, [x \cdot e = x \wedge e \cdot x = x]\)
2. \(\forall x\, \forall y\, \forall z\,[x \cdot (y \cdot z) = (x \cdot y) \cdot z]\)
3. \(\forall x\,\exists y [x \cdot y = e \wedge y \cdot x = e]\).

It’s also occasionally convenient to add the symbol \(\bot\) meaning false. You can treat it as an abbreviation for \(\neg \forall x\, [x = x]\) or some similar such formula.

We can also formalize what proofs look like. There are a million ways to do this, and the details don’t particularly matter, but we will discuss one simple proof system similar to what we will formalize in Idris later. Proofs will be relative to a context of local assumptions, often denoted \(\Gamma\). The notation \(\Gamma \vdash \phi\) means that you can prove \(\phi\) in the context \(\Gamma\). The proof system consists of several rules indicating what you can prove in what contexts. Here are some example rules for manipulating conjunctions.

\(\wedge I\)

if \(\Gamma \vdash \phi\) and \(\Gamma \vdash \psi\), then \(\Gamma \vdash \phi \wedge \psi\).

\(\wedge E_\ell\)

if \(\Gamma \vdash \phi \wedge \psi\), then \(\Gamma \vdash \phi\).

\(\wedge E_r\)

if \(\Gamma \vdash \phi \wedge \psi\), then \(\Gamma \vdash \psi\).

The whole point of the context is to include assumptions or hypotheses. So we will have a rule \(\mathrm{hyp}\), short for hypothesis, that says that we can prove, from our assumptions, any of our assumptions.

\(\mathrm{hyp}\)

if \(\phi \in \Gamma\), then \(\Gamma \vdash \phi\).

There is a particular format that we often write these rules in. We will place the hypotheses, draw a horizontal line, and put the conclusion below the line. We usually will also put the rule in parentheses to the right of the line. So the rule \(\wedge I\) looks like this:

If a rule has no hypotheses, like \(\mathrm{hyp}\), we put a blank line.

Then we can make a proof by stacking these deductions one after the other, making a big tree.

Here’s a proof that \(\phi \wedge \psi \vdash \psi \wedge \phi\).

Don’t worry too much about the details. We will see a lot more of this later. Let’s get on with actually implementing this in Idris!

Our signatures will need function and relation symbols. First, here’s a representation of function and relation symbols.

record FuncSym where
  constructor MkFuncSym
  name  : String
  arity : Nat

record RelSym where
  constructor MkRelSym
  name  : String
  arity : Nat

Function and relation symbols each have a name and arity. I haven’t introduced records, but this is approximately equivalent to the following definition.

data FuncSym = MkFuncSym String Nat

name : FuncSym -> String
name (MkFuncSym name _) = name

arity : FuncSym -> Nat
arity (MkFuncSym _ arity) = arity

While record projections are just in the regular function namespace, Idris is a lot less picky about stuff like this than Haskell. It is abundantly clear from the types which projection function is intended.

Then a signature just consists of some relation and function symbols.

record Signature (n, m : Nat) where
  constructor MkSignature
  funcs : Vect n FuncSym
  rels  : Vect m RelSym

We are using a vector here because, rather than indicate function and relation symbols by name, we will indicate them by index into this vector, so our representation of a function symbol in a term will be a Fin n. That way it is impossible to give a string that doesn’t refer to any function symbol.

Getting the arity of a function or relation symbol just from the index will come in handy.

funcArity : Signature n _ -> Fin n -> Nat
funcArity (MkSignature funcs rels) i = (index i funcs).arity

relArity : Signature _ m -> Fin m -> Nat
relArity (MkSignature funcs rels) i = (index i rels).arity

And that’s about it for Signature. Things get much more interesting when we move on to Term’s. Before we do that though, let’s build up an implementation of \(\mathcal{L}_{\mathrm{NT}}\) as an example.

Zero is a nullary function symbol.

zero : FuncSym
zero = MkFuncSym "0" 0

\(S\) is a unary function symbol.

suc : FuncSym
suc = MkFuncSym "S" 1

We also have \(+\) and \(\cdot\) as binary function symbols.

plus : FuncSym
plus = MkFuncSym "+" 2

times : FuncSym
times = MkFuncSym "*" 2

And, finally, \(\leq\) is a binary relation symbol.

leq : RelSym
leq = MkRelSym "<=" 2

Then we can package these together into a signature.

NT : Signature 4 1
NT = MkSignature
  [ zero, suc, plus, times ]
  [ leq ]

Here’s the definition of a Term.

data Term : Signature nFuncs nRels -> Nat -> Type where
  Var  : Fin n -> Term sig n
  Func : (i : Fin nFuncs) -> Vect (funcArity sig i) (Term sig n) -> Term sig n

This is a lot to unpack. Term is a Type, depending on a Signature with nFuncs function symbols and nRels relation symbols, as well as a Nat. The meaning of the Signature is clear, but the Nat less so. The Nat indicates an upper bound on the number of variables that can occur, which will be very handy later. So in the term \(1 + 1\), there aren’t any variables, meaning n can be anything. But in the term \(x + y\), there are two variables, so n needs to be at least 2.

There will implicitly be a list of variables available, more on this once we get to formulas, so Var takes an index into this list. We can imagine having a list of variables, say \(x,\, y,\, z\). Then Var 0 corresponds to \(x\), Var 1 to \(y\), and Var 2 to \(z\). This is why we need an upper bound on the number of variables occurring in the term.

Then the Func constructor is what made me switch from Haskell to Idris and get very excited. Func takes an i : Fin nFuncs, an index into the list of function symbols of the signature, and a Vect (funcArity sig i) (Term sig n). This is the argument list. It has length funcArity sig i, the arity of the function symbol with index i in the signature sig, and its elements are type Term sig n, that is terms from signature sig with the same upper bound on the number of variables as the main term.

This is confusing, so let’s create some terms in the language \(\mathcal{L}_\mathrm{NT}\) to get a feel for it. Let’s start with the term \(1 + 1\), or rather \(S 0 + S 0\). First the type signature. It is a term in the language \(\mathcal{L}_{\mathrm{NT}}\) with no variables, so that would make it a Term NT 0.

s0ps0 : Term NT 0
s0ps0 = Func 2
  [ Func 1 [ Func 0 [] ]
  , Func 1 [ Func 0 [] ]
  ]

The second element in our list of functions was plus, so the outermost Func is index 2. Likewise, suc is index 1 and zero is index 0.

If we had made a mistake and left off the second argument to plus, for example, we would get the following.

s0ps0' : Term NT 0
s0ps0' = Func 2
  [ Func 1 [ Func 0 [] ] ]

Then Idris would get very upset and give the following error message:

- + Errors (1)
 `-- src/Test.idr line 35 col 2:
     While processing right hand side of s0ps0'. When unifying:
         1
     and:
         2
     Mismatch between: 0 and 1.

     Test:35:3--35:25
      32 | 
      33 | s0ps0' : Term NT 0
      34 | s0ps0' = Func 2
      35 |   [ Func 1 [ Func 0 [] ] ]
             ^^^^^^^^^^^^^^^^^^^^^^

It’s not the most helpful error message in the world, but the 1 and 2 it’s unifying are from the length of the vector given as the argument list to Func 1 and evaluating funcArity NT 1, the expected argument length.

But if we take a step back for a moment, this is absolutely incredible. Giving the wrong number of arguments to a function symbol is a type error! When doing further analysis of terms later, we never need to deal with wrong numbers of arguments, since the type system guarantees, statically, that everything is correct. All the errors are taken care of at compile time⁷!

Working with the Func constructors directly is a bit of a pain, so let’s make some handy abbreviations.

A bit of a nasty trick I learned from Rocq is to use O (a capital ’o’) to represent zero if zero is already taken and 0 doesn’t work as an identifier. It works surprisingly well.

O : Term NT d
O = Func 0 []

Then we can make a function S : Term NT d -> Term NT d, such that for any term t, S t is the term \(S t\).

S : Term NT d -> Term NT d
S t = Func 1 [ t ]

Likewise, we can get a little fancy and implement \(+\) and \(\cdot\) as infix operators.

(+) : Term NT d -> Term NT d -> Term NT d
s + t = Func 2 [ s, t ]

(*) : Term NT d -> Term NT d -> Term NT d
s * t = Func 3 [ s, t ]

Now we can write the same term as before as S O + S O, which is significantly easier to read. We even get the precedence right, so we can do things like S O + S O * S (S O) and have it parse correctly as \(S 0 + S 0 * S S 0\).

Let’s start making logical formulas!

The definition of Formula is similar to Term.

data Formula : Signature nFuncs nRels -> Nat -> Type where
  Equal  : Term sig n -> Term sig n -> Formula sig n
  Rel    : (i : Fin nRels) -> Vect (relArity sig i) (Term sig n) -> Formula sig n
  Imp    : Formula sig n -> Formula sig n -> Formula sig n
  Bot    : Formula sig n
  Forall : Formula sig (S n) -> Formula sig n

Formula is again indexed by a signature and a Nat, and we have some constructors for making various formulas. It might seem like we don’t have enough, but it turns out this is actually enough to define anything (\(\neg \phi = \phi \to \bot\), then \(\phi \wedge \psi = \neg (\phi \to \neg \psi)\), \(\phi \vee \psi = \neg (\neg \phi \wedge \neg \psi)\), \(\exists x\, \phi = \neg \exists x \,\neg \phi\), etc.). Rel is very similar to Func from Term, in that it takes an index into the list of relation symbols and a vector of arguments of the appropriate length.

We can now start to go into how variables work in a bit more detail. The Nat, rather than just being an upper bound on the number of variables, is, more precisely, an upper bound on the number of free variables that occur in a formula. This was the same as the number of variables in Term, since Term doesn’t have any binders, but Formula does.

What Forall does, is it takes a formula with \(n + 1\) free variables, and binds a variable, leaving only \(n\) free variables. For example, suppose \(\phi\) is a formula with \(n + 1\) free variables, say \(x_1, x_2, \dots, x_n, x_{n+1}\). Then we can write \(\phi(x_1, \dots, x_n, x_{n+1})\). Then the formula \(\forall y\, [\phi(x_1, \dots, x_n, y)]\) only has \(n\) free variables, since \(y\) is now bound.

This begs the question, how does Forall actually bind variables? What associates a variable with a particular quantifier? I’m using De Bruijn indices. So variables are numbers, and the number indicates the number of binders between the variable and its binder. Let’s work through an example. Take the formula \(\forall x\, [(\forall y\, [x \leq y]) \to x = 0]\). This has no free variables, so it is type Formula NT n for any n. If we look at \(x \leq y\), there is one binder between \(x\) and where it is bound, so this occurrence of \(x\) has a De Bruijn index of \(1\). On the other hand, there aren’t any binders between \(y\) and its binder, so this occurrence of \(y\) has a De Bruijn index of \(0\). However, notice that the second occurrence of \(x\) is out of scope of \(y\), so there aren’t any binders between it and its binder, meaning this occurrence of \(x\) has a De Bruijn index of \(0\). So we can translate this formula into \(\forall \, [(\forall \, [1' \leq 0']) \to 0' = 0\), where the primes indicate indices.

You can also think of the Nat index as being the smallest number of quantifiers you would need to add in order to bind every variable.

Let’s continue our NT example. Before we do, though, let’s make some abbreviations. First we will abbreviate equality and \(\leq\).

infix 1 .=
(.=) : Term sig n -> Term sig n -> Formula sig n
(.=) = Equal

(<=) : Term NT n -> Term NT n -> Formula NT n
t1 <= t2 = Rel 0 [ t1, t2 ]

We can also make an infix version of Imp.

infixr 2 ==>
(==>) : Formula sig n -> Formula sig n -> Formula sig n
(==>) = Imp

We can also define negation in terms of Imp and Bot.

Not : Formula sig n -> Formula sig n
Not phi = phi ==> Bot

Then we can define conjunction in terms of Imp and Not.

(&&) : Formula sig n -> Formula sig n -> Formula sig n
phi && psi = Not (phi ==> Not psi)

Then we can also define disjunction.

(||) : Formula sig n -> Formula sig n -> Formula sig n
phi || psi = Not (Not phi && Not psi)

With these abbreviations established, let’s state some interesting facts about number theory.

Let’s state that addition is commutative. This would be \(\forall x\, \forall y\, [x + y = y + x]\). Our translation into Idris is as follows. First, we need to find all the De Bruijn indices. There aren’t any binders between \(y\) and its binder, and there is one between \(x\) and its binder, so we have \(\forall \, \forall\, [1' + 0' = 0' + 1']\). From here, it’s pretty straightforward to translate this to Idris.

addComm : Formula NT n
addComm = Forall (Forall (Var 1 + Var 0 .= Var 0 + Var 1))

We can even translate that complicated example from before into Idris no problem.

harderFormula : Formula NT n
harderFormula = Forall (Forall (Var 1 <= Var 0) -> Var 0 .= O)

Let’s translate all the Peano Axioms into Idris here. These are the axioms used as a foundation for number theory.

First, we have that \(0\) is not a successor, formally stated as \(\forall x\,[\neg 0 = S x]\). We can translate this easily enough.

zeroNotSuc : Formula NT d
zeroNotSuc = Forall (Not (O .= S (Var 0)))

Next we have that the successor function is injective, stated as \(\forall x\, \forall y\, [S x = S y \to x = y]\). This isn’t too difficult to translate to Idris.

sucInj : Formula NT d
sucInj = Forall (Forall (S (Var 0) .= S (Var 1) ==> Var 0 .= Var 1))

We also want \(x + 0 = x\), which we can state as below.

addZeroR : Formula NT d
addZeroR = Forall (Var 0 + O .= Var 0)

For convenience, and now that we’re more comfortable with De Bruijn indices, let’s establish the convention that \(y\) is the most recently bound variable, and \(x\) bound before that. Then we can make the abbreviations shown below.

Y : Term sig (S d)
Y = Var 0

X : Term sig (S (S d))
X = Var 1

This makes the formulas a little more natural looking.

We want \(\forall x\, \forall y\,[x + Sy = S(x + y)]\), which intuitively is true, since \(x + (y + 1) = (x + y) + 1\).

addSR : Formula NT d
addSR = Forall (Forall (X + S Y .= S (X + Y)))

Anything times zero is zero, so we should have \(\forall y\,[y \cdot 0 = 0]\). Note that we use \(y\) here, since it’s the most recently bound variable.

mulZeroR : Formula NT d
mulZeroR = Forall (Y * O .= O)

We want \(x \cdot (y + 1) = x \cdot y + x\), or \(\forall x\, \forall y\, [x \cdot S y = x \cdot y + x]\).

mulSucR : Formula NT d
mulSucR = Forall (Forall (X * S Y .= X * Y + X))

The final axiom is the most difficult. This is the axiom schema of induction. It says that for every formula \(\phi\) with at least one free variable \(x\), the following formula is an axiom: \[ \phi(0) \to (\forall x\, [\phi(x) \to \phi(S x)]) \to \forall x\, [\phi(x)] \] In English, if \(\phi(0)\) holds, and whenever \(\phi(x)\) holds, \(\phi(S x)\) holds, then \(\phi\) holds for every \(x\).

The way we are going to implement this is by making a function of type Formula NT (S d) -> Formula NT d. It will take a formula \(\phi\) with at least one free variable (i.e. a argument phi : Formula NT (S d)) and output the previously mentioned formula.

In order to do this, we do need the notion of substitution. The details are technical and very annoying, so I will be skipping them here. All the code is available here if you want to see the details. Here’s the implementation of induction⁸.

induction : {d : _} -> Formula NT (S d) -> Formula NT d
induction phi =
  elimBinder O phi ==>                            -- phi(0) ->
  (Forall (phi ==> (sub 0 (S Y) phi))) ==>        -- (forall x, [phi(x) -> phi(S x)]) ->
  Forall phi                                      -- forall x, [phi(x)]

I know I’m itching to prove something using these axioms, so let’s get into proofs!

I mentioned before that proofs are relative to a context, so we need some notion of a context. I implemented a type Context : Signature n m -> Nat -> Type that you can think of as a Vect k (Formula sig n), but the n’s on each formula are allowed to vary. The actual details of how this works don’t particularly matter, but the details are all available here.

With this out of the way, we can finally get to Proof! Here is the definition of Proof:

data Proof : Context sig g -> Formula sig n -> Type where
  Hyp     : {c : Context sig g} -> (i : Fin g) -> Proof c (snd (index i c))
  Weaken  : Proof c1 phi -> Subset c1 c2 -> Proof c2 phi
  ImpI    : Proof (phi :: c) psi -> Proof c (Imp phi psi)
  ImpE    : Proof c (Imp phi psi) -> Proof c phi -> Proof c psi
  ForallI : Proof c phi -> Proof c (Forall phi)
  ForallE : Proof c (Forall phi) -> Proof c (elimBinder t phi)
  BotE    : Proof c Bot -> Proof c phi
  Contra  : Proof (Not phi :: c) Bot -> Proof c phi  
  EqI     : Proof c (Equal t t)
  EqE     : {phi : Formula sig (S n)} -> Proof c (Equal s t) -> Proof c (elimBinder s phi) -> Proof c (elimBinder t phi)

An object of type Proof Gamma phi represents a proof of \(\phi\) in context \(\Gamma\), i.e. a witness that \(\Gamma \vdash \phi\). Each constructor in this type corresponds to a rule you can use to create a proof. Let’s go over each of these rules.

Let’s start by proving some very basic facts.