{
addfile ./src/unit_nocommute.v
hunk ./src/unit_nocommute.v 1
+Require Import unnamed_patches.
hunk ./src/unit_nocommute.v 3
+Inductive Unit : Set
+    := MkUnit .
+
+
+Definition unitInverse (x : Unit) : Unit :=
+    match x with
+    MkUnit => MkUnit
+    end.
+
+Definition unitCommute (x y x' y' : Unit) : Prop :=
+    match x, y, x', y' with
+    MkUnit, MkUnit, MkUnit, MkUnit => False
+    end.
+
+Notation "p ^u" := (unitInverse p).
+
+Lemma unitInverseInverse : forall (p : Unit), (p ^u)^u = p.
+Proof.
+intros.
+destruct p.
+unfold unitInverse.
+auto.
+Qed.
+
+Lemma UnitCommuteUnique : forall p q p' q' p'' q'' : Unit,
+  unitCommute p q q' p' -> unitCommute p q q'' p'' -> p' = p'' /\ q' = q''.
+Proof.
+intros.
+destruct p.
+destruct q.
+destruct p'.
+destruct q'.
+destruct p''.
+destruct q''.
+auto.
+Qed.
+
+
+Lemma UnitCommutable_dec : forall p q : Unit,
+  {q' : Unit & {p' : Unit & unitCommute p q q' p'}} +
+  {~ (exists q' p' : Unit, unitCommute p q q' p')}.
+Proof.
+destruct p.
+destruct q.
+simpl.
+intuition.
+right.
+intros.
+destruct H.
+destruct H.
+destruct x.
+destruct x0.
+elim H.
+Qed.
+
+Lemma UnitCommuteSelfInverse : forall p q p' q' : Unit, unitCommute p q q' p' <-> unitCommute q' p' p q.
+Proof.
+intros.
+destruct p.
+destruct q.
+destruct p'.
+destruct q'.
+simpl.
+tauto.
+Qed.
+
+
+Lemma UnitCommuteSquare : forall p q p' q' : Unit, unitCommute p q q' p' -> unitCommute (q' ^u) p p' (q ^u).
+Proof.
+intros.
+destruct p.
+destruct q.
+destruct p'.
+destruct q'.
+unfold unitInverse.
+destruct H.
+Qed.
+
+
+Lemma UnitCommuteConsistent1 : forall p1 q1 r1 q2 r2 q3 r3 p3 p5 : Unit,
+  unitCommute q1 r1 r2 q2 ->
+  unitCommute p1 q1 q3 p5 ->
+  unitCommute p5 r1 r3 p3 ->
+  exists r4 q4 p6 : Unit,
+    unitCommute q3 r3 r4 q4 /\
+    unitCommute p1 r2 r4 p6 /\ unitCommute p6 q2 q4 p3.
+Proof.
+intros.
+destruct p1.
+destruct q1.
+destruct r1.
+destruct q2.
+destruct r2.
+destruct q3.
+destruct r3.
+destruct p3.
+destruct p5.
+elim H.
+Qed.
+
+
+Lemma UnitCommuteConsistent2 : forall p3 q3 r3 q4 r4 q1 r1 p1 p5 : Unit,
+  unitCommute q3 r3 r4 q4 ->
+  unitCommute r3 p3 p5 r1 ->
+  unitCommute q3 p5 p1 q1 ->
+  exists r2 q2 p6 : Unit,
+    unitCommute q1 r1 r2 q2 /\
+    unitCommute q4 p3 p6 q2 /\ unitCommute r4 p6 p1 r2.
+Proof.
+intros.
+destruct p3.
+destruct q3.
+destruct r3.
+destruct q4.
+destruct r4.
+destruct q1.
+destruct r1.
+destruct p1.
+destruct p5.
+elim H.
+Qed.
+
+Definition UnitUnnamedPatch : UnnamedPatch :=
+    mkUnnamedPatch
+        Unit
+        unitInverse
+        unitInverseInverse
+        unitCommute
+        UnitCommuteUnique
+        UnitCommutable_dec
+        UnitCommuteSelfInverse
+        UnitCommuteSquare
+        UnitCommuteConsistent1
+        UnitCommuteConsistent2.
addfile ./src/unit_alwayscommute.v
hunk ./src/unit_alwayscommute.v 1
+Require Import unnamed_patches.
hunk ./src/unit_alwayscommute.v 3
+Inductive Unit : Set
+    := MkUnit .
+
+
+Definition unitInverse (x : Unit) : Unit :=
+    match x with
+    MkUnit => MkUnit
+    end.
+
+Definition unitCommute (x y x' y' : Unit) : Prop :=
+    match x, y, x', y' with
+    MkUnit, MkUnit, MkUnit, MkUnit => True
+    end.
+
+Notation "p ^u" := (unitInverse p).
+
+Lemma unitInverseInverse : forall (p : Unit), (p ^u)^u = p.
+Proof.
+intros.
+destruct p.
+unfold unitInverse.
+auto.
+Qed.
+
+Lemma UnitCommuteUnique : forall p q p' q' p'' q'' : Unit,
+  unitCommute p q q' p' -> unitCommute p q q'' p'' -> p' = p'' /\ q' = q''.
+Proof.
+intros.
+destruct p.
+destruct q.
+destruct p'.
+destruct q'.
+destruct p''.
+destruct q''.
+auto.
+Qed.
+
+
+Lemma UnitCommutable_dec : forall p q : Unit,
+  {q' : Unit & {p' : Unit & unitCommute p q q' p'}} +
+  {~ (exists q' p' : Unit, unitCommute p q q' p')}.
+Proof.
+intros.
+destruct p.
+destruct q.
+left.
+unfold unitCommute.
+exists MkUnit.
+exists MkUnit.
+trivial.
+Qed.
+
+Lemma UnitCommuteSelfInverse : forall p q p' q' : Unit, unitCommute p q q' p' <-> unitCommute q' p' p q.
+Proof.
+intros.
+destruct p.
+destruct q.
+destruct p'.
+destruct q'.
+simpl.
+tauto.
+Qed.
+
+
+Lemma UnitCommuteSquare : forall p q p' q' : Unit, unitCommute p q q' p' -> unitCommute (q' ^u) p p' (q ^u).
+Proof.
+intros.
+destruct p.
+destruct q.
+destruct p'.
+destruct q'.
+unfold unitInverse.
+trivial.
+Qed.
+
+
+Lemma UnitCommuteConsistent1 : forall p1 q1 r1 q2 r2 q3 r3 p3 p5 : Unit,
+  unitCommute q1 r1 r2 q2 ->
+  unitCommute p1 q1 q3 p5 ->
+  unitCommute p5 r1 r3 p3 ->
+  exists r4 q4 p6 : Unit,
+    unitCommute q3 r3 r4 q4 /\
+    unitCommute p1 r2 r4 p6 /\ unitCommute p6 q2 q4 p3.
+Proof.
+intros.
+destruct p1.
+destruct q1.
+destruct r1.
+destruct q2.
+destruct r2.
+destruct q3.
+destruct r3.
+destruct p3.
+destruct p5.
+exists MkUnit.
+exists MkUnit.
+exists MkUnit.
+split.
+split.
+split.
+trivial.
+trivial.
+Qed.
+
+
+Lemma UnitCommuteConsistent2 : forall p3 q3 r3 q4 r4 q1 r1 p1 p5 : Unit,
+  unitCommute q3 r3 r4 q4 ->
+  unitCommute r3 p3 p5 r1 ->
+  unitCommute q3 p5 p1 q1 ->
+  exists r2 q2 p6 : Unit,
+    unitCommute q1 r1 r2 q2 /\
+    unitCommute q4 p3 p6 q2 /\ unitCommute r4 p6 p1 r2.
+Proof.
+intros.
+destruct p3.
+destruct q3.
+destruct r3.
+destruct q4.
+destruct r4.
+destruct q1.
+destruct r1.
+destruct p1.
+destruct p5.
+exists MkUnit.
+exists MkUnit.
+exists MkUnit.
+split.
+split.
+split.
+trivial.
+trivial.
+Qed.
+
+Definition UnitUnnamedPatch : UnnamedPatch :=
+    mkUnnamedPatch
+        Unit
+        unitInverse
+        unitInverseInverse
+        unitCommute
+        UnitCommuteUnique
+        UnitCommutable_dec
+        UnitCommuteSelfInverse
+        UnitCommuteSquare
+        UnitCommuteConsistent1
+        UnitCommuteConsistent2.
hunk ./src/unit_alwayscommute.v 3
-Inductive Unit : Set
-    := MkUnit .
-
-
-Definition unitInverse (x : Unit) : Unit :=
-    match x with
-    MkUnit => MkUnit
-    end.
-
-Definition unitCommute (x y x' y' : Unit) : Prop :=
-    match x, y, x', y' with
-    MkUnit, MkUnit, MkUnit, MkUnit => True
-    end.
-
-Notation "p ^u" := (unitInverse p).
-
-Lemma unitInverseInverse : forall (p : Unit), (p ^u)^u = p.
-Proof.
-intros.
-destruct p.
-unfold unitInverse.
-auto.
-Qed.
-
-Lemma UnitCommuteUnique : forall p q p' q' p'' q'' : Unit,
-  unitCommute p q q' p' -> unitCommute p q q'' p'' -> p' = p'' /\ q' = q''.
-Proof.
-intros.
-destruct p.
-destruct q.
-destruct p'.
-destruct q'.
-destruct p''.
-destruct q''.
-auto.
-Qed.
-
-
-Lemma UnitCommutable_dec : forall p q : Unit,
-  {q' : Unit & {p' : Unit & unitCommute p q q' p'}} +
-  {~ (exists q' p' : Unit, unitCommute p q q' p')}.
-Proof.
-intros.
-destruct p.
-destruct q.
-left.
-unfold unitCommute.
-exists MkUnit.
-exists MkUnit.
-trivial.
-Qed.
-
-Lemma UnitCommuteSelfInverse : forall p q p' q' : Unit, unitCommute p q q' p' <-> unitCommute q' p' p q.
-Proof.
-intros.
-destruct p.
-destruct q.
-destruct p'.
-destruct q'.
-simpl.
-tauto.
-Qed.
-
-
-Lemma UnitCommuteSquare : forall p q p' q' : Unit, unitCommute p q q' p' -> unitCommute (q' ^u) p p' (q ^u).
-Proof.
-intros.
-destruct p.
-destruct q.
-destruct p'.
-destruct q'.
-unfold unitInverse.
-trivial.
-Qed.
-
-
-Lemma UnitCommuteConsistent1 : forall p1 q1 r1 q2 r2 q3 r3 p3 p5 : Unit,
-  unitCommute q1 r1 r2 q2 ->
-  unitCommute p1 q1 q3 p5 ->
-  unitCommute p5 r1 r3 p3 ->
-  exists r4 q4 p6 : Unit,
-    unitCommute q3 r3 r4 q4 /\
-    unitCommute p1 r2 r4 p6 /\ unitCommute p6 q2 q4 p3.
-Proof.
-intros.
-destruct p1.
-destruct q1.
-destruct r1.
-destruct q2.
-destruct r2.
-destruct q3.
-destruct r3.
-destruct p3.
-destruct p5.
-exists MkUnit.
-exists MkUnit.
-exists MkUnit.
-split.
-split.
-split.
-trivial.
-trivial.
-Qed.
-
-
-Lemma UnitCommuteConsistent2 : forall p3 q3 r3 q4 r4 q1 r1 p1 p5 : Unit,
-  unitCommute q3 r3 r4 q4 ->
-  unitCommute r3 p3 p5 r1 ->
-  unitCommute q3 p5 p1 q1 ->
-  exists r2 q2 p6 : Unit,
-    unitCommute q1 r1 r2 q2 /\
-    unitCommute q4 p3 p6 q2 /\ unitCommute r4 p6 p1 r2.
-Proof.
-intros.
-destruct p3.
-destruct q3.
-destruct r3.
-destruct q4.
-destruct r4.
-destruct q1.
-destruct r1.
-destruct p1.
-destruct p5.
-exists MkUnit.
-exists MkUnit.
-exists MkUnit.
-split.
-split.
-split.
-trivial.
-trivial.
-Qed.
-
-Definition UnitUnnamedPatch : UnnamedPatch :=
-    mkUnnamedPatch
-        Unit
-        unitInverse
-        unitInverseInverse
-        unitCommute
-        UnitCommuteUnique
-        UnitCommutable_dec
-        UnitCommuteSelfInverse
-        UnitCommuteSquare
-        UnitCommuteConsistent1
-        UnitCommuteConsistent2.
hunk ./src/unit_alwayscommute.v 1
-Require Import unnamed_patches.
rmfile ./src/unit_alwayscommute.v
hunk ./src/unit_nocommute.v 3
-Inductive Unit : Set
-    := MkUnit .
-
-
-Definition unitInverse (x : Unit) : Unit :=
-    match x with
-    MkUnit => MkUnit
-    end.
-
-Definition unitCommute (x y x' y' : Unit) : Prop :=
-    match x, y, x', y' with
-    MkUnit, MkUnit, MkUnit, MkUnit => False
-    end.
-
-Notation "p ^u" := (unitInverse p).
-
-Lemma unitInverseInverse : forall (p : Unit), (p ^u)^u = p.
-Proof.
-intros.
-destruct p.
-unfold unitInverse.
-auto.
-Qed.
-
-Lemma UnitCommuteUnique : forall p q p' q' p'' q'' : Unit,
-  unitCommute p q q' p' -> unitCommute p q q'' p'' -> p' = p'' /\ q' = q''.
-Proof.
-intros.
-destruct p.
-destruct q.
-destruct p'.
-destruct q'.
-destruct p''.
-destruct q''.
-auto.
-Qed.
-
-
-Lemma UnitCommutable_dec : forall p q : Unit,
-  {q' : Unit & {p' : Unit & unitCommute p q q' p'}} +
-  {~ (exists q' p' : Unit, unitCommute p q q' p')}.
-Proof.
-destruct p.
-destruct q.
-simpl.
-intuition.
-right.
-intros.
-destruct H.
-destruct H.
-destruct x.
-destruct x0.
-elim H.
-Qed.
-
-Lemma UnitCommuteSelfInverse : forall p q p' q' : Unit, unitCommute p q q' p' <-> unitCommute q' p' p q.
-Proof.
-intros.
-destruct p.
-destruct q.
-destruct p'.
-destruct q'.
-simpl.
-tauto.
-Qed.
-
-
-Lemma UnitCommuteSquare : forall p q p' q' : Unit, unitCommute p q q' p' -> unitCommute (q' ^u) p p' (q ^u).
-Proof.
-intros.
-destruct p.
-destruct q.
-destruct p'.
-destruct q'.
-unfold unitInverse.
-destruct H.
-Qed.
-
-
-Lemma UnitCommuteConsistent1 : forall p1 q1 r1 q2 r2 q3 r3 p3 p5 : Unit,
-  unitCommute q1 r1 r2 q2 ->
-  unitCommute p1 q1 q3 p5 ->
-  unitCommute p5 r1 r3 p3 ->
-  exists r4 q4 p6 : Unit,
-    unitCommute q3 r3 r4 q4 /\
-    unitCommute p1 r2 r4 p6 /\ unitCommute p6 q2 q4 p3.
-Proof.
-intros.
-destruct p1.
-destruct q1.
-destruct r1.
-destruct q2.
-destruct r2.
-destruct q3.
-destruct r3.
-destruct p3.
-destruct p5.
-elim H.
-Qed.
-
-
-Lemma UnitCommuteConsistent2 : forall p3 q3 r3 q4 r4 q1 r1 p1 p5 : Unit,
-  unitCommute q3 r3 r4 q4 ->
-  unitCommute r3 p3 p5 r1 ->
-  unitCommute q3 p5 p1 q1 ->
-  exists r2 q2 p6 : Unit,
-    unitCommute q1 r1 r2 q2 /\
-    unitCommute q4 p3 p6 q2 /\ unitCommute r4 p6 p1 r2.
-Proof.
-intros.
-destruct p3.
-destruct q3.
-destruct r3.
-destruct q4.
-destruct r4.
-destruct q1.
-destruct r1.
-destruct p1.
-destruct p5.
-elim H.
-Qed.
-
-Definition UnitUnnamedPatch : UnnamedPatch :=
-    mkUnnamedPatch
-        Unit
-        unitInverse
-        unitInverseInverse
-        unitCommute
-        UnitCommuteUnique
-        UnitCommutable_dec
-        UnitCommuteSelfInverse
-        UnitCommuteSquare
-        UnitCommuteConsistent1
-        UnitCommuteConsistent2.
hunk ./src/unit_nocommute.v 1
-Require Import unnamed_patches.
rmfile ./src/unit_nocommute.v
}