%% 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).
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.
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.
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}.
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}.
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.
intros. case H2.
apply ctxs_var to H1 H4. case H3. case H5.
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.
intros. apply disjoint_ext to _ H1 H2.
