From a75a26ca7f6c66b0d85f79315b9f8d7550cd5066 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Tue, 19 Apr 2016 12:07:44 -0400 Subject: Add a tactic for field inequalities Pair programming with Andres, a better proof of unifiedAddM1'_rep, some progress on twistedAddAssoc. --- src/Util/Tactics.v | 25 +++++++++++++++++++++++++ 1 file changed, 25 insertions(+) create mode 100644 src/Util/Tactics.v (limited to 'src/Util/Tactics.v') 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. -- cgit v1.2.3