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

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 contexted_patches.
Require Import catches_definition.
Require Import catches_commute_consistent.

Lemma CatchCommuteConsistent2 :
      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}
             {o op opq opqr or oq oqr : NameSet}
             {q3 : Catch ipl o oq}
             {r3 : Catch ipl oq oqr}
             {p3 : Catch ipl oqr opqr}
             {q4 : Catch ipl or oqr}
             {r4 : Catch ipl o or}
             {p1 : Catch ipl o op}
             {q1 : Catch ipl op opq}
             {r1 : Catch ipl opq opqr}
             {p5 : Catch ipl oq opq},
      <<q3, r3>> <~>c <<r4, q4>>
   -> <<r3, p3>> <~>c <<p5, r1>>
   -> <<q3, p5>> <~>c <<p1, q1>>
   -> (exists opr : NameSet,
       (exists r2 : Catch ipl op opr,
        (exists q2 : Catch ipl opr opqr,
         (exists p6 : Catch ipl or opr,
          <<q1, r1>> <~>c <<r2, q2>> /\
          <<q4, p3>> <~>c <<p6, q2>> /\
          <<r4, p6>> <~>c <<p1, r2>>)))).
Proof with auto.
intros.
(*
dependent destruction H; dependent destruction H0; dependent destruction H1...

XXX.



    destruct (commuteNames _ H) as [HX1 [HX2 HX3]].
    admit.
(*    congruence. *)
destruct (commuteConsistent1 _ H H0 H1) as [or [r4 [q4 [p6 [H2 [H3 H4]]]]]].
exists or.
exists (MkCatch r4).
exists (MkCatch q4).
exists (MkCatch p6).
split.
    apply MkCatchCommute...
split.
    apply MkCatchCommute...
apply MkCatchCommute...

(* XXX *)
*)
admit.
Qed.

Instance CatchPartPatchUniverse
             {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}
           : PartPatchUniverse (Catch ipl) (Catch ipl)
    := mkPartPatchUniverse
           (Catch ipl)
           (Catch ipl)
           (@CatchCommute _ _ _ _ _ _)
           cheat (* (@CatchCommutable_dec _ _ _ _ _) *)
           cheat (* (@CatchCommuteUnique1 _ _ _ _ _) *)
           (* (@CatchCommuteUnique2 _ _ _ _ _) *).

Instance CatchPatchUniverseInv
             {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}
           : PatchUniverseInv (CatchPartPatchUniverse ipl) (CatchPartPatchUniverse ipl)
    := mkPatchUniverseInv
           (Catch ipl)
           (Catch ipl)
           (CatchPartPatchUniverse ipl)
           (CatchPartPatchUniverse ipl)
           (@CatchCommuteSelfInverse _ _ _ _ _ _ _).

Instance CatchPatchUniverse
             {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}
           : PatchUniverse (CatchPatchUniverseInv ipl)
    := mkPatchUniverse
           (Catch ipl)
           (CatchPartPatchUniverse ipl)
           (CatchPatchUniverseInv ipl)
           (@catch_name _ _ _ _ _ _)
           (@CatchCommuteConsistent1 _ _ _ _ _ _ _)
           (@CatchCommuteConsistent2 _ _ _ _ _ _)
           (@CatchCommuteNames _ _ _ _ _ _).

End catches.