% From Dale Miller: % % It is easy to write code that determines if a given lambda-terms (type % tm) is in beta-normal form (using the fact that a term in normal form % is of the form (lambda x1 ... lambda xn. h t1 ... tn) where t1, ..., % tn are in beta-normal form and h is a variable (one of the x1, ..., % xn, or a variable introduced before). It is also possible to know % that a term is not in beta-normal form since it contains a beta-redex % (in abstract syntax, it would contain a subterm of the form (app (abs % R) M). An interesting theorem to try is the one that says % forall T : tm. (normal T) or (non-normal T). % This one should have a simple proof if the right induction invariant % can be stated. term (app M N) :- term M, term N. term (abs R) :- pi x\ term x => term (R x). non_normal (app (abs R) M). non_normal (app M N) :- non_normal M. non_normal (app M N) :- non_normal N. non_normal (abs R) :- pi x\ non_normal (R x). normal (abs R) :- pi x\ neutral x => normal (R x). normal M :- neutral M. neutral (app M N) :- neutral M, normal N.
Click on a command or tactic to see a detailed view of its use.
%% Disjoint partitioning of lambda terms into normal and non-normal form %% The ctxs predicate encodes the relationship between the context %% of the judgements (term T) and (normal T). Define nabla x, name x. Define ctxs nil nil. Define nabla x, ctxs (term x :: L) (neutral x :: K) := ctxs L K. %% Lemmas about contexts Theorem ctxs_member_term : forall X L K, ctxs L K -> member (term X) L -> member (neutral X) K. [Show Proof][Hide Proof] induction on 1. intros. case H1. case H2. case H2. search. apply IH to H3 H4. search. Theorem ctxs_var : forall E L K, ctxs L K -> member E K -> exists X, E = neutral X /\ name X. [Show Proof][Hide Proof] induction on 1. intros. case H1. case H2. case H2. search. apply IH to H3 H4. search. %% Partitioning is total Theorem total_ext : forall T L K, ctxs L K -> {L |- term T} -> {K |- normal T} \/ {non_normal T}. [Show Proof][Hide Proof] induction on 2. intros. case H2. apply ctxs_member_term to H1 H3. search. apply IH to H1 H3. apply IH to H1 H4. case H5. case H6. case H7. apply ctxs_var to H1 H9. search. search. search. search. apply IH to _ H3. case H4. search. search. Theorem total : forall T, {term T} -> {normal T} \/ {non_normal T}. [Show Proof][Hide Proof] intros. apply total_ext to _ H1. search. %% Partitioning is disjoint Theorem neutral_abs_absurd : forall L K R, ctxs L K -> {K |- neutral (abs R)} -> false. [Show Proof][Hide Proof] intros. case H2. apply ctxs_var to H1 H3. case H4. Theorem disjoint_ext : forall L K T, ctxs L K -> {K |- normal T} -> {non_normal T} -> false. [Show Proof][Hide Proof] induction on 3. intros. case H2. apply ctxs_var to H1 H4. case H3. apply IH to _ H4 H5. case H4. apply ctxs_var to H1 H5. case H6. case H3. case H3. apply neutral_abs_absurd to H1 H5. apply IH to H1 _ H7. apply IH to H1 H6 H7. Theorem disjoint : forall T, {normal T} -> {non_normal T} -> false. [Show Proof][Hide Proof] intros. apply disjoint_ext to _ H1 H2.