merge complex done

[topbloke-formulae.git] / article.tex

diff --git a/article.tex b/article.tex
index 4c5f6751682c83a13e478fdb11d64496abd1bd22..cbd56840b63d5579073f30786bcac5ed76fa1773 100644 (file)
--- a/article.tex
+++ b/article.tex
@@ -10,6 +10,8 @@
 
 \renewcommand{\ge}{\geqslant}
 \renewcommand{\le}{\leqslant}
 
 \renewcommand{\ge}{\geqslant}
 \renewcommand{\le}{\leqslant}

+\newcommand{\nge}{\ngeqslant}
+\newcommand{\nle}{\nleqslant}

 
 \newcommand{\has}{\sqsupseteq}
 \newcommand{\isin}{\sqsubseteq}
 
 \newcommand{\has}{\sqsupseteq}
 \newcommand{\isin}{\sqsubseteq}


@@ -53,7 +55,8 @@
 \newcommand{\pancsof}[2]{\pancs ( #1 , #2 ) }
 \newcommand{\pendsof}[2]{\pends ( #1 , #2 ) }
 
 \newcommand{\pancsof}[2]{\pancs ( #1 , #2 ) }
 \newcommand{\pendsof}[2]{\pends ( #1 , #2 ) }
 

-\newcommand{\merge}[4]{{\mathcal M}(#1,#2,#3,#4)}
+\newcommand{\merge}{{\mathcal M}}
+\newcommand{\mergeof}[4]{\merge(#1,#2,#3,#4)}

 %\newcommand{\merge}[4]{{#2 {{\frac{ #1 }{ #3 } #4}}}}
 
 \newcommand{\patch}{{\mathcal P}}
 %\newcommand{\merge}[4]{{#2 {{\frac{ #1 }{ #3 } #4}}}}
 
 \newcommand{\patch}{{\mathcal P}}


@@ -78,7 +81,8 @@
 \newcommand{\Largenexists}{\mathop{\hbox{\Large$\nexists$}}}
 
 \newcommand{\qed}{\square}
 \newcommand{\Largenexists}{\mathop{\hbox{\Large$\nexists$}}}
 
 \newcommand{\qed}{\square}

-\newcommand{\proof}[1]{{\it Proof.} #1 $\qed$}
+\newcommand{\proofstarts}{{\it Proof:}}
+\newcommand{\proof}[1]{\proofstarts #1 $\qed$}

 
 \newcommand{\gathbegin}{\begin{gather} \tag*{}}
 \newcommand{\gathnext}{\\ \tag*{}}
 
 \newcommand{\gathbegin}{\begin{gather} \tag*{}}
 \newcommand{\gathnext}{\\ \tag*{}}


@@ -152,7 +156,7 @@ 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.
 
 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} $ ]
+\item[ $\displaystyle \mergeof{C}{L}{M}{R} $ ]

 The contents of a git merge result:
 
 $\displaystyle D \isin C \equiv
 The contents of a git merge result:
 
 $\displaystyle D \isin C \equiv


@@ -259,15 +263,15 @@ XXX proof TBD.
 
 \subsection{No Replay for Merge Results}
 
 
 \subsection{No Replay for Merge Results}
 

-If we are constructing $C$, given
+If we are constructing $C$, with,

 \gathbegin
 \gathbegin

-  \merge{C}{L}{M}{R}
+  \mergeof{C}{L}{M}{R}

 \gathnext
   L \le C
 \gathnext
   R \le C
 \end{gather}
 \gathnext
   L \le C
 \gathnext
   R \le C
 \end{gather}

-No Replay is preserved.  {\it Proof:}
+No Replay is preserved.  \proofstarts

 
 \subsubsection{For $D=C$:} $D \isin C, D \le C$.  OK.
 
 
 \subsubsection{For $D=C$:} $D \isin C, D \le C$.  OK.
 


@@ -397,7 +401,7 @@ Used for removing a branch dependency.
 \gathnext
  \patchof{C} = \patchof{L}
 \gathnext
 \gathnext
  \patchof{C} = \patchof{L}
 \gathnext

- \merge{C}{L}{R^+}{R^-}
+ \mergeof{C}{L}{R^+}{R^-}

 \end{gather}
 
 \subsection{Conditions}
 \end{gather}
 
 \subsection{Conditions}


@@ -408,10 +412,9 @@ Used for removing a branch dependency.
 \[ \eqn{ Currently Included }{
  L \haspatch \pry
 }\]
 \[ \eqn{ Currently Included }{
  L \haspatch \pry
 }\]

-
-\subsection{Desired Contents}
-
-xxx need to prove $D \isin C \equiv D \not\in \pry \land D \isin L$.
+\[ \eqn{ Not Self }{
+ L \not\in \{ R^+ \}
+}\]

 
 \subsection{No Replay}
 
 
 \subsection{No Replay}
 


@@ -419,12 +422,48 @@ 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$
 
 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 \notin \pry \land D \isin L ] \lor D = C \]
+\proofstarts
+
+\subsubsection{For $D = C$:}
+
+Trivially $D \isin C$.  OK.
+
+\subsubsection{For $D \neq C, D \not\le L$:}
+
+By No Replay $D \not\isin L$.  Also $D \not\le R^-$ hence
+$D \not\isin R^-$.  Thus $D \not\isin C$.  OK.
+
+\subsubsection{For $D \neq C, D \le L, D \in \pry$:}
+
+By Currently Included, $D \isin L$.
+
+By Tip Self Inpatch, $D \isin R^+ \equiv D \le R^+$, but by
+by Unique Tip, $D \le R^+ \equiv D \le L$.  
+So $D \isin R^+$.
+
+By Base Acyclic, $D \not\isin R^-$.
+
+Apply $\merge$: $D \not\isin C$.  OK.
+
+\subsubsection{For $D \neq C, D \le L, D \notin \pry$:}
+
+By Tip Contents for $R^+$, $D \isin R^+ \equiv D \isin R^-$.
+
+Apply $\merge$: $D \isin C \equiv D \isin L$.  OK.
+
+$\qed$
+

 \subsection{Unique Base}
 
 Need to consider only $C \in \py$, ie $L \in \py$.
 
 xxx tbd
 
 \subsection{Unique Base}
 
 Need to consider only $C \in \py$, ie $L \in \py$.
 
 xxx tbd
 

+xxx need to finish anticommit
+

 \section{Merge}
 
 Merge commits $L$ and $R$ using merge base $M$ ($M < L, M < R$):
 \section{Merge}
 
 Merge commits $L$ and $R$ using merge base $M$ ($M < L, M < R$):


@@ -433,8 +472,9 @@ Merge commits $L$ and $R$ using merge base $M$ ($M < L, M < R$):
 \gathnext
  \patchof{C} = \patchof{L}
 \gathnext
 \gathnext
  \patchof{C} = \patchof{L}
 \gathnext

- \merge{C}{L}{M}{R}
+ \mergeof{C}{L}{M}{R}

 \end{gather}
 \end{gather}

+We will occasionally use $X,Y$ s.t. $\{X,Y\} = \{L,R\}$.

 
 \subsection{Conditions}
 
 
 \subsection{Conditions}
 


@@ -448,6 +488,21 @@ Merge commits $L$ and $R$ using merge base $M$ ($M < L, M < R$):
       \text{otherwise} : & \false
    \end{cases}
 }\]
       \text{otherwise} : & \false
    \end{cases}
 }\]

+\[ \eqn{ Removal Merge Ends }{
+    X \not\haspatch \p \land
+    Y \haspatch \p \land
+    M \haspatch \p
+  \implies
+    \pendsof{Y}{\py} = \pendsof{M}{\py}
+}\]
+\[ \eqn{ Addition Merge Ends }{
+    X \not\haspatch \p \land
+    Y \haspatch \p \land
+    M \nothaspatch \p
+   \implies \left[
+    \bigforall_{E \in \pendsof{X}{\py}} E \le Y
+   \right]
+}\]

 
 \subsection{No Replay}
 
 
 \subsection{No Replay}
 


@@ -487,4 +542,78 @@ That is, $\baseof{C} = R$.
 
 $\qed$
 
 
 $\qed$
 

+\subsection{Coherence and patch inclusion}
+
+Need to determine $C \haspatch \p$ based on $L,M,R \haspatch \p$.
+This involves considering $D \in \py$.  
+
+\subsubsection{For $L \nothaspatch \p, R \nothaspatch \p$:}
+$D \not\isin L \land D \not\isin R$.  $C \not\in \py$ (otherwise $L
+\in \py$ ie $L \haspatch \p$ by Tip Self Inpatch).  So $D \neq C$.
+Applying $\merge$ gives $D \not\isin C$ i.e. $C \nothaspatch \p$.
+
+\subsubsection{For $L \haspatch \p, R \haspatch \p$:}
+$D \isin L \equiv D \le L$ and $D \isin R \equiv D \le R$.
+(Likewise $D \isin X \equiv D \le X$ and $D \isin Y \equiv D \le Y$.)
+
+Consider $D = C$: $D \isin C$, $D \le C$, OK for $C \haspatch \p$.
+
+For $D \neq C$: $D \le C \equiv D \le L \lor D \le R
+ \equiv D \isin L \lor D \isin R$.  
+(Likewise $D \le C \equiv D \le X \lor D \le Y$.)
+
+Consider $D \neq C, D \isin X \land D \isin Y$:
+By $\merge$, $D \isin C$.  Also $D \le X$ 
+so $D \le C$.  OK for $C \haspatch \p$.
+
+Consider $D \neq C, D \not\isin X \land D \not\isin Y$:
+By $\merge$, $D \not\isin C$.  
+And $D \not\le X \land D \not\le Y$ so $D \not\le C$.  
+OK for $C \haspatch \p$.
+
+Remaining case, wlog, is $D \not\isin X \land D \isin Y$.
+$D \not\le X$ so $D \not\le M$ so $D \not\isin M$.  
+Thus by $\merge$, $D \isin C$.  And $D \le Y$ so $D \le C$.
+OK for $C \haspatch \p$.
+
+So indeed $L \haspatch \p \land R \haspatch \p \implies C \haspatch \p$.
+
+\subsubsection{For (wlog) $X \not\haspatch \p, Y \haspatch \p$:}
+
+$C \haspatch \p \equiv M \nothaspatch \p$.
+
+\proofstarts
+
+One of the Merge Ends conditions applies.  
+Recall that we are considering $D \in \py$.
+$D \isin Y \equiv D \le Y$.  $D \not\isin X$.
+We will show for each of
+various cases that $D \isin C \equiv M \nothaspatch \p \land D \le C$
+(which suffices by definition of $\haspatch$ and $\nothaspatch$).
+
+Consider $D = C$:  Thus $C \in \py, L \in \py$, and by Tip
+Self Inpatch $L \haspatch \p$, so $L=Y, R=X$.  By Tip Merge,
+$M=\baseof{L}$.  So by Base Acyclic $D \not\isin M$, i.e.
+$M \nothaspatch \p$.  And indeed $D \isin C$ and $D \le C$.  OK.
+
+Consider $D \neq C, M \nothaspatch P, D \isin Y$:
+$D \le Y$ so $D \le C$.  
+$D \not\isin M$ so by $\merge$, $D \isin C$.  OK.
+
+Consider $D \neq C, M \nothaspatch P, D \not\isin Y$:
+$D \not\le Y$.  If $D \le X$ then
+$D \in \pancsof{X}{\py}$, so by Addition Merge Ends and 
+Transitive Ancestors $D \le Y$ --- a contradiction, so $D \not\le X$.
+Thus $D \not\le C$.  By $\merge$, $D \not\isin C$.  OK.
+
+Consider $D \neq C, M \haspatch P, D \isin Y$:
+$D \le Y$ so $D \in \pancsof{Y}{\py}$ so by Removal Merge Ends
+and Transitive Ancestors $D \in \pancsof{M}{\py}$ so $D \le M$.
+Thus $D \isin M$.  By $\merge$, $D \not\isin C$.  OK.
+
+Consider $D \neq C, M \haspatch P, D \not\isin Y$:
+By $\merge$, $D \not\isin C$.  OK.
+
+$\qed$
+

 \end{document}
 \end{document}