In this walkthrough you will learn...

- How to use lemmas
- How to state and use definitions

This advanced walkthrough assumes you have finished the
beginner's walkthrough and are familiar
with the following tactics: `induction`

,
`intros`

, `case`

, `apply`

, and
`search`

.

This walkthrough is concerned with the simply-typed lambda calculus. Simple types are those constructed starting from base types using the function type constructor; the main difference between these types and those considered in the earlier walkthrough is that the language of types now does not include type variables. At the level of terms, another difference is that the atoms are assumed to have specific types at the beginning. We are interested in terms that are constructed only using applications and abstractions and so the type for atoms (that are only the abstracted variables) is given by including a type with each abstraction. Typing rules allow us to assign types to more complicated expressions. These rules look very much like the ones in the beginner's walkthrough with the only difference that the rule for abstractions has to use the provided type for the abstracted variable. The property that we will prove is that in such a case there is exactly one type that can be assigned to each well-formed term.

This walkthrough uses the following signature which we assume is saved
in `type-uniq.sig`

.

sig type-uniq. kind tm, ty type. type i ty. type arrow ty -> ty -> ty. type app tm -> tm -> tm. type abs ty -> (tm -> tm) -> tm. type of tm -> ty -> o.

Note that this signature differs from signature in the first
walkthrough in that the `abs`

constructor now takes two
arguments, the first of which is the type of the variable which is
abstracted over.

The specification of typing in the simply-typed lambda-calculus are
specified in the following module which we assume is saved
in `type-uniq.mod`

.

module type-uniq. of (abs T R) (arrow T U) :- pi x\ (of x T => of (R x) U). of (app M N) T :- of M (arrow U T), of N U.

Note that the rule for typing abstractions uses the type annotation which is attached to each abstraction.

The specification is already included with Abella in the directory
`examples/lambda-calculus/type-uniq`

as the
files `type-uniq.sig`

and `type-uniq.mod`

. We
can load this specification in Abella as follows.

~/abella/examples/lambda-calculus/type-uniq %We state our type uniqueness theorem as follows.abellaWelcome to Abella 2.0.0 Abella <Specification "type-uniq".Reading specification type-uniq Abella <

Abella <We will induct on the height ofTheorem type_uniq : forall E T1 T2, {of E T1} -> {of E T2} -> T1 = T2.

`{of E T1}`

,
use `intros`

, and then do case analysis on ```
{of E
T1}
```

. This results in two subgoals corresponding to the two
specification rules for `of`

. The first subgoal is
when `E`

is an abstraction; the second subgoal is
abbreviated for now.
Subgoal 1: Variables: E, T1, T2, U, R, T IH : forall E T1 T2, {of E T1}* -> {of E T2} -> T1 = T2 H2 : {of (abs T R) T2} H3 : {of n1 T |- of (R n1) U}* ============================ arrow T U = T2 Subgoal 2 is: T1 = T2At this point

`E`

has been bound to `(abs T R)`

.
There is only one way in which `{of (abs T R) T2}`

can be
derived, thus case analysis on this hypothesis acts like unfolding
this judgment. The result is as follows.
Subgoal 1: Variables: E, T1, T2, U, R, T, U1 IH : forall E T1 T2, {of E T1}* -> {of E T2} -> T1 = T2 H3 : {of n1 T |- of (R n1) U}* H4 : {of n1 T |- of (R n1) U1} ============================ arrow T U = arrow T U1 Subgoal 2 is: T1 = T2It looks like we are almost there, but something goes wrong when we try to apply the inductive hypothesis to

```
{of n1 T |- of (R n1)
U}*
```

and `{of n1 T |- of (R n1) U1}`

.
type_uniq <apply IH to H3 H4.Error: Contexts did not match

Basically what happened is that our theorem was stated for typing
judgments that have an empty context of hypothetical assumptions. We
can think of `{of E T1}`

as being
`{nil |- of E T1}`

. When we tried to apply our inductive
hypothesis to judgments which had non-empty contexts, it failed. The
problem is that *we need to generalize our theorem over the
possible contexts in which typing judgments are made*. Roughly we
want something like the following.

