diff options
| author | Jason Gross | 2018-12-05 16:05:13 -0500 |
|---|---|---|
| committer | Jason Gross | 2019-01-24 14:31:52 -0500 |
| commit | d69ec6e2e0931a87d2ec3b3f47d1969b365d91f7 (patch) | |
| tree | 6d9502307081d52dd8e00ab53142b1c7f1b54854 /test-suite | |
| parent | 594e53cda3845794bf1e14aec7b0d2a5ee9cd075 (diff) | |
Rename Z.div_mod_to_quot_rem, add Z.quot_rem_to_equations, Z.to_euclidean_division_equations
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/success/Nia.v | 8 |
1 files changed, 6 insertions, 2 deletions
diff --git a/test-suite/success/Nia.v b/test-suite/success/Nia.v index 6cb645d9eb..15028a4c00 100644 --- a/test-suite/success/Nia.v +++ b/test-suite/success/Nia.v @@ -2,9 +2,9 @@ Require Import Coq.ZArith.ZArith. Require Import Coq.micromega.Lia. Open Scope Z_scope. -(** Add [Z.div_mod_to_quot_rem] to the end of [zify], just for this +(** Add [Z.to_euclidean_division_equations] to the end of [zify], just for this file. *) -Ltac zify ::= repeat (zify_nat; zify_positive; zify_N); zify_op; Z.div_mod_to_quot_rem. +Ltac zify ::= repeat (zify_nat; zify_positive; zify_N); zify_op; Z.to_euclidean_division_equations. 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. @@ -22,6 +22,10 @@ Ltac saturate_mod_div := | [ H : context[?x mod ?y] |- _ ] => unique_pose_proof (Z_zerop_or (x / y)) | [ |- context[?x / ?y] ] => unique_pose_proof (Z_zerop_or y) | [ H : context[?x / ?y] |- _ ] => unique_pose_proof (Z_zerop_or y) + | [ |- context[Z.rem ?x ?y] ] => unique_pose_proof (Z_zerop_or (Z.quot x y)) + | [ H : context[Z.rem ?x ?y] |- _ ] => unique_pose_proof (Z_zerop_or (Z.quot x y)) + | [ |- context[Z.quot ?x ?y] ] => unique_pose_proof (Z_zerop_or y) + | [ H : context[Z.quot ?x ?y] |- _ ] => unique_pose_proof (Z_zerop_or y) end. Ltac t := intros; saturate_mod_div; try nia. |