(** %
# \section{\label{sec:catches}Catches and Repos}
% *)
Module Export catches_commute_consistent_1_1.

Require Import Equality.
Require Import names.
Require Import patch_universes.
Require Import invertible_patchlike.
Require Import invertible_patch_universe.
Require Import commute_square.
Require Import canonical_order.
Require Import contexted_patches.
Require Import catches_definition.

Lemma CatchCommuteConsistent1_1 :
      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}
             {cs : CommuteSquare pu_type pu_type}
             {o op opq opqr opr oq oqr : NameSet}
             {p1 : Catch ipl o op}
             {q1 : Catch ipl op opq}
             {r1 : Catch ipl opq opqr}
             {q2 : Catch ipl opr opqr}
             {r2 : Catch ipl op opr}
             {q3 : Catch ipl o oq}
             {r3 : Catch ipl oq oqr}
             {p3 : Catch ipl oqr opqr}
             {p5 : Catch ipl oq opq}
             (catchCommuteDetails : <<q1, r1>> <~>1 <<r2, q2>>)
             (commute2 : <<p1, q1>> <~>c <<q3, p5>>)
             (commute3 : <<p5, r1>> <~>c <<r3, p3>>),
      (exists or : NameSet,
       (exists r4 : Catch ipl o or,
        (exists q4 : Catch ipl or oqr,
         (exists p6 : Catch ipl or opr,
          <<q3, r3>> <~>c <<r4, q4>> /\
          <<p1, r2>> <~>c <<r4, p6>> /\
          <<p6, q2>> <~>c <<q4, p3>>)))).
Proof with auto.
intros.
dependent destruction catchCommuteDetails;
destruct commute2;
try (abstract (dependent destruction catchCommuteDetails));
dependent destruction catchCommuteDetails;
destruct commute3;
try (abstract (dependent destruction catchCommuteDetails));
dependent destruction catchCommuteDetails.
                (* case 1/5/1 *)
                destruct (commuteNames H) as [? [? ?]].
                congruence.
            (* case 1/5/2 *)
            destruct (commuteNames H) as [? [? ?]].
            congruence.
        (* case 1/5/6 *)
        (*  p1  q1  r1: x  y                 [y^; {:y}; :z] *)
        (*  p1  r2  q2: x  z                 [z^; {:z}; :y] *)
        (*  q3  p5  r1: y' x'                [y^; {:y}; :z] *)
        (*  q3  r3  p3: y' [y'^; {:y'}; :z'] x              *)
        (* #r4 #q4  p3: z' [z'^; {:z'}; :y'] x              *)
        (* #r4 #p6  q2: z' x''               [z^; {:z}; :y] *)
        dependent destruction H0.
        consEquality x.
        dependent destruction H0.
            dependent destruction H1.
                rename p0 into x.
                rename p into y.
                rename q into z.
                rename q' into y'.
                rename p1 into x'.
                set (HX := H).
                clearbody HX.
                apply commuteSelfInverse in HX.
                apply commuteSquare in HX.
                apply commuteSquare in HX.
                apply commuteSquare in HX.
                rewrite invertInverse in HX.
                rewrite invertInverse in HX.
                destruct (commuteUnique HX commutePQ) as [? [? ?]].
                subst.
                subst.
                clear HX commutePQ.
                rename p2 into x.
                rename ident' into z'.
                rename p' into x''.
                subst q'Effect.
                subst p'Effect.
                subst contextedP.
                subst contextedQ.
                subst conflictsP.
                subst conflictsQ.
                rename from1 into o.
                rename mid into ox.
                rename mid1 into oxy.
                rename to2 into oxz.
                rename from0 into oy.
                rename mid' into oz.

                assert (HX : List.map (addToContext x) (MkContextedPatch [] y :: nil)
                           = (MkContextedPatch [] y' :: nil)%list).
                    admit.
                revert q'ConflictsConflict.
                rewrite HX.
                intros.
                clear HX.

                exists oz.
                exists (MkCatch z').
                assert (z'i_OK : ConsOK (z' ^) []).
                    constructor.
                    rewrite SequenceContentsNil.
                    signedNameSetDec.
                assert (canonicallyOrdered : CanonicallyOrdered (z' ^ :> [])).
                    admit.
                assert (conflictsConflict : List.Forall (conflictsWith (MkContextedPatch [] y'))
                                                                       (MkContextedPatch [] z' :: nil)).
                    admit.
                exists (Conflictor (z' ^ :> [])
                                   (MkContextedPatch [] z' :: nil)
                                   (MkContextedPatch [] y') conflictsConflict canonicallyOrdered).
                exists (MkCatch x'').
                split.
                    apply isCatchCommute1.
                        constructor.
                    apply MkCatchCommute1.
                        destruct (commuteNames H) as [? [HX1 ?]].
                        destruct (commuteNames commute0) as [? [HX2 ?]].
                        rewrite <- HX1.
                        rewrite <- HX2...
                    intro z'i_y'_commute.
                    destruct z'i_y'_commute as [sns [y'' [z''i z'i_y'_commute]]].
                    contradiction do_not_commute.
                    apply commuteSquare in commute0.
                    apply commuteSelfInverse in H.
                    destruct (commuteConsistent2 z'i_y'_commute H commute0) as [? [? [? [? [? [? ?]]]]]].
                    exists x0.
                    exists x1.
                    exists x2...
                split.
                    apply isCatchCommute5.
                        constructor.
                    apply MkCatchCommute5...
                apply isCatchCommute6.
                    constructor.
                apply MkCatchCommute6.
                                    admit.
                                admit.
                            admit.
                        admit.
                    admit.
                congruence.
            contradiction (ConsEqNil x).
        contradiction (ConsEqNil x).
    (* case 1/7/4 *)
    admit.
(* case 1/7/8 *)
admit.
Qed.

End catches_commute_consistent_1_1.