provide \nge and \nle (which \not uses)

[topbloke-formulae.git] / article.tex

diff --git a/article.tex b/article.tex
index 01800f96132a69fb7a89ab4e9e6ab9d0a82e9519..20ab3613b294a18dd8bf09d8f49e4f7bc9ab8700 100644 (file)
--- a/article.tex
+++ b/article.tex
@@ -10,6 +10,8 @@
 
 \renewcommand{\ge}{\geqslant}
 \renewcommand{\le}{\leqslant}
+\newcommand{\nge}{\ngeqslant}
+\newcommand{\nle}{\nleqslant}
 
 \newcommand{\has}{\sqsupseteq}
 \newcommand{\isin}{\sqsubseteq}
@@ -53,8 +55,14 @@
 \newcommand{\pancsof}[2]{\pancs ( #1 , #2 ) }
 \newcommand{\pendsof}[2]{\pends ( #1 , #2 ) }
 
-\newcommand{\patchof}[1]{{\mathcal P} ( #1 ) }
-\newcommand{\baseof}[1]{{\mathcal B} ( #1 ) }
+\newcommand{\merge}[4]{{\mathcal M}(#1,#2,#3,#4)}
+%\newcommand{\merge}[4]{{#2 {{\frac{ #1 }{ #3 } #4}}}}
+
+\newcommand{\patch}{{\mathcal P}}
+\newcommand{\base}{{\mathcal B}}
+
+\newcommand{\patchof}[1]{\patch ( #1 ) }
+\newcommand{\baseof}[1]{\base ( #1 ) }
 
 \newcommand{\eqn}[2]{ #2 \tag*{\mbox{\bf #1}} }
 \newcommand{\corrolary}[1]{ #1 \tag*{\mbox{\it Corrolary.}} }
@@ -146,6 +154,17 @@ patch is applied to a non-Topbloke branch and then bubbles back to
 the Topbloke patch itself, we hope that git's merge algorithm will
 DTRT or that the user will no longer care about the Topbloke patch.
 
+\item[ $\displaystyle \merge{C}{L}{M}{R} $ ]
+The contents of a git merge result:
+
+$\displaystyle D \isin C \equiv
+  \begin{cases}
+    (D \isin L \land D \isin R) \lor D = C : & \true \\
+    (D \not\isin L \land D \not\isin R) \land D \neq C : & \false \\
+    \text{otherwise} : & D \not\isin M
+  \end{cases}
+$ 
+
 \end{basedescript}
 \newpage
 \section{Invariants}
@@ -231,15 +250,46 @@ by the LHS.  And $A \le A''$.
 \[ \eqn{Calculation Of Ends:}{
   \bigforall_{C \hasparents \set A}
     \pendsof{C}{\set P} =
-       \Bigl\{ E \Big|
+       \left\{ E \Big|
            \Bigl[ \Largeexists_{A \in \set A} 
                        E \in \pendsof{A}{\set P} \Bigr] \land
            \Bigl[ \Largenexists_{B \in \set A} 
                        E \neq B \land E \le B \Bigr]
-       \Bigr\}
+       \right\}
 }\]
 XXX proof TBD.
 
+\subsection{No Replay for Merge Results}
+
+If we are constructing $C$, given
+\gathbegin
+  \merge{C}{L}{M}{R}
+\gathnext
+  L \le C
+\gathnext
+  R \le C
+\end{gather}
+No Replay is preserved.  {\it Proof:}
+
+\subsubsection{For $D=C$:} $D \isin C, D \le C$.  OK.
+
+\subsubsection{For $D \isin L \land D \isin R$:}
+$D \isin C$.  And $D \isin L \implies D \le L \implies D \le C$.  OK.
+
+\subsubsection{For $D \neq C \land D \not\isin L \land D \not\isin R$:}
+$D \not\isin C$.  OK.
+
+\subsubsection{For $D \neq C \land (D \isin L \equiv D \not\isin R)
+ \land D \not\isin M$:}
+$D \isin C$.  Also $D \isin L \lor D \isin R$ so $D \le L \lor D \le
+R$ so $D \le C$.  OK.
+
+\subsubsection{For $D \neq C \land (D \isin L \equiv D \not\isin R)
+ \land D \isin M$:}
+$D \not\isin C$.  OK.
+
+$\qed$
+
 \section{Commit annotation}
 
 We annotate each Topbloke commit $C$ with:
@@ -341,7 +391,7 @@ $D \isin C \equiv D \isin A \equiv D \le A \equiv D \le C$.  $\qed$
 \section{Anticommit}
 
 Given $L, R^+, R^-$ where
-$\patchof{R^+} = \pry, \patchof{R^-} = \prn$.  
+$R^+ \in \pry, R^- = \baseof{R^+}$.  
 Construct $C$ which has $\pr$ removed.
 Used for removing a branch dependency.
 \gathbegin
@@ -349,17 +399,48 @@ Used for removing a branch dependency.
 \gathnext
  \patchof{C} = \patchof{L}
 \gathnext
- D \isin C \equiv
-   \begin{cases}
-      R \in \py : & \baseof{R} \ge \baseof{L}
-              \land [\baseof{L} = M \lor \baseof{L} = \baseof{M}] \\
-      R \in \pn : & R \ge \baseof{L}
-              \land M = \baseof{L} \\
-      \text{otherwise} : & \false
-   \end{cases}
+ \merge{C}{L}{R^+}{R^-}
 \end{gather}
 
-xxx want to prove $D \isin C \equiv D \not\in pry \land D \isin L$.
+\subsection{Conditions}
+
+\[ \eqn{ Unique Tip }{
+ \pendsof{L}{\pry} = \{ R^+ \}
+}\]
+\[ \eqn{ Currently Included }{
+ L \haspatch \pry
+}\]
+\[ \eqn{ Not Self }{
+ L \not\in \{ R^+ \}
+}\]
+
+\subsection{No Replay}
+
+By Unique Tip, $R^+ \le L$.  By definition of $\base$, $R^- \le R^+$
+so $R^- \le L$.  So $R^+ \le C$ and $R^- \le C$ and No Replay for
+Merge Results applies. $\qed$
+
+\subsection{Desired Contents}
+
+\[ $D \isin C \equiv [ D \not\in \pry \land D \isin L$ ] \lor D = C \]
+{\it Proof.}
+
+\subsubsection{For $D = C$:}
+
+Trivially $D \isin C$.  OK.
+
+\subsubsection{For $D \not\le C$:}
+
+
+
+\subsubsection{For $D \in R^+$:}
+By Currently Included, 
+
+\subsection{Unique Base}
+
+Need to consider only $C \in \py$, ie $L \in \py$.
+
+xxx tbd
 
 \section{Merge}
 
@@ -369,12 +450,7 @@ Merge commits $L$ and $R$ using merge base $M$ ($M < L, M < R$):
 \gathnext
  \patchof{C} = \patchof{L}
 \gathnext
- D \isin C \equiv
-  \begin{cases}
-    (D \isin L \land D \isin R) \lor D = C : & \true \\
-    (D \not\isin L \land D \not\isin R) \land D \neq C : & \false \\
-    \text{otherwise} : & D \not\isin M
-  \end{cases}
+ \merge{C}{L}{M}{R}
 \end{gather}
 
 \subsection{Conditions}
@@ -392,28 +468,7 @@ Merge commits $L$ and $R$ using merge base $M$ ($M < L, M < R$):
 
 \subsection{No Replay}
 
-\subsubsection{For $D=C$:} $D \isin C, D \le C$.  OK.
-
-\subsubsection{For $D \isin L \land D \isin R$:}
-$D \isin C$.  And $D \isin L \implies D \le L \implies D \le C$.  OK.
-
-\subsubsection{For $D \neq C \land D \not\isin L \land D \not\isin R$:}
-$D \not\isin C$.  OK.
-
-\subsubsection{For $D \neq C \land D \not\isin L \land D \not\isin R$:}
-$D \not\isin C$.  OK.
-
-\subsubsection{For $D \neq C \land (D \isin L \equiv D \not\isin R)
- \land D \not\isin M$:}
-$D \isin C$.  Also $D \isin L \lor D \isin R$ so $D \le L \lor D \le
-R$ so $D \le C$.  OK.
-
-\subsubsection{For $D \neq C \land (D \isin L \equiv D \not\isin R)
- \land D \isin M$:}
-$D \not\isin C$.  Also $D \isin L \lor D \isin R$ so $D \le L \lor D \le
-R$ so $D \le C$.  OK.
-
-$\qed$
+See No Replay for Merge Results.
 
 \subsection{Unique Base}