From 2a6da1ea172cbde1f72f4ea5ddaba7cba1ee97ca Mon Sep 17 00:00:00 2001 From: Leon Vatthauer Date: Tue, 12 Mar 2024 17:23:09 +0100 Subject: [PATCH] First draft of setoids chapter finished --- thesis/src/05_setoids.tex | 83 ++++++++++++++++++++++++++++++++++++--- 1 file changed, 78 insertions(+), 5 deletions(-) diff --git a/thesis/src/05_setoids.tex b/thesis/src/05_setoids.tex index ab36bd2..234cec3 100644 --- a/thesis/src/05_setoids.tex +++ b/thesis/src/05_setoids.tex @@ -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} \ No newline at end of file