%%% Basic lemmas concerning parallel reductions
%%% Author: Frank Pfenning
% Every lc.term reduces to itself (in parallel)

%sig BASIC = {
    %struct lc: LC %open term lam app.
    %struct par: PAR = {%struct lc := lc.} %open => beta ap lm. 

    identity : {M:term} M par.=> M  ->  type.

    %mode identity +M -R.
    %block lid : block {x:term}
               {eqx: x par.=> x}
                {u:identity x eqx}.
    
    id_lam : identity (lam M1) (par.lm R1)
       <- ({x:term} {eqx: x par.=> x}
	     identity x eqx -> identity (M1 x) (R1 x eqx)).

     id_app : identity (app M1 M2) (par.ap R1 R2)
       <- identity M1 R1
       <- identity M2 R2.

    %worlds (lid) (identity M R).
    %covers identity +M -R.
    %total M (identity M _).
    %terminates M (identity M _).
    %total M (identity M _).


%  Parallel multi-step reduction is transitive.

    append : M par.=>* M'  ->  M' par.=>* M''  ->  M par.=>* M''  -> type.
    %mode append +R* +S* -S*'.

    append_id   : append par.id S* S*.
    append_step : append (R1 par.; R2*) S* (R1 par.; S2*')
           <- append R2* S* S2*'.

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


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

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

subst_beta : subst ([x:term] [idx: x => x] beta (R1 x idx) (R2 x idx))
                   S (beta R1' R2')
           <- ({y:term} {idy: y => y}
                 ({N}{N'}{S':N => N'} subst ([x:term] [idx: x => x] idy) S' idy)
                 -> subst ([x:term] [idx: x => x] R1 x idx y idy)
                          S (R1' y idy))
           <- subst R2 S R2'.

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

subst_lm  : subst ([x:term] [idx: x => x] lm (R1 x idx))
                  S (lm R1')
          <- ({y:term} {idy: y => y}
                ({N}{N'}{S':N => N'}subst ([x:term] [idx: x => x] idy) S' idy)
                -> subst ([x:term] [idx: x => x] R1 x idx y idy)
                         S (R1' y idy)).


%block l1 : block {x:term A} {idx: x => x}
	     {hs: {N:term} {N':term} {S':N => N'}
		   subst ([y:term][idy:y => y] idx) S' idx}.
%worlds (l1) (subst R S R').
%covers subst +R +S -R'.
%terminates R (subst R S _).
%total R (subst R S _).

% 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'') S' S''
      <- ({x:term} {idx: x => x}
	    ({N}{N'}{S':N => N'}subst ([y:term] [idy: y => y] idx) S' idx)
            -> 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' S2' S'
      <- subst S1'' S2'' S''.

dia_bal : dia (beta R1' R2') (ap (lm R1'') R2'')
             S' (beta S1'' S2'')
       <- ({x:term} {idx: x => x}
	    ({N}{N'}{S':N => N'}subst ([y:term] [idy: y => y] idx) S' idx)
             -> 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' S2' S'.

dia_alb : dia (ap (lm R1') R2') (beta R1'' R2'')
             (beta S1' S2') S''
       <- ({x:term} {idx: x => x}
	    ({N}{N'}{S':N => N'}subst ([y:term] [idy: y => y] idx) S' idx)
             -> 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'' S2'' S''.

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}
	     ({N}{N'}{S':N => N'}subst ([y:term] [idy: y => y] idx) S' idx)
	     -> 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}
	     {hs: {N:term} {N':term} {S':N => N'} subst ([y:term][idy:y => y] idx) S' idx}
	     {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 _ _).
}.