Disjoint partitioning of lambda terms into normal and non-normal form

Executable Specification

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.

Reasoning

%% 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.