%%% Equivalence of ordinary and parallel reduction.
%%% Author: Frank Pfenning

% If M => N then M -->* N.

eq1 : M => N  ->  M -->* N  ->  type.
%mode eq1 +R -S*.

eq1_beta : eq1 (beta R1 R2) S*
         <- ({x:term} {eqx : x => x}
               eq1 eqx id1 -> eq1 (R1 x eqx) (S1* x))
         <- lm1* S1* S1*'
         <- apl1* S1*' S1*''
         <- eq1 R2 S2*
         <- apr1* S2* S2*'
         <- appd S2*' (step1 beta1 id1) S*'
         <- appd S1*'' S*' S*.

eq1_ap : eq1 (ap R1 R2) S*
       <- eq1 R1 S1*
       <- apl1* S1* S*'
       <- eq1 R2 S2*
       <- apr1* S2* S*''
       <- appd S*' S*'' S*.

eq1_lm : eq1 (lm R1) S*
       <- ({x:term} {eqx : x => x}
             eq1 eqx id1 -> eq1 (R1 x eqx) (S1* x))
       <- lm1* S1* S*.

% If M --> N then M => N.

eq2 : M --> N  ->  M => N  ->  type.
%mode eq2 +R -S.

eq2_beta1 : eq2 (beta1) (beta I1 I2)
          <- ({x:term} {eqx : x => x}
                identity x eqx -> identity (M1 x) (I1 x eqx))
          <- identity M2 I2.

eq2_lm1   : eq2 (lm1 R1) (lm ([x:term] [eqx : x => x] S1 x))
          <- {x:term} eq2 (R1 x) (S1 x).

eq2_apl1  : eq2 (apl1 R1) (ap S1 I2)
          <- eq2 R1 S1
          <- identity M2 I2.

eq2_apr1  : eq2 (apr1 R2) (ap I1 S2)
          <- eq2 R2 S2
          <- identity M1 I1.

% If M -->* N then M =>* N.

eq3 : M -->* N  ->  M =>* N  ->  type.
%mode eq3 +R* -S*.

eq3_id : eq3 id1 id.
eq3_step : eq3 (step1 R1 R2*) (S1 ; S2*)
         <- eq2 R1 S1
         <- eq3 R2* S2*.

% If M =>* N then M -->* N.

eq4 : M =>* N  ->  M -->* N  ->  type.
%mode eq4 +R* -S*.

eq4_id : eq4 id id1.
eq4_step : eq4 (R1 ; R2*) S*
         <- eq1 R1 S1*
         <- eq4 R2* S2*
         <- appd S1* S2* S*.

% If M <=> N then M <-> N.

eq5 : M <=> N  ->  M <-> N  ->  type.
%mode eq5 +C -C'.

eq5_red   : eq5 (reduce R*) (red S*)
          <- eq4 R* S*.
eq5_exp   : eq5 (expand R*) (sym (red S*))
          <- eq4 R* S*.
eq5_trans : eq5 (C1 ;; C2) (trans C1' C2')
          <- eq5 C1 C1'
          <- eq5 C2 C2'.

% If M <=> N then N <=> M.

sym_pconv : M <=> N  ->  N <=> M  ->  type.
%mode sym_pconv +C -C'.

spc_red   : sym_pconv (reduce R*) (expand R*).
spc_exp   : sym_pconv (expand R*) (reduce R*).
spc_trans : sym_pconv (C1 ;; C2) (C2' ;; C1')
          <- sym_pconv C1 C1'
          <- sym_pconv C2 C2'.

% The following is a bug not detected by term reconstruction
% spc_wrong : sym_pconv (C1 ;; C2) (C1' ;; C2')
%         <- sym_pconv C1 C1'
%         <- sym_pconv C2 C2'.

% If M <-> N then M <=> N.

eq6 : M <-> N  ->  M <=> N  ->  type.
%mode eq6 +C -C'.

eq6_refl  : eq6 refl (reduce id).
eq6_sym   : eq6 (sym C1) C'
          <- eq6 C1 C1'
          <- sym_pconv C1' C'.
eq6_trans : eq6 (trans C1 C2) (C1' ;; C2')
          <- eq6 C1 C1'
          <- eq6 C2 C2'.
eq6_red   : eq6 (red R*) (reduce S*)
          <- eq3 R* S*.