(** %
\section{\label{sec:named_patches}Named patches}

% *)
Module Export named_patches.

Require Import Equality.
Require Import ProofIrrelevance.

Require Import util.
Require Import unnamed_patches.
Require Import names.
Require Import patch_universes.
Require Import invertible_patchlike.
Require Import invertible_patch_universe.
Require Import commute_square.

(** %
Rather than working directly with unnamed patches, we will work with
named patches. A named patch is built out of a name and an unnamed
patch. For the motivation for this decision, see
\refAppendix{named_patch_motivation}.

# XXX
# \start{definition}{named-patches}
# We have a (possibly infinite) set of named patches $\patches$.
# \end{Idefinition}

\start{definition}{named-patches}
If $j \in \allnames$ and $\unnamed{p} \in \unnamedpatches$, then
$\namedpatch{j}{p}$ is a \emph{named patch}.

We define a (possibly infinite) set of \emph{named patches} $\patches$ thus:
$\forall j \in \allnames, \unnamed{p} \in \unnamedpatches .
 \namedpatch{j}{p} \in \patches$.
% *)

Record NamedPatch (unnamedPatch : UnnamedPatch)
                  (from to : NameSet) : Type := mkNamedPatch {
    np_unnamedPatch : up_type unnamedPatch;
    np_name : SignedName;
    np_nameOK : patchNamesOK from to np_name
}.
Implicit Arguments np_unnamedPatch [unnamedPatch from to].
Implicit Arguments np_name         [unnamedPatch from to].
Implicit Arguments np_nameOK       [unnamedPatch from to].
Implicit Arguments mkNamedPatch    [unnamedPatch from to].
(** %
\end{Idefinition}

From here on, the unqualified term ``patches'' will refer to named
patches.

\start{definition}{patch-name}
We define $\nameName$ to tell us the name of a patch, {\ie}
$\name{\namedpatch{j}{\unnamed{p}}} = j$.
\end{Idefinition}

\start{definition}{unnamed-patch-of}
We define $\unnamedpatch{p}$ to tell us the unnamed patch of a patch,
{\ie} $\unnamedpatch{\namedpatch{j}{\unnamed{q}}} = \unnamed{q}$.
\end{Idefinition}

\start{definition}{named-patch-inverse}
$\namedpatch{j}{\unnamed{p}}^ = \namedpatch{j^}{\unnamed{p}^}$
\begin{Iexplanation}
The inverse of a named patch has the inverse name, and the inverse
effect.
\end{Iexplanation}
% *)
(* XXX Should this be elsewhere?: *)
Lemma patchNamesOKInverse : forall {from to : NameSet}
                                   {n : SignedName}
                                   (namesOK : patchNamesOK from to n),
                            patchNamesOK to from (signedNameInverse n).
Proof with auto.
intros.
destruct n.
destruct s.
    simpl.
    destruct namesOK.
    split...
simpl.
destruct namesOK.
split...
Qed.

Definition namedPatchInverse {unnamedPatch : UnnamedPatch}
                             {from to : NameSet}
                             (p : NamedPatch unnamedPatch from to)
                           : NamedPatch unnamedPatch to from
(* XXX Shouldn't unnamedPatchInverse's first argument be implicit? *)
 := mkNamedPatch (unnamedPatchInverse _ (np_unnamedPatch p))
                 (signedNameInverse (np_name p))
                 (patchNamesOKInverse (np_nameOK p)).
Notation "p ^n" := (namedPatchInverse p)
    (at level 10).
