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 | |
parent | 8783d23b300ed9635ad7ad047a4c2f3edff6e70f (diff) |
Split off unique {pose,assert}
Diffstat (limited to 'src/Util')
-rw-r--r-- | src/Util/Tactics.v | 25 | ||||
-rw-r--r-- | src/Util/Tactics/UniquePose.v | 33 |
2 files changed, 34 insertions, 24 deletions
diff --git a/src/Util/Tactics.v b/src/Util/Tactics.v index dffd6e581..f76660830 100644 --- a/src/Util/Tactics.v +++ b/src/Util/Tactics.v @@ -8,6 +8,7 @@ Require Export Crypto.Util.Tactics.DoWithHyp. Require Export Crypto.Util.Tactics.RewriteHyp. Require Export Crypto.Util.Tactics.SpecializeBy. Require Export Crypto.Util.Tactics.SplitInContext. +Require Export Crypto.Util.Tactics.UniquePose. (** Test if a tactic succeeds, but always roll-back the results *) Tactic Notation "test" tactic3(tac) := @@ -26,30 +27,6 @@ Ltac contains search_for in_term := | appcontext[search_for] => idtac end. -(* [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. - Ltac set_evars := repeat match goal with | [ |- appcontext[?E] ] => is_evar E; let e := fresh "e" in set (e := E) 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. |