(** %
\section{\label{sec:catches}Catches and Repos}
% *)
Module Export catches_definition.

Require Import Equality.
Require Import List.

Require Import util.
Require Import names.
Require Import patch_universes.
Require Import patch_universes_sequences.
Require Import invertible_patchlike.
Require Import invertible_patch_universe.
Require Import commute_square.
Require Import merging.
Require Import contexted_patches.
Require Import canonical_order.

(** %
Now that we have laid the foundations, it is time to introduce
catches. We will now be dealing with another datatype, which may
either be a patch (as previously defined) or a \emph{conflictor}. We
will call these beasts \emph{catches}.

\begin{Iexplanation}
The basic idea is that, if two catches do not conflict, then we can
merge them, similar to the way that we merge patches. However,
if they do conflict then when we merge, we get a conflictor which
records the conflict.
To compute the contents of a repository we take the effects of all
the patches that are in the repository and do not conflict with any
other patch in the repository.
\end{Iexplanation}

\begin{Idefinition}[catches]
A catch is either $\patch{p}$ (the non-conflicted patch $p \in \patches$),
$\conflictor{\seq{r}}{X}{\seq{p}:q}$ (a conflicted patch $q \in \patches$), or
$\invconflictor{\seq{r}}{X}{\seq{p}:q}$ (the inverse of a conflicted patch
$q \in \patches$). In both cases, $\seq{r}$ is a sequence of patches,
$X$ is a set of contexted patches, and $\seq{p}:q$ is a contexted patch.
% *)

Program Definition conflictsWith {pu_type : NameSet -> NameSet -> Type}
                         {ppu : PartPatchUniverse pu_type pu_type}
                         {pui : PatchUniverseInv ppu ppu}
                         {pu : PatchUniverse pui}
                         {ipl : InvertiblePatchlike pu_type}
                         {ipu : InvertiblePatchUniverse pu ipl}
                         {from : NameSet}
                         (p : ContextedPatch pu from)
                         (q : ContextedPatch pu from)
                       : Prop
    := match p, q with
       | MkContextedPatch _ _ psContext psPatch _,
         MkContextedPatch _ _ qsContext qsPatch _ =>
             ~(mergable (psContext :+> psPatch :> [])
                        (qsContext :+> qsPatch :> []))
       end.
Next Obligation.
constructor.
rewrite SequenceContentsNil.
signedNameSetDec.
Qed.
Next Obligation.
constructor.
destruct wildcard'1.
destruct psContext.
unfold sequenceContents in *.
rewrite SequenceContentsBaseCons.
rewrite SequenceContentsBaseNil.
remember (sequenceBaseContents s) as seq.
signedNameSetDec.
Qed.
Next Obligation.
constructor.
rewrite SequenceContentsNil.
signedNameSetDec.
Qed.
Next Obligation.
constructor.
destruct wildcard'4.
destruct qsContext.
unfold sequenceContents in *.
rewrite SequenceContentsBaseCons.
rewrite SequenceContentsBaseNil.
remember (sequenceBaseContents s) as seq.
signedNameSetDec.
Qed.

Inductive Catch {pu_type : NameSet -> NameSet -> Type}
                {ppu : PartPatchUniverse pu_type pu_type}
                {pui : PatchUniverseInv ppu ppu}
                {pu : PatchUniverse pui}
                (ipl : InvertiblePatchlike pu_type)
                {ipu : InvertiblePatchUniverse pu ipl}
                (from to : NameSet)
              : Type
    := MkCatch : forall (p : pu_type from to),
                 Catch ipl from to
     | Conflictor : forall (effect : Sequence pu from to)
                           (conflicts : list (ContextedPatch pu to))
                           (ident : ContextedPatch pu to)
                           (* XXX Proof conflicts /= []?
                                  Proof effect^ \subseteq conflicts?
                                  Proof conflicts no dupes? *)
                           (allConflict : Forall (conflictsWith ident) conflicts)
                           (effectCanonicallyOrdered : CanonicallyOrdered effect),
                    Catch ipl from to.
Implicit Arguments MkCatch [pu_type ppu pui pu ipl ipu from to].
Implicit Arguments Conflictor [pu_type ppu pui pu ipl ipu from to].

(** %
\end{Idefinition}

\begin{Idefinition}[repos]
A \emph{repo} is a sequence of catches (up to commutation, to be
defined later) satisfying some requirements (that, again, we will give
later).

Let $\repos$ be the (possibly infinite) set of repos.
\end{Idefinition}

\begin{Iaside}
Do we really need inverse conflictors, or can we just use conflictors
and invert their internals?
\end{Iaside}

The meaning of $\patch{p}$ is hopefully clear, but what is the meaning
of $\conflictor{\seq{r}}{X}{\seq{p} : q}$? To answer this question, we need to
consider it in the context of a repo.

Suppose we have the repo $\seq{c} \conflictor{\seq{r}}{X}{\seq{p} : q}$.
The effect of the conflictor on the repo is $\seq{r}$, and as we have
already said, $\seq{p} : q$ is the (contexted) patch that this
conflictor represents. $X$ is the set of (contexted) patches in
$\seq{c}$ that $q$ conflicts with.

\begin{Iaside}
In darcs' theory, the transitive set of conflicts is stored. I don't
believe that this is needed, and not having it makes things simpler.
Not having it may also mean more things commute.
\end{Iaside}

But how is $\seq{r}$ calculated? $\seq{r}$ is the inverses of the subset
of the patches in $X$ that do not appear in the effect of any conflictor
in $\seq{c}$. In other words, the first catch to conflict with any given
patch reverts that patch.

We can picture a conflictor $\conflictor{\seq{r}}{X}{\seq{p}:q}$ in a repo as
looking like this:
\begin{igpic}{-2}{7}{-3}{4}
    \tlabelsep{3pt}
    \definepoint{from}{(-2,0)}
    \drawpoint{O}{(0,0)}
    \definepoint{midr}{(2,0)}
    \drawpoint{r}{(4,0)}
    \definepoint{to}{(6,0)}
    \definepoint{midp}{(4.5,1)}
    \drawpoint{p}{(5,2)}
    \definepoint{midq}{(5.5,3)}
    \definepoint{q}{(6,4)}
    \definepoint{midXa}{(4.5,-1.5)}
    \definepoint{Xa}{(5,-3)}
    \definepoint{Xb}{(6,-3)}
    \definepoint{Xc}{(7,-3)}
    #
    \arrow\dashed\lin{from}{O}
    \arrlab{O}{midr}{r}{tc}{$\seq{r}$}
    \arrlab{r}{midp}{p}{br}{$\seq{p}$}
    \arrlab{p}{midq}{q}{br}{$q$}
    \arrlab{r}{midXa}{Xa}{tr}{$X$}
    \arrow\lin{r}{Xb}
    \arrow\lin{r}{Xc}
    \arrow\dashed\lin{r}{to}
\end{igpic}

\begin{Idefinition}[catch-effect]
We define $\effectofName$ to tell us the effect that a catch has on the
repo:\\
$\begin{array}[t]{@{}l@{}}
 \effectof{\patch{p}} = p\\
 \effectof{\conflictor{\seq{r}}{X}{y}} = \seq{r}\\
 \effectof{\invconflictor{\seq{r}}{X}{y}} = \seq{r}^\\
 \end{array}$
\end{Idefinition}

\begin{Idefinition}[catch-conflicts]
We define $\catchConflictsName$ to tell us the patches that a catch
conflicts with, {\ie}:\\
$\begin{array}[t]{@{}l@{}}
 \catchConflicts{\patch{p}} = \emptyset\\
 \catchConflicts{\conflictor{\seq{r}}{X}{y}} = \names{X}\\
 \catchConflicts{\invconflictor{\seq{r}}{X}{y}} = \names{X}^\\
 \end{array}$
\end{Idefinition}

\begin{Idefinition}[catch-names]
We extend $\nameName$ and $\namesName$ to work on catches in the natural
way, {\ie}:\\
$\begin{array}[t]{@{}l@{}}
 \name{\patch{p}} = p\\
 \name{\conflictor{\seq{r}}{X}{\seq{p}:q}} = \name{q}\\
 \name{\invconflictor{\seq{r}}{X}{\seq{p}:q}} = \name{q}^\\
 \names{\nocatches} = \emptyset\\
 \names{c \seq{d}} = \mkset{\name{c}} \cup \names{\seq{d}}\\
 \end{array}$
% *)
Definition catch_name {pu_type : NameSet -> NameSet -> Type}
                      {ppu : PartPatchUniverse pu_type pu_type}
                      {pui : PatchUniverseInv ppu ppu}
                      {pu : PatchUniverse pui}
                      {ipl : InvertiblePatchlike pu_type}
                      {ipu : InvertiblePatchUniverse pu ipl}
                      {from to : NameSet}
                      (c : Catch ipl from to) : SignedName
 := match c with
    | MkCatch p => pu_nameOf p
    | Conflictor _ _ p _ _ => contextedPatch_name p
    end.
