Twelf is a tool for reasoning about
deductive systems. Elegantly, each declaration in Twelf looks like an
*inference rule*:

name : premise-1 -> ... -> premise-n -> conclusion.

An inference rule without premises is called
an *axiom*.

Let's get started with some Twelf code.

nat : type.
z : nat.
s : nat -> nat.

plus : nat -> nat -> nat -> type.
plus/z : plus z N N.
plus/s : plus N1 N2 N3 -> plus (s N1) N2 (s N3).

We can interpret an inference rule in two ways.

- Each conclusion is a
*type*. An axiom defines a*term*inhabiting the type of the conclusion. For example, the term`z`

inhabits the type`nat`

. Each premise is also a*type*. An inference rule with \(n\) premises defines a function with parameter types defined by the premises and return type defined by the conclusion. This function can be applied to \(n\) terms of the premise types to yield a term of the conclusion type. For example, the function`s`

can be applied to term`z`

, to yield the term`s z`

. $${\text{}\over{\text{type}}}(\text{nat}) \quad {\text{}\over{\text{nat}}}(\text{z}) \quad {\text{nat}\over{\text{nat}}}(\text{s})$$ - Each conclusion and premise is a
*proposition*. An inference rule defines a recipe to construct a*proof*or*evidence*for the proposition in the conclusion. For example, the rule`plus/s`

states that if you have evidence of`plus N1 N2 N3`

, then you can construct evidence for`plus (s N1) N2 (s N3)`

for any`nat`

terms`N1, N2, N3`

. $${\begin{align} \text{nat}\\ \text{nat}\\ \text{nat}\\ \end{align}\over{\text{type}}}(\text{plus}) \quad {\text{}\over{\text{plus z N N}}}(\text{plus/z}) \quad {\text{plus N1 N2 N3}\over{\text{plus (s N1) N2 (s N3)}}}(\text{plus/s})$$

This dual interpretation, propositions-as-types, is known as the
Curry-Howard isomorphism. The type interpretation is more natural when
we care to distinguish terms of the same type: even
though `z`

and `s z`

are both of
type `nat`

, we don't think of them as semantically
equivalent. The proposition interpretation is more natural when we
only care about inhabitation: whether it is true or false. For
example, `plus (s z) z (s z)`

is inhabited (true),
while `plus (s z) z z`

is not (false).

In Twelf, we can use the `%query`

command to ask about
inhabitation. Click the play button, and also try queries of your
own by editing the box.

%query * 1 plus (s z) z (s z).
%query 0 * plus (s z) z z.
%query * 3 plus A B C.

We can use the `%solve`

to actually construct a term of a certain type.

%solve a_nat : nat.
%solve a_deriv : plus (s (s z)) (s z) N.

A term for the type `plus (s (s z)) (s z) (s (s (s z)))`

is `plus/s (plus/s plus/z)`

. Indeed,
the `plus/z`

axiom gives us ```
plus z (s z) (s
z)
```

, and applying `plus/s`

twice constructs the
evidence for the desired proposition.

In our definition of `plus/z`

, the `N`

is an
implicit dependent type. We could also define the plus judgment with
all the dependent types made explicit. Now, we also would need to be
explicit in the applications of these new rules, as you can see with
the `%solve`

query below.

plus : nat -> nat -> nat -> type.
plus/z : {N:nat} plus z N N.
plus/s : {N1:nat} {N2:nat} {N3:nat} plus N1 N2 N3 -> plus (s N1) N2 (s N3).

%solve a_deriv : plus (s (s z)) (s z) N.

Note that `A -> B`

is just an abbreviation
for `{_:A} B`

, where the name of the term of
type `A`

is irrelevant, since the type `B`

does
not depend on it.

We can think of a rule with conclusion `type`

and \(n\)
premises as defining an \(n\)-place relation. Taken together, the
rules with conclusion whose head matches the relation name defines all
the way this relation may hold, i.e. all the possible derivations.

We can also define \(n\)-place relations, where some of the places
are universally quantified (inputs), and some are existentially
quantified (outputs). If we can show that the relation
is *total*, i.e. we can always find outputs for all possible
inputs, then we can interpret the relation as a theorem. The proof of
a theorem also takes the form of inference rules, and proceeds by
induction on the derivation rules of some (possibly none) of the
inputs.

Let's get more concrete with some Twelf code.

We show that `z`

is a neutral element on the right. The
induction is on the first term of type `nat`

. Thus, we have
a case (itself, an inference rule) for each inference rule whose
conclusion is `nat`

. In the `s`

case, we make
use of the induction hypothesis: the term of type `nat`

in
the premise (`N`

) is smaller than the term of
type `nat`

in the conclusion (`(s N)`

).

plus-z-right-neutral : {N:nat} plus N z N -> type.
%mode plus-z-right-neutral +N -D.
-/z : plus-z-right-neutral z plus/z.
-/s : plus-z-right-neutral N D -> plus-z-right-neutral (s N) (plus/s D).
%worlds () (plus-z-right-neutral _ _).
%total N (plus-z-right-neutral N _).

We show that we can increment on the right. The induction is on the
first term of type `plus N1 N2 N3`

