% Mechanization of POPLMARK Reloaded challenge:
% Section 2.2 Defining Strong Normalization

% Accessibility definition
inductive Sn : (g: cxt) {M: [g |- tm A[]]} ctype =
| Acc : {g:cxt}{A : [ |- ty]}{M : [g |- tm A[]]}
        ({M' : [g |- tm A[]]} {S: [g |- step M M']} Sn [g |- M'])
     -> Sn [g |- M]
;

% Multi-step strong normalization
% If Sn [g |- M] and [g |- mstep M M'] then Sn [g |- M'].
rec mstep_sn: (g: cxt) {M : [g |- tm A[]]}{M': [g |- tm A[]]}
		       [g |- mstep M M'] -> Sn [g |- M] -> Sn [g |- M'] =
    / total sn (mstep_sn g m m' ms sn) /
    mlam M => mlam M' => fn ms => fn sn =>
    case ms of
    | [g |- m-refl] =>  sn
    | [g |- m-step S MS'] => let Acc [g] [ |- A] [g |- _ ] r = sn in
			     let sn' = r [_ |- _] [_ |- S] in
  			       mstep_sn [_ |- _] [_ |- M'] [_ |- MS'] sn'
;

% Inductive definition
inductive SN : (g: cxt) {M: [g |- tm A[]]} ctype =
  | SNeu : SNe [g |- R] -> SN [g |- R]
  | SAbs : SN [g, x: tm A[] |- M] -> SN [g |- abs \x. M]
  | SRed : SNRed [g |- M] [g |- M'] -> SN [g |- M']
	   -> SN [g |- M]

and inductive SNe : (g: cxt) {M: [ g |- tm A[]]} ctype =
      | SVar : {#p: [g |- tm A[]]} SNe [g |- #p]
      | SApp : SNe [g |- R] -> SN [g |- M] -> SNe [g |- app R M]

and inductive SNRed : (g: cxt) {M: [g |- tm A[]]} {M': [g |- tm A[]]} ctype =
      | SBeta : {M: [g, x: tm A[] |- tm B[]]} SN [g |- N]
		-> SNRed [g |- app (abs \x. M) N] [g |- M[..,N]]
      | SAppl : SNRed [g |- R] [g |- R']
		-> SNRed [g |- app R M] [g |- app R' M]
;

% Head reduction
inductive SnRed : (g: cxt) {M: [g |- tm A[]]} {M': [g |- tm A[]]} ctype =
  | SnBeta : {M: [g, x: tm A[] |- tm B[]]} Sn [g |- N]
	     -> SnRed [g |- app (abs \x. M) N] [g |- M[.., N]]
  | SnAppl : SnRed [g |- M] [g |- M']
	     -> SnRed [g |- (app M N)] [g |- app M' N]
;
