Skip to content

Commit cd8e839

Browse files
JasonGrossJasonGross
committed
Add some utility tactics
I used these for proving some decidability properties and for defining Gallina quotation functions.
1 parent 112cace commit cd8e839

File tree

14 files changed

+523
-0
lines changed

14 files changed

+523
-0
lines changed

‎utils/_CoqProject‎

Lines changed: 13 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -30,3 +30,16 @@ theories/ReflectEq.v
3030
theories/monad_utils.v
3131
theories/utils.v
3232

33+
# extra tactics
34+
theories/MCTactics/DestructHead.v
35+
theories/MCTactics/DestructHyps.v
36+
theories/MCTactics/FindHyp.v
37+
theories/MCTactics/GeneralizeOverHoles.v
38+
theories/MCTactics/Head.v
39+
theories/MCTactics/InHypUnderBindersDo.v
40+
theories/MCTactics/SpecializeAllWays.v
41+
theories/MCTactics/SpecializeBy.v
42+
theories/MCTactics/SpecializeUnderBindersBy.v
43+
theories/MCTactics/SplitInContext.v
44+
theories/MCTactics/UniquePose.v
45+
theories/MCTactics/Zeta1.v

‎utils/theories/MCTactics/DestructHead.v‎

Lines changed: 88 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,88 @@
1+
Require Import MetaCoq.Utils.MCTactics.Head.
2+
Require Import MetaCoq.Utils.MCTactics.DestructHyps.
3+
4+
Ltac destruct_head_matcher T HT :=
5+
match head HT with
6+
| T => idtac
7+
end.
8+
Ltac destruct_head T := destruct_all_matches ltac:(destruct_head_matcher T).
9+
Ltac destruct_one_head T := destruct_one_match ltac:(destruct_head_matcher T).
10+
Ltac destruct_head' T := destruct_all_matches' ltac:(destruct_head_matcher T).
11+
12+
Ltac inversion_head T := inversion_all_matches ltac:(destruct_head_matcher T).
13+
Ltac inversion_one_head T := inversion_one_match ltac:(destruct_head_matcher T).
14+
Ltac inversion_head' T := inversion_all_matches' ltac:(destruct_head_matcher T).
15+
16+
17+
Ltac head_hnf_matcher T HT :=
18+
match head_hnf HT with
19+
| T => idtac
20+
end.
21+
Ltac destruct_head_hnf T := destruct_all_matches ltac:(head_hnf_matcher T).
22+
Ltac destruct_one_head_hnf T := destruct_one_match ltac:(head_hnf_matcher T).
23+
Ltac destruct_head_hnf' T := destruct_all_matches' ltac:(head_hnf_matcher T).
24+
25+
Ltac inversion_head_hnf T := inversion_all_matches ltac:(head_hnf_matcher T).
26+
Ltac inversion_one_head_hnf T := inversion_one_match ltac:(head_hnf_matcher T).
27+
Ltac inversion_head_hnf' T := inversion_all_matches' ltac:(head_hnf_matcher T).
28+
29+
(** Faster versions for some common connectives *)
30+
Ltac destruct_one_head'_ex := match goal with H : ex _ |- _ => destruct H end.
31+
Ltac destruct_one_head_ex := destruct_one_head'_ex; simpl in *.
32+
Ltac destruct_head'_ex := repeat destruct_one_head'_ex.
33+
Ltac destruct_head_ex := repeat destruct_one_head_ex.
34+
35+
Ltac destruct_one_head'_sig := match goal with H : sig _ |- _ => destruct H end.
36+
Ltac destruct_one_head_sig := destruct_one_head'_sig; simpl in *.
37+
Ltac destruct_head'_sig := repeat destruct_one_head'_sig.
38+
Ltac destruct_head_sig := repeat destruct_one_head_sig.
39+
40+
Ltac destruct_one_head'_sigT := match goal with H : sigT _ |- _ => destruct H end.
41+
Ltac destruct_one_head_sigT := destruct_one_head'_sigT; simpl in *.
42+
Ltac destruct_head'_sigT := repeat destruct_one_head'_sigT.
43+
Ltac destruct_head_sigT := repeat destruct_one_head_sigT.
44+
45+
Ltac destruct_one_head'_prod := match goal with H : prod _ _ |- _ => destruct H end.
46+
Ltac destruct_one_head_prod := destruct_one_head'_prod; simpl in *.
47+
Ltac destruct_head'_prod := repeat destruct_one_head'_prod.
48+
Ltac destruct_head_prod := repeat destruct_one_head_prod.
49+
50+
Ltac destruct_one_head'_and := match goal with H : and _ _ |- _ => destruct H end.
51+
Ltac destruct_one_head_and := destruct_one_head'_and; simpl in *.
52+
Ltac destruct_head'_and := repeat destruct_one_head'_and.
53+
Ltac destruct_head_and := repeat destruct_one_head_and.
54+
55+
Ltac destruct_one_head'_or := match goal with H : or _ _ |- _ => destruct H end.
56+
Ltac destruct_one_head_or := destruct_one_head'_or; simpl in *.
57+
Ltac destruct_head'_or := repeat destruct_one_head'_or.
58+
Ltac destruct_head_or := repeat destruct_one_head_or.
59+
60+
Ltac destruct_one_head'_sum := match goal with H : sum _ _ |- _ => destruct H end.
61+
Ltac destruct_one_head_sum := destruct_one_head'_sum; simpl in *.
62+
Ltac destruct_head'_sum := repeat destruct_one_head'_sum.
63+
Ltac destruct_head_sum := repeat destruct_one_head_sum.
64+
65+
Ltac destruct_one_head'_unit := match goal with H : unit |- _ => clear H || destruct H end.
66+
Ltac destruct_one_head_unit := destruct_one_head'_unit; simpl in *.
67+
Ltac destruct_head'_unit := repeat destruct_one_head'_unit.
68+
Ltac destruct_head_unit := repeat destruct_one_head_unit.
69+
70+
Ltac destruct_one_head'_True := match goal with H : True |- _ => clear H || destruct H end.
71+
Ltac destruct_one_head_True := destruct_one_head'_True; simpl in *.
72+
Ltac destruct_head'_True := repeat destruct_one_head'_True.
73+
Ltac destruct_head_True := repeat destruct_one_head_True.
74+
75+
Ltac destruct_one_head'_bool := match goal with H : bool |- _ => clear H || destruct H end.
76+
Ltac destruct_one_head_bool := destruct_one_head'_bool; simpl in *.
77+
Ltac destruct_head'_bool := repeat destruct_one_head'_bool.
78+
Ltac destruct_head_bool := repeat destruct_one_head_bool.
79+
80+
Ltac destruct_one_head'_False := match goal with H : False |- _ => destruct H end.
81+
Ltac destruct_one_head_False := destruct_one_head'_False; simpl in *.
82+
Ltac destruct_head'_False := repeat destruct_one_head'_False.
83+
Ltac destruct_head_False := repeat destruct_one_head_False.
84+
85+
Ltac destruct_one_head'_Empty_set := match goal with H : Empty_set |- _ => destruct H end.
86+
Ltac destruct_one_head_Empty_set := destruct_one_head'_Empty_set; simpl in *.
87+
Ltac destruct_head'_Empty_set := repeat destruct_one_head'_Empty_set.
88+
Ltac destruct_head_Empty_set := repeat destruct_one_head_Empty_set.

