(** %
\section{\label{sec:unnamed_patches}Unnamed Patches}
% *)
Module Export unnamed_patches.
(** %

We start by introducing \emph{unnamed patches}, and the concept of
\emph{patch commutation}. For now, we will refer to unnamed patches as
simply \emph{patches}.

\start{definition}{unnamed-patches}
We have a (possibly infinite) set of patches $\unnamedpatches$.
% *)

Reserved Notation "p ^u" (at level 10).
Reserved Notation "<< p , q >> <~>u << q' , p' >>" (at level 60, no associativity).
Reserved Notation "p <~?~>u q"     (at level 60, no associativity).

Record UnnamedPatch : Type := mkUnnamedPatch {
    up_type : Set;
(** %
\end{Idefinition}

The underlining in the $\unnamedpatches$ and $\unnamed{p}$ syntax is a
bit heavy, but we prefer to reserve the cleaner syntax for named
patches.

\start{axiom}{unnamed-patch-inverse}
$\forall \unnamed{p} \in \unnamedpatches .
 \unnamed{p}^ \in \unnamedpatches$.
% *)
(*
XXX inverse is an axiom in the latex. Maybe it should
be a definition?
*)
unnamedPatchInverse : up_type -> up_type
    where "p ^u" := (unnamedPatchInverse p);
(** %
\begin{Iexplanation}
All patches have an inverse.
\end{Iexplanation}
\end{Iaxiom}
% *)

unnamedPatchInvertInverse : forall (p : up_type), (p^u)^u = p;

(** %
\start{definition}{unnamed-patch-commute}
There is a $<->$ relation, pronounced ``commutes to'', such that:\\
$\begin{array}[t]{@{}r@{~}l@{}}
 \multicolumn{2}{@{}l@{}}{\forall \unnamed{p} \in \unnamedpatches,
                                  \unnamed{q} \in \unnamedpatches .}\\
     &\left( \exists \unnamed{p'} \in \unnamedpatches,
                     \unnamed{q'} \in \unnamedpatches .
      \pair{\unnamed{p}}{\unnamed{q}} <->
      \pair{\unnamed{q'}}{\unnamed{p'}} \right )\\
 \vee&\pair{\unnamed{p}}{\unnamed{q}} <-> \fail
 \end{array}$
% *)
unnamedPatchCommute : up_type -> up_type -> up_type -> up_type -> Prop
    where "<< p , q >> <~>u << q' , p' >>" := (unnamedPatchCommute p q q' p');
(** %
\begin{Iexplanation}
We write
$\pair{\unnamed{p}}{\unnamed{q}} <-> \pair{\unnamed{q'}}{\unnamed{p'}}$
if $\unnamed{p}$ and $\unnamed{q}$ commute, resulting in $\unnamed{q'}$
and $\unnamed{p'}$.In other words, doing $\unnamed{p}$ and then
$\unnamed{q}$ is equivalent to doing $\unnamed{q'}$ and then
$\unnamed{p'}$, where $\unnamed{p}$ and $\unnamed{p'}$ are morally
equivalent, and likewise $\unnamed{q}$ and $\unnamed{q'}$ are morally
equivalent.

For example, adding ``Hello'' to line 3 of a file and then adding
``World'' to line 5 of the file is equivalent to adding ``World'' to line
4 of the file and then adding ``Hello'' to line 3 of a file. We
therefore say that
$\pair{\textrm{add ``Hello'' 3}}{\textrm{add ``World'' 5}}
 <->
 \pair{\textrm{add ``World'' 4}}{\textrm{add ``Hello'' 3}}$.

We can represent this diagramatically thus:
\begin{igpic}{0}{4}{-1}{1}
    \drawpoint{O}{(0,0)}
    \definepoint{midP}{(1,0.8)}
    \drawpoint{P}{(2,1)}
    \definepoint{midQ}{(1,-0.8)}
    \drawpoint{Q}{(2,-1)}
    \definepoint{midPQ}{(3,0.8)}
    \definepoint{midQP}{(3,-0.8)}
    \drawpoint{PQ}{(4,0)}
    \arrlab{O}{midP}{P}{br}{$\unnamed{p}$}
    \arrlab{P}{midPQ}{PQ}{bl}{$\unnamed{q}$}
    \arrlab{O}{midQ}{Q}{tr}{$\unnamed{q'}$}
    \arrlab{Q}{midQP}{PQ}{tl}{$\unnamed{p'}$}
\end{igpic}
Here the dots are repository states, and the arrows are patches;
$\unnamed{p}\unnamed{q}$ and $\unnamed{q'}\unnamed{p'}$ get us from the
same state, to the same state, but via different intermediate states.

We write $\pair{\unnamed{p}}{\unnamed{q}} <-> \fail$ if $\unnamed{p}$
and $\unnamed{q}$ do not commute. In other words, it is not possible to
do the moral equivalent of $\unnamed{q}$ before $\unnamed{p}$.

For example,
$\pair{\textrm{replace line 3 with ``Hello''}}#
      {\textrm{replace line 3 with ``World''}}
<-> \fail$
\end{Iexplanation}
\end{Idefinition}

\start{axiom}{unnamed-patch-commute-unique}
$\begin{array}[t]{@{}l@{}}
 \forall \unnamed{p} \in \unnamedpatches, \unnamed{q} \in \unnamedpatches,
         j \in (\unnamedpatches \times \unnamedpatches) \cup \mkset{\fail},
         k \in (\unnamedpatches \times \unnamedpatches) \cup \mkset{\fail} .\\
 (\pair{\unnamed{p}}{\unnamed{q}} <-> j) \wedge
 (\pair{\unnamed{p}}{\unnamed{q}} <-> k) => j = k
 \end{array}$
% *)
UnnamedPatchCommuteUnique :
      forall {p   : up_type} {q   : up_type}
             {p'  : up_type} {q'  : up_type}
             {p'' : up_type} {q'' : up_type},
      <<p, q>> <~>u <<q', p'>>
   -> <<p, q>> <~>u <<q'', p''>>
   -> (p' = p'') /\ (q' = q'');
(** %
\begin{Iexplanation}
Either $\unnamed{p}$ and $\unnamed{q}$ \emph{always} commute, or they
\emph{never} commute. If they do commute, then the result is always the
same.
\end{Iexplanation}
\end{Iaxiom}

Now that we know that the result of a commute is unique, we can afford
to be a bit lax about quantifying over variables. For example, if we are
dealing with two patches $\unnamed{p}$ and $\unnamed{q}$ and we say that
$\pair{\unnamed{p}}{\unnamed{q}} <-> \pair{\unnamed{q'}}{\unnamed{p'}}$
then it is implied that we are considering the case where $\unnamed{p}$
and $\unnamed{q}$ commute, and that the result of the commutation is
$\unnamed{q'}$ and $\unnamed{p'}$.

\start{definition}{unnamed-patches-commutable}
We define $\commutesName$ to relate two patches if they are commutable,
{\ie}
$\commutes{\unnamed{p}}{\unnamed{q}} <=>
 \exists \unnamed{p'}, \unnamed{q'} .
 \pair{\unnamed{p}}{\unnamed{q}} <-> \pair{\unnamed{q'}}{\unnamed{p'}}$
% *)


unnamedPatchCommutable : up_type -> up_type -> Prop
 := fun (p : up_type) => fun (q : up_type) =>
    (exists q' : up_type, exists p' : up_type,
    <<p, q>> <~>u <<q', p'>>)
where "p <~?~>u q" := (unnamedPatchCommutable p q);

unnamedPatchCommutable_dec :
      forall (p : up_type) (q : up_type),
      { q' : up_type &
      { p' : up_type &
      <<p, q>> <~>u <<q', p'>> }}
      +
      {~(p <~?~>u q)};
(** %
\end{Idefinition}

\start{axiom}{unnamed-patch-commute-self-inverse}
$\begin{array}[t]{@{}l@{}}
 \forall \unnamed{p}  \in \unnamedpatches, \unnamed{q}  \in \unnamedpatches,
         \unnamed{p}' \in \unnamedpatches, \unnamed{q}' \in \unnamedpatches .\\
 (\pair{\unnamed{p}}{\unnamed{q}} <-> \pair{\unnamed{q'}}{\unnamed{p'}}) <=>
 (\pair{\unnamed{q'}}{\unnamed{p'}} <-> \pair{\unnamed{p}}{\unnamed{q}})
 \end{array}$
% *)
UnnamedPatchCommuteSelfInverse :
      forall (p  : up_type) (q  : up_type)
             (p' : up_type) (q' : up_type),
      (<<p,  q>>  <~>u <<q', p'>>) <->
      (<<q', p'>> <~>u <<p,  q>>);
(** %
\begin{Iexplanation}
If you commute a pair of patches, and then commute them back again, then
you end up back where you started. Note also that we require that if
commuting one way succeeds then commuting the other way also succeeds.
\end{Iexplanation}
\end{Iaxiom}

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

UnnamedPatchCommuteSquare :
      forall (p  : up_type) (q  : up_type)
             (p' : up_type) (q' : up_type),
      <<p, q>> <~>u <<q', p'>> ->
      << q'^u, p>> <~>u <<p', q^u>>;

(* XXX UnnamedPatchCommuteConsistent[12] copy/pasted from
       unnamed_patch_sequences without accompanying text *)
UnnamedPatchCommuteConsistent1 :
      forall {p1 : up_type}
             {q1 : up_type}
             {r1 : up_type}
             {q2 : up_type}
             {r2 : up_type}
             {q3 : up_type}
             {r3 : up_type}
             {p3 : up_type}
             {p5 : up_type},
      <<q1, r1>> <~>u <<r2, q2>>
   -> <<p1, q1>> <~>u <<q3, p5>>
   -> <<p5, r1>> <~>u <<r3, p3>>
   -> exists r4 : up_type,
      exists q4 : up_type,
      exists p6 : up_type,
      <<q3, r3>> <~>u <<r4, q4>> /\
      <<p1, r2>> <~>u <<r4, p6>> /\
      <<p6, q2>> <~>u <<q4, p3>>;

UnnamedPatchCommuteConsistent2 :
      forall {p3 : up_type}
             {q3 : up_type}
             {r3 : up_type}
             {q4 : up_type}
             {r4 : up_type}
             {q1 : up_type}
             {r1 : up_type}
             {p1 : up_type}
             {p5 : up_type},
      <<q3, r3>> <~>u <<r4, q4>>
   -> <<r3, p3>> <~>u <<p5, r1>>
   -> <<q3, p5>> <~>u <<p1, q1>>
   -> exists r2 : up_type,
      exists q2 : up_type,
      exists p6 : up_type,
      <<q1, r1>> <~>u <<r2, q2>> /\
      <<q4, p3>> <~>u <<p6, q2>> /\
      <<r4, p6>> <~>u <<p1, r2>>
}.
(** %
\begin{Iexplanation}
\refAxiom{unnamed-patch-inverse} tells us that all patches have an
inverse. Therefore we can augment our patch commutation diagram with
inverse patches:
\begin{igpic}[2][1.3]{0}{4}{-2}{2}
    \drawpoint{O}{(0,0)}
    \definepoint{midP}{(0.8,1.2)}
    \definepoint{midPinv}{(1.2,0.8)}
    \drawpoint{P}{(2,2)}
    \definepoint{midQ}{(0.8,-1.2)}
    \definepoint{midQinv}{(1.2,-0.8)}
    \drawpoint{Q}{(2,-2)}
    \definepoint{midPQ}{(3.2,1.2)}
    \definepoint{midPQinv}{(2.8,0.8)}
    \definepoint{midQP}{(3.2,-1.2)}
    \definepoint{midQPinv}{(2.8,-0.8)}
    \drawpoint{PQ}{(4,0)}
    \arrlab{O}{midP}{P}{br}{$\unnamed{p}$}
    \arrlab{P}{midPinv}{O}{tl}{$\unnamed{p}^$}
    \arrlab{P}{midPQ}{PQ}{bl}{$\unnamed{q}$}
    \arrlab{PQ}{midPQinv}{P}{tr}{$\unnamed{q}^$}
    \arrlab{O}{midQ}{Q}{tr}{$\unnamed{q'}$}
    \arrlab{Q}{midQinv}{O}{bl}{$\unnamed{q'}^$}
    \arrlab{Q}{midQP}{PQ}{tl}{$\unnamed{p'}$}
    \arrlab{PQ}{midQPinv}{Q}{br}{$\unnamed{p'}^$}
\end{igpic}
This axiom tells us that we can rotate the diagram 90 degrees clockwise
and we again have a valid commutation diagram. The arrows from left to
right along the top are $\unnamed{q'}^ \unnamed{p}$ and along the bottom
are $\unnamed{p'} \unnamed{q}^$, thus
$\pair{\unnamed{q'}^}{\unnamed{p}} <->
 \pair{\unnamed{p'}}{\unnamed{q}^}$.

In actual fact, by applying this axiom twice or three times, we can see
that all four of the rotations are equivalent, and thus
$\pair{\unnamed{p'}^}{\unnamed{q'}^} <->
 \pair{\unnamed{q}^}{\unnamed{p}^}$ and
$\pair{\unnamed{q}}{\unnamed{p'}^} <->
 \pair{\unnamed{p}^}{\unnamed{q'}}$.
\end{Iexplanation}
\end{Iaxiom}
% *)

Notation "p ^u" := (unnamedPatchInverse _ p).
Notation "<< p , q >> <~>u << q' , p' >>" := (unnamedPatchCommute _ p q q' p').
Notation "p <~?~>u q" := (unnamedPatchCommutable _ p q).

End unnamed_patches.