(** %
\section{\label{sec:XXX}XXX}
% *)

Require Import Arith.
Require Import Compare_dec.
Require Import Equality.
Require Import Setoid.

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

Reserved Notation "<< p , qs >> <~>om << qs' , p' >>"
    (at level 60, no associativity).
Inductive OneManyCommute
             {T : NameSet -> NameSet -> Type}
             {ppu : PartPatchUniverse T T}
             {pui : PatchUniverseInv ppu ppu}
             {pu : PatchUniverse pui}
           : forall {from mid1 mid2 to}
                    (p : T from mid1)
                    (qs : Sequence pu mid1 to)
                    (qs' : Sequence pu from mid2)
                    (p' : T mid2 to),
             Prop
    := NilOneManyCommute : forall {from to : NameSet}
                                  (p : T from to),
                           <<p, []>> <~>om <<[], p>>
     | ConsOneManyCommute : forall {from mid1 mid2 mid1' mid2' to : NameSet}
                                   {p : T from mid1}
                                   {q : T mid1 mid2}
                                   {qs : Sequence pu mid2 to}
                                   {p'' : T mid1' mid2}
                                   {q' : T from mid1'}
                                   {qs' : Sequence pu mid1' mid2'}
                                   {p' : T mid2' to}
                                   {consOK : ConsOK q qs}
                                   {consOK : ConsOK q' qs'}
                                   (commutePQ : << p, q >> <~> << q', p'' >>)
                                   (commutePQs : << p'', qs >> <~>om << qs', p' >>),
                            <<p, (q :> qs)>> <~>om <<(q' :> qs'), p'>>
where "<< p , qs >> <~>om << qs' , p' >>"
    := (@OneManyCommute _ _ _ _ _ _ _ _ p qs qs' p').

Lemma OneManyCommuteNames
             {pu_type : NameSet -> NameSet -> Type}
             {ppu : PartPatchUniverse pu_type pu_type}
             {pui : PatchUniverseInv ppu ppu}
             {pu : PatchUniverse pui}
             {from mid mid' to : NameSet}
             {p : pu_type from mid}
             {qs : Sequence pu mid to}
             {qs' : Sequence pu from mid'}
             {p' : pu_type mid' to}
             (p_qs_commute_qs'_p' : <<p, qs>> <~>om <<qs', p'>>)
           : pu_nameOf p = pu_nameOf p' /\ sequenceContents qs = sequenceContents qs'.
Proof with auto.
destruct qs as [qs qsSequenceOK].
destruct qs' as [qs' qs'SequenceOK].
dependent induction qs generalizing from p qs' qs'SequenceOK p_qs_commute_qs'_p'.
    dependent destruction p_qs_commute_qs'_p'.
        unfold sequenceContents...
    rewrite NilSeqToNil in x0.
    contradiction (ConsEqNil x0).
dependent destruction p_qs_commute_qs'_p'.
destruct qs'.
    rewrite NilSeqToNil in x.
    contradiction (ConsEqNil x).

consSeqToCons p qs.
consSeqToCons p1 qs'.
consEquality x0.
consEquality x.
rewrite SequenceContentsCons.
rewrite SequenceContentsCons.
destruct (commuteNames commutePQ) as [H_p_eq [H_q_eq H_p_q_neq]].
rewrite H_q_eq.
specialize (IHqs psSequenceOK).
specialize (IHqs p').
specialize (IHqs mid0).
specialize (IHqs p'').
specialize (IHqs qs').
specialize (IHqs psSequenceOK0).
specialize (IHqs p_qs_commute_qs'_p').
unfold block in IHqs.
destruct IHqs as [pNames qsNames].
rewrite pNames in H_p_eq.
rewrite H_p_eq.
rewrite qsNames...
Qed.

Module impl.

Definition OneManyCommutable
             {T : NameSet -> NameSet -> Type}
             {ppu : PartPatchUniverse T T}
             {pui : PatchUniverseInv ppu ppu}
             {pu : PatchUniverse pui}
             {from mid1 to}
             (p : T from mid1)
             (qs : Sequence pu mid1 to)
           : Prop
 := exists mid2 : NameSet,
    exists qs' : Sequence pu from mid2,
    exists p' : T mid2 to,
    <<p, qs>> <~>om <<qs', p'>>.
Notation "p <~?~>om qs" := (OneManyCommutable p qs)
    (at level 60, no associativity).

Lemma OneManyCommutable_dec
             {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)
           : { mid2 : NameSet &
             { qs' : Sequence pu from mid2 &
             { p' : pu_type mid2 to &
             <<p, qs>> <~>om <<qs', p'>> }}}
           + {~(p <~?~>om qs)}.
Proof with auto.
destruct qs as [qs qsSequenceOK].
dependent induction qs generalizing from p.
    left.
    exists from.
    exists [].
    exists p.
    rewrite NilSeqToNil.
    apply NilOneManyCommute.
rename p0 into q.
destruct (commutable_dec q p).
    destruct (ConsSeqToCons p qs) as [qsSequenceOK' [qQsConsOK qQsEquality]].
    rewrite qQsEquality.
    destruct s as [mid' [q' [p' p_q_commute_q'_p']]].
    specialize (IHqs qsSequenceOK').
    specialize (IHqs mid').
    specialize (IHqs p').
    unfold block in IHqs.
    dependent destruction IHqs.
        left.
        destruct s as [mid'' [qs' [p'' p_qs_commute_qs'_p'']]].
        exists mid''.
        assert (q'qs'consOK : ConsOK q' qs').
            constructor.
            destruct qsSequenceOK.
            destruct sequenceNoDupes0.
            destruct (commuteNames p_q_commute_q'_p') as [pNames [qNames pQNames]].
            rewrite <- qNames.
            destruct (OneManyCommuteNames p_qs_commute_qs'_p'') as [? qsNamesEq].
            rewrite <- qsNamesEq.
            unfold sequenceContents...
        exists (q' :> qs').
        exists p''.
        apply (ConsOneManyCommute p_q_commute_q'_p' p_qs_commute_qs'_p'').
    right.
    intro omcommute.
    elim n.
    destruct omcommute as [? [? [? omcommute]]].
    dependent destruction omcommute.
    consEquality x.
    doCommuteUnique p_q_commute_q'_p' commutePQ.
    exists mid2'.
    exists qs'.
    exists p'0...
right.
intro omcommute.
elim n.
destruct omcommute as [? [? [? omcommute]]].
dependent destruction omcommute.
consSeqToCons p qs.
consEquality x.
exists mid1'.
exists q'.
exists p''...
Qed.

Lemma OneManyCommuteUnique {pu_type : NameSet -> NameSet -> Type}
                           {ppu : PartPatchUniverse pu_type pu_type}
                           {pui : PatchUniverseInv ppu ppu}
                           {pu : PatchUniverse pui}
                           {from mid mid' mid'' to : NameSet}
                           {p : pu_type from mid}
                           {qs : Sequence pu mid to}
                           {qs' : Sequence pu from mid'}
                           {p' : pu_type mid' to}
                           {qs'' : Sequence pu from mid''}
                           {p'' : pu_type mid'' to}
                           (commute1 : <<p, qs>> <~>om <<qs', p'>>)
                           (commute2 : <<p, qs>> <~>om <<qs'', p''>>)
                         : (mid' = mid'') /\ p' ~= p'' /\ qs' ~= qs''.
Proof with auto.
destruct qs as [qs qsSequenceOK].
destruct qs' as [qs' qs'SequenceOK].
destruct qs'' as [qs'' qs''SequenceOK].
dependent induction qs generalizing from p qs' qs'' qs'SequenceOK qs''SequenceOK commute1 commute2.
    dependent destruction commute1.
        dependent destruction commute2.
            split...
            split...
            proofIrrel qs'SequenceOK qs''SequenceOK...
        rewrite NilSeqToNil in x1.
        contradiction (ConsEqNil x1).
    rewrite NilSeqToNil in x0.
    contradiction (ConsEqNil x0).
consSeqToCons p qs.
dependent destruction commute1.
consEquality x0.
dependent destruction commute2.
consEquality x1.
doCommuteUnique commutePQ commutePQ0.
destruct qs'0.
destruct qs'1.
specialize (IHqs psSequenceOK).
specialize (IHqs p').
specialize (IHqs p'0).
specialize (IHqs mid1').
specialize (IHqs p''0).
specialize (IHqs s).
specialize (IHqs s0).
specialize (IHqs sequenceOK).
specialize (IHqs sequenceOK0).
specialize (IHqs commute1).
specialize (IHqs commute2).
unfold block in IHqs.
destruct IHqs as [? [? ?]].
split...
split...
subst.
apply JMeq_eq in H1.
inversion H1.
subst.
proofIrrel sequenceOK sequenceOK0.
proofIrrel consOK0 consOK1.
rewrite x0 in x.
rewrite x...
Qed.

End impl.

Instance OneManyPartPatchUniverse
             {T : NameSet -> NameSet -> Type}
             {ppu : PartPatchUniverse T T}
             {pui : PatchUniverseInv ppu ppu}
             {pu : PatchUniverse pui}
           : PartPatchUniverse
                 T
                 (Sequence pu)
    := mkPartPatchUniverse
           T
           (Sequence pu)
           (@OneManyCommute _ _ _ _)
           (@impl.OneManyCommutable_dec _ _ _ _)
           (@impl.OneManyCommuteUnique _ _ _ _).

Lemma OneManyCommuteNil
          {T : NameSet -> NameSet -> Type}
          {ppu : PartPatchUniverse T T}
          {pui : PatchUniverseInv ppu ppu}
          {pu : PatchUniverse pui}
          {from to : NameSet}
          (p : T from to)
        : <<p, []>> <~> <<[], p>>.
Proof.
simpl commute.
apply NilOneManyCommute.
Qed.