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 five primary tactics of Abella: 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

As in the first walkthrough, we have the constructors app and abs for our lambda-terms, except abs now takes two arguments: a type for its input and an abstraction denoting its body. Thus for example the term λx:a. λy:b. x will be written

abs a (x\ abs b (y\ x))

The rules for typing in the simply-typed lambda-calculus are as follows.

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.

Reasoning

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.

2 subgoal(s).

  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.

2 subgoal(s).

  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: Context is empty

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 nil.
Define nabla x, ctx (of x T :: L) := ctx L.

The system should accept these commands 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. This definition ensures that the following atomic judgment 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 judgments 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 A (A :: L).
Define 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 x)) 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,
  (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.

1 subgoal(s).


  ============================
   forall L T, nabla x, member (of x (T x)) L -> false

member_nominal_absurd < induction on 1.

1 subgoal(s).


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

member_nominal_absurd < intros.

1 subgoal(s).

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

member_nominal_absurd < case H1.

1 subgoal(s).

  Variables: L, T, L3, L2
  IH : forall L T, nabla x, member (of x (T x)) L * -> false
  H2 : member (of n1 (T n1)) 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 n1)) 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.

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.

2 subgoal(s).

  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.

2 subgoal(s).

  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.

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

Effecting an unfolding in the manner described in the current situation yields the following as the new proof state. Note here that the eigenvariable T2 in the hypothesis H4 in the old proof state has been replaced with a new eigenvariable (that we still call T2) applied to the introduced nominal constant.

member_uniq < case H1.
2 subgoal(s).

  Variables: L, E, T1, T2, L1, 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 n1 (T2 n1)) L2
  H5 : ctx L2
  ============================
   T = T2 n1

subgoal 2 is:
 T1 = T2

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

member_uniq < apply member_nominal_absurd to H4.

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

1 subgoal(s).

  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.

1 subgoal(s).

  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.

member_uniq < case H1.
1 subgoal(s).

  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 n1)) L2 *
  H5 : member (of (E n1) (T2 n1)) L2
  H6 : ctx L2
  ============================
   T1 n1 = T2 n1

member_uniq < apply IH to H6 H4 H5.

1 subgoal(s).

  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 n1)) L2 *
  H5 : member (of (E n1) (T2 n1)) L2
  H6 : ctx L2
  ============================
   T2 n1 = T2 n1

member_uniq < search.
Proof completed.

We need two more lemmas 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. Thus we'll need the following.

Theorem member_app_absurd : forall M N T L,
  ctx L -> member (of (app M N) T) L -> false.

The proof of this lemma is straightforward so I'll just show it.

1 subgoal(s).


  ============================
   forall M N T L, ctx L -> member (of (app M N) T) L -> false

member_app_absurd < induction on 2.

1 subgoal(s).


  IH : forall M N T L, ctx L -> member (of (app M N) T) L * -> false
  ============================
   forall M N T L, ctx L -> member (of (app M N) T) L @ -> false

member_app_absurd < intros.

1 subgoal(s).

  Variables: M, N, T, L
  IH : forall M N T L, ctx L -> member (of (app M N) T) L * -> false
  H1 : ctx L
  H2 : member (of (app M N) T) L @
  ============================
   false

member_app_absurd < case H2.

2 subgoal(s).

  Variables: M, N, T, L, L1
  IH : forall M N T L, ctx L -> member (of (app M N) T) L * -> false
  H1 : ctx (of (app M N) T :: L1)
  ============================
   false

subgoal 2 is:
 false

member_app_absurd < case H1.

1 subgoal(s).

  Variables: M, N, T, L, L1, B
  IH : forall M N T L, ctx L -> member (of (app M N) T) L * -> false
  H1 : ctx (B :: L1)
  H3 : member (of (app M N) T) L1 *
  ============================
   false

member_app_absurd < case H1.

1 subgoal(s).

  Variables: M, N, T, L, L1, B, L2, T1
  IH : forall M N T L, ctx L -> member (of (app M N) T) L * -> false
  H3 : member (of (app (M n1) (N n1)) (T n1)) L2 *
  H4 : ctx L2
  ============================
   false

member_app_absurd < apply IH to H4 H3.
Proof completed.

Notice that at one point we did case analysis on ctx (of (app M N) T :: L1) which completed that subgoal since ctx restricts the first argument of of to be a nominal constant.

