sig normal. kind tm type. type app tm -> tm -> tm. type abs (tm -> tm) -> tm. type term tm -> o. type non_normal tm -> o. type neutral, normal tm -> o.
% From Dale Miller: % % It is easy to write code that determines if a given lambda-term (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. module normal. 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.
%% The ctxs predicate encodes the relationship between the context %% of the judgements (term T) and (normal T). Specification "normal". Define name : tm -> prop by nabla x, name x. Define ctxs : olist -> olist -> prop by ctxs nil nil ; nabla x, ctxs (term x :: L) (neutral x :: K) := ctxs L K. %% Lemmas about contexts Theorem ctxs_member_term : forall L K E, ctxs L K -> member E L -> exists X, E = term X /\ member (neutral X) K /\ name X. Theorem ctxs_var : forall E L K, ctxs L K -> member E K -> exists X, E = neutral X /\ name X. %% Partitioning is total Theorem total_ext : forall T L K, ctxs L K -> {L |- term T} -> {K |- normal T} \/ {non_normal T}.induction on 2. intros. case H2. apply IH to H1 H3. apply IH to H1 H4. case H5. case H6. case H7. search. search. apply ctxs_var to H1 H10. case H9. search. search. apply IH to _ H3. case H4. search. search. apply ctxs_member_term to H1 H4. case H3. search.Theorem total : forall T, {term T} -> {normal T} \/ {non_normal T}. %% Partitioning is disjoint Theorem neutral_abs_absurd : forall L K R, ctxs L K -> {K |- neutral (abs R)} -> false. Theorem disjoint_ext : forall L K T, ctxs L K -> {K |- normal T} -> {non_normal T} -> false.induction on 3. intros. case H2. case H3. apply IH to _ H4 H5. case H4. case H3. apply neutral_abs_absurd to H1 H5. apply IH to H1 _ H7. apply IH to H1 H6 H7. apply ctxs_var to H1 H6. case H5. case H7. case H3. apply ctxs_var to H1 H5. case H4.Theorem disjoint : forall T, {normal T} -> {non_normal T} -> false.