```
``````
forall L E T1 T2, {L |- of E T1} -> {L |- of E T2} -> T1 = T2.
```

However, this statement is too general and, in fact, not true. To begin
with, we are not interested in it being true for all `L`

,
only for those `L`

s that assign types to terms. Moreover,
the relevant `L`

s should assign types only to nominal
constants (which represent abstracted variables in the proof) and at
most one type to each such constant. Notice that without this
uniqueness assumption about the assignment of types to variables, the
proposition cannot be true.
The way we will realize this restriction is by defining a property
called `ctx`

that we expect all good contexts to satisfy
and then requiring this property to hold of `L`

in the
statement of the theorem.
If you are following this walkthrough in Abella, you first need to
type "`abort.`

" to give up on our previous proof
attempt. Then enter the following definition of `ctx`

.

Define ctx : olist -> prop by ctx nil ; nabla x, ctx (of x T :: L) := ctx L.

The system should accept this command with no output. What this
definition says is that the empty list is well-formed context and the
list `(of x T :: L)`

is a well-formed context if
`x`

is a nominal constant and `L`

is a
well-formed context; here `nil`

represents the empty list
and `::`

is a built-in infix constructor for lists.
When we define `ctx`

here we also give it a type which
is `olist -> prop`

, where `olist`

is the type of
lists of terms of type `o`

and `prop`

is the type of formulas in the reasoning logic.

The definition of `ctx`

ensures that the following atomic
formula is provable in the reasoning logic

```
ctx (of n1 T1 :: of n2 T2 :: of n3 T3 :: nil)
```

where `n1`

, `n2`

, and `n3`

are
nominal constants. This definition also ensures that the following
formulas are ```
ctx (of n1 T1 :: of n1 T2 :: nil)
```

```
ctx (of (app M N) T :: nil)
```

```
ctx (of (abs R) T :: nil)
```

These non-examples illustrate facts that we would like to prove about
well-formed contexts. The first is that they cannot contain more than
one typing judgment for the same nominal constant. In proving this
lemma, we will need another fact about the non-occurrence of nominal
constants with a particular kind of scope in a list. This property can
be stated using the predicate `member`

that is known to
Abella via the following definition. **Do not type this in, since
this is already defined in Abella**.

Define member : o -> olist -> prop by member A (A :: L) ; member A (B :: L) := member A L.The property we need is stated in the following lemma:

Theorem member_nominal_absurd : forall L T, nabla x, member (of x T) L -> false.Before we consider a proof of this lemma, it is useful to consider the following simpler observation that is in some ways related:

Theorem non_occurrence : forall L, nabla (x:tm), (x = L) -> false.The particular order in which the quantifiers over

`L`

and
`x`

are scoped automatically enforces the requirement that
any nominal constant substituted for `x`

cannot appear in
the term substituted for `L`

. Abella understands
this and this theorem is therefore easily proved. In detail, the proof
will follow quickly by using the tactics `intros`

and
`case H1`

.
Given that non_occurrence is provable, one might wonder if
member_nominal_absurd does not follow immediately from it: the
property is after all similar in that we are trying to show the
non-occurrence of the nominal constant plugged in for `x`

in the statement of member_nominal_absurd in the term substituted for
`L`

. Unfortunately, this is not true. `L`

is a
list that is, in a sense, constructed using the definition of
`member`

and we have to factor this non-occurrence property
through that definition.

Once we have observed this much, the actual proof is easy to perform and so I'll just show it.

============================ forall L T, nabla x, member (of x T) L -> false member_nominal_absurd <induction on 1.

IH : forall L T, nabla x, member (of x T) L * -> false ============================ forall L T, nabla x, member (of x T) L @ -> false member_nominal_absurd <intros.

Variables: L, T IH : forall L T, nabla x, member (of x T) L * -> false H1 : member (of n1 T) L @ ============================ false member_nominal_absurd <case H1.

Variables: L, T, L3, L2 IH : forall L T, nabla x, member (of x T) L * -> false H2 : member (of n1 T) L3 * ============================ false member_nominal_absurd <The interesting part is when we didapply IH to H2.Proof completed.

`case H1`

we didn't
have to consider the subgoal when `(of n1 T)`

