Some Reductions for Annotated Natural Deductions

%%% Reduction of annotated minimal linear natural deductions
%%% Author: Frank Pfenning
%%%
%%% This incorporates no strategy, just gives the rules
%%% Also, this includes no commutative reductions.

rede : elim A & elim A -> type.
redi : intro A & intro A -> type.

%% Coercion

rede_coerce : rede (i2e (e2i E) , E).  % needed? --- seems eta-like.
redi_coerce : redi (e2i (i2e I) , I).

%% Multiplicative Connectives

rede_imp : rede (impe' I2 (i2e (impi' I1)) , i2e (I1 (i2e I2))).

redi_times : redi (timese' I3 (i2e (timesi' I1 I2)) , I3 (i2e I1) (i2e I2)).

redi_one : redi (onee' I1 (i2e (onei')) , I1).

rede_with1 : rede (withe1' (i2e (withi' (I1 , I2))) , i2e I1).
rede_with2 : rede (withe2' (i2e (withi' (I1 , I2))) , i2e I2).

% no rede_top 

redi_plus1 : redi (pluse' (I2 , I3) (i2e (plusi1' I1)) , I2 (i2e I1)).
redi_plus2 : redi (pluse' (I2 , I3) (i2e (plusi2' I1)) , I3 (i2e I1)).

% no redi_zero

rede_forall : rede (foralle' T (i2e (foralli' I1)) , i2e (I1 T)).

redi_exists : redi (existse' I2 (i2e (existsi' T I1)) , I2 T (i2e I1)).

redi_! : redi (!e' I2 (i2e (!i' I1)) , I2 (i2e I1)).

Frank Pfenning