Fix Capture Soundness

soundness.tex

@@ -272,59 +272,35 @@ $\Delta \vdash  \sigma(C') \implies \Delta \vdash \sigma(C)$
 \item[Adopt] Assumption, because $C \subset C'$
 %\item[Capture, Reduce] are always applied together. We have to destinct between two cases:
 \item[Prepare]
-To show 
-$\Delta \vdash \sigma(\wctype{\overline{\wildcard{B}{\type{U}}{\type{L}}}}{C}{\ol{S}}) <: \sigma(\wcNtype{\Delta''}{N})$ by S-Exists we have to proof:
+%To show 
+%$\Delta \vdash \sigma(\wctype{\Delta'}{C}{\ol{S}}) <: \sigma(\wctype{\overline{\wildcard{X}{U}{L}}}{C}{\ol{T}})$ by S-Exists we have to proof:
+Given a constraint $ \wctype{\Delta'}{C}{\ol{S}} \lessdot \wctype{\Delta''}{C}{\ol{T}}$ first the \rulename{Prepare} rule
+then the \rulename{Capture} rule is applied.
+Therefore we can assume $\Delta, \Delta' \vdash \sigma(\exptype{C}{\ol{S}}) <: \sigma(\wctype{\Delta''}{C}{\ol{T}})$ (see proof for \rulename{Capture})
+which implies $\Delta \vdash \sigma(\wctype{\Delta'}{C}{\ol{S}}) <: \sigma(\wctype{\Delta''}{C}{\ol{T}})$ by S-Exists:
+$\text{fv}(\sigma(\wctype{\Delta''}{C}{\ol{T}})) = \emptyset$ implies $\text{dom}(\Delta'') \cap \text{fv}(\sigma(\wctype{\Delta''}{C}{\ol{T}})) = \emptyset$.
+$\text{fv}(\sigma(\wctype{\Delta'}{C}{\ol{S}})) = \emptyset$ implies $\text{fv}(\ol{S})\subseteq \text{dom}(\Delta, \Delta')$.
 
 
-
-We set $\Delta' = \sigma(\wildcardEnv)$.
-
-\begin{gather}
-\Delta', \Delta \vdash [\ol{T}/\ol{\type{A}}]\ol{L} <: \ol{T} \\
-\Delta', \Delta \vdash \ol{T} <: [\ol{T}/\ol{\type{X}}]\ol{U} \\
-\label{rp:3}
-\text{fv}(\ol{T}) \subseteq \text{dom}(\Delta, \overline{\wildcard{B}{U}{L}}) \\
-\label{rp:4}
-\text{dom}(\overline{\wildcard{B}{U}{L}}) \cap \text{fv}(\wctype{\ol{\wildcard{A}{U}{L}}}{C}{\ol{T}}) = \emptyset\\
-[\ol{A}/\ol{T}] = \ol{T} %TODO: rename T
-\end{gather}
-
-\item[Prepare] 
-To show 
-$\Delta \vdash \sigma(\wctype{\overline{\wildcard{B}{\type{U'}}{\type{L'}}}}{C}{\ol{S}}) <: \sigma(\wctype{\overline{\wildcard{A}{\type{U}}{\type{L}}}}{C}{\ol{T}})$ by S-Exists we have to proof:
-\begin{gather}
-\Delta', \Delta \vdash [\ol{T}/\ol{\type{A}}]\ol{L} <: \ol{T} \\
-\Delta', \Delta \vdash \ol{T} <: [\ol{T}/\ol{\type{X}}]\ol{U} \\
-\label{rp:3}
-\text{fv}(\ol{T}) \subseteq \text{dom}(\Delta, \overline{\wildcard{B}{U}{L}}) \\
-\label{rp:4}
-\text{dom}(\overline{\wildcard{B}{U}{L}}) \cap \text{fv}(\wctype{\ol{\wildcard{A}{U}{L}}}{C}{\ol{T}}) = \emptyset\\
-[\ol{A}/\ol{T}] = \ol{T} %TODO: rename T
-\end{gather}
-
-We know
-\begin{gather}
-    \sigma(\ol{S}) = [\ol{\wtv{a}}/\ol{A}]\ol{T}\\
-    \ol{\wtv{a}} \lessdot [\ol{\wtv{a}}/\ol{A}]\ol{U}\\
-    [\ol{\wtv{a}}/\ol{A}]\ol{L} \lessdot \ol{\wtv{a}}\\
-    \text{fv}(\wctype{\overline{\wildcard{B}{\type{U'}}{\type{L'}}}}{C}{\ol{S}}) = \emptyset\\
-\label{rp:fv2}
-    \text{fv}(\wctype{\overline{\wildcard{A}{\type{U}}{\type{L}}}}{C}{\ol{T}}) = \emptyset
-\end{gather}
-
-\ref{rp:fv2} implies \ref{rp:4}.
-Due to $\text{fv}(\sigma(\wctype{\overline{\wildcard{B}{\type{U}}{\type{L}}}}{C}{\ol{S}})) = \emptyset$ implies
-$\text{fv}(\type{T}) \subseteq \text{dom}(\overline{\wildcard{B}{\type{U}}{\type{L}}})$
-and therefore \ref{rp:3}.
+% Under the assumption there exists a $\Delta''$ with
+% $\Delta, \Delta'' \vdash \sigma(\exptype{C}{\ol{S}}) <: \sigma(\wctype{\overline{\wildcard{X}{U}{L}}}{C}{\ol{T}})$
+% and $\Delta' \subseteq \Delta''$ and $\text{fv}(\Delta) = \emptyset$.
+% Due to $\text{fv}(\sigma(\wctype{\Delta'}{C}{\ol{S}})) = \emptyset$
+% and $\text{fv}(\sigma(\wctype{\overline{\wildcard{X}{U}{L}}}{C}{\ol{T}})) = \emptyset$
+% we can say %TODO: Can we really say that? Weakening does not apply (it is the other direction than weakening)
+% $\Delta, \Delta' \vdash \sigma(\exptype{C}{\ol{S}}) <: \sigma(\wctype{\overline{\wildcard{X}{U}{L}}}{C}{\ol{T}})$
+% which implies 
+% $\Delta \vdash \sigma(\wctype{\Delta'}{C}{\ol{S}}) <: \sigma(\wctype{\overline{\wildcard{X}{U}{L}}}{C}{\ol{T}})$.
 
 \item[Capture]
 Everytime the \rulename{Capture} rule is invoked we add the freshly generated free variables to the global environment $\wildcardEnv$.
 They are from this point on treated like global variables and therefore we can assume $\sigma(\wildcardEnv \cup \ol{\wildcard{C}{U}{L}}) \subseteq \Delta'$ in
 $\Delta, \Delta' \vdash \sigma([\ol{\rwildcard{C}}/\ol{\rwildcard{B}}] \exptype{C}{\ol{S}})
 <: \sigma(\wctype{\Delta}{C}{\ol{T}})$,
-which implies $\Delta, \Delta'/\set{\ol{\wildcard{C}{U}{L}}} \vdash \type{N} <: \sigma(\wctype{\Delta}{C}{\ol{T}})$,
-with $\wcNtype{\overline{\wildcard{C}{\type{U}}{\type{L}}}}{N} = \sigma(\wctype{\overline{\wildcard{C}{\type{U}}{\type{L}}}}{C}{\ol{S}})$
-We can rename a fresh wildcard $\rwildcard{C}$ freely.
+which implies $\Delta, \Delta'/\set{\ol{\wildcard{C}{U}{L}}} \vdash \sigma(\wctype{\overline{\wildcard{C}{\type{U}}{\type{L}}}}{C}{\ol{S}}) <: \sigma(\wctype{\Delta}{C}{\ol{T}})$.
+As long as $\ol{C} \notin \text{fv}(\sigma(\wctype{\Delta}{C}{\ol{T}}))$ (TODO: do we need to set the right side to not contain free variables?: NO! because all free variables are inside $\Delta$).
+%with $\type{N}= \sigma(\wctype{\overline{\wildcard{C}{\type{U}}{\type{L}}}}{C}{\ol{S}})$
+%We can rename a fresh wildcard $\rwildcard{C}$ freely.
 
 % 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$ the preposition holds because