is at
the head of `L`

. Here the fact that the instantiation
of `L`

cannot contain `n1`

, the nominal constant
substituted for `x`

, gets used.
If we now attempt to prove the uniqueness property for contexts we
will still run into a small problem: we will encounter terms of the
form `T n1`

where `T`

is a variable of
type `ty`

and `n1`

is a nominal constant of type
`tm`

. Such terms are absurd since it is not possible for a
term of type `tm`

to appear inside a term of
type `ty`

. Abella does not know this, however, since the
user may later add a new constant with type `tm -> ty`

which would allow such dependencies. In order to let Abella know that
such constants will never be introduced, we tell it that the
types `tm`

and `ty`

are *closed* using
the following command:

Close tm, ty.

Now we can now state and prove the uniqueness property for contexts.

Theorem member_uniq : forall L E T1 T2, ctx L -> member (of E T1) L -> member (of E T2) L -> T1 = T2.This lemma can be proved by induction on any of the hypotheses. We will induct on

`member (of E T1) L`

followed by
`intros`

and case analysis on ```
member (of E T1)
L
```

. This results in two subgoals based on whether ```
(of E
T1)
```

occurs in the head or the tail of `L`

. The proof
state is as follows.
Subgoal 1: Variables: L, E, T1, T2, L1 IH : forall L E T1 T2, ctx L -> member (of E T1) L * -> member (of E T2) L -> T1 = T2 H1 : ctx (of E T1 :: L1) H3 : member (of E T2) (of E T1 :: L1) ============================ T1 = T2 Subgoal 2 is: T1 = T2The first subgoal is when

`(of E T1)`

is at the head of
`L`

which is therefore `(of E T1 :: L1)`

. Next
we do case analysis on `member (of E T2) (of E T1 :: L1)`

which will replace the current subgoal with two new subgoals, bringing
the total number of subgoals to three. The first subgoal will be
when `(of E T2)`

is at the head of the list. This
means `T1 = T2`

so the subgoal is trivially handled
by `search.`

After this, two subgoals remain.
Subgoal 1.2: Variables: L, E, T1, T2, L1 IH : forall L E T1 T2, ctx L -> member (of E T1) L * -> member (of E T2) L -> T1 = T2 H1 : ctx (of E T1 :: L1) H4 : member (of E T2) L1 ============================ T1 = T2 Subgoal 2 is: T1 = T2Let's stop to think about the first subgoal. It is stating that

`(of E T1 :: L1)`

is a well-formed typing context and
yet there is another binding for `E`

in `L1`

.
This is a contradiction and we need to expose it to the prover.
Here we perform case analysis on `ctx (of E T1 :: L1)`

.
This case analysis will be interesting because the `ctx`

was defined with a nabla quantifier in the head of the definition. As
a reminder, here is the relevant definition of `ctx`

.
**Don't type this in again, it is only to remind you.**

nabla x, ctx (of x T :: L) := ctx LBased on the intended meaning of this clause that we discussed earlier,

```
ctx (of E T1 ::
L1)
```

can follow from it only if `E`

is a nominal
constant and `T1`

and `L1`

are restricted to be
terms that do not contain this nominal constant. The logical
form of the unfolding rule is treated in detail in this paper. The
effect of this rule on the existing proof state will be to introduce a
new nominal constant for `E`

and to require that the newly
introduced eigenvariables not contain this constant. Of course, the
previously available eigenvariables can use the nominal constant. To
resolve this seemingly contradictory requirements, we stipulate that
no eigenvariable can be instantiated by a term containing a nominal
constant but we also replace the original eigenvariables by new ones
applied to the introduced nominal constant. This mechanism, that is
known technically as raising, allows dependencies to be represented
even under the restriction on substitutions for eigenvariables. In the
current case, however, the nominal constant we are raising over has
type `tm`

and the only eigenvariables we might have to
raise are of type `ty`

. Since we used
the `Close`

command, Abella knows that the `ty`

variables cannot depend on terms of type `tm`

, and thus no
raising is performed.
Effecting an unfolding in the manner described in the current situation yields the following as the new proof state.