. Thus, we need to
consider all possible inference rules
for `plus`

: `plus/z`

and `plus/z`

. We
use the backwards arrow `<-`

, so that we can start with
the conclusion and then construct how we reach it.

plus-s-right-inc : plus N1 N2 N3 -> plus N1 (s N2) (s N3) -> type.
%mode plus-s-right-inc +D1 -D2.
-/z : plus-s-right-inc plus/z plus/z.
-/s : plus-s-right-inc (plus/s D1) (plus/s D2)
<- plus-s-right-inc D1 D2.
%worlds () (plus-s-right-inc _ _).
%total D (plus-s-right-inc D _).

Now, let's prove that `plus`

is commutative.

plus-comm : plus N1 N2 N3 -> plus N2 N1 N3 -> type.
%mode plus-comm +D1 -D2.
-/z : plus-comm plus/z D
<- plus-z-right-neutral _ D.
-/s : plus-comm (plus/s D1) D3
<- plus-comm D1 D2
<- plus-s-right-inc D2 D3.
%worlds () (plus-comm _ _).
%total D (plus-comm D _).

Exercise: Show that the plus relation is total, i.e. we can always add any two numbers.

% TODO .

plus-total : {N1:nat} {N2:nat} plus N1 N2 N3 -> type.
%mode plus-total +N1 +N2 -D.
-/z : plus-total z N2 plus/z.
-/s : plus-total (s N1) N2 (plus/s D)
<- plus-total N1 N2 D.
%worlds () (plus-total _ _ _).
%total N1 (plus-total N1 _ _).

Often, we need to reason about *equality* between terms. For a
given type, we can define equality structurally or reflexively.

The recipe for structural equality has one case per derivation rule.

nat-eq-struct : nat -> nat -> type.
nat-eq-struct/z : nat-eq-struct z z.
nat-eq-struct/s : nat-eq-struct (s N1) (s N2)
<- nat-eq-struct N1 N2.

The recipe for reflexive equality always has just one case for identity.

nat-eq : nat -> nat -> type.
nat-eq/id : nat-eq N N.

Exercise: Show that the two definitions of equality for `nat`

, reflexive and structural, are equivalent.

nat-eq-r2s : nat-eq N1 N2 -> nat-eq-struct N1 N2 -> type.
%mode nat-eq-r2s +A -B.
% TODO .
%worlds () (nat-eq-r2s _ _).
%total A (nat-eq-r2s A _).
nat-eq-s2r : nat-eq-struct N1 N2 -> nat-eq N1 N2 -> type.
%mode nat-eq-s2r +A -B.
% TODO .
%worlds () (nat-eq-s2r _ _).
%total A (nat-eq-s2r A _).

nat-eq-struct-refl : {N:nat} nat-eq-struct N N -> type.
%mode nat-eq-struct-refl +N -D.
-/z : nat-eq-struct-refl z nat-eq-struct/z.
-/s : nat-eq-struct-refl (s N) (nat-eq-struct/s D)
<- nat-eq-struct-refl N D.
%worlds () (nat-eq-struct-refl _ _).
%total N (nat-eq-struct-refl N _).
nat-eq-s : nat-eq N1 N2 -> nat-eq (s N1) (s N2) -> type.
%mode nat-eq-s +A -B.
-/id : nat-eq-s nat-eq/id nat-eq/id.
%worlds () (nat-eq-s _ _).
%total A (nat-eq-s A _).
nat-eq-r2s : nat-eq N1 N2 -> nat-eq-struct N1 N2 -> type.
%mode nat-eq-r2s +A -B.
-/id : nat-eq-r2s nat-eq/id D
<- nat-eq-struct-refl _ D.
%worlds () (nat-eq-r2s _ _).
%total A (nat-eq-r2s A _).
nat-eq-s2r : nat-eq-struct N1 N2 -> nat-eq N1 N2 -> type.
%mode nat-eq-s2r +A -B.
-/z : nat-eq-s2r nat-eq-struct/z nat-eq/id.
-/s : nat-eq-s2r (nat-eq-struct/s D) EQ'
<- nat-eq-s2r D EQ
<- nat-eq-s EQ EQ'.
%worlds () (nat-eq-s2r _ _).
%total A (nat-eq-s2r A _).

Armed with equality, we can show that the third place of
the `plus`

relation is uniquely determined by the other two
places.

nat-eq-s : nat-eq N1 N2 -> nat-eq (s N1) (s N2) -> type.
%mode nat-eq-s +A -B.
-/id : nat-eq-s nat-eq/id nat-eq/id.
%worlds () (nat-eq-s _ _).
%total A (nat-eq-s A _).
plus-unique : plus N1 N2 N3 -> plus N1 N2 N3' -> nat-eq N3 N3' -> type.
%mode plus-unique +D1 +D2 -EQ.
-/z : plus-unique plus/z plus/z nat-eq/id.
-/s : plus-unique (plus/s D1) (plus/s D2) EQ'
<- plus-unique D1 D2 EQ
<- nat-eq-s EQ EQ'.
%worlds () (plus-unique _ _ _).
%total D (plus-unique D _ _).