(** %
\section{\label{sec:catch_patch_universe}Catch Patch Universe}
% *)
Module Export catch_patch_universe.

Require Import hunks.
Require Import catches.
Require Import catches_definition.
Require Import patch_universes.
Require Import names.

Definition HunkCatchType := Catch HunkInvertiblePatchlike.

Definition HunkCatchPartPatchUniverse := CatchPartPatchUniverse HunkInvertiblePatchlike.
Definition HunkCatchPatchUniverseInv := CatchPatchUniverseInv HunkInvertiblePatchlike.
Definition HunkCatchPatchUniverse := CatchPatchUniverse HunkInvertiblePatchlike.

Lemma hunkCatchCommuteInSequenceConsistent :
    forall {o oq oqr oqrs ou our ours : NameSet}
           {qs : Sequence HunkCatchPatchUniverse o oq}
           {r : HunkCatchType oq oqr}
           {s : HunkCatchType oqr oqrs}
           (* ts omitted for now *)
           {us : Sequence HunkCatchPatchUniverse o ou}
           {r' : HunkCatchType ou our}
           {s' : HunkCatchType our ours}
           {vs : Sequence HunkCatchPatchUniverse ours oqrs}

           (s_NilConsOK : ConsOK s [])
           (r_s_NilConsOK : ConsOK r (s :> []))
           (qs_r_s_NilAppendOK : AppendOK qs (r :> s :> []))

           (s'_vsConsOK : ConsOK s' vs)
           (r'_s'_vsConsOK : ConsOK r' (s' :> vs))
           (us_r'_s'_vsAppendOK : AppendOK us (r' :> (s' :> vs))),
    (<<qs :+> r :> s :> []>> <~~>* <<us :+> r' :> s' :> vs>>)
 -> (catch_name r = catch_name r')
 -> (catch_name s = catch_name s')
 -> (r <~?~> s)
 -> (r' <~?~> s').
Proof.
apply (@commuteInSequenceConsistent HunkCatchType HunkCatchPartPatchUniverse HunkCatchPatchUniverseInv HunkCatchPatchUniverse).
Qed.

(** %

$\patch{p} (\patch{a} \patch{b} + \patch{c} \patch{d}) =
 \patch{p} \patch{a} \patch{b}
 \conflictor{b^ a^}{\mkset{:a, a:b}}{:c}
 \conflictor{\nopatches}{\mkset{:a, a:b}}{c:d}$

You can trace a sequence $p a b b^ a^ a b$

XXXXXXXXXXXXXXXXXXXXXX

XXX Want to show that catches inhabit a patch universe

XXX This all need to be updated properly for catches

XXX At some point we need to say that equality on catches is only up to
commutation of their internals

\start{lemma}{catch-commute-unique}
$\begin{array}[t]{@{}l@{}}
 \forall p \in \patches, q \in \patches,
         j \in (\patches \times \patches) \cup \mkset{\fail},
         k \in (\patches \times \patches) \cup \mkset{\fail} .\\
 (\pair{p}{q} <-> j) \wedge
 (\pair{p}{q} <-> k) => j = k
 \end{array}$
\begin{Iexplanation}
This is \refLemma{named-patch-commute-unique}
restated for catches.
\end{Iexplanation}
\begin{Iproof}
Catch commute is a load of patch commutes. Each of those patch commutes
has a unique result by \refLemma{named-patch-commute-unique}.
\end{Iproof}
\end{Ilemma}

XXX This needs to be strengthened to only talk
about catches adjacent in a repo:

\start{lemma}{catch-commute-self-inverse}
$\begin{array}[t]{@{}l@{}}
 \forall p  \in \patches, q  \in \patches,
         p' \in \patches, q' \in \patches .\\
 (\pair{p}{q} <-> \pair{q'}{p'}) <=>
 (\pair{q'}{p'} <-> \pair{p}{q})
 \end{array}$
\begin{Iexplanation}
This is \refLemma{named-patch-commute-self-inverse}
restated for catches.
\end{Iexplanation}
\begin{Iproof}
XXX Need names/numbers for the rules.

If two catches commutes by the patch/conflicting-patch rule, then they
commute back by the same rule.

If two catches commutes by the conflictor/conflicting-patch rule, then they
commute back by the patch/conflicting-conflictor rule, and vice-versa.

For the conflictor/conflicting-conflictor rule, in the forward direction
we have\\
$\pair{\conflictor{\seq{r} \seq{s}}{W}{x}}#
      {\conflictor{\seq{t}}{\mkset{\seq{t}^x} \union Y}{z}} <->
 \pair{\conflictor{\seq{r} \seq{t'}}{\seq{s'}Y}{\seq{s'}z}}#
      {\conflictor{\seq{s'}}{\mkset{z} \union \seq{t}^W}{\seq{t}^x}}$\\
Adding an identity (XXX need a lemma that this is an identity) and some
parentheses to the right hand side gives us\\
$\pair{\conflictor{\seq{r} \seq{t'}}{(\seq{s'}Y)}{(\seq{s'}z)}}#
      {\conflictor{\seq{s'}}{\mkset{\seq{s'}^ (\seq{s'} z)} \union
                             (\seq{t}^W)}{(\seq{t}^x)}}$\\
and by the conflictor/conflicting-conflictor rule we get\\
$\begin{array}[t]{@{}l@{}}
 \pair{\conflictor{\seq{r} \seq{t'}}{(\seq{s'}Y)}{(\seq{s'}z)}}#
      {\conflictor{\seq{s'}}{\mkset{\seq{s'}^ (\seq{s'} z)} \union
                             (\seq{t}^W)}{(\seq{t}^x)}} <->\\
 \pair{\conflictor{\seq{r} \seq{s}}{\seq{t}(\seq{t}^W)}{\seq{t}(\seq{t}^x)}}#
      {\conflictor{\seq{t}}{\mkset{(\seq{t}^x)} \union \seq{s'}^(\seq{s'}Y)}{\seq{s'}^(\seq{s'}z)}}\\
    \quad \textrm{ if } \begin{array}[t]{@{}l@{}}
                        \pair{\seq{t'}}{\seq{s'}} <-> \pair{\seq{s}}{\seq{t}}\\
                        \names{\seq{r}^} \subseteq \names{\seq{t}^W)}\\
                        \names{\seq{t'}^} \cap \names{\seq{t}^W)} = \emptyset\\
                        \end{array}
 \end{array}$\\
XXX Show side conditions OK\\
Finally, simplifying the result (XXX need a lemma for that too) gives us\\
$\pair{\conflictor{\seq{r} \seq{t'}}{(\seq{s'}Y)}{(\seq{s'}z)}}#
      {\conflictor{\seq{s'}}{\mkset{\seq{s'}^ (\seq{s'} z)} \union
                             (\seq{t}^W)}{(\seq{t}^x)}} <->
 \pair{\conflictor{\seq{r} \seq{s}}{W}{x}}#
      {\conflictor{\seq{t}}{\mkset{(\seq{t}^x)} \union Y}{z}}$\\
and we are back where we started, as required.

XXX patch/patch

XXX conflictor/patch

XXX patch/conflictor

XXX conflictor/conflictor
\end{Iproof}
\end{Ilemma}

XXX We need to do something about this one. We probably need to add the
cases for inverse conflicting patches in the commute rules. This will
have the side-effect that we won't need to strengthen the other lemmata.

\start{lemma}{catch-commute-square}
$\begin{array}[t]{@{}l@{}}
 \forall p  \in \patches, q  \in \patches,
 \forall p' \in \patches, q' \in \patches .\\
    \left(\pair{p}{q} <->
          \pair{q'}{p'}\right) <=>
    \left(\pair{q'^}{p} <->
          \pair{p'}{q^}\right)
 \end{array}$
\begin{Iexplanation}
This is \refLemma{named-patch-commute-square}
restated for catches.
\end{Iexplanation}
\begin{Iproof}
XXX
\end{Iproof}
\end{Ilemma}

XXX This needs to be strengthened to only talk
about catches adjacent in a repo:

\start{lemma}{catch-commute-preserves-commute}
$\begin{array}[t]{@{}l@{}}
 \forall p  \in \patches,
         q  \in \patches,
         r  \in \patches,
         p' \in \patches,
         q' \in \patches,
         r' \in \patches.\\
    \left(\pair{p}{qr} <->
          \pair{q'r'}{p'}\right)
 => \left(\left(\commutes{q}{r}\right) <=>
          \left(\commutes{q'}{r'}\right)\right)
 \end{array}$
\begin{Iexplanation}
This is \refLemma{named-patch-commute-preserves-commute}
restated for catches.
\end{Iexplanation}
\begin{Iproof}
XXX
\end{Iproof}
\end{Ilemma}

XXX This needs to be strengthened to only talk
about catches adjacent in a repo:

\start{lemma}{catch-commute-consistent}
$\begin{array}[t]{@{}l@{}}
 \forall p  \in \patches,
         q  \in \patches,
         r  \in \patches,
         p' \in \patches,
         q' \in \patches,
         r' \in \patches.\\
    \left(\pair{q}{r} <->
          \pair{r'}{q'}\right) =>
    \left(\left(\pair{p}{qr} <->
                \pair{\_}{p'}\right)
<=>       \left(\pair{p}{r'q'} <->
                \pair{\_}{p'}\right)\right)
 \end{array}$
\begin{Iexplanation}
This is \refLemma{named-patch-commute-consistent}
restated for catches.
\end{Iexplanation}
\begin{Iproof}
XXX
\end{Iproof}
\end{Ilemma}
% *)

End catch_patch_universe.