%!TEX root = ../Main.tex
\section{Mechanization}
\label{s:Mechanization}

In this section we discuss the engineering details of the proof, including the concrete representation in Coq. We also discuss the technical lemmas needed to reason about substitution, effect masking and lifting an lowering of de Bruijn indices. The de Bruijn lifting and substitution operators themselves are well understood and for details of these we refer the reader to \CITE. We focus on the lowering and masking operators which are not found in prior work. \TODO{Cite POPLMark F-sub paper}

% -----------------------------------------------------------------------------
\subsection{Concrete Representation}
The following data types are the concrete representation we use in the Coq script. On the right we have written the pretty syntax as per \S\ref{s:Grammar}. Note that in the followin definitions, the @Type@ constructor refers to the meta-level Coq data type, and not to the notion of type in the object language, \SystemFre. We omit the definition of the value and expression languages as the representation and operators we use on these are largely standard.

\medskip
% -- Kinds --------------------------------------------------------------------
\noindent
\textbf{Kinds}
\begin{tabbing}
M \= MMMMMMMMMMMMMMMMMMMMMM \= MMMMMMMMMM \= MMMMM \kill
\> @Inductive ki : Type :=@        \> $\mkind$                                     \\
\> @ | KData   : ki@               \> $~::=  \kcData$                              \\
\> @ | KRegion : ki@               \> $~~~|~~~ \kcRegion$                          \\
\> @ | KEffect : ki@               \> $~~~|~~~ \kcEffect$                          \\
\> @ | KFun    : ki -> ki -> ki.@  \> $~~~|~~~ \mkind \kto \mkind$                 \\
\end{tabbing}

% -- Types --------------------------------------------------------------------
\noindent
\textbf{Types}
\begin{tabbing}
M \= MMMMMMMMMMMMMMMMMMMMMM \= MMMMMMMMMM \= MMMMM \kill
\> @Inductive ty : Type :=@        \> $\mtype$                                     \\
\> @ | TVar    : nat -> ty@        \> $~::= ix\bra{x}$                             \\           
\> @ | TForall : ki  -> ty -> ty@  \> $~~~|~~~ \forall\bra{a} : \mkind.~ \mtype$   \\
\> @ | TApp    : ty  -> ty -> ty@  \> $~~~|~~~ \mtype~ \mtype$                     \\
\> @ | TSum    : ty  -> ty -> ty@  \> $~~~|~~~ \mtype~ \vee~ \mtype$               \\
\> @ | TBot    : ki  -> ty@        \> $~~~|~~~ \bot_{\mkind}$                      \\
\> @ | TCon0   : tycon0 -> ty@     \> $~~~|~~~ \mtycon_0$                          \\
\> @ | TCon1   : tycon1 -> ty@     \> $~~~|~~~ \mtycon_1$                          \\
\> @ | TCon2   : tycon2 -> ty@     \> $~~~|~~~ \mtycon_2$                          \\
\> @ | TRgn    : nat    -> ty@     \> $~~~|~~~ \trgn{n}$
\end{tabbing}


% -----------------------------------------------------------------------------
\subsection{Flattening and Bunching}

As mentioned in \REF, it is a key design decision to represent effect sums directly in the type language (@ty@). During the development of this work we attempted to factor out effects into their own Coq data type. However, doing this means the boilerplate lemmas for lifting, substitution, lowering and the other type-level operators need to be restated and re-proved, which is a significant adminstrative burden. We also attempted to factor the representation of types to include a Coq @list@ of effects instead of separate @TSum@ and @TBot@ constructors, but found the latter easier. With the current (@ty@) repesentation, many lemmas on types can be proved by automatically by induction over the structure of the type language, whereas if we add a separate node containing a @list@ of types, then we need to perform sub-proofs via induction over the structure of this list.

Nevertheless, when proving lemmas involving effect masking we often want to reason about a @list@ of effect. We use the following functions to convert between the \emph{bunched} @ty@ representation with its @TSum@ and @TBot@ constructors, and a \emph{flat} list of effects.

\begin{small}
\begin{code}
  Fixpoint flattenT (tt : ty) : list ty
   := match tt with
      | TSum t1 t2 => flattenT t1 ++ flattenT t2
      | TBot       => nil
      | _          => tt :: nil
      end.
\end{code}
\end{small}

\begin{small}
\begin{code}
  Fixpoint bunchT (tt : list ty) : ty
   := match tt with
      | nil        => TBot
      | t :: ts    => TSum t (bunchT k ts)
      end.
\end{code}
\end{small}

\begin{lemma}[BunchT-FlattenT] If we flatten an effect type and then bunch it, the resulting type is equivalent to the original.
\end{lemma}

$
\begin{array}{lll}
        \pIf    & \KindT {ke}{sp}{t}{\kcEffect}                         \\
        \pthen  & \EquivT{ke}{sp}{\trm{bunchT}~ (\trm{flattenT}~ t)}{t}{\kcEffect}
\end{array}
$
\qqed


\clearpage{}
% -----------------------------------------------------------------------------
\subsection{Lifting, Lowering and Substitution}