‎utils/theories/MCTactics/DestructHyps.v‎

Lines changed: 46 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,46 @@
1+
(** given a [matcher] that succeeds on some hypotheses and fails on
2+
others, destruct any matching hypotheses, and then execute [tac]
3+
after each [destruct].
4+
5+
The [tac] part exists so that you can, e.g., [simpl in *], to
6+
speed things up. *)
7+
Ltac do_one_match_then matcher do_tac tac :=
8+
idtac;
9+
match goal with
10+
| [ H : ?T |- _ ]
11+
=> matcher T; do_tac H;
12+
try match type of H with
13+
| T => clear H
14+
end;
15+
tac
16+
end.
17+
18+
Ltac do_all_matches_then matcher do_tac tac :=
19+
repeat do_one_match_then matcher do_tac tac.
20+
21+
Ltac destruct_all_matches_then matcher tac :=
22+
do_all_matches_then matcher ltac:(fun H => destruct H) tac.
23+
Ltac destruct_one_match_then matcher tac :=
24+
do_one_match_then matcher ltac:(fun H => destruct H) tac.
25+
26+
Ltac inversion_all_matches_then matcher tac :=
27+
do_all_matches_then matcher ltac:(fun H => inversion H; subst) tac.
28+
Ltac inversion_one_match_then matcher tac :=
29+
do_one_match_then matcher ltac:(fun H => inversion H; subst) tac.
30+
31+
Ltac destruct_all_matches matcher :=
32+
destruct_all_matches_then matcher ltac:( simpl in * ).
33+
Ltac destruct_one_match matcher := destruct_one_match_then matcher ltac:( simpl in * ).
34+
Ltac destruct_all_matches' matcher := destruct_all_matches_then matcher idtac.
35+
36+
Ltac inversion_all_matches matcher := inversion_all_matches_then matcher ltac:( simpl in * ).
37+
Ltac inversion_one_match matcher := inversion_one_match_then matcher ltac:( simpl in * ).
38+
Ltac inversion_all_matches' matcher := inversion_all_matches_then matcher idtac.
39+
40+
(* matches anything whose type has a [T] in it *)
41+
Ltac destruct_type_matcher T HT :=
42+
match HT with
43+
| context[T] => idtac
44+
end.
45+
Ltac destruct_type T := destruct_all_matches ltac:(destruct_type_matcher T).
46+
Ltac destruct_type' T := destruct_all_matches' ltac:(destruct_type_matcher T).

