blob: 95a060750b497cd85665e8f8ef06fc15a505c1a1 (
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
|
Require Export Crypto.Util.FixCoqMistakes.
Require Import Crypto.Util.Tactics.Head.
(** 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 set_match_refl v' only_when :=
lazymatch goal with
| [ |- context G[match ?e with _ => _ end eq_refl] ]
=> only_when e;
let T := fresh in
evar (T : Type); evar (v' : T);
subst T;
let vv := (eval cbv delta [v'] in v') in
let G' := context G[vv] in
let G''' := context G[v'] in
lazymatch goal with |- ?G'' => unify G' G'' end;
change G'''
end.
Ltac set_match_refl_hyp v' only_when :=
lazymatch goal with
| [ H : context G[match ?e with _ => _ end eq_refl] |- _ ]
=> only_when e;
let T := fresh in
evar (T : Type); evar (v' : T);
subst T;
let vv := (eval cbv delta [v'] in v') in
let G' := context G[vv] in
let G''' := context G[v'] in
let G'' := type of H in
unify G' G'';
change G''' in H
end.
Ltac destruct_by_existing_equation match_refl_hyp :=
let v := (eval cbv delta [match_refl_hyp] in match_refl_hyp) in
lazymatch v with
| match ?e with _ => _ end (@eq_refl ?T ?e)
=> let H := fresh in
let e' := fresh in
pose e as e';
change e with e' in (value of match_refl_hyp) at 1;
first [ pose (@eq_refl T e : e = e') as H;
change (@eq_refl T e) with H in (value of match_refl_hyp);
clearbody H e'
| pose (@eq_refl T e : e' = e) as H;
change (@eq_refl T e) with H in (value of match_refl_hyp);
clearbody H e' ];
destruct e'; subst match_refl_hyp
end.
Ltac destruct_rewrite_sumbool e :=
let H := fresh in
destruct e as [H|H];
try lazymatch type of H with
| ?LHS = ?RHS
=> lazymatch RHS with
| context[LHS] => fail
| _ => idtac
end;
rewrite ?H; rewrite ?H in *;
repeat match goal with
| [ |- context G[LHS] ]
=> let LHS' := fresh in
pose LHS as LHS';
let G' := context G[LHS'] in
change G';
replace LHS' with RHS by (subst LHS'; symmetry; apply H);
subst LHS'
end
end.
Ltac break_match_step only_when :=
match goal with
| [ |- context[match ?e with _ => _ end] ]
=> only_when e; is_var e; destruct e
| [ |- context[match ?e with _ => _ end] ]
=> only_when e;
match type of e with
| sumbool _ _ => destruct_rewrite_sumbool e
end
| [ |- context[if ?e then _ else _] ]
=> only_when e; destruct e eqn:?
| [ |- context[match ?e with _ => _ end] ]
=> only_when e; destruct e eqn:?
| _ => let v := fresh in set_match_refl v only_when; destruct_by_existing_equation v
end.
Ltac break_match_hyps_step only_when :=
match goal with
| [ H : context[match ?e with _ => _ end] |- _ ]
=> only_when e; is_var e; destruct e
| [ H : context[match ?e with _ => _ end] |- _ ]
=> only_when e;
match type of e with
| sumbool _ _ => destruct_rewrite_sumbool e
end
| [ H : context[if ?e then _ else _] |- _ ]
=> only_when e; destruct e eqn:?
| [ H : context[match ?e with _ => _ end] |- _ ]
=> only_when e; destruct e eqn:?
| _ => let v := fresh in set_match_refl_hyp v only_when; destruct_by_existing_equation v
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 break_innermost_match_step :=
break_match_step ltac:(fun v => lazymatch v with
| context[match _ with _ => _ end] => fail
| _ => idtac
end).
Ltac break_innermost_match_hyps_step :=
break_match_hyps_step ltac:(fun v => lazymatch v with
| context[match _ with _ => _ end] => fail
| _ => idtac
end).
Ltac break_innermost_match := repeat break_innermost_match_step.
Ltac break_innermost_match_hyps := repeat break_innermost_match_hyps_step.
|
