%% Type uniqueness for the simply-typed lambda-calculus
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.
induction on 1. intros. case H1. apply IH to H2.
%% 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.
induction on 2. intros. case H2.
case H3.
search.
case H1. apply member_nominal_absurd to H4.
case H3.
case H1. apply member_nominal_absurd to H4.
case H1. apply IH to H6 H4 H5. search.
Theorem ctx_mem :
forall L E,
ctx L -> member E L ->
exists N X, E = of X N /\ name X.
induction on 2. intros. case H2.
case H1. search.
case H1.
apply IH to H4 H3. search.
Theorem type_uniq_ext : forall L E T1 T2,
ctx L -> {L |- of E T1} -> {L |- of E T2} -> T1 = T2.
induction on 2. intros. case H2.
case H3.
apply IH to _ H4 H5. search.
apply ctx_mem to H1 H6. case H7. case H5.
case H3.
apply IH to H1 H4 H6. search.
apply ctx_mem to H1 H7. case H8. case H6.
apply ctx_mem to H1 H5. case H4. case H6.
case H3. apply ctx_mem to H1 H8. case H7.
apply ctx_uniq to H1 H5 H8. search.
Theorem type_uniq : forall E T1 T2,
{of E T1} -> {of E T2} -> T1 = T2.
intros. apply type_uniq_ext to _ H1 H2. search.
