% Mechanization of POPLMARK Reloaded challenge:
% Section 2.6: Challenge 2b: Strong Normalization Proof using Logical Predicate
%              Extended with Disjoint Sums

inductive Eq: (g: cxt) [g |- tm A[]] -> [g |- tm A[]] -> ctype =
  Refl : Eq [g |- M] [g |- M];

% Logical predicate
stratified Red : {A : [|- ty]} (g : cxt) {M : [g |- tm A[]]} ctype =
  | RBase : SN [g |- M] -> Red [|- base] [g |- M]
  | RArr  : ({g' : cxt} {#S : [g' |-# g]} {N : [g' |- tm A[]]}
	     Red [|- A] [g' |- N] -> Red [|- B] [g' |- app M[#S] N])
            -> Red [ |- arr A B ] [g |- M]
  | RSum  : DSClosure [g |- M] -> Red [|- sum A B] [g |- M]

% Closure for disjoint sums
and inductive DSClosure : (g : cxt) {M : [ g |- tm (sum A[] B[]) ]} ctype =
  | DSLeft  : Red [|- A] [g |- N] -> Eq [g |- inl B[] N] [g |- M] -> DSClosure [g |- M]
  | DSRight : Red [|- B] [g |- N] -> Eq [g |- inr A[] N] [g |- M] -> DSClosure [g |- M]
  | DSSNe   : SNe [g |- M] -> DSClosure [g |- M]
  | DSRed   : DSClosure [g |- M] -> SNRed [g |- N] [g |- M] -> DSClosure [g |- N]
;

% Semantic substitutions
inductive RedS : {g : cxt} (g' : cxt) {#S : [g' |- g]} ctype =
  | RNil  : RedS [] [ g' |- ^ ]
  | RCons : Red [|- A] [g' |- M]
            -> RedS [g] [g' |- #S]
            -> RedS [g, x : tm A[]] [g' |- #S, M]
;

% Weakening for logical predicate and semantic substitutions
rec rename_red : {g : cxt} {g' : cxt} {A:[|- ty]} {M : [g |- tm A[]]} {#R : [g' |-# g]}
			   Red [|- A] [g |- M] -> Red [|- A] [g' |- M[#R]] =  
    / total a (rename_red g g' a) /
      mlam g, g', A, M, #R => fn r => case [ |- A ] of
    | [ |- base ] => let RBase s = r in RBase (renameSN [_ ] [_ ] [g' |- #R] [g |- M] s)
    | [ |- arr A B] => let RArr r' = r in
		       RArr (mlam g'', #S, N => fn rn =>
			     r' [g'']  [g'' |- #R[#S[..]]] [g'' |- N] rn)
    | [ |- sum A B] => let RSum d = r in RSum (rename_DS [g] [g'] [ |- _] [ |- _] [_ |- _] [g' |- #R] d)

% Inner IH for disjoint sum closure
and rename_DS: {g : cxt} {g' : cxt} {A:[ |- ty]} {B:[ |- ty]} {M : [g |- tm (sum A[] B[])]} {#R : [g' |-# g]}
			 DSClosure [g |- M] -> DSClosure [g' |- M[#R]] =
    / total d (rename_DS g g' a b m r d) /
      mlam g, g', A, B, M, #R => fn d => case d of
    | DSLeft r' Refl => DSLeft (rename_red [g] [g'] [ |- _] [_ |- _] [g' |- #R] r') Refl
    | DSRight r' Refl => DSRight (rename_red [g] [g'] [ |- _] [_ |- _] [g' |- #R] r') Refl
    | DSSNe sne => DSSNe (renameSNe [_ |- #R] [_ |- _] sne)
    | DSRed d' r' => let d'' = rename_DS [g] [g'] [ |- _] [ |- _] [_ |- _] [g' |- #R] d' in
		     DSRed d'' (renameSNRed [_ |- #R] [_ |- _] r')

and rename_redS: {g : cxt} {g' : cxt} {#R : [g' |-# g]} RedS [h] [g |- #S]   -> RedS [h] [g' |- #S[#R]] = 
    / total rs (rename_redS g g' s rs) /
      mlam g, g', #R => fn rs => case rs of
    | RNil => RNil
    | RCons r rs' => RCons (rename_red  [g] [g'] [ |- _] [_ |- _] [g' |- #R] r)
			   (rename_redS [g] [g'] [g' |- #R] rs') 
;


% Reducibility candidate conditions
rec cr1 : {g : cxt} {A :[|- ty]} {M : [g |- tm A[]]} Red [ |- A] [g |- M] -> SN [g |- M] = 
    / total a (cr1 g a ) /
      mlam g, A, M => fn r => case [ |- A ] of 
    | [ |- base] => let RBase s = r in s
    | [ |- arr A B] => let rv = cr3 [g, x:tm A[]][ |- A] [g, x:tm A[] |- x] (SVar [g, x:tm A[] |- x]) in
		       let RArr r'  = r in
		       let s = cr1 [g, x:tm A[]] [ |- B] [g, x:tm A[] |- app M[..] x]
				   (r' [g, x:tm A[]] [g, x:tm A[] |- ..] [g, x:tm A[] |- x] rv) in
		       let sm = ext_SN [g,x:tm A[] |- M[..]] [g, x:tm A[] |- x] s in
		       anti_renameSN [ _ ] [ _ ] [g, x:tm A[] |- ..] [g |- M] sm
    | [ |- sum A B] => let RSum d = r in ds_cr1 [_] [ |- _] [ |- _] [_ |- _] d

% Inner IH for disjoint sum closure
and ds_cr1 : {g : cxt} {A : [|- ty]} {B : [|- ty]} {M : [g |- tm (sum A[] B[])]} DSClosure [g |- M] -> SN [g |- M] =
    / total d (ds_cr1 g a b m d) /
      mlam g, A, B, M => fn d => case d of
    | DSLeft r' Refl => SInl (cr1 [_] [ |- _] [_ |- _] r')
    | DSRight r' Refl => SInr (cr1 [_] [ |- _] [_ |- _] r')
    | DSSNe sne => SNeu sne
    | DSRed d' r' => let sn = ds_cr1 [_] [ |- _] [ |- _] [_ |- _] d' in SRed r' sn

and cr2 :  {g : cxt} {A : [|- ty]} {M : [g |- tm A[]]} {M' : [g |- tm A[]]}
		     SNRed [g |- M] [g |- M'] -> Red [ |- A] [g |- M'] -> Red [ |- A] [g |- M] = 
    / total a (cr2 g a) /
      mlam g, A, M, M' => fn sr, rm' => case [ |- A] of
    | [ |- base ] => let RBase sm' = rm' in RBase (SRed sr sm')
    | [ |- arr A B] => let RArr rm' = rm' in
		       RArr (mlam g', #R, N => fn rn =>
			     cr2 [g'] [ |- B] [g' |- app M[#R] N] [g' |- app M'[#R] N]
				 (SAppl (renameSNRed [g' |- #R] [g |- M] sr))
				 (rm' [g'] [g' |- #R] [g' |- N] rn))
    | [ |- sum A B] => let RSum d = rm' in RSum (DSRed d sr)

and cr3 : {g :cxt} {A : [|- ty]} {M : [g |- tm A[]]} SNe [g |- M] -> Red [|- A] [g |- M] =
    / total a (cr3 g a) /
      mlam g, A, M => fn sm => case [|- A] of
    | [ |- base ] => RBase (SNeu sm)
    | [ |- arr A B] => RArr (mlam g', #R, N => fn rn =>
			     let sn  = cr1 [g'] [ |- A] [g' |- N] rn in
			     cr3 [g'] [ |- B] [g' |- app M[#R] N]
				 (SApp (renameSNe [g' |- #R] [g |- M] sm)  sn))
    | [ |- sum A B] => RSum (DSSNe sm)
;

% Variables are reducible
rec red_var : {g : cxt} {#p : [g |- tm A[]]} Red [ |- A] [g |- #p] = 
    / total (red_var ) /
      mlam g, #p => cr3 [_] [|- _] [_ |- _] (SVar [g |- #p]);

rec fundVar : {g : cxt} {#p : [g |- tm A[]]}
			RedS [g] [g' |- #S]
	      -> Red [|- A] [g' |- #p[#S]] =
    / total g (fundVar g) /
      mlam g, #p => fn s => case [g] of
    | [] => impossible [ |- #p ]
    | [g, x : tm A[]] => (case [g, x : tm _ |- #p] of
			  | [g, x : tm A[] |- x     ] => let RCons r s' = s in r
			  | [g, x : tm A[] |- #q[..]] => let RCons r s' = s in fundVar [g] [g |- #q] s')
;

rec eq_red : Eq [g |- M] [g |- N] -> Red [ |- C] [g |- match M (\x.N1) (\y.N2)]
	     -> Red [ |- C] [g |- match N (\x.N1) (\y.N2)] =
    / total (eq_red) /
      fn e => fn r => let Refl = e in r;

% Fundamental lemma
rec fundamental_lemma : {g : cxt} {g' : cxt} {M : [g |- tm A[]]} {#S : [g' |- g]} RedS [g] [g' |- #S]
			-> Red [|- A[]] [g' |- M[#S]] = 
    / total m (fundamental_lemma g g' a m) /
      mlam g, g', M, #S => fn rs => case [g |- M] of 
   | [g |- #p] => fundVar [g] [g |- #p] rs
   | [g |- app M N] => let RArr r1 = fundamental_lemma [g] [g'] [g |- M] [g' |- #S] rs in 
		       let r2 = fundamental_lemma [g] [g'] [g |- N] [g' |- #S] rs in 
		       r1 [g'] [g' |- ..] [g' |- N[#S]] r2
   | [g |- abs  \x.M] => 
     RArr (mlam g'', #R, N => fn rn => 
	   let rs' = rename_redS [g'] [g''] [g'' |- #R] rs in
	   let r   = fundamental_lemma  [g, x:tm _ ] [g''] [g, x:tm _ |- M] [g'' |- #S[#R], N] (RCons rn rs') in 
	   let sn = cr1 [_] [ |- _ ] [_ |- _ ] rn in 
	   let sn' = SBeta [g'', x:tm _ |- M[#S[#R[..]], x]] sn in 
	   cr2 [_] [ |- _ ] [_ |- _ ] [_ |- _ ] sn' r)

   | [g |- inl B[] M] => let r = fundamental_lemma [g] [g'] [g |- M] [g' |- #S] rs in RSum (DSLeft r Refl)
   | [g |- inr A[] M] => let r = fundamental_lemma [g] [g'] [g |- M] [g' |- #S] rs in RSum (DSRight r Refl)
   | [g |- match M (\x.N1) (\y.N2)] =>
     let r = fundamental_lemma [g] [g'] [g |- M] [g' |- #S] rs in
     let RSum d = r in main_ds [g] [g'] [g' |- M[#S]] [g, x: tm _ |- N1] [g, y: tm _ |- N2] [g' |- #S] rs d

% Inner IH for disjoint sum closure
and main_ds : {g : cxt} {g' : cxt}
			{M : [g' |- tm (sum A[] B[])]}
			{N1 : [g, x: tm A[] |- tm C[]]} {N2: [g, y: tm B[] |- tm C[]]}
			{#S : [g' |- g]} RedS [g] [g' |- #S]
	      -> DSClosure [g' |- M]
	      -> Red [ |- C[]] [g' |- match M (\x.N1[#S[..], x]) (\y.N2[#S[..], y])] =
    / total d (main_ds g g' m n1 n2 s rs d) /
      mlam g, g', M, N1, N2, #S => fn rs => fn d =>
    case d of
    | DSLeft r e => let sn0 = cr1 [_] [|- _] [_ |- _] r in
		    let r1 = fundamental_lemma [_, x:tm _] [_] [_, x:tm _ |- N1] [_ |- #S[..], _] (RCons r rs) in
		    let r2 = fundamental_lemma [_, y:tm _] [_, y:tm _] [_, y:tm _ |- N2] [_ |- #S[..], _]
					(RCons (red_var [g', y : tm _ ] [g', y : tm _ |- y])
					       (rename_redS [g'] [g', y : tm _ ] [g', y : tm _ |- ..] rs)) in
		    let r1' = fundamental_lemma [_, x:tm _] [_, x:tm _] [_, x:tm _ |- N1] [_ |- #S[..], _]
					 (RCons (red_var [g', x: tm _ ] [g', x: tm _ |- x])
						(rename_redS [g'] [g', x: tm _ ] [g', x: tm _ |- ..] rs)) in
		    let sn1 = cr1 [_] [|- _] [_ |- _] r1' in
		    let sn2 = cr1 [_] [|- _] [_ |- _] r2 in
		    let snr = SCInl sn0 sn1 sn2 in
		    eq_red e (cr2 [_] [|- _] [_ |- _] [_ |- _] snr r1)

    | DSRight r e => let sn0 = cr1 [_] [|- _] [_ |- _] r in
		     let r1 = fundamental_lemma [_, x:tm _] [_, x:tm _] [_, x:tm _ |- N1] [_ |- #S[..], _]
					 (RCons (red_var [g', x:tm _] [g', x:tm _ |- x])
						(rename_redS [g'] [g', x:tm _] [g', x:tm _ |- ..] rs)) in
		     let r2 = fundamental_lemma [_, y:tm _] [_] [_, y:tm _ |- N2] [_ |- #S[..], _] (RCons r rs) in
		     let r2' = fundamental_lemma [_, y:tm _] [_, y:tm _] [_, y:tm _ |- N2] [_ |- #S[..], _]
					  (RCons (red_var [g', y : tm _ ] [g', y : tm _ |- y])
						 (rename_redS [g'] [g', y : tm _ ] [g', y : tm _ |- ..] rs)) in
		     let sn1 = cr1 [_] [|- _] [_ |- _] r1 in
		     let sn2 = cr1 [_] [|- _] [_ |- _] r2' in
		     let snr = SCInr sn0 sn1 sn2 in
		     eq_red e (cr2 [_] [|- _] [_ |- _] [_ |- _] snr r2)

    | DSSNe sne => let r1 = fundamental_lemma [_, x:tm _] [_, x:tm _] [_, x:tm _ |- N1] [_ |- #S[..], _]
				       (RCons (red_var [g', x:tm _] [g', x:tm _ |- x])
					      (rename_redS [g'] [g', x:tm _] [g', x:tm _ |- ..] rs)) in
		   let r2 = fundamental_lemma [_, y:tm _] [_, y:tm _] [_, y:tm _ |- N2] [_ |- #S[..], _]
				       (RCons (red_var [g', y : tm _ ] [g', y : tm _ |- y])
					      (rename_redS [g'] [g', y : tm _ ] [g', y : tm _ |- ..] rs)) in
		   let sn1 = cr1 [_] [|- _] [_ |- _] r1 in
		   let sn2 = cr1 [_] [|- _] [_ |- _] r2 in
		   let sne' = SCase sne sn1 sn2 in
		   cr3 [_] [|- _] [_ |- _] sne'

    | DSRed d' r => let (r : SNRed [_ |- _] [g' |- M']) = r in
		    let r' = main_ds [g] [g'] [g' |- M'] [g, x:tm _ |- N1] [g, y:tm _ |- N2] [_ |- #S] rs d' in
		    let snr = SRCase r [g', x:tm _ |- N1[#S[..], x]] [g', y:tm _ |- N2[#S[..], y]] in
		    cr2 [_] [|- _] [_ |- _] [_ |- _] snr r'
;

% All well-typed terms are strongly normalizing.
rec id_red : {g : cxt} RedS [g] [g |- ..] = 
    / total g (id_red g) /
      mlam g => case [g] of 
      | [] => RNil
      | [g, x: tm A[]] => let r  = id_red [g] in 
			  let r' = rename_redS [g] [g, x : tm A[]] [g, x : tm A[] |- ..] r in
			  RCons (red_var [g, x : tm A[]] [g, x : tm A[] |- x]) r'
;

rec norm : {g : cxt} {M : [g |- tm A[]]} SN [g |- M] = 
    / total  (norm) /
      mlam g, M => cr1 [_] [ |- _ ] [ _ |- _ ] (fundamental_lemma [g] [g] [g |- M] [g |- ..] (id_red [g]));
