Start with cctv and soundness proof

TIforWildFJ.tex

@@ -38,6 +38,8 @@
 \usepackage{arydshln}
 \usepackage{dashbox}
 
+\usepackage{mathpartir}
+
 \input{prolog}
 
 \begin{document}

soundness.tex

@@ -718,3 +718,40 @@ Same as Subst
 % \caption{T-Call and T-Field} \label{fig:tletexpr}
 % \end{figure}
 
+
+\begin{lemma}{\unify{} Soundness:}\label{lemma:unifySoundness}
+\unify{}'s type solutions are correct respective to the subtyping rules defined in figure \ref{fig:subtyping}.
+\begin{description}
+\item[If] $(\sigma, \Delta) = \unify{}( \Delta', \, \overline{ \type{S} \lessdot \type{T} } )$ %\cup \overline{ \type{S} \doteq \type{S'} })$
+\item[Then] there exists a $\sigma'$ with: 
+
+\begin{itemize}
+\item $\sigma''(\overline{\cctv{x}}) = \overline{\wctype{\Delta''}{C}{\ol{T}}}$
+\item $\sigma' = \set{ \overline{\cctv{x}} \mapsto \overline{\exptype{C}{\ol{T}}} } \cup \sigma$
+\item $\Delta, \Delta', \overline{\Delta''} \vdash \overline{\sigma'(\type{S}) <: \sigma'(\type{T})}$
+\end{itemize}
+\end{description}
+\end{lemma}
+
+\textit{Proof:}
+For every step in the \unify{} algorithm:
+Assuming the unifier $\sigma$ is correct for a constraint set $C'$, the unifier is also correct for the
+constraint set $C$ before the transformation.
+
+\unify{} terminates with $C = \emptyset$ for which the preposition holds:
+$\Delta \vdash \sigma(\emptyset)$
+
+We now show that for every transformation of a constraint set $C$ to a constraint set $C'$
+the preposition holds for $C$ using the assumption that it holds for $C'$ :
+$\Delta \vdash  \sigma(C') \implies \Delta \vdash \sigma(C)$
+
+\begin{description}
+\item[Reduce] Given $\wctype{\Delta}{C}{\ol{S}} \lessdot \wctype{\overline{\wildcard{X}{\type{U}}{\type{L}}}}{C}{\ol{T}}$
+we have to show S-Exists for some $\Delta''$ and $\ol{T} = \sigma(\overline{\wtv{a}})$:
+\begin{itemize}
+\item $\Delta'' \vdash \subst{\ol{T}}{\ol{X}}\ol{L} <: \ol{T}$ by assumption and $\subst{\ol{\wtv{a}}}{\ol{X}}\ol{L} \lessdot \ol{\wtv{a}}$
+\item $\Delta'' \vdash \ol{T} <: \subst{\ol{T}}{\ol{X}}\ol{U}$ by assumption and $\ol{\wtv{a}} \lessdot \subst{\ol{\wtv{a}}}{\ol{X}}\ol{L}$
+\item $\text{fv}(\ol{T}) \subseteq \text{dom}(\Delta'', \Delta')$ by setting $\Delta''$ accordingly
+
+\end{itemize}
+\end{description}

unify.tex

@@ -225,27 +225,6 @@ We define two types as equal if they are mutual subtypes of each other.
     \leavevmode
     \fbox{
     \begin{tabular}[t]{l@{~}l}
-   \rulename{Prepare} %The lessdotCC constraint only ensures that the left side looses its wildcardEnvironment.
-   %It does not ensure that the left side doesn't contain free variables. If you want to ensure that you have to give the left side a normal placeholder
-   & 
-   $
-   \begin{array}[c]{@{}ll}
-   \begin{array}[c]{l}
-       \wildcardEnv \vdash 
-       C \cup \, \set{ \wctype{\Delta}{C}{\ol{S}} \lessdot \wctype{\Delta'}{C}{\ol{T}} } \\ 
-     \hline
-     \vspace*{-0.4cm}\\
-       \wildcardEnv \vdash 
-       C \cup \, \set{ \wctype{\Delta}{C}{\ol{S}} \lessdotCC \wctype{\Delta'}{C}{\ol{T}} } \\ 
-   \end{array}
-    %\quad \ol{Y} = \textit{fresh}(\ol{X})
-    \quad \begin{array}[c]{l}
-     \text{fv}(\type{N'}) \subseteq \Delta_{in} \\
-     \text{wtv}(\type{N'}) = \emptyset
-     \end{array}
-   \end{array}
-   $
-\\\\
 \rulename{Trim}
 & 
 $
@@ -421,6 +400,42 @@ After \rulename{Subst} and \rulename{Same} the remaining constraints are $\tv{b}
 $\tv{a} \lessdot \wctype{\wildcard{A}{\type{Integer}}{\type{Integer}}}{List}{\rwildcard{A}}$
 %which is equal to $\tv{a} \lessdot \exptype{List}{\type{Integer}}$ and additionally we have $\tv{b} \doteq \type{Integer}$.
 
+\begin{figure}
+\begin{mathpar}
+\inferrule[Reduce]{
+    \wildcardEnv \vdash 
+            C \cup \, \set{ \wctype{\Delta}{C}{\ol{S}} \lessdot
+            \wctype{\overline{\wildcard{A}{\type{U}}{\type{L}}}}{C}{\ol{T}} }
+}{
+\wildcardEnv
+           \vdash C \cup \, \set{ 
+           \ol{\type{S}} \doteq [\ol{\wtv{a}}/\overline{\rwildcard{A}}]\ol{\type{T}},
+          \ol{\wtv{a}} \lessdot [\ol{\wtv{a}}/\overline{\rwildcard{A}}]\ol{U}, [\ol{\wtv{a}}/\overline{\rwildcard{A}}]\ol{L} \lessdot \ol{\wtv{a}} }
+}
+\quad \text{wtv}(\wctype{\overline{\wildcard{A}{\type{U}}{\type{L}}}}{C}{\ol{T}}) = \emptyset
+\and
+\inferrule[Reduce-Empty]{
+    \wildcardEnv \vdash 
+            C \cup \, \set{ \exptype{C}{\ol{S}} \lessdot
+            \wctype{\overline{\wildcard{A}{\type{U}}{\type{L}}}}{C}{\ol{T}} }
+}{
+\wildcardEnv
+           \vdash C \cup \, \set{ 
+           \ol{\type{S}} \doteq [\ol{\wtv{a}}/\overline{\rwildcard{A}}]\ol{\type{T}},
+          \ol{\wtv{a}} \lessdot [\ol{\wtv{a}}/\overline{\rwildcard{A}}]\ol{U}, [\ol{\wtv{a}}/\overline{\rwildcard{A}}]\ol{L} \lessdot \ol{\wtv{a}} }
+}
+\and
+\inferrule[Exclude]{
+\wildcardEnv \vdash 
+C \cup \, \set{ \wctype{\Delta}{C}{\ol{S}} \lessdot \type{T} }
+}{
+\subst{\tv{a}}{\wtv{a}}\wildcardEnv \vdash 
+[\tv{a}/\wtv{a}]C \cup \, [\tv{a}/\wtv{a}]\set{ \wctype{\Delta}{C}{\ol{S}} \lessdot \type{T} } \\  
+}\quad \Delta \neq \emptyset,
+\wtv{a} \in \text{fv}(\type{T}), \tv{a} \ \text{fresh}
+\end{mathpar}
+\end{figure}
+
 \begin{figure}
     \begin{center}
         \leavevmode
@@ -458,7 +473,7 @@ $\tv{a} \lessdot \wctype{\wildcard{A}{\type{Integer}}{\type{Integer}}}{List}{\rw
         \begin{array}[c]{@{}ll}
         \begin{array}[c]{l}
             \wildcardEnv \vdash 
-            C \cup \, \set{ \exptype{C}{\ol{S}} \lessdot
+            C \cup \, \set{ \wctype{\Delta}{C}{\ol{S}} \lessdot
             \wctype{\overline{\wildcard{A}{\type{U}}{\type{L}}}}{C}{\ol{T}} } \\ 
           \hline
           \vspace*{-0.4cm}\\