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.
Click on a command or tactic to see a detailed view of its use.
%% Type uniqueness for the simply-typed lambda-calculus %% There are some results about nominal variables, freshness, and lists %% that we can prove in general. %% Start generic section Define nabla x, name x. Define nabla x, fresh x E. Theorem member_fresh : forall X L E, member E L -> fresh X L -> fresh X E. [Show Proof][Hide Proof] induction on 1. intros. case H1. case H2. search. assert fresh X L1. case H2. search. apply IH to H3 H4. search. %% End generic section Define ctx nil. Define ctx (of X T :: L) := fresh 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 T, ctx L -> member (of E T) L -> name E. [Show Proof][Hide Proof] induction on 2. intros. case H1. case H2. case H2. case H3. search. apply IH to H4 H5. search. Theorem ctx_uniq : forall L E T1 T2, ctx L -> member (of E T1) L -> member (of E T2) L -> T1 = T2. [Show Proof][Hide Proof] induction on 1. intros. case H1. case H2. case H2. case H3. search. apply member_fresh to H6 H4. case H7. case H3. apply member_fresh to H6 H4. case H7. apply IH to H5 H6 H7. search. Theorem type_uniq : forall L E T1 T2, ctx L -> {L |- of E T1} -> {L |- of E T2} -> T1 = T2. [Show Proof][Hide Proof] induction on 2. intros. case H2. case H3. apply ctx_uniq to H1 H4 H5. search. apply of_name to H1 H4. case H6. apply of_name to H1 H4. case H7. case H3. apply of_name to H1 H5. case H6. apply IH to _ H4 H5. search. case H3. apply of_name to H1 H6. case H7. apply IH to H1 H4 H6. search.