\begin{small}
\begin{code}
Fixpoint liftTT (n: nat) (d: nat) (tt: ty) : ty 
 := match tt with
    |  TVar ix     => match nat_compare ix d with
                      | Lt => tt    
                      | _  => TVar (ix + n) end
    |  TForall k t => TForall k (liftTT n (S d) t)
    |  TApp t1 t2  => TApp      (liftTT n d t1) (liftTT n d t2)
    ... end.
\end{code}

\begin{small}
\begin{code}
Fixpoint lowerTT (d: nat) (tt: ty) : option ty 
 := match tt with
    |  TVar ix     => match nat_compare ix d with
                      | Eq                 => None
                      | Gt                 => Some (TVar (ix - 1))
                      | _                  => Some (TVar  ix)     end
    |  TForall k t => match lowerTT (S d) t with
                      | Some t2            => Some (TForall k t2)
                      | _                  => None                end
    |  TApp t1 t2  => match lowerTT d t1, lowerTT d t2 with
                      | Some t1', Some t2' => Some (TApp t1' t2')
                      | _, _               => None                end
    ... end.
\end{code}
\end{small}

\begin{code}
Fixpoint substTT (d: nat) (u: ty) (tt: ty) : ty 
 := match tt with
    | TVar ix      => match nat_compare ix d with
                      | Eq => u
                      | Gt => TVar (ix - 1)
                      | _  => TVar  ix     end
    |  TForall k t => TForall k (substTT (S d) (liftTT 1 0 u) t)
    |  TApp t1 t2  => TApp      (substTT d u t1) (substTT d u t2)
    ... end.
\end{code}
\end{small}


\clearpage{}
% -----------------------------------------------------------------------------
\subsection{Effect Masking}

\begin{small}
\begin{code}
Fixpoint maskOnT (p : ty -> bool) (e : ty) : ty
 := match e with
    |  TSum  t1 t2 => TSum (maskOnT p t1) (maskOnT p t2)
    |  TCon1 tc t1 => if p e then TBot else e
    | _            => e
    end.

Definition maskOnVarT n e := maskOnT (isEffectOnVar n) e.
Definition maskOnRgnT n e := maskOnT (isEffectOnRgn n) e.
\end{code}
\end{small}


% -----------------------------------------------
\begin{lemma}Equivalence and Subsumption of masked effects.
\end{lemma}
$
\begin{array}{llll}
    \pIf    & \EquivT{\mke}{\msp}
                {t_1~~~~~~~~~~~~~~~~~~~~}
                {t_2~~~~~~~~~~~~~~~~~~~~}
                {\kcEffect}

\\  \pthen  & \EquivT{\mke}{\msp}
                {\trm{maskOnT}~ p~ t_1}
                {\trm{maskOnT}~ p~ t_2}
                {\kcEffect}
\end{array}
$

\medskip
$
\begin{array}{llll}
    \pIf    & \SubsT{\mke}{\msp}
                {t_1~~~~~~~~~~~~~~~~~~~~}
                {t_2~~~~~~~~~~~~~~~~~~~~}
                {\kcEffect}

\\  \pthen  & \SubsT{\mke}{\msp}
                {\trm{maskOnT}~ p~ t_1}
                {\trm{maskOnT}~ p~ t_2}
                {\kcEffect}
\end{array}
$

\medskip
$
\begin{array}{llll}
    \pIf    & \SubsT{\mke}{\msp}
                {e_1}
                {e_2~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~}
                {\kcEffect}

\\  \pthen  & \SubsT{\mke}{\msp}
                {e_1}
                {(\trm{maskOnT}~ p~ e_2)~~~~~~~~~~~~~~~~}
                {\kcEffect}
\end{array}
$
\qqed

% -----------------------------------------------
\begin{lemma}Commutativity of masking with lifting.
\end{lemma}
$
\begin{array}{llll}
        \trm{maskOnVarT}~ r~ (\trm{liftTT}~ 1~ (1 + (r + d))~ e)        \\
        = \trm{liftTT}~ 1~ (1 + (r + d))~ (\trm{maskOnVarT}~ r~ e)
\end{array}     
$
\qqed

\begin{lemma}Commutativity of masking with substitution.
\end{lemma}
$
\begin{array}{llll}
    \pIf   & \neg(\trm{freeTT}~ d~ t_2)\\
    \pthen & \trm{maskOnVarT}~ d~ (\trm{substTT}~ (1 + d' + d)~ t_2~ t_1)   \\
           & = \trm{substTT}~ (1 + d' + d)
                        ~(\trm{maskOnVarT}~ d~ t_2)
                        ~(\trm{maskOnVarT}~ d~ t_1)
\end{array}
$
\qqed



% -----------------------------------------------------------------------------
\clearpage{}
\textbf{TODO:}
\begin{itemize}
\item   Effect join and bottom.
\item   Defining lifting, lowering, substitution and masking in a later section.
\item   Put technical properties of substitution, masking and lifting in a later section.
        Things like @lowerTT_substTT_liftTT@ and @maskOnVar_substTT@. Useful to state lemmas.
\item   Define allocRegion and deallocRegion, and give lemmas.
\end{itemize}
