Comments on Well-Formedness proof

soundness.tex

@@ -68,6 +68,24 @@ By structural induction over the expression $\texttt{e}$.
     % $\ol{N} <: [\ol{S}/\ol{X}]\ol{U}$,
     % TODO: S ok? We could proof $\Delta, \Delta' \overline{\Delta} \vdash \ol{S} \ \ok$
     % by proofing every substitution in Unify is ok aslong as every type in the inputs is ok
+    % S ok when all variables are in the environment and every L <: U and U <: Class-bound
+    % This can be given by the constraints generated. We can proof if T ok and S <: T and T <: S' then S ok and S' ok
+
+    % If S ok and T <. S , then Unify generates a T ok
+    S typeinference:
+    T <: [S/Y]U
+    We apply the following lemma
+    Lemma
+    if T ok and T <: S then S ok
+
+    until
+    T = [S/Y]U
+
+    and then we can say by 
+    Lemma:
+    If [S/Y]U ok then S ok (TODO: proof!)
+
+    So we do not have to proof S ok (but T)
 
     $\Delta \vdash \sigma(\tv{a}), \wcNtype{\Delta_c}{N} \ \ok$ %TODO
     %Easy, because unify only generates substitutions for normal type placeholders which are OK
@@ -131,6 +149,24 @@ Method calls generate multiple constraints that share the same wildcard placehol
 % $\text{fv}(\type{T}) \subseteq \text{dom}(\Delta)$.
 % %UNIFY fails when there are free variables on the right side of a a =. T constraint
 
+\begin{lemma}
+    Well-formedness is hereditary
+    \begin{description}
+        \item[If] $\triangle \vdash \exptype{C}{\ol{X}} \ \ok$ and $\triangle \vdash \exptype{C}{\ol{X}} <: \type{S}$
+        \item[Then] $\triangle \vdash \type{S} \ \ok$
+    \end{description}
+\end{lemma}
+\textit{Proof:}
+
+\begin{lemma}
+    Well-formedness is hereditary
+    \begin{description}
+        \item[If] $\triangle \vdash \type{T} \ \ok$ and $\triangle \vdash \type{S} <: \type{T}$
+        \item[Then] $\triangle \vdash \type{S} \ \ok$
+    \end{description}
+\end{lemma}
+
+
 \begin{lemma} \label{lemma:tvsNoFV}
     \unify{} does not add free variables to types not containing free variables.
     \begin{description}