Split off unique {pose,assert}

1 files changed, 33 insertions, 0 deletions

diff --git a/src/Util/Tactics/UniquePose.v b/src/Util/Tactics/UniquePose.v
new file mode 100644
index 000000000..da6c6974e
--- /dev/null
+++ b/src/Util/Tactics/UniquePose.v
@@ -0,0 +1,33 @@
+Require Export Crypto.Util.FixCoqMistakes.
+
+(** [pose proof defn], but only if no hypothesis of the same type exists.
+    most useful for proofs of a proposition *)
+Tactic Notation "unique" "pose" "proof" constr(defn) :=
+  let T := type of defn in
+  match goal with
+  | [ H : T |- _ ] => fail 1
+  | _ => pose proof defn
+  end.
+
+(** [pose defn], but only if that hypothesis doesn't exist *)
+Tactic Notation "unique" "pose" constr(defn) :=
+  lazymatch goal with
+  | [ H := defn |- _ ] => fail
+  | _ => pose defn
+  end.
+
+(** [assert T], but only if no hypothesis of the same type exists.
+    most useful for proofs of a proposition *)
+Tactic Notation "unique" "assert" constr(T) :=
+  match goal with
+  | [ H : T |- _ ] => fail 1
+  | _ => assert T
+  end.
+
+(** [assert T], but only if no hypothesis of the same type exists.
+    most useful for proofs of a proposition *)
+Tactic Notation "unique" "assert" constr(T) "by" tactic3(tac) :=
+  match goal with
+  | [ H : T |- _ ] => fail 1
+  | _ => assert T by tac
+  end.