Soundness

This commit is contained in:
JanUlrich 2024-06-11 18:32:54 +02:00
parent 255e3854ef
commit 837bed5752

View File

@ -257,10 +257,19 @@ constraints in the original constraint set and
there exists a typing for the remaining type placeholders
so that the constraint set is satisfied.
\begin{lemma} \label{lemma:subtypeOnly}
If $\sigma(\tv{a}) = \emptyset$ then $\tv{a}$ appears only on the right side of $\tv{a} \lessdot \type{T}$ constraints.
\end{lemma}
\begin{lemma} \label{lemma:reduceToSigma}
If algorithm is successfull and $\type{T} \lessdot \tv{a}$ or $\tv{a} \doteq \type{T}$ or $\type{T} \doteq \tv{a}$ then $\sigma(\tv{a}) \neq \emptyset$
\end{lemma}
Proof:
Every type placeholder gets a solution, because there must be atleast one $\tv{a} \lessdot \type{N}$ constraint.
Then either the Solution-Sub generates a $\sigma'$ or the Solution rule can be used due to lemma \ref{lemma:reduceToSigma}.
Or algorithm terminates with $\emptyset$.
The Solution-Sub rule is always correct.
Proof:
\SetEnumitemKey{ncases}{itemindent=!,before=\let\makelabel\ncasesmakelabel}
\newcommand*\ncasesmakelabel[1]{Case #1}
@ -272,7 +281,6 @@ Proof:
{\endproof}
\begin{proof}
Some text or \texttt{\string\leavevmode} (so the enumerate starts in another line)
\begin{enumerate}[ncases]
\item $\tv{a} \lessdot \type{N}$.
\begin{subproof}