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