diff options
author | Jason Gross <jgross@mit.edu> | 2017-04-03 12:09:12 -0400 |
---|---|---|
committer | Jason Gross <jgross@mit.edu> | 2017-04-03 12:09:12 -0400 |
commit | 619fb284271a5df392fb24003dc82d06d0df0c2b (patch) | |
tree | b1f36a87cb3068721d470b34f07a4f092f1e85c3 | |
parent | 9fc2db495004409347ef6098530535596abcb48f (diff) |
Add UnifyAbstractReflexivity tactics
-rw-r--r-- | _CoqProject | 1 | ||||
-rw-r--r-- | src/Util/Tactics.v | 1 | ||||
-rw-r--r-- | src/Util/Tactics/UnifyAbstractReflexivity.v | 58 |
3 files changed, 60 insertions, 0 deletions
diff --git a/_CoqProject b/_CoqProject index f0e376f1c..edc8fd185 100644 --- a/_CoqProject +++ b/_CoqProject @@ -328,6 +328,7 @@ src/Util/Tactics/RewriteHyp.v src/Util/Tactics/SpecializeBy.v src/Util/Tactics/SplitInContext.v src/Util/Tactics/SubstLet.v +src/Util/Tactics/UnifyAbstractReflexivity.v src/Util/Tactics/UniquePose.v src/Util/Tactics/VM.v src/WeierstrassCurve/Pre.v diff --git a/src/Util/Tactics.v b/src/Util/Tactics.v index 274e8a0bc..d6ab637aa 100644 --- a/src/Util/Tactics.v +++ b/src/Util/Tactics.v @@ -11,6 +11,7 @@ Require Export Crypto.Util.Tactics.RewriteHyp. Require Export Crypto.Util.Tactics.SpecializeBy. Require Export Crypto.Util.Tactics.SplitInContext. Require Export Crypto.Util.Tactics.SubstLet. +Require Export Crypto.Util.Tactics.UnifyAbstractReflexivity. Require Export Crypto.Util.Tactics.UniquePose. Require Export Crypto.Util.Tactics.VM. 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. |