rename exclusive tip contents corollary

[topbloke-formulae.git] / article.tex

diff --git a/article.tex b/article.tex
index b97350feb3e49447324ba7a794cdaf5b5ebe6425..01297a8fb0681c79d7ffc1933fe941f02f77adb5 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}}


@@ -62,8 +65,8 @@
 \newcommand{\patchof}[1]{\patch ( #1 ) }
 \newcommand{\baseof}[1]{\base ( #1 ) }
 
 \newcommand{\patchof}[1]{\patch ( #1 ) }
 \newcommand{\baseof}[1]{\base ( #1 ) }
 

+\newcommand{\eqntag}[2]{ #2 \tag*{\mbox{#1}} }

 \newcommand{\eqn}[2]{ #2 \tag*{\mbox{\bf #1}} }
 \newcommand{\eqn}[2]{ #2 \tag*{\mbox{\bf #1}} }

-\newcommand{\corrolary}[1]{ #1 \tag*{\mbox{\it Corrolary.}} }

 
 %\newcommand{\bigforall}{\mathop{\hbox{\huge$\forall$}}}
 \newcommand{\bigforall}{%
 
 %\newcommand{\bigforall}{\mathop{\hbox{\huge$\forall$}}}
 \newcommand{\bigforall}{%


@@ -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


@@ -202,7 +206,7 @@ Ie, the two limbs of the RHS of Tip Contents are mutually exclusive.
 Let $B = \baseof{C}$ in $D \isin \baseof{C}$.  Now $B \in \pn$.
 So by Base Acyclic $D \isin B \implies D \notin \py$.
 }
 Let $B = \baseof{C}$ in $D \isin \baseof{C}$.  Now $B \in \pn$.
 So by Base Acyclic $D \isin B \implies D \notin \py$.
 }

-\[ \corrolary{
+\[ \eqntag{{\it Corollary - equivalent to Tip Contents}}{

   \bigforall_{C \in \py} D \isin C \equiv
   \begin{cases}
     D \in \py : & D \le C \\
   \bigforall_{C \in \py} D \isin C \equiv
   \begin{cases}
     D \in \py : & D \le C \\


@@ -248,19 +252,26 @@ by the LHS.  And $A \le A''$.
 \[ \eqn{Calculation Of Ends:}{
   \bigforall_{C \hasparents \set A}
     \pendsof{C}{\set P} =
 \[ \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]
            \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}
 
 }\]
 XXX proof TBD.
 
 \subsection{No Replay for Merge Results}
 

-If we are constructing $C$ such that $\merge{C}{L}{M}{R}$, No Replay
-is preserved.  {\it Proof:}
+If we are constructing $C$, with,
+\gathbegin
+  \mergeof{C}{L}{M}{R}
+\gathnext
+  L \le C
+\gathnext
+  R \le C
+\end{gather}
+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.
 


@@ -270,9 +281,6 @@ $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 \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
 \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


@@ -280,8 +288,7 @@ R$ so $D \le C$.  OK.
 
 \subsubsection{For $D \neq C \land (D \isin L \equiv D \not\isin R)
  \land D \isin M$:}
 
 \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.
+$D \not\isin C$.  OK.

 
 $\qed$
 
 
 $\qed$
 


@@ -386,7 +393,7 @@ $D \isin C \equiv D \isin A \equiv D \le A \equiv D \le C$.  $\qed$
 \section{Anticommit}
 
 Given $L, R^+, R^-$ where
 \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
 Construct $C$ which has $\pr$ removed.
 Used for removing a branch dependency.
 \gathbegin


@@ -394,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}


@@ -402,16 +409,60 @@ Used for removing a branch dependency.
 \[ \eqn{ Unique Tip }{
  \pendsof{L}{\pry} = \{ R^+ \}
 }\]
 \[ \eqn{ Unique Tip }{
  \pendsof{L}{\pry} = \{ R^+ \}
 }\]

-\[ \eqn{ Correct Base }{
- \baseof{R^+} = R^-
-}\]

 \[ \eqn{ Currently Included }{
  L \haspatch \pry
 }\]
 \[ \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 \notin \pry \land D \isin L ] \lor D = C \]
+\proofstarts

 
 

+\subsubsection{For $D = C$:}

 
 

-xxx want to prove $D \isin C \equiv D \not\in \pry \land D \isin L$.
+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
+
+xxx need to finish anticommit

 
 \section{Merge}
 
 
 \section{Merge}
 


@@ -421,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}
 


@@ -436,10 +488,25 @@ 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{Merge Results}
+\subsection{No Replay}

 
 

-As above.
+See No Replay for Merge Results.

 
 \subsection{Unique Base}
 
 
 \subsection{Unique Base}
 


@@ -475,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}