diff options
author | Jason Gross <jgross@mit.edu> | 2017-01-31 19:51:17 -0500 |
---|---|---|
committer | Jason Gross <jgross@mit.edu> | 2017-01-31 19:51:17 -0500 |
commit | 72efe58cb53c46b9ca8e7b133e9786f0ca8d0c43 (patch) | |
tree | 46f903586114bc1b2e8952c40c0b58e503fcfe7f /src/Util/Tactics/UniquePose.v | |
parent | 8783d23b300ed9635ad7ad047a4c2f3edff6e70f (diff) |
Split off unique {pose,assert}
Diffstat (limited to 'src/Util/Tactics/UniquePose.v')
-rw-r--r-- | src/Util/Tactics/UniquePose.v | 33 |
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. |