We need a similar lemma for abstractions which I'll simply state and leave you to prove. Hint: the proof is the same as the previous lemma.

Theorem member_abs_absurd : forall L T R T',
  ctx L -> member (of (abs T R) T') L -> false.

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, with a pause which introduces a convenient feature of the apply tactic.

1 subgoal(s).


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

type_uniq_ext < induction on 2.

1 subgoal(s).


  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.

1 subgoal(s).

  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.

3 subgoal(s).

  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
  H3 : {L |- of E T2}
  H4 : member (of E T1) L
  ============================
   T1 = T2

subgoal 2 is:
 arrow T U = T2

subgoal 3 is:
 T1 = T2

type_uniq_ext < case H3.

5 subgoal(s).

  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
  H4 : member (of E T1) L
  H5 : member (of E T2) L
  ============================
   T1 = T2

subgoal 2 is:
 T1 = arrow T U

subgoal 3 is:
 T1 = T2

subgoal 4 is:
 arrow T U = T2

subgoal 5 is:
 T1 = T2

type_uniq_ext < apply member_uniq to H1 H4 H5.

5 subgoal(s).

  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
  H4 : member (of E T2) L
  H5 : member (of E T2) L
  ============================
   T2 = T2

subgoal 2 is:
 T1 = arrow T U

subgoal 3 is:
 T1 = T2

subgoal 4 is:
 arrow T U = T2

subgoal 5 is:
 T1 = T2

type_uniq_ext < search.

4 subgoal(s).

  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
  H4 : member (of (abs T R) T1) L
  H5 : {L, of n1 T |- of (R n1) U}
  ============================
   T1 = arrow T U

subgoal 2 is:
 T1 = T2

subgoal 3 is:
 arrow T U = T2

subgoal 4 is:
 T1 = T2

type_uniq_ext < apply member_abs_absurd to H1 H4.

3 subgoal(s).

  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
  H4 : member (of (app M N) T1) L
  H5 : {L |- of M (arrow U T2)}
  H6 : {L |- of N U}
  ============================
   T1 = T2

subgoal 2 is:
 arrow T U = T2

subgoal 3 is:
 T1 = T2

type_uniq_ext < apply member_app_absurd to H1 H4.

2 subgoal(s).

  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

type_uniq_ext < case H3.

3 subgoal(s).

  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
  H4 : {L, of n1 T |- of (R n1) U}*
  H5 : member (of (abs T R) T2) L
  ============================
   arrow T U = T2

subgoal 2 is:
 arrow T U = arrow T U1

subgoal 3 is:
 T1 = T2

type_uniq_ext < apply member_abs_absurd to H1 H5.

2 subgoal(s).

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

2 subgoal(s).

  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 2 is:
 T1 = T2

type_uniq_ext < search.

1 subgoal(s).

  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

type_uniq_ext < case H3.

2 subgoal(s).

  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
  H4 : {L |- of M (arrow U T1)}*
  H5 : {L |- of N U}*
  H6 : member (of (app M N) T2) L
  ============================
   T1 = T2

subgoal 2 is:
 T1 = T2

type_uniq_ext < apply member_app_absurd to H1 H6.

1 subgoal(s).

  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

type_uniq_ext < apply IH to H1 H4 H6.

1 subgoal(s).

  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

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.
1 subgoal(s).


  ============================
   forall E T1 T2, {of E T1} -> {of E T2} -> T1 = T2

type_uniq < intros.

1 subgoal(s).

  Variables: E, T1, T2
  H1 : {of E T1}
  H2 : {of E T2}
  ============================
   T1 = T2

type_uniq < apply type_uniq_ext to _ H1 H2.

1 subgoal(s).

  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 may wonder about all the lemmas we had to prove. One way to simply this is to define a two generic notions: that a term must be a nominal constant, and that a nominal constant does not appear in another term. We can define both of these as follows.

Define nabla x, name x.
Define nabla x, fresh x E.

Using these definitions makes it easier to avoid excess lemmas. You can look at examples/type_uniq for a development which follows this approach.

Notice that we only used the five primary tactics of Abella: induction, intros, case, apply, and search. This is fairly typical. You should now have a good understanding of these tactics 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 in the reference guide. You are also encourage to specify and reason about your own logical system. If so, please let me hear about it: andrew.gacek@gmail.com.