%%% The Church-Rosser theorem for parallel reduction
%%% Author: Frank Pfenning
%%% Modified by Adam Poswolsky so subst creates a parametric function that can be used to 
%%%%  perform the substitution in dia.

subst : ({x:term} x => x -> M x => M' x) -> ({x:term}{y:term} x => y -> M x => M' y) -> type.
%mode subst +R -R'.

subst_idx : subst ([x:term] [idx: x => x] idx) ([x][y][r] r).

subst_beta : subst ([x:term] [idx: x => x] beta (R1 x idx) (R2 x idx)) ([x][y][r : x => y] beta (R1' x y r) (R2' x y r))
	    <- ({z}{idz} subst ([x][idx : x => x] R1 x idx z idz) ([x][y][r] R1' x y r z idz))
	    <- subst R2 R2'.

subst_ap  : subst ([x:term] [idx: x => x] ap (R1 x idx) (R2 x idx)) ([x][y][r] ap (R1' x y r) (R2' x y r))
	    <- subst R1 R1'
	    <- subst R2 R2'.

subst_lm  : subst ([x:term] [idx: x => x] lm (R1 x idx)) ([x][y][r] lm (R1' x y r))
          <- ({z}{idz} subst ([x][idx : x => x] R1 x idx z idz) ([x][y][r] R1' x y r z idz)).

subst_lmBase : subst ([x][idx] R) ([x][y][r] R).

%block l1 : block {x:term} {idx: x => x}.
%worlds (l1) (subst R R').
%covers subst +R -R'.
%terminates R (subst R _).
%total R (subst R _).



% Diamond property for parallel reduction

dia : M => M'  ->  M => M''  ->  M' => N  ->  M'' => N  -> type.
% %mode +{M} +{M'} +{M''} +{R':M => M'} +{R'':M => M''}
%      -{N} -{S':M' => N} -{S'':M'' => N} dia R' R'' S' S''.

%mode dia +R' +R'' -S' -S''.

% Proof by induction on the structure of the first two derivations.
% We consider the various possible cases.
% b = beta, a = ap, l = lm,

dia_bb : dia (beta R1' R2') (beta R1'' R2'') (S1'G _ _ S2') (S1''G _ _ S2'')
      <- ({x:term} {idx: x => x} dia idx idx idx idx
            -> dia (R1' x idx) (R1'' x idx)
                   (S1' x idx) (S1'' x idx))
      <- dia R2' R2'' S2' S2''
      <- subst S1' S1'G
      <- subst S1'' S1''G.


dia_bal : dia (beta R1' R2') (ap (lm R1'') R2'')
             (S1'G _ _ S2') (beta S1'' S2'')
       <- ({x:term} {idx: x => x} dia idx idx idx idx
             -> dia (R1' x idx) (R1'' x idx)
                    (S1' x idx) (S1'' x idx))
       <- dia R2' R2'' S2' S2''
       <- subst S1' S1'G.

dia_alb : dia (ap (lm R1') R2') (beta R1'' R2'')
             (beta S1' S2') (S1''G _ _ S2'')
       <- ({x:term} {idx: x => x} dia idx idx idx idx
             -> dia (R1' x idx) (R1'' x idx)
                    (S1' x idx) (S1'' x idx))
       <- dia R2' R2'' S2' S2''
       <- subst S1'' S1''G.

dia_aa  : dia (ap R1' R2') (ap R1'' R2'') (ap S1' S2') (ap S1'' S2'')
       <- dia R1' R1'' S1' S1''
       <- dia R2' R2'' S2' S2''.

dia_ll  : dia (lm R1') (lm R1'') (lm S1') (lm S1'')
       <- ({x:term} {idx: x => x} dia idx idx idx idx
             -> dia (R1' x idx) (R1'' x idx) (S1' x idx) (S1'' x idx)).

%block l2 : block {x:term} {idx:x => x}
	     {hd: dia idx idx idx idx}.
%worlds (l2) (dia _ _ _ _).
%covers dia +R' +R'' -S' -S''.
%terminates [R' R''] (dia R' R'' _ _).
%total [R' R''] (dia R' R'' _ _).

% The strip lemma for parallel reduction.

strip : M => M'  ->  M =>* M''  ->  M' =>* N  ->  M'' => N -> type.
% %mode +{M} +{M'} +{M''} +{R':M => M'} +{R'':M =>* M''}
%       -{N} -{S*':M' =>* N} -{S'':M'' => N} strip R' R'' S*' S''.
%mode strip +R' +R'' -S*' -S''.

strip_id   : strip R' id id R'.
strip_step : strip R' (R1'' ; R2*'') (S1' ; S2*') S''
          <- dia R' R1'' S1' S1''
          <- strip S1'' R2*'' S2*' S''.

%worlds () (strip R' R'' S*' S'').
%covers strip +R' +R'' -S*' -S''.
%terminates R'' (strip R' R'' _ _).
%total R'' (strip R' R'' _ _).

% Confluence for parallel multi-step reduction.

conf :  M =>* M'  ->  M =>* M''  ->  M' =>* N  ->  M'' =>* N -> type.
% %mode +{M} +{M'} +{M''} +{R*':M =>* M'} +{R*'':M =>* M''}
%      -{N} -{S*':M' =>* N} -{S*'':M'' =>* N} conf R*' R*'' S*' S*''.
%mode conf +R*' +R*'' -S*' -S*''.

conf_id   : conf id R*'' R*'' id.
conf_step : conf (R1' ; R2*') R*'' S*' (S1'' ; S2*'')
         <- strip R1' R*'' S1*' S1''
         <- conf R2*' S1*' S*' S2*''.

%worlds () (conf R*' R*'' S*' S*'').
%covers conf +R*' +R*'' -S*' -S*''.
%terminates R*' (conf R*' R*'' _ _).
%total R*' (conf R*' R*'' _ _).

% Church-Rosser Theorem for parallel reduction

cr :  M <=> M'  ->  M =>* N  ->  M' =>* N  -> type.
% %mode +{M} +{M'} +{C:M <=> M'}
%       -{N} -{S*:M =>* N} -{S*':M' =>* N} cr C S* S*'.
%mode cr +C -S* -S*'.

cr_reduce  : cr (reduce R*) R* id.
cr_expand  : cr (expand R*) id R*.
cr_compose : cr (C1 ;; C2) S* S*'
          <- cr C1 S1* R1*
          <- cr C2 R2* S2*
          <- conf R1* R2* T1* T2*
          <- append S1* T1* S*
          <- append S2* T2* S*'.

%worlds () (cr C S* S*').
%covers cr +C -S* -S*'.
%terminates C (cr C _ _).
%total C (cr C _ _).