member_uniq <We can complete this subgoal by applying our lemma about occurrences of nominal constants.case H1.Subgoal 1.2: Variables: L, E, T1, T2, L1, L2 IH : forall L E T1 T2, ctx L -> member (of E T1) L * -> member (of E T2) L -> T1 = T2 H4 : member (of n1 T2) L2 H5 : ctx L2 ============================ T1 = T2 Subgoal 2 is: T1 = T2

member_uniq <This completes the subgoal and leaves just the following subgoal left to be proven.apply member_nominal_absurd to H4.

Subgoal 2: Variables: L, E, T1, T2, L1, B IH : forall L E T1 T2, ctx L -> member (of E T1) L * -> member (of E T2) L -> T1 = T2 H1 : ctx (B :: L1) H3 : member (of E T2) (B :: L1) H4 : member (of E T1) L1 * ============================ T1 = T2Now we perform case analysis on

```
member (of E T2) (B ::
L1)
```

which generates two subgoals. The first subgoal is
symmetric to the previous subgoal we considered, so I'll leave that for
you. The other subgoal is as follows.
Subgoal 2.2: Variables: L, E, T1, T2, L1, B IH : forall L E T1 T2, ctx L -> member (of E T1) L * -> member (of E T2) L -> T1 = T2 H1 : ctx (B :: L1) H4 : member (of E T1) L1 * H5 : member (of E T2) L1 ============================ T1 = T2All we need now to apply the inductive hypothesis is a judgment like

`ctx L1`

. We get this by case analysis which triggers
raising of eigenvariables; this raising which is shown in the prover
state below ends up having no effect on the proof itself. The rest of
the proof is, in fact, as follows.
member_uniq <case H1.Subgoal 2.2: Variables: L, E, T1, T2, L1, B, L2, T IH : forall L E T1 T2, ctx L -> member (of E T1) L * -> member (of E T2) L -> T1 = T2 H4 : member (of (E n1) T1) L2 * H5 : member (of (E n1) T2) L2 H6 : ctx L2 ============================ T1 = T2 member_uniq <apply IH to H6 H4 H5.

Subgoal 2.2: Variables: L, E, T1, T2, L1, B, L2, T IH : forall L E T1 T2, ctx L -> member (of E T1) L * -> member (of E T2) L -> T1 = T2 H4 : member (of (E n1) T2) L2 * H5 : member (of (E n1) T2) L2 H6 : ctx L2 ============================ T2 = T2 member_uniq <We need another property about the context before we can prove our generalized theorem. We've shown well-formed contexts cannot have two typing judgments for the same variable, but we still have to show that such contexts can only contain typing judgments for nominal constants. For this we define a notation that a term must be a nominal constant.search.Proof completed.

Define name : tm -> prop by nabla x, name x.Given a variable

`X`

and an assumption `name X`

,
`X`

must be a nominal constant by the definition
of `name`

. The structural property about a well-formed
context is basically an inspection of its definition, which is stated as
follows.
Theorem ctx_mem : forall L E, ctx L -> member E L -> exists N X, E = of X N /\ name X.The proof of this lemma is straightforward so I'll just show it.

============================ forall L E, ctx L -> member E L -> (exists N X, E = of X N /\ name X) ctx_mem <induction on 2.

IH : forall L E, ctx L -> member E L * -> (exists N X, E = of X N /\ name X) ============================ forall L E, ctx L -> member E L @ -> (exists N X, E = of X N /\ name X) ctx_mem <intros.

Variables: L, E IH : forall L E, ctx L -> member E L * -> (exists N X, E = of X N /\ name X) H1 : ctx L H2 : member E L @ ============================ exists N X, E = of X N /\ name X ctx_mem <case H2.

Subgoal 1: Variables: L, E, L1 IH : forall L E, ctx L -> member E L * -> (exists N X, E = of X N /\ name X) H1 : ctx (E :: L1) ============================ exists N X, E = of X N /\ name X Subgoal 2 is: exists N X, E = of X N /\ name X ctx_mem <case H1.

Subgoal 1: Variables: L, E, L1, L2, T IH : forall L E, ctx L -> member E L * -> (exists N X, E = of X N /\ name X) H3 : ctx L2 ============================ exists N X, of n1 T = of X N /\ name X Subgoal 2 is: exists N X, E = of X N /\ name X ctx_mem <search.

