From 69696cb76d8c5874b78b74a1d32e5a0bd33d2036 Mon Sep 17 00:00:00 2001
From: Leon Vatthauer <leon.vatthauer@fau.de>
Date: Wed, 6 Mar 2024 16:29:43 +0100
Subject: [PATCH] Continue working on proofs concerning K
---
thesis/main.tex | 52 ++++-----------
thesis/src/04_iteration.tex | 123 ++++++++++++++++++++++++++++--------
2 files changed, 109 insertions(+), 66 deletions(-)
diff --git a/thesis/main.tex b/thesis/main.tex
index 7619561..8fa05e7 100644
--- a/thesis/main.tex
+++ b/thesis/main.tex
@@ -99,51 +99,18 @@
\usepackage{noto-mono}
-\usepackage{mathpazo}
\usepackage{unicode-math}
+% \setmainfont{STIX-Regular}
+% \setmathfont{STIX Two Math Regular}
+
\usepackage{mathrsfs}
\usepackage[colorinlistoftodos,prependcaption,textsize=tiny]{todonotes}
\usepackage{xargs}
\usepackage{xstring}
-%\usepackage{fontspec}
-%\setmonofont{Noto Sans Mono}
-\usepackage{pict2e}
-
-% \newcommand{\lbparen}{%
-% \mathopen{%
-% \sbox0{$()$}%
-% \setlength{\unitlength}{\dimexpr\ht0+\dp0}%
-% \raisebox{-\dp0}{%
-% \begin{picture}(.32,1)
-% \linethickness{\fontdimen8\textfont3}
-% \roundcap
-% \put(0,0){\raisebox{\depth}{$($}}
-% \polyline(0.32,0)(0.1,0)(0.1,1)(0.32,1)
-% \end{picture}%
-% }%
-% }%
-% }
-
-% \newcommand{\rbparen}{%
-% \mathclose{%
-% \sbox0{$()$}%
-% \setlength{\unitlength}{\dimexpr\ht0+\dp0}%
-% \raisebox{-\dp0}{%
-% \begin{picture}(.32,1)
-% \linethickness{\fontdimen8\textfont3}
-% \roundcap
-% \put(0.02,0){\raisebox{\depth}{$)$}}
-% \polyline(0.1,0)(0.32,0)(0.32,1)(0.1,1)
-% \end{picture}%
-% }%
-% }%
-% }
-
-\newcommand{\lbparen}{〖}
% https://unicodeplus.com/U+3016
-
-\newcommand{\rbparen}{〗}
+\newcommand*{\lbparen}{〖}
+\newcommand*{\rbparen}{〗}
% category C
\newcommand*{\C}{\ensuremath{\mathscr{C}}}
@@ -160,10 +127,15 @@
\newcommand*{\strongpreelgot}[1]{\ensuremath{\mathit{StrongPreElgot}(#1)}}
\newcommand*{\setoids}{\ensuremath{\mathit{Setoids}}}
% free objects
-\newcommand*{\freee}[1]{\ensuremath{#1^\bigstar}}
+\newcommand*{\freee}[1]{\ensuremath{#1^\star}}
\newcommand*{\free}[1]{
\ensuremath{
- \IfSubStr{#1}{\circ}{{\freee{(#1)}}}{\freee{#1}}
+ \IfSubStr{#1}{\circ}
+ {{\freee{(#1)}}}
+ {\IfSubStr{#1}{\;}
+ {\freee{(#1)}}
+ {\freee{#1}}
+ }
}
}
% right stability
diff --git a/thesis/src/04_iteration.tex b/thesis/src/04_iteration.tex
index 7a00d81..57fef40 100644
--- a/thesis/src/04_iteration.tex
+++ b/thesis/src/04_iteration.tex
@@ -305,7 +305,7 @@ A symmetrical variant of the previous definition is sometimes useful.
\\=\;&\ls{f \circ swap} \circ (h^{\#_y} \times id) \circ swap
\\=\;&((\ls{f \circ swap} + id) \circ dstr \circ (id \times h))^{\#_a} \circ swap
\\=\;&(((\ls{f \circ swap} \circ swap) + id) \circ dstl \circ (id \times h))^{\#_a}\tag{\ref{law:uniformity}}
- \\=\;&(((\rs{f} + id) \circ dstl \circ (id \times h))^{\#_a}
+ \\=\;&(((\rs{f} + id) \circ dstl \circ (id \times h))^{\#_a},
\end{alignat*}
for any $Z \in \obj{\C}, h : Z \rightarrow KY + Z$.
@@ -318,7 +318,7 @@ A symmetrical variant of the previous definition is sometimes useful.
\\=\;&(\ls{f \circ swap} + id) \circ dstr \circ (h \times id) \circ swap.
\end{alignat*}
- The diagram commutes, since
+ The requisite diagram commutes, since
\begin{alignat*}{1}
&\rs{f} \circ (id \times \eta)
\\=\;&\ls{f \circ swap} \circ swap \circ (id \times \eta)
@@ -342,19 +342,20 @@ A symmetrical variant of the previous definition is sometimes useful.
\\=\;&((g + id) \circ dstl \circ (id \times h))^{\#_a} \circ swap
\\=\;&(((g \circ swap) + id) \circ dstr \circ (h \times id))^{\#_a},\tag{\ref{law:uniformity}}
\end{alignat*}
+ for any $Z \in \obj{\C}, h : Z \rightarrow KY + Z$.
- where the application of \ref{law:uniformity} is justified by
+ The application of \ref{law:uniformity} is justified by
\begin{alignat*}{1}
&(id + swap) \circ ((g \circ swap) + id) \circ dstr \circ (h \times id)
\\=\;&(g + id) \circ (swap + swap) \circ dstr \circ (h \times id)
\\=\;&(g + id) \circ dstl \circ swap \circ (h \times id)
- \\=\;&(g + id) \circ dstl \circ (id \times h) \circ swap
+ \\=\;&(g + id) \circ dstl \circ (id \times h) \circ swap.
\end{alignat*}
- This concludes one direction of the proof that left stability and right stability imply each other, the other direction follows by a symmetrical proof.
+ This concludes one direction of the proof that left stability and right stability imply each other, the other direction follows symmetrically.
\end{proof}
-The following theorem illustrates that stability of $KX$ indeed simulates the behavior of $KX$ in a cartesian closed category.
+In a less general setting stability indeed follows automatically.
\todo[inline]{Fix proof, replace free object operator, fix references.}
@@ -362,31 +363,70 @@ The following theorem illustrates that stability of $KX$ indeed simulates the be
In a cartesian closed category every free Elgot algebra is stable.
\end{theorem}
\begin{proof}
- Let $X \in \obj{\C}$ and $((KX, (-)^\#), \llbracket - \rrbracket)$ be a free Elgot algebra on $X$.
+ Let $\C$ be cartesian closed and let $(KX, (-)^\#, \free{(-)})$ be a free Elgot algebra on some $X \in \obj{\C}$.
- We will show that $KX$ is left-stable, i.e. given $X \in \obj{\C}, A \in \vert\elgotalgs{\C}\vert$ and $f : Y \times X \rightarrow A$ we define
- $\ls{f} := eval \circ (\llbracket curry\;f \rrbracket \times id)$.
- Note that we are using the universal property of a free object over $\textit{Elgot}(\C)$ which when spelled out requires us to show that $A^X$ is an Elgot algebra, for that we reference lemma~\ref{lem:elgotexp}.
- \ref{sharpl1} and \ref{sharpl2} then follow by properties of the exponential and of distributive categories, uniqueness is more interesting:
- Let $g : KY \times X \rightarrow A$ be a morphism satisfying \ref{sharpl1} and \ref{sharpl2}, we need to show that $g = eval \circ (\llbracket curry\;f \rrbracket \times id)$. We use that fact that $curry$ is an injective mapping, i.e. it suffices to show that:
- \[curry\; g = \llbracket curry\;f \rrbracket = curry (eval \circ (\llbracket curry\;f \rrbracket \times id))\]
- Where the second step holds for any exponential and the first step is proven by the universal property of free objects, i.e. we need to show that $curry\;g \circ \eta = curry\;f$ which follows by \ref{sharpl1}, and we need to check that $curry\;g$ is left iteration preserving which follows from \ref{sharpl2}.
+ To show left stability of $KX$ we define $\ls{f} := eval \circ (\free{curry\;f} \times id)$ for any $X \in \obj{\C}, A \in \vert\elgotalgs{\C}\vert$, and $f : Y \times X \rightarrow A$.
+ We will now verify that this does indeed satisfy the requisite properties, i.e.
+ \begin{alignat*}{1}
+ &eval \circ (\free{curry\;f} \times id) \circ (\eta \times id)
+ \\=\;&eval \circ ((\free{curry\;f} \circ \eta) \times id)
+ \\=\;&eval \circ (curry\;f) \times id)
+ \\=\;&f
+ \end{alignat*}
+ and for any $Z \in \obj{\C}, h : Z \rightarrow KY + Z$:
+ \begin{alignat*}{1}
+ &eval \circ (\free{curry\;f} \times id) \circ (h^{\#_a} \times id)
+ \\=\;&eval \circ ((\free{curry\;f} \circ h^{\#_a}) \times id)
+ \\=\;&eval \circ (curry(((eval + id) \circ dstr \circ (((\free{curry\;f} + id) \circ h) \times id))^{\#_b})) \times id)
+ \\=\;&((eval + id) \circ dstr \circ (((\free{curry\;f} + id) \circ h) \times id))^{\#_b}
+ \\=\;&((eval + id) \circ dstr \circ ((\free{curry\;f} + id) \times id) \circ (h \times id))^{\#_b}
+ \\=\;&((eval + id) \circ ((\free{curry\;f} \times id) + id) \circ dstr \circ (h \times id))^{\#_b}
+ \\=\;&(((eval \circ (\free{curry\;f} \times id)) + id) \circ dstr \circ (h \times id))^{\#_b}.
+ \end{alignat*}
+
+ \unsure[inline]{Maybe prove that curry is injective in preliminaries.}
+
+ Lastly, we need to check uniqueness of $\ls{f}$. Let us consider a left iteration preserving morphism $g : KY \times X \rightarrow A$ that satisfies $g \circ (\eta \times id) = f$. Since $curry$ is an injective mapping it suffices to show that
+ \begin{alignat*}{1}
+ &curry\;\ls{f}
+ \\=\;&curry(eval \circ (\free{curry\;f} \times id))
+ \\=\;&\free{curry\;f}
+ \\=\;&curry\;g.
+ \end{alignat*}
+ Where the last step is the only non-trivial one. Since $\free{curry\;f}$ is a unique iteration preserving morphism satisfying $\free{curry\;f} \circ \eta = curry\;f$, we are left to show that $g$ is also iteration preserving and satisfies the same property.
+
+ \unsure[inline]{Maybe prove helper lemmas about exponentials in preliminaries, like subst, beta and eta.}
+
+ Indeed,
+ \begin{alignat*}{1}
+ &curry\;g \circ h^{\#}
+ \\=\;&curry\;(g \circ (h^{\#} \times id))
+ \\=\;&curry\;(((g + id) \circ dstr \circ (h \times id))^{\#_a})
+ \\=\;&curry\;((((eval \circ (curry\; g \times id)) + id) \circ dstr \circ (h \times id))^{\#_a})
+ \\=\;&curry\;(((eval + id) \circ ((curry\; g \times id) + id) \circ dstr \circ (h \times id))^{\#_a})
+ \\=\;&curry\;(((eval + id) \circ dstr \circ ((curry\;g + id) \times id) \circ (h \times id))^{\#_a})
+ \\=\;&curry\;(((eval + id) \circ dstr \circ (((curry\;g + id) \circ h) \times id))^{\#_a})
+ \end{alignat*}
+ for any $Z \in \obj{\C}, h : Z \rightarrow KY + Z$, and
+ \begin{alignat*}{1}
+ &curry\;g \circ \eta
+ \\=\;&curry(g \circ (\eta \times id))
+ \\=\;&curry\;f
+ \end{alignat*}
+
+ This completes the proof.
\end{proof}
-For the rest of this chapter we will assume every $KX$ to exist and be stable to show that it is an equational lifting monad and in fact the initial strong pre-Elgot monad.
+For the rest of this chapter we will assume every $KX$ to exist and be stable. Under these assumptions we show that $\mathbf{K}$ is an equational lifting monad and in fact the initial strong pre-Elgot monad.
-Before proving strength, we will introduce a proof principle similar to remark~\ref{rem:coinduction}.
-
-\begin{remark}[Proof by stability]~\label{rem:proofbystability}
- Given two morphisms $g, h : X \times KY \rightarrow A$ where $X, Y \in \obj{\C}, A \in \obj{\elgotalgs{\C}}$ to show that $g = h$ it suffices to find a morphism $f : X \times Y \rightarrow A$ such that $g$ and $h$ satisfy \ref{sharpr1} and \ref{sharpr2}.
+Let us first introduce a proof principle similar to \autoref{rem:coinduction}.
+\begin{remark}[Proof by right-stability]~\label{rem:proofbystability}
+ Given two morphisms $g, h : X \times KY \rightarrow A$ where $X, Y \in \obj{\C}, A \in \obj{\elgotalgs{\C}}$ to show that $g = h$ it suffices to show that $g$ and $h$ are right iteration preserving and there exists a morphism $f : X \times Y \rightarrow A$ such that $g \circ (id \times \eta) = f$ and $h \circ (id \times \eta) = f$.
\end{remark}
-
-Of course there is also a symmetric version of this:
-
+Of course there is also a symmetric version of this.
\begin{remark}[Proof by left-stability]~\label{rem:proofbyleftstability}
- Given two morphisms $g, h : KY \times X \rightarrow A$ where $X, Y \in \obj{\C}, A \in \obj{\elgotalgs{\C}}$ to show that $g = h$ it suffices to find a morphism $f : Y \times X \rightarrow A$ such that $g$ and $h$ satisfy \ref{sharpl1} and \ref{sharpl2}.
+ Given two morphisms $g, h : X \times KY \rightarrow A$ where $X, Y \in \obj{\C}, A \in \obj{\elgotalgs{\C}}$ to show that $g = h$ it suffices to show that $g$ and $h$ are left iteration preserving and there exists a morphism $f : Y \times X \rightarrow A$ such that $g \circ (\eta \times id) = f$ and $h \circ (\eta \times id) = f$.
\end{remark}
-
\todo[inline]{Maybe do a helper proposition first that characterizes tau with the three laws in the file}
\begin{theorem}
@@ -397,7 +437,7 @@ Of course there is also a symmetric version of this:
\change[inline]{Maybe put complete proof}
- To check naturality and the strength laws we will use remark~\ref{rem:proofbystability} and for brevity only state the needed unifying morphism by pasting \ref{sharpl1} into the required diagram. The proofs of \ref{sharpr1} and \ref{sharpr2} can then be looked up in the formalization.
+ To check naturality and the strength laws we will use \autoref{rem:proofbystability} and for brevity only state the needed unifying morphism by pasting \ref{sharpl1} into the required diagram. The proofs of \ref{sharpr1} and \ref{sharpr2} can then be looked up in the formalization.
For naturality of $\tau$ we use:
% https://q.uiver.app/#q=WzAsNSxbMSwwLCJBIFxcdGltZXMgS0IiXSxbMCwzLCJBIFxcdGltZXMgQiJdLFsxLDIsIksoQSBcXHRpbWVzIEIpIl0sWzMsMiwiSyhYIFxcdGltZXMgWSkiXSxbMywwLCJYIFxcdGltZXMgS1kiXSxbMSwwLCJpZCBcXHRpbWVzIFxcZXRhIiwwLHsiY3VydmUiOi0yfV0sWzAsMiwiXFx0YXUiLDJdLFsyLDMsIksoZlxcdGltZXMgZykiLDJdLFswLDQsImYgXFx0aW1lcyBLZyJdLFs0LDMsIlxcdGF1Il0sWzEsMywiXFxldGEgXFxjaXJjIChmIFxcdGltZXMgZykiLDIseyJjdXJ2ZSI6Mn1dXQ==
@@ -507,7 +547,38 @@ Of course there is also a symmetric version of this:
\end{theorem}
\begin{proof}
- \todo[inline]{Proof that K is equational lifting}
+ We need to show that $\tau \circ \Delta = K \langle \eta , id \rangle$. Note that $K \langle \eta , id \rangle = \free{\eta \circ \langle \eta , id \rangle}$, which is a unique Elgot algebra morphism satisfying $K \langle \eta , id \rangle \circ \eta = \eta \circ \langle \eta , id \rangle$. It thus suffices to show that $\tau \circ \Delta$ satisfies the same identity and is iteration preserving.
+
+ The identity follows easily
+
+ \todo[inline]{Reference $\tau-\eta$ in last step:}
+
+ \begin{alignat*}{1}
+ &\tau \circ \Delta \circ \eta
+ \\=\;&\tau \circ \langle \eta , \eta \rangle
+ \\=\;&\tau \circ (id \times \eta) \circ \langle \eta , id \rangle
+ \\=\;&\eta \circ \langle \eta , id \rangle.
+ \end{alignat*}
+
+ For iteration preservation of $\tau \circ \Delta$ consider $Z \in \obj{\C}$ and $h : Z \rightarrow KX + Z$, then
+ \begin{alignat*}{1}
+ &\tau \circ \Delta \circ h^{\#}
+ \\=\;&\tau \circ \langle h^{\#} , h^{\#} \rangle
+ \\=\;&\tau \circ (id \times h^{\#}) \circ \langle h^{\#} , id \rangle
+ \\=\;&((\tau + id) \circ dstl \circ (id \times f))^\# \circ \langle h^{\#} , id \rangle
+ \\=\;&(((\tau \circ \Delta) + id) \circ f)^\#.\tag{\ref{law:uniformity}}
+ \end{alignat*}
+
+ Note that by monicity of $dstl^{-1}$ and by \ref{law:fixpoint}
+ \[(\Delta + \langle f^\# , id \rangle) \circ f = dstl \circ \langle f^\# , f \rangle. \]
+ The application of \ref{law:uniformity} is then justified by
+ \begin{alignat*}{1}
+ &(id + \langle f^\# , id \rangle) \circ ((\tau \circ \Delta) + id) \circ f
+ \\=\;&((\tau \circ \Delta) + \langle f^\# , id \rangle) \circ f
+ \\=\;&(\tau + id) \circ (\Delta + \langle f^\# , id \rangle) \circ f
+ \\=\;&(\tau + id) \circ dstl \circ \langle f^\# , f \rangle
+ \\=\;&(\tau + id) \circ dstl \circ (id \times f) \circ \langle f^\# , id \rangle.
+ \end{alignat*}
\end{proof}
\begin{theorem}