

% -----------------------------------------------------------------------------
\begin{lemma}[Forms of Terms and Types]
	
When a term is in normal form we can determine its shape by inspecting its type. Similarly, when a type is in normal form we can determine its shape by inspecting its kind.

For example:

\statement{
	If	&~ $t \in Value$ \\
	 \ and	&~ $\tyJudge{\emptyset}{\Sigma}{t}{\tau_1 \to \tau_2}{\sigma}$ \\
	then	&~ $t = \teLam{x}{\tau_1}{t'}$
}
\end{lemma}

\begin{proof}
By inspection of the typing rules. The only values that can have function types are lambda abstractions and variables, but as the type environment is empty the value cannot be a variable. Note that locations cannot have function types because abstractions in the store always appear inside data constructors.
\end{proof}

% -----------------------------------------------------------------------------
\begin{lemma}[No free witness variables in effects]

\medskip
\statement{
	If 	&~ $\tyJudge{\Gamma}{\Sigma}{t}{\varphi}{\sigma}$ \\
	\ and	&~ $\kiJudge{\Gamma}{\Sigma}{w}{\kappa}$ and $\ksJudgeGS{\kappa}{\Diamond}$ \\[1ex]
	then	&~ $\sigma[\delta/w] \equiv \sigma$
}
\end{lemma}


% -----------------------------------------------------------------------------
\begin{lemma}[No free witness variables in term types]

\medskip
\statement{
	If 	&~ $\tyJudge{\Gamma}{\Sigma}{t}{\varphi}{\sigma}$ \\
	\ and	&~ $\kiJudge{\Gamma}{\Sigma}{w}{\kappa}$ and $\ksJudgeGS{\kappa}{\Diamond}$ \\[1ex]
	then	&~ $\varphi[\delta/w] \equiv \varphi$
}
\end{lemma}


% -----------------------------------------------------------------------------
\begin{lemma}[Weaken Store Typing]

If we can assign a term $t$ some type and effect, then we can also assign $t$ the same type
and effect under a larger store typing. This property is also true for kind judgements.

\medskip
\statement{
	If 	&~ $\tyJudge{\Gamma}{\Sigma}{t}{\tau}{\sigma}$ 	\\
	\ and	&~ $\Sigma' \supseteq \Sigma$			\\
	then	&~ $\tyJudge{\Gamma}{\Sigma'}{t}{\tau}{\sigma}$
}

\begin{proof}
By induction over the derivation of \ $\tyJudge{\Gamma}{\Sigma}{t}{\tau}{\sigma}$. At the top of the
derivation tree we will have uses of (TyLoc) that include statements such as 
$\tyJudge{\Gamma}{\Sigma,~ l :  \tau}{l}{\tau}{\bot}$. 
These statements remain true when $\Sigma$ is extended.
\end{proof}

\end{lemma}


% -----------------------------------------------------------------------------
\begin{lemma}[Strengthen Type Environment]

\medskip
\statement{
	If	&~ $\kiJudge{\Gamma, \ x : \tau}{\Sigma}{\varphi}{\kappa}$ \\
	then	&~ $\kiJudge{\Gamma}{\Sigma}{\varphi}{\kappa}$
}
\end{lemma}


% -----------------------------------------------------------------------------
\begin{lemma}[Weaken Type Environment]

\medskip
\begin{tabular}{lllll}
	If	&~ $\tyJudgeGS{t}{\tau_1}{\sigma}$ 	&\qq \qq & If	&~ $\kiJudgeGS{\varphi}{\kappa}$ \\
	 \ and	&~ $x \notin fv(t)$ 			&    & \ and	&~ $a \notin fv(\varphi)$ \\
	then	&~ $\tyJudge	
			{\Gamma,~ x : \tau_2}
			{\Sigma}
			{t}
			{\tau_1}
			{\sigma}$
& &	then	&~ $\kiJudge
			{\Gamma,~ a : \varphi_2}
			{\Sigma}
			{\varphi}
			{\kappa}$
\end{tabular}

%\statement{
%	If	&~ $\kiJudgeGS{\varphi}{\kappa}$ \\
%	 \ and	&~ $a \notin fv(\varphi)$ \\
%	then	&~ $\kiJudge
%			{\Gamma,~ a : \varphi_2}
%			{\Sigma}
%			{\varphi}
%			{\kappa}$
%}
\end{lemma}

\medskip
% -----------------------------------------------------------------------------
\begin{theorem}[Progress of Purity]

\medskip
\statement{
	If 	&~ $\kiJudge{\emptyset}{\Sigma}{\delta}{\iPure \ \sigma}$ \\
	 \ and 	&~ $\trm{nofab}(\delta)$ \\
	then 	&~ $\delta = \un{\rpure \ \sigma}$ \\
 	 \ or	&~ $H ;  \delta \leadsto \delta'$ for all $H$ and some $\delta'$.
}
\end{theorem}

\begin{proof}
By induction over the derivation of \ $\kiJudge{\emptyset}{\Sigma}{\delta}{\iPure \ \sigma}$

\tabbedstmts{
	(IH)	\> Progress of Purity holds for all subterms of $\delta$.	
		\> (assume)
}


\tabbedstmts{
	(\un{1})	\> $\kiJudge{\emptyset}{\Gamma}{\delta}{\iPure \ \sigma}$
			\> (assume)
\\
	(\un{2}) 
			\> $\trm{nofab}(\delta)$
			\> (assume)
\\
	(3) 		\> $\delta \in 
				\{ \un{\rpure~ \sigma},\ \iMkPureBot
			 	, \ \iMkPurify \ \un{\rho} \ \delta_1,$ 
\\
			\> $\qq \iMkPureJoin \ \sigma_2 \ \sigma_3 \ \delta_2 \ \delta_3 \}$
			\> (Forms of Types 1)
\\[1ex]
	$\pCase  \ \ \delta = \un{\rpure~ \sigma}$
\\
(4)			\> immediate

\\[1ex]
	$\pCase  \ \ \delta = \iMkPureBot$
\\
	(5) 		\> $H \ ; \ \iMkPureBot \leadsto \un{\rpure \ \bot}$
			\> (EwPureBot)
\\[1ex]
	$\pCase  \ \ \delta = \iMkPurify \ \un{\rho} \ \delta_1$
\\
	(6)	 	\> $\delta_1 = \un{\rconst \ \rho}$
			\> (Kind of $\iMkPurify$ \ 2)
\\
	(7) 		\> $H \ ; \ \iMkPurify \ \un{\rho} \ \un{\rconst \ \rho} \leadsto \un{\rpure \ (\iRead \ \rho)}$
			\> (EwPurify 6)
\\[1ex]
	$\pCase  \ \ \delta = \iMkPureJoin \ \sigma_2 \ \sigma_3 \ \delta_2 \ \delta_3$
\\
	(8)	 	\> $\kiJudge{\emptyset}{\Sigma}{\delta_2}{\iPure \ \sigma_2}$
			\> (Kind of $\iMkPureJoin$ 1)
\\
	(9) 		\> $\trm{nofab}(\delta_2)$
			\> (Def. nofab 2)
\\
	(10)		\> $\delta_2 = \un{\rpure \ \sigma_2} \ \ \trm{or} \ \
		   		H ; \delta_2 \leadsto \delta_2'$
			\> (IH 8 9)
\\
	(11)		\> $\delta_3 = \un{\rpure \ \sigma_3} \ \ \trm{or} \ \
		   		H ; \delta_3 \leadsto \delta_3'$
			\> (Similarly)
\\[1ex]	
	(12)		\> Either (EwContext) or (EwPureJoin) applies.
}
\end{proof}


\clearpage{}
% -----------------------------------------------------------------------------
\begin{lemma}[Preservation of Purity]

\statement{
	If	&~ $\kiJudgeGS{\delta}{Pure~ \sigma}$ \\
	~ and	&~ $\wcJudge{H}{\delta}{\delta'}$ \\
	then	&~ $\kiJudgeGS{\delta'}{Pure~ \sigma}$
}
\end{lemma}

\begin{proof}
By induction over the derivation of $\kiJudgeGS{\delta}{Pure~ \sigma}$

\medskip
\tabbedstmts{
	(IH)	\> Preservation of Purity holds for all subterms of $\delta$.	
		\> (assume)
}


\medskip
% -------------------------------------
\pCase{$\delta = MkPureBot$ / EwPureBot}
\tabbedstmts{
	(\un{1})	\> $\kiJudgeGS{MkPureBot}{Pure~ \bot}$
			\> (assume)
\\
	(\un{2})	\> $\wcJudge{H}{MkPureBot}{\un{\rpure~ \bot}}$
	 		\> (assume)
\\
	(3)		\> $\kiJudgeGS
				{\un{\rpure~ \bot}}
				{Pure~ \bot}$
			\> (KiPure)
}


\medskip
% -------------------------------------
\pCase{$\delta = MkPurify~ \un{\rho}~ \un{\rconst~ \rho}$ / EwPurify}
$$
	\infer
	{ (\un{1})~
	  \kiJudgeGS
		{MkPurify~ \un{\rho}~ \un{\rconst~ \rho}}
		{Pure~ (Read~ \un{\rho})}
	}
	{ \infer{(3)~
	  \kiJudgeGS
		{(MkPurify~ \un{\rho})}
		{Const~ \un{\rho} \to Pure~ (Read~ \un{\rho})}}
		{\vdots}
	  \quad
	  (4)~
	  \kiJudgeGS
		{\un{\rconst~ \rho}}
		{Const~ \un{\rho}}
	}
$$
$$
	(\un{2})\
	\wcJudge{H}
		{MkPurify~ \un{\rho}~ \un{\rconst~ \rho}}
		{\un{pure~ (Read~ \rho)}}
$$

\tabbedstmts{
	(5)		\> $\un{\rconst~ \rho} \in \Sigma$
			\> (KiConst 4)
\\
	(6)		\> $\kiJudgeGS
				{\un{\rpure~ (Read~ \rho)}}
				{Pure~ (Read~ \un{\rho})}$
			\> (KiPure 6)
}


\medskip
% -------------------------------------
The remaining cases are similar to the EwPurify case.
\end{proof}




