%%% Soundness of uniform proofs
%%% Shows correspondence to canonical deductions
%%% Author: Frank Pfenning

% Uniform proofs yield canonical deductions

ss_can : s_sound (S : solve A) D -> can A D -> type.
hs_atm : h_sound H D -> atm D -> type.
is_atm : i_sound I D -> ({u:pf A} atm u -> atm (D u)) -> type.

ssc_and  : ss_can (ss_and SS2 SS1) (can_andi CN2 CN1)
	    <- ss_can SS1 CN1
	    <- ss_can SS2 CN2.

%{
ssc_imp  : ss_can (ss_imp SS1) (can_impi CN1)
	    <- {d:assume A} {u:pf A} {hs:h_sound d u} {at:atm u}
	       hs_atm hs at -> ss_can (SS1 d u hs) (CN1 u at).
}%

ssc_true : ss_can (ss_true) (can_truei).

%{
ssc_forall : ss_can (ss_forall SS1) (can_foralli CN1)
	      <- {a:i} ss_can (SS1 a) (CN1 a).
}%

ssc_atom : ss_can (ss_atom IS2 HS1) (can_atm (AT2 _ AT1))
	    <- hs_atm HS1 AT1
	    <- is_atm IS2 AT2.

isc_andl : is_atm (is_andl IS1)
	    ([u:pf (A and B)] [at:atm u] AT1 (andel u) (atm_andel at))
	    <- is_atm IS1 AT1.

isc_andr : is_atm (is_andr IS1)
	    ([u:pf (A and B)] [at:atm u] AT1 (ander u) (atm_ander at))
	    <- is_atm IS1 AT1.

isc_imp  : is_atm (is_imp SS2 IS1)
	    ([u:pf (A imp B)] [at:atm u] AT1 (impe u _) (atm_impe CN2 at))
	    <- is_atm IS1 AT1
	    <- ss_can SS2 CN2.

isc_forall : is_atm (is_forall IS1)
	      ([u:pf (forall A)] [at:atm u] AT1 (foralle u _) (atm_foralle at))
	      <- is_atm IS1 AT1.

isc_atom : is_atm (is_atom) ([u:pf (atom P)] [at:atm u] at).