Advanced walkthrough: type uniqueness
This walkthrough assumes you have finished the
beginner's walkthrough and are familiar with induction,
intros, case, apply, and search. You will learn how to use lemmas and
how to state and use definitions.
The presentation is the simply-typed lambda-calculus. Simple types are built from base types using the function type constructor, and the language of types does not include type variables. At the level of terms, atoms are assumed to have specific types from the beginning. We consider terms built using applications and abstractions, with the type of an abstracted variable given by an annotation on the abstraction. The property we prove is that every well-formed term has exactly one type.
Executable specification
The walkthrough uses the following signature, saved in type-uniq.sig.
sig type-uniq.
kind tm, ty type.
type app tm -> tm -> tm.
type abs ty -> (tm -> tm) -> tm.
type arrow ty -> ty -> ty.
type of tm -> ty -> o.
The difference from the first walkthrough is that abs takes two arguments:
the type of the abstracted variable and the abstraction itself.
The typing specification 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.
The rule for abstractions uses the type annotation attached to the abstraction.
Reasoning
The specification is included with Abella in
examples/lambda-calculus/type-uniq. Load it as follows.
$ abella
Welcome to Abella 2.1.0-dev.
Abella < Specification "type-uniq".
Reading specification "./type-uniq".
Abella <
State type uniqueness as follows.
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}, introduce the variables, and then
do case analysis on {of E T1}. This produces two subgoals corresponding to
the two specification rules. The first subgoal is when E is an abstraction;
the second 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, so case analysis on this hypothesis acts
like unfolding the judgment.
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 applying the inductive hypothesis to
{of n1 T |- of (R n1) U}* and {of n1 T |- of (R n1) U1} fails.
apply IH to H3 H4.
Error: Contexts did not match
The theorem was stated for typing judgments with an empty context of
hypothetical assumptions. We can think of {of E T1} as
{nil |- of E T1}. Applying the inductive hypothesis to judgments with
non-empty contexts fails. We need to generalize the theorem over the possible
contexts in which typing judgments are made. Roughly, we want the following.
forall L E T1 T2, {L |- of E T1} -> {L |- of E T2} -> T1 = T2.
This statement is too general and, in fact, not true. We are only interested in contexts that assign types to terms. Moreover, the relevant contexts should assign types only to nominal constants, and at most one type to each such constant. Without this uniqueness assumption the proposition cannot be true.
We realize the restriction by defining a property ctx that good contexts
satisfy, and requiring it to hold of L. First type abort. to give up on
the previous proof attempt. Then enter the definition of ctx.
abort.
Define ctx : olist -> prop by
ctx nil ;
nabla x, ctx (of x T :: L) := ctx L.
The system accepts this command with no output. The definition says that the
empty list is a well-formed context, and that 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. The type of ctx 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 ensures that the following atomic formula is provable in the reasoning logic.
ctx (of n1 T1 :: of n2 T2 :: of n3 T3 :: nil)
It 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)
The first non-example says that a context cannot contain more than one typing
judgment for the same nominal constant. Proving this fact requires another
property about the non-occurrence of nominal constants with a particular scope
in a list. This property is stated using the predicate member, which Abella
already defines. At type olist it is
member : o -> olist -> prop
with the usual clauses for an element of a list. See Reasoning logic for the built-in constants.
The property we need is the following lemma.
Theorem member_nominal_absurd : forall L T, nabla x,
member (of x T) L -> false.
Before proving it, consider the following simpler observation.
Theorem non_occurrence : forall L, nabla (x:tm),
(x = L) -> false.
The order in which L and x are quantified enforces that any nominal
constant substituted for x cannot appear in the term substituted for L.
Abella understands this, so the theorem is easily proved with intros and
case H1.
Given non_occurrence, one might wonder whether member_nominal_absurd
follows immediately. It does not: L is a list constructed using the
definition of member, and the non-occurrence property must be factored
through that definition.
The proof of member_nominal_absurd is as follows.
============================
forall L T, nabla x, member (of x T) L -> false
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
intros.
Variables: L, T
IH : forall L T, nabla x, member (of x T) L * -> false
H1 : member (of n1 T) L @
============================
false
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
apply IH to H2.
Proof completed.
When we did case H1, we did not have to consider the subgoal where of n1 T
is at the head of L. The fact that the instantiation of L cannot contain
n1 is used here.
If we now attempt to prove uniqueness for contexts, we still run into a
problem: we encounter terms of the form T n1 where T has type ty and
n1 is a nominal constant of type tm. Such terms are absurd because a term
of type tm cannot appear inside a term of type ty. Abella does not know
this, because a new constant with type tm -> ty could later be introduced.
To say that such constants will never be introduced, declare tm and ty to
be closed.
Close tm, ty.
Now state 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.
Prove this by induction on member (of E T1) L, then intros, then case
analysis on member (of E T1) L. This produces two subgoals based on whether
of E T1 occurs at the head or in the tail of L.
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, case analysis on member (of E T2) (of E T1 :: L1)
replaces the current subgoal with two new subgoals, for a total of three. The
first is when of E T2 is at the head of the list, which means T1 = T2, so
search handles it. 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
The first subgoal says 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.
Perform case analysis on ctx (of E T1 :: L1). This is interesting because
ctx was defined with a nabla quantifier in the head of the definition.
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
The clause can apply only if E is a nominal constant and T1 and L1 are
restricted to terms that do not contain this nominal constant. The rule
introduces a new nominal constant for E and requires that newly introduced
eigenvariables not contain it, while previously available eigenvariables may
use it. This mechanism is called raising.
Complete the subgoal by applying the lemma about occurrences of nominal constants.
apply member_nominal_absurd to H4.
Only the following subgoal remains.
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
Perform case analysis on member (of E T2) (B :: L1), which generates two
subgoals. The first is symmetric to the previous one; the other 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
To apply the inductive hypothesis we need a judgment such as ctx L1. Case
analysis on H1 produces it, and the raising of eigenvariables has no effect
on the rest of the proof.
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
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
search.
Proof completed.
We need one more property before proving the generalized theorem. We have shown that well-formed contexts cannot have two typing judgments for the same variable, but we still have to show that such contexts contain typing judgments only for nominal constants. Define a notation for being 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. The structural property of a well-formed context is an inspection of
its definition.
Theorem ctx_mem : forall L E,
ctx L -> member E L -> exists N X, E = of X N /\ name X.
The proof is straightforward.
induction on 2. intros. case H2.
case H1. search.
case H1.
apply IH to H4 H3. search.
Proof completed.
At one point we did case analysis on ctx (E :: L1), which exposes E as
of n1 T. Since n1 is a nominal constant, search completes the subgoal.
Now state the 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 is by induction on one of the typing judgments. The body considers
the possible ways in which the two typing judgments are derived. Because the
judgments have non-empty contexts, we must consider that, for example,
of E T1 comes directly from the context L. Case analysis on a hypothesis
like {L |- of E T1} therefore results in three subgoals.
The first case is when 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
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
We are now considering the case when E is the abstraction abs T R and the
typing judgments are formed using the abstraction rule. The typing context has
grown to include a typing assumption for a new nominal constant n1. To apply
the inductive hypothesis to the new typing judgments for R n1, we must
ensure that of n1 T :: L is a well-formed context. This is easy, since
neither T nor L can depend on n1.
One option is to use assert to state ctx (of n1 T :: L) and prove it with
search. A more convenient option is apply with unknowns: put _ where a
hypothesis is needed and let the prover guess what must be proved and try
search. If search fails, the current subgoal is delayed and the unknown
hypothesis becomes the current goal. Here ctx (of n1 T :: L) is solved by
search, so no extra subgoal is generated.
apply IH to _ H4 H5.
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
search.
The next subgoal is when the typing judgment comes from a clause in the context. This is where backchaining judgments appear.
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
A judgment of the form {L, [F] |- G} is a backchaining judgment. It says
that G, here of (abs T R) T2, is proved by backchaining on some formula
F in the context L. The hypothesis member F L shows that F is
contained in L.
Case analysis on H5 fails, because the structure of F is unknown.
case H5.
Error: Cannot perform case-analysis on flexible head
Apply ctx_mem to reveal that F has the form of X N.
apply ctx_mem to H1 H6.
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
Now perform case analysis on H5, which backchains the goal on the clause
of X N.
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
As a result of backchaining, X is unified with abs T R. Case analysis on
H7 completes the subgoal, because abs T R is not a nominal constant.
case H7.
The case where E is an application is proved similarly.
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
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
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
search.
The next subgoal is also a backchaining case.
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
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
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
case H8.
The last case is when the goal formula is derived from a clause F in the
context. Apply ctx_mem to reveal the structure of F, then case-analyze the
backchaining judgment.
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
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
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
case H6.
The case analysis reveals that E is a nominal constant. Eigenvariables are
raised over n1 because of their dependency on it. The goal formula of n1 T2
in H3 can only be derived from the context, because n1 cannot be an
abstraction or an application. The same technique for backchaining judgments
is used 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
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
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
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
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.
Applying ctx_uniq proves 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
search.
Proof completed.
We can now use the generalized theorem to prove the specific theorem. Watch for another use of apply with unknowns.
Theorem type_uniq : forall E T1 T2,
{of E T1} -> {of E T2} -> T1 = T2.
intros.
Variables: E, T1, T2
H1 : {of E T1}
H2 : {of E T2}
============================
T1 = T2
apply type_uniq_ext to _ H1 H2.
Variables: E, T1, T2
H1 : {of E T2}
H2 : {of E T2}
============================
T2 = T2
search.
Proof completed.
You have now proved type uniqueness for the simply-typed lambda-calculus. The
full development is in examples/lambda-calculus/type-uniq/type-uniq.thm.
You should now understand the most common tactics in Abella, as well as definitions and lemmas. With this knowledge you can read the examples included with Abella. You are also encouraged to specify and reason about your own logical system.