diff options
Diffstat (limited to 'src/Util/Tactics.v')
-rw-r--r-- | src/Util/Tactics.v | 25 |
1 files changed, 25 insertions, 0 deletions
diff --git a/src/Util/Tactics.v b/src/Util/Tactics.v new file mode 100644 index 000000000..08ebfe13e --- /dev/null +++ b/src/Util/Tactics.v @@ -0,0 +1,25 @@ +(** * Generic Tactics *) + +(* [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. +(* [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. |