Advanced Walkthrough: Type Uniqueness

In this walkthrough you will learn...

• How to use lemmas
• How to state and use definitions

Introduction

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.

Executable Specification

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.

Reasoning

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 % abella
Welcome to Abella 2.0.0
Abella < Specification "type-uniq".
Reading specification type-uniq

Abella <

We state our type uniqueness theorem as follows.

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

We will induct on the height of {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 = T2

At 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 = T2

It 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 Ls that assign types to terms. Moreover, the relevant Ls 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 not provable.

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 < apply IH to H2.
Proof completed.

The interesting part is when we did 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 ctx_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 = T2

The 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 = T2

Let'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 L

Based 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.

ctx_uniq < 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

We can complete this subgoal by applying our lemma about occurrences of nominal constants.

ctx_uniq < apply member_nominal_absurd to H4.

This completes the subgoal and leaves just the following subgoal left to be proven.

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 = T2

Now 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 = T2

All 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.

ctx_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

ctx_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

ctx_uniq < search.
Proof completed.

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.

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 < search.
Proof completed.

Notice that at one point we did case analysis on 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 < case H2.

In the first case, the goal formula 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 < apply IH to _ H4 H5.

We are now considering the case when 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 < apply ctx_mem to H1 H6.

At this point we encounter a judgment of the form {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 H5.
Error: Cannot perform case-analysis on flexible head

Case analysis fails because the structure of 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 < case H7.

As a result of backchaining, 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 < case H8.

The last case is when the goal formula is derived from some clause 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 < case H6.

The case analysis above reveals the fact that 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 < apply ctx_uniq to H1 H5 H8.

At this point we know 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 < search.
Proof completed.

We can now use this generalized theorem to prove our specific theorem. Watch closely and you'll see another use of apply with unknowns.

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 < search.
Proof completed.

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.

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