diff options
Diffstat (limited to 'src/Util/Tactics')
-rw-r--r-- | src/Util/Tactics/UnifyAbstractReflexivity.v | 58 |
1 files changed, 58 insertions, 0 deletions
diff --git a/src/Util/Tactics/UnifyAbstractReflexivity.v b/src/Util/Tactics/UnifyAbstractReflexivity.v new file mode 100644 index 000000000..bc1616cf0 --- /dev/null +++ b/src/Util/Tactics/UnifyAbstractReflexivity.v @@ -0,0 +1,58 @@ +(** * Various variants on [reflexivity] and [abstract reflexivity] for evars *) +(** 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]. *) +Ltac unify_transformed_rhs_abstract_tac transform_rhs unify exact_no_check := + intros; clear; + lazymatch goal with + | [ |- ?LHS = ?RHS ] + => let RHS' := transform_rhs RHS in + unify LHS RHS'; clear; + 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. *) +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. +(** The tactic [abstract_vm_compute_rhs_no_evar_reflexivity] costs only one + [vm_compute] and proves only evar-free goals. Best when the cost + of retypechecking [RHS] is small, or at least smaller than the + cost of retypechecking [LHS]. *) +Ltac abstract_vm_compute_rhs_no_evar_reflexivity := + unify_transformed_rhs_abstract_tac + idterm + noop2 + vm_cast_no_check. |