(** %
\end{Idefinition}

\start{definition}{named-patch-commute}
We extend $<->$ to named patches thus:\\
$\left(
     \pair{\namedpatch{j}{\unnamed{p}}}{\namedpatch{k}{\unnamed{q}}}
     <->
     \pair{\namedpatch{k}{\unnamed{q'}}}{\namedpatch{j}{\unnamed{p'}}}
 \right)
 <=>
 \left(j \ne k\right) \wedge
 \left(j \ne k^\right) \wedge
 \left(\pair{p}{q} <-> \pair{q'}{p'}\right)$
% *)
Inductive namedPatchCommute {unnamedPatch : UnnamedPatch}
                            {from mid1 mid2 to : NameSet}
        : NamedPatch unnamedPatch from mid1
       -> NamedPatch unnamedPatch mid1 to
       -> NamedPatch unnamedPatch from mid2
       -> NamedPatch unnamedPatch mid2 to
       -> Prop
    := MkNamedPatchCommute : forall (up  : up_type unnamedPatch) (uq  : up_type unnamedPatch)
                                    (up' : up_type unnamedPatch) (uq' : up_type unnamedPatch)
                                    (np : SignedName) (nq : SignedName)
                                    (not_equal : np <> nq)
                                    (not_inverse : np <> signedNameInverse nq)
                                    (pOK  : patchNamesOK from mid1 np)
                                    (qOK  : patchNamesOK mid1 to   nq)
                                    (q'OK : patchNamesOK from mid2 nq)
                                    (p'OK : patchNamesOK mid2 to   np),
              unnamedPatchCommute unnamedPatch up uq uq' up'
           -> namedPatchCommute (mkNamedPatch up  np pOK)
                                (mkNamedPatch uq  nq qOK)
                                (mkNamedPatch uq' nq q'OK)
                                (mkNamedPatch up' np p'OK).
Notation "<< p , q >> <~>n << q' , p' >>"
    := (namedPatchCommute p q q' p')
    (at level 60, no associativity).
(** %
\begin{Iexplanation}
Named patches do not commute with themself or their inverse.
Other than that, they commute iff their unnamed patches commute.
\end{Iexplanation}
\end{Idefinition}

\start{lemma}{named-patch-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}$
% *)
(* We have to split this into 2 parts in the coq, as we can't
   directly say that q' = q'' as they have different types. *)

Lemma NamedPatchCommuteUnique :
      forall {unnamedPatch : UnnamedPatch}
             {from mid mid' mid'' to : NameSet}
             {p   : NamedPatch unnamedPatch from mid}   {q   : NamedPatch unnamedPatch mid   to}
             {q'  : NamedPatch unnamedPatch from mid'}  {p'  : NamedPatch unnamedPatch mid'  to}
             {q'' : NamedPatch unnamedPatch from mid''} {p'' : NamedPatch unnamedPatch mid'' to},
      <<p, q>> <~>n <<q', p'>>
   -> <<p, q>> <~>n <<q'', p''>>
   -> (mid' = mid'') /\ (p' ~= p'') /\ (q' ~= q'').
Proof with auto.
intros unnamedPatch from mid mid' mid'' to p q q' p' q'' p'' commute' commute''.
dependent destruction commute'.
dependent destruction commute''.
assert (mid' = mid'').
    apply NameSetEquality.
    clear - q'OK q'OK0.
    destruct nq.
    destruct s.
        unfold patchNamesOK in *.
        inversion_clear q'OK.
        inversion_clear q'OK0.
        nameSetDec.
    unfold patchNamesOK in *.
    nameSetDec.
split...
subst.
destruct (UnnamedPatchCommuteUnique unnamedPatch H H0).
subst.
proofIrrel p'OK p'OK0.
proofIrrel q'OK q'OK0.
split...
Qed.

(** %
\begin{Iexplanation}
This is \refAxiom{unnamed-patch-commute-unique}
restated for named patches.
\end{Iexplanation}
\begin{Iproof}
If $\name{p} = \name{q}$ or $\name{p} = \name{q}^$ then $j = k = \fail$.

Otherwise the result follows from
\refAxiom{unnamed-patch-commute-unique} applied to the commute of the
unnamed patches.
\end{Iproof}
\end{Ilemma}

\start{definition}{named-patches-commutable}
We extend $\commutesName$ to relate two named patches if they are
commutable, {\ie}\\
$\commutes{p}{q} <=>
 \exists p', q' .
 \pair{p}{q} <-> \pair{q'}{p'}$
% *)
Definition namedPatchCommutable {unnamedPatch : UnnamedPatch}
                                {from mid1 to : NameSet}
                                (p : NamedPatch unnamedPatch from mid1)
                                (q : NamedPatch unnamedPatch mid1 to) : Prop
 := exists mid2 : NameSet,
    exists q' : NamedPatch unnamedPatch from mid2,
    exists p' : NamedPatch unnamedPatch mid2 to,
    <<p, q>> <~>n <<q', p'>>.
Notation "p <~?~> q" := (namedPatchCommutable p q)
    (at level 60, no associativity).

Lemma namedPatchCommutable_dec :
      forall {unnamedPatch : UnnamedPatch}
             {from mid to : NameSet}
             (p : NamedPatch unnamedPatch from mid)
             (q : NamedPatch unnamedPatch mid to),
      {mid2 : NameSet &
      { q' : NamedPatch unnamedPatch from mid2 &
      { p' : NamedPatch unnamedPatch mid2 to &
      <<p, q>> <~>n <<q', p'>> }}}
    + {~(p <~?~> q)}.
Proof with auto.
intros.
dependent destruction p.
dependent destruction q.
rename np_name0 into snp.
rename np_name1 into snq.
rename np_unnamedPatch0 into up.
rename np_unnamedPatch1 into uq.
rename np_nameOK0 into np_nameOK.
rename np_nameOK1 into nq_nameOK.
destruct (SignedNameOrderedTypeWithLeibniz.eq_dec snp snq).
    (* This is the case where the two patches have the same name *)
    right.
    intro.
    dependent destruction H.
    dependent destruction H.
    dependent destruction H.
    dependent destruction H.
    congruence.
destruct (SignedNameOrderedTypeWithLeibniz.eq_dec snp (signedNameInverse snq)).
    (* This is the case where the two patches have inverse names *)
    right.
    intro.
    dependent destruction H.
    dependent destruction H.
    dependent destruction H.
    dependent destruction H.
    congruence.
(* In the remaining cases, whether the named patches commute is
   determined by whether the unnamed patches commute *)
destruct (unnamedPatchCommutable_dec unnamedPatch up uq).
    (* This is the case where the unnamed patches commute *)
    left.
    destruct s as [uq' [up' up_uq_commute_uq'_up']].
    destruct snq as [sq nq].
    (* XXX Can we get coq to leave this for us?: *)
    set (snq := MkSignedName sq nq).
    destruct snp as [sp np].
    (* XXX Can we get coq to leave this for us?: *)
    set (snp := MkSignedName sp np).
    destruct sq.
        (* This is the case where q is a positive patch *)
        remember (NameSetAdd nq from) as oq.
        exists oq.
        assert (q'OK : patchNamesOK from oq snq).
            destruct sp.
                simpl in *.
                nameSetDec.
            simpl in *.
            assert (neq : np <> nq).
                intro.
                subst.
                congruence.
            nameSetDec.
        exists (mkNamedPatch uq' snq q'OK).
        assert (p'OK : patchNamesOK oq to snp).
            destruct sp.
                simpl in *.
                assert (neq : np <> nq).
                    intro.
                    subst.
                    congruence.
                subst. (* XXX Shouldn't be needed *)
                split.
                    clear - np_nameOK n neq.
                    nameSetDec.
                clear - np_nameOK nq_nameOK.
                nameSetDec.
            simpl in *.
            assert (neq : np <> nq).
                intro.
                subst.
                congruence.
            subst. (* XXX Shouldn't be needed *)
            split.
                clear - np_nameOK nq_nameOK n0 neq.
                nameSetDec.
            clear - np_nameOK nq_nameOK n0.
            nameSetDec.
        exists (mkNamedPatch up' snp p'OK).
        apply MkNamedPatchCommute...
    (* This is the case where q is a negative patch *)
    remember (NameSetRemove nq from) as oq.
    exists oq.
    assert (q'OK : patchNamesOK from oq snq).
        destruct sp.
            simpl in *.
            subst. (* XXX Shouldn't be needed *)
            split.
                nameSetDec.
            assert (neq : np <> nq).
                intro.
                subst.
                congruence.
            nameSetDec.
        simpl in *.
        subst. (* XXX Shouldn't be needed *)
        split.
            nameSetDec.
        nameSetDec.
    exists (mkNamedPatch uq' snq q'OK).
    assert (p'OK : patchNamesOK oq to snp).
        destruct sp.
            simpl in *.
            subst. (* XXX Shouldn't be needed *)
            split.
                nameSetDec.
            destruct np_nameOK as [? HX1].
            destruct nq_nameOK as [? HX2].
            destruct q'OK as [? HX3].
            assert (HX4 : NameSetIn nq from).
                clear - HX3.
                nameSetDec.
            assert (neq : np <> nq).
                congruence.
            clear - neq HX1 HX2 H0.
            nameSetDec.
        simpl in *.
        subst. (* XXX Shouldn't be needed *)
        split.
            nameSetDec.
        destruct np_nameOK as [? HX1].
        destruct nq_nameOK as [? HX2].
        clear - H HX1 H0 HX2.
        nameSetDec.
    exists (mkNamedPatch up' snp p'OK).
    apply MkNamedPatchCommute...
(* This is the case where the unnamed patches do not commute *)
right.
intro.
dependent destruction H.
dependent destruction H.
dependent destruction H.
dependent destruction H.
assert (up <~?~>u uq).
    unfold unnamedPatchCommutable.
    exists uq'.
    exists up'...
congruence.
Qed.
(** %
\end{Idefinition}
*)

Instance NamedPartPatchUniverse (unnamedPatch : UnnamedPatch)
         : PartPatchUniverse (NamedPatch unnamedPatch) (NamedPatch unnamedPatch)
    := mkPartPatchUniverse
           (NamedPatch unnamedPatch)
           (NamedPatch unnamedPatch)
           (@namedPatchCommute _)
           (@namedPatchCommutable_dec _)
           (@NamedPatchCommuteUnique _).

(** %
\start{lemma}{named-patch-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}$
% *)
Lemma NamedPatchCommuteSelfInverse :
      forall {unnamedPatch : UnnamedPatch}
             {from mid1 mid2 to : NameSet}
             {p : NamedPatch unnamedPatch from mid1}
             {q : NamedPatch unnamedPatch mid1 to}
             {q' : NamedPatch unnamedPatch from mid2}
             {p' : NamedPatch unnamedPatch mid2 to}
             (namedCommute : <<p,  q>>  <~> <<q', p'>>),
      (<<q',  p'>>  <~> <<p, q>>).
Proof with auto.
intros.
destruct namedCommute.
apply UnnamedPatchCommuteSelfInverse in H.
simpl commute.
apply MkNamedPatchCommute...
intro.
elim not_inverse.
apply namesInverseInjective.
rewrite nameInverseInverse...
Qed.
(** %
\begin{Iexplanation}
This is \refAxiom{unnamed-patch-commute-self-inverse}
restated for named patches.
\end{Iexplanation}
\begin{Iproof}
If $\name{p} = \name{q}$ or $\name{p} = \name{q}^$ then both commutes
fail, so the result holds.

Otherwise the result follows from
\refAxiom{unnamed-patch-commute-self-inverse} applied to the commute of
the unnamed patches.
\end{Iproof}
\end{Ilemma}

\start{lemma}{named-patch-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 \refAxiom{unnamed-patch-commute-square}
restated for named patches.
\end{Iexplanation}
\begin{Iproof}
If $\name{p} = \name{q}$ or $\name{p} = \name{q}^$ then both commutes
fail, so the result holds.

Otherwise the result follows from
\refAxiom{unnamed-patch-commute-square} applied to the commute of
the unnamed patches.
\end{Iproof}
% *)

(* XXX Move this somewhere more general *)
Lemma monotonicNeq : forall {t u : Set}
                            (f : t -> u)
                            (x y : t),
                     (f x <> f y)
                  -> (x <> y).
Proof.
intros.
intro.
elim H.
subst.
auto.
Qed.

Instance NamedPatchUniverseInv
               {unnamedPatch : UnnamedPatch}
               (namedPartPatchUniverse : PartPatchUniverse
                                             (NamedPatch unnamedPatch)
                                             (NamedPatch unnamedPatch))
             : PatchUniverseInv (NamedPartPatchUniverse unnamedPatch)
                                (NamedPartPatchUniverse unnamedPatch)
    := mkPatchUniverseInv
           (NamedPatch unnamedPatch)
           (NamedPatch unnamedPatch)
           (NamedPartPatchUniverse unnamedPatch)
           (NamedPartPatchUniverse unnamedPatch)
           (@NamedPatchCommuteSelfInverse unnamedPatch).

(** %
\end{Ilemma}
% *)

(* XXX NamedPatchCommuteConsistent[12] copy/pasted from
       patch_sequences without the accompanying text *)

Lemma NamedPatchCommuteConsistent1 :
      forall {unnamedPatch : UnnamedPatch}
             {o op opq opqr opr oq oqr : NameSet}
             {p1 : NamedPatch unnamedPatch o op}
             {q1 : NamedPatch unnamedPatch op opq}
             {r1 : NamedPatch unnamedPatch opq opqr}
             {q2 : NamedPatch unnamedPatch opr opqr}
             {r2 : NamedPatch unnamedPatch op opr}
             {q3 : NamedPatch unnamedPatch o oq}
             {r3 : NamedPatch unnamedPatch oq oqr}
             {p3 : NamedPatch unnamedPatch oqr opqr}
             {p5 : NamedPatch unnamedPatch oq opq},
      <<q1, r1>> <~> <<r2, q2>>
   -> <<p1, q1>> <~> <<q3, p5>>
   -> <<p5, r1>> <~> <<r3, p3>>
   -> (exists or : NameSet,
       (exists r4 : NamedPatch unnamedPatch o or,
        (exists q4 : NamedPatch unnamedPatch or oqr,
         (exists p6 : NamedPatch unnamedPatch or opr,
          <<q3, r3>> <~> <<r4, q4>> /\
          <<p1, r2>> <~> <<r4, p6>> /\
          <<p6, q2>> <~> <<q4, p3>>)))).
Proof with auto.
intros unnamedPatch o op opq opqr opr oq oqr p1 q1 r1 q2 r2 q3 r3 p3 p5
       q1_r1_commutes_r2_q2
       p1_q1_commutes_q3_p5
       p5_r1_commutes_r2_p3.
simpl commute in *.
dependent destruction q1_r1_commutes_r2_q2.
dependent destruction p1_q1_commutes_q3_p5.
dependent destruction p5_r1_commutes_r2_p3.
rename nq into nr.
rename np into nq.
rename np0 into np.
destruct np as [sp np].
destruct nq as [sq nq].
destruct nr as [sr nr].
(* XXX Can we get coq to leave these for us?: *)
set (snr := MkSignedName sr nr).
set (snq4 := MkSignedName sq nq).
set (snp6 := MkSignedName sp np).
destruct (UnnamedPatchCommuteConsistent1 _ H H0 H1)
  as [r4 [q4 [p6 [H3 [H4 H5]]]]].
destruct sr.
    (* This is the case where r is a positive patch *)
    remember (NameSetAdd nr o) as or.
    exists or.
    assert (snrPatchNamesOK : patchNamesOK o or snr).
        subst.
        simpl in *.
        split.
            clear - q'OK pOK0 not_equal1 not_inverse1.
            destruct sp.
                nameSetDec.
            assert (neq : nr <> np).
                congruence.
            nameSetDec.
        clear.
        nameSetDec.
    exists (mkNamedPatch r4 snr snrPatchNamesOK).
    assert (q4PatchNamesOK : patchNamesOK or oqr snq4).
        subst.
        simpl in *.
        destruct sq.
            split.
                clear - not_equal q'OK0.
                assert (neq : nr <> nq).
                    congruence.
                nameSetDec.
            clear - q'OK1 q'OK0.
            nameSetDec.
        split.
            clear - not_inverse q'OK1 q'OK0.
            assert (neq : nr <> nq).
                congruence.
            nameSetDec.
        clear - not_inverse q'OK1 q'OK0.
        nameSetDec.
    exists (mkNamedPatch q4 snq4 q4PatchNamesOK).
    assert (p6PatchNamesOK : patchNamesOK or opr snp6).
        subst.
        simpl in *.
        destruct sp.
            split.
                clear - pOK0 not_equal1.
                assert (neq : np <> nr).
                    congruence.
                nameSetDec.
            clear - q'OK pOK0.
            nameSetDec.
        split.
            clear - pOK0 q'OK not_inverse1.
            assert (neq : np <> nr).
                congruence.
            nameSetDec.
        clear - pOK0 q'OK not_inverse1.
        nameSetDec.
    exists (mkNamedPatch p6 snp6 p6PatchNamesOK).
    split.
        apply MkNamedPatchCommute...
    split.
        apply MkNamedPatchCommute...
    apply MkNamedPatchCommute...
(* This is the case where r is a negative patch *)
remember (NameSetRemove nr o) as or.
exists or.
assert (snrPatchNamesOK : patchNamesOK o or snr).
    subst.
    simpl in *.
    split.
        clear.
        nameSetDec.
    assert (HX : NameSetIn nr o).
        clear - q'OK pOK0 not_equal1 not_inverse1.
        destruct sp.
            assert (neq : np <> nr).
                congruence.
            nameSetDec.
        nameSetDec.
    clear - HX.
    nameSetDec.
exists (mkNamedPatch r4 snr snrPatchNamesOK).
assert (q4PatchNamesOK : patchNamesOK or oqr snq4).
    subst.
    simpl in *.
    destruct sq.
        split.
            clear - q'OK0.
            nameSetDec.
        clear - not_inverse q'OK1 q'OK0.
        assert (neq : nr <> nq).
            congruence.
        nameSetDec.
    split.
        clear - q'OK1 q'OK0.
        nameSetDec.
    clear - q'OK1 q'OK0.
    nameSetDec.
exists (mkNamedPatch q4 snq4 q4PatchNamesOK).
assert (p6PatchNamesOK : patchNamesOK or opr snp6).
    subst.
    simpl in *.
    destruct sp.
        split.
            clear - pOK0.
            nameSetDec.
        clear - q'OK pOK0 not_inverse1.
        assert (neq : np <> nr).
            congruence.
        nameSetDec.
    split.
        clear - pOK0 q'OK.
        nameSetDec.
    clear - pOK0 q'OK.
    nameSetDec.
exists (mkNamedPatch p6 snp6 p6PatchNamesOK).
split.
    apply MkNamedPatchCommute...
split.
    apply MkNamedPatchCommute...
apply MkNamedPatchCommute...
Qed.

Lemma NamedPatchCommuteConsistent2 :
      forall {unnamedPatch : UnnamedPatch}
             {o op opq opqr or oq oqr : NameSet}
             {q3 : NamedPatch unnamedPatch o oq}
             {r3 : NamedPatch unnamedPatch oq oqr}
             {p3 : NamedPatch unnamedPatch oqr opqr}
             {q4 : NamedPatch unnamedPatch or oqr}
             {r4 : NamedPatch unnamedPatch o or}
             {p1 : NamedPatch unnamedPatch o op}
             {q1 : NamedPatch unnamedPatch op opq}
             {r1 : NamedPatch unnamedPatch opq opqr}
             {p5 : NamedPatch unnamedPatch oq opq},
      <<q3, r3>> <~> <<r4, q4>>
   -> <<r3, p3>> <~> <<p5, r1>>
   -> <<q3, p5>> <~> <<p1, q1>>
   -> (exists opr : NameSet,
       (exists r2 : NamedPatch unnamedPatch op opr,
        (exists q2 : NamedPatch unnamedPatch opr opqr,
         (exists p6 : NamedPatch unnamedPatch or opr,
          <<q1, r1>> <~> <<r2, q2>> /\
          <<q4, p3>> <~> <<p6, q2>> /\
          <<r4, p6>> <~> <<p1, r2>>)))).
Proof with auto.
intros.
simpl commute in *.
dependent destruction H.
dependent destruction H0.
dependent destruction H1.
rename nq into nr.
rename np into nq.
rename nq0 into np.
destruct np as [sp np].
destruct nq as [sq nq].
destruct nr as [sr nr].
(* XXX Can we get coq to leave this for us?: *)
set (snr2 := MkSignedName sr nr).
set (snq2 := MkSignedName sq nq).
set (snp6 := MkSignedName sp np).
destruct (UnnamedPatchCommuteConsistent2 _ H H0 H1)
  as [ur2 [uq2 [up6 [? [? ?]]]]].
destruct sr.
    (* This is the case where r is a positive patch *)
    remember (NameSetAdd nr op) as opr.
    exists opr.
    assert (snrPatchNamesOK : patchNamesOK op opr snr2).
        subst.
        simpl in *.
        split.
            clear - q'OK q'OK1 not_equal0 not_inverse0.
            destruct sp.
                assert (neq : np <> nr).
                    congruence.
                nameSetDec.
            nameSetDec.
        nameSetDec.
    exists (mkNamedPatch ur2 snr2 snrPatchNamesOK).
    assert (q2PatchNamesOK : patchNamesOK opr opqr snq2).
        subst.
        simpl in *.
        destruct sq.
            split.
                clear - not_equal p'OK1.
                assert (neq : nq <> nr).
                    congruence.
                nameSetDec.
            clear - p'OK0 p'OK1.
            nameSetDec.
        split.
            clear - not_inverse p'OK1 p'OK0.
            assert (neq : nq <> nr).
                congruence.
            nameSetDec.
        clear - not_inverse p'OK1 p'OK0.
        nameSetDec.
    exists (mkNamedPatch uq2 snq2 q2PatchNamesOK).
    assert (p6PatchNamesOK : patchNamesOK or opr snp6).
        subst.
        simpl in *.
        destruct sp.
            split.
                clear - q'OK q'OK1 not_equal0.
                assert (neq : np <> nr).
                    congruence.
                nameSetDec.
            clear - q'OK q'OK1.
            nameSetDec.
        split.
            clear - q'OK1 not_inverse0.
            assert (neq : np <> nr).
                congruence.
            nameSetDec.
        clear - q'OK q'OK1 not_inverse0.
        nameSetDec.
    exists (mkNamedPatch up6 snp6 p6PatchNamesOK).
    split.
        apply MkNamedPatchCommute...
    split.
        apply MkNamedPatchCommute...
    apply MkNamedPatchCommute...
(* This is the case where r is a negative patch *)
remember (NameSetRemove nr op) as opr.
exists opr.
assert (snrPatchNamesOK : patchNamesOK op opr snr2).
    subst.
    simpl in *.
    split.
        clear.
        nameSetDec.
    assert (HX : NameSetIn nr op).
        clear - q'OK1 q'OK not_equal0 not_inverse0.
        destruct sp.
            nameSetDec.
        assert (neq : np <> nr).
            congruence.
        nameSetDec.
    clear - HX.
    nameSetDec.
exists (mkNamedPatch ur2 snr2 snrPatchNamesOK).
assert (q2PatchNamesOK : patchNamesOK opr opqr snq2).
    subst.
    simpl in *.
    destruct sq.
        split.
            clear - p'OK1.
            nameSetDec.
        clear - p'OK0 p'OK1 not_inverse.
        assert (neq : nq <> nr).
            congruence.
        nameSetDec.
    split.
        clear - p'OK1 p'OK0.
        nameSetDec.
    clear - p'OK1 p'OK0.
    nameSetDec.
exists (mkNamedPatch uq2 snq2 q2PatchNamesOK).
assert (p6PatchNamesOK : patchNamesOK or opr snp6).
    subst.
    simpl in *.
    destruct sp.
        split.
            clear - q'OK q'OK1.
            nameSetDec.
        clear - q'OK q'OK1 not_inverse0.
        nameSetDec.
    split.
        clear - q'OK1.
        nameSetDec.
    assert (HX : NameSetIn nr op).
        clear - snrPatchNamesOK.
        nameSetDec.
    clear - q'OK q'OK1 HX.
    nameSetDec.
exists (mkNamedPatch up6 snp6 p6PatchNamesOK).
split.
    apply MkNamedPatchCommute...
split.
    apply MkNamedPatchCommute...
apply MkNamedPatchCommute...
Qed.

(* XXX unused: *)
Lemma NamedPatchContexts : forall {unnamedPatch : UnnamedPatch}
                                  {from to : NameSet}
                                  (p : NamedPatch unnamedPatch from to),
                           patchNamesOK from to (np_name p).
Proof with auto.
intros.
destruct p.
unfold np_name.
unfold patchNamesOK in *.
destruct np_name0.
destruct s; split; nameSetDec.
Qed.

Lemma NamedPatchCommuteNames :
      forall {unnamedPatch : UnnamedPatch}
             {from mid1 mid2 to : NameSet}
             {p  : NamedPatch unnamedPatch from mid1} {q  : NamedPatch unnamedPatch mid1 to}
             {q' : NamedPatch unnamedPatch from mid2} {p' : NamedPatch unnamedPatch mid2 to},
      << p , q >> <~> << q' , p' >>
   -> (np_name p = np_name p') /\
      (np_name q = np_name q') /\
      (np_name p <> np_name q).
Proof with auto.
intros.
destruct H.
unfold np_name...
Qed.

Instance NamedPatchUniverse {unnamedPatch : UnnamedPatch}
                              {namedPartPatchUniverse : PartPatchUniverse (NamedPatch unnamedPatch) (NamedPatch unnamedPatch)}
                              (namedPatchUniverseInv : PatchUniverseInv
                                                             (NamedPartPatchUniverse unnamedPatch)
                                                             (NamedPartPatchUniverse unnamedPatch))
 : PatchUniverse (NamedPatchUniverseInv namedPartPatchUniverse)
    := mkPatchUniverse
           (NamedPatch unnamedPatch)
           (NamedPartPatchUniverse unnamedPatch)
           (NamedPatchUniverseInv namedPartPatchUniverse)
           (@np_name _)
           (@NamedPatchCommuteConsistent1 _)
           (@NamedPatchCommuteConsistent2 _)
           (@NamedPatchCommuteNames _).

Lemma NamedPatchInvertInverse :
      forall {unnamedPatch : UnnamedPatch}
             {from to : NameSet}
             (p : NamedPatch unnamedPatch from to),
      (p^n)^n = p.
Proof with auto.
intros.
destruct p.
unfold namedPatchInverse.
simpl.
rewrite unnamedPatchInvertInverse.
destruct np_name0.
destruct s.
    simpl.
    f_equal.
    apply proof_irrelevance.
simpl.
f_equal.
apply proof_irrelevance.
Qed.

Lemma NamedPatchNameOfInverse
          {unnamedPatch : UnnamedPatch}
          {from to : NameSet}
          (p : NamedPatch unnamedPatch from to)
      : np_name (p ^n) = signedNameInverse (np_name p).
Proof.
auto.
Qed.

Instance NamedInvertiblePatchlike (unnamedPatch : UnnamedPatch)
 : InvertiblePatchlike (NamedPatch unnamedPatch)
    := mkInvertiblePatchlike
           (NamedPatch unnamedPatch)
           (@namedPatchInverse _)
           (@NamedPatchInvertInverse _).

Lemma NamedPatchCommuteSquare :
      forall {unnamedPatch : UnnamedPatch}
             {o op oq opq : NameSet}
             {p  : NamedPatch unnamedPatch o  op}
             {q  : NamedPatch unnamedPatch op opq}
             {q' : NamedPatch unnamedPatch o  oq}
             {p' : NamedPatch unnamedPatch oq opq},
      <<p, q>> <~> <<q', p'>> ->
      << q'^, p>> <~> <<p', q^>>.
Proof with auto.
intros.
destruct H.
apply UnnamedPatchCommuteSquare in H.
constructor.
        simpl...
    simpl.
    apply (monotonicNeq signedNameInverse).
    rewrite nameInverseInverse.
    rewrite nameInverseInverse...
simpl...
Qed.

Instance NamedCommuteSquare
               (unnamedPatch : UnnamedPatch)
 : CommuteSquare (NamedPatch unnamedPatch) (NamedPatch unnamedPatch)
    := mkCommuteSquare
           (NamedPatch unnamedPatch)
           (NamedPatch unnamedPatch)
           _
           _
           _
           (@NamedPatchCommuteSquare _).

Instance NamedInvertiblePatchUniverse
               {unnamedPatch : UnnamedPatch}
               {namedPartPatchUniverse : PartPatchUniverse (NamedPatch unnamedPatch) (NamedPatch unnamedPatch)}
               {namedPatchUniverseInv : PatchUniverseInv (NamedPartPatchUniverse unnamedPatch) (NamedPartPatchUniverse unnamedPatch)}
 : InvertiblePatchUniverse
       (NamedPatchUniverse namedPatchUniverseInv)
       (NamedInvertiblePatchlike unnamedPatch)
    := mkInvertiblePatchUniverse
           (NamedPatch unnamedPatch)
           (NamedPartPatchUniverse unnamedPatch)
           (NamedPatchUniverseInv namedPartPatchUniverse)
           (NamedPatchUniverse namedPatchUniverseInv)
           (NamedInvertiblePatchlike unnamedPatch)
           (@NamedPatchNameOfInverse _).

End named_patches.