blob: 2324e1b348ab12977814625e1a433d7b55a08279 (
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
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
|
(** * Generic Tactics *)
(** Test if a tactic succeeds, but always roll-back the results *)
Tactic Notation "test" tactic3(tac) :=
try (first [ tac | fail 2 tac "does not succeed" ]; fail 0 tac "succeeds"; [](* test for [t] solved all goals *)).
(** [not tac] is equivalent to [fail tac "succeeds"] if [tac] succeeds, and is equivalent to [idtac] if [tac] fails *)
Tactic Notation "not" tactic3(tac) := try ((test tac); fail 1 tac "succeeds").
(** find the head of the given expression *)
Ltac head expr :=
match expr with
| ?f _ => head f
| _ => expr
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.
(** destruct discriminees of [match]es in the goal *)
(* Prioritize breaking apart things in the context, then things which
don't need equations, then simple matches (which can be displayed
as [if]s), and finally matches in general. *)
Ltac break_match_step only_when :=
match goal with
| [ |- appcontext[match ?e with _ => _ end] ]
=> only_when e; is_var e; destruct e
| [ |- appcontext[match ?e with _ => _ end] ]
=> only_when e;
match type of e with
| sumbool _ _ => destruct e
end
| [ |- appcontext[if ?e then _ else _] ]
=> only_when e; destruct e eqn:?
| [ |- appcontext[match ?e with _ => _ end] ]
=> only_when e; destruct e eqn:?
end.
Ltac break_match := repeat break_match_step ltac:(fun _ => idtac).
Ltac break_match_when_head_step T :=
break_match_step
ltac:(fun e => let T' := type of e in
let T' := head T' in
constr_eq T T').
Ltac break_match_when_head T := repeat break_match_when_head_step T.
Ltac free_in x y :=
idtac;
match y with
| appcontext[x] => fail 1 x "appears in" y
| _ => idtac
end.
Ltac setoid_subst'' R x :=
is_var x;
match goal with
| [ H : R x ?y |- _ ]
=> free_in x y; rewrite ?H in *; clear x H
| [ H : R ?y x |- _ ]
=> free_in x y; rewrite <- ?H in *; clear x H
end.
Ltac setoid_subst' x :=
is_var x;
match goal with
| [ H : ?R x _ |- _ ] => setoid_subst'' R x
| [ H : ?R _ x |- _ ] => setoid_subst'' R x
end.
Ltac setoid_subst_rel' R :=
idtac;
match goal with
| [ H : R ?x _ |- _ ] => setoid_subst'' R x
| [ H : R _ ?x |- _ ] => setoid_subst'' R x
end.
Ltac setoid_subst_rel R := repeat setoid_subst_rel' R.
Ltac setoid_subst_all :=
repeat match goal with
| [ H : ?R ?x ?y |- _ ] => is_var x; setoid_subst'' R x
| [ H : ?R ?x ?y |- _ ] => is_var y; setoid_subst'' R y
end.
Tactic Notation "setoid_subst" ident(x) := setoid_subst' x.
Tactic Notation "setoid_subst" := setoid_subst_all.
Ltac destruct_trivial_step :=
match goal with
| [ H : unit |- _ ] => clear H || destruct H
| [ H : True |- _ ] => clear H || destruct H
end.
Ltac destruct_trivial := repeat destruct_trivial_step.
Ltac clear_duplicates_step :=
match goal with
| [ H : ?T, H' : ?T |- _ ] => clear H'
| [ H := ?T, H' := ?T |- _ ] => clear H'
end.
Ltac clear_duplicates := repeat clear_duplicates_step.
|
