blob: 32959d716f34963fd734d9ea79e840f8ea4e63e9 (
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
|
(** * Tactics for moving around [let ... in ...] and [dlet ... in ...] *)
Require Import Crypto.Util.LetIn.
(** The tactic [sig_dlet_in_rhs_to_context] moves to the context any
[dlet x := y in ...] on the rhs of a goal of the form [{ a | lhs =
rhs }]. *)
Ltac sig_dlet_in_rhs_to_context_step v :=
lazymatch goal with
| [ |- { a | _ = @Let_In ?A ?B ?x _ } ]
=> pose x as v;
change (@Let_In A B x) with (fun P : forall a : A, B a => P v);
cbv beta
end.
Ltac sig_dlet_in_rhs_to_context :=
repeat let v := fresh "x" in sig_dlet_in_rhs_to_context_step v.
(** The tactic [sig_dlet_in_lhs_to_context] moves to the context any
[dlet x := y in ...] on the lhs of a goal of the form [{ a | lhs =
rhs }]. *)
Ltac sig_dlet_in_lhs_to_context_step v :=
lazymatch goal with
| [ |- { a | @Let_In ?A ?B ?x _ = _ } ]
=> pose x as v;
change (@Let_In A B x) with (fun P : forall a : A, B a => P v);
cbv beta
end.
Ltac sig_dlet_in_lhs_to_context :=
repeat let v := fresh "x" in sig_dlet_in_lhs_to_context_step v.
(** The tactic [goal_dlet_to_context] moves to the context any
[dlet x := y in ...] in the goal. *)
Ltac goal_dlet_to_context_step v :=
match goal with
| [ |- context[@Let_In ?A ?B ?x] ]
=> pose x as v;
change (@Let_In A B x) with (fun P : forall a : A, B a => P v);
cbv beta
end.
Ltac goal_dlet_to_context :=
repeat let v := fresh "x" in goal_dlet_to_context_step v.
(** Takes in a uconstr [uc], uses [set] to find it in the goal and
passes the constr that it finds to [k] *)
Local Ltac with_uconstr_in_goal uc k :=
let f := fresh in
set (f := uc);
let f' := (eval cbv delta [f] in f) in
subst f; k f'.
(** This tactic creates a [dlet x := f in rhs] in the rhs of a goal
of the form [lhs = rhs]. *)
Ltac context_to_dlet_in_rhs f :=
lazymatch goal with
| [ |- ?R ?LHS ?RHS ]
=> with_uconstr_in_goal
f
ltac:(fun f
=> let RHS' := lazymatch (eval pattern f in RHS) with
| ?RHS _ => RHS
end in
let x := fresh "x" in
transitivity (dlet x := f in RHS' x);
[ | clear; abstract (cbv [Let_In]; reflexivity) ]
)
end.
Tactic Notation "context_to_dlet_in_rhs" uconstr(f) := context_to_dlet_in_rhs f.
|
