blob: 3abd5819520c90d1cf95c8c0aa6daa088abdbb6c (
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
|
Require Export Crypto.Util.FixCoqMistakes.
Ltac transparent_specialize_one H arg :=
first [ let test := eval unfold H in H in idtac;
let H' := fresh in rename H into H'; pose (H' arg) as H; subst H'
| specialize (H arg) ].
(** try to specialize all non-dependent hypotheses using [tac], maintaining transparency *)
Ltac guarded_specialize_by' tac guard_tac :=
idtac;
match goal with
| [ H : ?A -> ?B |- _ ]
=> guard_tac H;
let H' := fresh in
assert (H' : A) by tac;
transparent_specialize_one H H';
try clear H' (* if [H] was transparent, [H'] will remain *)
end.
Ltac specialize_by' tac := guarded_specialize_by' tac ltac:(fun _ => idtac).
Ltac specialize_by tac := repeat specialize_by' tac.
(** [specialize_by auto] should not mean [specialize_by ( auto
with * )]!!!!!!! (see
https://coq.inria.fr/bugs/show_bug.cgi?id=4966) We fix this design
flaw. *)
Tactic Notation "specialize_by" tactic3(tac) := specialize_by tac.
(** A marginally faster version of [specialize_by assumption] *)
Ltac specialize_by_assumption :=
repeat match goal with
| [ H : ?T, H' : (?T -> ?U)%type |- _ ]
=> lazymatch goal with
| [ _ : context[H'] |- _ ] => fail
| [ |- context[H'] ] => fail
| _ => specialize (H' H)
end
end.
|
