%%% Reduction rules for natural deduction
%%% Author: Frank Pfenning

%%% Local Reductions

==>L : nd A -> nd A -> type.  %name ==>L L
%infix none 14 ==>L

redl_andl   : (andel (andi D E)) ==>L D.
redl_andr   : (ander (andi D E)) ==>L E.

redl_imp    : (impe (impi D) E) ==>L (D E).

redl_orl    : (ore (oril D) E1 E2) ==>L (E1 D).
redl_orr    : (ore (orir D) E1 E2) ==>L (E2 D).

redl_not    : (note (noti D) C E) ==>L (D C E).

redl_forall : (foralle (foralli D) T) ==>L (D T).

redl_exists : (existse (existsi T D) E) ==>L (E T D).

%%% Congruences

==> : nd A -> nd A -> type.		%name ==> R
%infix none 14 ==>

red_local    : D ==>L D'
		-> D ==> D'.

% Conjunction
red_andi1    : D1 ==> D1'
		-> (andi D1 D2) ==> (andi D1' D2).
red_andi2    : D2 ==> D2'
		-> (andi D1 D2) ==> (andi D1 D2').
red_andel    : D ==> D'
		-> (andel D) ==> (andel D').
red_ander    : D ==> D'
		-> (ander D) ==> (ander D').

% Implication
red_impi     : ({u:nd A} u ==> u -> (D u) ==> (D' u))
		-> (impi D) ==> (impi D').
red_impe1    : D1 ==> D1'
		-> (impe D1 D2) ==> (impe D1' D2).
red_impe2    : D2 ==> D2'
		-> (impe D1 D2) ==> (impe D1 D2').

% Disjunction
red_oril     : D ==> D'
		-> (oril D) ==> (oril D').
red_orir     : D ==> D'
		-> (orir D) ==> (orir D').
red_ore1     : D1 ==> D1'
		-> (ore D1 D2 D3) ==> (ore D1' D2 D3).
red_ore2     : ({u:nd A} u ==> u -> (D2 u) ==> (D2' u))
		-> (ore D1 D2 D3) ==> (ore D1 D2' D3).
red_ore3     : ({u:nd B} u ==> u -> (D3 u) ==> (D3' u))
		-> (ore D1 D2 D3) ==> (ore D1 D2 D3').

% Negation
red_noti     : ({p:o} {u:nd A} u ==> u -> (D p u) ==> (D' p u))
		-> (noti D) ==> (noti D').
red_note1    : D1 ==> D1'
		-> (note D1 C D2) ==> (note D1' C D2).
red_note2    : D2 ==> D2'
		-> (note D1 C D2) ==> (note D1 C D2').

% Truth
red_truei    : (truei) ==> (truei).

% Falsehood
red_falsee   : D ==> D'
		-> (falsee D) ==> (falsee D').

% Universal Quantification
red_foralli  : ({a:i} (D a) ==> (D' a))
		-> (foralli D) ==> (foralli D').
red_foralle  : D ==> D'
		-> (foralle D T) ==> (foralle D' T).

% Existential Quantification
red_existsi  : D ==> D'
		-> (existsi T D) ==> (existsi T D').
red_existse1 : D1 ==> D1'
		-> (existse D1 D2) ==> (existse D1' D2).
red_existse2 : ({a:i} {u:nd (A a)} (D2 a u) ==> (D2' a u))
		-> (existse D1 D2) ==> (existse D1 D2').