stan/Ecoop2024_TIforWildFJ
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Start soundness for prepare rule

Browse Source
This commit is contained in:
Andreas Stadelmeier 2024-01-15 20:43:19 +01:00
parent b9e0b1fa6d
commit b546da831d
1 changed files with 13 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

16
soundness.tex
View File

@ -271,15 +271,25 @@ $\Delta \vdash \sigma(C') \implies \Delta \vdash \sigma(C)$
%\item[Capture, Reduce] are always applied together. We have to destinct between two cases: %\item[Capture, Reduce] are always applied together. We have to destinct between two cases:
\item[Prepare] \item[Prepare]
To show To show
$\Delta \vdash \wctype{\overline{\wildcard{B}{U}{L}}}{C}{\ol{S}} <: \wctype{\overline{\wildcard{A}{\type{U}}{\type{L}}}}{C}{\ol{T}}$ by S-Exists we have to proof: $\Delta \vdash \wctype{\overline{\wildcard{B}{\type{U'}}{\type{L'}}}}{C}{\ol{S}} <: \wctype{\overline{\wildcard{A}{\type{U}}{\type{L}}}}{C}{\ol{T}}$ by S-Exists we have to proof:
We know
\begin{gather}
\ol{S} = \ol{T}\\
\text{fv}(\wctype{\overline{\wildcard{B}{\type{U'}}{\type{L'}}}}{C}{\ol{S}}) = \emptyset\\
\text{fv}(\wctype{\overline{\wildcard{A}{\type{U}}{\type{L}}}}{C}{\ol{T}}) = \emptyset
%TODO
\end{gather}
\begin{gather} \begin{gather}
\Delta', \Delta \vdash [\ol{T}/\ol{\type{A}}]\ol{L} <: \ol{T} \\ \Delta', \Delta \vdash [\ol{T}/\ol{\type{A}}]\ol{L} <: \ol{T} \\
\Delta', \Delta \vdash \ol{T} <: [\ol{T}/\ol{\type{X}}]\ol{U} \\ \Delta', \Delta \vdash \ol{T} <: [\ol{T}/\ol{\type{X}}]\ol{U} \\
\text{fv}(\ol{T}) \subseteq \text{dom}(\Delta) \\ \label{rp:3}
\text{fv}(\ol{T}) \subseteq \text{dom}(\Delta, \overline{\wildcard{B}{U}{L}}) \\
\label{rp:4} \label{rp:4}
\text{dom}(\overline{\wildcard{B}{U}{L}}) \cap \text{fv}(\wctype{\ol{\wildcard{X}{U}{L}}}{C}{\ol{S}}) = \emptyset \text{dom}(\overline{\wildcard{B}{U}{L}}) \cap \text{fv}(\wctype{\ol{\wildcard{A}{U}{L}}}{C}{\ol{T}}) = \emptyset
\end{gather} \end{gather}
\ref{rp:4} is always true. \ref{rp:4} is always true.
Due to $\text{fv}(\sigma(\wctype{\overline{\wildcard{B}{\type{U}}{\type{L}}}}{C}{\ol{S}})) = \emptyset$ implies \ref{rp:3}.
\item[Capture] \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}}) = \emptyset$ the preposition holds by Assumption and S-Exists.