Subgoal 2: Variables: L, E, L1, B IH : forall L E, ctx L -> member E L * -> (exists N X, E = of X N /\ name X) H1 : ctx (B :: L1) H3 : member E L1 * ============================ exists N X, E = of X N /\ name X ctx_mem <case H1.

Subgoal 2: Variables: L, E, L1, B, L2, T IH : forall L E, ctx L -> member E L * -> (exists N X, E = of X N /\ name X) H3 : member (E n1) L2 * H4 : ctx L2 ============================ exists N X, E n1 = of X N /\ name X ctx_mem <apply IH to H4 H3.

Subgoal 2: Variables: L, E, L1, B, L2, T, N, X IH : forall L E, ctx L -> member E L * -> (exists N X, E = of X N /\ name X) H3 : member (of (X n1) N) L2 * H4 : ctx L2 H5 : name (X n1) ============================ exists N1 X1, of (X n1) N = of X1 N1 /\ name X1 ctx_mem <Notice that at one point we did case analysis onsearch.Proof completed.

`ctx (E :: L1)`

which exposes `E`

to be `of n1 T`

. Since `n1`

is a nominal constant, a `search`

completed the subgoal.
Now we can state and prove our generalized theorem.

Theorem type_uniq_ext : forall L E T1 T2, ctx L -> {L |- of E T1} -> {L |- of E T2} -> T1 = T2.The proof of this lemma is by induction on one of the typing judgments. The body of the proof consists of considering the possible ways in which the two typing judgments are derived. Because these typing judgments have non-empty contexts, we will have to consider the possibility that, for example, the typing judgment

```
(of E
T1)
```

comes directly from the context `L`

. Thus case
analysis on a hypothesis like `{L |- of E T1}`

will result
in three subgoals.
The entire proof is listed below. We pay special attention to
cases where the typing judgment is derived from the context. We will
also pause to introduce a convenient feature of the `apply`

tactic.

============================ forall L E T1 T2, ctx L -> {L |- of E T1} -> {L |- of E T2} -> T1 = T2 type_uniq_ext <induction on 2.

IH : forall L E T1 T2, ctx L -> {L |- of E T1}* -> {L |- of E T2} -> T1 = T2 ============================ forall L E T1 T2, ctx L -> {L |- of E T1}@ -> {L |- of E T2} -> T1 = T2 type_uniq_ext <intros.

Variables: L, E, T1, T2 IH : forall L E T1 T2, ctx L -> {L |- of E T1}* -> {L |- of E T2} -> T1 = T2 H1 : ctx L H2 : {L |- of E T1}@ H3 : {L |- of E T2} ============================ T1 = T2 type_uniq_ext <In the first case, the goal formulacase H2.

`of E T1`

is
derived from the program clause for abstraction.
Subgoal 1: Variables: L, E, T1, T2, U, R, T IH : forall L E T1 T2, ctx L -> {L |- of E T1}* -> {L |- of E T2} -> T1 = T2 H1 : ctx L H3 : {L |- of (abs T R) T2} H4 : {L, of n1 T |- of (R n1) U}* ============================ arrow T U = T2 Subgoal 2 is: T1 = T2 Subgoal 3 is: T1 = T2 type_uniq_ext <case H3.

Subgoal 1.1: Variables: L, E, T1, T2, U, R, T, U1 IH : forall L E T1 T2, ctx L -> {L |- of E T1}* -> {L |- of E T2} -> T1 = T2 H1 : ctx L H4 : {L, of n1 T |- of (R n1) U}* H5 : {L, of n1 T |- of (R n1) U1} ============================ arrow T U = arrow T U1 Subgoal 1.2 is: arrow T U = T2 Subgoal 2 is: T1 = T2 Subgoal 3 is: T1 = T2 type_uniq_ext <We are now considering the case whenapply IH to _ H4 H5.

`E`

is the abstraction
`(abs T R)`

and the typing judgments are formed using the
typing rule for abstractions. Thus the typing context has grown
to include a typing assumption for a new nominal constant
`n1`

. In order to apply our inductive hypothesis to the
new typing judgments for `(R n1)`

