%{This is the solution to [[POPL_Tutorial/MinML_Preservation_Theorem|this exercise]].

Type safety for MinML

|hidden = true}%

%% Syntax %%

tp : type.				%name tp T.
nat : tp.
arr : tp -> tp -> tp.

%% Expressions %%

exp : type.				%name exp E.
fn : tp -> (exp -> exp) -> exp.
app : exp -> exp -> exp.
z : exp.
s : exp -> exp.
ifz : exp -> exp -> (exp -> exp) -> exp.

%% Static semantics %%

of : exp -> tp -> type.			%name of Dof.
%mode of +E -T.

of/z : of z nat.
of/fn : of (fn T1 ([x] E x)) (arr T1 T2)
	 <- ({x:exp} of x T1 -> of (E x) T2).
of/app : of (app E1 E2) T
      <- of E1 (arr T2 T)
      <- of E2 T2.
of/s : of (s E) nat 
	<- of E nat.
of/ifz : of (ifz E E1 ([x] E2 x)) T
	  <- of E nat
	  <- of E1 T
	  <- ({x:exp} of x nat -> of (E2 x) T).

%% Dynamic semantics %%

value : exp -> type.			%name value Dval.
%mode value +E.

value/z : value z.
value/s : value (s E) 
	   <- value E.
value/fn : value (fn _ _).

step : exp -> exp -> type.		%name step Dstep.
%mode step +E1 -E2.

step/app/fn : step (app E1 E2) (app E1' E2)
	       <- step E1 E1'.
step/app/arg : step (app E1 E2) (app E1 E2')
		<- value E1 <- step E2 E2'.
step/app/beta : step (app (fn _ ([x] E x)) E2) (E E2)
		 <- value E2.
step/s : step (s E) (s E') 
	  <- step E E'.
step/ifz/arg : step (ifz E E1 ([x] E2 x)) (ifz E' E1 ([x] E2 x))
		<- step E E'.
step/ifz/z : step (ifz z E1 ([x] E2 x)) E1.
step/ifz/s : step (ifz (s E) E1 ([x] E2 x)) (E2 E)
	      <- value E.

%{ 

== Preservation ==

}%

pres : step E E' -> of E T -> of E' T -> type. %name pres Dpres.
%mode pres +Dstep +Dof -Dof.

- : pres
     (step/s Dstep)
     (of/s Dof)
     (of/s Dof')
     <- pres Dstep Dof Dof'.

- : pres
     (step/ifz/arg Dstep)
     (of/ifz ([x] [dx] Dof2 x dx) Dof1 Dof)
     (of/ifz ([x] [dx] Dof2 x dx) Dof1 Dof')
     <- pres Dstep Dof Dof'.

- : pres
     step/ifz/z
     (of/ifz _ Dof1 _)
     Dof1.

- : pres
     (step/ifz/s (_ : value E))
     (of/ifz ([x] [dx] Dof2 x dx) _ (of/s Dof))
     (Dof2 E Dof).

- : pres
     (step/app/fn Dstep1)
     (of/app Dof2 Dof1)
     (of/app Dof2 Dof1')
     <- pres Dstep1 Dof1 Dof1'.

- : pres
     (step/app/arg Dstep2 _)
     (of/app Dof2 Dof1)
     (of/app Dof2' Dof1)
     <- pres Dstep2 Dof2 Dof2'.

- : pres
     (step/app/beta _)
     (of/app
	Dof2
	(of/fn [x] [dx] (Dof1 x dx)))
     (Dof1 _ Dof2).

%worlds () (pres Dstep Dof Dof').
%total Dstep (pres Dstep _ _).