\section{Soundness}



% %This lemma can be used to proof Normalize rule!
% \begin{lemma}\label{lemma:wildcardReplacement}
%     Wildcards with the same upper and lower bound can be replaced by their bounds without breaking subtype relations.
%     \begin{description}
%         \item[If] $\Delta \cup \set{\wildcard{X}{\type{U}}{\type{L}}} \vdash \type{T} <: \type{S}$
%         \item[and] $\type{U} = \type{L}$ and $\text{fv}(\type{U}) = \emptyset$
%         \item[Then] $\Delta \vdash [\type{U}/\type{X}]\type{T} <: [\type{U}/\type{X}]\type{S}$
%         \end{description}
% \end{lemma}
% \textit{Proof:} %TODO
% %By structural induction over the subtype relation
% %S-Refl: by assumption L <: L implies [\type{U}/\type{X}]L

% \begin{lemma}\label{lemma:noAdditionalFV}
%     Type solution $\sigma$ does not add additional free variables.
%     \begin{description}
%         \item[If] $(\sigma, \Delta) = \unify{}( \overline{ \type{S} \lessdot \type{T} } \cup C)$
%         \item[and] $fv(\overline{ \type{S} }) = \emptyset$, $fv(\overline{ \type{T} }) = \emptyset$
%         \item[Then] $fv(\sigma(\overline{ \type{S} })) = \emptyset, fv(\sigma(\overline{ \type{T} })) = \emptyset$
%         \end{description}
% \end{lemma}

% \begin{lemma}
% % https://math.libretexts.org/Bookshelves/Mathematical_Logic_and_Proof/Book%3A_Mathematical_Reasoning__Writing_and_Proof_(Sundstrom)/07%3A_Equivalence_Relations/7.03%3A_Equivalence_Classes
% $\doteq$ is an equivalence relation on a constraint set $C$.

% \begin{description}
% \item[If] $\Delta \vdash \overline{\type{T} <: \type{S}}$ and $\type{T} \doteq \type{S}$
% \item[Then] $\Delta \vdash [\type{T}/\type{S}](\overline{\type{T} <: \type{S}})$
% \end{description}
% \end{lemma}

\begin{lemma}
The \unify{} algorithm only produces correct output for constraints not containing free variables.