(** %
\end{Idefinition}

\begin{Idefinition}[repo-properties]
Repos are inductively defined as follows:

$\emptyrepo$ is a repo.

$\seq{c} \patch{p}$ is a repo if
\begin{itemize}
\item $\seq{c}$ is a repo
\item $\name{p}$ is positive
\item $\name{p} \notin \names{\seq{c}}$
\item $\effectof{c} p$ is sensible
\end{itemize}

$\seq{c} \seq{d} \seq{e} \conflictor{\seq{r}}{X}{\seq{p} : q}$
is a repo if:
\begin{itemize}
\item $\seq{c} \seq{d} \seq{e}$ is a repo
\item $\seq{e}$ is a sequence of patches ({\ie} there are no conflictors
      in $\seq{e}$)
\item $\effectof{\seq{e}} = \seq{r}^$
\item $\effectof{\seq{d}} = \seq{p}^$
\item $\names{\seq{d} \seq{e}} = \names{X}$
\item Every catch in $d$ is either a conflictor, or in
      $\catchConflicts{d}$
\item $\name{y}$ is positive
\item $\name{y} \notin \names{\seq{c} \seq{d} \seq{e}}$
\item There is no catch $f$ and catch sequence $\seq{g}$ such that
      $\seq{d} \seq{e} = f \seq{g}$ and $f$ does not conflict with
      $\patch{q}$.
\item $\effectof{c} q$ is sensible
\end{itemize}

# XXX We don't allow undo catches in the repo yet
# $\seq{c} \seq{d} \seq{d}^$ is a repo if $\seq{c} \seq{d}$ is a repo and
# all of $\names{\seq{d}}$ are positive.
\end{Idefinition}

\begin{Idefinition}[catch-inverse]
We define\\
$\begin{array}[t]{@{}l@{}}
 \patch{p}^ = \patch{p^}\\
 \conflictor{\seq{r}}{X}{y}^ = \invconflictor{\seq{r}}{X}{y}\\
 \invconflictor{\seq{r}}{X}{y}^ = \conflictor{\seq{r}}{X}{y}
 \end{array}$

# XXX this is if we don't have a special inverse comflictor constructor:
# \conflictor{Es}{Z}{Ps:p}^
# = \conflictor{Es^}{\mkset{(Es Qs q : q^) \mid (Qs : q) \in Z}}{Es Ps p:p^}
% *)
(* XXX Put this elsewhere? *)
Definition invertSignedNameSet (s : SignedNameSet)
                             : SignedNameSet
 := SignedNameSetMod.fold (fun sn s' => SignedNameSetAdd (signedNameInverse sn) s') s SignedNameSetMod.empty.

(*
Definition CatchInverse {ipl : InvertiblePatchlike}
                        {from to : NameSet}
                        (c : Catch ipl from to)
                      : Catch ipl to from
 := match c with
    | MkCatch p => MkCatch (invert _ p)
    | Conflictor _ effect conflicts ident =>
          Conflictor (invertSequence effect)
                     (map (fun cp => addSequenceToContext effect (invertContextedPatch cp)) conflicts)
                     (addSequenceToContext effect (invertContextedPatch ident))
    end.
*)
(** %\end{Idefinition}

\import{}{catch_merge}
\import{}{catch_commute}
% *)

