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.thm]

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

Specification "type-uniq".

%% There are some results about nominal variables, freshness, and lists
%% that we can prove in general.

%% Start generic section

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

% Theorem member_prune : forall G E, nabla (n:tm),
%  member (E n) G -> (exists E', E = x\E').
% induction on 1. intros. case H1.
%  search.
%  apply IH to H2. search.

Theorem member_nominal_absurd : forall L T, nabla x,
  member (of x T) L -> false.

%% End generic section

Close tm, ty.

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

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

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


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

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