Takahashi's proof of Church-Rosser using complete developments

Executable Specification

[View cr.sig] [View cr.mod]
sig cr.

kind     tm                type.

type     app               tm -> tm -> tm.
type     abs               (tm -> tm) -> tm.

type     trm, notabs       tm -> o.
type     pr1, cd1          tm -> tm -> o.
type     beta, betan       tm -> tm -> o.

%% Takahashi's proof of Church-Rosser using complete developments
%% Masako Takahashi, "Parallel reduction in lambda-calculus",
%%   Information and Computation 118(1), April 1995.
%%
%% Abella proof contributed by Randy Pollack

module cr.

% pure lambda terms
trm (app M N) :- trm M, trm N.
trm (abs R) :- pi x\ trm x => trm (R x).

% one step of Tait/Martin-Loef parallel reduction
pr1 (app T1 S1) (app T2 S2) :- pr1 T1 T2, pr1 S1 S2.
pr1 (abs S1) (abs S2) :- pi x\ pr1 x x => pr1 (S1 x) (S2 x).
pr1 (app (abs T1) S1) (T2 S2) :- pr1 (abs T1) (abs T2), pr1 S1 S2.

% a trm is not an abstraction
notabs (app M N).

% one step of complete development
% For a useful explanation of this coding, see
% http://twelf.plparty.org/wiki/Reformulating_languages_to_use_hypothetical_judgements
cd1 (app T1 S1) (app T2 S2) :- notabs T1, cd1 T1 T2, cd1 S1 S2.
cd1 (abs S1) (abs S2) :- pi x\ notabs x => cd1 x x => cd1 (S1 x) (S2 x).
cd1 (app (abs T1) S1) (T2 S2) :- cd1 (abs T1) (abs T2), cd1 S1 S2.

% ordinary one-step beta reduction
beta (app M N) (app M' N) :- beta M M'.
beta (app M N) (app M N') :- beta N N'.
beta (abs S1) (abs S2) :- pi x\ beta (S1 x) (S2 x).
beta (app (abs R) M) (R M).

% beta*
betan M M.
betan M N :- beta M P, betan P N.

Reasoning

[View cr.thm]

Click on a command or tactic to see a detailed view of its use.

%% Masako Takahashi, "Parallel reduction in lambda-calculus",
%%   Information and Computation 118(1), April 1995.
%%
%% Abella proof contributed by Randy Pollack

Specification "cr".

Define ctxs : olist -> olist -> olist -> prop by
  ctxs nil nil nil ;
  nabla x, ctxs (trm x :: L) (pr1 x x :: K) (cd1 x x :: notabs x :: J) :=
    ctxs L K J.

Define name : tm -> prop by
  nabla x, name x.

%% properties of correct contexts
Theorem trm_worlds : forall L K J E,
  ctxs L K J -> member E L ->
  exists A, E = trm A /\
    name A /\ member (pr1 A A) K /\ member (cd1 A A) J /\
      member (notabs A) J.

Theorem pr1_worlds : forall L K J E,
  ctxs L K J -> member E K ->
  exists A B, E = pr1 A B /\
    name A /\ A = B /\ member (trm A) L /\
     member (cd1 A B) J /\ member (notabs A) J.

Theorem cd_worlds : forall L K J E,
  ctxs L K J -> member E J ->
   (exists A B, E = cd1 A B /\
     name A /\ A = B /\ member (trm A) L /\
       member (pr1 A A) K /\ member (notabs A) J)
\/ (exists A, E = notabs A /\
     name A /\ member (trm A) L /\ member (pr1 A A) K /\
       member (cd1 A A) J).

%% The meaning of "notabs" is as expected
Theorem notabs_abs_absurd: forall A L K J,
   ctxs L K J -> {J |- notabs (abs A)} -> false.

% {J |- cd1 A B} implies A is a term
Theorem cd1_trm : forall A B L K J,
  ctxs L K J -> {J |- cd1 A B} -> {L |- trm A}.

% similarly, {K |- pr1 A B} implies A is a term
Theorem pr1_trm : forall A B L K J,
  ctxs L K J -> {K |- pr1 A B} -> {L |- trm A}.

%% Just for information, every cd1 step is a pr1 step.
%% Proof by induction over term structure, but second hypothesis
%% is derivable.
Theorem pre_cd1_pr1 : forall A B L K J,
  ctxs L K J -> {L |- trm A} -> {J |- cd1 A B} -> {K |- pr1 A B}.

Theorem cd1_pr1 : forall A B L K J,
  ctxs L K J -> {J |- cd1 A B} -> {K |- pr1 A B}.

%% pr1 is reflexive
Theorem pr1_rfl : forall A L K J,
  ctxs L K J -> {L |- trm A} -> {K |- pr1 A A}.

%% cd1 has no overlap between rules, so is a functional relation
Theorem cd1_unique: forall A B C L K J,
  ctxs L K J -> {J |- cd1 A B} -> {J |- cd1 A C} -> B = C.

%% now to show pr1 has diamond property (Takahashi proof, using cd1)

%% There is a cd1 step from every trm
Theorem cd1_exists : forall A L K J,
  ctxs L K J -> {L |- trm A} -> exists B, {J |- cd1 A B}.

%% inversion lemmas about the shape of pr1 steps
Theorem pr1_name: forall A B L K J,
     ctxs L K J -> {K |- pr1 A B} -> name A -> B = A.

Theorem pr1_abs: forall R B L K J,
  ctxs L K J -> {K |- pr1 (abs R) B} -> exists S, B = (abs S).

Theorem pre_pr1_subst_lem: forall A1 A2 B1 B2 L K J, nabla x,
  ctxs L K J -> {K, pr1 x x |- pr1 (A1 x) (A2 x)} -> {K |- pr1 B1 B2} ->
         {K |- pr1 (A1 B1) (A2 B2)}.

Theorem pr1_subst_lem: forall A1 A2 B1 B2 L K J,
 ctxs L K J ->
    {K |- pr1 (abs A1) (abs A2)} -> {K |- pr1 B1 B2} ->
         {K |- pr1 (A1 B1) (A2 B2)}.

%% The key lemma that allows to show that pr1 has the diamond
%% property.
Theorem cd1_pr1_triangle : forall A B C L K J,
     ctxs L K J -> {K |- pr1 A B} -> {J |- cd1 A C} -> {K |- pr1 B C}.

%% The main result
Theorem pr1_diamond : forall A B1 B2 L K J,
   ctxs L K J -> {K |- pr1 A B1} -> {K |- pr1 A B2} ->
        exists C, {K |- pr1 B1 C} /\ {K |- pr1 B2 C}.