% Mechanization of POPLMARK Reloaded challenge:
% Sec 2.4: Challenge 1b: Soundness of inductive definition of strongly normalizing terms
%                        Extended with Disjoint Sums

% If SNe [g |- R] then Neutral [g |- R].
rec neutralSNe : (g: cxt) {R: [g |- tm A[]]} SNe [g |- R] -> Neutral [g |- R] =
    / total sne (neutralSNe g a r sne) /
    mlam R => fn sne =>
    case sne of
    | SVar [g |- #p] => Nvar [g |- #p]
    | SApp sne' sn => let neu = neutralSNe [_ |- _] sne' in Napp [_ |- _] [_ |- _] neu
    | SCase sne' sn1 sn2 => let neu = neutralSNe [_ |- _] sne' in
			    let sn1 : SN [g, x: tm A[] |- N1] = sn1 in
			    let sn2 : SN [g, x: tm B[] |- N2] = sn2 in
			    Ncase [_ |- _] [_ |- N1] [_ |- N2] neu
;


rec soundSN : (g: cxt) {M: [g |- tm A[]]} SN [g |- M] -> Sn [g |- M] =
    / total s (soundSN g a m s) /
    mlam M => fn sn =>
    case sn of
    | SNeu sne => soundSNe [_ |- M] sne
    | SAbs sn' => let sn'' = soundSN [_ |- _] sn' in abs_sn  [_] [ |- _] [|- _]  [_ |- _] sn''
    | SRed snr sn' => let snr' = soundSNRed [_ |- _] [_ |- _] snr in
		      let sn'' = soundSN [_ |- _] sn' in
		      backwards_closure [_ |- M] [_ |- _] snr' sn''
    | SInl sn' => let sn'' = soundSN [_ |- _] sn' in inl_sn [_ |- _] [|- _] sn''
    | SInr sn' => let sn'' = soundSN [_ |- _] sn' in inr_sn [_ |- _] [|- _] sn''

and soundSNe : (g: cxt) {M: [g |- tm A[]]} SNe [g |- M] -> Sn [g |- M] =
    / total s (soundSNe g a m s) /
    mlam M => fn sne =>
    case sne of
    | SVar [g |- #p] => varSn [g |- #p]
    | SApp sne' sn => let snl = soundSNe [_ |- _] sne' in
		      let snr = soundSN [_ |- _] sn in
		      let neu = neutralSNe [_ |- _] sne' in
		      app_sn [_] [ |- _] [|- _] [_ |- _] [_ |- _] neu snl snr
    | SCase sne' snl snr => let neu = neutralSNe [_ |- _] sne' in
			    let sn0 = soundSNe [_ |- _] sne' in
			    let sn1 = soundSN [_ |- _] snl in
			    let sn2 = soundSN [_ |- _] snr in
			    match_sn [_ |- _] [_ |- _] [_ |- _] neu sn0 sn1 sn2

and soundSNRed : (g: cxt) {M: [g |- tm A[]]} {M': [g |- tm A[]]}
			  SNRed [g |- M] [g |- M'] -> SnRed [g |- M] [g |- M'] =
     / total s (soundSNRed g a m m' s) /
    mlam M => mlam M' => fn snr =>
    case snr of
    | SBeta ([g, x: tm A[] |- M]) sn => let sn' = soundSN [_ |- _] sn in SnBeta [_ |- M] sn'
    | SAppl snr' => let snr'' = soundSNRed [_ |- _] [_ |- _] snr' in SnAppl snr''
    | SCInl sn0 sn1 sn2 => let sn0' = soundSN [_ |- _] sn0 in
			   let sn1' = soundSN [_ |- _] sn1 in
			   let sn2' = soundSN [_ |- _] sn2 in
			   SnCInl sn0' sn1' sn2'
    | SCInr sn0 sn1 sn2 => let sn0' = soundSN [_ |- _] sn0 in
			   let sn1' = soundSN [_ |- _] sn1 in
			   let sn2' = soundSN [_ |- _] sn2 in
			   SnCInr sn0' sn1' sn2'
    | SRCase snr' [g, x: tm A[] |- N1] [g, y: tm B[] |- N2] => let snr'' = soundSNRed [_ |- _] [_ |- _] snr' in
							       SnCasR snr'' [_ |- N1] [_ |- N2]
;

