blob: 28dc942ef3d377fad44cc30aa574e2e8e9f1da34 (
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
|
(** * Various variants on [reflexivity] and [abstract reflexivity] for evars *)
Require Import Crypto.Util.Tactics.ClearAll.
(** This file defines a number of different ways to solve goals of the
form [LHS = RHS] where [LHS] may contain evars and [RHS] must not
contain evars. Most tactics use [abstract] to reduce the load on
[Defined] and to catch looping behavior early. *)
(** This is the generic tactic; from a goal [LHS = RHS], it transforms
the RHS with a passed transformer, unifies the output with LHS
using the passed [unify] tactic, and then uses the passed variant
of [exact_no_check] to [abstract] a subproof of the form [eq_refl
new_rhs]. If there is no evar in the [LHS], don't run
transformation nor unification. *)
Ltac unify_transformed_rhs_abstract_tac transform_rhs unify exact_no_check :=
intros; clear_all;
lazymatch goal with
| [ |- ?LHS = ?RHS ]
=> tryif has_evar LHS
then (let RHS' := transform_rhs RHS in
unify LHS RHS'; clear;
abstract exact_no_check (eq_refl RHS'))
else (abstract exact_no_check (eq_refl RHS))
end.
Ltac idterm x := x.
Ltac noop2 x y := idtac.
Ltac eval_vm_compute_in x := eval vm_compute in x.
Ltac eval_compute_in x := eval vm_compute in x.
Ltac unify_tac x y := unify x y.
(** The tactic [abstract_vm_compute_rhs_reflexivity] unifies [LHS]
with the result of [vm_compute]ing [RHS], and costs two
[vm_compute]s, unless there is no evar in the [LHS], in which case
it costs only one [vm_compute]. *)
Ltac unify_abstract_vm_compute_rhs_reflexivity :=
unify_transformed_rhs_abstract_tac
eval_vm_compute_in
unify_tac
vm_cast_no_check.
(** The tactic [abstract_compute_rhs_reflexivity] unfies [LHS] with
the result of running [compute] in [RHS], and costs a [compute]
and a [vm_compute]. Use this if you don't want to lose binder
names or otherwise can't use [vm_compute]. *)
Ltac unify_abstract_compute_rhs_reflexivity :=
unify_transformed_rhs_abstract_tac
eval_compute_in
unify_tac
vm_cast_no_check.
(** The tactic [abstract_rhs_reflexivity] unifies [LHS] with [RHS]. *)
Ltac unify_abstract_rhs_reflexivity :=
unify_transformed_rhs_abstract_tac
idterm
unify_tac
exact_no_check.
|
