blob: fea7dfe1686371d6cd377a60b69577530eaee66e (
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
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
|
(** * 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_hyps_step only_when :=
match goal with
| [ H : appcontext[match ?e with _ => _ end] |- _ ]
=> only_when e; is_var e; destruct e
| [ H : appcontext[match ?e with _ => _ end] |- _ ]
=> only_when e;
match type of e with
| sumbool _ _ => destruct e
end
| [ H : appcontext[if ?e then _ else _] |- _ ]
=> only_when e; destruct e eqn:?
| [ H : 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_hyps := repeat break_match_hyps_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_hyps_when_head_step T :=
break_match_hyps_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 break_match_hyps_when_head T := repeat break_match_hyps_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.
|
