(** %
\section{\label{sec:merging}Merging}
% *)
Module Export merging.

Require Import names.
Require Import patch_universes.
Require Import patch_universes_sequences.
Require Import invertible_patchlike.
Require Import invertible_patch_universe.

(* XXX *)
Axiom cheat : forall {a}, a.

Definition commuteOutCommonPrefix
    {pu_type : NameSet -> NameSet -> Type}
    {ppu : PartPatchUniverse pu_type pu_type}
    {pui : PatchUniverseInv ppu ppu}
    {pu : PatchUniverse pui}
    {from tox toy : NameSet}
    (xs : Sequence pu from tox)
    (ys : Sequence pu from toy)
  : { from' : NameSet &
      prod (Sequence pu from' tox)
           (Sequence pu from' toy) }
    := cheat.

Lemma commuteOutCommonPrefixCons
    {pu_type : NameSet -> NameSet -> Type}
    {ppu : PartPatchUniverse pu_type pu_type}
    {pui : PatchUniverseInv ppu ppu}
    {pu : PatchUniverse pui}
    {ipl : InvertiblePatchlike pu_type}
    {from mid to1 to2 : NameSet}
    (p : pu_type from mid)
    (xs : Sequence pu mid to1)
    (ys : Sequence pu mid to2)
    {pXsConsOK : ConsOK p xs}
    {pYsConsOK : ConsOK p ys}
  : commuteOutCommonPrefix       xs        ys
  = commuteOutCommonPrefix (p :> xs) (p :> ys).
Proof.
admit.
Qed.

Definition mergable {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 tox toy : NameSet}
                    (xs : Sequence pu from tox)
                    (ys : Sequence pu from toy)
                  : Prop
    := match commuteOutCommonPrefix xs ys with
       existT _ (pair xs' ys') => xs'^ <~?~> ys'
       end.

Lemma mergable_dec {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}
                   {fromx mid1x mid2x tox : NameSet}
                   {p : Sequence pu fromx mid1x}
                   {q : Sequence pu fromx mid2x}
                 : { mergable p q }
                 + {~(mergable p q)}.
Proof with auto.
unfold mergable.
destruct (commuteOutCommonPrefix p q) as [newFrom [xs ys]].
destruct (commutable_dec (xs^) ys).
    left.
    destruct s as [to [ys' [xs'inv commute]]].
    exists to.
    exists ys'.
    exists xs'inv...
right...
Qed.

Lemma mergableCons1
    {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 to1 to2 : NameSet}
    (p : pu_type from mid)
    {xs : Sequence pu mid to1}
    {ys : Sequence pu mid to2}
    {pXsConsOK : ConsOK p xs}
    {pYsConsOK : ConsOK p ys}
    (mergableXsYs : mergable xs ys)
  : mergable (p :> xs) (p :> ys).
Proof with auto.
unfold mergable.
rewrite <- (commuteOutCommonPrefixCons p xs ys).
fold (mergable xs ys)...
Qed.

Lemma mergableCons2
    {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 to1 to2 : NameSet}
    {p : pu_type from mid}
    {xs : Sequence pu mid to1}
    {ys : Sequence pu mid to2}
    {pXsConsOK : ConsOK p xs}
    {pYsConsOK : ConsOK p ys}
    (mergablePXsPYs : mergable (p :> xs) (p :> ys))
  : mergable xs ys.
Proof with auto.
unfold mergable.
rewrite (commuteOutCommonPrefixCons p xs ys).
fold (mergable (p :> xs) (p :> ys))...
Qed.

Lemma mergableAppend1
    {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 to1 to2 : NameSet}
    (ps : Sequence pu from mid)
    {xs : Sequence pu mid to1}
    {ys : Sequence pu mid to2}
    {psXsConsOK : AppendOK ps xs}
    {psYsConsOK : AppendOK ps ys}
    (mergableXsYs : mergable xs ys)
  : mergable (ps :+> xs) (ps :+> ys).
Proof with auto.
destruct ps as [ps psSequenceOK].
induction ps.
    rewrite AppendNilSeq.
    rewrite AppendNilSeq...
destruct (ConsSeqToCons p ps) as [XpsSequenceOK [XpPsConsOK XpPsEquality]].
set (X := MkSequence (Cons p ps) psSequenceOK).
generalize (eq_refl X).
(*
unfold X at 2.
rewrite XpPsEquality.
intro.
rewrite H.
clearbody X.
clearbody X.

consSeqToCons p ps.
clearbody X.
destruct (ConsSeqToCons p ps) as [XpsSequenceOK [XpPsConsOK XpPsEquality]].
rewrite XpPsEquality.
rewrite AppendConsSeq.
unfold mergable.
rewrite <- (commuteOutCommonPrefixCons p xs ys).
fold (mergable xs ys)...
*)
admit.
Qed.

Lemma mergableAppend2
    {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 to1 to2 : NameSet}
    (ps : Sequence pu from mid)
    {xs : Sequence pu mid to1}
    {ys : Sequence pu mid to2}
    {psXsConsOK : AppendOK ps xs}
    {psYsConsOK : AppendOK ps ys}
    (mergablePXsPYs : mergable (ps :+> xs) (ps :+> ys))
  : mergable xs ys.
Proof with auto.
destruct ps as [ps psSequenceOK].
induction ps.
    rewrite AppendNilSeq in mergablePXsPYs.
    rewrite AppendNilSeq in mergablePXsPYs...
destruct (ConsSeqToCons p ps) as [XpsSequenceOK [XpPsConsOK XpPsEquality]].
(*
rewrite XpPsEquality.
set (X := MkSequence (Cons p ps) psSequenceOK).
generalize (eq_refl X).
unfold mergable.
rewrite (commuteOutCommonPrefixCons p xs ys).
fold (mergable (p :> xs) (p :> ys))...
*)
admit.
Qed.

Lemma mergableSymmetric
    {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 to1 to2 : NameSet}
    {xs : Sequence pu from to1}
    {ys : Sequence pu from to2}
    (mergableXsYs : mergable xs ys)
  : mergable ys xs.
Proof with auto.
admit.
Qed.

End merging.