\begin{description}
\item[If] $(\sigma, \Delta) = \unify{}( \overline{ \type{S} \lessdot \type{T} } \cup \overline{ \type{S'} \lessdot \type{T'} } )$ %\cup \overline{ \type{S} \doteq \type{S'} })$
\item[and] $fv(\overline{ \type{S} }) = \emptyset$, $fv(\overline{ \type{T} }) = \emptyset$
\item[Then] there exists a $\Delta'$ with:
$\Delta \vdash \overline{\sigma(\type{S}) <: \sigma(\type{T})}$
and $\Delta, \Delta' \vdash \overline{\text{CC}(\sigma(\type{S'})) <: \sigma(\type{T'})}$
% and $\sigma(\type{T'}) = \sigma(\type{T'})$.

The function $\text{CC}$ is given as $\text{CC}(\wcNtype{\Delta}{N}) = \type{N}$
\end{description}
\end{lemma}

\textit{Proof:}
%(we are going backwards over the algorithm)
%first we have to determine the \Delta'' -> it's only the wildcards which are free in N
% during this proof we can use Delta'' as we like

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.
\begin{description}
\item[Assumption:] $\unify{}(C) = (\Delta, \sigma)$, with $\Delta \vdash \sigma(C)$
\item[Induction step:] For every case $C'$ which can be transformed to $C$ we have to show $\Delta \vdash \sigma(C')$   
\end{description}

\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[AddDelta] $C$ is not changed
\item[GenDelta] by definition, S-Var-Left, and S-Trans %The generated type variable is unique due to the solved form property. %and the solved form property (no $\tv{a}$ in $C$)
\item[GenSigma] by definition.
% holds for $\set{\tv{a} \doteq \type{G}}$ by definition.
% Holds for $C$ by assumption and because $\tv{a} \notin C$ by solved form definition ($[\type{G}/\tv{a}]C = C$).
\item[Ground] Assumption and S-Bot
\item[Sub-Elim] Assumption and S-Refl
\item[Force] by assumption and $\rwildcard{X} = \type{U}$ %TODO: step 5 should remove all X^T_T with T (make wildcards with same upper and lower bounds to normal types)
\item[Raise] Assumption, S-Trans
\item[Settle] Assumption, S-Trans
\item[Super] S-Extends ($\vdash \wctype{\Delta}{C}{\ol{T}} <: \wctype{\Delta}{D}{[\ol{T}/\ol{X}]\ol{N}}$), S-Trans
\item[\generalizeRule{}] by Assumption, because $C \subset C'$
\item[Adapt] Assumption, S-Extends, S-Trans
\item[Adopt] Assumption, because $C \subset C'$
%\item[Capture, Reduce] are always applied together. We have to destinct between two cases:
\item[Capture]
If $\text{fv}(\wctype{\Delta}{C}{\ol{T}}) = \emptyset$ the preposition holds by Assumption and S-Exists.
If $\text{fv}(\wctype{\Delta}{C}{\ol{T}}) \neq \emptyset$ we have to show $\Delta' \vdash \text{CC}(\sigma(\wctype{\overline{\wildcard{B}{\type{U'}}{\type{L'}}}}{C}{\ol{S}})) <: \sigma(\wctype{\Delta}{C}{\ol{T}})$,
which holds by assumption with $\Delta'$ chosen in a way that $\text{fv}(\exptype{C}{\ol{S}}) \subseteq \Delta'$. The variables $\ol{C}$ in $\ol{S}$ can be renamed to $\ol{B}$, because $\ol{C}$ are fresh.
%If $\text{fv}(\wctype{\Delta}{C}{\ol{T}}) \neq \emptyset$ we have to show $\Delta \vdash \sigma(\exptype{C}{\ol{S}}) <: \sigma(\wctype{\Delta}{C}{\ol{T}})$.
%$\Delta \vdash \sigma([\ol{C}/\ol{B}]\exptype{C}{\ol{S}}) <: \sigma(\wctype{\Delta}{C}{\ol{T}})$ holds by assumption and
%the variables $\ol{B}$ in $\ol{S}$ can be renamed to $\ol{C}$, because $\ol{C} \notin \ol{S}$ ($\ol{C}$ are fresh).
%The assumption implies $\text{fv}(\ol{S}) \subseteq \text{dom}(\Delta \cup \set{\overline{\wildcard{C}{\type{U'}}{\type{L'}}}})$
%, which implies $\text{fv}(\ol{S}) \subseteq \text{dom}(\Delta \cup \set{\overline{\wildcard{B}{\type{U'}}{\type{L'}}}})$.

%We are doing a capture conversion. If $\type{T}$ does not contain free variables, this does not affect the subtype relation.
\item[Reduce] %Assumption and S-Exists.
If $\text{fv}(\exptype{C}{\ol{S}}) = \emptyset$ the preposition holds by Assumption and S-Exists.
If $\text{fv}(\exptype{C}{\ol{S}}) \neq \emptyset$ there exists a $\Delta'$ with
$\Delta' \vdash \text{CC}(\sigma(\exptype{C}{\ol{S}})) <: \sigma(\wctype{\overline{\wildcard{A}{\type{U}}{\type{L}}}}{C}{\ol{T}})$.
\item[Match] Assumption, S-Trans
\item[Trim] Assumption and S-Exists
\item[Remove] $C$ is not changed
\item[Circle] S-Refl
\item[Swap] by definition
\item[Erase] S-Refl
\item[Equals] by definition
% \item[Reduce]
% The renaming from $\rwildcard{C}$ to $\rwildcard{B}$ is not a problem. It's allowed to rename wildcards inside a type.
% Removing $\rwildcard{C}$ from the environment does not change anything because it was freshly generated and is used nowhere.

% The rest follows directly from S-Exists.
% We can say: $\text{fv}(\wctype{\overline{\wildcard{A}{\type{U}}{\type{L}}}}{C}{\ol{T}}) = \emptyset$,
% because the input to the \unify{} algorithm has no free type variables and we never substitute a type with free type variables
% and none of the other steps of the algorithm generates a $\lessdot$ constraint containing free type variables on the right side. %TODO: proof

% $\text{fv}(\ol{T}) \subseteq \text{dom}(\wildcardEnv \cup \overline{\wildcard{B}{\type{U'}}{\type{L'}}})$
% TODO: The capture conversion has to be when substituting a $\wtv{a}$ variable. Then we have to rename!
% %Lets first try it without the capture conversion. And involve the wtvs in the second step
% % The algorithm works by never substituting wildcards



% \unify{} cannot guarantee the premise $\text{dom}(\Delta, \Delta') \cap \text{fv}(\wcNtype{\overline{\wildcard{X}{\type{U}}{\type{L}}}}{N}) = \emptyset$.
% We loosen the soundness requirements and allow a arbitrary environment $\Delta''$ to be added to the right side of the subtype relation.
% This is still sufficient to proof soundness for the whole algorithm.
% We show that the need for the additional environment $\Delta''$ can be satisfied by a let statement.

% \begin{itemize}
% \item $\Delta, \Delta' \vdash [\ol{T}/\ol{X}]\ol{L} <: \ol{T}$: S-Exists 
% \item $\Delta, \Delta' \vdash \ol{T} <: [\ol{T}/\ol{X}]\ol{U}$: S-Exists
% \item $\textit{fv}(\ol{T}) \subseteq \text{dom}{\Delta, \Delta'}$: $\wildcardEnv$ holds all variables %TODO: Proof
% \end{itemize}
\item[Normalize] Assumption and lemma 5 \emph{substitution preserves subtyping}.%\ref{lemma:wildcardReplacement}. (Or Lemma 5 from the wildcard paper. \emph{substitution preserves subtyping})
% The GenSigma step replaces both sides of $\rwildcard{A} \doteq \rwildcard{B}$ with the upper bound $\type{U}$.
% This works for every constraint, whether it contains free variables or not.
% It does not add to free variables of constraints because the upper bound does not contain any.
The GenSigma and Gen Delta steps remove Wildcards which have the same upper and lower bound.
$\rwildcard{A},\rwildcard{B} \notin \sigma(C)$

% sigma(T) = sigma(U) we have to show that T = U means \Delta \vdash [T/U]C \implies \Delta \vdash [U/T]C 
% the constraints L <. U, U <. L lead to L =. U
%If L is List<X> with X being free wildcard
%then U <. L will fail if U is type variable




% this is because bounds never contain free variables (is that true?)

%This type contains free variables when A is replaced by an CC wildcard

%This must fail:
\begin{verbatim}
<A> A m(List<? extends List<A>> l, A)

m(List<List<? super String>> l, "hi") 
\end{verbatim}
%This fails because of Equals rule (TODO: proof)

\item[Tame] same reasoning as Normalize
\item[Bot] S-Bot
\item[Pit] S-Bot
\item[Upper] S-Trans and S-VarLeft
\item[Lower] S-Trans and S-VerRight
\item[Subst-WC] by S-Refl
\item[Subst]
$\sigma(C \cup \set{\tv{a} \doteq \type{T}}) = \sigma([\type{T}/\tv{a}]C \cup \set{\tv{a} \doteq \type{T}})$
and
$\sigma(\wildcardEnv) = \sigma([\type{T}/\tv{a}]\wildcardEnv)$
\item[Subst-WC]
%Proof by Lemma 5 \emph{Type substitution preserves subtyping} from \cite{WildcardsNeedWitnessProtection}.
Same as Subst
\end{description}

\subsection{Type Inference Soundness}
The type solution is a correct one in respect to the type rules.

Problem:
The capture conversion and let statements.
Constraint a <. b => CC(X.C<X>) <: C<X>
Why is X the only type used

$\type{T} \lessdot \type{S}$:
If the left part of the constraint has no free variables the solution $\sigma(\type{T})$ will have neither.
This means that all used type variables on both sides are bound in the global environment or the environment of the left side
%X.C<X> <: C<X>
%C<X> = C<X> (both sides must be the same)
%the left side has no free variables!