(** %
\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.
Require Import commute_square.

Require Import patch_universes_sequences.many.
Require Import patch_universes_sequences.one_many.
Require Import patch_universes_sequences.many_one.
Require Import patch_universes_sequences.one_many_one.

Module Type Sig.
Parameter ManyManyPartPatchUniverse : forall
             {T : NameSet -> NameSet -> Type}
             {ppu : PartPatchUniverse T T}
             {pui : PatchUniverseInv ppu ppu}
             {pu : PatchUniverse pui},
             PartPatchUniverse
                 (Sequence pu)
                 (Sequence pu).
Parameter ManyManyPatchUniverseInv : forall
             {T : NameSet -> NameSet -> Type}
             {ppu : PartPatchUniverse T T}
             {pui : PatchUniverseInv ppu ppu}
             {pu : PatchUniverse pui},
             PatchUniverseInv
                 ManyManyPartPatchUniverse
                 ManyManyPartPatchUniverse.
Parameter ManyManyCommuteSquare : forall
             {T : NameSet -> NameSet -> Type}
             {ppu : PartPatchUniverse T T}
             {pui : PatchUniverseInv ppu ppu}
             {pu : PatchUniverse pui}
             {ipl : InvertiblePatchlike T}
             {ipu : InvertiblePatchUniverse pu ipl},
             CommuteSquare (Sequence pu) (Sequence pu).
End Sig.

Module impl : Sig.

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

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

Lemma ManyManyCommuteNames
             {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}
             {qs : Sequence pu mid to}
             {qs' : Sequence pu from mid'}
             {ps' : Sequence pu mid' to}
             (p_qs_commute_qs'_p' : <<ps, qs>> <~>mm <<qs', ps'>>)
           : (sequenceContents ps = sequenceContents ps')
          /\ (sequenceContents qs = sequenceContents qs').
Proof with auto.
destruct ps as [ps psSequenceOK].
destruct ps' as [ps' ps'SequenceOK].
dependent induction ps generalizing mid' ps' ps'SequenceOK qs' p_qs_commute_qs'_p'.
    dependent induction p_qs_commute_qs'_p'.
        unfold sequenceContents...
    rewrite NilSeqToNil in x0.
    contradiction (ConsEqNil x0).
consSeqToCons p ps.
dependent destruction p_qs_commute_qs'_p'.
consEquality x0.
destruct ps'0 as [ps'0 ps'0SequenceOK].
specialize (IHps psSequenceOK0).
specialize (IHps qs).
specialize (IHps mid2').
specialize (IHps ps'0).
specialize (IHps ps'0SequenceOK).
specialize (IHps qs'').
specialize (IHps p_qs_commute_qs'_p').
unfold block in IHps.
destruct IHps as [? ?].
destruct (OneManyCommuteNames commutePQ) as [? ?].
split.
    rewrite SequenceContentsCons.
    rewrite H.
    rewrite <- x.
    rewrite SequenceContentsCons.
    unfold sequenceContents.
    rewrite H1...
rewrite H0...
Qed.

Lemma ManyManyCommuteUnique {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}
                            {qs : Sequence pu mid to}
                            {qs' : Sequence pu from mid'}
                            {ps' : Sequence pu mid' to}
                            {qs'' : Sequence pu from mid''}
                            {ps'' : Sequence pu mid'' to}
                            (commute1 : <<ps, qs>> <~>mm <<qs', ps'>>)
                            (commute2 : <<ps, qs>> <~>mm <<qs'', ps''>>)
                          : (mid' = mid'') /\ ps' ~= ps'' /\ qs' ~= qs''.
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'  qs'  ps'  ps'SequenceOK  commute1
                                    mid'' qs'' ps'' ps''SequenceOK 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.
destruct ps'0.
destruct ps'1.
specialize (IHps psSequenceOK0).
specialize (IHps qs).
specialize (IHps mid2').
specialize (IHps qs''0).
specialize (IHps s).
specialize (IHps sequenceOK).
specialize (IHps commute1).
specialize (IHps mid2'0).
specialize (IHps qs'').
specialize (IHps s0).
specialize (IHps sequenceOK0).
specialize (IHps commute2).
unfold block in IHps.
destruct IHps as [? [? ?]].
subst.
apply JMeq_eq in H0.
apply JMeq_eq in H1.
inversion H0.
subst.
proofIrrel sequenceOK sequenceOK0.
doCommuteUnique commutePQ0 commutePQ.
proofIrrel consOK0 consOK1.
rewrite x0 in x.
rewrite x...
Qed.

Lemma ManyManyCommutable_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)
             (qs : Sequence pu mid to)
           : { mid2 : NameSet &
             { qs' : Sequence pu from mid2 &
             { ps' : Sequence pu mid2 to &
             <<ps, qs>> <~>mm <<qs', ps'>> }}}
           + {~(ps <~?~>mm qs)}.
Proof with auto.
destruct ps as [ps psSequenceOK].
dependent induction ps.
    left.
    exists to.
    exists qs.
    exists [].
    rewrite NilSeqToNil.
    apply NilManyManyCommute.
consSeqToCons p ps.
specialize (IHps psSequenceOK0).
specialize (IHps qs).
unfold block in IHps.
destruct IHps.
    destruct s as [? [? [? ?]]].
    destruct (commutable_dec p x0).
        left.
        destruct s as [? [? [? ?]]].
        exists x2.
        exists x3.
        assert (HX : ConsOK x4 x1).
            constructor.
            destruct pPsConsOK.
            destruct (ManyManyCommuteNames m) as [? ?].
            destruct (OneManyCommuteNames c) as [? ?].
            rewrite <- H1.
            rewrite <- H...
        exists (x4 :> x1).
        apply (ConsManyManyCommute m c).
    right.
    intro.
    elim n.
    destruct H as [? [? [? ?]]].
    dependent destruction H.
    consEquality x.
    destruct (ManyManyCommuteUnique m H) as [? [? ?]].
    subst.
    subst.
    exists mid1'.
    exists qs'.
    exists p'...
right.
intro.
elim n.
destruct H as [? [? [? ?]]].
dependent destruction H.
consEquality x.
exists mid2'.
exists qs''.
exists ps'...
Qed.

Instance ManyManyPartPatchUniverse
             {T : NameSet -> NameSet -> Type}
             {ppu : PartPatchUniverse T T}
             {pui : PatchUniverseInv ppu ppu}
             {pu : PatchUniverse pui}
           : PartPatchUniverse
                 (Sequence pu)
                 (Sequence pu)
    := mkPartPatchUniverse
           (Sequence pu)
           (Sequence pu)
           (@ManyManyCommute _ _ _ _)
           (@ManyManyCommutable_dec _ _ _ _)
           (@ManyManyCommuteUnique _ _ _ _).

Lemma manyManyCommuteOtherWay
           {pu_type : NameSet -> NameSet -> Type}
           {ppu : PartPatchUniverse pu_type pu_type}
           {pui : PatchUniverseInv ppu ppu}
           {pu : PatchUniverse pui}
           {o op opq opqr oq oqr : NameSet}
           {ps :  Sequence pu o op}
           {q :  pu_type op opq}
           {rs :  Sequence pu opq opqr}
           {q' :  pu_type o oq}
           {ps'' :  Sequence pu oq opq}
           {rs' :  Sequence pu oq oqr}
           {ps' :  Sequence pu oqr opqr}
           {q_rs_OK : ConsOK q rs}
           {q'_rs'_OK : ConsOK q' rs'}
           (ps_q_commute : <<ps,  q>> <~> <<q', ps''>>)
           (ps_rs_commute : <<ps'', rs>> <~> <<rs', ps'>>)
     : << ps, q :> rs >> <~> << q' :> rs', ps' >>.
Proof with auto.
destruct ps as [ps psOK].
destruct rs as [rs rsOK].
destruct ps'' as [ps'' ps''OK].
destruct ps' as [ps' ps'OK].
destruct rs' as [rs' rs'OK].
revert ps_rs_commute.
revert ps_q_commute.
revert ps'OK.
revert ps'.
revert q'_rs'_OK.
revert rs'OK.
revert rs'.
revert q_rs_OK.
revert psOK.
revert q.
revert rsOK.
revert rs.
revert ps''OK.
revert ps''.
revert q'.
revert oqr.
revert oq.
revert opqr.
revert opq.
dependent induction ps.
    intros.
    simpl in ps_q_commute.
    rewrite NilSeqToNil in ps_q_commute.
    dependent destruction ps_q_commute.
        simpl in ps_rs_commute.
        rewrite NilSeqToNil in ps_rs_commute.
        dependent destruction ps_rs_commute.
            proofIrrel rsOK rs'OK.
            proofIrrel q_rs_OK q'_rs'_OK.
            simpl commute.
            rewrite NilSeqToNil.
            rewrite NilSeqToNil.
            apply NilManyManyCommute.
        contradiction (ConsEqNil x0).
    contradiction (ConsEqNil x0).
intros.
consSeqToCons p ps.
simpl commute in ps_q_commute.
dependent destruction ps_q_commute.
consEquality x0.
destruct ps''.
    rewrite NilSeqToNil in x.
    contradiction (ConsEqNil x).
consSeqToCons p0 ps''.
consEquality x.
simpl commute in ps_rs_commute.
dependent destruction ps_rs_commute.
consEquality x0.
destruct ps'.
    rewrite NilSeqToNil in x.
    contradiction (ConsEqNil x).
consSeqToCons p1 ps'.
consEquality x.
destruct qs'' as [qs'' qs''OK].
specialize (IHps mid3).
specialize (IHps to).
specialize (IHps mid0).
specialize (IHps mid1).
specialize (IHps q'').
specialize (IHps ps'').
specialize (IHps psSequenceOK0).
specialize (IHps rs).
specialize (IHps rsOK).
specialize (IHps q).
specialize (IHps psSequenceOK).
specialize (IHps q_rs_OK).
specialize (IHps qs'').
specialize (IHps qs''OK).
solveFirstIn IHps.
    constructor.
    destruct (OneManyCommuteNames commutePQ) as [? ?]. (* XXX Make instance first and use commuteNames? *)
    destruct (commuteNames commutePQ0) as [? [? ?]].
    destruct q'_rs'_OK.
    clear - consNotAlreadyThere0 H0 H2.
    rewrite H0.
    remember (sequenceContents (MkSequence rs' rs'OK)) as seq.
    signedNameSetDec.
specialize (IHps ps').
specialize (IHps psSequenceOK1).
specialize (IHps ps_q_commute).
specialize (IHps ps_rs_commute).
simpl commute.
refine (ConsManyManyCommute IHps _).
simpl commute.
apply (ConsOneManyCommute commutePQ0 commutePQ).
Qed.

Lemma manyManyCommuteSelfInverse :
    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)
           (qs :  Sequence pu mid1 to)
           (qs' : Sequence pu from mid2)
           (ps' : Sequence pu mid2 to),
        (<<ps,  qs>> <~> <<qs', ps'>>)
     -> (<<qs', ps'>> <~> <<ps,  qs>>).
Proof.
intros.
destruct ps as [ps psOK].
destruct qs as [qs qsOK].
destruct ps' as [ps' ps'OK].
destruct qs' as [qs' qs'OK].
simpl in H.
revert H.
revert psOK.
revert ps.
revert qsOK.
revert qs.
revert qs'OK.
revert qs'.
revert ps'OK.
revert from.
revert mid1.
dependent induction ps'.
    intros.
    dependent destruction H.
        proofIrrel qsOK qs'OK.
        simpl commute.
        rewrite NilSeqToNil.
        rewrite NilSeqToNil.
        dependent induction qs'.
            rewrite NilSeqToNil.
            apply NilManyManyCommute.
        consSeqToCons p qs'.
        specialize (IHqs' ps'OK).
        specialize (IHqs' psSequenceOK).
        solveFirstIn IHqs'.
            constructor.
            constructor.
        specialize (IHqs' x).
        apply (ConsManyManyCommute IHqs').
        apply OneManyCommuteNil.
    rewrite NilSeqToNil in x.
    contradiction (ConsEqNil x).
intros.
dependent destruction H.
consSeqToCons p ps'.
consEquality x.
destruct ps.
    rewrite NilSeqToNil in x0.
    contradiction (ConsEqNil x0).
consSeqToCons p1 ps.
consEquality x0.
destruct qs'' as [qs'' qs''OK].
specialize (IHps' to0).
specialize (IHps' mid0).
specialize (IHps' psSequenceOK).
specialize (IHps' qs'').
specialize (IHps' qs''OK).
specialize (IHps' qs).
specialize (IHps' qsOK).
specialize (IHps' ps).
specialize (IHps' psSequenceOK0).
specialize (IHps' H).
apply commuteSelfInverse in commutePQ.
apply (manyManyCommuteOtherWay commutePQ IHps').
Qed.

Instance ManyManyPatchUniverseInv
             {T : NameSet -> NameSet -> Type}
             {ppu : PartPatchUniverse T T}
             {pui : PatchUniverseInv ppu ppu}
             {pu : PatchUniverse pui}
           : PatchUniverseInv
                 ManyManyPartPatchUniverse
                 ManyManyPartPatchUniverse
    := mkPatchUniverseInv
           (Sequence pu)
           (Sequence pu)
           ManyManyPartPatchUniverse
           ManyManyPartPatchUniverse
           manyManyCommuteSelfInverse.

Lemma manyManyCommuteSquare :
      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)
             (ps  : Sequence pu from mid1) (qs  : Sequence pu mid1 to)
             (qs' : Sequence pu from mid2) (ps' : Sequence pu mid2 to),
       << ps , qs >> <~> << qs' , ps' >>
    -> << qs' ^ , ps >> <~> << ps' , qs^ >>.
Proof.
intros.
destruct ps as [ps psOK].
destruct qs as [qs qsOK].
destruct ps' as [ps' ps'OK].
destruct qs' as [qs' qs'OK].
simpl in H.
dependent induction H.
    apply commuteSelfInverse.
    rewrite NilSeqToNil.
    rewrite NilSeqToNil.
    proofIrrel qsOK qs'OK.
    simpl commute.
    apply NilManyManyCommute.
destruct ps0 as [ps0 ps0OK].
destruct ps'0 as [ps'0 ps'0OK].
destruct qs'' as [qs'' qs''OK].
destruct ps.
    rewrite NilSeqToNil in x0.
    contradiction (ConsEqNil x0).
consSeqToCons p0 ps.
consEquality x0.
inversion x0.
subst.
destruct ps'.
    rewrite NilSeqToNil in x.
    contradiction (ConsEqNil x).
consSeqToCons p ps'.
consEquality x.
inversion x.
subst.
specialize (IHManyManyCommute ipl).
specialize (IHManyManyCommute ipu).
specialize (IHManyManyCommute ps).
specialize (IHManyManyCommute psSequenceOK).
specialize (IHManyManyCommute qs).
specialize (IHManyManyCommute qsOK).
specialize (IHManyManyCommute qs'').
specialize (IHManyManyCommute qs''OK).
specialize (IHManyManyCommute ps').
specialize (IHManyManyCommute psSequenceOK0).
specialize (IHManyManyCommute eq_refl).
specialize (IHManyManyCommute eq_refl).
specialize (IHManyManyCommute eq_refl).
specialize (IHManyManyCommute eq_refl).
refine (manyManyCommuteOtherWay _ IHManyManyCommute).
admit.
Qed.

Instance ManyManyCommuteSquare
             {T : NameSet -> NameSet -> Type}
             {ppu : PartPatchUniverse T T}
             {pui : PatchUniverseInv ppu ppu}
             {pu : PatchUniverse pui}
             {ipl : InvertiblePatchlike T}
             {ipu : InvertiblePatchUniverse pu ipl}
           : CommuteSquare (Sequence pu) (Sequence pu)
    := mkCommuteSquare
           (Sequence pu)
           (Sequence pu)
           ManyManyPartPatchUniverse
           ManyManyPartPatchUniverse
           SeqInvertiblePatchlike
           manyManyCommuteSquare.

End impl.