From 43e75127b313f3f62bd0bcea99fc46f82042e22d Mon Sep 17 00:00:00 2001
From: Andreas Stadelmeier <andi@paulus.haus>
Date: Mon, 5 Feb 2024 14:54:42 +0100
Subject: [PATCH] Nearly finish soundness for TYPE

---
 soundness.tex | 71 +++++++++++++++------------------------------------
 1 file changed, 20 insertions(+), 51 deletions(-)

diff --git a/soundness.tex b/soundness.tex
index 1862884..1e065e5 100644
--- a/soundness.tex
+++ b/soundness.tex
@@ -109,11 +109,13 @@ $\texttt{let}\ \texttt{x} : \wcNtype{\Delta'}{N} = \texttt{e} \ \texttt{in}\
 % Solution: Make this a lemma and guarantee that Unify does only create types Delta.T with \Delta subset fv(T)
 % This is possible because free variables (except those in \Delta_in) are never used in wildcard environments
 
-We could use unify to generate S by
-$\unify{}((\Delta, \Delta', \overline{\Delta}), [\ol{\tv{a}}/\ol{X}][\ol{\tv{b}}/\ol{Y}]\set{\ol{N} \lessdot \ol{T}, \type{N} \lessdot \exptype{C}{\ol{X}}})$
-%TODO: Proof that this always works.
-% Only the variables in \Delta' ol\Delta are used. Maybe change the lemma 10 to that.
-% That part of the unify algorithm is not influenced by other free variables
+By lemma \ref{lemma:unifyWeakening} we know that 
+$\unify{}(\Delta, [\ol{\tv{a}}/\ol{X}][\ol{\tv{b}}/\ol{Y}]\set{ \overline{\wcNtype{\Delta}{N}} \lessdotCC \ol{T}, \wcNtype{\Delta'}{N} \lessdotCC \exptype{C}{\ol{X}}})$
+has a solution.
+Also $\overline{\wcNtype{\Delta}{N}} \lessdot \ol{T}$ and $\wcNtype{\Delta'}{N} \lessdotCC \exptype{C}{\ol{X}}$ will be converted to 
+$\ol{N} \lessdot \ol{T}$ and $\type{N} \lessdot \exptype{C}{\ol{X}}$ by the \rulename{Capture} rule.
+Which then results in the same as calling $\unify{}((\Delta, \Delta', \overline{\Delta}), [\ol{\tv{a}}/\ol{X}][\ol{\tv{b}}/\ol{Y}]\set{\ol{N} \lessdot \ol{T}, \type{N} \lessdot \exptype{C}{\ol{X}}})$,
+which shows $\Delta, \Delta', \overline{\Delta} \vdash \overline{N} <: [\ol{S}/\ol{X}]\overline{U}$.
 
     This implies $\text{dom}(\Delta') \subseteq \text{fv}(\type{N})$ and $\text{dom}(\Delta') \subseteq \text{fv}(\type{N})$
     $\Delta, \Delta', \overline{\Delta} \vdash [\ol{S}/\ol{X}]\type{U} \type{T}$,
@@ -141,25 +143,7 @@ $\unify{}((\Delta, \Delta', \overline{\Delta}), [\ol{\tv{a}}/\ol{X}][\ol{\tv{b}}
 %     \end{gather}
 
 Method calls generate multiple constraints that share the same wildcard placeholders ($\ol{\wtv{a}}$, $\ol{\wtv{b}}$).
-%TODO: show that only those wildcards in the parameters and receiver type are used ($\ol{\Delta}$)
 
-    % X.List<X> <. List<a?>
-    % set \sigma(r) = X.N
-    % If there exists a subtype r <: T, then r <: X.N, N <: T with X.N == r
-    % If  CC(X.N) <: T, then N <: T
-    % R <: X.N due to S-Refl.
-    % \Delta, X \vdash N <: T due to assumption and S-Exists.
-    % What if X.N <: Y (where is this Y coming from?)
-    % %TODO:
-    % We have to show, that all constraints using the same wtv's C = X1.T1 <. X2.T2 ,...
-    % with a? \in T1, T2, ....
-    % then \Delta' \subseteq X1, X2, ... for \Delta, \Delta \vdash sigma(T1) <: sigma(X2.T2), ....
-
-    % when only wildcards in the top level domain from the constraints involving the a? variables are involved
-    % then they are all contained in $\Delta, \Delta', \overline{Delta}$, which makes S ok true! (does it?)
-    % and due to r <. T, the judgements N <: [S/X]U and T_r <: \Delta.N are true!
-
-    % If $\ol{\tv{r}} \lessdot \ol{T}$ how can we say that \Delta' only uses
 \end{description}
 
 % \begin{lemma} Unify does add free variables to types not containing free variables (or wildcard placeholders)
@@ -237,22 +221,22 @@ The GenSigma and GenDelta rules check for well-formedness.
 \textit{Proof:}
 Trivial. \unify{} fails when a constraint $\tv{a} \doteq \rwildcard{X}$ arises.
 
-\begin{lemma} \label{lemma:unifyCC}
-Free variables do not leave their scope. TODO
-Wildcard variables are only substituted by wildcards inside the same constraint.
+% do we even have to proof that?
+% \begin{lemma}
+% C = Delta.N <c T
+% is the same for Unify as:
+% Delta |-  N <. T
+% \end{lemma}
 
+\begin{lemma} \label{lemma:unifyWeakening}
+Removing constraints does not render \unify{} impossible.
+If there is a solution for a constraint set $C$, then there is also a solution for a subset of that constraint set.
 \begin{description}
-    \item[If] $(\sigma, \Delta) = \unify{}( C \cup \set{ \type{T} \lessdot \type{S} } \cup \set{ \overline{\type{T} \lessdotCC \type{S} } } )$
-    \item[and] $\text{fv}(\type{T}, \type{S}) \subseteq \text{fv}(\ol{T}, \ol{S})$, 
-        $\sigma(\ol{T}) = \ol{\wcNtype{\Delta}{N}}$ and $\sigma(\type{T}) = \wcNtype{\Delta'}{N'}$
-    \item[then] $ \Delta, \overline{\Delta}, \Delta' \vdash \sigma(\type{T}) <: \sigma(\type{S}) $
-
-    % \item[If] $(\sigma, \Delta) = \unify{}( C \cup \set{ \overline{\wcNtype{\Delta}{N} \lessdot \type{T} } } )$
-    % \item[and] $\text{fv}(\ol{T}) \notin C$, $\text{fv}(\ol{\wcNtype{\Delta}{N}}) \notin C$
-    % \item[Then] $\Delta, \overline{\Delta} \vdash \overline{ \sigma(\type{N}) <: \sigma(\type{T}) }$
+    \item[If] $(\sigma, \Delta) = \unify{}( C \cup C')$
+    \item[then] $ (\sigma', \Delta') = \unify{}( C')$
 \end{description}
-
-Their scope is the set of constraints, which contain the same free variable placeholders.
+\textit{Proof:}
+%TODO
 
 \end{lemma}
 \textit{Proof:}
@@ -273,21 +257,6 @@ and $\Delta, \Delta', \overline{\Delta} \vdash \overline{\type{N} <: \sigma'(\ty
 otherwise $\Delta, \Delta' \vdash \overline{\sigma'(\type{S'}) <: \sigma'(\type{T'})}$
 % and $\sigma(\type{T'}) = \sigma(\type{T'})$.
 
-% The function $\CC{}$ is given as $\CC{}(\wcNtype{\Delta}{N}) = \type{N}$
-
-% Unify cannot guarantee that only wildcards declared on the left side are used. Example input:
-% List<b?> <. List<b?>
-% b? =. X
-% but if the left side is a normal type (no fv's) then this can be guaranteed (maybe?)
-%String <. X_String % here X is not in the environment
-
-% What is the problem?
-% a? can only use wildcards, which are declared in \Delta or on the left side 
-% Otherwise constraints of the form a <. T cannot ensure soundness!
-
-% We could say that a? only gets free variables hold by the constraints a? appears in
-
-% a constraint a <. T means that there are free variables 
 \end{description}
 \end{lemma}