blob: da6c6974e7dbf818616ffbb6a1c60827fccb2f15 (
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
26
27
28
29
30
31
32
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.
|
