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

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

Module Export impl : Sig.

Fixpoint invertSequenceBase {pu_type : NameSet -> NameSet -> Type}
                                {ppu : PartPatchUniverse pu_type pu_type}
                                {pui : PatchUniverseInv ppu ppu}
                                {pu : PatchUniverse pui}
                                {ipl : InvertiblePatchlike pu_type}
                                {from to : NameSet}
                                (ps : SequenceBase pu from to)
                              : SequenceBase pu to from
 := match ps with
    | Nil _ => Nil
    | Cons _ _ _ p ps' => appendBase
                              (invertSequenceBase ps')
                              (Cons (p^) Nil)
    end.

Lemma invertedCons {pu_type : NameSet -> NameSet -> Type}
                         {ppu : PartPatchUniverse pu_type pu_type}
                         {pui : PatchUniverseInv ppu ppu}
                         {pu : PatchUniverse pui}
                         {ipl : InvertiblePatchlike pu_type}
                         {from mid to : NameSet}
                         {p : pu_type from mid}
                         {ps : SequenceBase pu mid to}
                       : invertSequenceBase (Cons p ps)
                       = appendBase (invertSequenceBase ps)
                                    (Cons (p^) Nil).
Proof.
auto.
Qed.

Lemma invertedSequenceNotIn
    {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 to : NameSet}
    {n : SignedName}
    {ps : SequenceBase pu from to}
    (n_not_in_ps : ~ SignedNameSetIn n (sequenceBaseContents ps))
  : ~ SignedNameSetIn (signedNameInverse n) (sequenceBaseContents (invertSequenceBase ps)).
Proof with auto.
dependent induction ps.
    unfold invertSequenceBase.
    unfold sequenceBaseContents.
    signedNameSetDec.
rewrite SequenceContentsBaseCons in n_not_in_ps.
solveFirstIn IHps.
    remember (sequenceBaseContents ps) as seq.
    signedNameSetDec.
rewrite invertedCons.
rewrite SequenceContentsBaseAppend.
rewrite SequenceContentsBaseCons.
rewrite SequenceContentsBaseNil.
rewrite nameOfInverse.
assert (n_not_p : n <> pu_nameOf p).
    remember (sequenceBaseContents ps) as seq.
    signedNameSetDec.
assert (in_not_ip : signedNameInverse n <> signedNameInverse (pu_nameOf p)).
    intro in_is_ip.
    elim n_not_p.
    apply (f_equal signedNameInverse) in in_is_ip.
    rewrite nameInverseInverse in in_is_ip.
    rewrite nameInverseInverse in in_is_ip...
remember (sequenceBaseContents (invertSequenceBase ps)) as seq.
signedNameSetDec.
Qed.

Lemma sequenceNoDupesAppend {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 to : NameSet}
                            {ps : SequenceBase pu from mid}
                            {qs : SequenceBase pu mid to}
                            (psOK : SequenceNoDupes ps)
                            (qsOK : SequenceNoDupes qs)
                            (psQsOK : SignedNameSetMod.Empty
                                          (SignedNameSetMod.inter
                                               (sequenceBaseContents ps)
                                               (sequenceBaseContents qs)))
                          : SequenceNoDupes (appendBase ps qs).
Proof with auto.
induction ps...
specialize (IHps qs).
solveFirstIn IHps.
    rewrite SequenceNoDupesCons in psOK.
    destruct psOK...
specialize (IHps qsOK).
rewrite SequenceContentsBaseCons in psQsOK.
solveFirstIn IHps.
    remember (sequenceBaseContents ps) as ps_seq.
    remember (sequenceBaseContents qs) as qs_seq.
    signedNameSetDec.
rewrite AppendBaseCons.
rewrite SequenceNoDupesCons.
split...
rewrite SequenceNoDupesCons in psOK.
rewrite SequenceContentsBaseAppend.
remember (sequenceBaseContents ps) as ps_seq.
remember (sequenceBaseContents qs) as qs_seq.
destruct psOK.
signedNameSetDec.
Qed.

Lemma invertedSequenceOK {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 to : NameSet}
                         {ps : SequenceBase pu from to}
                         (sequenceOK : SequenceOK ps)
                       : SequenceOK (invertSequenceBase ps).
Proof with auto.
constructor.
destruct sequenceOK as [sequenceNoDupes].
induction ps...
destruct sequenceNoDupes as [pNotInPs psNoDupes].
specialize (IHps psNoDupes).
rewrite invertedCons.
apply invertedSequenceNotIn in pNotInPs.
refine (sequenceNoDupesAppend IHps _ _).
    simpl.
    split...
    signedNameSetDec.
simpl.
rewrite nameOfInverse.
remember (sequenceBaseContents (invertSequenceBase ps)) as seq.
signedNameSetDec.
Qed.

Definition invertSequence {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 to : NameSet}
                          (ps : Sequence pu from to)
                        : Sequence pu to from
 := match ps with
    | MkSequence s sOK =>
        MkSequence (invertSequenceBase s) (invertedSequenceOK sOK)
    end.

Lemma sequenceBaseAppendAssociative
               {pu_type : NameSet -> NameSet -> Type}
               {ppu : PartPatchUniverse pu_type pu_type}
               {pui : PatchUniverseInv ppu ppu}
               {pu : PatchUniverse pui}
               {ipl : InvertiblePatchlike pu_type}
               {o op opq opqr : NameSet}
               (ps : SequenceBase pu o op)
               (qs : SequenceBase pu op opq)
               (rs : SequenceBase pu opq opqr)
             : appendBase (appendBase ps qs) rs
             = appendBase ps (appendBase qs rs).
Proof with auto.
induction ps...
rewrite AppendBaseCons.
rewrite AppendBaseCons.
rewrite AppendBaseCons.
specialize (IHps qs).
rewrite IHps...
Qed.

Lemma invertSequenceBaseAppend
               {pu_type : NameSet -> NameSet -> Type}
               {ppu : PartPatchUniverse pu_type pu_type}
               {pui : PatchUniverseInv ppu ppu}
               {pu : PatchUniverse pui}
               {ipl : InvertiblePatchlike pu_type}
               {from mid to : NameSet}
               (ps : SequenceBase pu from mid)
               (qs : SequenceBase pu mid to)
             : invertSequenceBase (appendBase ps qs)
             = appendBase (invertSequenceBase qs) (invertSequenceBase ps).
Proof with auto.
induction ps.
    simpl.
    rewrite AppendBaseNil2...
rewrite invertedCons.
rewrite AppendBaseCons.
rewrite invertedCons.
specialize (IHps qs).
rewrite IHps.
rewrite sequenceBaseAppendAssociative...
Qed.

Lemma invertInvertSequenceBase
               {pu_type : NameSet -> NameSet -> Type}
               {ppu : PartPatchUniverse pu_type pu_type}
               {pui : PatchUniverseInv ppu ppu}
               {pu : PatchUniverse pui}
               {ipl : InvertiblePatchlike pu_type}
               {from to : NameSet}
               (ps : SequenceBase pu from to)
             : invertSequenceBase (invertSequenceBase ps) = ps.
Proof with auto.
induction ps...
rewrite invertedCons.
rewrite invertSequenceBaseAppend.
rewrite invertedCons.
rewrite invertInverse.
rewrite IHps...
Qed.

Lemma invertedSequenceOKSelfInverse
               {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 to : NameSet}
               (ps : SequenceBase pu from to)
               (psOK : SequenceOK ps)
               (H : invertSequenceBase (invertSequenceBase ps) = ps)
    : invertedSequenceOK (invertedSequenceOK psOK) ~= psOK.
Proof with auto.
remember (invertedSequenceOK (invertedSequenceOK psOK)) as X.
clear HeqX.
revert X.
rewrite H.
intros.
cut (X = psOK).
    intro.
    rewrite H0...
apply proof_irrelevance.
Qed.

Lemma equalMkSequences
    {pu_type : NameSet -> NameSet -> Type}
    {ppu : PartPatchUniverse pu_type pu_type}
    {pui : PatchUniverseInv ppu ppu}
    {pu : PatchUniverse pui}
    {ipl : InvertiblePatchlike pu_type}
    {from to : NameSet}
    (xs ys : SequenceBase pu from to)
    (xs_eq_ys : xs = ys)
  : forall
    (xsOK : SequenceOK xs)
    (ysOK : SequenceOK ys)
    (xsOK_eq_ysOK : xsOK ~= ysOK),
    MkSequence xs xsOK = MkSequence ys ysOK.
Proof with auto.
rewrite xs_eq_ys.
intros.
rewrite xsOK_eq_ysOK...
Qed.

Lemma invertInvertSequence
               {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 to : NameSet)
               (ps : Sequence pu from to)
             : invertSequence (invertSequence ps) = ps.
Proof with auto.
destruct ps as [ps psOK].
simpl.
apply equalMkSequences.
    rewrite invertInvertSequenceBase...
apply invertedSequenceOKSelfInverse.
rewrite invertInvertSequenceBase...
Qed.

Instance SeqInvertiblePatchlike
             {T : NameSet -> NameSet -> Type}
             {ppu : PartPatchUniverse T T}
             {pui : PatchUniverseInv ppu ppu}
             {pu : PatchUniverse pui}
             {ipl : InvertiblePatchlike T}
             {ipu : InvertiblePatchUniverse pu ipl}
           : InvertiblePatchlike (Sequence pu)
    := mkInvertiblePatchlike
           (Sequence pu)
           (@invertSequence _ _ _ _ _ _)
           invertInvertSequence.

(*
XXX
Lemma invertedCons {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 to : NameSet}
                         (p : pu_type from mid)
                         (ps : Sequence pu mid to)
                         {p_ps_OK : ConsOK p ps}
                       : { pinv_nil_OK : ConsOK (p ^) [] |
                         { psinv_pinv_nil_OK : AppendOK (ps ^) (p ^ :> []) |
                           (p :> ps) ^ = ps ^ :+> (p ^ :> []) }}.
Proof.
solveExists.
    constructor.
    unfold nilSeq.
    unfold sequenceContents.
    unfold sequenceBaseContents.
    signedNameSetDec.
solveExists.
    constructor.
    admit.
destruct ps as [ps psOK].
dependent induction ps.
    admit.
admit.
Qed.
*)

Lemma invertNil
             {T : NameSet -> NameSet -> Type}
             {ppu : PartPatchUniverse T T}
             {pui : PatchUniverseInv ppu ppu}
             {pu : PatchUniverse pui}
             {ipl : InvertiblePatchlike T}
             {ipu : InvertiblePatchUniverse pu ipl}
             {cxt : NameSet}
           : [] ^ = ([] : Sequence pu cxt cxt).
Proof.
simpl.
unfold nilSeq.
f_equal.
apply proof_irrelevance.
Qed.

End impl.