leonv/bsc-leon-vatthauer
1
0
Fork 0
mirror of https://git8.cs.fau.de/theses/bsc-leon-vatthauer.git synced 2024-05-31 07:28:34 +02:00
Code Issues Projects Releases Packages Wiki Activity

First draft of setoids chapter finished

Browse source
This commit is contained in:
Leon Vatthauer 2024-03-12 17:23:09 +01:00
parent 98cdfffdb9
commit 2a6da1ea17
Signed by: leonv
SSH key fingerprint: SHA256:G4+ddwoZmhLPRB1agvXzZMXIzkVJ36dUYZXf5NxT+u8
1 changed files with 78 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

83
thesis/src/05_setoids.tex
View file

@ -418,16 +418,89 @@ Let us now return to the missing Corollary of \autoref{thm:Dfreeelgot}.
Let us proceed as follows
\begin{alignat*}{1}
& g^{\sharp_b} (\tilde{D}fst\;z)
\\\overset{B}{=}\;&g_1^{\sharp_b}\tag{\ref{law:uniformity}}
\\\overset{B}{=}\;&g_2^{\sharp_b}
\\\overset{B}{=}\;&g_1^{\sharp_b}\;z\tag{\ref{law:uniformity}}
\\\overset{B}{=}\;&g_2^{\sharp_b}\;z
\\\overset{B}{=}\;&g^{\sharp_b}(\iota^*\;z). \tag{\ref{law:uniformity}}
\end{alignat*}
Now, we are left to find suitable \(g_1, g_2 : \tilde{D}(A \times \mathbb{N}) \leadsto B + (\tilde{D} (A \times \mathbb{N}))\). Consider,
\[g_1 p := \begin{cases}
Now, we are left to find suitable \(g_1, g_2 : \tilde{D}(A \times \mathbb{N}) \leadsto B + \tilde{D} (A \times \mathbb{N})\). Consider,
\[g_1\;p := \begin{cases}
i_1(f\;x) & \text{if } p = now\;(x, zero) \\
i_2(\tilde{D}o (\iota\;(x,n))) & \text{if } p = now\;(x, n + 1) \\
i_2\;(x,n) & \text{if } p = later\;(x, n)
i_2\;q & \text{if } p = later\;q
\end{cases}\]
and
\[g_2\;p := \begin{cases}
i_1(f\;x) & \text{if } p = now\;(x , n) \\
i_2\;(x , n) & \text{if } p = later\;(x, n)
\end{cases}\]
where \(o : A \leadsto A \times \mathbb{N}\) is a setoid function that maps every \(z : A\) to \((z , 0) : A \times \mathbb{N}\). The applications of \ref{law:uniformity} are then justified by the definitions of \(g_1\) and \(g_2\) as well as the fact that \(\iota \circ o \doteq now\). % chktex 2
We are thus done after showing that \(g_1^{\sharp_b}\;z \overset{B}{=} g_2^{\sharp_b}\;z\). Consider another setoid function \[g_3 : \tilde{D}(A \times \mathbb{N}) \rightarrow B + \tilde{D}(A \times \mathbb{N}) + \tilde{D}(A \times \mathbb{N}),\]
defined by
\[g_3\;p := \begin{cases}
i_1(f\;x) & \text{if } p = now\;(x, 0) \\
i_2(i_1(\tilde{D}o(\iota\;(x,n)))) & \text{if } p = now\;(x, n + 1) \\
i_2(i_2\;q) & \text{if } p = later\;q
\end{cases}\]
Let us now proceed by
\begin{alignat*}{1}
& g_1^{\sharp_b}\;z
\\\overset{B}{=}\;&{((id + [ id , id ]) \circ g_3)}^{\sharp_b}\;z
\\\overset{B}{=}\;&{([ i_1 , {((id + [ id , id]) \circ g_3)}^{\sharp_b} + id ] \circ g_3)}^{\sharp_b}\;z\tag{\ref{law:diamond}}
\\\overset{B}{=}\;&g_2^{\sharp_b}\;z.
\end{alignat*}
Where for the first step notice that \(g_1\;x \overset{+}{=} (id + [ id , id ])(g_3\;x)\) for any \(x : \tilde{D}(A \times \mathbb{N})\) follows simply by case distinction on \(x\). For the last step, it suffices to show that \([ i_1 , {((id + [ id , id]) \circ g_3)}^{\sharp_b} + id ] (g_3\;x) \overset{+}{=} g_2\;x\) for any \(x : \tilde{D}(A \times \mathbb{N})\). We proceed by case distinction on \(x\).
\begin{mycase}
\case{} \(x = now\;(y, 0)\)\\
The goal reduces to
\begin{alignat*}{1}
& [ i_1 , {((id + [ id , id]) \circ g_3)}^{\sharp_b} + id ] (g_3\;x)
\\\overset{+}{=}\;&[ i_1 , {((id + [ id , id]) \circ g_3)}^{\sharp_b} + id ] (i_1(f\;y))
\\\overset{+}{=}\;&i_1(f\;y)
\\\overset{+}{=}\;&g_2\;x,
\end{alignat*}
which indeed holds by the definitions of \(g_2\) and \(g_3\).
\case{} \(x = now\;(y, n + 1)\)\\
The goal reduces to
\begin{alignat*}{1}
& [ i_1 , {((id + [ id , id]) \circ g_3)}^{\sharp_b} + id ] (g_3\;x)
\\\overset{+}{=}\;&[ i_1 , {((id + [ id , id]) \circ g_3)}^{\sharp_b} + id ] (i_2(i_1(\tilde{D}o(\iota\;(y,n)))))
\\\overset{+}{=}\;&i_1({((id + [ id , id]) \circ g_3)}^{\sharp_b}((\tilde{D}o(\iota\;(y,n)))))
\\\overset{+}{=}\;&i_1(f\;y)\tag{\ref{finalhelper}}
\\\overset{+}{=}\;&g_2\;x
\end{alignat*}
Where
\[{((id + [ id , id]) \circ g_3)}^{\sharp_b}(\tilde{D}o(\iota\;(y,n))) \overset{B}{=} f\;y \tag{\(\Asterisk\)}\label{finalhelper}\]
follows by induction on \(n\):
\subcase{} \(n = 0\)\\
We are done by
\begin{alignat*}{1}
& {((id + [ id , id]) \circ g_3)}^{\sharp_b}(\tilde{D}o(\iota\;(y,0)))
\\\overset{B}{=}\;&{((id + [ id , id]) \circ g_3)}^{\sharp_b}(\tilde{D}o(now\;y))
\\\overset{B}{=}\;&{((id + [ id , id]) \circ g_3)}^{\sharp_b}(now(y,0))
\\\overset{B}{=}\;&([ id , {((id + [ id , id]) \circ g_3)}^{\sharp_b} ] \circ (id + [ id , id]) \circ g_3) (now(y,0))\tag{\ref{law:fixpoint}}
\\\overset{B}{=}\;&([ id , {((id + [ id , id]) \circ g_3)}^{\sharp_b} ] \circ (id + [ id , id])) i_1(f\;y)
\\\overset{B}{=}\;&[ id , {((id + [ id , id]) \circ g_3)}^{\sharp_b} ] i_1(f\;y)
\\\overset{B}{=}\;&f\;y
\end{alignat*}
\subcase{} \(n = m + 1\)\\
Assuming that \({((id + [ id , id]) \circ g_3)}^{\sharp_b}(\tilde{D}o(\iota\;(y,m))) \overset{B}{=} f\;y\), we are done by
\begin{alignat*}{1}
& {((id + [ id , id]) \circ g_3)}^{\sharp_b}(\tilde{D}o(\iota\;(y,m+1)))
\\\overset{B}{=}\;&{((id + [ id , id]) \circ g_3)}^{\sharp_b}(\tilde{D}o(later(\iota\;(y,m))))
\\\overset{B}{=}\;&{((id + [ id , id]) \circ g_3)}^{\sharp_b}(later(\tilde{D}o(\iota\;(y,m))))
\\\overset{B}{=}\;&([ id , {((id + [ id , id]) \circ g_3)}^{\sharp_b} ] \circ (id + [ id , id]) \circ g_3) (later(\tilde{D}o(\iota\;(y,m))))\tag{\ref{law:fixpoint}}
\\\overset{B}{=}\;&([ id , {((id + [ id , id]) \circ g_3)}^{\sharp_b} ] \circ (id + [ id , id])) (i_2(i_2(\tilde{D}o(\iota\;(y,m)))))
\\\overset{B}{=}\;&[ id , {((id + [ id , id]) \circ g_3)}^{\sharp_b} ](\tilde{D}o(\iota\;(y,m)))
\\\overset{B}{=}\;&f\;y\tag*{\qedhere}
\end{alignat*}
\end{mycase}
\end{proof}