(** % \section{\label{sec:patch_universes}Patch Universes} % *) Module Export patch_universes. Require Import Equality. Require Import names. Require Import util. (** % In this section we will introduce \emph{patch universes}. Provided a patch type, and the operations on it, satisfies certain axioms, a set of sequences of patches forms a patch universe if it satisfies certain invariants. In this section we will use notation normally used for named patches, but to refer to any patch type that can form a patch universe. Likewise, the term ``patch'' refers to the patch type of the particular patch universe being used. We use $\universe$ to denote the entire universe. % *) Definition patchNamesOK (from to : NameSet) (sn : SignedName) : Prop := match sn with | MkSignedName Positive n => (~ NameSetIn n from) /\ (NameSetEqual to (NameSetAdd n from)) | MkSignedName Negative n => (~ NameSetIn n to) /\ (NameSetEqual from (NameSetAdd n to)) end. Reserved Notation "<< p , q >> <~> << q' , p' >>" (at level 60, no associativity). Reserved Notation "p <~?~> q" (at level 60, no associativity). Class PartPatchUniverse (pu_type1 pu_type2 : (NameSet -> NameSet -> Type)) : Type := mkPartPatchUniverse { commute : forall {from mid1 mid2 to : NameSet}, pu_type1 from mid1 -> pu_type2 mid1 to -> pu_type2 from mid2 -> pu_type1 mid2 to -> Prop where "<< p , q >> <~> << q' , p' >>" := (commute p q q' p'); commutable : forall {from mid1 to : NameSet}, pu_type1 from mid1 -> pu_type2 mid1 to -> Prop := fun {from mid1 to : NameSet} (p : pu_type1 from mid1) (q : pu_type2 mid1 to) => exists mid2 : NameSet, exists q' : pu_type2 from mid2, exists p' : pu_type1 mid2 to, <> <~> <> where "p <~?~> q" := (commutable p q); commutable_dec : forall {from mid to : NameSet} (p : pu_type1 from mid) (q : pu_type2 mid to), {mid2 : NameSet & { q' : pu_type2 from mid2 & { p' : pu_type1 mid2 to & <> <~> <> }}} + {~(p <~?~> q)}; commuteUnique : forall {from mid mid' mid'' to : NameSet} {p : pu_type1 from mid} {q : pu_type2 mid to} {q' : pu_type2 from mid'} {p' : pu_type1 mid' to} {q'' : pu_type2 from mid''} {p'' : pu_type1 mid'' to}, <> <~> <> -> <> <~> <> -> (mid' = mid'') /\ (p' ~= p'') /\ (q' ~= q'') }. Notation "<< p , q >> <~> << q' , p' >>" := (commute p q q' p'). Notation "p <~?~> q" := (commutable p q). Ltac doCommuteUnique H1 H2 := let HmidsEqHmidsEq := fresh "HmidsEqHmidsEq" in let HpsEq := fresh "HpsEq" in let HqsEq := fresh "HqsEq" in destruct (commuteUnique H1 H2) as [HmidsEq [HpsEq HqsEq]]; subst; subst. Class PatchUniverseInv {pu_type1 pu_type2 : (NameSet -> NameSet -> Type)} (ppu1 : PartPatchUniverse pu_type1 pu_type2) (ppu2 : PartPatchUniverse pu_type2 pu_type1) : Type := mkPatchUniverseInv { commuteSelfInverse : forall {from mid1 mid2 to : NameSet} {p : pu_type1 from mid1} {q : pu_type2 mid1 to} {q' : pu_type2 from mid2} {p' : pu_type1 mid2 to}, (<> <~> <>) -> (<> <~> <>) }. Class PatchUniverse {pu_type : (NameSet -> NameSet -> Type)} {ppu : PartPatchUniverse pu_type pu_type} (pui : PatchUniverseInv ppu ppu) : Type := mkPatchUniverse { pu_nameOf : forall {from to : NameSet}, pu_type from to -> SignedName; (** % \begin{igpic}{-1}{15}{-1}{15} \drawlabpoint{o}{(0,0)}{tr} \drawlabpoint{op}{(6,0)}{tl} \drawlabpoint{oq}{(0,6)}{br} \drawlabpoint{opq}{(6,6)}{bc} \existential{\drawlabpoint{or}{(4,2)}{tl}} \drawlabpoint{opr}{(10,2)}{tl} \drawlabpoint{oqr}{(4,8)}{bc} \drawlabpoint{opqr}{(10,8)}{bc} # The far face \definepoint{OrOpr}{(8,2)} \definepoint{OrOqr}{(4,4)} \definepoint{OprOpqr}{(10,5)} \definepoint{OqrOpqr}{(7,8)} # The links between the two \definepoint{OOr}{(2,1)} \definepoint{OpOpr}{(8,1)} \definepoint{OqOqr}{(2,7)} \definepoint{OpqOpqr}{(8,7)} # The near face \definepoint{OOp}{(3,0)} \definepoint{OOq}{(0,3)} \definepoint{OpOpq}{(6,4)} \definepoint{OqOpq}{(2,6)} # The far face \earrlab{or}{OrOpr}{opr}{bc}{$p_6$} \earrlab{or}{OrOqr}{oqr}{cr}{$q_4$} \arrlab{opr}{OprOpqr}{opqr}{cl}{$q_2$} \arrlab{oqr}{OqrOpqr}{opqr}{bc}{$p_3$} # The links between the two \earrlab{o}{OOr}{or}{tl}{$r_4$} \arrlab{op}{OpOpr}{opr}{tl}{$r_2$} \arrlab{oq}{OqOqr}{oqr}{br}{$r_3$} \arrlab{opq}{OpqOpqr}{opqr}{tl}{$r_1$} # The near face \arrlab{o}{OOp}{op}{tc}{$p_1$} \arrlab{o}{OOq}{oq}{cl}{$q_3$} \arrlab{op}{OpOpq}{opq}{cl}{$q_1$} \arrlab{oq}{OqOpq}{opq}{tc}{$p_5$} \end{igpic} % *) commuteConsistent1 : forall {o op opq opqr opr oq oqr : NameSet} {p1 : pu_type o op} {q1 : pu_type op opq} {r1 : pu_type opq opqr} {q2 : pu_type opr opqr} {r2 : pu_type op opr} {q3 : pu_type o oq} {r3 : pu_type oq oqr} {p3 : pu_type oqr opqr} {p5 : pu_type oq opq}, <> <~> <> -> <> <~> <> -> <> <~> <> -> exists or : NameSet, exists r4 : pu_type o or, exists q4 : pu_type or oqr, exists p6 : pu_type or opr, <> <~> <> /\ <> <~> <> /\ <> <~> <>; commuteConsistent2 : forall {o op opq opqr or oq oqr : NameSet} {q3 : pu_type o oq} {r3 : pu_type oq oqr} {p3 : pu_type oqr opqr} {q4 : pu_type or oqr} {r4 : pu_type o or} {p1 : pu_type o op} {q1 : pu_type op opq} {r1 : pu_type opq opqr} {p5 : pu_type oq opq}, <> <~> <> -> <> <~> <> -> <> <~> <> -> exists opr : NameSet, exists r2 : pu_type op opr, exists q2 : pu_type opr opqr, exists p6 : pu_type or opr, <> <~> <> /\ <> <~> <> /\ <> <~> <>; (* This isn't true for conflictors, but happily turned out not to be used in the proofs so far: pu_contexts : forall {from to : NameSet} (p : pu_type from to), patchNamesOK from to (pu_nameOf p); *) (** % We will write sequences of patches as $\seq{p}$, and we require that patches $p$ have names $\name{p}$. The set of names in a sequence of patches, or in a set of sequences of patches, is $\names{p}$; the set of names used in the whole universe is therefore $\names{\universe}$. The commute relations $<->$, $\commutesName$ and $<->*$ work on patches and sequences of patches in the normal way. % *) commuteNames : forall {from mid1 mid2 to : NameSet} {p : pu_type from mid1} {q : pu_type mid1 to} {q' : pu_type from mid2} {p' : pu_type mid2 to}, << p , q >> <~> << q' , p' >> -> (pu_nameOf p = pu_nameOf p') /\ (pu_nameOf q = pu_nameOf q') /\ (pu_nameOf p <> pu_nameOf q) }. (* Lemma commuteOKOfInverse : forall {o op op' opq o' oq oq' oqp : NameSet} (commuteOK : CommuteOK), CommuteOK o' oq oq' oqp o op op' opq. Proof. intros. constructor. remember commuteFromOK. clear - e. nameSetDec. remember commuteMid2OK. clear - e. nameSetDec. remember commuteMid1OK. clear - e. nameSetDec. remember commuteToOK. clear - e. nameSetDec. Qed. *) Inductive SequenceBase {pu_type : NameSet -> NameSet -> Type} {ppu : PartPatchUniverse pu_type pu_type} {pui : PatchUniverseInv ppu ppu} (patchUniverse : PatchUniverse pui) : NameSet -> NameSet -> Type := Nil : forall {cxt : NameSet}, SequenceBase patchUniverse cxt cxt | Cons : forall {from mid to : NameSet} (p : pu_type from mid) (qs : SequenceBase patchUniverse mid to), SequenceBase patchUniverse from to. Implicit Arguments Nil [pu_type ppu pui patchUniverse cxt]. Implicit Arguments Cons [pu_type ppu pui patchUniverse from mid to]. Fixpoint sequenceBaseContents {pu_type : NameSet -> NameSet -> Type} {ppu : PartPatchUniverse pu_type pu_type} {pui : PatchUniverseInv ppu ppu} {pu : PatchUniverse pui} {from to : NameSet} (s : SequenceBase pu from to) : SignedNameSet := match s with | Nil _ => SignedNameSetMod.empty | Cons _ _ _ p qs => SignedNameSetMod.add (pu_nameOf p) (sequenceBaseContents qs) end. Fixpoint SequenceNoDupes {pu_type : NameSet -> NameSet -> Type} {ppu : PartPatchUniverse pu_type pu_type} {pui : PatchUniverseInv ppu ppu} {pu : PatchUniverse pui} {from to : NameSet} (s : SequenceBase pu from to) : Prop := match s with | Nil _ => True | Cons _ _ _ p qs => ~SignedNameSetMod.In (pu_nameOf p) (sequenceBaseContents qs) /\ SequenceNoDupes qs end. Lemma SequenceNoDupesCons {pu_type : NameSet -> NameSet -> Type} {ppu : PartPatchUniverse pu_type pu_type} {pui : PatchUniverseInv ppu ppu} {pu : PatchUniverse pui} {from mid to : NameSet} {x : pu_type from mid} {ys : SequenceBase pu mid to} : SequenceNoDupes (Cons x ys) = ~ SignedNameSetIn (pu_nameOf x) (sequenceBaseContents ys) /\ SequenceNoDupes ys. Proof. auto. Qed. Class SequenceOK {pu_type : NameSet -> NameSet -> Type} {ppu : PartPatchUniverse pu_type pu_type} {pui : PatchUniverseInv ppu ppu} {pu : PatchUniverse pui} {from to : NameSet} (s : SequenceBase pu from to) := { sequenceNoDupes : SequenceNoDupes s }. Inductive Sequence {pu_type : NameSet -> NameSet -> Type} {ppu : PartPatchUniverse pu_type pu_type} {pui : PatchUniverseInv ppu ppu} (pu : PatchUniverse pui) (from to : NameSet) : Type := MkSequence : forall (s : SequenceBase pu from to) {sequenceOK : SequenceOK s}, Sequence pu from to. Implicit Arguments MkSequence [pu_type ppu pui pu from to]. Definition sequenceContents {pu_type : NameSet -> NameSet -> Type} {ppu : PartPatchUniverse pu_type pu_type} {pui : PatchUniverseInv ppu ppu} {pu : PatchUniverse pui} {from to : NameSet} (s : Sequence pu from to) : SignedNameSet := match s with | MkSequence s _ => sequenceBaseContents s end. Class ConsOK {pu_type : NameSet -> NameSet -> Type} {ppu : PartPatchUniverse pu_type pu_type} {pui : PatchUniverseInv ppu ppu} {pu : PatchUniverse pui} {from mid to : NameSet} (head : pu_type from mid) (tail : Sequence pu mid to) := { consNotAlreadyThere : ~ SignedNameSetIn (pu_nameOf head) (sequenceContents tail) }. Implicit Arguments ConsOK [pu_type ppu pui pu from mid to]. Program Definition nilSeq {pu_type : NameSet -> NameSet -> Type} {ppu : PartPatchUniverse pu_type pu_type} {pui : PatchUniverseInv ppu ppu} {pu : PatchUniverse pui} (cxt : NameSet) : Sequence pu cxt cxt := MkSequence Nil _. Next Obligation. constructor. constructor. Qed. Program Definition consSeq {pu_type : NameSet -> NameSet -> Type} {ppu : PartPatchUniverse pu_type pu_type} {pui : PatchUniverseInv ppu ppu} {pu : PatchUniverse pui} {from mid to : NameSet} (p : pu_type from mid) (qs : Sequence pu mid to) (consOK : ConsOK p qs) : Sequence pu from to := match qs with | MkSequence s _ => MkSequence (Cons p s) _ end. Next Obligation. constructor. constructor. destruct consOK. unfold sequenceContents in consNotAlreadyThere0. auto. destruct wildcard'. auto. Qed. Notation "s :> t" := (consSeq s t _) (at level 60, right associativity). Notation "[]" := (nilSeq _) (no associativity). Lemma NilSeqToNil {pu_type : NameSet -> NameSet -> Type} {ppu : PartPatchUniverse pu_type pu_type} {pui : PatchUniverseInv ppu ppu} {pu : PatchUniverse pui} {cxt : NameSet} (nilSequenceOK : SequenceOK Nil) : MkSequence Nil nilSequenceOK = nilSeq cxt. Proof with auto. unfold nilSeq. f_equal. apply proof_irrelevance. Qed. Lemma ConsSeqToCons {pu_type : NameSet -> NameSet -> Type} {ppu : PartPatchUniverse pu_type pu_type} {pui : PatchUniverseInv ppu ppu} {pu : PatchUniverse pui} {from mid to : NameSet} (p : pu_type from mid) (ps : SequenceBase pu mid to) {pPsSequenceOK : SequenceOK (Cons p ps)} : { psSequenceOK : SequenceOK ps & { consOK : ConsOK p (MkSequence ps psSequenceOK) & MkSequence (Cons p ps) pPsSequenceOK = p :> (MkSequence ps psSequenceOK)}}. Proof with auto. solveExists. constructor. destruct pPsSequenceOK as [pPsSequenceNoDupes]. destruct pPsSequenceNoDupes... solveExists. constructor. destruct pPsSequenceOK as [pPsSequenceNoDupes]. destruct pPsSequenceNoDupes. unfold sequenceContents... unfold consSeq. f_equal. apply proof_irrelevance. Qed. Ltac consSeqToCons p ps := let psSequenceOK := fresh "psSequenceOK" in let pPsConsOK := fresh "pPsConsOK" in let pPsEquality := fresh "pPsEquality" in destruct (ConsSeqToCons p ps) as [psSequenceOK [pPsConsOK pPsEquality]]; rewrite pPsEquality in *; clear pPsEquality. Lemma ConsEqNil {pu_type : NameSet -> NameSet -> Type} {ppu : PartPatchUniverse pu_type pu_type} {pui : PatchUniverseInv ppu ppu} {patchUniverse : PatchUniverse pui} {cxt mid : NameSet} {p : pu_type cxt mid} {ps : Sequence patchUniverse mid cxt} {consOK : ConsOK p ps} (consEqNil : (p :> ps) = []) : False. Proof. destruct ps. unfold consSeq in consEqNil. inversion consEqNil. Qed. Program Fixpoint appendBase {pu_type : NameSet -> NameSet -> Type} {ppu : PartPatchUniverse pu_type pu_type} {pui : PatchUniverseInv ppu ppu} {patchUniverse : PatchUniverse pui} {from mid to : NameSet} (ps : SequenceBase patchUniverse from mid) (qs : SequenceBase patchUniverse mid to) : SequenceBase patchUniverse from to := match ps with | Nil _ => qs | Cons _ midP _ p ps' => Cons p (appendBase (from := midP) (to := to) ps' qs) end. Lemma SequenceContentsBaseNil {pu_type : NameSet -> NameSet -> Type} {ppu : PartPatchUniverse pu_type pu_type} {pui : PatchUniverseInv ppu ppu} {patchUniverse : PatchUniverse pui} {cxt : NameSet} : sequenceBaseContents (Nil (cxt := cxt)) = SignedNameSetMod.empty. Proof with auto. unfold sequenceBaseContents... Qed. Lemma SequenceContentsBaseCons {pu_type : NameSet -> NameSet -> Type} {ppu : PartPatchUniverse pu_type pu_type} {pui : PatchUniverseInv ppu ppu} {patchUniverse : PatchUniverse pui} {from mid to : NameSet} (p : pu_type from mid) (ps : SequenceBase patchUniverse mid to) : sequenceBaseContents (Cons p ps) = SignedNameSetMod.add (pu_nameOf p) (sequenceBaseContents ps). Proof with auto. unfold sequenceBaseContents at 1. fold (sequenceBaseContents (from := mid) (to := to))... Qed. Lemma AppendBaseCons {pu_type : NameSet -> NameSet -> Type} {ppu : PartPatchUniverse pu_type pu_type} {pui : PatchUniverseInv ppu ppu} {patchUniverse : PatchUniverse pui} {from mid1 mid2 to : NameSet} (p : pu_type from mid1) (ps : SequenceBase patchUniverse mid1 mid2) (qs : SequenceBase patchUniverse mid2 to) : appendBase (Cons p ps) qs = Cons p (appendBase ps qs). Proof with auto. unfold appendBase at 1. fold (appendBase (from := mid1) (mid := mid2) (to := to))... Qed. Lemma AppendBaseNil {pu_type : NameSet -> NameSet -> Type} {ppu : PartPatchUniverse pu_type pu_type} {pui : PatchUniverseInv ppu ppu} {patchUniverse : PatchUniverse pui} {from to : NameSet} (ps : SequenceBase patchUniverse from to) : appendBase Nil ps = ps. Proof with auto. simpl... Qed. Lemma AppendBaseNil2 {pu_type : NameSet -> NameSet -> Type} {ppu : PartPatchUniverse pu_type pu_type} {pui : PatchUniverseInv ppu ppu} {patchUniverse : PatchUniverse pui} {from to : NameSet} (ps : SequenceBase patchUniverse from to) : appendBase ps Nil = ps. Proof with auto. induction ps... simpl. rewrite IHps... Qed. Lemma SequenceContentsBaseAppend {pu_type : NameSet -> NameSet -> Type} {ppu : PartPatchUniverse pu_type pu_type} {pui : PatchUniverseInv ppu ppu} {patchUniverse : PatchUniverse pui} {from mid to : NameSet} (ps : SequenceBase patchUniverse from mid) (qs : SequenceBase patchUniverse mid to) : sequenceBaseContents (appendBase ps qs) = SignedNameSetMod.union (sequenceBaseContents ps) (sequenceBaseContents qs). Proof with auto. induction ps. rewrite SequenceContentsBaseNil. rewrite AppendBaseNil. apply SignedNameSetEquality. signedNameSetDec. specialize (IHps qs). rewrite AppendBaseCons. rewrite SequenceContentsBaseCons. rewrite SequenceContentsBaseCons. rewrite IHps. apply SignedNameSetEquality. signedNameSetDec. Qed. Lemma SequenceContentsConsSeq {pu_type : NameSet -> NameSet -> Type} {ppu : PartPatchUniverse pu_type pu_type} {pui : PatchUniverseInv ppu ppu} {patchUniverse : PatchUniverse pui} {from mid to : NameSet} {p : pu_type from mid} {qs : SequenceBase patchUniverse mid to} {sequenceOK : SequenceOK (Cons p qs)} : sequenceContents (MkSequence (Cons p qs) sequenceOK) = SignedNameSetMod.add (pu_nameOf p) (sequenceBaseContents qs). Proof with auto. unfold sequenceContents. unfold sequenceBaseContents. fold (sequenceBaseContents (from := mid) (to := to))... Qed. Lemma SequenceContentsNil {pu_type : NameSet -> NameSet -> Type} {ppu : PartPatchUniverse pu_type pu_type} {pui : PatchUniverseInv ppu ppu} {patchUniverse : PatchUniverse pui} {cxt : NameSet} : sequenceContents (nilSeq cxt) = SignedNameSetMod.empty. Proof with auto. unfold nilSeq. unfold sequenceContents. unfold sequenceBaseContents... Qed. Lemma SequenceContentsCons {pu_type : NameSet -> NameSet -> Type} {ppu : PartPatchUniverse pu_type pu_type} {pui : PatchUniverseInv ppu ppu} {patchUniverse : PatchUniverse pui} {from mid to : NameSet} {p : pu_type from mid} {qs : Sequence patchUniverse mid to} {consOK : ConsOK p qs} : sequenceContents (p :> qs) = SignedNameSetMod.add (pu_nameOf p) (sequenceContents qs). Proof with auto. unfold consSeq. destruct qs. apply SequenceContentsConsSeq. Qed. Class AppendOK {pu_type : NameSet -> NameSet -> Type} {ppu : PartPatchUniverse pu_type pu_type} {pui : PatchUniverseInv ppu ppu} {patchUniverse : PatchUniverse pui} {from mid to : NameSet} (ps : Sequence patchUniverse from mid) (qs : Sequence patchUniverse mid to) := { appendNoIntersection : SignedNameSetMod.Empty (SignedNameSetMod.inter (sequenceContents ps) (sequenceContents qs)) }. Program Definition append {pu_type : NameSet -> NameSet -> Type} {ppu : PartPatchUniverse pu_type pu_type} {pui : PatchUniverseInv ppu ppu} {patchUniverse : PatchUniverse pui} {from mid to : NameSet} (ps : Sequence patchUniverse from mid) (qs : Sequence patchUniverse mid to) (appendOK : AppendOK ps qs) : Sequence patchUniverse from to := match ps with | MkSequence psBase psOK => match qs with | MkSequence qsBase qsOK => MkSequence (appendBase psBase qsBase) _ end end. Next Obligation. induction psBase. rewrite AppendBaseNil. auto. destruct psOK as [psNoDupes]. destruct psNoDupes. solveFirstIn IHpsBase. constructor. auto. specialize (IHpsBase qsBase). specialize (IHpsBase qsOK). destruct appendOK as [appendNoIntersection]. unfold sequenceContents. unfold sequenceContents in appendNoIntersection. solveFirstIn IHpsBase. clear IHpsBase. rewrite SequenceContentsBaseCons in appendNoIntersection. constructor. unfold sequenceContents. (* coq bug 2699 *) remember (sequenceBaseContents psBase) as ps. remember (sequenceBaseContents qsBase) as qs. signedNameSetDec. rewrite AppendBaseCons. constructor. constructor. rewrite SequenceContentsBaseCons in appendNoIntersection. rewrite SequenceContentsBaseAppend. (* coq bug 2699 *) remember (sequenceBaseContents psBase) as ps. remember (sequenceBaseContents qsBase) as qs. signedNameSetDec. destruct IHpsBase. auto. Qed. Notation "ps :+> qs" := (append ps qs _) (at level 60, right associativity). Lemma SequenceContentsAppend {pu_type : NameSet -> NameSet -> Type} {ppu : PartPatchUniverse pu_type pu_type} {pui : PatchUniverseInv ppu ppu} {patchUniverse : PatchUniverse pui} {from mid to : NameSet} (ps : Sequence patchUniverse from mid) (qs : Sequence patchUniverse mid to) {appendOK : AppendOK ps qs} : sequenceContents (ps :+> qs) = SignedNameSetMod.union (sequenceContents ps) (sequenceContents qs). Proof with auto. destruct ps. destruct qs. unfold sequenceContents. unfold append. apply SequenceContentsBaseAppend. Qed. Lemma AppendNilSeq {pu_type : NameSet -> NameSet -> Type} {ppu : PartPatchUniverse pu_type pu_type} {pui : PatchUniverseInv ppu ppu} {patchUniverse : PatchUniverse pui} {from to : NameSet} (ps : Sequence patchUniverse from to) {sequenceOK : SequenceOK Nil} {appendOK : AppendOK (MkSequence Nil sequenceOK) ps} : MkSequence Nil sequenceOK :+> ps = ps. Proof with auto. destruct ps. unfold append. f_equal. apply proof_irrelevance. Qed. Lemma AppendNil {pu_type : NameSet -> NameSet -> Type} {ppu : PartPatchUniverse pu_type pu_type} {pui : PatchUniverseInv ppu ppu} {patchUniverse : PatchUniverse pui} {from to : NameSet} (ps : Sequence patchUniverse from to) {appendOK : AppendOK [] ps} : [] :+> ps = ps. Proof with auto. unfold nilSeq. apply AppendNilSeq. Qed. Lemma AppendConsSeq {pu_type : NameSet -> NameSet -> Type} {ppu : PartPatchUniverse pu_type pu_type} {pui : PatchUniverseInv ppu ppu} {patchUniverse : PatchUniverse pui} {from mid1 mid2 to : NameSet} (p : pu_type from mid1) (ps : SequenceBase patchUniverse mid1 mid2) (qs : Sequence patchUniverse mid2 to) {ppsOK : SequenceOK (Cons p ps)} {append1OK : AppendOK (MkSequence (Cons p ps) ppsOK) qs} : exists psOK : SequenceOK ps, exists append2OK : AppendOK (MkSequence ps psOK) qs, exists cons1OK : ConsOK p ((MkSequence ps psOK) :+> qs), (MkSequence (Cons p ps) ppsOK :+> qs) = p :> ((MkSequence ps psOK) :+> qs). Proof with auto. destruct ppsOK as [ppsNoDupes]. destruct append1OK as [append1NoIntersection]. solveExists. unfold SequenceNoDupes in ppsNoDupes. fold (SequenceNoDupes (from := mid1) (to := mid2)) in ppsNoDupes. constructor. destruct ppsNoDupes... solveExists. constructor. rewrite SequenceContentsConsSeq in append1NoIntersection. destruct qs. unfold sequenceContents. unfold sequenceContents in append1NoIntersection. (* coq bug 2699 *) remember (sequenceBaseContents ps) as psContents. remember (sequenceBaseContents s) as sContents. signedNameSetDec. solveExists. constructor. destruct qs. rewrite SequenceContentsConsSeq in append1NoIntersection. destruct ppsNoDupes. unfold sequenceContents. unfold append. rewrite SequenceContentsBaseAppend. unfold sequenceContents in append1NoIntersection. (* coq bug 2699 *) remember (sequenceBaseContents ps) as psContents. remember (sequenceBaseContents s) as sContents. signedNameSetDec. destruct qs. simpl. f_equal. apply proof_irrelevance. Qed. Lemma AppendCons {pu_type : NameSet -> NameSet -> Type} {ppu : PartPatchUniverse pu_type pu_type} {pui : PatchUniverseInv ppu ppu} {patchUniverse : PatchUniverse pui} {from mid1 mid2 to : NameSet} (p : pu_type from mid1) (ps : Sequence patchUniverse mid1 mid2) (qs : Sequence patchUniverse mid2 to) {cons1OK : ConsOK p ps} {append1OK : AppendOK (p :> ps) qs} : exists append2OK : AppendOK ps qs, exists cons2OK : ConsOK p (ps :+> qs), (p :> ps) :+> qs = p :> ps :+> qs. Proof with auto. destruct append1OK as [append1NoIntersection]. solveExists. constructor. rewrite SequenceContentsCons in append1NoIntersection. (* coq bug 2699 *) remember (sequenceContents ps) as psContents. remember (sequenceContents qs) as qsContents. signedNameSetDec. solveExists. constructor. rewrite SequenceContentsCons in append1NoIntersection. destruct cons1OK. rewrite SequenceContentsAppend. (* coq bug 2699 *) remember (sequenceContents ps) as psContents. remember (sequenceContents qs) as qsContents. signedNameSetDec. destruct ps. destruct qs. simpl. f_equal. apply proof_irrelevance. Qed. (** % There is also a merge relation $\partialmergeName$. Given two patches $p$ and $q$, either there exists $p'$ and $q'$ such that $\names{p} = \names{p'}$, $\names{q} = \names{q'}$, $\partialmerge{p}{q} = \pair{q'}{p'}$ and $p q' <->* q p'$; or $\partialmerge{p}{q} = \fail$. \start{axiom}{patch-universe-commute-preserves-commute} $ \left(\pair{p}{qr} <-> \pair{q'r'}{p'}\right) => \left(\left(\commutes{q}{r}\right) <=> \left(\commutes{q'}{r'}\right)\right)$ % *) (* commute : pu_type -> pu_type -> pu_type -> pu_type -> Prop where "<< p , q >> <~> << q' , p' >>" := (commute p q q' p'); *) (** % \begin{Iexplanation} This is \refLemma{named-patch-commute-preserves-commute} restated for patch universes. \end{Iexplanation} \end{Iaxiom} \start{axiom}{patch-universe-commute-consistent} $ \left(\pair{q}{r} <-> \pair{r'}{q'}\right) => \left(\left(\pair{p}{qr} <-> \pair{\_}{p'}\right) <=> \left(\pair{p}{r'q'} <-> \pair{\_}{p'}\right)\right)$ % *) (** % \begin{Iexplanation} This is \refLemma{named-patch-commute-consistent} restated for named patches. \end{Iexplanation} \end{Iaxiom} Those are the operations and axioms that your patch type must provide. We now explain what can be done in a patch universe, and what invariants must be satisfied by the operations while they are done. The operations you can do in a patch universe are: \begin{description} \item[Record] Given a sequence of patches $\seq{p}$ we can record a patch with a fresh name, giving us $\seq{p} q$. \item[Unrecord] Given a sequence of patches $\seq{p} q$ we can unpull $q$ leaving us $\seq{p}$. \item[Commute] Given $\seq{p}$, we can make $\seq{q}$ where $\seq{p} <->* \seq{q}$. \item[Merge] Given $\seq{p} \seq{q}$ and $\seq{p} \seq{r}$, if $\partialmerge{\seq{q}}{\seq{r}} = \pair{\seq{r'}}{\seq{q'}}$ then we can make $\seq{p} \seq{q} \seq{r'}$ and $\seq{p} \seq{r} \seq{q'}$. \end{description} XXX and unrecord XXX The remainder of this section is proofs of things \start{lemma}{commute-in-sequence-consistent} Suppose $\seq{p} q r \seq{s} <->* \seq{t} q' r' \seq{u}$ where $\name{q} = \name{q'}$ and $\name{r} = \name{r'}$. Then $\left( \commutes{q}{r} \right) <=> \left( \commutes{q'}{r'} \right)$. \begin{Iexplanation} Suppose we have adjacent two patches $q$ and $r$ in a sequence. No amount of commuting within this sequence can alter whether or not $q$ and $r$ commute. \end{Iexplanation} \begin{Iproof} Suppose, for the purpose of contradiction, that we have a counter example of minimal sequence length. Without loss of generality, assume that $\commutes{q}{r}$ holds but $\commutes{q'}{r'}$ does not. If $\seq{p} = \nopatches$ and $\seq{s} = \nopatches$ then we trivially have a contradiction. We will assume that $\seq{p}$ is non-empty, but an analogous argument covers the case where only $\seq{s}$ is non-empty. So $\seq{p} = v \seq{p'}$, for some patch $v$ and sequence $\seq{p'}$. We will first show, by induction on the structure of $<->*$, that at each step $v$ can be commuted directly to the start of the sequence. Trivially that is true for the initial sequence $v \seq{p'} q r \seq{s}$. Suppose that it is true for a sequence $\seq{a_1} a_2 a_3 \seq{a_4}$ where $\pair{a_2}{a_3} <-> \pair{a_3'}{a_2'}$; then we must show that it is true for $\seq{a_1} a_3' a_2' \seq{a_4}$. If $v$ is in $\seq{a_1}$ then it is trivially true, using the same sequence of commutes as before. If $v$ is $a_2$ then it is true, by first commuting with $a_3'$ and then continuing as before. If $v$ is $a_3$ then it is true, by skipping the first commute of the previous sequence. The must interesting case is when $v$ is in $\seq{a_4}$. We know that $v$ can be commuted past everything else in $\seq{a_4}$ until we have $\seq{a_1} a_2 a_3 v' \seq{a_4'}$, then past $a_2 a_3$ giving us $\seq{a_1} v'' a_2'' a_3'' \seq{a_4'}$, and finally past $\seq{a_1}$, giving us $v''' \seq{a_1'} a_2'' a_3'' \seq{a_4'}$. But \refAxiom{patch-universe-commute-consistent} tells us that $\pair{a_3' a_2'}{v'} <-> \pair{v''}{a_3''' a_2'''}$, so it is also true for this case. Now, consider the final sequence. If $v$ is in $\seq{t}$ then trivially whether $q'$ and $r'$ commute is unchanged. If $v$ is in $\seq{u}$ then \refAxiom{patch-universe-commute-preserves-commute} tells us that whether $q'$ and $r'$ commute is unchanged. Therefore we can construct a shorter counter example, by commuting $v$ to the left of the sequence at each stage, and removing it. \end{Iproof} % *) (* XXX Lemma NamePersistsInSequenceNameSet : forall {patchUniverse : PatchUniverse} {o op opq opqr : NameSet} (p : (pu_type patchUniverse) o op) (qs : Sequence (pu_type patchUniverse) op opq) (rs : Sequence (pu_type patchUniverse) opq opqr), NameSetIn (pu_nameOf patchUniverse p) opq -> NameSetIn (pu_nameOf patchUniverse p) opqr. Proof with auto. intros. dependent induction rs... specialize (IHrs patchUniverse). specialize (IHrs p). specialize (IHrs mid). specialize (IHrs (qs :+> (p0 :> []))). assert (p_in_mid : NameSetIn (pu_nameOf patchUniverse p) mid). destruct (pu_contexts patchUniverse p0). fsetdec. specialize (IHrs p_in_mid). specialize (IHrs opqr refl refl)... Qed. Lemma NamePersistsInSequence : forall {patchUniverse : PatchUniverse} {o op opq : NameSet} (p : (pu_type patchUniverse) o op) (qs : Sequence (pu_type patchUniverse) op opq), NameSetIn (pu_nameOf patchUniverse p) opq. Proof with auto. intros. assert (p_in_op : NameSetIn (pu_nameOf patchUniverse p) op). destruct (pu_contexts patchUniverse p). fsetdec. set (H1 := NamePersistsInSequenceNameSet p [] qs p_in_op)... Qed. Lemma NameInSequenceUnique : forall {patchUniverse : PatchUniverse} {o op opq opqr : NameSet} (p : (pu_type patchUniverse) o op) (qs : Sequence (pu_type patchUniverse) op opq) (r : (pu_type patchUniverse) opq opqr), (pu_nameOf patchUniverse p <> pu_nameOf patchUniverse r). Proof with auto. intros. set (p_in_opq := NamePersistsInSequence p qs). clearbody p_in_opq. destruct (pu_contexts patchUniverse r). congruence. Qed. *) Reserved Notation "<< ps >> <~~> << qs >>" (at level 60, no associativity). Inductive CommuteRelates {pu_type : NameSet -> NameSet -> Type} {ppu : PartPatchUniverse pu_type pu_type} {pui : PatchUniverseInv ppu ppu} {patchUniverse : PatchUniverse pui} {from to : NameSet} : Sequence patchUniverse from to -> Sequence patchUniverse from to -> Prop := SwapNow : forall {op opq oq : NameSet} {p : pu_type from op} {q : pu_type op opq} {q' : pu_type from oq} {p' : pu_type oq opq} {rs : Sequence patchUniverse opq to} (qRsConsOK : ConsOK q rs) (qQRsConsOK : ConsOK p (q :> rs)) (pRsConsOK : ConsOK p' rs) (qPRsConsOK : ConsOK q' (p' :> rs)), <> <~> <> -> <

q :> rs>> <~~> < p' :> rs>> | SwapLater : forall {mid : NameSet} (p : pu_type from mid) {qs : Sequence patchUniverse mid to} {rs : Sequence patchUniverse mid to} (pQsOK : ConsOK p qs) (pRsOK : ConsOK p rs), CommuteRelates (from := mid) qs rs -> CommuteRelates (p :> qs) (p :> rs) where "<< ps >> <~~> << qs >>" := (@CommuteRelates _ _ _ _ _ _ ps qs). (* Lemma CommuteRelatesSameContentsBase {pu_type : NameSet -> NameSet -> Type} {ppu : PartPatchUniverse pu_type pu_type} {pui : PatchUniverseInv ppu ppu} {patchUniverse : PatchUniverse pui} {from to : NameSet} {s t : SequenceBase patchUniverse from to} {sSequenceOK : SequenceOK s} {tSequenceOK : SequenceOK t} (commuteRelates : << MkSequence s sSequenceOK >> <~~> << MkSequence t tSequenceOK >>) : sequenceBaseContents s = sequenceBaseContents t. Proof. dependent destruction commuteRelates. *) Lemma CommuteRelatesSameContents {pu_type : NameSet -> NameSet -> Type} {ppu : PartPatchUniverse pu_type pu_type} {pui : PatchUniverseInv ppu ppu} {patchUniverse : PatchUniverse pui} {from to : NameSet} {s t : Sequence patchUniverse from to} (commuteRelates : << s >> <~~> << t >>) : sequenceContents s = sequenceContents t. Proof with auto. induction commuteRelates as [ ? ? ? ? ? ? ? ? ? ? ? ? ? ? commute | ? ? ? ? ? ? ? ? ? qs_rs_same_contents ]. rewrite SequenceContentsCons. rewrite SequenceContentsCons. rewrite SequenceContentsCons. rewrite SequenceContentsCons. destruct (commuteNames commute) as [? [? ?]]. apply SignedNameSetEquality. signedNameSetDec. rewrite SequenceContentsCons. rewrite SequenceContentsCons. rewrite qs_rs_same_contents... Qed. Reserved Notation "<< p >> <~~>* << q >>" (at level 60, no associativity). (* XXX Would this be better with 3 constructors, Same, Swap and Trans? *) Inductive TransitiveCommuteRelates {pu_type : NameSet -> NameSet -> Type} {ppu : PartPatchUniverse pu_type pu_type} {pui : PatchUniverseInv ppu ppu} {patchUniverse : PatchUniverse pui} {from to : NameSet} : Sequence patchUniverse from to -> Sequence patchUniverse from to -> Prop := Same : forall (s : Sequence patchUniverse from to), TransitiveCommuteRelates s s | Swap : forall {s : Sequence patchUniverse from to} {t : Sequence patchUniverse from to} {u : Sequence patchUniverse from to}, <> <~~> <> -> <> <~~>* <> -> <> <~~>* <> where "<< p >> <~~>* << q >>" := (@TransitiveCommuteRelates _ _ _ _ _ _ p q). Lemma TransitiveCommuteRelatesSameContents {pu_type : NameSet -> NameSet -> Type} {ppu : PartPatchUniverse pu_type pu_type} {pui : PatchUniverseInv ppu ppu} {patchUniverse : PatchUniverse pui} {from to : NameSet} {s t : Sequence patchUniverse from to} (transitiveCommuteRelates : << s >> <~~>* << t >>) : sequenceContents s = sequenceContents t. Proof with auto. induction transitiveCommuteRelates as [? | ? ? ? s_commute_t ? t_u_same_contents]... rewrite <- t_u_same_contents. rewrite (CommuteRelatesSameContents s_commute_t)... Qed. Reserved Notation "<< p , qs >> <~ << rs >>" (at level 60, no associativity). Inductive commuteOutLeft {pu_type : NameSet -> NameSet -> Type} {ppu : PartPatchUniverse pu_type pu_type} {pui : PatchUniverseInv ppu ppu} {patchUniverse : PatchUniverse pui} {from mid to : NameSet} : Sequence patchUniverse from to -> pu_type from mid -> Sequence patchUniverse mid to -> Prop := commuteOutLeftDone : forall (p : pu_type from mid) (qs : Sequence patchUniverse mid to) (p_qsConsOK : ConsOK p qs), <> <~ <

qs>> | commuteOutLeftSwap : forall {mid_q mid_r : NameSet} {p : pu_type mid_r mid_q} {qs : Sequence patchUniverse mid_q to} {rs : Sequence patchUniverse mid_r to} {p' : pu_type from mid} {q : pu_type mid mid_q} {r : pu_type from mid_r} (q_qsConsOK : ConsOK q qs) (r_rsConsOK : ConsOK r rs), <> <~ <> -> <> <~> <> -> < qs>> <~ < rs>> where "<< p , qs >> <~ << rs >>" := (@commuteOutLeft _ _ _ _ _ _ _ rs p qs). (* Inductive commuteOutRight {patchUniverse : PatchUniverse} {from mid to : NameSet} : Sequence patchUniverse from to -> Sequence patchUniverse from mid -> (pu_type patchUniverse) mid to -> Prop := commuteOutRightDone : forall (ps : Sequence patchUniverse from mid) (q : (pu_type patchUniverse) mid to), commuteOutRight (ps :+> q :> []) ps q | commuteOutRightSwap : forall {beforeq mid' : NameSet} {ps : Sequence patchUniverse from beforeq} {q : (pu_type patchUniverse) beforeq to} {rs : Sequence patchUniverse from mid'} {s : (pu_type patchUniverse) mid' beforeq} {q' : (pu_type patchUniverse) mid' mid} {s' : (pu_type patchUniverse) mid to}, @commuteOutRight patchUniverse from mid' beforeq ps rs s -> <> <~> <> -> commuteOutRight (ps :+> q :> []) (rs :+> q' :> []) s'. Notation "<< rs >> ~> << ps , q >>" := (commuteOutRight rs ps q) (at level 60, no associativity). *) Lemma TransitiveTransitiveCommute : forall {pu_type : NameSet -> NameSet -> Type} {ppu : PartPatchUniverse pu_type pu_type} {pui : PatchUniverseInv ppu ppu} {patchUniverse : PatchUniverse pui} {from to : NameSet} {ps qs rs : Sequence patchUniverse from to} (ps_qs : <> <~~>* <>) (qs_rs : <> <~~>* <>), (<> <~~>* <>). Proof with auto. intros. induction ps_qs as [? | ? ? ? s_commute_t ? IH]... apply IH in qs_rs. apply (Swap s_commute_t qs_rs). Qed. Lemma SymmetricCommute : forall {pu_type : NameSet -> NameSet -> Type} {ppu : PartPatchUniverse pu_type pu_type} {pui : PatchUniverseInv ppu ppu} {patchUniverse : PatchUniverse pui} {from to : NameSet} {ps qs : Sequence patchUniverse from to} (ps_qs : <> <~~> <>), (<> <~~> <>). Proof with auto. intros. induction ps_qs as [? ? ? ? ? ? ? ? ? ? ? ? ? ? commute | ?]. apply commuteSelfInverse in commute. apply (SwapNow _ _ _ _ commute). apply SwapLater... Qed. Lemma SymmetricTransitiveCommute : forall {pu_type : NameSet -> NameSet -> Type} {ppu : PartPatchUniverse pu_type pu_type} {pui : PatchUniverseInv ppu ppu} {patchUniverse : PatchUniverse pui} {from to : NameSet} {ps qs : Sequence patchUniverse from to} (ps_qs : <> <~~>* <>), (<> <~~>* <>). Proof with auto. intros. induction ps_qs as [? | ? ? ? s_commute_t ? IH]. apply Same. apply SymmetricCommute in s_commute_t. apply (TransitiveTransitiveCommute IH (Swap s_commute_t (Same _))). Qed. Lemma EnlargeTransitiveCommuteRelation : forall {pu_type : NameSet -> NameSet -> Type} {ppu : PartPatchUniverse pu_type pu_type} {pui : PatchUniverseInv ppu ppu} {patchUniverse : PatchUniverse pui} {from mid to : NameSet} {p : pu_type from mid} {qs rs : Sequence patchUniverse mid to} (pQsOK : ConsOK p qs) (pRsOK : ConsOK p rs) (qs_rs : <> <~~>* <>), (<< (p :> qs) >> <~~>* << (p :> rs) >>). Proof with auto. intros. induction qs_rs as [? | ? ? ? s_commute_t ? IH]. proofIrrel pQsOK pRsOK. apply Same. assert (ptOK : ConsOK p t). constructor. destruct pQsOK. rewrite <- (CommuteRelatesSameContents s_commute_t)... apply (Swap (SwapLater p _ _ s_commute_t) (IH ptOK pRsOK)). Qed. Lemma ConsEquality1 {pu_type : NameSet -> NameSet -> Type} {ppu : PartPatchUniverse pu_type pu_type} {pui : PatchUniverseInv ppu ppu} {pu : PatchUniverse pui} {from mid1 mid2 to : NameSet} {p : pu_type from mid1} {q : pu_type from mid2} {ps : Sequence pu mid1 to} {qs : Sequence pu mid2 to} {pConsOK : ConsOK p ps} {qConsOK : ConsOK q qs} (eq : p :> ps = q :> qs) : mid1 = mid2. Proof with auto. destruct ps. destruct qs. unfold consSeq in eq. dependent destruction eq... Qed. Lemma ConsEquality2 {pu_type : NameSet -> NameSet -> Type} {ppu : PartPatchUniverse pu_type pu_type} {pui : PatchUniverseInv ppu ppu} {pu : PatchUniverse pui} {from mid to : NameSet} {p : pu_type from mid} {q : pu_type from mid} {ps : Sequence pu mid to} {qs : Sequence pu mid to} {pConsOK : ConsOK p ps} {qConsOK : ConsOK q qs} (eq : p :> ps = q :> qs) : p = q /\ ps = qs. Proof with auto. destruct ps as [? psSequenceOK]. destruct qs as [? qsSequenceOK]. unfold consSeq in eq. dependent destruction eq. proofIrrel psSequenceOK qsSequenceOK. split... Qed. Lemma ConsEquality3 {pu_type : NameSet -> NameSet -> Type} {ppu : PartPatchUniverse pu_type pu_type} {pui : PatchUniverseInv ppu ppu} {pu : PatchUniverse pui} {from mid to : NameSet} {p : pu_type from mid} {ps : Sequence pu mid to} {pConsOK : ConsOK p ps} {qConsOK : ConsOK p ps} (eq : consSeq p ps pConsOK = consSeq p ps qConsOK) : pConsOK = qConsOK. Proof with auto. apply proof_irrelevance... Qed. Ltac consEquality hyp := let hyp' := fresh "H" in let H1 := fresh "H" in let H2 := fresh "H" in let H3 := fresh "H" in rename hyp into hyp'; set (H1 := ConsEquality1 hyp'); clearbody H1; subst; destruct (ConsEquality2 hyp') as [H2 hyp]; try (rewrite hyp in *); subst; try (set (H3 := ConsEquality3 hyp'); clearbody H3; subst); clear hyp'. Lemma commuteOutLeftConsistentStep : forall {pu_type : NameSet -> NameSet -> Type} {ppu : PartPatchUniverse pu_type pu_type} {pui : PatchUniverseInv ppu ppu} {patchUniverse : PatchUniverse pui} {from mid to : NameSet} {ps1 ps2 : Sequence patchUniverse from to} {q : pu_type from mid} {rs1 : Sequence patchUniverse mid to} (commute_relates_ps1_ps2 : <> <~~> <>) (q_rs1_commutes_left_out_of_ps1 : <> <~ <>), (exists rs2 : Sequence patchUniverse mid to, (<> <~~>* <>) /\ (<> <~ <>)). Proof with auto. intros. (** % \begin{igpic}{0}{4}{-1}{1} \drawpoint{from}{(0,0)} \definepoint{fromMid}{(2,0.5)} \drawpoint{mid}{(4,0)} \definepoint{midToA}{(7,0.5)} \definepoint{midToB}{(7,-0.5)} \drawpoint{to}{(10,0)} \definepoint{fromToA}{(5,2)} \definepoint{fromToB}{(5,-2)} \arrlab{from}{fromToA}{to}{bc}{$\seq{ps1}$} \arrlab{from}{fromToB}{to}{tc}{$\seq{ps2}$} \arrlab{from}{fromMid}{mid}{bc}{$q$} \arrlab{mid}{midToA}{to}{bc}{$\seq{rs1}$} \earrlab{mid}{midToB}{to}{tc}{$\seq{rs2}$} \end{igpic} % *) (* XXX disambig down to here *) dependent induction commute_relates_ps1_ps2 generalizing mid q rs1 q_rs1_commutes_left_out_of_ps1. (* This is the case where we have a swap at the head *) rename op into midA, opq into midB, oq into midC. rename q0 into s, q' into s'. rename H into p_s_commute_s'_p'. (** % \begin{igpic}{0}{4}{-1}{1} \drawlabpoint{from}{(0,0)}{cl} \drawlabpoint{mid}{(10,4)}{bc} \drawlabpoint{midA}{(4,2)}{tc} \drawlabpoint{midB}{(8,0)}{cr} \drawlabpoint{midC}{(4,-2)}{bc} \drawlabpoint{to}{(14,0)}{cl} \definepoint{fromMidA}{(1.5,1.5)} \definepoint{midAMidB}{(7,1.5)} \definepoint{fromMidC}{(1.5,-1.5)} \definepoint{midCMidB}{(7,-1.5)} \definepoint{midBTo}{(11,-0.5)} \definepoint{fromMid}{(3,3)} \definepoint{midTo}{(11,1.5)} \definepoint{midToX}{(13,2)} \arrlab{from}{fromMidA}{midA}{tl}{$p$} \arrlab{midA}{midAMidB}{midB}{bl}{$s$} \arrlab{from}{fromMidC}{midC}{tr}{$s'$} \arrlab{midC}{midCMidB}{midB}{tl}{$p'$} \arrlab{midB}{midBTo}{to}{tc}{$\seq{rs}$} \arrlab{from}{fromMid}{mid}{br}{$q$} \arrlab{mid}{midTo}{to}{tr}{$\seq{rs1}$} \earrlab{mid}{midToX}{to}{bl}{$\seq{rs2}$} \end{igpic} % *) dependent destruction q_rs1_commutes_left_out_of_ps1. (* This is the case where the commute out is done. But the swap has messed it up, so we will have to undo it to build the commute out. *) (** % \begin{igpic}{0}{4}{-1}{1} \drawlabpoint{from}{(0,0)}{cl} \drawlabpoint{midA}{(4,2)}{tc} \drawlabpoint{midB}{(8,0)}{cr} \drawlabpoint{midC}{(4,-2)}{bc} \drawlabpoint{to}{(14,0)}{cl} \definepoint{fromMidA}{(1.5,1.5)} \definepoint{midAMidB}{(7,1.5)} \definepoint{fromMidC}{(1.5,-1.5)} \definepoint{midCMidB}{(7,-1.5)} \definepoint{midBTo}{(11,-0.5)} \definepoint{midATo}{(11,2)} \arrlab{from}{fromMidA}{midA}{tl}{$p$} \arrlab{midA}{midAMidB}{midB}{bl}{$s$} \arrlab{from}{fromMidC}{midC}{tr}{$s'$} \arrlab{midC}{midCMidB}{midB}{tl}{$p'$} \arrlab{midB}{midBTo}{to}{tc}{$\seq{rs}$} \earrlab{midA}{midATo}{to}{bc}{$\seq{rs2}$} \end{igpic} % *) consEquality x. exists (q :> rs). split. apply Same. apply commuteSelfInverse in p_s_commute_s'_p'. refine (commuteOutLeftSwap _ _ _ p_s_commute_s'_p')... apply commuteOutLeftDone. (* This is the case where the commuteout actually does some work *) rename mid_q into midD. rename q into p'', p0 into q', p'0 into q, qs into us. rename H into p_q'_commute_q_p''. (** % \begin{igpic}{0}{4}{-1}{1} \drawlabpoint{from}{(0,0)}{cl} \drawlabpoint{mid}{(5,5)}{bc} \drawlabpoint{midD}{(7,3)}{bl} \drawlabpoint{midA}{(4,2)}{tc} \drawlabpoint{midB}{(8,0)}{cr} \drawlabpoint{midC}{(4,-2)}{bc} \drawlabpoint{to}{(14,2)}{cl} \definepoint{midMidD}{(6.5,4)} \definepoint{midAMidD}{(6,3)} \definepoint{midDTo}{(9,2.2)} \definepoint{fromMidA}{(1.5,1.5)} \definepoint{midAMidB}{(7,1.5)} \definepoint{fromMidC}{(1.5,-1.5)} \definepoint{midCMidB}{(7,-1.5)} \definepoint{midBTo}{(11,0.5)} \definepoint{fromMid}{(2,3)} \definepoint{midTo}{(12,4)} \arrlab{from}{fromMidA}{midA}{tl}{$p$} \arrlab{midA}{midAMidB}{midB}{bl}{$s$} \arrlab{from}{fromMidC}{midC}{tr}{$s'$} \arrlab{midC}{midCMidB}{midB}{tl}{$p'$} \arrlab{midB}{midBTo}{to}{tl}{$\seq{rs}$} \arrlab{from}{fromMid}{mid}{br}{$q$} \arrlab{mid}{midMidD}{midD}{bl}{$p''$} \arrlab{midA}{midAMidD}{midD}{br}{$q'$} \arrlab{midD}{midDTo}{to}{tr}{$\seq{us}$} \earrlab{mid}{midTo}{to}{bl}{$\seq{rs2}$} \end{igpic} % *) (* There are two possibilities: * The commuteout does exactly one commute, and the swap has just done it for us * The commuteout does more than one swap, and so we need to use the lemma to rewrite the last 2 swaps *) dependent destruction q_rs1_commutes_left_out_of_ps1. (* This is the case where the commuteout does exactly one commute, so we now have nothing to do *) consEquality x. consEquality x. rename q into s''. rename p_q'_commute_q_p'' into p_s_commute_s''_p''. (** % \begin{igpic}{0}{4}{-1}{1} \drawlabpoint{from}{(0,0)}{cl} \drawlabpoint{mid}{(4,4)}{bc} \drawlabpoint{midA}{(4,2)}{tc} \drawlabpoint{midB}{(8,0)}{cr} \drawlabpoint{midC}{(4,-2)}{bc} \drawlabpoint{to}{(10,2)}{cl} \definepoint{fromMidA}{(1.5,1.5)} \definepoint{midAMidB}{(7,1.5)} \definepoint{fromMidC}{(1.5,-1.5)} \definepoint{midCMidB}{(7,-1.5)} \definepoint{midBTo}{(9,0.5)} \definepoint{fromMid}{(1.5,2.5)} \definepoint{midMidB}{(7.5,2.5)} \definepoint{fromMid}{(1.5,3)} \definepoint{midTo}{(8,3.5)} \arrlab{from}{fromMidA}{midA}{tl}{$p$} \arrlab{midA}{midAMidB}{midB}{bl}{$s$} \arrlab{from}{fromMidC}{midC}{tr}{$s'$} \arrlab{midC}{midCMidB}{midB}{tl}{$p'$} \arrlab{from}{fromMid}{mid}{br}{$s''$} \arrlab{mid}{midMidB}{midB}{bl}{$p''$} \arrlab{midB}{midBTo}{to}{tl}{$\seq{rs}$} \earrlab{mid}{midTo}{to}{bl}{$\seq{rs2}$} \end{igpic} % *) doCommuteUnique p_s_commute_s'_p' p_s_commute_s''_p''. rename p'' into p', s'' into s'. rename mid into midC. (** % \begin{igpic}{0}{4}{-1}{1} \drawlabpoint{from}{(0,0)}{cl} \drawlabpoint{midA}{(4,2)}{tc} \drawlabpoint{midB}{(8,0)}{cr} \drawlabpoint{midC}{(4,-2)}{bc} \drawlabpoint{to}{(10,0)}{cl} \definepoint{fromMidA}{(1.5,1.5)} \definepoint{midAMidB}{(7,1.5)} \definepoint{fromMidC}{(1.5,-1.5)} \definepoint{midCMidB}{(7,-1.5)} \definepoint{midBTo}{(9,0.5)} \definepoint{midMidB}{(7.5,2.5)} \definepoint{midCTo}{(8,-2.5)} \arrlab{from}{fromMidA}{midA}{tl}{$p$} \arrlab{midA}{midAMidB}{midB}{bl}{$s$} \arrlab{from}{fromMidC}{midC}{tr}{$s'$} \arrlab{midC}{midCMidB}{midB}{tl}{$p'$} \arrlab{midB}{midBTo}{to}{bc}{$\seq{rs}$} \earrlab{midC}{midCTo}{to}{tl}{$\seq{rs2}$} \end{igpic} % *) assert (Heq : q_qsConsOK = pRsConsOK). apply proof_irrelevance. subst. exists (q0 :> rs). split. apply Same. apply commuteOutLeftDone. (* This is the case where the commuteout does at least commute2, so we have to jump over the swap *) consEquality x. consEquality x. rename mid_q into midE. rename p'0 into q'. rename p0 into r. rename q0 into t. rename qs into ss. rename H into s_r_commute_q'_t. (** % \begin{igpic}{0}{4}{-1}{1} \drawlabpoint{from}{(0,0)}{cl} \drawlabpoint{midA}{(4,2)}{tc} \drawlabpoint{midB}{(8,0)}{cr} \drawlabpoint{midC}{(4,-2)}{bc} \drawlabpoint{to}{(12,0)}{tc} \drawlabpoint{mid}{(4,4)}{tc} \drawlabpoint{midD}{(8,4)}{bl} \drawlabpoint{midE}{(11,3)}{bl} \definepoint{fromMidA}{(1.5,1.5)} \definepoint{midAMidB}{(7,1.5)} \definepoint{fromMidC}{(1.5,-1.5)} \definepoint{midCMidB}{(7,-1.5)} \definepoint{midBTo}{(10,0.5)} \definepoint{midMidB}{(7.5,2.5)} \definepoint{midTo}{(12,5.5)} \definepoint{fromMid}{(1.5,3)} \definepoint{midMidD}{(6,4.5)} \definepoint{midAMidD}{(6,3.5)} \definepoint{midDMidE}{(10,3.5)} \definepoint{midBMidE}{(9,2)} \definepoint{midETo}{(12,1.5)} \arrlab{from}{fromMidA}{midA}{tl}{$p$} \arrlab{midA}{midAMidB}{midB}{bl}{$s$} \arrlab{from}{fromMidC}{midC}{tr}{$s'$} \arrlab{midC}{midCMidB}{midB}{tl}{$p'$} \arrlab{midB}{midBTo}{to}{bc}{$\seq{rs}$} \arrlab{from}{fromMid}{mid}{br}{$q$} \arrlab{midA}{midAMidD}{midD}{bc}{$q'$} \arrlab{mid}{midMidD}{midD}{bc}{$p''$} \arrlab{midD}{midDMidE}{midE}{bl}{$t$} \arrlab{midB}{midBMidE}{midE}{tl}{$r$} \arrlab{midE}{midETo}{to}{bl}{$\seq{ss}$} \earrlab{mid}{midTo}{to}{bl}{$\seq{rs2}$} \end{igpic} % *) assert (H := commuteConsistent2 p_s_commute_s'_p' s_r_commute_q'_t p_q'_commute_q_p''). destruct H as [? [t' [p''' [r' [p''_t_commute_t'_p''' [p'_r_commute_r'_p''' s'_r'_commute_q_t']]]]]]. destruct (commuteNames p''_t_commute_t'_p''') as [name_p''_name_p''' [name_t_name_t' name_p_not_name_t]]. assert (p'''_ssConsOK : ConsOK p''' ss). constructor. destruct q_qsConsOK as [H]. rewrite SequenceContentsCons in H. rewrite <- name_p''_name_p'''. (* coq bug 2699 *) remember (sequenceContents ss) as ssContents. signedNameSetDec. assert (t'_p'''_ssConsOK : ConsOK t' (p''' :> ss)). constructor. destruct q_qsConsOK0 as [H]. rewrite SequenceContentsCons. rewrite <- name_p''_name_p'''. rewrite <- name_t_name_t'. clear - name_p_not_name_t H. (* coq bug 2699 *) remember (sequenceContents ss) as ssContents. signedNameSetDec. exists (t' :> p''' :> ss). split. apply (Swap (SwapNow _ _ _ _ p''_t_commute_t'_p''') (Same _)). refine (commuteOutLeftSwap _ _ _ s'_r'_commute_q_t'). refine (commuteOutLeftSwap _ _ _ p'_r_commute_r'_p''')... (* This is the case where we have a swap later *) dependent destruction q_rs1_commutes_left_out_of_ps1. (* This is the case where the commute out left is done. If the swap doesn't happen until later, then the commute out left is still done in the other sequence. *) consEquality x. exists rs. split. apply (Swap commute_relates_ps1_ps2 (Same _)). apply commuteOutLeftDone. (* And this is the real inductive case, which follows trivially by induction. *) consEquality x. specialize (IHcommute_relates_ps1_ps2 mid_q). specialize (IHcommute_relates_ps1_ps2 p0). specialize (IHcommute_relates_ps1_ps2 qs0). specialize (IHcommute_relates_ps1_ps2 q_rs1_commutes_left_out_of_ps1). destruct IHcommute_relates_ps1_ps2 as [? [? ?]]. assert (consOK : ConsOK q x). constructor. destruct q_qsConsOK. rewrite <- (TransitiveCommuteRelatesSameContents H0)... exists (q :> x). split. apply (EnlargeTransitiveCommuteRelation _ _ H0). apply (commuteOutLeftSwap _ _ H1 H). Qed. Lemma commuteOutLeftConsistent : forall {pu_type : NameSet -> NameSet -> Type} {ppu : PartPatchUniverse pu_type pu_type} {pui : PatchUniverseInv ppu ppu} {patchUniverse : PatchUniverse pui} {from mid to : NameSet} {ps1 ps2 : Sequence patchUniverse from to} {q : pu_type from mid} {rs1 : Sequence patchUniverse mid to} (ps1_ps2 : <> <~~>* <>) (p_out_of_ps1 : <> <~ <>), (exists rs2 : Sequence patchUniverse mid to, (<> <~~>* <>) /\ (<> <~ <>)). Proof with auto. intros. dependent induction ps1_ps2 generalizing rs1 p_out_of_ps1. (* ps1 = ps2 case *) exists rs1. split... apply Same. (* case where there is at least one commute to be done *) set (Hstep := commuteOutLeftConsistentStep H p_out_of_ps1). destruct Hstep as [rs2 [rs1_rs2 q_out_of_t]]. specialize (IHps1_ps2 rs2 q_out_of_t). destruct IHps1_ps2 as [rs3 [rs2_rs3 q_out_of_ps2]]. exists rs3. split... apply (TransitiveTransitiveCommute rs1_rs2 rs2_rs3). Qed. (* $\seq{p} q r \seq{s} <->* \seq{t} q' r' \seq{u}$ where $\name{q} = \name{q'}$ and $\name{r} = \name{r'}$. Then $\left( \commutes{q}{r} \right) <=> \left( \commutes{q'}{r'} \right)$. *) Lemma CommuteOutLeftPreservesCommute : forall {pu_type : NameSet -> NameSet -> Type} {ppu : PartPatchUniverse pu_type pu_type} {pui : PatchUniverseInv ppu ppu} {patchUniverse : PatchUniverse pui} {o op opq opqr opqrs ot : NameSet} {ps : Sequence patchUniverse o op} {q : pu_type op opq} {r : pu_type opq opqr} {ss : Sequence patchUniverse opqr opqrs} {t : pu_type o ot} {us : Sequence patchUniverse ot opqrs} (r_ssConsOK : ConsOK r ss) (q_r_ssConsOK : ConsOK q (r :> ss)) (ps_q_r_ssAppendOK : AppendOK ps (q :> r :> ss)) (t_q_different_names : pu_nameOf t <> pu_nameOf q) (t_r_different_names : pu_nameOf t <> pu_nameOf r) (commuteOut : <> <~ << ps :+> (q :> r :> ss) >>), (exists otp : NameSet, exists otpq : NameSet, exists otpqr : NameSet, exists ps' : Sequence patchUniverse ot otp, exists q' : pu_type otp otpq, exists r' : pu_type otpq otpqr, exists ss' : Sequence patchUniverse otpqr opqrs, exists r'_ss'ConsOK : ConsOK r' ss', exists q'_r'_ss'ConsOK : ConsOK q' (r' :> ss'), exists ps'_q'_r'_ss'AppendOK : AppendOK ps' (q' :> (r' :> ss')), (pu_nameOf q = pu_nameOf q') /\ (pu_nameOf r = pu_nameOf r') /\ (us = ps' :+> (q' :> (r' :> ss'))) /\ (~(q <~?~> r) -> ~(q' <~?~> r'))). Proof with auto. intros. destruct ps as [ps psOK]. revert opq opqr opqrs ot q r ss t us r_ssConsOK q_r_ssConsOK ps_q_r_ssAppendOK t_q_different_names t_r_different_names commuteOut. dependent induction ps. intros. rewrite AppendNilSeq in commuteOut. dependent destruction commuteOut. consEquality x. congruence. dependent destruction commuteOut. consEquality x. consEquality x. destruct (commuteNames H) as [? [? ?]]. congruence. exists ot. exists mid_q. exists mid_q0. exists []. exists q0. exists q1. exists qs. exists q_qsConsOK0. exists q_qsConsOK. solveExists. constructor. unfold sequenceContents. signedNameSetDec. consEquality x. consEquality x. split. destruct (commuteNames H0) as [? [? ?]]... split. destruct (commuteNames H) as [? [? ?]]... split. rewrite AppendNil. f_equal. intro. intro. elim H1. destruct H2 as [? [? [? ?]]]. apply commuteSelfInverse in H. apply commuteSelfInverse in H0. set (commuteConsistent := commuteConsistent1 H2 H0 H). destruct commuteConsistent as [? [? [? [? [? [? ?]]]]]]. unfold commutable. exists x2. exists x3. exists x4... intros. destruct (AppendConsSeq p ps (q :> r :> ss)) as [? [? [? ?]]]. rewrite H in commuteOut. move commuteOut at top. dependent destruction commuteOut. consEquality x. exists to. exists opq. exists opqr. exists (MkSequence ps x2). exists q. exists r. exists ss. exists r_ssConsOK. exists q_r_ssConsOK. exists x0. split... rename IHps into IH. consEquality x. specialize (IH x2). specialize (IH opq). specialize (IH opqr). specialize (IH opqrs). specialize (IH mid_q). specialize (IH q). specialize (IH r). specialize (IH ss). specialize (IH p0). specialize (IH qs). specialize (IH r_ssConsOK). specialize (IH q_r_ssConsOK). specialize (IH x0). destruct (commuteNames H) as [? [name_v_eq_name_v' ?]]. rewrite name_v_eq_name_v' in *. specialize (IH t_q_different_names). specialize (IH t_r_different_names). specialize (IH commuteOut). destruct IH as [otp [otpq [otpqr [ps' [q' [r' [ss' [r'_ss'ConsOK [q'_r'_ss'ConsOK [ps'_q'_r'_ss'AppendOK [? [? [ws_equals_ps'_q'_r'_ss' ? ]]]]]]]]]]]]]. exists otp. exists otpq. exists otpqr. subst. assert (q0_ps'ConsOK : ConsOK q0 ps'). constructor. destruct q_qsConsOK. rewrite SequenceContentsAppend in consNotAlreadyThere0. (* coq bug 2699 *) remember (pu_nameOf q0) as q0Name. remember (sequenceContents ps') as ps'Contents. remember (sequenceContents (q' :> r' :> ss')) as otherContents. signedNameSetDec. exists (q0 :> ps'). exists q'. exists r'. exists ss'. exists r'_ss'ConsOK. exists q'_r'_ss'ConsOK. solveExists. clear - ps'_q'_r'_ss'AppendOK q_qsConsOK. constructor. destruct ps'_q'_r'_ss'AppendOK. destruct q_qsConsOK. rewrite SequenceContentsCons. rewrite SequenceContentsCons. rewrite SequenceContentsCons. rewrite SequenceContentsAppend in consNotAlreadyThere0. rewrite SequenceContentsCons in consNotAlreadyThere0. rewrite SequenceContentsCons in consNotAlreadyThere0. rewrite SequenceContentsCons in appendNoIntersection0. rewrite SequenceContentsCons in appendNoIntersection0. (* coq bug 2699 *) remember (pu_nameOf q0) as q0Name. remember (pu_nameOf q') as q'Name. remember (pu_nameOf r') as r'Name. remember (sequenceContents ps') as ps'Contents. remember (sequenceContents ss') as ss'Contents. remember (SignedNameSetAdd q'Name (SignedNameSetAdd r'Name ss'Contents)) as q'r'ss'. clear - consNotAlreadyThere0 appendNoIntersection0. signedNameSetDec. split... split... split... destruct (AppendCons q0 ps' (q' :> r' :> ss')) as [? [? ?]]. rewrite H6. proofIrrel x ps'_q'_r'_ss'AppendOK. proofIrrel x3 q_qsConsOK... Qed. Lemma ShorterCounterExampleExists : forall {pu_type : NameSet -> NameSet -> Type} {ppu : PartPatchUniverse pu_type pu_type} {pui : PatchUniverseInv ppu ppu} {patchUniverse : PatchUniverse pui} {o op opq opqr opqrs opqrst ou our ours : NameSet} {p : pu_type o op} {qs : Sequence patchUniverse op opq} {r : pu_type opq opqr} {s : pu_type opqr opqrs} {ts : Sequence patchUniverse opqrs opqrst} {us : Sequence patchUniverse o ou} {r' : pu_type ou our} {s' : pu_type our ours} {vs : Sequence patchUniverse ours opqrst} (s_tsConsOK : ConsOK s ts) (r_s_tsConsOK : ConsOK r (s :> ts)) (qs_r_s_tsAppendOK : AppendOK qs (r :> s :> ts)) (p_qs_r_s_tsConsOK : ConsOK p (qs :+> r :> s :> ts)) (s'_vsConsOK : ConsOK s' vs) (r'_s'_vsConsOK : ConsOK r' (s' :> vs)) (us_r'_s'_vsAppendOK : AppendOK us (r' :> s' :> vs)) (H : << p :> qs :+> r :> s :> ts >> <~~>* << us :+> r' :> s' :> vs >>) (rs_same : pu_nameOf r = pu_nameOf r') (ss_same : pu_nameOf s = pu_nameOf s') (r_s_commutable : r <~?~> s) (r'_s'_not_commutable : ~(r' <~?~> s')), (exists ou' : NameSet, exists our' : NameSet, exists ours' : NameSet, exists us' : Sequence patchUniverse op ou', exists r'' : pu_type ou' our', exists s'' : pu_type our' ours', exists vs' : Sequence patchUniverse ours' opqrst, exists s''_vs'ConsOK : ConsOK s'' vs', exists r''_s''_vs'ConsOK : ConsOK r'' (s'' :> vs'), exists us'_r''_s''_vs'AppendOK : AppendOK us' (r'' :> s'' :> vs'), << qs :+> r :> s :> ts >> <~~>* << us' :+> r'' :> s'' :> vs' >> /\ (pu_nameOf r = pu_nameOf r'') /\ (pu_nameOf s = pu_nameOf s'') /\ ~(r'' <~?~> s'')). Proof with auto. intros. assert (p_out_of_lhs: < r :> s :> ts>> <~ <

qs :+> r :> s :> ts>>). apply commuteOutLeftDone. set (p_out_of_rhs := commuteOutLeftConsistent H p_out_of_lhs). destruct p_out_of_rhs as [? [transitive_commute p_out_of_rhs]]. assert (p_not_r : pu_nameOf p <> pu_nameOf r). clear - p_qs_r_s_tsConsOK. destruct p_qs_r_s_tsConsOK. rewrite SequenceContentsAppend in consNotAlreadyThere0. rewrite SequenceContentsCons in consNotAlreadyThere0. rewrite SequenceContentsCons in consNotAlreadyThere0. (* coq bug 2699 *) remember (sequenceContents qs) as qsContents. remember (sequenceContents ts) as tsContents. remember (pu_nameOf p) as pName. remember (pu_nameOf r) as rName. remember (pu_nameOf s) as sName. signedNameSetDec. assert (p_not_r' : pu_nameOf p <> pu_nameOf r'). rewrite <- rs_same... assert (p_not_s : pu_nameOf p <> pu_nameOf s). clear - p_qs_r_s_tsConsOK. destruct p_qs_r_s_tsConsOK. rewrite SequenceContentsAppend in consNotAlreadyThere0. rewrite SequenceContentsCons in consNotAlreadyThere0. rewrite SequenceContentsCons in consNotAlreadyThere0. (* coq bug 2699 *) remember (sequenceContents qs) as qsContents. remember (sequenceContents ts) as tsContents. remember (pu_nameOf p) as pName. remember (pu_nameOf r) as rName. remember (pu_nameOf s) as sName. signedNameSetDec. assert (p_not_s' : pu_nameOf p <> pu_nameOf s'). rewrite <- ss_same... set (HX := CommuteOutLeftPreservesCommute _ _ _ p_not_r' p_not_s' p_out_of_rhs). destruct HX as [opp [oppq [oppqr [ps'' [q'' [r'' [ss'' [r''_ss''ConsOK [q''_r''_ss''ConsOK [ps''_q''_r''_ss''AppendOK [? [? [? ?]]] ] ]] ]] ]]]]]. exists opp. exists oppq. exists oppqr. exists ps''. exists q''. exists r''. exists ss''. exists r''_ss''ConsOK. exists q''_r''_ss''ConsOK. exists ps''_q''_r''_ss''AppendOK. subst. split... split. rewrite rs_same... rewrite ss_same... Qed. Lemma EmptyCounterExampleExists : forall {pu_type : NameSet -> NameSet -> Type} {ppu : PartPatchUniverse pu_type pu_type} {pui : PatchUniverseInv ppu ppu} {patchUniverse : PatchUniverse pui} {o oq oqr oqrs ou our ours : NameSet} {qs : Sequence patchUniverse o oq} {r : pu_type oq oqr} {s : pu_type oqr oqrs} {us : Sequence patchUniverse o ou} {r' : pu_type ou our} {s' : pu_type our ours} {vs : Sequence patchUniverse ours oqrs} (s_NilConsOK : ConsOK s []) (r_s_tsConsOK : ConsOK r (s :> [])) (qs_r_s_NilAppendOK : AppendOK qs (r :> s :> [])) (s'_vsConsOK : ConsOK s' vs) (r'_s'_vsConsOK : ConsOK r' (s' :> vs)) (us_r'_s'_vsAppendOK : AppendOK us (r' :> s' :> vs)) (* t omitted for now *) (transitive_commute : < r :> s :> []>> <~~>* < r' :> s' :> vs>>) (rs_same : pu_nameOf r = pu_nameOf r') (ss_same : pu_nameOf s = pu_nameOf s') (r_s_commutable : r <~?~> s) (r'_s'_not_commutable : ~(r' <~?~> s')), ( exists lNil_r_s_NilAppendOK : AppendOK [] (r :> s :> []), exists ou' : NameSet, exists our' : NameSet, exists ours' : NameSet, exists us' : Sequence patchUniverse oq ou', exists r'' : pu_type ou' our', exists s'' : pu_type our' ours', exists vs' : Sequence patchUniverse ours' oqrs, exists s''_vs'ConsOK : ConsOK s'' vs', exists r''_s''_vs'ConsOK : ConsOK r'' (s'' :> vs'), exists us'_r''_s''_vs'AppendOK : AppendOK us' (r'' :> s'' :> vs'), TransitiveCommuteRelates ([] :+> r :> s :> []) (us' :+> r'' :> s'' :> vs') /\ (pu_nameOf r = pu_nameOf r') /\ (pu_nameOf s = pu_nameOf s') /\ ~(r'' <~?~> s'')). Proof with trivial. intros. destruct qs. rename s0 into qs. move qs at top. revert oqr oqrs ou our ours r s us r' s' vs s_NilConsOK r_s_tsConsOK qs_r_s_NilAppendOK s'_vsConsOK r'_s'_vsConsOK us_r'_s'_vsAppendOK transitive_commute rs_same ss_same r_s_commutable r'_s'_not_commutable. dependent induction qs. (* [] case *) intros. solveExists. constructor. rewrite SequenceContentsNil. signedNameSetDec. exists ou. exists our. exists ours. exists us. exists r'. exists s'. exists vs. exists s'_vsConsOK. exists r'_s'_vsConsOK. exists us_r'_s'_vsAppendOK. split. rewrite AppendNil. rewrite AppendNilSeq in transitive_commute... split... split... (* Cons case *) intros. unfold block in IHqs. destruct (AppendConsSeq p qs (r :> s :> [])) as [? [? [? ?]]]. rewrite H in transitive_commute. set (HX := ShorterCounterExampleExists _ _ _ _ _ _ _ transitive_commute rs_same ss_same r_s_commutable r'_s'_not_commutable). destruct HX as [ou' [our' [ours' [us' [r'' [s'' [vs' [s''_vs'ConsOK [r''_s''_vs'ConsOK [us'_r''_s''_vs'AppendOK [transitive_commute_3 [r_r''_same [s_s''_same r''_s''_not_commutable ]]]]]]]]]]]]]. specialize (IHqs x). specialize (IHqs oqr oqrs). specialize (IHqs ou' our' ours'). specialize (IHqs r s). specialize (IHqs us' r'' s'' vs'). specialize (IHqs s_NilConsOK). specialize (IHqs r_s_tsConsOK). specialize (IHqs x0). specialize (IHqs s''_vs'ConsOK). specialize (IHqs r''_s''_vs'ConsOK). specialize (IHqs us'_r''_s''_vs'AppendOK). specialize (IHqs transitive_commute_3). specialize (IHqs r_r''_same s_s''_same). specialize (IHqs r_s_commutable r''_s''_not_commutable). destruct IHqs as [lNil_r_s_NilAppendOK [ou'' [our'' [ours'' [us'' [r''' [s''' [vs'' [s'''_vs''ConsOK [r'''_s'''_vs''ConsOK [us''_r'''_s'''_vs''AppendOK [? [? [? ?]]] ]]]]]]]]]]]. exists lNil_r_s_NilAppendOK. exists ou''. exists our''. exists ours''. exists us''. exists r'''. exists s'''. exists vs''. exists s'''_vs''ConsOK. exists r'''_s'''_vs''ConsOK. exists us''_r'''_s'''_vs''AppendOK. repeat split... Qed. Lemma TwoSequenceTransitiveCommuteRelatesTwoSequence1 : forall {pu_type : NameSet -> NameSet -> Type} {ppu : PartPatchUniverse pu_type pu_type} {pui : PatchUniverseInv ppu ppu} {patchUniverse : PatchUniverse pui} {o or ors ou our ours : NameSet} {r : pu_type o or} {s : pu_type or ors} {us : Sequence patchUniverse o ou} {r' : pu_type ou our} {s' : pu_type our ours} {vs : Sequence patchUniverse ours ors} (s_NilConsOK : ConsOK s []) (r_s_NilConsOK : ConsOK r (s :> [])) (Nil_r_s_NilAppendOK : AppendOK [] (r :> (s :> []))) (s'_vsConsOK : ConsOK s' vs) (r'_s'_vsConsOK : ConsOK r' (s' :> vs)) (us_r'_s'_vsAppendOK : AppendOK us (r' :> (s' :> vs))) , (<<[] :+> r :> s :> []>> <~~>* < r' :> s' :> vs>>) -> (ou = o) /\ (ours = ors). Proof with auto. intros. rewrite AppendNil in H. (* XXX Remove this, and don't take [] *) dependent induction H. (* This is the case where the transitive commute is finished *) destruct us. dependent destruction s0. (* This is the case where the original us is [] *) split... rewrite AppendNilSeq in x. consEquality x. consEquality x... destruct (AppendConsSeq p s0 (r' :> s' :> vs)) as [? [? [? Heq1]]]. rewrite Heq1 in x. consEquality x. destruct s0. rewrite AppendNilSeq in x. consEquality x. symmetry in x. contradiction (ConsEqNil x). destruct (AppendConsSeq p0 s0 (r' :> s' :> vs)) as [? [? [? Heq2]]]. rewrite Heq2 in x. consEquality x. destruct s0. rewrite AppendNilSeq in x. symmetry in x. contradiction (ConsEqNil x). destruct (AppendConsSeq p1 s0 (r' :> s' :> vs)) as [? [? [? Heq3]]]. rewrite Heq3 in x. symmetry in x. contradiction (ConsEqNil x). dependent destruction H. consEquality x. consEquality x. rename IHTransitiveCommuteRelates into IH. specialize (IH ours). specialize (IH vs). specialize (IH our). specialize (IH s'). specialize (IH s'_vsConsOK). specialize (IH ou). specialize (IH us). specialize (IH r'). specialize (IH r'_s'_vsConsOK). specialize (IH us_r'_s'_vsAppendOK). specialize (IH oq). specialize (IH q'). specialize (IH p'). specialize (IH pRsConsOK). specialize (IH qPRsConsOK). solveFirstIn IH. constructor. rewrite SequenceContentsNil. signedNameSetDec. specialize (IH eq_refl). specialize (IH eq_refl). unfold block in IH... consEquality x. dependent destruction H. consEquality x. contradiction (ConsEqNil x). consEquality x. dependent destruction H. contradiction (ConsEqNil x). contradiction (ConsEqNil x). Qed. Lemma TwoSequenceTransitiveCommuteRelatesTwoSequence2 : forall {pu_type : NameSet -> NameSet -> Type} {ppu : PartPatchUniverse pu_type pu_type} {pui : PatchUniverseInv ppu ppu} {patchUniverse : PatchUniverse pui} {o or ors our: NameSet} {r : pu_type o or} {s : pu_type or ors} {us : Sequence patchUniverse o o} {r' : pu_type o our} {s' : pu_type our ors} {vs : Sequence patchUniverse ors ors} (s_NilConsOK : ConsOK s []) (r_s_NilConsOK : ConsOK r (s :> [])) (Nil_r_s_NilAppendOK : AppendOK [] (r :> (s :> []))) (s'_vsConsOK : ConsOK s' vs) (r'_s'_vsConsOK : ConsOK r' (s' :> vs)) (us_r'_s'_vsAppendOK : AppendOK us (r' :> (s' :> vs))) , (<<[] :+> r :> s :> []>> <~~>* < r' :> s' :> vs>>) -> ((us = []) /\ (vs = [])). Proof with auto. intros. rewrite AppendNil in H. (* XXX Remove this, and don't take [] *) dependent induction H. destruct us. dependent destruction s0. split. unfold nilSeq. f_equal. apply proof_irrelevance. rewrite AppendNilSeq in x. consEquality x. consEquality x... destruct (AppendConsSeq p s0 (r' :> s' :> vs)) as [? [? [? Heq1]]]. rewrite Heq1 in x. consEquality x. destruct s0. rewrite AppendNilSeq in x. consEquality x. symmetry in x. contradiction (ConsEqNil x). destruct (AppendConsSeq p0 s0 (r' :> s' :> vs)) as [? [? [? Heq2]]]. rewrite Heq2 in x. consEquality x. destruct s0. rewrite AppendNilSeq in x. symmetry in x. contradiction (ConsEqNil x). destruct (AppendConsSeq p1 s0 (r' :> s' :> vs)) as [? [? [? Heq3]]]. rewrite Heq3 in x. symmetry in x. contradiction (ConsEqNil x). dependent destruction H. consEquality x. consEquality x. rename IHTransitiveCommuteRelates into IH. specialize (IH vs). specialize (IH us). specialize (IH our). specialize (IH r'). specialize (IH s'). specialize (IH s'_vsConsOK). specialize (IH r'_s'_vsConsOK). specialize (IH us_r'_s'_vsAppendOK). specialize (IH oq). specialize (IH q'). specialize (IH p'). specialize (IH pRsConsOK). specialize (IH qPRsConsOK). solveFirstIn IH. constructor. rewrite SequenceContentsNil. signedNameSetDec. specialize (IH eq_refl). specialize (IH eq_refl). unfold block in IH... consEquality x. dependent destruction H. consEquality x. contradiction (ConsEqNil x). consEquality x. dependent destruction H. contradiction (ConsEqNil x). contradiction (ConsEqNil x). Qed. Lemma commuteInSequenceConsistent : forall {pu_type : NameSet -> NameSet -> Type} {ppu : PartPatchUniverse pu_type pu_type} {pui : PatchUniverseInv ppu ppu} {patchUniverse : PatchUniverse pui} {o oq oqr oqrs (* oqrst *) ou our ours : NameSet} {qs : Sequence patchUniverse o oq} {r : pu_type oq oqr} {s : pu_type oqr oqrs} (* {ts : Sequence patchUniverse _ oqrs oqrst} *) {us : Sequence patchUniverse o ou} {r' : pu_type ou our} {s' : pu_type our ours} {vs : Sequence patchUniverse ours oqrs} (s_NilConsOK : ConsOK s []) (r_s_NilConsOK : ConsOK r (s :> [])) (qs_r_s_NilAppendOK : AppendOK qs (r :> s :> [])) (s'_vsConsOK : ConsOK s' vs) (r'_s'_vsConsOK : ConsOK r' (s' :> vs)) (us_r'_s'_vsAppendOK : AppendOK us (r' :> (s' :> vs))) (transitive_commute : < r :> s :> []>> <~~>* < r' :> s' :> vs>>) (rs_same : pu_nameOf r = pu_nameOf r') (ss_same : pu_nameOf s = pu_nameOf s') (r_s_commutable : r <~?~> s), (r' <~?~> s'). Proof with trivial. intros. case (commutable_dec r' s')... intros. destruct s0 as [? [? [? ?]]]. exists x. exists x0. exists x1... intro r'_s'_not_commutable. destruct (EmptyCounterExampleExists _ _ _ _ _ _ transitive_commute rs_same ss_same r_s_commutable r'_s'_not_commutable) as [? [? [? [? [? [r'' [s'' [? [? [? [? [HX [? [? not_commutable]]]]]]]]]]]]]]. (* XXX rewrite AppendNil in HX. *) assert (HY : <<[] :+> r :> s :> []>> <~~>* <<[] :+> r :> s :> []>>). apply Same. (* XXX rewrite AppendNil in HY. *) destruct (TwoSequenceTransitiveCommuteRelatesTwoSequence1 _ _ _ _ _ _ HX). destruct (TwoSequenceTransitiveCommuteRelatesTwoSequence1 _ _ _ _ _ _ HY). subst. destruct (TwoSequenceTransitiveCommuteRelatesTwoSequence2 _ _ _ _ _ _ HX) as [? ?]. destruct (TwoSequenceTransitiveCommuteRelatesTwoSequence2 _ _ _ _ _ _ HY) as [? ?]. subst. assert (r'' <~?~> s''). apply SymmetricTransitiveCommute in HX. apply (TransitiveTransitiveCommute HX) in HY. dependent destruction HX... rewrite AppendNil in HY. rewrite AppendNil in H1. dependent destruction H1. consEquality x. consEquality x. exists oq0. exists q'. exists p'... consEquality x. dependent destruction H1. consEquality x. contradiction (ConsEqNil x). consEquality x. dependent destruction H1. contradiction (ConsEqNil x). contradiction (ConsEqNil x). contradiction. Qed. (** % \end{Ilemma} XXX Is this right? Looks wrong to me now: \start{lemma}{patch-in-sequence-has-minimal-context} If $\seq{p} q \seq{r} s \seq{t} <->* \seq{u} q' \seq{v}$ (where $\name{q} = \name{q'}$) and $\name{q} \notin \names{\seq{u}}$, then $\commutes{q}{\seq{r} s}$. \begin{Iexplanation} Within a sequence, a patch has a minimal context. \end{Iexplanation} \begin{Iproof} Suppose, for the purpose of contraction, that we have a counterexample. Given $s$, let us consider the right-most $q$ for which the property doesn't hold. Then $\names{\seq{r}} \subseteq \names{\seq{u}}$, so at some point during the $<->*$ relation $q$ commuted with each of them, and with $s$. Therefore, by \refLemma{commute-in-sequence-consistent}, it can be commuted past them all. But we assumed that it could not. Contradiction. \end{Iproof} \end{Ilemma} \start{lemma}{patch-in-universe-has-minimal-context} If $\seq{ps} q \seq{r} s \seq{t}$ and $\seq{u} q' \seq{v}$, where $\name{q} = \name{q'}$ and $\name{q} \notin \names{\seq{u}}$, are in a patch universe then $\pair{q}{\seq{r} s} <-> \pair{\seq{r'} s'}{q''}$. \begin{Iexplanation} Within a patch universe, a patch has a minimal context. \end{Iexplanation} \begin{Iproof} When a patch is first recorded, \refLemma{patch-in-sequence-has-minimal-context} tells us that it has a minimal context. Another patch being recorded or unrecorded trivially doesn't alter its minimal context, as both operations act on the end of the patch sequence. Commute trivially doesn't affect the minimal context, as the sequence doesn't change. When merging, the patch is either in the common prefix or one of the suffixes. If it is in the common prefix or the suffix that remains unchanged then the minimal context is unaffected for the same reason that it is when recording new patches. If it is in the other suffix, then the definition of $\partialmergeName$ tells us that we can commute it to give us the case where it is in the first suffix, so this case is satisfied too. \end{Iproof} \end{Ilemma} XXX This is one of the important theorems: That given a patch universe, we can get to the point that the merge algorithm starts at \start{theorem}{patch-universe-provides-merge-input} Suppose we have two patch sequences $\seq{p}$ and $\seq{q}$. Then $\single{\seq{p}} <->* \single{\seq{r}\seq{s}}$ and $\single{\seq{q}} <->* \single{\seq{r}\seq{t}}$ where $\names{\seq{s}} \cap \names{\seq{t}} = \emptyset$. \begin{Iexplanation} XXX \end{Iexplanation} \begin{Iproof} XXX \end{Iproof} \end{Itheorem} XXX Sequences will be considered equal if they are equal up to commutation; in particular, when we talk about something like $\seq{p} \seq{q}$ we mean ``a sequence $\seq{r}$ which, after some number of commutations, is equal to $\seq{p} \seq{q}$''. % *) End patch_universes.