sig stlc. kind tm, ty type. type arr ty -> ty -> ty. type b ty. type app tm -> tm -> tm. type abs ty -> (tm -> tm) -> tm. type ty ty -> o. type tm tm -> o.
module stlc. ty b. ty (arr T1 T2) :- ty T1, ty T2. tm (app M1 M2) :- tm M1, tm M2. tm (abs T R) :- ty T, pi x\ tm x => tm (R x).
Click on a command or tactic to see a detailed view of its use.
Specification "stlc". %% The strengthening lemma in Section 5.1 and its proof Theorem ty_indep_tm_simp : forall T, nabla x, {tm x |- ty (T x)} -> exists T', T = y\T' /\ {ty T'}.induction on 1. intros. case H1. % Case: T x = b search. % Case: T x = arr (T1 x) (T2 x) apply IH to H2. apply IH to H3. search. % Case: context case H3. case H2. case H4.Define name : tm -> prop by nabla x, name x. Define ctx : olist -> prop by ctx nil; nabla x, ctx (tm x :: L) := ctx L. Theorem ctx_mem : forall L E, ctx L -> member E L -> exists X, E = tm X /\ name X. %% The strengthening lemma in B.3 which is used in Section 5.3 Theorem ty_indep_tm : forall L T, nabla x, ctx L -> {L, tm x |- ty (T x)} -> exists T', T = y\T' /\ {L |- ty T'}.induction on 2. intros. case H2. % Case: T x = b search. % Case: T x = arr (T1 x) (T2 x) apply IH to _ H3. apply IH to _ H4. search. % Case: context case H4. case H3. apply ctx_mem to H1 H5. case H3.