%%% Equivalence between soundness and completeness proofs %%% Author: Frank Pfenning peq : csd C D C' -> ccp D C' C -> type. %mode peq +SD -CP. % Natural Numbers peq_z : peq (csd_z) (ccp_z). peq_s : peq (csd_s SD1) (ccp_s CP1) <- peq SD1 CP1. peq_case_z : peq (csd_case_z SD2 SD1) (ccp_case_z CP1 CP2) <- peq SD1 CP1 <- peq SD2 CP2. peq_case_s : peq (csd_case_s SD3 SD1) (ccp_case_s CP1 CP3) <- peq SD1 CP1 <- peq SD3 CP3. % Pairs peq_pair : peq (csd_pair SD2 SD1) (ccp_pair CP1 CP2) <- peq SD1 CP1 <- peq SD2 CP2. peq_fst : peq (csd_fst SD1) (ccp_fst CP1) <- peq SD1 CP1. peq_snd : peq (csd_snd SD1) (ccp_snd CP1) <- peq SD1 CP1. % Functions peq_lam : peq (csd_lam) (ccp_lam). peq_app : peq (csd_app SD3 SD2 SD1) (ccp_app CP1 CP2 CP3) <- peq SD1 CP1 <- peq SD2 CP2 <- peq SD3 CP3. % Definitions peq_letv : peq (csd_letv SD2 SD1) (ccp_letv CP1 CP2) <- peq SD1 CP1 <- peq SD2 CP2. peq_letn : peq (csd_letn SD1) (ccp_letn CP1) <- peq SD1 CP1. % Recursion peq_fix : peq (csd_fix SD1) (ccp_fix CP1) <- peq SD1 CP1. % Values peq_vl : peq (csd_vl) (ccp_vl). %%% For complete evaluations proof_equiv : ceval_sound CE D -> ceval_complete D CE -> type. pequiv : proof_equiv (cevsd SD) (cevcp CP) <- peq SD CP.