---
tags: chapman, programming languages
---

# Theorem proving (2019)

The aim of the lecture is to show that the idea of automatically generating a parser from a context free grammar can also be applied to automatically generating a proof checker from the rules of logic.

To generate a parser from a context free grammar, we used BNFC. To generate a proof checker from a logical theory, we use two different theorem proves known as

# Isabelle and Idris

## Learning Outcomes

This lecture can only skim the surface of a rich and deep field. Here are some highlights worth remembering.

- *Interactive Theorem Provers* or *Proof Assistants* can be used to construct interactively and check automatically mathematical proofs.
- Two example proofs that show the similarity of programming and proving.
- Dependent types.
- Propositions-as-types and Curry-Howard isomorphism.
- In the proposition-as-types paradigm
- proofs are programs and programs are proofs
- mathematical induction is recursion
- the inductive case in a proof is performed by recursively calling the proof (=program) on a smaller argument.

## Introduction

[Continuing the lecture on induction](https://hackmd.io/@m5rnD-8SSPuuSHTKgXvMjg/BkHZL3jFS), I want to give the briefest introduction to two programming languages, Isabelle and Idris.

Inductive definitions and proofs can be implemented in both Isabelle and Idris in a nice way and we will look at [NumExp in Isabelle](https://github.com/alexhkurz/programming-languages-2019/blob/master/NumExp.thy) and at [NumExp in Idris](https://github.com/alexhkurz/programming-languages-2019/blob/master/NumExp.idr).

[Isabelle](https://isabelle.in.tum.de) is a special purpose programming language which can do a lot of things (even general programming), but is designed to program mathematical proofs. To explain the fundamentals of how it works we look in some detail at how to prove $1+n\approx n+1$.

**Exercise:** Install [Isabelle](https://isabelle.in.tum.de) and open the file [NumExp](https://github.com/alexhkurz/programming-languages-2019/blob/master/NumExp.thy). Read through the file in the Isabelle IDE to get a sense of how a formalisation of the previous lecture looks in an interactive theorem prover.

**Remark:** For those who want to learn more, a good point to start working with Isabelle is the book [Concrete Semantics](http://concrete-semantics.org), which is available for free online.

[Idris](https://www.idris-lang.org/) is a general purpose programming language inspired by Haskell, but with a much more powerful type system: Idris has so-called *dependent types*. And this allows us to use Idris not only as a programming language but also as a theorem prover. Indeed, types can be used to formulate properties of programs as types. For example, the $\approx$ relation becomes a type and the proof of $1+n\approx n+1$ a program of that type.

**Exercise:** (I assume here that you have done the exercise on Isabelle above first.) Install [Idris](http://docs.idris-lang.org/en/latest/tutorial/starting.html). Download [NumExp](https://github.com/alexhkurz/programming-languages-2019/blob/master/NumExp.idr). Run `idris NumExp.idr` from the command line. Run `eval_num (S O)` (where `O` is the letter `O`, not the number `0`). Consult the code in `NumExp.idr` to understand the result. Run your own variations. Compare with the Isabelle code in `NumExp.idr`. Run `plusone O`, `plusone (S O)`, etc. Try to understand in what sense the output of running `plusone (S O)` is a proof that `O+(S O)=(S O)+O`. Finally you can also run larger examples such as `comm_plus (S O) (S (S O))`. It quickly becomes clear, though, that the output is not meant to be read by humans.

**Remark:** In our Idris definition of `Num`, we pronounce the symbol `O` as "One". But feel free to read it as `0`. For what follows, it really makes no difference whether we start the numbers at zero or one.

## The language of arithmetic expressions

The language of `num` and `exp` we defined above

num ::= 1 | S num
exp ::= num | exp + exp | exp * exp

is in Isabelle defined as

datatype num = One | S num
datatype exp = Num num | Plus exp exp | Mult exp exp

We replace `1, +, *` with `One, Plus, Mult`, because the former already have a meaning in Isabelle. But this is only notation. Worth noticing is that we replace `exp::=num` by `exp=Num num`. Why the extra occurrence of `Num`? One way to think about this is as a type casting which turns a `num` into an `exp`. We didn't need to write it in our mathematical notation above because we used the convention that numbers are written as $n, \ldots$ and expressions as $e,\ldots$.

Isabelle allows us to get closer to the mathematical notation by introducing some syntactic sugar, which makes the actual code look like (but the simpler one above would work just as well)

datatype num = One ("𝟭") | S num ("_+𝟭")
datatype exp = Num num ("⟨_⟩") | Plus exp exp (infix ":+:" 14) | Mult exp exp (infix ":*:" 15)

In Idris the language is defined as

data Num = O | S Num
data Exp = N Num | (:+:) Exp Exp | (:*:) Exp Exp

where we read `O` as "One".

## Implementing a Logical Theory

In our example, the logical theory consists of

- the rules of equational reasoning
- the axiom of associativity for expressions
- the axiom $Sk=k+1$ relating the plus-one on numbers to the plus-one on expressions

This logical theory can be discribed in both Isablle and Idris in a similar way.

In Isabelle:

inductive equal_exp :: "exp ⇒ exp ⇒ bool" where
equal_exp_refl: "e ≡ex e" |
equal_exp_symm: "e1 ≡ex e2 ⟹ e2 ≡ex e1" |
equal_exp_trans: "e1 ≡ex e2 ⟹ e2 ≡ex e3 ⟹ e1 ≡ex e3" |
equal_exp_cong_plus: "e1 ≡ex e1' ⟹ e2 ≡ex e2' ⟹ e1 :+: e2 ≡ex e1' :+: e2'" |
equal_exp_plusone: "⟨n+𝟭⟩ ≡ex ⟨n⟩ :+: ⟨𝟭⟩" |
equal_exp_assoc: "(e1 :+: (e2 :+: e3)) ≡ex ((e1 :+: e2) :+: e3)"

In Idris:

data (:=:) : Exp -> Exp -> Type where
EqExpRefl : e :=: e
EqExpSymm : e1 :=: e2 -> e2 :=: e1
EqExpTrans : e1 :=: e2 -> e2 :=: e3 -> e1 :=: e3
EqExpPlusEq : e1 :=: e1' -> e2 :=: e2' -> e1 :+: e2 :=: e1' :+: e2'
EqExpPlusOne : (N (S n)) :=: (N n) :+: (N O)
EqExpAssoc : e1 :+: (e2 :+: e3) :=: (e1 :+: e2) :+: e3

These two snippets of code look almost the same. Almost all differences are purely notational and not interesting.

The one big difference that is interesting is that Isabelle has `bool` in a place where Idris has `Type`.

In Isabelle we formalise $\approx$ by a function `equal_exp` that takes two expressions and returns a truth value. This allows us to say in Isabelle whether an equation $e\approx e'$ is derivable or not.

In Idris we decided to write `:=:` instead of $\approx$ (not important difference) and `e :=: e'` is not a boolean but a type (important). So `e :=: e'` is treated in the same way as `Num`or `Exp`. Indeed, `e :=: e'` is a data type. Notice that the type `e :=: e'` is *dependent* on the terms `e` and `e'`.

So why does it make it sense to say that the proposition `e :=: e'` is a type?

## Propositions-As-Types and Curry-Howard

In fact, and this is known as the "Propositions as Types" paradigm, or also as the Curry-Howard-Isomorphism, it is possible to think of propositions and of types as interchangable concepts:

Intuitively, a type can be identified with the set of elements that have this type and a proposition can be identified with the set of elements of which the proposition is true.

Similarly, a program that computes a value of type $T$ corresponds to a proof that the proposition $T$ is true.

**Example:** In `NumExp.idr`, there is a function

plusone

which has type

(n : Num) -> (N O) :+: (N n) :=: (N n) :+: (N O)

that is, `plusone` takes as input a number `n` and outputs a term of type `(N O) :+: (N n) :=: (N n) :+: (N O)`, that is, `plusone n` outputs a proof that $1+n\approx n+1$.

**Remark:** The difference of the proposition $1+n\approx n+1$ and the type `(N O) :+: (N n) :=: (N n) :+: (N O)` is purely notational, the main difference being that in the Idris code we need to "typecast" the number `n` into an expression `N n`, whereas this distinction is kept implicit in the mathematical notation.

**Exercise:** Run `plusone O` and explain in which sense the output

EqExpRefl : (N O) :+: (N O) :=: (N O) :+: (N O)

is indeed a proof of $1+1\approx 1+1$.

**Exercise:** Run `plusone (S O)` and explain in which sense the output is indeed a proof of $1+2\approx 2+1$.

## Proofs

We now go back to the previous lecture. Recall

**Proposition 1:** $\quad 1+Sk \approx Sk +1$

*Proof.*
$$ 1+Sk \approx 1+ (k+1) \approx (1+k)+1 \approx (k+1)+1 \approx Sk +1$$

**Exercise 1:** Recall the rules ${\ \rm (refl)\ }
,
{\ \rm (sym)\ }
,
{\ \rm (trans)\ }
,
{\ \rm (cong)\ }
,
{\ \rm (assoc)\ }$ from the previous lecture. You will also need $Sk\approx k+1$ and the induction hypothesis. Annotate each "$\approx$" above with the name of the rule justifying it.

**Solution 1** is in the footnote and best read only after attempting your own solution, but needed for what follows. [^solution1]

In both Isabelle and Idris, one has essentially to program the proof. That is, there will be a sequence of commands, or a nested call of functions, telling the program which rule to apply in which order.

### Automated Proof Checking in Isabelle

Let us do Isabelle first. I copy in the Isabelle code, but this should really be looked at in the Isabelle IDE.

The reason why the code is unreadable as it is, is that it only shows the rules that are applied, but not the so-called "proof state", that is, what the rules are supposed to prove. In the Isabelle IDE, the proof state corresponding to each line of the code can be made visible in the "Output" pane.

Anyway, the idea is that with a bit of care, one can see how the program below corresponds to the mathematical proof we reviewed in Solution 1. Even now, just looking at the raw code, you should be able to identify the rules that have been applied.

**Exercise:** Can you reconstruct the proof from the code below?

(* Proposition 1 in the lecture notes. *)
lemma plusone: "⟨𝟭⟩ :+: ⟨n⟩ ≡ex ⟨n⟩ :+: ⟨𝟭⟩"
apply (induction n)
apply (rule equal_exp_refl)

apply(rule equal_exp_trans)
apply(rule equal_exp_cong_plus)
apply(rule equal_exp_refl)
apply(rule equal_exp_plusone)

apply(rule equal_exp_trans)
apply(rule equal_exp_assoc)

apply(rule equal_exp_trans)
apply(rule equal_exp_cong_plus)
apply simp
apply(rule equal_exp_refl)

apply(rule equal_exp_cong_plus)
apply(rule equal_exp_symm)
apply(rule equal_exp_plusone)
apply(rule equal_exp_refl)
done

Isabelle is being developed with the aim to make machine proofs readable to humans as much as possible. And, indeed, one can write the Isabelle source code above also in a much more readable form (using the *tactic* `exp_tac`, the source code of which is also available in `NumExp.thy`):

lemma plusone: "⟨𝟭⟩ :+: ⟨n⟩ ≡ex ⟨n⟩ :+: ⟨𝟭⟩"
proof (induction n)
case One
then show ?case by (simp add: equal_exp_refl)
next
case (S m)
have "⟨𝟭⟩ :+: ⟨m+𝟭⟩ ≡ex ⟨𝟭⟩ :+: (⟨m⟩ :+: ⟨𝟭⟩)" by exp_tac
also have "… ≡ex (⟨𝟭⟩ :+: ⟨m⟩) :+: ⟨𝟭⟩" by exp_tac
also have "… ≡ex (⟨m⟩ :+: ⟨𝟭⟩) :+: ⟨𝟭⟩" by(exp_tac rule:S)
also have "… ≡ex (⟨m+𝟭⟩) :+: ⟨𝟭⟩" by exp_tac
finally show ?case by simp
qed

If we translate the above into "pseudo-code", it almost looks like the mathematics proof:

lemma plusone: "1+n ≡ex n+1"
proof (induction n)
case One
then show ?case by (simp add: equal_exp_refl)
next
case (S m)
have "1 + ⟨m+1⟩ ≡ex 1 + (m + 1)"
also have "… ≡ex ( 1 + m ) + 1"
also have "… ≡ex ( m + 1 ) + 1"
also have "… ≡ex ⟨m+1⟩ + 1"
finally show ?case by simp
qed

Indeed, replacing `⟨m+1⟩` by $Sm$, this is now easy to match with the mathematical proof

$$ 1+Sm = 1+ (m+1) = (1+m)+1 = (m+1)+1 = Sm +1$$

I find this close match between math and programming very pleasing and I would say, well done, Isabelle.

What about Idris?

### Automated Proof Checking in Idris

total plusone : (n : Num) -> (N O) :+: (N n) :=: (N n) :+: (N O)
plusone O = EqExpRefl
plusone (S n) =
EqExpTrans
(EqExpPlusEq EqExpRefl EqExpPlusOne)
(EqExpTrans EqExpAssoc
(EqExpTrans
(EqExpPlusEq
(plusone n)
EqExpRefl)
(EqExpPlusEq
(EqExpSymm EqExpPlusOne)
EqExpRefl)))

Wow ... what is going on here?

The lecture is coming to end $\ldots$ so I have to leave this an exercise. But I give you some hints:

- A rule like `EqExpTrans` is now a function that takes as arguments two proofs and produces a new proof.
- The proof itself is then a function as well, named `plusone`.
- The induction step is now implemented as the function `plusone` calling itself recursively.

I am very excited about this last item $\ldots$ we started surveying different forms of induction and ended up discovering that inductive proofs and recursive programs are the same.

**Remark:** The general paradigm is called "proposition as types" more often than "proofs as programs". To understand what is meant by this let us look at the Idris code snippet

total plusone : (n : Num) -> (N O) :+: (N n) :=: (N n) :+: (N O)

Ignoring `total`, we can read
- `plusone : _` as "`plusone` is an element of type `_`"
- `(n : Num) -> _` as "for all `n` of type `Num` there is an element of type `_`"
- `(N O) :+: (N n) :=: (N n) :+: (N O)` as "$1+n=n+1$"

In other words, the proposition "$1+n=n+1$" can be read as a type. But the word "type" is short for "data type" and a data type is a set of data elements. So what are the elements here?
[^elementsoftypes]

**Remark:** I recommend to install Idris and run the code. But I pasted in below the result of calling `plusone` on the argument 3 (remember that `O` stands here for "One"). Can you explain what happens?

*NumExp> plusone (S (S O))
EqExpTrans (EqExpPlusEq EqExpRefl EqExpPlusOne)
(EqExpTrans EqExpAssoc
(EqExpTrans (EqExpPlusEq (EqExpTrans (EqExpPlusEq EqExpRefl
EqExpPlusOne)
(EqExpTrans EqExpAssoc
(EqExpTrans (EqExpPlusEq EqExpRefl
EqExpRefl)
(EqExpPlusEq (EqExpSymm EqExpPlusOne)
EqExpRefl))))
EqExpRefl)
(EqExpPlusEq (EqExpSymm EqExpPlusOne)
EqExpRefl))) : (N O) :+:
(N (S (S O))) :=:
(N (S (S O))) :+:
(N O)
*NumExp>

[^solution1]: Solution to Exercise 1.
\begin{align}
1+Sk &\approx 1+ (k+1) \quad & Sk \approx k+1\\
1+ (k+1) & \approx (1+k)+1 & \textrm{(assoc)}\\
(1+k)+1 &\approx (k+1)+1 & \textrm{IH, (cong)}\\
(k+1)+1 &\approx Sk +1 & Sk \approx k+1\\
1+Sk &\approx Sk +1 & 3\times\textrm{(trans)}\\
\end{align}

[^elementsoftypes]: Answer: The elements are the proofs `plusone n` for all `n` in `Num`.