(** %
\section{\label{sec:unnamed_patch_sequences}Unnamed Patch Sequences}
% *)
Module Export patch_sequences.

Require Import unnamed_patches.

(** %
\start{definition}{unnamed-patch-sequences}
We write the empty sequence of unnamed patches as $\nopatches$.

We compose unnamed patch sequences with juxtaposition.
\end{Idefinition}

\start{definition}{unnamed-patch-sequence-commute}
We extend $<->$ to work with combinations of patches and patch sequences
in the natural way:

Commuting a patch with a sequence:\\
$\begin{array}[t]{@{}l@{}}
 \pair{\unnamed{p}}{\epsilon} <-> \pair{\epsilon}{\unnamed{p}}\\
 \pair{\unnamed{p}}{\unnamed{q} \unnamed{\seq{r}}} <->
 \pair{\unnamed{q'} \unnamed{\seq{r}'}}{\unnamed{p'}}\\
    \quad \textrm{ if } \begin{array}[t]{@{}l@{}}
                        \pair{\unnamed{p}}{\unnamed{q}} <->
                        \pair{\unnamed{q'}}{\unnamed{p''}}\\
                        \pair{\unnamed{p''}}{\unnamed{\seq{r}}} <->
                        \pair{\unnamed{\seq{r}'}}{\unnamed{p'}}
                        \end{array}
 \end{array}$

Commuting a sequence with a patch:\\
$\begin{array}[t]{@{}l@{}}
 \pair{\epsilon}{\unnamed{p}} <-> \pair{\unnamed{p}}{\epsilon}\\
 \pair{\unnamed{\seq{p}} \unnamed{q}}{\unnamed{r}} <->
 \pair{\unnamed{r'}}{\unnamed{\seq{p}'} \unnamed{q'}}\\
    \quad \textrm{ if } \begin{array}[t]{@{}l@{}}
                        \pair{\unnamed{q}}{\unnamed{r}} <->
                        \pair{\unnamed{r''}}{\unnamed{q'}}\\
                        \pair{\unnamed{\seq{p}}}{\unnamed{r''}} <->
                        \pair{\unnamed{r'}}{\unnamed{\seq{p}'}}
                        \end{array}
 \end{array}$

Commuting a sequence with another sequence:\\
$\begin{array}[t]{@{}l@{}}
 \pair{\unnamed{\seq{p}}}{\epsilon} <-> \pair{\epsilon}{\unnamed{\seq{p}}}\\
 \pair{\epsilon}{\unnamed{\seq{p}}} <-> \pair{\unnamed{\seq{p}}}{\epsilon}\\
 \pair{\unnamed{\seq{p}} \unnamed{q}}{\unnamed{r} \unnamed{\seq{s}}} <->
 \pair{\unnamed{r''} \unnamed{\seq{s}''}}{\unnamed{\seq{p}''} \unnamed{q''}}\\
    \quad \textrm{ if }
        \begin{array}[t]{@{}l@{}}
        \pair{\unnamed{q}}{\unnamed{r}} <->
        \pair{\unnamed{r'}}{\unnamed{q'}}\\
        \pair{\unnamed{\seq{p}}}{\unnamed{r'}} <->
        \pair{\unnamed{r''}}{\unnamed{\seq{p}'}}\\
        \pair{\unnamed{q'}}{\unnamed{\seq{s}}} <->
        \pair{\unnamed{\seq{s}'}}{\unnamed{q''}}\\
        \pair{\unnamed{\seq{p}'}}{\unnamed{\seq{s}'}} <->
        \pair{\unnamed{\seq{s}''}}{\unnamed{\seq{p}''}}\\
        \end{array}
 \end{array}$

Note that the first two definitions are degenerate cases of the third.

In all cases, if the above rules don't apply the commute fails.
\end{Idefinition}

# XXX I don't think we need the whole hexagon here.
# Just pq commute, qr commute and pr commute implies pq still commute.
# \start{axiom}{unnamed-patch-commute-associates}
# $\begin{array}[t]{@{}r@{~}l@{}}
#  \multicolumn{2}{@{}l@{}}{
#  \forall p \in \patches, q \in \patches, r \in \patches,
#          p_q \in \patches, p_r \in \patches, p_{qr} \in \patches,
#          q_p \in \patches, q_r \in \patches, q_{pr} \in \patches,
#          r_p \in \patches, r_q \in \patches, r_{pq} \in \patches .}\\
#     &(\pair{q}{r}           <-> \pair{r_q}{q_r})   \wedge
#      (\pair{p}{q}           <-> \pair{q_p}{p_q}) \wedge
#      (\pair{p_q}{r}         <-> \pair{r_p}{p_{qr}})\\
#  <=>&(\pair{q_p}{r_p}       <-> \pair{r_{pq}}{q_{pr}}) \wedge
#      (\pair{q_{pr}}{p_{qr}} <-> \pair{p_r}{q_r}) \wedge
#      (\pair{r_{pq}}{p_r}    <-> \pair{p}{r_q})
#  \end{array}$
# \begin{Iexplanation}
# This is much clearer if we consider it in diagramatic form:
# \begin{igpic}{0}{3.6}{-0.8}{2.8}
#     \tlabelsep{4pt}
#     \pointdef{PQR}(0,0)
#     \pointdef{PRQ}(0,2)
#     \pointdef{RPQ}(1.8,2.8)
#     \pointdef{RQP}(3.6,2)
#     \pointdef{QRP}(3.6,0)
#     \pointdef{QPR}(1.8,-0.8)
#     \point{\PQR,\PRQ,\QPR,\QRP,\RPQ,\RQP}
#     \tlabel[tr]\PQR{pqr}
#     \tlabel[br]\PRQ{prq}
#     \tlabel[bc]\RPQ{rpq}
#     \tlabel[bl]\RQP{rqp}
#     \tlabel[tl]\QRP{qrp}
#     \tlabel[tc]\QPR{qpr}
#     \lin{\PQR}{\PRQ}
#     \lin{\PRQ}{\RPQ}
#     \lin{\RPQ}{\RQP}
#     \lin{\RQP}{\QRP}
#     \lin{\QRP}{\QPR}
#     \lin{\QPR}{\PQR}
# \end{igpic}
# This is not like most of our diagrams; here the dots all represent the
# same repository state, and we move from one to the other by commuting
# the order of the patches.
# 
# We start off with the patch sequence $pqr$.
# This axiom says that if $q$ and $r$ commute ({\ie} you can move from the
# bottom left to the top left) and $p$ can be commuted past $qr$ (you can
# move from bottom left to bottom right), then $q$ and $r$ still commute
# after $p$ has been commuted past them (you can move from the bottom
# right to the top right), and you can commute $p$ back again (move from
# the top right to the top left).
# \end{Iexplanation}
# \end{Iaxiom}

\start{axiom}{unnamed-patch-commute-preserves-commute}
$\begin{array}[t]{@{}l@{}}
 \forall \unnamed{p}  \in \unnamedpatches,
         \unnamed{q}  \in \unnamedpatches,
         \unnamed{r}  \in \unnamedpatches,
         \unnamed{p'} \in \unnamedpatches,
         \unnamed{q'} \in \unnamedpatches,
         \unnamed{r'} \in \unnamedpatches.\\
    \left(\pair{\unnamed{p}}{\unnamed{q}\unnamed{r}} <->
          \pair{\unnamed{q'}\unnamed{r'}}{\unnamed{p'}}\right)
 => \left(\left(\commutes{\unnamed{q}}{\unnamed{r}}\right) <=>
          \left(\commutes{\unnamed{q'}}{\unnamed{r'}}\right)\right)
 \end{array}$

\begin{Iexplanation}
This axiom says that if two patches commute then they still commute if
you commute something else past both of them.

Likewise, if two patches do not commute, then they still do not commute
after commuting something else past them.
\end{Iexplanation}
\end{Iaxiom}

\start{axiom}{unnamed-patch-commute-consistent}
$\begin{array}[t]{@{}l@{}}
 \forall \unnamed{p}  \in \unnamedpatches,
         \unnamed{q}  \in \unnamedpatches,
         \unnamed{r}  \in \unnamedpatches,
         \unnamed{p'} \in \unnamedpatches,
         \unnamed{q'} \in \unnamedpatches,
         \unnamed{r'} \in \unnamedpatches.\\
    \left(\pair{\unnamed{q}}{\unnamed{r}} <->
          \pair{\unnamed{r'}}{\unnamed{q'}}\right) =>
    \left(\left(\pair{\unnamed{p}}{\unnamed{q}\unnamed{r}} <->
                \pair{\_}{\unnamed{p'}}\right)
<=>       \left(\pair{\unnamed{p}}{\unnamed{r'}\unnamed{q'}} <->
                \pair{\_}{\unnamed{p'}}\right)\right)
 \end{array}$
% *)
Axiom UnnamedPatchCommuteConsistent1 :
      forall {unnamedPatch : UnnamedPatch}
             {p1 : up_type unnamedPatch}
             {q1 : up_type unnamedPatch}
             {r1 : up_type unnamedPatch}
             {q2 : up_type unnamedPatch}
             {r2 : up_type unnamedPatch}
             {q3 : up_type unnamedPatch}
             {r3 : up_type unnamedPatch}
             {p3 : up_type unnamedPatch}
             {p5 : up_type unnamedPatch},
      <<q1, r1>> <~>u <<r2, q2>>
   -> <<p1, q1>> <~>u <<q3, p5>>
   -> <<p5, r1>> <~>u <<r3, p3>>
   -> (exists r4 : up_type unnamedPatch,
       (exists q4 : up_type unnamedPatch,
        (exists p6 : up_type unnamedPatch,
         <<q3, r3>> <~>u <<r4, q4>> /\
         <<p1, r2>> <~>u <<r4, p6>> /\
         <<p6, q2>> <~>u <<q4, p3>>))).

Axiom UnnamedPatchCommuteConsistent2 :
      forall {unnamedPatch : UnnamedPatch}
             {p3 : up_type unnamedPatch}
             {q3 : up_type unnamedPatch}
             {r3 : up_type unnamedPatch}
             {q4 : up_type unnamedPatch}
             {r4 : up_type unnamedPatch}
             {q1 : up_type unnamedPatch}
             {r1 : up_type unnamedPatch}
             {p1 : up_type unnamedPatch}
             {p5 : up_type unnamedPatch},
      <<q3, r3>> <~>u <<r4, q4>>
   -> <<r3, p3>> <~>u <<p5, r1>>
   -> <<q3, p5>> <~>u <<p1, q1>>
   -> (exists r2 : up_type unnamedPatch,
       (exists q2 : up_type unnamedPatch,
        (exists p6 : up_type unnamedPatch,
         <<q1, r1>> <~>u <<r2, q2>> /\
         <<q4, p3>> <~>u <<p6, q2>> /\
         <<r4, p6>> <~>u <<p1, r2>>))).
(** %
\begin{Iexplanation}
This axiom says that commuting a patch $p$ past two patches $qr$
gives you the same patch $p'$ regardless of whether $q$ and $r$ have
been commuted or not.
\end{Iexplanation}
\end{Iaxiom}

# XXX Do we need this at the unnamed level?:
# 
# Sequences will be considered equal if they are equal up to commutation;
# in particular, when we talk about something like $\seq{p} \seq{q}$ we
# mean ``a sequence $\seq{r}$ which, after some number of commutations, is
# equal to $\seq{p} \seq{q}$''.

% *)
End patch_sequences.