, we must ensure that
`(of n1 T :: L)`

is a well-formed context, i.e. that it is
accepted by the definition of `ctx`

. This should be easy
since it is clear that neither `T`

nor `L`

can
depends on `n1`

.
One option is to use the `assert`

tactic to explicitly
state `ctx (of n1 T :: L)`

. We could then prove this
assertion using the `search`

tactic. A more convenient
option is to use what is called "apply with unknowns." For this we
simply put a `_`

where we want the system to generate a
hypothesis for us. The prover will then guess what needs be proved for
the unknown hypothesis and attempt to prove it using the
`search`

tactic. If this fails, the current subgoal will be
delayed and the unknown hypothesis will become the current goal. In
our case, `ctx (of n1 T :: L)`

will be solved by
`search`

so there is no extra subgoal generated. We now
return you to the rest of the proof.

Subgoal 1.1: Variables: L, E, T1, T2, U, R, T, U1 IH : forall L E T1 T2, ctx L -> {L |- of E T1}* -> {L |- of E T2} -> T1 = T2 H1 : ctx L H4 : {L, of n1 T |- of (R n1) U1}* H5 : {L, of n1 T |- of (R n1) U1} ============================ arrow T U1 = arrow T U1 Subgoal 1.2 is: arrow T U = T2 Subgoal 2 is: T1 = T2 Subgoal 3 is: T1 = T2 type_uniq_ext <search.

Subgoal 1.2: Variables: L, E, T1, T2, U, R, T, F IH : forall L E T1 T2, ctx L -> {L |- of E T1}* -> {L |- of E T2} -> T1 = T2 H1 : ctx L H4 : {L, of n1 T |- of (R n1) U}* H5 : {L, [F] |- of (abs T R) T2} H6 : member F L ============================ arrow T U = T2 Subgoal 2 is: T1 = T2 Subgoal 3 is: T1 = T2 type_uniq_ext <At this point we encounter a judgment of the formapply ctx_mem to H1 H6.

```
{L, [F] |- G}
```

for the first time. Such a judgment is called a backchaining
judgment, which indicates that the goal formula `G`

, which
is `of (abs T R) T2`

in this case, is proved by
backchaining on some formula `F`

in the
context `L`

. The hypothesis `member F L`

is
introduced to show that `F`

is contained in
`L`

.
If we perform case analysis on `H5`

, we
will get an error message:

type_uniq_ext <Case analysis fails because the structure ofcase H5.Error: Cannot perform case-analysis on flexible head

`F`

is
unknown. To make progress we apply the lemma `ctx_mem`

to
reveal `F`

, which is of the form `of X N`

. Then
we perform case analysis on `H5`

which backchains the goal
`of (abs T R) T2`

on the clause `of X N`

, as shown below.
Subgoal 1.2: Variables: L, E, T1, T2, U, R, T, F, N, X IH : forall L E T1 T2, ctx L -> {L |- of E T1}* -> {L |- of E T2} -> T1 = T2 H1 : ctx L H4 : {L, of n1 T |- of (R n1) U}* H5 : {L, [of X N] |- of (abs T R) T2} H6 : member (of X N) L H7 : name X ============================ arrow T U = T2 Subgoal 2 is: T1 = T2 Subgoal 3 is: T1 = T2 type_uniq_ext <case H5.

Subgoal 1.2: Variables: L, E, T1, T2, U, R, T, F, N, X IH : forall L E T1 T2, ctx L -> {L |- of E T1}* -> {L |- of E T2} -> T1 = T2 H1 : ctx L H4 : {L, of n1 T |- of (R n1) U}* H6 : member (of (abs T R) T2) L H7 : name (abs T R) ============================ arrow T U = T2 Subgoal 2 is: T1 = T2 Subgoal 3 is: T1 = T2 type_uniq_ext <As a result of backchaining,case H7.

`X`

is unified with `abs T R`

.
Case analysis on `H7`

completed this subgoal because `abs T R`

is not a nominal constant.
The case that `E`

is an application is proved in a similar way.