‎utils/theories/MCTactics/FindHyp.v‎

Lines changed: 31 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,31 @@
1+
Ltac find_hyp_eq a b := match goal with _ => constr_eq_nounivs a b end.
2+
(* Work around https://github.com/coq/coq/issues/15554 *)
3+
Ltac find_hyp T :=
4+
lazymatch T with
5+
| T
6+
=> (* we're not in https://github.com/coq/coq/issues/15554 *)
7+
multimatch goal with
8+
| [ H : T |- _ ] => H
9+
end
10+
| _
11+
=> (* https://github.com/coq/coq/issues/15554 *)
12+
multimatch goal with
13+
| [ H : ?T' |- _ ] => let __ := find_hyp_eq T T' in
14+
H
15+
end
16+
end.
17+
18+
Ltac find_hyp_with_body body :=
19+
lazymatch body with
20+
| body
21+
=> (* we're not in https://github.com/coq/coq/issues/15554 *)
22+
multimatch goal with
23+
| [ H := body |- _ ] => H
24+
end
25+
| _
26+
=> (* https://github.com/coq/coq/issues/15554 *)
27+
multimatch goal with
28+
| [ H := ?body' |- _ ] => let __ := find_hyp_eq body body' in
29+
H
30+
end
31+
end.

‎utils/theories/MCTactics/GeneralizeOverHoles.v‎

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,7 @@
1+
Require Import MetaCoq.Utils.MCTactics.Zeta1.
2+
Require Import Coq.ssr.ssreflect.
3+
4+
Ltac generalize_over_holes tac :=
5+
zeta1 (ltac:(let H := fresh in
6+
(pose H := ltac:(let v := tac () in refine v));
7+
exact H)).

‎utils/theories/MCTactics/Head.v‎

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
(** find the head of the given expression *)
2+
Ltac head expr :=
3+
match expr with
4+
| ?f _ => head f
5+
| _ => expr
6+
end.
7+
8+
Ltac head_hnf expr := let expr' := eval hnf in expr in head expr'.

‎utils/theories/MCTactics/InHypUnderBindersDo.v‎

Lines changed: 104 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,104 @@
1+
Require Import MetaCoq.Utils.MCTactics.SpecializeBy.
2+
Require Import MetaCoq.Utils.MCTactics.GeneralizeOverHoles.
3+
Require Import MetaCoq.Utils.MCTactics.UniquePose.
4+
5+
Ltac guarded_in_hyp_term_under_binders_do' guard_tac H tac :=
6+
let is_transparent := match goal with
7+
| _ => let __ := (eval cbv delta [H] in H) in
8+
constr:(true)
9+
| _ => constr:(false)
10+
end in
11+
let __ := lazymatch goal with _ => guard_tac H end in
12+
match goal with
13+
| _ => let __ := lazymatch goal with _ => progress tac H end in
14+
H
15+
| _ => let __ := lazymatch is_transparent with
16+
| true => let H' := fresh in
17+
rename H into H';
18+
let v := open_constr:(_) in
19+
pose (H' v) as H;
20+
subst H'
21+
| false
22+
=> (* kludge for old Coq *)
23+
(*let v := open_constr:(_) in*)
24+
let t := open_constr:(_) in
25+
let v := fresh in
26+
evar (v : t);
27+
specialize (H v);
28+
subst v
29+
end in
30+
guarded_in_hyp_term_under_binders_do' guard_tac H tac
31+
end.
32+
33+
Ltac guarded_in_hyp_term_under_binders_do guard_tac H tac :=
34+
generalize_over_holes ltac:(fun _ => guarded_in_hyp_term_under_binders_do' guard_tac H tac).
35+
36+
Ltac guarded_in_hyp_gen_hyp_under_binders_do all_ways guard_tac H tac :=
37+
idtac;
38+
let is_transparent := match goal with
39+
| _ => let __ := (eval cbv delta [H] in H) in
40+
constr:(true)
41+
| _ => constr:(false)
42+
end in
43+
lazymatch constr:((all_ways, is_transparent)) with
44+
| (false, true)
45+
=> let H' := fresh in
46+
rename H into H';
47+
let H'' := guarded_in_hyp_term_under_binders_do guard_tac H' tac in
48+
pose H'' as H;
49+
subst H'
50+
| (true, true)
51+
=> let H := guarded_in_hyp_term_under_binders_do guard_tac H tac in
52+
unique pose H
53+
| (false, false)
54+
=> let H' := fresh in
55+
rename H into H';
56+
let H'' := guarded_in_hyp_term_under_binders_do guard_tac H' tac in
57+
pose proof H'' as H;
58+
clear H'
59+
| (true, false)
60+
=> let H := guarded_in_hyp_term_under_binders_do guard_tac H tac in
61+
unique pose proof H
62+
end.
63+
64+
Ltac guarded_in_hyp_hyp_under_binders_do guard_tac H tac :=
65+
guarded_in_hyp_gen_hyp_under_binders_do false guard_tac H tac.
66+
Ltac guarded_in_hyp_hyp_all_ways_under_binders_do guard_tac H tac :=
67+
guarded_in_hyp_gen_hyp_under_binders_do true guard_tac H tac.
68+
69+
Ltac guard_noop H := idtac.
70+
71+
Ltac guarded_in_hyp_gen_under_binders_do' all_ways tac guard_tac :=
72+
idtac;
73+
match goal with
74+
| [ H : _ |- _ ]
75+
=> guard_tac H;
76+
guarded_in_hyp_gen_hyp_under_binders_do all_ways guard_noop H tac
77+
end.
78+
79+
Ltac guarded_in_hyp_under_binders_do' tac guard_tac :=
80+
guarded_in_hyp_gen_under_binders_do' false tac guard_tac.
81+
82+
Ltac in_hyp_gen_under_binders_do' all_ways tac := guarded_in_hyp_gen_under_binders_do' all_ways tac ltac:(fun _ => idtac).
83+
84+
Ltac in_hyp_under_binders_do' tac := in_hyp_gen_under_binders_do' false tac.
85+
86+
Ltac guarded_in_hyp_gen_under_binders_do all_ways tac guard_tac := repeat guarded_in_hyp_gen_under_binders_do' all_ways tac guard_tac.
87+
88+
Ltac guarded_in_hyp_under_binders_do tac guard_tac := guarded_in_hyp_gen_under_binders_do false tac guard_tac.
89+
90+
Ltac guarded_in_hyp_all_ways_under_binders_do tac guard_tac := guarded_in_hyp_gen_under_binders_do true tac guard_tac.
91+
92+
Ltac in_hyp_gen_under_binders_do all_ways tac := repeat in_hyp_gen_under_binders_do' all_ways tac.
93+
94+
Ltac in_hyp_under_binders_do tac := in_hyp_gen_under_binders_do false tac.
95+
96+
Ltac in_hyp_all_ways_under_binders_do tac := in_hyp_gen_under_binders_do true tac.
97+
98+
(** [in_hyp_under_binders_do auto] should not mean [in_hyp_under_binders_do ( auto
99+
with * )]!!!!!!! (see
100+
https://coq.inria.fr/bugs/show_bug.cgi?id=4966) We fix this design
101+
flaw. *)
102+
Tactic Notation "in_hyp_under_binders_do" tactic3(tac) := in_hyp_under_binders_do tac.
103+
104+
Tactic Notation "in_hyp_all_ways_under_binders_do" tactic3(tac) := in_hyp_all_ways_under_binders_do tac.

‎utils/theories/MCTactics/SpecializeAllWays.v‎

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,7 @@
1+
Require Export MetaCoq.Utils.MCTactics.UniquePose.
2+
3+
Ltac specialize_all_ways :=
4+
repeat match goal with
5+
| [ H : ?A, H' : forall a : ?A, _ |- _ ]
6+
=> unique pose proof (H' H)
7+
end.

‎utils/theories/MCTactics/SpecializeBy.v‎

Lines changed: 36 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,36 @@
1+
Ltac transparent_specialize_one H arg :=
2+
first [ let test := eval unfold H in H in idtac;
3+
let H' := fresh in rename H into H'; pose (H' arg) as H; subst H'
4+
| specialize (H arg) ].
5+
6+
(** try to specialize all non-dependent hypotheses using [tac], maintaining transparency *)
7+
Ltac guarded_specialize_by' tac guard_tac :=
8+
idtac;
9+
match goal with
10+
| [ H : ?A -> ?B |- _ ]
11+
=> guard_tac H;
12+
let H' := fresh in
13+
assert (H' : A) by tac;
14+
transparent_specialize_one H H';
15+
try clear H' (* if [H] was transparent, [H'] will remain *)
16+
end.
17+
Ltac specialize_by' tac := guarded_specialize_by' tac ltac:(fun _ => idtac).
18+
19+
Ltac specialize_by tac := repeat specialize_by' tac.
20+
21+
(** [specialize_by auto] should not mean [specialize_by ( auto
22+
with * )]!!!!!!! (see
23+
https://coq.inria.fr/bugs/show_bug.cgi?id=4966) We fix this design
24+
flaw. *)
25+
Tactic Notation "specialize_by" tactic3(tac) := specialize_by tac.
26+
27+
(** A marginally faster version of [specialize_by assumption] *)
28+
Ltac specialize_by_assumption :=
29+
repeat match goal with
30+
| [ H : ?T, H' : (?T -> ?U)%type |- _ ]
31+
=> lazymatch goal with
32+
| [ _ : context[H'] |- _ ] => fail
33+
| [ |- context[H'] ] => fail
34+
| _ => specialize (H' H)
35+
end
36+
end.

0 commit comments

Comments
 (0)