From 16b69f9a2c3a204f148a0a2c9158c87a125d26ec Mon Sep 17 00:00:00 2001 From: partowp Date: Wed, 5 Aug 2026 19:41:40 +0100 Subject: [PATCH] PF --- draft/draft.tex | 230 +++++++++++++++++++++++++++--------------------- 1 file changed, 132 insertions(+), 98 deletions(-) diff --git a/draft/draft.tex b/draft/draft.tex index 6ffa923..a9d7ffd 100644 --- a/draft/draft.tex +++ b/draft/draft.tex @@ -576,38 +576,42 @@ The definition derives the ordering on morphisms of each hom-set $\Hom(X,\sub Y) 0&Sg(k)(g(x))= 0 \end{cases} \end{gather*} - First, we need to prove that $\mu'$ is a subdistribution. - For every $x \in X$, $\mu'(x) \ge 0$. We have: + Now, we need to prove that $\mu'$ is a subdistribution, but we do not need to prove it directly. Proving that $\mu'\appr\mu$ entails that $\mu'$ is a subdistribution. So, we prove that $\mu'\appr\mu$. +For every $x\in X$, have the following cases: +\begin{itemize} + \item $Sg(\mu)(g(x))= 0$: We have $\mu'(x)=0$, and obviously $\mu'\appr\mu$. + \item $Sg(\mu)(g(x))\neq 0$: We have $\frac{\nu(g(x))}{Sg(\mu)(g(x))} \comp \mu(x)$, and since $\nu\appr Sg(\mu)$ then we have: \begin{align*} - \sum_{x \in X} \mu'(x)&\\ - =& \sum_{x \in X} \frac{\nu(g(x))}{Sg(\mu)(g(x))} \comp \mu(x)&(Sg(\mu)(g(x))\neq 0)\\ - =& \sum_{y \in Y} \sum_{x \in g^{\mone}(y)} \frac{\nu(y)}{Sg(\mu)(y)} \comp \mu(x)&(Sg(\mu)(y)\neq 0)\\ - =& \sum_{y \in Y} \frac{\nu(y)}{Sg(\mu)(y)} \comp \sum_{x \in g^{\mone}(y)} \mu(x)&(Sg(\mu)(y)\neq 0)\\ - =& \sum_{y \in Y} \frac{\nu(y)}{Sg(\mu)(y)} \comp Sg(\mu)(y)&(Sg(\mu)(y)\neq 0)\\ - =& \sum_{y \in Y} \nu(y)\\ - \leq& 1 + &\quad\frac{\nu(g(x))}{Sg(\mu)(g(x))}\leq 1\\ + \Rightarrow&\quad\frac{\nu(g(x))}{Sg(\mu)(g(x))}\comp \mu(x)\leq \mu(x) \end{align*} - As for every $x\in X$ that $Sg(\mu)(g(x))=0$, $\mu'(x)=0$, it does not have effect the inequality. Thus $\mu'$ is a subdistribution. Now, we prove $Sg(\mu') = \nu$. +\end{itemize} +% First, we need to prove that $\mu'$ is a subdistribution. +% For every $x \in X$, $\mu'(x) \ge 0$. We have: +% \begin{align*} +% \sum_{x \in X} \mu'(x)&\\ +% =& \sum_{x \in X} \frac{\nu(g(x))}{Sg(\mu)(g(x))} \comp \mu(x)&(Sg(\mu)(g(x))\neq 0)\\ +% =& \sum_{y \in Y} \sum_{x \in g^{\mone}(y)} \frac{\nu(y)}{Sg(\mu)(y)} \comp \mu(x)&(Sg(\mu)(y)\neq 0)\\ +% =& \sum_{y \in Y} \frac{\nu(y)}{Sg(\mu)(y)} \comp \sum_{x \in g^{\mone}(y)} \mu(x)&(Sg(\mu)(y)\neq 0)\\ +% =& \sum_{y \in Y} \frac{\nu(y)}{Sg(\mu)(y)} \comp Sg(\mu)(y)&(Sg(\mu)(y)\neq 0)\\ +% =& \sum_{y \in Y} \nu(y)\\ +% \leq& 1 +% \end{align*} +% As for every $x\in X$ that $Sg(\mu)(g(x))=0$, $\mu'(x)=0$, it does not effect the inequality. Thus $\mu'$ is a subdistribution. +Now, we prove $Sg(\mu') = \nu$. For any $y \in Y$, we have: - \begin{align*} - Sg(\mu')(y)&\\ - = &\sum_{x \in g^{\mone}(y)} \mu'(x)\\ - = &\sum_{x \in g^{\mone}(y)} \frac{\nu(y)}{Sg(\mu)(y)} \comp \mu(x)&(Sg(\mu)(y)\neq 0)\\ - = &\frac{\nu(y)}{Sg(\mu)(y)} \comp \sum_{x \in g^{\mone}(y)} \mu(x)&(Sg(\mu)(y)\neq 0)\\ - = &\frac{\nu(y)}{Sg(\mu)(y)} \comp Sg(\mu)(y)&(Sg(\mu)(y)\neq 0)\\ - = &\mu(y) - \end{align*} - (If $Sg(\mu)(y) = 0$, then $\nu(y) = 0$, and the sum is $0$ as well, so the equality still holds.) \\ - Now, we are left to prove that $\mu'\appr\mu$. - For every $x\in X$, have the following cases: \begin{itemize} - \item $Sg(\mu)(g(x))= 0$: We have $\mu'(x)=0$, and obviously $\mu'\appr\mu$. - \item $Sg(\mu)(g(x))\neq 0$: We have $\frac{\nu(g(x))}{Sg(\mu)(g(x))} \comp \mu(x)$, and since $\nu\appr Sg(\mu)$ then we have: + \item $Sg(\mu)(y) = 0$: We have $\nu(y) = 0$, and the sum is $0$ as well, so the equality holds.\\ + \item $Sg(\mu)(y)\neq 0$: \begin{align*} - &\quad\frac{\nu(g(x))}{Sg(\mu)(g(x))}\leq 1\\ - \Rightarrow&\quad\frac{\nu(g(x))}{Sg(\mu)(g(x))}\comp \mu(x)\leq \mu(x) - \end{align*}\qed - \end{itemize} + Sg(\mu')(y)&\\ + = &\sum_{x \in g^{\mone}(y)} \mu'(x)\\ + = &\sum_{x \in g^{\mone}(y)} \frac{\nu(y)}{Sg(\mu)(y)} \comp \mu(x)\\ + = &\frac{\nu(y)}{Sg(\mu)(y)} \comp \sum_{x \in g^{\mone}(y)} \mu(x)\\ + = &\frac{\nu(y)}{Sg(\mu)(y)} \comp Sg(\mu)(y)\\ + = &\nu(y) + \end{align*} + \end{itemize}\qed \end{proof} @@ -1302,6 +1306,7 @@ A big concern with this approach is that Comma Objects are defined in a 2-catego \subsection{Choosing a suitable order for our setting} Maybe we can first choose a suitable order on $T(\Sigma_\val\mS\times D(\mS,\mS))$ and then prove that if a relation and its inverse is a simulation then it is a bisimulation as well. Maybe $T$ being $\omega$-continuous can give the ordering. It can be something easier that relates to termination as well! That if a term has a big-step evaluation, then it is bigger than or equal to any other term, and if it does not, then it is less than or equal to any other term. \section{Symmetric Simulation is a Bisimulation} +\todo{Obviously, this chapter should be changed. All the definitions should be moved to somewhere else. You should start the chapter by giving your counter examples, and then presenting your proofs.} \begin{definition}[Graph] In a category $\BC$ a graph is a tuple $(R,X)$ of the following form: \begin{equation*} @@ -2417,79 +2422,78 @@ We define $\join$ on each $\Hom(X,\powf Y)$ for every sets $X$ and $Y$: % \todo{Finish.} %\end{proof} \subsection{Powerset Functor} -\begin{lemma}\label{lem:proj-dist-set} - For relations $R_1$ and $R_2$ the following equation holds: - \begin{gather*} - %(\powf p_i)^\dagger(R_1\cup R_2)=(\powf p_i)^\dagger(R_1)\cup(\powf p_i)^\dagger(R_2) - \powf p_i(R_1\cup R_2)=\powf p_i(R_1)\cup(\powf p_i)(R_2) - \end{gather*} -\end{lemma} -\begin{proof} - We prove the lemma for the case that $i=1$. The proof is the same for $i=2$. - Assuming $x_1\in\powf p_1(R_1\cup R_2)$ then exists $x_2$ that $(x_1,x_2)\in R_1\cup R_2$, thus either $(x_1,x_2)\in R_1$ or $(x_1,x_2)\in R_2$, so we have $x_1\in\powf p_1R_1$ or $x_1\in\powf p_1R_2$, respectively. So, we have $x_1\in \powf p_1R_1\cup\powf p_1R_2$. - - Now, assuming that $x_1\in\powf p_1R_1\cup\powf p_1R_2$ either $x_1\in\powf p_1R_1$ or $x_1\in\powf p_1R_2$. Without loss of generality, we can assume $x_1\in\powf p_1R_j$, where $j\in\{1,2\}$. - Then there exists $x_2$ that $(x_1,x_2)\in R_j$, then we have $(x_1,x_2)\in R_1\cup R_2$ that gives $x_1\in\powf p_1(R_1\cup R_2)$.\qed - % We prove the lemma for the case that $i=1$. The proof is the same for $i=2$. - % - % First, we prove $(\powf p_1)^\dagger\comp((\powf s)^\dagger\comp\sigma\comp s\join\sigma)(x_1,x_2)\subseteq(\powf p_1)^\dagger\comp(\powf s)^\dagger\comp\sigma\comp s\join(\powf p_1)^\dagger\comp\sigma(x_1,x_2)$. - % Assuming $y_1\in(\powf p_1)^\dagger\comp((\powf s)^\dagger\comp\sigma\comp s\join\sigma)(x_1,x_2)$ then exists $y_2$ that we have either $(y_1,y_2)\in(\powf s)^\dagger\comp\sigma\comp s(x_1,x_2)$ or $(y_1,y_2)\in\sigma(x_1,x_2)$. So, we have either $y_1\in(\powf p_1)^\dagger\comp(\powf s)^\dagger\comp\sigma\comp s(x_1,x_2)$ or $y_1\in(\powf p_1)^\dagger\comp\sigma(x_1,x_2)$ that means that we have $y_1\in(\powf p_1)^\dagger\comp(\powf s)^\dagger\comp\sigma\comp s\join(\powf p_1)^\dagger\comp\sigma(x_1,x_2)$. - % - % Now, we prove $(\powf p_1)^\dagger\comp(\powf s)^\dagger\comp\sigma\comp s\join(\powf p_1)^\dagger\comp\sigma(x_1,x_2)\subseteq(\powf p_1)^\dagger\comp((\powf s)^\dagger\comp\sigma\comp s\join\sigma)(x_1,x_2)$. Assuming $y_1\in(\powf p_1)^\dagger\comp(\powf s)^\dagger\comp\sigma\comp s\join(\powf p_1)^\dagger\comp\sigma(x_1,x_2)$ then we have: - % \begin{itemize} - % \item $y_1\in(\powf p_1)^\dagger\comp(\powf s)^\dagger\comp\sigma\comp s(x_1,x_2)$: Then there exists $y_2$ such that $(y_1,y_2)\in(\powf s)^\dagger\comp\sigma\comp s(x_1,x_2)$. So, $(y_1,y_2)\in(\powf s)^\dagger\comp\sigma\comp s\join\sigma(x_1,x_2)$, thus $y_1\in(\powf p_1)^\dagger\comp((\powf s)^\dagger\comp\sigma\comp s\join\sigma)(x_1,x_2)$. - % \item $y_1\in(\powf p_1)^\dagger\comp\sigma(x_1,x_2)$: Then there exists $y_2$ such that $(y_1,y_2)\in\sigma(x_1,x_2)$. So, $(y_1,y_2)\in(\powf s)^\dagger\comp\sigma\comp s\join\sigma(x_1,x_2)$, thus $y_1\in(\powf p_1)^\dagger\comp((\powf s)^\dagger\comp\sigma\comp s\join\sigma)(x_1,x_2)$. - % \end{itemize} \qed - % \todo{Rewrite the proof according to the statement!} -\end{proof} -%\begin{rem} -% Assuming that $\sigma_1$ and $\sigma_2$ are witnesses that $R$ is an Aczel-Mendler simulation from a coalgebra $(X,\alpha)$ to another coalgebra $(Y,\beta)$, then $\sigma_1\meet\sigma_2$ is not necessarily a witness that $R$ is an Aczel-Mendler simulation. -%\end{rem} -Since $\subseteq$ is a liftable order (\autoref{def:liftable-ord}), we have the following lemma. The liftability is not used in the proof, but if $\subseteq$ was not liftable, perhaps we could not prove this. -\begin{prop}\label{prop:alph-prod} - Assuming that $R$ is a relation, and $\sigma\c R\to\powf R$ is a witness for $R$ to be an AM simulation, then there exists $\sigma'\c R\to\powf R$ that is another witness for $R$ to be an AM simulation, such that $\powf p_1\comp\sigma'=\alpha\comp p_1$. -\end{prop} -\begin{proof} - We define $\sigma'(x_1,x_2)=\{(x'_1,x'_2)\mid x'_1\in\alpha\comp p_1(x_1,x_2)\;,\;(x'_1,x'_2)\in\sigma(x_1,x_2)\}$. We have $\sigma'\subseteq\sigma$ that gives $\powf p_2\comp\sigma'\subseteq\powf p_2\comp\sigma$. Additionally, we have $\powf p_1\comp\sigma'\subseteq\alpha\comp p_1$. - Furthermore, if $x'_1\in\alpha\comp p_1(x_1,x_2)$, since $\alpha\comp p_1\subseteq \powf p_1\comp\sigma$ then $x'_1\in\powf p_1\comp\sigma(x_1,x_2)$. Let $(x'_1,x'_2)\in\sigma(x_1,x_2)$. By definition of $\sigma'$, we have $(x'_1,x'_2)\in\sigma'(x_1,x_2)$, so $x'_1\in\powf p_1\comp\sigma'(x_1,x_2)$ that means $\alpha\comp p_1\subseteq \powf p_1\comp\sigma'$ as well. So, $\sigma'$ is another witness for $R$ to be an AM simulation, and we have $\alpha\comp p_1=\powf p_1\comp\sigma'$. - \qed -\end{proof} -An abstract version of the above proposition is given by Dubut that is the following: -\begin{prop}\label{prop:alph-prod-dubut} - Assuming that $R$ is a relation, and $\sigma\c R\to FR$ is a witness for $R$ to be an AM-simulation, then there exists $\sigma'\c R\to FR$ that is another witness for $R$ to be an AM-simulation, such that $Fp_1\comp\sigma'=\alpha\comp p_1$. -\end{prop}\qed -Now, we prove our main statement. -\begin{prop}\label{prop:sym-rel-bisim} - Assuming that $R$ is a symmetric relation, and $\sigma\c R\to \powf R$ is a witness for $R$ to be a simulation, for which $\powf p_1\comp\sigma=\alpha\comp p_1$, then the following morphism is a witness for $R$ to be a bisimulation: - \begin{gather*} - \sigma\join(\powf s\comp\sigma\comp s) - \end{gather*} -\end{prop} -\begin{proof} - For every $(x_1,x_2)\in R$ by~\autoref{lem:proj-dist-set} and~\autoref{lem:sim-opsim-inc}.\ref{item:sim-opsim-inc:I} we have - \begin{gather*} - \powf p_1\comp(\sigma\join(\powf s\comp\sigma\comp s))(x_1,x_2)= - \powf p_1\comp\sigma(x_1,x_2). - \end{gather*} -% and by~\autoref{prop:alph-prod}, - Recall that $\powf p_1\comp\sigma(x_1,x_2)=\alpha(x_1)$. By~\autoref{lem:proj-dist-set} and~\autoref{lem:sim-opsim-inc}.\ref{item:sim-opsim-inc:II} we have - \begin{gather*} - \powf p_2\comp(\sigma\join(\powf s\comp\sigma\comp s))(x_1,x_2)= - \powf p_2\comp(\powf s\comp\sigma\comp s)(x_1,x_2). - \end{gather*} - Since $\powf p_1\comp\sigma=\alpha\comp p_1$ by precomposing $s$ to the both sides of the equation we get $\powf p_2\comp(\powf s\comp\sigma\comp s)=\alpha\comp p_2$. So, $\sigma\join(\powf s\comp\sigma\comp s)$ is a witness for $R$ to be an AM bisimulation.\qed -\end{proof} -\begin{cor} - Considering~\autoref{prop:alph-prod}, assuming that $R$ is a symmetric relation and it is an AM simulation, then $R$ is an AM bisimulation as well. -\end{cor} -Now, we make the proof more abstract. We prove the statement for set-functors of the form $\powf F$, where $F$ is an arbitrary set-functor, and $\powf$ is the powerset functor. - -\subsection{PF} -\begin{lemma}\label{lem:proj-dist-set-abs} +%\begin{lemma}\label{lem:proj-dist-set} +% For relations $R_1$ and $R_2$ the following equation holds: +% \begin{gather*} +% %(\powf p_i)^\dagger(R_1\cup R_2)=(\powf p_i)^\dagger(R_1)\cup(\powf p_i)^\dagger(R_2) +% \powf p_i(R_1\cup R_2)=\powf p_i(R_1)\cup(\powf p_i)(R_2) +% \end{gather*} +%\end{lemma} +%\begin{proof} +% We prove the lemma for the case that $i=1$. The proof is the same for $i=2$. +% Assuming $x_1\in\powf p_1(R_1\cup R_2)$ then exists $x_2$ that $(x_1,x_2)\in R_1\cup R_2$, thus either $(x_1,x_2)\in R_1$ or $(x_1,x_2)\in R_2$, so we have $x_1\in\powf p_1R_1$ or $x_1\in\powf p_1R_2$, respectively. So, we have $x_1\in \powf p_1R_1\cup\powf p_1R_2$. +% +% Now, assuming that $x_1\in\powf p_1R_1\cup\powf p_1R_2$ either $x_1\in\powf p_1R_1$ or $x_1\in\powf p_1R_2$. Without loss of generality, we can assume $x_1\in\powf p_1R_j$, where $j\in\{1,2\}$. +% Then there exists $x_2$ that $(x_1,x_2)\in R_j$, then we have $(x_1,x_2)\in R_1\cup R_2$ that gives $x_1\in\powf p_1(R_1\cup R_2)$.\qed +% % We prove the lemma for the case that $i=1$. The proof is the same for $i=2$. +% % +% % First, we prove $(\powf p_1)^\dagger\comp((\powf s)^\dagger\comp\sigma\comp s\join\sigma)(x_1,x_2)\subseteq(\powf p_1)^\dagger\comp(\powf s)^\dagger\comp\sigma\comp s\join(\powf p_1)^\dagger\comp\sigma(x_1,x_2)$. +% % Assuming $y_1\in(\powf p_1)^\dagger\comp((\powf s)^\dagger\comp\sigma\comp s\join\sigma)(x_1,x_2)$ then exists $y_2$ that we have either $(y_1,y_2)\in(\powf s)^\dagger\comp\sigma\comp s(x_1,x_2)$ or $(y_1,y_2)\in\sigma(x_1,x_2)$. So, we have either $y_1\in(\powf p_1)^\dagger\comp(\powf s)^\dagger\comp\sigma\comp s(x_1,x_2)$ or $y_1\in(\powf p_1)^\dagger\comp\sigma(x_1,x_2)$ that means that we have $y_1\in(\powf p_1)^\dagger\comp(\powf s)^\dagger\comp\sigma\comp s\join(\powf p_1)^\dagger\comp\sigma(x_1,x_2)$. +% % +% % Now, we prove $(\powf p_1)^\dagger\comp(\powf s)^\dagger\comp\sigma\comp s\join(\powf p_1)^\dagger\comp\sigma(x_1,x_2)\subseteq(\powf p_1)^\dagger\comp((\powf s)^\dagger\comp\sigma\comp s\join\sigma)(x_1,x_2)$. Assuming $y_1\in(\powf p_1)^\dagger\comp(\powf s)^\dagger\comp\sigma\comp s\join(\powf p_1)^\dagger\comp\sigma(x_1,x_2)$ then we have: +% % \begin{itemize} +% % \item $y_1\in(\powf p_1)^\dagger\comp(\powf s)^\dagger\comp\sigma\comp s(x_1,x_2)$: Then there exists $y_2$ such that $(y_1,y_2)\in(\powf s)^\dagger\comp\sigma\comp s(x_1,x_2)$. So, $(y_1,y_2)\in(\powf s)^\dagger\comp\sigma\comp s\join\sigma(x_1,x_2)$, thus $y_1\in(\powf p_1)^\dagger\comp((\powf s)^\dagger\comp\sigma\comp s\join\sigma)(x_1,x_2)$. +% % \item $y_1\in(\powf p_1)^\dagger\comp\sigma(x_1,x_2)$: Then there exists $y_2$ such that $(y_1,y_2)\in\sigma(x_1,x_2)$. So, $(y_1,y_2)\in(\powf s)^\dagger\comp\sigma\comp s\join\sigma(x_1,x_2)$, thus $y_1\in(\powf p_1)^\dagger\comp((\powf s)^\dagger\comp\sigma\comp s\join\sigma)(x_1,x_2)$. +% % \end{itemize} \qed +% % \todo{Rewrite the proof according to the statement!} +%\end{proof} +%%\begin{rem} +%% Assuming that $\sigma_1$ and $\sigma_2$ are witnesses that $R$ is an Aczel-Mendler simulation from a coalgebra $(X,\alpha)$ to another coalgebra $(Y,\beta)$, then $\sigma_1\meet\sigma_2$ is not necessarily a witness that $R$ is an Aczel-Mendler simulation. +%%\end{rem} +%Since $\subseteq$ is a liftable order (\autoref{def:liftable-ord}), we have the following lemma. The liftability is not used in the proof, but if $\subseteq$ was not liftable, perhaps we could not prove this. +%\begin{prop}\label{prop:alph-prod} +% Assuming that $R$ is a relation, and $\sigma\c R\to\powf R$ is a witness for $R$ to be an AM simulation, then there exists $\sigma'\c R\to\powf R$ that is another witness for $R$ to be an AM simulation, such that $\powf p_1\comp\sigma'=\alpha\comp p_1$. +%\end{prop} +%\begin{proof} +% We define $\sigma'(x_1,x_2)=\{(x'_1,x'_2)\mid x'_1\in\alpha\comp p_1(x_1,x_2)\;,\;(x'_1,x'_2)\in\sigma(x_1,x_2)\}$. We have $\sigma'\subseteq\sigma$ that gives $\powf p_2\comp\sigma'\subseteq\powf p_2\comp\sigma$. Additionally, we have $\powf p_1\comp\sigma'\subseteq\alpha\comp p_1$. +% Furthermore, if $x'_1\in\alpha\comp p_1(x_1,x_2)$, since $\alpha\comp p_1\subseteq \powf p_1\comp\sigma$ then $x'_1\in\powf p_1\comp\sigma(x_1,x_2)$. Let $(x'_1,x'_2)\in\sigma(x_1,x_2)$. By definition of $\sigma'$, we have $(x'_1,x'_2)\in\sigma'(x_1,x_2)$, so $x'_1\in\powf p_1\comp\sigma'(x_1,x_2)$ that means $\alpha\comp p_1\subseteq \powf p_1\comp\sigma'$ as well. So, $\sigma'$ is another witness for $R$ to be an AM simulation, and we have $\alpha\comp p_1=\powf p_1\comp\sigma'$. +% \qed +%\end{proof} +%A more abstract version of the following proposition is given by Dubut: +%\begin{prop}\label{prop:alph-prod-dubut} +% Assuming that $R$ is a relation, and $\sigma\c R\to FR$ is a witness for $R$ to be an AM-simulation, then there exists $\sigma'\c R\to FR$ that is another witness for $R$ to be an AM-simulation, such that $Fp_1\comp\sigma'=\alpha\comp p_1$. +%\end{prop}\qed +%Now, we prove our main statement. +%\begin{prop}\label{prop:sym-rel-bisim} +% Assuming that $R$ is a symmetric relation, and $\sigma\c R\to \powf R$ is a witness for $R$ to be a simulation, for which $\powf p_1\comp\sigma=\alpha\comp p_1$, then the following morphism is a witness for $R$ to be a bisimulation: +% \begin{gather*} +% \sigma\join(\powf s\comp\sigma\comp s) +% \end{gather*} +%\end{prop} +%\begin{proof} +% For every $(x_1,x_2)\in R$ by~\autoref{lem:proj-dist-set} and~\autoref{lem:sim-opsim-inc}.\ref{item:sim-opsim-inc:I} we have +% \begin{gather*} +% \powf p_1\comp(\sigma\join(\powf s\comp\sigma\comp s))(x_1,x_2)= +% \powf p_1\comp\sigma(x_1,x_2). +% \end{gather*} +%% and by~\autoref{prop:alph-prod}, +% Recall that $\powf p_1\comp\sigma(x_1,x_2)=\alpha(x_1)$. By~\autoref{lem:proj-dist-set} and~\autoref{lem:sim-opsim-inc}.\ref{item:sim-opsim-inc:II} we have +% \begin{gather*} +% \powf p_2\comp(\sigma\join(\powf s\comp\sigma\comp s))(x_1,x_2)= +% \powf p_2\comp(\powf s\comp\sigma\comp s)(x_1,x_2). +% \end{gather*} +% Since $\powf p_1\comp\sigma=\alpha\comp p_1$ by precomposing $s$ to the both sides of the equation we get $\powf p_2\comp(\powf s\comp\sigma\comp s)=\alpha\comp p_2$. So, $\sigma\join(\powf s\comp\sigma\comp s)$ is a witness for $R$ to be an AM bisimulation.\qed +%\end{proof} +%\begin{cor} +% Considering~\autoref{prop:alph-prod}, assuming that $R$ is a symmetric relation and it is an AM simulation, then $R$ is an AM bisimulation as well. +%\end{cor} +%Now, we make the proof more abstract. We prove the statement for set-functors of the form $\powf F$, where $F$ is an arbitrary set-functor, and $\powf$ is the powerset functor. +We prove the stronger statement for $\powf$, where $F$ is an arbitrary endofunctor on $\Set$. The ordering that we consider on this functor is the set inclusion. We recall the following lemma: +\begin{lemma}\label{lem:func-dist-set} For sets $X$ and $Y$ in $\powf A$, and a function $f\c A\to B$ the following equation holds: \begin{gather*} %(\powf p_i)^\dagger(R_1\cup R_2)=(\powf p_i)^\dagger(R_1)\cup(\powf p_i)^\dagger(R_2) - \powf f(X\cup Y)=\powf f(X)\cup \powf f(Y) + \powf f(X_1\cup X_2)=\powf f(X_1)\cup \powf f(X_2) \end{gather*} \end{lemma} \begin{proof} @@ -2509,7 +2513,37 @@ Now, we make the proof more abstract. We prove the statement for set-functors of % \end{itemize} \qed % \todo{Rewrite the proof according to the statement!} \end{proof} -\todo{Finish this proof. With this, you can give the proof for $\powf F$. After you finished this, you can remove the previous sections.} +The following statement is proven by Dubut: +\begin{prop}\label{prop:alph-prod-dubut-pf} + Assuming that $R$ is a relation, and $\sigma\c R\to FR$ is a witness for $R$ to be an AM-simulation, then there exists $\sigma'\c R\to FR$ that is another witness for $R$ to be an AM-simulation, such that $Fp_1\comp\sigma'=\alpha\comp p_1$. +\end{prop}\qed +For arbitrary sets $X$ and $Y$, and functions $f,g\in\Hom(X,\powf FY)$, we define $f\join g$ as follows: +\begin{gather*} + (f\join g)(x)=f(x)\cup g(x) +\end{gather*} +\begin{prop}\label{prop:sym-rel-bisim-pf} + Assuming that $R$ is a symmetric relation, and $\sigma\c R\to \powf FR$ is a witness for $R$ to be an AM-simulation, then the following morphism is a witness for $R$ to be an AM-bisimulation: + \begin{gather*} + \sigma\join(\powf Fs\comp\sigma\comp s) + \end{gather*} +\end{prop} +\begin{proof} + For every $(x_1,x_2)\in R$ by~\autoref{lem:func-dist-set} and~\autoref{lem:sim-opsim-inc}.\ref{item:sim-opsim-inc:I} we have + \begin{gather*} + \powf Fp_1\comp(\sigma\join(\powf Fs\comp\sigma\comp s))(x_1,x_2)= + \powf Fp_1\comp\sigma(x_1,x_2). + \end{gather*} + % and by~\autoref{prop:alph-prod}, + Recall that by~\autoref{prop:lift-gen-func}, set inclusion is a liftable ordering, so by~\autoref{prop:alph-prod-dubut-pf}, we have $\powf Fp_1\comp\sigma(x_1,x_2)=\alpha(x_1)$. By~\autoref{lem:func-dist-set} and~\autoref{lem:sim-opsim-inc}.\ref{item:sim-opsim-inc:II} we have + \begin{gather*} + \powf Fp_2\comp(\sigma\join(\powf Fs\comp\sigma\comp s))(x_1,x_2)= + \powf Fp_2\comp(\powf Fs\comp\sigma\comp s)(x_1,x_2). + \end{gather*} + Since $\powf Fp_1\comp\sigma=\alpha\comp p_1$ by precomposing $s$ to the both sides of the equation we get $\powf Fp_2\comp(\powf Fs\comp\sigma\comp s)=\alpha\comp p_2$. So, $\sigma\join(\powf Fs\comp\sigma\comp s)$ is a witness for $R$ to be an AM bisimulation.\qed +\end{proof} +\begin{cor} + Assuming that $R$ is a symmetric relation and it is an AM-simulation on a $\powf F$ coalgebra, then $R$ is an AM-bisimulation as well. +\end{cor} \subsection{Maybe Functor} We prove that symmetric simulation is a bisimulation for the case that $FX=X+1$. First, we prove it for $\Set$.\\