Subgoal 2: Variables: L, E, T1, T2, U, N, M IH : forall L E T1 T2, ctx L -> {L |- of E T1}* -> {L |- of E T2} -> T1 = T2 H1 : ctx L H3 : {L |- of (app M N) T2} H4 : {L |- of M (arrow U T1)}* H5 : {L |- of N U}* ============================ T1 = T2 Subgoal 3 is: T1 = T2 type_uniq_ext <case H3.

Subgoal 2.1: Variables: L, E, T1, T2, U, N, M, U1 IH : forall L E T1 T2, ctx L -> {L |- of E T1}* -> {L |- of E T2} -> T1 = T2 H1 : ctx L H4 : {L |- of M (arrow U T1)}* H5 : {L |- of N U}* H6 : {L |- of M (arrow U1 T2)} H7 : {L |- of N U1} ============================ T1 = T2 Subgoal 2.2 is: T1 = T2 Subgoal 3 is: T1 = T2 type_uniq_ext <apply IH to H1 H4 H6.

Subgoal 2.1: Variables: L, E, T1, T2, U, N, M, U1 IH : forall L E T1 T2, ctx L -> {L |- of E T1}* -> {L |- of E T2} -> T1 = T2 H1 : ctx L H4 : {L |- of M (arrow U1 T2)}* H5 : {L |- of N U1}* H6 : {L |- of M (arrow U1 T2)} H7 : {L |- of N U1} ============================ T2 = T2 Subgoal 2.2 is: T1 = T2 Subgoal 3 is: T1 = T2 type_uniq_ext <search.

Subgoal 2.2: Variables: L, E, T1, T2, U, N, M, F IH : forall L E T1 T2, ctx L -> {L |- of E T1}* -> {L |- of E T2} -> T1 = T2 H1 : ctx L H4 : {L |- of M (arrow U T1)}* H5 : {L |- of N U}* H6 : {L, [F] |- of (app M N) T2} H7 : member F L ============================ T1 = T2 Subgoal 3 is: T1 = T2 type_uniq_ext <apply ctx_mem to H1 H7.

Subgoal 2.2: Variables: L, E, T1, T2, U, N, M, F, N1, X IH : forall L E T1 T2, ctx L -> {L |- of E T1}* -> {L |- of E T2} -> T1 = T2 H1 : ctx L H4 : {L |- of M (arrow U T1)}* H5 : {L |- of N U}* H6 : {L, [of X N1] |- of (app M N) T2} H7 : member (of X N1) L H8 : name X ============================ T1 = T2 Subgoal 3 is: T1 = T2 type_uniq_ext <case H6.

Subgoal 2.2: Variables: L, E, T1, T2, U, N, M, F, N1, X IH : forall L E T1 T2, ctx L -> {L |- of E T1}* -> {L |- of E T2} -> T1 = T2 H1 : ctx L H4 : {L |- of M (arrow U T1)}* H5 : {L |- of N U}* H7 : member (of (app M N) T2) L H8 : name (app M N) ============================ T1 = T2 Subgoal 3 is: T1 = T2 type_uniq_ext <The last case is when the goal formula is derived from some clausecase H8.

`F`

in the context. As described before, we first apply the lemma `ctx_mem`

to reveal the structure of `F`

. We then perform case analysis to backchain
the goal formula on `F`

.
Subgoal 3: Variables: L, E, T1, T2, F IH : forall L E T1 T2, ctx L -> {L |- of E T1}* -> {L |- of E T2} -> T1 = T2 H1 : ctx L H3 : {L |- of E T2} H4 : {L, [F] |- of E T1}* H5 : member F L ============================ T1 = T2 type_uniq_ext <apply ctx_mem to H1 H5.

Subgoal 3: Variables: L, E, T1, T2, F, N, X IH : forall L E T1 T2, ctx L -> {L |- of E T1}* -> {L |- of E T2} -> T1 = T2 H1 : ctx L H3 : {L |- of E T2} H4 : {L, [of X N] |- of E T1}* H5 : member (of X N) L H6 : name X ============================ T1 = T2 type_uniq_ext <case H4.

