diff options
| -rw-r--r-- | plugins/omega/PreOmega.v | 14 | ||||
| -rw-r--r-- | test-suite/success/Nia.v | 15 |
2 files changed, 14 insertions, 15 deletions
diff --git a/plugins/omega/PreOmega.v b/plugins/omega/PreOmega.v index 08bfec84bc..7ebc2fb04f 100644 --- a/plugins/omega/PreOmega.v +++ b/plugins/omega/PreOmega.v @@ -16,7 +16,8 @@ Local Open Scope Z_scope. (** This tactic uses the complete specification of [Z.div] and [Z.modulo] to remove these functions from the goal without losing - information. *) + information. The [Z.div_mod_to_quot_rem_cleanup] tactic removes + needless hypotheses, which makes tactics like [nia] run faster. *) Module Z. Lemma mod_0_r_ext x y : y = 0 -> x mod y = 0. @@ -42,7 +43,16 @@ Module Z. | [ H : context[?x / ?y] |- _ ] => div_mod_to_quot_rem_generalize x y | [ H : context[?x mod ?y] |- _ ] => div_mod_to_quot_rem_generalize x y end. - Ltac div_mod_to_quot_rem := repeat div_mod_to_quot_rem_step. + Ltac div_mod_to_quot_rem' := repeat div_mod_to_quot_rem_step. + Ltac div_mod_to_quot_rem_cleanup := + repeat match goal with + | [ H : ?T -> _, H' : ?T |- _ ] => specialize (H H') + | [ H : ?T -> _, H' : ~?T |- _ ] => clear H + | [ H : ~?T -> _, H' : ?T |- _ ] => clear H + | [ H : 0 < ?x -> _, H' : ?x < 0 |- _ ] => clear H + | [ H : ?x < 0 -> _, H' : 0 < ?x |- _ ] => clear H + end. + Ltac div_mod_to_quot_rem := div_mod_to_quot_rem'; div_mod_to_quot_rem_cleanup. End Z. (** * zify: the Z-ification tactic *) diff --git a/test-suite/success/Nia.v b/test-suite/success/Nia.v index b79a6bde3d..6cb645d9eb 100644 --- a/test-suite/success/Nia.v +++ b/test-suite/success/Nia.v @@ -2,20 +2,9 @@ Require Import Coq.ZArith.ZArith. Require Import Coq.micromega.Lia. Open Scope Z_scope. -Ltac cleanup := - repeat match goal with - | [ H : ?T -> _, H' : ?T |- _ ] => specialize (H H') - | [ H : ?T -> _, H' : ~?T |- _ ] => clear H - | [ H : ~?T -> _, H' : ?T |- _ ] => clear H - | [ H : 0 < ?x -> _, H' : ?x < 0 |- _ ] => clear H - | [ H : ?x < 0 -> _, H' : 0 < ?x |- _ ] => clear H - | _ => progress subst - end. - (** Add [Z.div_mod_to_quot_rem] to the end of [zify], just for this - file. Note that we also add a [cleanup] tactic, which is very - important for speed purposes. *) -Ltac zify ::= repeat (zify_nat; zify_positive; zify_N); zify_op; Z.div_mod_to_quot_rem; cleanup. + file. *) +Ltac zify ::= repeat (zify_nat; zify_positive; zify_N); zify_op; Z.div_mod_to_quot_rem. Lemma Z_zerop_or x : x = 0 \/ x <> 0. Proof. nia. Qed. Lemma Z_eq_dec_or (x y : Z) : x = y \/ x <> y. Proof. nia. Qed. |