(** %
\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 "<< ps , q >> <~>mo << q' , ps' >>"
    (at level 60, no associativity).
Inductive ManyOneCommute
             {T : NameSet -> NameSet -> Type}
             {ppu : PartPatchUniverse T T}
             {pui : PatchUniverseInv ppu ppu}
             {pu : PatchUniverse pui}
           : forall {from mid1 mid2 to}
                    (qs : Sequence pu from mid1)
                    (p : T mid1 to)
                    (p' : T from mid2)
                    (qs' : Sequence pu mid2 to),
             Prop
    := NilManyOneCommute : forall {from to : NameSet}
                                  (p : T from to),
                           <<[], p>> <~>mo <<p, []>>
     | ConsManyOneCommute : forall {from mid1 mid2 mid1' mid2' to : NameSet}
                                   {p : T from mid1}
                                   {ps : Sequence pu mid1 mid2}
                                   {q : T mid2 to}
                                   {ps' : Sequence pu mid2' to}
                                   {q'' : T mid1 mid2'}
                                   {p' : T mid1' mid2'}
                                   {q' : T from mid1'}
                                   {consOK : ConsOK p ps}
                                   {consOK : ConsOK p' ps'}
                                   (commutePsQ : << ps, q >> <~>mo << q'', ps' >>)
                                   (commutePQ : << p, q'' >> <~> << q', p' >>),
                            <<(p :> ps), q>> <~>mo <<q', (p' :> ps')>>
where "<< ps , q >> <~>mo << q' , ps' >>"
    := (@ManyOneCommute _ _ _ _ _ _ _ _ ps q q' ps').

Lemma ManyOneCommuteNames
             {pu_type : NameSet -> NameSet -> Type}
             {ppu : PartPatchUniverse pu_type pu_type}
             {pui : PatchUniverseInv ppu ppu}
             {pu : PatchUniverse pui}
             {from mid mid' to : NameSet}
             {ps : Sequence pu from mid}
             {q : pu_type mid to}
             {q' : pu_type from mid'}
             {ps' : Sequence pu mid' to}
             (ps_q_commute_q'_ps' : <<ps, q>> <~>mo <<q', ps'>>)
           : sequenceContents ps = sequenceContents ps'
          /\ pu_nameOf q = pu_nameOf q'.
Proof with auto.
destruct ps as [ps psSequenceOK].
destruct ps' as [ps' ps'SequenceOK].
unfold sequenceContents.
dependent induction ps generalizing mid' q' ps' ps'SequenceOK ps_q_commute_q'_ps'.
    dependent destruction ps_q_commute_q'_ps'...
    rewrite NilSeqToNil in x0.
    contradiction (ConsEqNil x0).
dependent destruction ps_q_commute_q'_ps'.
destruct ps'.
    rewrite NilSeqToNil in x.
    contradiction (ConsEqNil x).
consSeqToCons p ps.
consSeqToCons p1 ps'.
consEquality x0.
consEquality x.
rewrite SequenceContentsBaseCons.
rewrite SequenceContentsBaseCons.
destruct (commuteNames commutePQ) as [H_p_eq [H_q_eq H_p_q_neq]].
rewrite H_p_eq.
specialize (IHps psSequenceOK0).
specialize (IHps q).
specialize (IHps mid0).
specialize (IHps q'').
specialize (IHps ps').
specialize (IHps psSequenceOK1).
specialize (IHps ps_q_commute_q'_ps').
unfold block in IHps.
destruct IHps as [psNames qNames].
move psNames at bottom.
move qNames at bottom.
rewrite qNames.
rewrite H_q_eq.
rewrite psNames...
Qed.

Module impl.

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

Lemma ManyOneCommuteUnique {pu_type : NameSet -> NameSet -> Type}
                           {ppu : PartPatchUniverse pu_type pu_type}
                           {pui : PatchUniverseInv ppu ppu}
                           {pu : PatchUniverse pui}
                           {from mid mid' mid'' to : NameSet}
                           {ps : Sequence pu from mid}
                           {q : pu_type mid to}
                           {q' : pu_type from mid'}
                           {ps' : Sequence pu mid' to}
                           {q'' : pu_type from mid''}
                           {ps'' : Sequence pu mid'' to}
                           (commute1 : <<ps, q>> <~>mo <<q', ps'>>)
                           (commute2 : <<ps, q>> <~>mo <<q'', ps''>>)
                         : (mid' = mid'') /\ ps' ~= ps'' /\ q' ~= q''.
Proof with auto.
destruct ps as [ps psSequenceOK].
destruct ps' as [ps' ps'SequenceOK].
destruct ps'' as [ps'' ps''SequenceOK].
dependent induction ps generalizing mid' mid'' ps' ps'' q' q'' ps'SequenceOK ps''SequenceOK commute1 commute2.
(* generalizing from p qs' qs'' qs'SequenceOK qs''SequenceOK commute1 commute2. *)
    dependent destruction commute1.
        dependent destruction commute2.
            split...
            split...
            proofIrrel ps'SequenceOK ps''SequenceOK...
        rewrite NilSeqToNil in x1.
        contradiction (ConsEqNil x1).
    rewrite NilSeqToNil in x0.
    contradiction (ConsEqNil x0).
consSeqToCons p ps.
dependent destruction commute1.
consEquality x0.
dependent destruction commute2.
consEquality x1.
specialize (IHps psSequenceOK0).
specialize (IHps q).
specialize (IHps mid2').
specialize (IHps mid2'0).
destruct ps'0 as [ps'0 ps'0SequenceOK].
destruct ps'1 as [ps'1 ps'1SequenceOK].
specialize (IHps ps'0).
specialize (IHps ps'1).
specialize (IHps q''0).
specialize (IHps q'').
specialize (IHps ps'0SequenceOK).
specialize (IHps ps'1SequenceOK).
specialize (IHps commute1).
specialize (IHps commute2).
unfold block in IHps.
destruct IHps as [? [? ?]].
subst.
subst.
doCommuteUnique commutePQ commutePQ0.
apply JMeq_eq in H0.
inversion H0.
subst.
proofIrrel ps'0SequenceOK ps'1SequenceOK.
proofIrrel consOK0 consOK1.
rewrite x0 in x.
rewrite x.
split...
Qed.

Lemma ManyOneCommutable_dec
             {pu_type : NameSet -> NameSet -> Type}
             {ppu : PartPatchUniverse pu_type pu_type}
             {pui : PatchUniverseInv ppu ppu}
             {pu : PatchUniverse pui}
             {from mid to : NameSet}
             (ps : Sequence pu from mid)
             (q : pu_type mid to)
           : { mid2 : NameSet &
             { q' : pu_type from mid2 &
             { ps' : Sequence pu mid2 to &
             <<ps, q>> <~>mo <<q', ps'>> }}}
           + {~(ps <~?~>mo q)}.
Proof with auto.
destruct ps as [ps psSequenceOK].
dependent induction ps.
    left.
    exists to.
    exists q.
    exists [].
    rewrite NilSeqToNil.
    apply NilManyOneCommute.
consSeqToCons p ps.
specialize (IHps psSequenceOK0).
specialize (IHps q).
unfold block in IHps.
destruct IHps as [[mid1 [q' [ps' commuteX]]] | no].
    destruct (commutable_dec p q').
        left.
        destruct s as [? [? [? ?]]].
        exists x.
        exists x0.
        destruct ps'.
        assert (x1_s_ConsOK : ConsOK x1 (MkSequence s sequenceOK)).
            destruct (ManyOneCommuteNames commuteX).
            unfold sequenceContents in H.
            constructor.
            unfold sequenceContents.
            rewrite <- H.
            destruct (commuteNames c) as [? [? ?]].
            rewrite <- H1.
            destruct psSequenceOK.
            destruct sequenceNoDupes0...
        exists (x1 :> MkSequence s sequenceOK).
        apply (ConsManyOneCommute commuteX c).
    right.
    intro.
    destruct H as [? [? [? commuteY]]].
    dependent destruction commuteY.
    consEquality x.
    elim n.
    destruct (ManyOneCommuteUnique commuteX commuteY) as [? [? ?]].
    subst.
    subst.
    exists mid1'.
    exists q'0.
    exists p'...
right.
intro.
destruct H as [? [? [? commuteX]]].
dependent destruction commuteX.
consEquality x.
elim no.
exists mid2'.
exists q''.
exists ps'...
Qed.

End impl.

Instance ManyOnePartPatchUniverse
             {T : NameSet -> NameSet -> Type}
             {ppu : PartPatchUniverse T T}
             {pui : PatchUniverseInv ppu ppu}
             {pu : PatchUniverse pui}
           : PartPatchUniverse
                 (Sequence pu)
                 T
    := mkPartPatchUniverse
           (Sequence pu)
           T
           (@ManyOneCommute _ _ _ _)
           (@impl.ManyOneCommutable_dec _ _ _ _)
           (@impl.ManyOneCommuteUnique _ _ _ _).