# sred.thm

%% Ralph Loader's proof of standardization %% (Notes on Simply Typed Lambda Calculus, ECS-LFCS-98-381) %% an adaption of Hongwei Xi's arithmetical proof %% (Upper bounds for standardizations and an application, JSL 1999) %% to Gordon Plotkin's inductive formulation of standard reduction. %% (Call-by-name, Call-by-value and the Lambda-Calculus, TCS 1975) %% %% Abella proof by Andreas Abel (October 2009) Specification "sred". %% Technical lemma about fresh variables. Theorem member_prune : forall E (L:olist), nabla (x:tm), member (E x) L -> exists F, E = y\F. induction on 1. intros. case H1. search. apply IH to H2. search. %% Matching contexts of term variables x and x -->s x. Define ctx : olist -> olist -> prop by ctx nil nil ; nabla x, ctx (tm x :: C) (sred x x :: D) := ctx C D. Theorem ctx_member1 : forall C D H, ctx C D -> member H C -> exists X, H = tm X /\ member (sred X X) D. induction on 2. intros. case H2. case H1. search. case H1. apply IH to H4 H3. search. Theorem ctx_member2 : forall C D H, ctx C D -> member H D -> exists X, H = sred X X /\ member (tm X) C. induction on 2. intros. case H2. case H1. search. case H1. apply IH to H4 H3. search. %% Technical lemma: weak head reduction is independent of context. Theorem wh_ctx : forall C D T T', ctx C D -> {D |- wh T T'} -> {wh T T'}. induction on 2. intros. case H2. search. apply IH to H1 H3. search. apply ctx_member2 to H1 H4. case H3. %% Standard reduction is reflexive. Theorem srefl : forall C D T, ctx C D -> {C |- tm T} -> {D |- sred T T}. induction on 2. intros. case H2. apply IH to H1 H3. apply IH to H1 H4. search. apply IH to _ H3. search. apply ctx_member1 to H1 H4. case H3. search. %% Standard reduction is closed under substitution. Theorem ssubst : forall C D T T' S S', nabla x, ctx C D -> {D, sred x x |- sred (T x) (T' x)} -> {D |- sred S S'} -> {D |- sred (T S) (T' S')}. induction on 2. intros. case H2. %% case weak head step apply IH to H1 H5 H3. apply wh_ctx to _ H4. inst H7 with n1 = S. search. %% case: application apply IH to H1 H4 H3. apply IH to H1 H5 H3. search. %% case: abstraction apply IH to _ H4 H3. search. %% case hypothesis case H5. case H4. search. apply ctx_member2 to H1 H6. case H4. apply member_prune to H6. search. %% Variables do not beta reduce. Theorem name_not_beta : forall T, nabla x, {beta x T} -> false. intros. case H1. Theorem var_not_beta : forall C D T T', ctx C D -> member (tm T) C -> {beta T T'} -> false. induction on 2. intros. case H2. case H1. case H3. case H1. apply IH to H5 H4 H3. %% Variables are not abstractions. Theorem var_not_abs : forall C D R, ctx C D -> member (tm (abs R)) C -> false. induction on 2. intros. case H2. case H1. case H1. apply IH to H4 H3. %% Applying a sred which ends in a lambda, removing the resulting redex. Theorem sred_beta : forall C D M N N' R, ctx C D -> {D |- sred M (abs R)} -> {D |- sred N N'} -> {D |- sred (app M N) (R N')}. induction on 2. intros. case H2. % weak head reduction case apply IH to H1 H5 H3. search. % abstraction case apply ssubst to H1 H4 H3. search. % variable case (impossible) apply ctx_member2 to H1 H5. case H4. apply var_not_abs to H1 H6. %% Main Lemma: %% Standard reduction is closed under appending a beta step. Theorem sappend : forall C D T T' T'', ctx C D -> {D |- sred T T'} -> {beta T' T''} -> {D |- sred T T''}. induction on 2. intros. case H2. % weak head step case apply IH to H1 H5 H3. search. % application case case H3. % cases on beta step. % subcase reduction in function part apply IH to H1 H4 H6. search. % subcase reduction in argument part apply IH to H1 H5 H6. search. % subcase beta-contraction apply sred_beta to H1 H4 H5. search. % abstraction case case H3. apply IH to _ H4 H5. search. % variable case apply ctx_member2 to H1 H5. case H4. apply var_not_beta to H1 H6 H3. %% QED ! %% Theorem: Each beta reduction sequence can be standardized. Theorem standardization: forall T T', {tm T} -> {betas T T'} -> {sred T T'}. induction on 2. intros. case H2. apply srefl to _ H1. search. apply IH to H1 H3. apply sappend to _ H5 H4. search.