% Mini ML Value Soundness + Type Preservation

LF tp     : type =
  | nat   : tp
  | arrow : tp -> tp -> tp
;
--name tp T.

LF exp    : type =
  | z     : exp
  | suc   : exp -> exp
  | match : exp -> exp -> (exp -> exp) -> exp
  | letv  : exp -> (exp -> exp) -> exp
  | lam   : tp -> (exp -> exp) -> exp
  | app   : exp -> exp -> exp
;
--name exp E.

LF value  : exp -> type =
  | v_z   : value z
  | v_s   : value E -> value (suc E)
  | v_lam : value (lam T (\x. E x))
;
--name value V.

% Evaluation
LF eval    : exp -> exp -> type =
  | ev_z   : eval z z
  | ev_s   : eval E V
             -> eval (suc E) (suc V)
  | ev_m_z : eval E1 V
             -> eval E z
             -> eval (match E E1 (\x. E2 x)) V
  | ev_m_s : eval (E2 V2) V
             -> eval E (suc V2)
             -> eval (match E E1 (\x. E2 x)) V
  | ev_l   : eval (E2 V1) V
             -> eval E1 V1
             -> eval (letv E1 (\x. E2 x)) V
  | ev_lam : eval (lam T (\x. E x)) (lam T (\x. E x))
  | ev_app : eval E1 (lam T (\x. E x))
             -> eval E2 V2
             -> eval (E V2) V
             -> eval (app E1 E2) V
;
--name eval F.

% Typing
LF oft       : exp -> tp -> type =
  | tp_z     : oft z nat
  | tp_s     : oft E nat
               -> oft (suc E) nat
  | tp_match : ({x:exp}oft x nat -> oft (E2 x) T)
               -> oft E1 T
               -> oft E nat
               -> oft (match E E1 (\x. E2 x)) T
  | tp_lam   : ({x:exp} oft x T1 -> oft (E x) T2)
               -> oft (lam T1 (\x. E x)) (arrow T1 T2)
  | tp_app   : oft E2 T2
               -> oft E1 (arrow T2 T1)
               -> oft (app E1 E2) T1
  | tp_letv  : ({x:exp} oft x T1 -> oft (E2 x) T2)
               -> oft E1 T1
               -> oft (letv E1 (\x. E2 x)) T2
;
--name oft D u.