Subgoal 3: Variables: L, E, T1, T2, F, N, X IH : forall L E T1 T2, ctx L -> {L |- of E T1}* -> {L |- of E T2} -> T1 = T2 H1 : ctx L H3 : {L |- of E T2} H5 : member (of E T1) L H6 : name E ============================ T1 = T2 type_uniq_ext <The case analysis above reveals the fact thatcase H6.

`E`

is a
nominal constant. Eigenvariables are raised over this nominal
constant `n1`

because of their dependency
on `n1`

.
Now the goal formula `of n1 T2`

in
`H3`

can only be derived from the context because the
nominal constant `n1`

cannot be an abstraction or an
application. The same technique for reasoning about backchaining
judgments is used once again for `{L n1 |- of n1 T2}`

.
Subgoal 3: Variables: L, E, T1, T2, F, N, X IH : forall L E T1 T2, ctx L -> {L |- of E T1}* -> {L |- of E T2} -> T1 = T2 H1 : ctx (L n1) H3 : {L n1 |- of n1 T2} H5 : member (of n1 T1) (L n1) ============================ T1 = T2 type_uniq_ext <case H3.

Subgoal 3: Variables: L, E, T1, T2, F, N, X, F1 IH : forall L E T1 T2, ctx L -> {L |- of E T1}* -> {L |- of E T2} -> T1 = T2 H1 : ctx (L n1) H5 : member (of n1 T1) (L n1) H7 : {L n1, [F1 n1] |- of n1 T2} H8 : member (F1 n1) (L n1) ============================ T1 = T2 type_uniq_ext <apply ctx_mem to H1 H8.

Subgoal 3: Variables: L, E, T1, T2, F, N, X, F1, N1, X1 IH : forall L E T1 T2, ctx L -> {L |- of E T1}* -> {L |- of E T2} -> T1 = T2 H1 : ctx (L n1) H5 : member (of n1 T1) (L n1) H7 : {L n1, [of (X1 n1) N1] |- of n1 T2} H8 : member (of (X1 n1) N1) (L n1) H9 : name (X1 n1) ============================ T1 = T2 type_uniq_ext <case H7.

Subgoal 3: Variables: L, E, T1, T2, F, N, X, F1, N1, X1 IH : forall L E T1 T2, ctx L -> {L |- of E T1}* -> {L |- of E T2} -> T1 = T2 H1 : ctx (L n1) H5 : member (of n1 T1) (L n1) H8 : member (of n1 T2) (L n1) H9 : name n1 ============================ T1 = T2 type_uniq_ext <At this point we knowapply ctx_uniq to H1 H5 H8.

`of n1 T1`

and `of n1 T2`

are both in the same context. By applying `ctx_uniq`

we prove
that `T1`

and `T2`

are the same.
Subgoal 3: Variables: L, E, T1, T2, F, N, X, F1, N1, X1 IH : forall L E T1 T2, ctx L -> {L |- of E T1}* -> {L |- of E T2} -> T1 = T2 H1 : ctx (L n1) H5 : member (of n1 T2) (L n1) H8 : member (of n1 T2) (L n1) H9 : name n1 ============================ T2 = T2 type_uniq_ext <We can now use this generalized theorem to prove our specific theorem. Watch closely and you'll see another use of apply with unknowns.search.Proof completed.

Abella <Theorem type_uniq : forall E T1 T2, {of E T1} -> {of E T2} -> T1 = T2.============================ forall E T1 T2, {of E T1} -> {of E T2} -> T1 = T2 type_uniq <intros.

Variables: E, T1, T2 H1 : {of E T1} H2 : {of E T2} ============================ T1 = T2 type_uniq <apply type_uniq_ext to _ H1 H2.

Variables: E, T1, T2 H1 : {of E T2} H2 : {of E T2} ============================ T2 = T2 type_uniq <Congratulations! We've now proved type uniqueness for the simply-typed lambda-calculus. You can look at examples/lambda-calculus/type-uniq/type-uniq.thm for a full development.search.Proof completed.

You should now have a basic understanding of the most popular tactics in Abella as well as of definitions and lemmas. With this knowledge you are ready to understand any of the examples included with Abella. I suggest looking at the examples listed on the homepage and perhaps those smaller examples listed here. You are also encourage to specify and reason about your own logical system. If so, please let us hear about it: Abella mailing list