blob: 08ebfe13e0fdb10c51596259e1265c75ccfc8e29 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
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.
|
