psuedomerge: initial version

[topbloke-formulae.git] / pseudomerge.tex

diff --git a/pseudomerge.tex b/pseudomerge.tex
new file mode 100644 (file)
index 0000000..1e9422c
--- /dev/null
+++ b/pseudomerge.tex
@@ -0,0 +1,89 @@
+\section{Pseudo-merge}
+
+Given $L$ and some other commits $\set R$, generate a
+`fake merge': i.e., a commit which is a descendant of $L$ and $\set R$
+but whose contents are exactly those of $L$.
+
+\gathbegin
+ C \hasparents \{ L \} \cup \set R
+\gathnext
+ \patchof{C} = \patchof{L}
+\gathnext
+ D \isin C \equiv D \isin L \lor D = C
+\end{gather}
+
+\subsection{Conditions}
+
+\[ \eqn{ Base Only }{
+ \patchof{L} \neq \py
+}\]
+
+\[ \eqn{ Unique Tips }{
+ C \haspatch \p \implies
+  \bigexists_T
+    \pendsof{C}{\py} = \{ T \}
+}\]
+
+\[ \eqn{ Foreign Unaffected }{
+ \bigforall_{ D \text{ s.t. } \patchof{D} = \bot }
+  \left[ \bigexists_{A \in \set A} D \le A \right]
+   \implies
+  D \le L
+}\]
+ TODO THAT IS IMPOSSIBLE TO CALCULATE
+
+\subsection{Lemma: Foreign Identical}
+
+$\patchof{D} = \bot \implies \big[ D \le C \equiv D \le L \big]$.
+
+\proof{
+If $D \le L$, trivially $D \le C$; so conversely
+$D \not\le C \implies D \not\le L$.  
+Whereas if $D \le C$, either $D \le L$ or
+$\exists{A \in \set A} D \le A$ (since $D \neq C$),
+in which case by Foreign Unaffected $D \le L$.
+}
+
+\subsection{No Replay}
+
+Ingredients Prevent Replay applies:
+$A = L$ always satisfies the $\exists$.  $\qed$
+
+\subsection{Unique Base}
+
+Not applicable, by Base Only.
+
+\subsection{Tip Contents}
+
+Not applicable, by Base Only.
+
+\subsection{Base Acyclic}
+
+Relevant only if $L \in \pn$.  For $D = C$, $D \in \pn$; OK.
+For $D \neq C$, OK by Base Acyclic for $L$. $\qed$
+
+\subsection{Coherence and Patch Inclusion}
+
+$$
+\begin{cases}
+  L \haspatch    \p : & C \haspatch    \p \\
+  L \nothaspatch \p : & C \nothaspatch \p
+\end{cases}
+$$
+
+\proof{
+Consider some $D \in \py$.  $D \neq C$ by Base Only.
+So $C \has \p \equiv L \has \p$.
+}
+
+\subsection{Unique Tips}
+
+Explicitly dealt with by our Unique Tips condition.
+
+\subsection{Foreign Inclusion}
+
+True by Foreign Identical, and Foreign Inclusion of $L$.
+
+\subsection{Foreign Contents}
+
+Not applicable.