-
Notifications
You must be signed in to change notification settings - Fork 0
/
LocalTactics.v
55 lines (46 loc) · 1.76 KB
/
LocalTactics.v
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
Require Import stdpp.tactics.
Require Import stdpp.fin_sets.
Ltac primforced term taclist :=
let n := numgoals in
destruct term eqn:?; try solve [intros; exfalso; subst; (solve taclist || discriminate || contradiction || congruence)];
let m := numgoals in
tryif (guard m <= n) then idtac else fail 0 term "not forced".
Tactic Notation "forced" constr(term) :=
primforced term idtac.
Tactic Notation "forced" constr(term) "by" tactic_list(t) :=
primforced term t.
Global Tactic Notation "define" "(" ident(H) ":" open_constr(type) ")" :=
unshelve refine (let H := (_ : type) in _).
(* Based somewhat on https://github.com/tchajed/coq-tricks/blob/master/src/Deex.v
with extra support for constructive exists *)
Ltac deex :=
repeat match goal with
| [ H: exists (name:_), _ |- _ ] =>
let name' := fresh name in
destruct H as [name' H]
| [ H: { name:_ & _ } |- _ ] =>
let name' := fresh name in
destruct H as [name' H]
| [ H: { name:_ | _ } |- _ ] =>
let name' := fresh name in
destruct H as [name' H]
end.
(* Add products *)
Ltac deprod :=
repeat match goal with
| [ H: exists (name:_), _ |- _ ] =>
let name' := fresh name in
destruct H as [name' H]
| [ H: { name:_ & _ } |- _ ] =>
let name' := fresh name in
destruct H as [name' H]
| [ H: { name:_ | _ } |- _ ] =>
let name' := fresh name in
destruct H as [name' H]
| [ H: _ /\ _ |- _ ] =>
destruct H
| [ H: (_ * _)%type |- _] =>
destruct H
end.
Ltac deep_set_unfold :=
repeat progress (intro || deprod || simplify_eq || set_unfold).