Type uniqueness for the simply-typed lambda-calculus

Executable Specification

[View type-uniq.sig] [View type-uniq.mod]
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.

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.

Reasoning

[View type-uniq-fresh.thm]

Click on a command or tactic to see a detailed view of its use.

%%
%% This development uses an explicit freshness predicate which may be
%% easier to understand for new users to Abella.

Specification "type-uniq".

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

Define fresh : tm -> o -> prop by
  nabla x, fresh x E.

Define freshlist : tm -> olist -> prop by
  nabla x, freshlist x E.

Theorem member_fresh : forall X L E,
  member E L -> freshlist X L -> fresh X E.

Define ctx : olist -> prop by
  ctx nil ;
  ctx (of X T :: L) := freshlist X L /\ ctx L.

% We could define this second clause as simply
%   Define nabla x, ctx (of x T :: L) := ctx L.
% but it turns out that the version with fresh is much easier to reason with
% since it does not require introducting nominal variables in most cases.
% Moreover, we can use lemmas based on fresh rather than on nominal variables.

Theorem of_name : 
  forall L E,
  ctx L -> member E L ->
  exists X T, E = of X T /\ name X.

Theorem ctx_uniq : forall L E T1 T2,
  ctx L -> member (of E T1) L -> member (of E T2) L -> T1 = T2.

Theorem type_uniq : forall L E T1 T2,
  ctx L -> {L |- of E T1} -> {L |- of E T2} -> T1 = T2.