(* XXX Put these things below in the right places: *)
Lemma commute_OneMany_ManyOne
    : forall {pu_type : NameSet -> NameSet -> Type}
             {ppu : PartPatchUniverse pu_type pu_type}
             {pui : PatchUniverseInv ppu ppu}
             {pu : PatchUniverse pui}
             {from mid1 mid2 to : NameSet}
             (p   : pu_type from mid1)
             (qs  : Sequence pu  mid1 to)
             (qs' : Sequence pu  from mid2)
             (p'  : pu_type mid2 to),
      <<p, qs>> <~>om <<qs', p'>>
   -> <<qs', p'>> <~>mo <<p, qs>>.
Proof.
intros.
dependent induction H.
    constructor.
apply commuteSelfInverse in commutePQ.
apply (ConsManyOneCommute IHOneManyCommute commutePQ).
Qed.

Lemma commute_ManyOne_OneMany
    : forall {pu_type : NameSet -> NameSet -> Type}
             {ppu : PartPatchUniverse pu_type pu_type}
             {pui : PatchUniverseInv ppu ppu}
             {pu : PatchUniverse pui}
             {from mid1 mid2 to : NameSet}
             (ps  : Sequence pu  from mid1)
             (q   : pu_type mid1 to)
             (q'  : pu_type from mid2)
             (ps' : Sequence pu  mid2 to),
      <<ps, q>> <~>mo <<q', ps'>>
   -> <<q', ps'>> <~>om <<ps, q>>.
Proof.
intros.
dependent induction H.
    constructor.
apply commuteSelfInverse in commutePQ.
apply (ConsOneManyCommute commutePQ IHManyOneCommute).
Qed.

(*
XXX
Inductive AllCommutePast {pu_type : NameSet -> NameSet -> Type}
                         {ppu : PartPatchUniverse pu_type pu_type}
                         {pui : PatchUniverseInv ppu ppu}
                         {pu : PatchUniverse pui}
                         {ipl : InvertiblePatchlike pu}
                         {from mid : NameSet}
                         (p : pu_type from mid)
                       : list (ContextedPatch pu mid)
                      -> list (ContextedPatch pu from)
                      -> Prop
    := AllCommutePastNil :
           AllCommutePast p nil nil
     | AllCommutePastCons :
           forall {cp : ContextedPatch pu mid}
                  {cps : list (ContextedPatch pu mid)}
                  {cp' : ContextedPatch pu from}
                  {cps' : list (ContextedPatch pu from)},
           CommutePast p cp cp' ->
           AllCommutePast p cps cps' ->
           AllCommutePast p (cons cp cps) (cons cp' cps').
*)

(*
(* XXX Need to define this properly *)
Parameter sequenceCommuteInverse
    : forall {pu_type : NameSet -> NameSet -> Type}
             {ppu : PartPatchUniverse pu_type pu_type}
             {pui : PatchUniverseInv ppu ppu}
             {pu : PatchUniverse pui}
             {ipl : InvertiblePatchlike ppu}
             {from mid mid' to : NameSet}
             {psContains qsContains ps'Contains qs'Contains : SignedNameSet}
             (ps  : Sequence pu from mid )
             (qs  : Sequence pu mid  to  )
             (qs' : Sequence pu from mid')
             (ps' : Sequence pu mid' to  ),
      <<ps, qs>> <~> <<qs', ps'>>
   -> <<qs', ps'>> <~> <<ps, qs>>.
*)

(* XXX Put this somewhere else? *)
Lemma CommuteOutNameInSequence {pu_type : NameSet -> NameSet -> Type}
                               {ppu : PartPatchUniverse pu_type pu_type}
                               {pui : PatchUniverseInv ppu ppu}
                               {pu : PatchUniverse pui}
                               {from mid to : NameSet}
                               {p : pu_type from mid}
                               {qs : Sequence pu mid to}
                               {rs : Sequence pu from to}
                               (commuteOutLeft : <<p, qs>> <~ <<rs>>)
                             : SignedNameSetIn (pu_nameOf p) (sequenceContents rs).
Proof with auto.
induction commuteOutLeft.
    rewrite SequenceContentsCons.
    signedNameSetDec.
destruct (commuteNames H) as [? [? ?]].
rewrite <- H1.
rewrite SequenceContentsCons.
(* coq bug 2699 *)
remember (sequenceContents rs) as X.
signedNameSetDec.
Qed.

(* XXX Put this somewhere else? *)
Lemma TransitiveCommuteRelatesCons {pu_type : NameSet -> NameSet -> Type}
                                   {ppu : PartPatchUniverse pu_type pu_type}
                                   {pui : PatchUniverseInv ppu ppu}
                                   {pu : PatchUniverse pui}
                                   {from mid to : NameSet}
                                   {p : pu_type from mid}
                                   {qs : Sequence pu mid to}
                                   {rs : Sequence pu mid to}
                                   {pQs : ConsOK p qs}
                                   {pRs : ConsOK p rs}
                                   (trans : <<p :> qs>> <~~>* <<p :> rs>>)
                                 : <<qs>> <~~>* <<rs>>.
Proof with auto.
destruct (commuteOutLeftConsistent trans (commuteOutLeftDone p qs _)) as [rs' [X2 X3]].
dependent induction X3.
    consEquality x...
consEquality x...
set (X := CommuteOutNameInSequence X3).
clearbody X.
destruct pRs.
elim consNotAlreadyThere0.
destruct (commuteNames H) as [? [? ?]].
rewrite <- H1...
Qed.

(* XXX Put this elsewhere? *)
Fixpoint conflictsNames {pu_type : NameSet -> NameSet -> Type}
                                 {ppu : PartPatchUniverse pu_type pu_type}
                                 {pui : PatchUniverseInv ppu ppu}
                                 {pu : PatchUniverse pui}
                                 {ipl : InvertiblePatchlike pu_type}
                                 {from : NameSet}
                                 (conflicts : list (ContextedPatch pu from))
                      : SignedNameSet
    := match conflicts with
       | nil => SignedNameSetMod.empty
       | cp :: conflicts' => SignedNameSetMod.add (contextedPatch_name cp) (conflictsNames conflicts')
       end.

(* XXX Move this elsewhere *)
Program Fixpoint noneCommutePastBase
           {pu_type : NameSet -> NameSet -> Type}
           {ppu : PartPatchUniverse pu_type pu_type}
           {pui : PatchUniverseInv ppu ppu}
           {pu : PatchUniverse pui}
           {from mid to : NameSet}
           (x : SequenceBase pu from mid)
           (y : SequenceBase pu mid to)
           (appendOK : SignedNameSetMod.Empty
                           (SignedNameSetMod.inter
                               (sequenceBaseContents x) (sequenceBaseContents y)))
           (xNoDupes : SequenceNoDupes x)
           (yNoDupes : SequenceNoDupes y)
         : Prop
    := match x with
       | Nil _ => True
       | Cons _ _ _ p ps =>
             ~(commutable p (MkSequence (appendBase ps y) _))
             /\ noneCommutePastBase ps y _ _ _
       end.
Next Obligation.
simpl.
subst.
constructor.
rewrite SequenceContentsBaseCons in appendOK.
rewrite SequenceNoDupesCons in xNoDupes.
destruct xNoDupes as [? xNoDupes].
remember (pu_nameOf p) as pName.
clear HeqpName.
dependent induction ps generalizing from p.
    rewrite AppendBaseNil.
    auto.
rewrite SequenceNoDupesCons in xNoDupes.
destruct xNoDupes as [? xNoDupes].
rewrite AppendBaseCons.
unfold SequenceNoDupes.
fold (SequenceNoDupes (from := mid) (to := to)).
split.
    rewrite SequenceContentsBaseAppend.
    rewrite SequenceContentsBaseCons in appendOK.
    remember (sequenceBaseContents ps) as psSeq.
    remember (sequenceBaseContents y) as ySeq.
    signedNameSetDec.
specialize (IHps y).
specialize (IHps yNoDupes).
specialize (IHps pName).
solveFirstIn IHps.
    rewrite SequenceContentsBaseCons in appendOK.
    clear - appendOK.
    remember (sequenceBaseContents ps) as psSeq.
    remember (sequenceBaseContents y) as ySeq.
    signedNameSetDec.
solveFirstIn IHps.
    rewrite SequenceContentsBaseCons in H.
    remember (sequenceBaseContents ps) as psSeq.
    signedNameSetDec.
specialize (IHps xNoDupes).
specialize (IHps from).
specialize (IHps p).
auto.
Qed.
Next Obligation.
simpl.
subst.
rewrite SequenceContentsBaseCons in appendOK.
remember (sequenceBaseContents ps) as psC.
remember (sequenceBaseContents y) as yC.
signedNameSetDec.
Qed.
Next Obligation.
subst.
rewrite SequenceNoDupesCons in xNoDupes.
destruct xNoDupes.
auto.
Qed.

(* XXX Move this elsewhere *)
Program Definition noneCommutePast
           {pu_type : NameSet -> NameSet -> Type}
           {ppu : PartPatchUniverse pu_type pu_type}
           {pui : PatchUniverseInv ppu ppu}
           {pu : PatchUniverse pui}
           {from mid to : NameSet}
           (x : Sequence pu from mid)
           (y : Sequence pu mid to)
           (appendOK : AppendOK x y)
         : Prop
    := match x with
       MkSequence xs _ =>
           match y with
           MkSequence ys _ =>
               noneCommutePastBase xs ys _ _ _
           end
       end.
Next Obligation.
destruct appendOK.
simpl in appendNoIntersection0.
auto.
Qed.
Next Obligation.
destruct wildcard'.
auto.
Qed.
Next Obligation.
destruct wildcard'0.
auto.
Qed.

(* XXX Move this elsewhere *)
Lemma uncommutableSame
             {pu_type : NameSet -> NameSet -> Type}
             {ppu : PartPatchUniverse pu_type pu_type}
             {pui : PatchUniverseInv ppu ppu}
             {pu : PatchUniverse pui}
             {from mid to : NameSet}
             (xs : Sequence pu from mid)
             (ys : Sequence pu mid to)

             {midsplit1 midsplit2 mid1' mid2' : NameSet}
             {ns1 : Sequence pu from midsplit1}
             {ns2 : Sequence pu from midsplit2}
             {cs1 : Sequence pu midsplit1 mid}
             {cs2 : Sequence pu midsplit2 mid}
             {ys1 : Sequence pu midsplit1 mid1'}
             {ys2 : Sequence pu midsplit2 mid2'}
             {cs1' : Sequence pu mid1' to}
             {cs2' : Sequence pu mid2' to}
             {appendOKNs1Cs1 : AppendOK ns1 cs1}
             {appendOKNs2Cs2 : AppendOK ns2 cs2}
             (split1 : <<xs>> <~~>* <<ns1 :+> cs1>>)
             (split2 : <<xs>> <~~>* <<ns2 :+> cs2>>)
             (commute1 : <<cs1, ys>> <~> <<ys1, cs1'>>)
             (commute2 : <<cs2, ys>> <~> <<ys2, cs2'>>)
             {appendOKNs1Ys1 : AppendOK ns1 ys1}
             {appendOKNs2Ys2 : AppendOK ns2 ys2}
             (ns1NonCommute : noneCommutePast ns1 ys1 _)
             (ns2NonCommute : noneCommutePast ns2 ys2 _)
      : midsplit1 = midsplit2 /\ ns1 ~= ns2 /\ cs1 ~= cs2.
Proof.
admit.
Qed.

(* p [p^, {:p}, :q] <-> q [q^, {:q}, :p] *)
Inductive CatchCommute1 {pu_type : NameSet -> NameSet -> Type}
                        {ppu : PartPatchUniverse pu_type pu_type}
                        {pui : PatchUniverseInv ppu ppu}
                        {pu : PatchUniverse pui}
                        {ipl : InvertiblePatchlike pu_type}
                        {ipu : InvertiblePatchUniverse pu ipl}
        : forall {from mid1 mid2 to : NameSet},
          Catch ipl from mid1
       -> Catch ipl mid1 to
       -> Catch ipl from mid2
       -> Catch ipl mid2 to
       -> Prop
    := MkCatchCommute1 :
           forall {from to1 to2 : NameSet}
                  (p : pu_type from to1)
                  (q : pu_type from to2)
                  (namesDifferent : pu_nameOf p <> pu_nameOf q)
                  (do_not_commute : ~(commutable (invert q) p))
                  (invPConsOK : ConsOK (invert p) [])
                  (invQConsOK : ConsOK (invert q) [])
                  (contextedP := MkContextedPatch [] p)
                  (contextedQ := MkContextedPatch [] q)
                  (conflictsP := cons contextedP nil)
                  (conflictsQ := cons contextedQ nil)
                  (q'Effect    := invert p :> [])
                  (p'Effect    := invert q :> [])
                  (q'EffectCanonicallyOrdered : CanonicallyOrdered q'Effect)
                  (p'EffectCanonicallyOrdered : CanonicallyOrdered p'Effect)
                  (* XXX Want to deduce these from do_not_commute really *)
                  (qConflictsP : Forall (conflictsWith contextedQ) conflictsP)
                  (pConflictsQ : Forall (conflictsWith contextedP) conflictsQ)
                  ,
           CatchCommute1 (MkCatch p)
                         (Conflictor q'Effect
                                     conflictsP
                                     contextedQ
                                     qConflictsP
                                     q'EffectCanonicallyOrdered)
                         (MkCatch q)
                         (Conflictor p'Effect
                                     conflictsQ
                                     contextedP
                                     pConflictsQ
                                     p'EffectCanonicallyOrdered).
Notation "<< p , q >> <~>1 << q' , p' >>"
    := (CatchCommute1 p q q' p')
    (at level 60, no associativity).

Inductive CatchCommute2 {pu_type : NameSet -> NameSet -> Type}
                        {ppu : PartPatchUniverse pu_type pu_type}
                        {pui : PatchUniverseInv ppu ppu}
                        {pu : PatchUniverse pui}
                        {ipl : InvertiblePatchlike pu_type}
                        {ipu : InvertiblePatchUniverse pu ipl}
        : forall {from mid1 mid2 to : NameSet},
          Catch ipl from mid1
       -> Catch ipl mid1 to
       -> Catch ipl from mid2
       -> Catch ipl mid2 to
       -> Prop
     := MkCatchCommute2 :
           (* p [p^ r, {r^:p} U X, y] <-> [r, X, y] [, {y}, r^:p] *)
           forall {from mid to : NameSet}
                  (p : pu_type from mid)
                  (qEffect : Sequence pu mid to)
                  (qEffectCanonicallyOrdered : CanonicallyOrdered qEffect)
                  (qConflicts : list (ContextedPatch pu to))
                  (qIdentity : ContextedPatch pu to)
                  (qEffect' : Sequence pu from to)
                  (qEffect'CanonicallyOrdered : CanonicallyOrdered qEffect')
                  (qConflicts' : list (ContextedPatch pu to))
                  (qIdentity' : ContextedPatch pu to)
                  (pEffect' : Sequence pu to to)
                  (pEffect'CanonicallyOrdered : CanonicallyOrdered pEffect')
                  (pConflicts' : list (ContextedPatch pu to))
                  (pIdentity' : ContextedPatch pu to)
                  (namesDifferent : pu_nameOf p <> contextedPatch_name qIdentity)
                  (invPRsConsOK : ConsOK (invert p) qEffect')
                  (invQEffect'pOK : ContextedPatchOK (invert qEffect') p)
                  (qConflictsConflict : Forall (conflictsWith qIdentity) qConflicts)
                  (q'ConflictsConflict : Forall (conflictsWith qIdentity') qConflicts')
                  (p'ConflictsConflict : Forall (conflictsWith pIdentity') pConflicts'),
           <<qEffect>> <~~>* <<invert p :> qEffect'>>
        -> qConflicts = (MkContextedPatch (invert qEffect') p) :: qConflicts'
        -> qIdentity' = qIdentity
        -> pEffect' = []
        -> pConflicts' = qIdentity :: nil
        -> pIdentity' = MkContextedPatch (invert qEffect') p
        -> ~(qConflicts' = nil)
        -> CatchCommute2 (MkCatch p)
                         (Conflictor qEffect
                                     qConflicts
                                     qIdentity
                                     qConflictsConflict
                                     qEffectCanonicallyOrdered)
                         (Conflictor qEffect'
                                     qConflicts'
                                     qIdentity'
                                     q'ConflictsConflict
                                     qEffect'CanonicallyOrdered)
                         (Conflictor pEffect'
                                     pConflicts'
                                     pIdentity'
                                     p'ConflictsConflict
                                     pEffect'CanonicallyOrdered).
Notation "<< p , q >> <~>2 << q' , p' >>"
    := (CatchCommute2 p q q' p')
    (at level 60, no associativity).

Inductive CatchCommute3 {pu_type : NameSet -> NameSet -> Type}
                        {ppu : PartPatchUniverse pu_type pu_type}
                        {pui : PatchUniverseInv ppu ppu}
                        {pu : PatchUniverse pui}
                        {ipl : InvertiblePatchlike pu_type}
                        {ipu : InvertiblePatchUniverse pu ipl}
        : forall {from mid1 mid2 to : NameSet},
          Catch ipl from mid1
       -> Catch ipl mid1 to
       -> Catch ipl from mid2
       -> Catch ipl mid2 to
       -> Prop
     := MkCatchCommute3 :
           (* [r, X, y] [, {y}, r^:q] <-> q [q^ r, {r^:q} U X, y] *)
           forall {from mid to : NameSet}
                  (pEffect : Sequence pu from to)
                  (pEffectCanonicallyOrdered : CanonicallyOrdered pEffect)
                  (pConflicts : list (ContextedPatch pu to))
                  (pIdentity : ContextedPatch pu to)
                  (qEffect : Sequence pu to to)
                  (qEffectCanonicallyOrdered : CanonicallyOrdered qEffect)
                  (qConflicts : list (ContextedPatch pu to))
                  (qIdentity : ContextedPatch pu to)
                  (q' : pu_type from mid)
                  (pEffect' : Sequence pu mid to)
                  (pEffect'CanonicallyOrdered : CanonicallyOrdered pEffect')
                  (pConflicts' : list (ContextedPatch pu to))
                  (pIdentity' : ContextedPatch pu to)
                  (namesDifferent : contextedPatch_name pIdentity <> contextedPatch_name qIdentity)
                  (invPRsConsOK : ConsOK (invert q') pEffect)
                  (invPEffectq'OK : ContextedPatchOK (invert pEffect) q')
                  (pConflictsConflict : Forall (conflictsWith pIdentity) pConflicts)
                  (qConflictsConflict : Forall (conflictsWith qIdentity) qConflicts)
                  (p'ConflictsConflict : Forall (conflictsWith pIdentity') pConflicts'),
           qEffect = []
        -> qConflicts = pIdentity :: nil
        -> qIdentity = MkContextedPatch (invert pEffect) q'
        -> <<pEffect'>> <~~>* <<invert q' :> pEffect>>
        -> pConflicts' = (MkContextedPatch (invert pEffect) q') :: pConflicts
        -> pIdentity' = pIdentity
        -> ~(pConflicts = nil)
        -> CatchCommute3 (Conflictor pEffect
                                     pConflicts
                                     pIdentity
                                     pConflictsConflict
                                     pEffectCanonicallyOrdered)
                         (Conflictor qEffect
                                     qConflicts
                                     qIdentity
                                     qConflictsConflict
                                     qEffectCanonicallyOrdered)
                         (MkCatch q')
                         (Conflictor pEffect'
                                     pConflicts'
                                     pIdentity'
                                     p'ConflictsConflict
                                     pEffect'CanonicallyOrdered).
Notation "<< p , q >> <~>3 << q' , p' >>"
    := (CatchCommute3 p q q' p')
    (at level 60, no associativity).

Inductive CatchCommute4
                        {pu_type : NameSet -> NameSet -> Type}
                        {ppu : PartPatchUniverse pu_type pu_type}
                        {pui : PatchUniverseInv ppu ppu}
                        {pu : PatchUniverse pui}
                        {ipl : InvertiblePatchlike pu_type}
                        {ipu : InvertiblePatchUniverse pu ipl}
        : forall {from mid1 mid2 to : NameSet},
          Catch ipl from mid1
       -> Catch ipl mid1 to
       -> Catch ipl from mid2
       -> Catch ipl mid2 to
       -> Prop
     := MkCatchCommute4 :
(*
           (* [r s, W, x] [t, {t^x} U Y, z] <-> [r t', s'Y, s'z] [s', z U t^W, t^x] *)
*)
           forall {o or ors orst ort : NameSet}

                  (pEffect : Sequence pu o ors)
                  (pEffectCanonicallyOrdered : CanonicallyOrdered pEffect)
                  (pConflicts : list (ContextedPatch pu ors))
                  (pIdentity : ContextedPatch pu ors)
                  (qEffect : Sequence pu ors orst)
                  (qEffectCanonicallyOrdered : CanonicallyOrdered qEffect)
                  (qConflicts : list (ContextedPatch pu orst))
                  (qOtherConflicts : list (ContextedPatch pu orst))
                  (qIdentity : ContextedPatch pu orst)
                  (qEffect' : Sequence pu o ort)
                  (qEffect'CanonicallyOrdered : CanonicallyOrdered qEffect')
                  (qConflicts' : list (ContextedPatch pu ort))
                  (qIdentity' : ContextedPatch pu ort)
                  (pEffect' : Sequence pu ort orst)
                  (pEffect'CanonicallyOrdered : CanonicallyOrdered pEffect')
                  (pConflicts' : list (ContextedPatch pu orst))
                  (pIdentity' : ContextedPatch pu orst)
                  (commonEffect : Sequence pu o or)
                  (pOnlyEffect : Sequence pu or ors)
                  (pEffectCanonicallyOrdered : CanonicallyOrdered pEffect)
                  (qOnlyEffect : Sequence pu or ort)
                  (pEffectCanonicallyOrdered : CanonicallyOrdered pEffect)

                  (namesDifferent : contextedPatch_name pIdentity <> contextedPatch_name qIdentity)

                  (appendOK_commonEffect_pOnlyEffect : AppendOK commonEffect pOnlyEffect)
                  (appendOK_commonEffect_qOnlyEffect : AppendOK commonEffect qOnlyEffect)

                  (pConflictsConflict : Forall (conflictsWith pIdentity) pConflicts)
                  (qConflictsConflict : Forall (conflictsWith qIdentity) qConflicts)
                  (q'ConflictsConflict : Forall (conflictsWith qIdentity') qConflicts')
                  (p'ConflictsConflict : Forall (conflictsWith pIdentity') pConflicts')

                  (iqEffect_notIn_pIdentity :
                          SignedNameSetMod.Empty
                              (SignedNameSetMod.inter
                                   (sequenceContents (invert qEffect))
                                   (contextedPatchContents pIdentity)))
                  (pEffect'_notIn_qOtherConflicts : Forall (fun qOtherConflict =>
                                  SignedNameSetMod.Empty
                                  (SignedNameSetMod.inter
                                       (sequenceContents pEffect')
                                       (contextedPatchContents qOtherConflict)))
                                 qOtherConflicts)
                  (pEffect'_notIn_qIdentity : SignedNameSetMod.Empty
                              (SignedNameSetMod.inter
                                   (sequenceContents pEffect')
                                   (contextedPatchContents qIdentity)))
                  (iqEffect_notIn_pConflicts : Forall (fun pConflict =>
                                  SignedNameSetMod.Empty
                                  (SignedNameSetMod.inter
                                       (sequenceContents (invert qEffect))
                                       (contextedPatchContents pConflict)))
                                 pConflicts)

                  (noneCommutePastCommonEffectPOnlyEffect : noneCommutePast commonEffect pOnlyEffect appendOK_commonEffect_pOnlyEffect)
                  (noneCommutePastCommonEffectQOnlyEffect : noneCommutePast commonEffect qOnlyEffect appendOK_commonEffect_qOnlyEffect),

           <<pEffect>> <~~>* <<commonEffect :+> pOnlyEffect>>
        -> qConflicts = addSequenceToContext (invert qEffect) pIdentity iqEffect_notIn_pIdentity :: qOtherConflicts
        -> <<qEffect'>> <~~>* <<commonEffect :+> qOnlyEffect>>
        -> qConflicts' = addSequenceToContexts pEffect' qOtherConflicts pEffect'_notIn_qOtherConflicts
        -> qIdentity' = addSequenceToContext pEffect' qIdentity pEffect'_notIn_qIdentity
        -> pConflicts' = qIdentity :: addSequenceToContexts (invert qEffect) pConflicts iqEffect_notIn_pConflicts
        -> pIdentity' = addSequenceToContext (invert qEffect) pIdentity iqEffect_notIn_pIdentity
        -> <<pOnlyEffect, qEffect>> <~> <<qOnlyEffect, pEffect'>>
        -> ~(pConflicts = nil)
        -> ~(qConflicts' = nil)
        -> CatchCommute4 (Conflictor pEffect
                                     pConflicts
                                     pIdentity
                                     pConflictsConflict
                                     pEffectCanonicallyOrdered)
                         (Conflictor qEffect
                                     qConflicts
                                     qIdentity
                                     qConflictsConflict
                                     qEffectCanonicallyOrdered)
                         (Conflictor qEffect'
                                     qConflicts'
                                     qIdentity'
                                     q'ConflictsConflict
                                     qEffect'CanonicallyOrdered)
                         (Conflictor pEffect'
                                     pConflicts'
                                     pIdentity'
                                     p'ConflictsConflict
                                     pEffect'CanonicallyOrdered).
Notation "<< p , q >> <~>4 << q' , p' >>"
    := (CatchCommute4 p q q' p')
    (at level 60, no associativity).

Inductive CatchCommute5 {pu_type : NameSet -> NameSet -> Type}
                        {ppu : PartPatchUniverse pu_type pu_type}
                        {pui : PatchUniverseInv ppu ppu}
                        {pu : PatchUniverse pui}
                        {ipl : InvertiblePatchlike pu_type}
                        {ipu : InvertiblePatchUniverse pu ipl}
        : forall {from mid1 mid2 to : NameSet},
          Catch ipl from mid1
       -> Catch ipl mid1 to
       -> Catch ipl from mid2
       -> Catch ipl mid2 to
       -> Prop
     := MkCatchCommute5 :
           (* Successful commute: patch/patch *)
           forall {from mid1 mid2 to : NameSet}
                  (p : pu_type from mid1)
                  (q : pu_type mid1 to)
                  (q' : pu_type from mid2)
                  (p' : pu_type mid2 to),
           <<p, q>> <~> <<q', p'>> ->
           CatchCommute5 (MkCatch p) (MkCatch q) (MkCatch q') (MkCatch p').
Notation "<< p , q >> <~>5 << q' , p' >>"
    := (CatchCommute5 p q q' p')
    (at level 60, no associativity).

(* XXX The ones below here should check there isn't already a conflict *)
Inductive CatchCommute6 {pu_type : NameSet -> NameSet -> Type}
                        {ppu : PartPatchUniverse pu_type pu_type}
                        {pui : PatchUniverseInv ppu ppu}
                        {pu : PatchUniverse pui}
                        {ipl : InvertiblePatchlike pu_type}
                        {ipu : InvertiblePatchUniverse pu ipl}
        : forall {from mid1 mid2 to : NameSet},
          Catch ipl from mid1
       -> Catch ipl mid1 to
       -> Catch ipl from mid2
       -> Catch ipl mid2 to
       -> Prop
    := MkCatchCommute6 :
           (* Successful commute: patch/conflictor *)
           forall {from mid1 mid2 to : NameSet}
                  (p : pu_type from mid1)
                  (qEffect : Sequence pu mid1 to)
                  (qEffectCanonicallyOrdered : CanonicallyOrdered qEffect)
                  (qConflicts : list (ContextedPatch pu to))
                  (qIdentity : ContextedPatch pu to)
                  (qEffect' : Sequence pu from mid2)
                  (qEffect'CanonicallyOrdered : CanonicallyOrdered qEffect')
                  (qConflicts' : list (ContextedPatch pu mid2))
                  (qIdentity' : ContextedPatch pu mid2)
                  (p' : pu_type mid2 to)
                  (namesDifferent : pu_nameOf p <> contextedPatch_name qIdentity)
                  (noConflict : ~SignedNameSetIn (pu_nameOf p) (conflictsNames qConflicts))
                  (qConflictsConflict : Forall (conflictsWith qIdentity) qConflicts)
                  (q'ConflictsConflict : Forall (conflictsWith qIdentity') qConflicts'),
           <<p, qEffect>> <~>om <<qEffect', p'>> ->
           CommutePast p' qIdentity qIdentity' ->
           qConflicts' = map (addToContext p') qConflicts ->
           ~(qConflicts = nil) ->
           CatchCommute6 (MkCatch p)
                         (Conflictor qEffect
                                     qConflicts
                                     qIdentity
                                     qConflictsConflict
                                     qEffectCanonicallyOrdered)
                         (Conflictor qEffect'
                                     qConflicts'
                                     qIdentity'
                                     q'ConflictsConflict
                                     qEffect'CanonicallyOrdered)
                         (MkCatch p').
Notation "<< p , q >> <~>6 << q' , p' >>"
    := (CatchCommute6 p q q' p')
    (at level 60, no associativity).

Inductive CatchCommute7 {pu_type : NameSet -> NameSet -> Type}
                        {ppu : PartPatchUniverse pu_type pu_type}
                        {pui : PatchUniverseInv ppu ppu}
                        {pu : PatchUniverse pui}
                        {ipl : InvertiblePatchlike pu_type}
                        {ipu : InvertiblePatchUniverse pu ipl}
        : forall {from mid1 mid2 to : NameSet},
          Catch ipl from mid1
       -> Catch ipl mid1 to
       -> Catch ipl from mid2
       -> Catch ipl mid2 to
       -> Prop
     := MkCatchCommute7 :
           (* Successful commute: conflictor/patch *)
           forall {from mid1 mid2 to : NameSet}
                  (pEffect : Sequence pu from mid1)
                  (pEffectCanonicallyOrdered : CanonicallyOrdered pEffect)
                  (pConflicts : list (ContextedPatch pu mid1))
                  (pIdentity : ContextedPatch pu mid1)
                  (q : pu_type mid1 to)
                  (q' : pu_type from mid2)
                  (pEffect' : Sequence pu mid2 to)
                  (pEffect'CanonicallyOrdered : CanonicallyOrdered pEffect')
                  (pConflicts' : list (ContextedPatch pu to))
                  (pIdentity' : ContextedPatch pu to)
                  (namesDifferent : contextedPatch_name pIdentity <> pu_nameOf q)
                  (pConflictsConflict : Forall (conflictsWith pIdentity) pConflicts)
                  (p'ConflictsConflict : Forall (conflictsWith pIdentity') pConflicts'),
           <<pEffect, q>> <~>mo <<q', pEffect'>> ->
           CommutePast (invert q) pIdentity pIdentity' ->
           pConflicts' = map (addToContext (invert q)) pConflicts ->
           ~(pConflicts = nil) ->
           CatchCommute7 (Conflictor pEffect
                                     pConflicts
                                     pIdentity
                                     pConflictsConflict
                                     pEffectCanonicallyOrdered)
                         (MkCatch q)
                         (MkCatch q')
                         (Conflictor pEffect'
                                     pConflicts'
                                     pIdentity'
                                     p'ConflictsConflict
                                     pEffect'CanonicallyOrdered).
Notation "<< p , q >> <~>7 << q' , p' >>"
    := (CatchCommute7 p q q' p')
    (at level 60, no associativity).

Inductive CatchCommute8 {pu_type : NameSet -> NameSet -> Type}
                        {ppu : PartPatchUniverse pu_type pu_type}
                        {pui : PatchUniverseInv ppu ppu}
                        {pu : PatchUniverse pui}
                        {ipl : InvertiblePatchlike pu_type}
                        {ipu : InvertiblePatchUniverse pu ipl}
        : forall {from mid1 mid2 to : NameSet},
          Catch ipl from mid1
       -> Catch ipl mid1 to
       -> Catch ipl from mid2
       -> Catch ipl mid2 to
       -> Prop
     := MkCatchCommute8 :
           (* Successful commute: conflictor/conflictor *)
           forall {from common mid1 mid2 to : NameSet}
                  (pEffect : Sequence pu from mid1)
                  (pEffectCanonicallyOrdered : CanonicallyOrdered pEffect)
                  (pConflicts : list (ContextedPatch pu mid1))
                  (pIdentity : ContextedPatch pu mid1)
                  (qEffect : Sequence pu mid1 to)
                  (qEffectCanonicallyOrdered : CanonicallyOrdered qEffect)
                  (qConflicts : list (ContextedPatch pu to))
                  (qIdentity : ContextedPatch pu to)
                  (qEffect' : Sequence pu from mid2)
                  (qEffect'CanonicallyOrdered : CanonicallyOrdered qEffect')
                  (qConflicts' : list (ContextedPatch pu mid2))
                  (qIdentity' : ContextedPatch pu mid2)
                  (pEffect' : Sequence pu mid2 to)
                  (pEffect'CanonicallyOrdered : CanonicallyOrdered pEffect')
                  (pConflicts' : list (ContextedPatch pu to))
                  (pIdentity' : ContextedPatch pu to)
                  (commonEffect : Sequence pu from common)
                  (commonEffectCanonicallyOrdered : CanonicallyOrdered commonEffect)
                  (pOnlyEffect : Sequence pu common mid1)
                  (pOnlyEffectCanonicallyOrdered : CanonicallyOrdered pOnlyEffect)
                  (qOnlyEffect : Sequence pu common mid2)
                  (qOnlyEffectCanonicallyOrdered : CanonicallyOrdered qOnlyEffect)
                  (appendOK_commonEffect_pOnlyEffect : AppendOK commonEffect pOnlyEffect)
                  (appendOK_commonEffect_qOnlyEffect : AppendOK commonEffect qOnlyEffect)
                  (namesDifferent : contextedPatch_name pIdentity <> contextedPatch_name qIdentity)
                  (pConflictsConflict : Forall (conflictsWith pIdentity) pConflicts)
                  (qConflictsConflict : Forall (conflictsWith qIdentity) qConflicts)
                  (q'ConflictsConflict : Forall (conflictsWith qIdentity') qConflicts')
                  (p'ConflictsConflict : Forall (conflictsWith pIdentity') pConflicts')

                  (iqEffect_notIn_pConflicts : Forall (fun pConflict =>
                                  SignedNameSetMod.Empty
                                  (SignedNameSetMod.inter
                                       (sequenceContents (invert qEffect))
                                       (contextedPatchContents pConflict)))
                                 pConflicts)
                  (pEffect'_notIn_qConflict : Forall (fun qConflict =>
                                  SignedNameSetMod.Empty
                                  (SignedNameSetMod.inter
                                       (sequenceContents pEffect')
                                       (contextedPatchContents qConflict)))
                                 qConflicts)
                  (qEffect_notIn_qIdentity :
                          SignedNameSetMod.Empty
                              (SignedNameSetMod.inter
                                   (sequenceContents qEffect)
                                   (contextedPatchContents qIdentity)))
                  ,

           (* Effects *)
(*
                        pEffect                                 qEffect
    <from> commonEffect <common> pOnlyEffect <mid1>       <mid1>qEffect<to>

                        qEffect'                                pEffect'
    <from> commonEffect <common> qOnlyEffect <mid2>       <mid2>pEffect'<to>
*)
           <<pOnlyEffect, qEffect>> <~> <<qOnlyEffect, pEffect'>> ->
           <<pEffect>> <~~>* <<commonEffect :+> pOnlyEffect>> ->
           <<qEffect'>> <~~>* <<commonEffect :+> qOnlyEffect>> ->
           SignedNameSetMod.Empty
               (SignedNameSetMod.inter
                    (sequenceContents pOnlyEffect)
                    (sequenceContents qOnlyEffect)) ->

           (* Identities *)
           CommuteManyPast (invert qEffect) pIdentity pIdentity' ->
           CommuteManyPast pEffect' qIdentity qIdentity' ->

           (* Conflicts *)
           pConflicts' = addSequenceToContexts (invert qEffect) pConflicts iqEffect_notIn_pConflicts ->
           qConflicts' = addSequenceToContexts pEffect' qConflicts pEffect'_notIn_qConflict ->

           (* The patches themselves can't conflict *)
           ~(conflictsWith pIdentity (addSequenceToContext qEffect qIdentity qEffect_notIn_qIdentity)) ->

           ~(pConflicts = nil) ->
           ~(qConflicts = nil) ->

           CatchCommute8 (Conflictor pEffect
                                     pConflicts
                                     pIdentity
                                     pConflictsConflict
                                     pEffectCanonicallyOrdered)
                         (Conflictor qEffect
                                     qConflicts
                                     qIdentity
                                     qConflictsConflict
                                     qEffectCanonicallyOrdered)
                         (Conflictor qEffect'
                                     qConflicts'
                                     qIdentity'
                                     q'ConflictsConflict
                                     qEffect'CanonicallyOrdered)
                         (Conflictor pEffect'
                                     pConflicts'
                                     pIdentity'
                                     p'ConflictsConflict
                                     pEffect'CanonicallyOrdered).
Notation "<< p , q >> <~>8 << q' , p' >>"
    := (CatchCommute8 p q q' p')
    (at level 60, no associativity).

(* XXX Temporary? *)
Inductive commuteNum : nat -> Prop
    := mkCommuteNum : forall (myCommuteNum : nat), commuteNum myCommuteNum.

Inductive CatchCommute {pu_type : NameSet -> NameSet -> Type}
                       {ppu : PartPatchUniverse pu_type pu_type}
                       {pui : PatchUniverseInv ppu ppu}
                       {pu : PatchUniverse pui}
                       {ipl : InvertiblePatchlike pu_type}
                       {ipu : InvertiblePatchUniverse pu ipl}
                       {from mid1 mid2 to : NameSet}
                       (p : Catch ipl from mid1)
                       (q : Catch ipl mid1 to)
                       (q' : Catch ipl from mid2)
                       (p' : Catch ipl mid2 to)
                     : Prop
       (* p [p^, {:p}, :q] <-> q [q^, {:q}, :p] *)
    := isCatchCommute1 : forall (myCommuteNum : commuteNum 1)
                                (catchCommuteDetails : CatchCommute1 p q q' p'),
                         CatchCommute p q q' p'
           (* p [p^ r, {r^:p} U X, y] <-> [r, X, y] [, {y}, r^:p] *)
     | isCatchCommute2 : forall (myCommuteNum : commuteNum 2)
                                (catchCommuteDetails : CatchCommute2 p q q' p'),
                         CatchCommute p q q' p'
           (* [r, X, y] [, {y}, r^:q] <-> q [q^ r, {r^:q} U X, y] *)
     | isCatchCommute3 : forall (myCommuteNum : commuteNum 3)
                                (catchCommuteDetails : CatchCommute3 p q q' p'),
                         CatchCommute p q q' p'
           (* [r s, W, x] [t, {t^x} U Y, z] <-> [r t', s'Y, s'z] [s', z U t^W, t^x] *)
     | isCatchCommute4 : forall (myCommuteNum : commuteNum 4)
                                (catchCommuteDetails : CatchCommute4 p q q' p'),
                         CatchCommute p q q' p'
           (* Successful commute: patch/patch *)
     | isCatchCommute5 : forall (myCommuteNum : commuteNum 5)
                                (catchCommuteDetails : CatchCommute5 p q q' p'),
                         CatchCommute p q q' p'
           (* Successful commute: patch/conflictor *)
     | isCatchCommute6 : forall (myCommuteNum : commuteNum 6)
                                (catchCommuteDetails : CatchCommute6 p q q' p'),
                         CatchCommute p q q' p'
           (* Successful commute: conflictor/patch *)
     | isCatchCommute7 : forall (myCommuteNum : commuteNum 7)
                                (catchCommuteDetails : CatchCommute7 p q q' p'),
                         CatchCommute p q q' p'
           (* Successful commute: conflictor/conflictor *)
     | isCatchCommute8 : forall (myCommuteNum : commuteNum 8)
                                (catchCommuteDetails : CatchCommute8 p q q' p'),
                         CatchCommute p q q' p'.
Notation "<< p , q >> <~>c << q' , p' >>"
    := (CatchCommute p q q' p')
    (at level 60, no associativity).

(* XXX Move this lemma to contexted_patches: *)
Lemma nameOfAddSequenceToContext :
      forall {pu_type : NameSet -> NameSet -> Type}
             {ppu : PartPatchUniverse pu_type pu_type}
             {pui : PatchUniverseInv ppu ppu}
             {pu : PatchUniverse pui}
             {ipl : InvertiblePatchlike pu_type}
             {from to : NameSet}
             {ps : Sequence pu from to}
             {cp : ContextedPatch pu to}
             {notIn : SignedNameSetMod.Empty
                          (SignedNameSetMod.inter
                               (sequenceContents ps)
                               (contextedPatchContents cp))},
      contextedPatch_name (addSequenceToContext ps cp notIn) = contextedPatch_name cp.
Proof with auto.
intros.
(*
XXX
induction ps.
    admit.
*)
admit.
Qed.

(* XXX *)
Lemma addSequenceToContextInverse1 :
      forall {pu_type : NameSet -> NameSet -> Type}
             {ppu : PartPatchUniverse pu_type pu_type}
             {pui : PatchUniverseInv ppu ppu}
             {pu : PatchUniverse pui}
             {ipl : InvertiblePatchlike pu_type}
             {ipu : InvertiblePatchUniverse pu ipl}
             {from to : NameSet}
             {ps : Sequence pu from to}
             {cp : ContextedPatch pu from}
             {notInInv : SignedNameSetMod.Empty
                             (SignedNameSetMod.inter
                                  (sequenceContents (invert ps))
                                  (contextedPatchContents cp))}
             {notIn : SignedNameSetMod.Empty
                          (SignedNameSetMod.inter
                               (sequenceContents ps)
                               (contextedPatchContents (addSequenceToContext (invert ps) cp notInInv)))},
      addSequenceToContext ps
          (addSequenceToContext (invert ps) cp notInInv) notIn = cp.
Proof with auto.
(*
XXX
intros.
induction ps.
    admit.
*)
admit.
Qed.

(*
XXX
Lemma addSequenceToContextInverse2 :
      forall {pu_type : NameSet -> NameSet -> Type}
             {ppu : PartPatchUniverse pu_type pu_type}
             {pui : PatchUniverseInv ppu ppu}
             {pu : PatchUniverse pui}
             {ipl : InvertiblePatchlike pu_type}
             {ipu : InvertiblePatchUniverse pu ipl}
             {from to : NameSet}
             {ps : Sequence pu from to}
             {cp : ContextedPatch pu to},
      addSequenceToContext (invert ps)
          (addSequenceToContext ps cp) = cp.
Proof with auto.
intros.
(*
XXX
induction ps.
    admit.
*)
admit.
Qed.

Lemma addSequenceToContextIdentity1 :
      forall {pu_type : NameSet -> NameSet -> Type}
             {ppu : PartPatchUniverse pu_type pu_type}
             {pui : PatchUniverseInv ppu ppu}
             {pu : PatchUniverse pui}
             {ipl : InvertiblePatchlike pu_type}
             {ipu : InvertiblePatchUniverse pu ipl}
             {from to : NameSet}
             {ps : Sequence pu from to},
      forall (cp : ContextedPatch pu from),
      (fun x =>
           addSequenceToContext ps
               (addSequenceToContext (invert ps) x)) cp
    = (fun x => x) cp.
Proof with auto.
intros.
simpl.
apply addSequenceToContextInverse1...
Qed.

Lemma addSequenceToContextIdentity2 :
      forall {pu_type : NameSet -> NameSet -> Type}
             {ppu : PartPatchUniverse pu_type pu_type}
             {pui : PatchUniverseInv ppu ppu}
             {pu : PatchUniverse pui}
             {ipl : InvertiblePatchlike pu_type}
             {ipu : InvertiblePatchUniverse pu ipl}
             {from to : NameSet}
             {ps : Sequence pu from to},
      forall (cp : ContextedPatch pu to),
      (fun x =>
           addSequenceToContext (invert ps)
               (addSequenceToContext ps x)) cp
    = (fun x => x) cp.
Proof with auto.
intros.
simpl.
apply addSequenceToContextInverse2...
Qed.
*)

(* XXX Move this lemma to contexted_patches: *)
Lemma nameOfCommutePast :
      forall {pu_type : NameSet -> NameSet -> Type}
             {ppu : PartPatchUniverse pu_type pu_type}
             {pui : PatchUniverseInv ppu ppu}
             {pu : PatchUniverse pui}
             {ipl : InvertiblePatchlike pu_type}
             {from to : NameSet}
             {p : pu_type from to}
             {cp : ContextedPatch pu to}
             {cp' : ContextedPatch pu from},
      CommutePast p cp cp'
   -> contextedPatch_name cp' = contextedPatch_name cp.
Proof with auto.
intros.
induction H.
    simpl.
    destruct (commuteNames commute0) as [? [? ?]]...
simpl in *...
Qed.

(* XXX Move this lemma to contexted_patches: *)
Lemma nameOfCommuteManyPast :
      forall {pu_type : NameSet -> NameSet -> Type}
             {ppu : PartPatchUniverse pu_type pu_type}
             {pui : PatchUniverseInv ppu ppu}
             {pu : PatchUniverse pui}
             {ipl : InvertiblePatchlike pu_type}
             {from to : NameSet}
             {ps : Sequence pu from to}
             {cp : ContextedPatch pu to}
             {cp' : ContextedPatch pu from},
      CommuteManyPast ps cp cp'
   -> contextedPatch_name cp' = contextedPatch_name cp.
Proof with auto.
intros.
induction H...
rewrite <- IHCommuteManyPast.
apply (nameOfCommutePast CommutePPast).
Qed.

(* XXX Move this lemma?: *)
Lemma nameOfCommuteOneMany :
      forall {pu_type : NameSet -> NameSet -> Type}
             {ppu : PartPatchUniverse pu_type pu_type}
             {pui : PatchUniverseInv ppu ppu}
             {pu : PatchUniverse pui}
             {from mid1 mid2 to : NameSet}
             {p : pu_type from mid1}
             {qs : Sequence pu mid1 to}
             {qs' : Sequence pu from mid2}
             {p' : pu_type mid2 to},
      <<p, qs>> <~> <<qs', p'>>
   -> pu_nameOf p = pu_nameOf p'.
Proof with auto.
intros.
induction H...
rewrite <- IHOneManyCommute.
destruct (commuteNames commutePQ)...
Qed.

(* XXX Move this lemma?: *)
Lemma nameOfCommuteManyOne :
      forall {pu_type : NameSet -> NameSet -> Type}
             {ppu : PartPatchUniverse pu_type pu_type}
             {pui : PatchUniverseInv ppu ppu}
             {pu : PatchUniverse pui}
             {ipl : InvertiblePatchlike pu_type}
             {from mid1 mid2 to : NameSet}
             {ps : Sequence pu from mid2}
             {q : pu_type mid2 to}
             {q' : pu_type from mid1}
             {ps' : Sequence pu mid1 to},
      <<ps, q>> <~> <<q', ps'>>
   -> pu_nameOf q = pu_nameOf q'.
Proof with auto.
intros.
induction H...
rewrite IHManyOneCommute.
destruct (commuteNames commutePQ) as [? [? ?]]...
Qed.

Lemma CatchCommuteNames :
      forall {pu_type : NameSet -> NameSet -> Type}
             {ppu : PartPatchUniverse pu_type pu_type}
             {pui : PatchUniverseInv ppu ppu}
             {pu : PatchUniverse pui}
             {ipl : InvertiblePatchlike pu_type}
             {ipu : InvertiblePatchUniverse pu ipl}
             {from mid1 mid2 to : NameSet}
             {p  : Catch ipl from mid1} {q  : Catch ipl mid1 to}
             {q' : Catch ipl from mid2} {p' : Catch ipl mid2 to}
             (c : << p , q >> <~>c << q' , p' >>),
      (catch_name p = catch_name p') /\
      (catch_name q = catch_name q') /\
      (catch_name p <> catch_name q).
Proof with auto.
intros.
dependent destruction c; dependent destruction catchCommuteDetails; simpl; subst...
                (* case 4 *)
                rewrite nameOfAddSequenceToContext.
                rewrite nameOfAddSequenceToContext...
            (* case 5 *)
            apply commuteNames...
        (* case 6 *)
        destruct qIdentity.
        destruct qIdentity'.
        apply nameOfCommutePast in H0.
        simpl in *.
        destruct (OneManyCommuteNames H).
        split...
    (* case 7 *)
    destruct pIdentity.
    destruct pIdentity'.
    simpl in *.
    apply nameOfCommutePast in H0.
    simpl in *.
    destruct (ManyOneCommuteNames H).
    split...
(* case 8 *)
destruct pIdentity.
destruct pIdentity'.
destruct qIdentity.
destruct qIdentity'.
simpl in *.
apply nameOfCommuteManyPast in H3.
apply nameOfCommuteManyPast in H4...
Qed.

Definition CatchCommutable {pu_type : NameSet -> NameSet -> Type}
                           {ppu : PartPatchUniverse pu_type pu_type}
                           {pui : PatchUniverseInv ppu ppu}
                           {pu : PatchUniverse pui}
                           {ipl : InvertiblePatchlike pu_type}
                           {ipu : InvertiblePatchUniverse pu ipl}
                           {from mid1 to : NameSet}
                           (p : Catch ipl from mid1)
                           (q : Catch ipl mid1 to) : Prop
 := exists mid2 : NameSet,
    exists q' : Catch ipl from mid2,
    exists p' : Catch ipl mid2 to,
    <<p, q>> <~>c <<q', p'>>.
Notation "p <~?~>c q" := (CatchCommutable p q)
    (at level 60, no associativity).

Lemma CatchCommutable_dec :
      forall {pu_type : NameSet -> NameSet -> Type}
             {ppu : PartPatchUniverse pu_type pu_type}
             {pui : PatchUniverseInv ppu ppu}
             {pu : PatchUniverse pui}
             {ipl : InvertiblePatchlike pu_type}
             {ipu : InvertiblePatchUniverse pu ipl}
             {from mid to : NameSet}
             (p : Catch ipl from mid)
             (q : Catch ipl mid to),
      {p <~?~>c q} + {~(p <~?~>c q)}.
Proof with auto.
intros.
destruct p; destruct q.
            (* Two patches case *)
            destruct (commutable_dec p p0) as [commutable | not_commutable].
                left.
                destruct commutable as [mid' [q' [p' c']]].
                exists mid'.
                exists (MkCatch q').
                exists (MkCatch p').
                apply isCatchCommute5.
                    apply mkCommuteNum.
                apply MkCatchCommute5...
            right.
            intro c.
            destruct c as [mid' [q' [p' c']]].
            destruct c'; dependent destruction catchCommuteDetails.
            elim not_commutable.
            exists mid2.
            exists q'.
            exists p'...
        (* Patch/Conflictor case *)
        admit.
    (* Conflictor/Patch case *)
    admit.
(* Conflictor/Conflictor case *)
admit.
Qed.

Lemma CatchCommuteSelfInverse :
      forall {pu_type : NameSet -> NameSet -> Type}
             {ppu : PartPatchUniverse pu_type pu_type}
             {pui : PatchUniverseInv ppu ppu}
             {pu : PatchUniverse pui}
             {ipl : InvertiblePatchlike pu_type}
             {ipu : InvertiblePatchUniverse pu ipl}
             {cs : CommuteSquare pu_type pu_type}
             {from mid1 mid2 to : NameSet}
             {p : Catch ipl from mid1}
             {q : Catch ipl mid1 to}
             {q' : Catch ipl from mid2}
             {p' : Catch ipl mid2 to}
             (c : <<p, q>> <~>c <<q', p'>>),
      (<<q', p'>> <~>c <<p, q>>).
Proof with auto.
intros.
destruct c; destruct catchCommuteDetails.
                            (* MkCatchCommute1 case *)
                            apply isCatchCommute1.
                                apply mkCommuteNum.
                            apply MkCatchCommute1.
                                apply sym_not_eq...
                            intro commutable.
                            elim do_not_commute.
                            destruct commutable as [mid [q' [p' Hcommute]]].
                            exists mid.
                            exists (invert p').
                            exists (invert q')...
                            apply commuteInverses in Hcommute.
                            rewrite invertInverse in Hcommute.
                            apply commuteSelfInverse...
                        (* MkCatchCommute2 case *)
                        subst.
                        apply isCatchCommute3.
                            apply mkCommuteNum.
                        eapply MkCatchCommute3...
                    (* MkCatchCommute3 case *)
                    subst.
                    apply isCatchCommute2.
                        apply mkCommuteNum.
                    eapply MkCatchCommute2...
                (* MkCatchCommute4 case *)
                apply isCatchCommute4.
                    apply mkCommuteNum.
                (*
                XXX
                refine (MkCatchCommute4
                            qEffect' qConflicts' qIdentity'
                            pEffect' pConflicts' (map (addSequenceToContext (invert qEffect)) pConflicts) pIdentity'
                            pEffect pConflicts pIdentity
                            qEffect qConflicts qIdentity
                            commonEffect _ _ _ _ _ _ _ _ _ _ _ _ _ _ _)...
                                                subst.
                                                rewrite nameOfAddSequenceToContext.
                                                rewrite nameOfAddSequenceToContext...
                                            apply H1.
                                        subst.
                                        rewrite addSequenceToContextInverse2...
                                    apply H.
                                rewrite map_map.
                                rewrite (map_ext _ _ addSequenceToContextIdentity1).
                                rewrite map_id...
                            subst.
                            rewrite addSequenceToContextInverse1...
                        subst.
                        rewrite map_map.
                        rewrite (map_ext _ _ addSequenceToContextIdentity2).
                        rewrite map_id...
                    subst.
                    rewrite addSequenceToContextInverse2...
                apply sequenceCommuteInverse...
                *)
                admit.
            (* MkCatchCommute5 case *)
            apply isCatchCommute5.
                apply mkCommuteNum.
            apply MkCatchCommute5.
            apply commuteSelfInverse in H...
        (* MkCatchCommute6 case *)
        apply isCatchCommute7.
            apply mkCommuteNum.
        apply MkCatchCommute7.
                        rewrite <- (nameOfCommuteOneMany H).
                        rewrite (nameOfCommutePast H0).
                        apply sym_not_eq...
                    apply commute_OneMany_ManyOne...
                admit.
            admit.
        subst.
        apply map_neq_nil...
    (* MkCatchCommute7 case *)
    apply isCatchCommute6.
        apply mkCommuteNum.
    apply MkCatchCommute6.
                        rewrite <- (nameOfCommuteManyOne H).
                        rewrite (nameOfCommutePast H0).
                        apply sym_not_eq...
                    admit.
                apply commute_ManyOne_OneMany...
            admit.
        admit.
    subst.
    apply map_neq_nil...
(* MkCatchCommute8 case *)
apply isCatchCommute8.
    apply mkCommuteNum.
assert (ipEffect'_notIn_qConflict' : Forall (fun qConflict' =>
                        SignedNameSetMod.Empty
                        (SignedNameSetMod.inter
                             (sequenceContents (invert pEffect'))
                             (contextedPatchContents qConflict')))
                       qConflicts').
    admit.
assert (qEffect_notIn_pConflict' : Forall (fun pConflict' =>
                        SignedNameSetMod.Empty
                        (SignedNameSetMod.inter
                             (sequenceContents qEffect)
                             (contextedPatchContents pConflict')))
                       pConflicts').
    admit.
assert (pEffect'_notIn_pIdentity' : SignedNameSetMod.Empty
                    (SignedNameSetMod.inter
                         (sequenceContents pEffect')
                         (contextedPatchContents pIdentity'))).
    admit.
refine (MkCatchCommute8 qEffect' qEffect'CanonicallyOrdered qConflicts' qIdentity'
                        pEffect' pEffect'CanonicallyOrdered pConflicts' pIdentity'
                        pEffect  pEffectCanonicallyOrdered  pConflicts  pIdentity
                        qEffect  qEffectCanonicallyOrdered  qConflicts  qIdentity
                        commonEffect commonEffectCanonicallyOrdered
                        qOnlyEffect qOnlyEffectCanonicallyOrdered
                        pOnlyEffect pOnlyEffectCanonicallyOrdered
                        appendOK_commonEffect_qOnlyEffect appendOK_commonEffect_pOnlyEffect
                        _
                        q'ConflictsConflict p'ConflictsConflict
                        pConflictsConflict qConflictsConflict
                        ipEffect'_notIn_qConflict' qEffect_notIn_pConflict' pEffect'_notIn_pIdentity'
                        _ _ _ _ _ _ _ _ _ _ _)...
                                    rewrite (nameOfCommuteManyPast H3).
                                    rewrite (nameOfCommuteManyPast H4)...
                                (* XXX apply sequenceCommuteInverse... *)
                                admit.
                            clear - H2.
                            remember (sequenceContents qOnlyEffect) as qSeq.
                            remember (sequenceContents pOnlyEffect) as pSeq.
                            signedNameSetDec.
                        admit.
                    admit.
                admit.
            admit.
        admit.
    subst.
    apply addSequenceToContexts_not_nil2...
subst.
apply addSequenceToContexts_not_nil2...
Qed.

Lemma CatchCommuteUnique :
      forall {pu_type : NameSet -> NameSet -> Type}
             {ppu : PartPatchUniverse pu_type pu_type}
             {pui : PatchUniverseInv ppu ppu}
             {pu : PatchUniverse pui}
             {ipl : InvertiblePatchlike pu_type}
             {ipu : InvertiblePatchUniverse pu ipl}
             {from mid mid' mid'' to : NameSet}
             {p   : Catch ipl from mid}   {q   : Catch ipl mid   to}
             {q'  : Catch ipl from mid'}  {p'  : Catch ipl mid'  to}
             {q'' : Catch ipl from mid''} {p'' : Catch ipl mid'' to}
             (commute1 : <<p, q>> <~>c <<q', p'>>)
             (commute2 : <<p, q>> <~>c <<q'', p''>>),
      (mid' = mid'') /\ (p' ~= p'') /\ (q' ~= q'').
Proof with auto.
intros.
dependent destruction commute1;
dependent destruction catchCommuteDetails;
dependent destruction commute2;
dependent destruction catchCommuteDetails.
(* 20: Rule 1 / Rule 1 *)
(* XXX Can we replace all these substs with a single tactic? *)
subst contextedP.
subst contextedP0.
subst contextedQ.
subst contextedQ0.
subst conflictsP.
subst conflictsP0.
subst conflictsQ.
subst conflictsQ0.
subst p'Effect0.
subst q'Effect.
subst p'Effect.
subst q'Effect0.
proofIrrel invQConsOK invQConsOK0.
proofIrrel invPConsOK invPConsOK0.
proofIrrel pConflictsQ pConflictsQ0.
proofIrrel p'EffectCanonicallyOrdered p'EffectCanonicallyOrdered0.
split...
(* 19: Rule 1 / Rule 2 *)
congruence.
(* 18: Rule 1 / Rule 6 *)
simpl in noConflict.
elim noConflict.
signedNameSetDec.
(* 17: Rule 2 / Rule 1 *)
congruence.
(* 16: Rule 2 / Rule 2 *)
proofIrrel namesDifferent namesDifferent0.
apply (f_equal invert) in x.
rewrite invertInverse in x.
rewrite invertInverse in x.
subst.
proofIrrel invPRsConsOK invPRsConsOK0.
proofIrrel pEffect'CanonicallyOrdered pEffect'CanonicallyOrdered0.
proofIrrel qEffect'CanonicallyOrdered qEffect'CanonicallyOrdered0.
proofIrrel invQEffect'pOK invQEffect'pOK0.
proofIrrel p'ConflictsConflict p'ConflictsConflict0.
proofIrrel q'ConflictsConflict q'ConflictsConflict0.
split...
(* 15: Rule 2 / Rule 6 *)
subst.
simpl in noConflict.
elim noConflict.
signedNameSetDec.
(* 14: Rule 3 / Rule 3 *)
proofIrrel invPRsConsOK invPRsConsOK0.
assert (pEffect'sEqual : <<pEffect'>> <~~>* <<pEffect'0>>).
    apply SymmetricTransitiveCommute in H9.
    apply (TransitiveTransitiveCommute H2 H9)...
assert (pEffect' = pEffect'0).
    apply (CanonicallyOrderedUnique pEffect'CanonicallyOrdered pEffect'CanonicallyOrdered0 pEffect'sEqual).
subst.
proofIrrel invPEffectq'OK invPEffectq'OK0.
proofIrrel p'ConflictsConflict p'ConflictsConflict0.
proofIrrel pEffect'CanonicallyOrdered pEffect'CanonicallyOrdered0.
split...
(* 13: Rule 3 / Rule 4 *)
rewrite addSequenceToContexts_nil in H15.
congruence.
(* 12: Rule 3 / Rule 8 *)
subst.
elim H14.
assert (X : addSequenceToContext [] (MkContextedPatch (invert pEffect) q') qEffect_notIn_qIdentity
          = MkContextedPatch (invert pEffect) q').
    admit.
rewrite X.
dependent destruction p'ConflictsConflict...
(* 11: Rule 4 / Rule 3 *)
rewrite addSequenceToContexts_nil in H8.
congruence.
(* 10: Rule 4 / Rule 4 *)
subst.
destruct (uncommutableSame _ _ H H9 H6 H16
              noneCommutePastCommonEffectQOnlyEffect
              noneCommutePastCommonEffectQOnlyEffect0)
    as [X1 [X2 X3]].
subst.
subst.
doCommuteUnique H6 H16.
proofIrrel appendOK_commonEffect_qOnlyEffect appendOK_commonEffect_qOnlyEffect0.
assert (<<qEffect'>> <~~>* <<qEffect'0>>).
    apply SymmetricTransitiveCommute in H11.
    apply (TransitiveTransitiveCommute H1 H11).
assert (qEffect' = qEffect'0).
    apply CanonicallyOrderedUnique...
subst.
split...
proofIrrel p'ConflictsConflict p'ConflictsConflict0.
proofIrrel pEffect'CanonicallyOrdered pEffect'CanonicallyOrdered0.
proofIrrel q'ConflictsConflict q'ConflictsConflict0.
proofIrrel qEffect'CanonicallyOrdered qEffect'CanonicallyOrdered0.
split...
(* 9: Rule 4 / Rule 8 *)
subst.

(**
XXX
dependent destruction qConflictsConflict.

H17 : ~ conflictsWith pIdentity
      (addSequenceToContext qEffect qIdentity)


H0 : conflictsWith qIdentity
       (addSequenceToContext
           (invert qEffect) pIdentity)


assert (pConflictsWithQ: conflictsWith pIdentity (addSequenceToContext qEffect qIdentity)).
    admit.



congruence.
XXX.


Want: conflictsWith pIdentity (addSequenceToContext qEffect qIdentity)).

qConflictsConflict : Forall (conflictsWith qIdentity)
                       (addSequenceToContext (invert qEffect)
                          pIdentity :: qOtherConflicts)
=>
    conflictsWith qIdentity
                  (addSequenceToContext (invert qEffect) pIdentity)
=>
    conflictsWith (addSequenceToContext (invert qEffect) pIdentity)
                  qIdentity

qConflictsConflict : Forall (conflictsWith qIdentity)
                       (addSequenceToContext (invert qEffect)
                          pIdentity :: qOtherConflicts)

H17 : ~ conflictsWith pIdentity (addSequenceToContext qEffect qIdentity)

qConflictsConflict0 : Forall (conflictsWith qIdentity)
                        (addSequenceToContext (invert qEffect)
                           pIdentity :: qOtherConflicts)


p'ConflictsConflict : Forall
                        (conflictsWith
                           (addSequenceToContext (invert qEffect)
                              pIdentity))
                        (qIdentity
                         :: map
                              (addSequenceToContext (invert qEffect))
                              pConflicts)
*)

admit.
(* 8: Rule 5 / Rule 5 *)
doCommuteUnique H H0...
(* 7: Rule 6 / Rule 1 *)
simpl in noConflict.
elim noConflict.
signedNameSetDec.
(* 6: Rule 6 / Rule 2 *)
simpl in noConflict.
elim noConflict.
signedNameSetDec.
(* 5: Rule 6 / Rule 6 *)
admit.
(* 4: Rule 7 / Rule 7 *)
admit.
(* 3: Rule 8 / Rule 3 *)
admit.
(* 2: Rule 8 / Rule 4 *)
admit.
(* 1: Rule 8 / Rule 8 *)
admit.
Qed.

Lemma CatchCommuteUnique2 :
      forall {pu_type : NameSet -> NameSet -> Type}
             {ppu : PartPatchUniverse pu_type pu_type}
             {pui : PatchUniverseInv ppu ppu}
             {pu : PatchUniverse pui}
             {ipl : InvertiblePatchlike pu_type}
             {ipu : InvertiblePatchUniverse pu ipl}
             {from mid mid' to : NameSet}
             {p   : Catch ipl from mid}  {q   : Catch ipl mid  to}
             {q'  : Catch ipl from mid'} {p'  : Catch ipl mid' to}
             {q'' : Catch ipl from mid'} {p'' : Catch ipl mid' to}
             (commute1 : <<p, q>> <~>c <<q', p'>>)
             (commute2 : <<p, q>> <~>c <<q'', p''>>),
      (p' = p'') /\ (q' = q'').
Proof with auto.
(*
XXX
intros.
dependent destruction commute1;
dependent destruction catchCommuteDetails;
dependent destruction commute2;
dependent destruction catchCommuteDetails.
(* Rule 1 / Rule 1 *)
split...
assert (HX1 : nilOK = nilOK0).
    apply proof_irrelevance.
rewrite HX1.
assert (HX2 : invQContains = invQContains0).
    clear - invQConsOK invQConsOK0.
    destruct invQConsOK.
    destruct invQConsOK0.
    apply SignedNameSetEquality.
    remember (pu_nameOf (q^)) as HX. (* Workaround for coq 2464 *)
    signedNameSetDec.
subst.
assert (HX2 : invQConsOK = invQConsOK0).
    apply proof_irrelevance.
rewrite HX2...
(* Rule 1 / Rule 2 *)
congruence.
(* Rule 1 / Rule 6 *)
admit.
(* Others... *)
congruence.
admit.
admit.
admit.
admit.
admit.
admit.
admit.
admit.
admit.
admit.
admit.
admit.
admit.
admit.
admit.
admit.
(*
destruct (commuteUnique _ H H0).
subst.
split...
admit.
*)
*)
admit.
Qed.

End catches_definition.