aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--_CoqProject2
-rw-r--r--src/Arithmetic/BarrettReduction/Generalized.v12
-rw-r--r--src/Arithmetic/BarrettReduction/RidiculousFish.v12
-rw-r--r--src/Arithmetic/Saturated/MontgomeryAPI.v2
-rw-r--r--src/Experiments/NewPipeline/Arithmetic.v14
-rw-r--r--src/Experiments/NewPipeline/Toplevel1.v8
-rw-r--r--src/Experiments/SimplyTypedArithmetic.v12
-rw-r--r--src/LegacyArithmetic/Double/Proofs/Multiply.v2
-rw-r--r--src/LegacyArithmetic/Double/Proofs/RippleCarryAddSub.v8
-rw-r--r--src/Util/QUtil.v8
-rw-r--r--src/Util/ZUtil.v10
-rw-r--r--src/Util/ZUtil/AddGetCarry.v2
-rw-r--r--src/Util/ZUtil/CC.v2
-rw-r--r--src/Util/ZUtil/Div.v6
-rw-r--r--src/Util/ZUtil/Div/Bootstrap.v12
-rw-r--r--src/Util/ZUtil/Modulo.v6
-rw-r--r--src/Util/ZUtil/Modulo/Bootstrap.v22
-rw-r--r--src/Util/ZUtil/Tactics/DivModToQuotRem.v39
-rw-r--r--src/Util/ZUtil/Tactics/RewriteModSmall.v2
-rw-r--r--src/Util/ZUtil/ZSimplify/Autogenerated.v2
20 files changed, 116 insertions, 67 deletions
diff --git a/_CoqProject b/_CoqProject
index bbfffaabc..9e426282f 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -6615,10 +6615,12 @@ src/Util/ZUtil/Testbit.v
src/Util/ZUtil/Z2Nat.v
src/Util/ZUtil/ZSimplify.v
src/Util/ZUtil/Zselect.v
+src/Util/ZUtil/Div/Bootstrap.v
src/Util/ZUtil/Hints/Core.v
src/Util/ZUtil/Hints/PullPush.v
src/Util/ZUtil/Hints/ZArith.v
src/Util/ZUtil/Hints/Ztestbit.v
+src/Util/ZUtil/Modulo/Bootstrap.v
src/Util/ZUtil/Modulo/PullPush.v
src/Util/ZUtil/Tactics/CompareToSgn.v
src/Util/ZUtil/Tactics/DivModToQuotRem.v
diff --git a/src/Arithmetic/BarrettReduction/Generalized.v b/src/Arithmetic/BarrettReduction/Generalized.v
index 54b8c7c6c..9fa37721a 100644
--- a/src/Arithmetic/BarrettReduction/Generalized.v
+++ b/src/Arithmetic/BarrettReduction/Generalized.v
@@ -145,8 +145,8 @@ Section barrett.
pose proof (Z.mod_pos_bound (b ^ (2*k)) n).
assert (0 < b ^ (k - offset)) by auto with zarith.
assert (a/n < b ^ k) by auto using Z.div_lt_upper_bound with zarith.
- assert (b ^ (2 * k) - m * n = b ^ (2 * k) mod n) by (subst m; Z.div_mod_to_quot_rem; nia).
- autorewrite with push_Zpow in *; Z.div_mod_to_quot_rem; nia.
+ assert (b ^ (2 * k) - m * n = b ^ (2 * k) mod n) by (subst m; Z.div_mod_to_quot_rem_in_goal; nia).
+ autorewrite with push_Zpow in *; Z.div_mod_to_quot_rem_in_goal; nia.
Qed.
Lemma helper_2 : n * (a / n) - b ^ (k - offset) < b ^ (k - offset) * (a / b ^ (k - offset)).
@@ -154,7 +154,7 @@ Section barrett.
pose proof (Z.mod_pos_bound a n).
pose proof (Z.mod_pos_bound a (b ^ (k - offset))).
assert (0 < b ^ (k - offset)) by auto with zarith.
- Z.div_mod_to_quot_rem; lia.
+ Z.div_mod_to_quot_rem_in_goal; lia.
Qed.
Let epsilon := (a / n) * b ^ (k+offset) - (a / b ^ (k - offset)) * m.
@@ -162,7 +162,7 @@ Section barrett.
Lemma q_epsilon : q = (a / n) + (- epsilon) / b ^ (k + offset).
Proof.
subst q epsilon.
- autorewrite with push_Zpow in *; do 2 Z.div_mod_to_quot_rem; nia.
+ autorewrite with push_Zpow in *; do 2 Z.div_mod_to_quot_rem_in_goal; nia.
Qed.
Lemma epsilon_lower : - b ^ (k + offset) < epsilon.
@@ -170,7 +170,7 @@ Section barrett.
pose proof q_epsilon as Hq_epsilon.
rewrite (proj2_sig q_nice) in Hq_epsilon.
cut (- epsilon / b ^ (k + offset) <= 0);
- [ Z.div_mod_to_quot_rem | break_match_hyps ]; nia.
+ [ Z.div_mod_to_quot_rem_in_goal | break_match_hyps ]; nia.
Qed.
Lemma m_pos : 0 < m.
@@ -192,7 +192,7 @@ Section barrett.
exists (0 <? epsilon).
rewrite q_epsilon.
pose proof epsilon_bound. pose proof epsilon_lower.
- break_match; Z.ltb_to_lt; Z.div_mod_to_quot_rem; nia.
+ break_match; Z.ltb_to_lt; Z.div_mod_to_quot_rem_in_goal; nia.
Qed.
Lemma q_bound : a / n - 1 <= q.
diff --git a/src/Arithmetic/BarrettReduction/RidiculousFish.v b/src/Arithmetic/BarrettReduction/RidiculousFish.v
index 908e098b8..b9697839d 100644
--- a/src/Arithmetic/BarrettReduction/RidiculousFish.v
+++ b/src/Arithmetic/BarrettReduction/RidiculousFish.v
@@ -138,7 +138,7 @@ Lemma wrap_bound (a b : Z) (H : 0 < a) :
0 <= wrap a b < 2^a.
Proof.
unfold wrap.
- Z.div_mod_to_quot_rem.
+ Z.div_mod_to_quot_rem_in_goal.
lia.
Qed.
@@ -147,7 +147,7 @@ Lemma remove_outer_wrap (a a' b : Z) (H : 0 < a' <= a) :
Proof.
unfold wrap.
apply Z.mod_small.
- Z.div_mod_to_quot_rem.
+ Z.div_mod_to_quot_rem_in_goal.
assert (2^a' <= 2^a) by (apply Z.pow_le_mono_r; lia).
lia.
Qed.
@@ -185,7 +185,7 @@ Qed.
Lemma a_minus_b_div_2_plus_b (a b : Z) (H : a >= b) :
(a - b) / 2 + b = (a + b) / 2.
-Proof. Z.div_mod_to_quot_rem; lia. Qed.
+Proof. Z.div_mod_to_quot_rem_in_goal; lia. Qed.
Lemma p_bound (d bits : Z) (Hbits : 0 < bits) (H : 1 < d < 2^bits) :
0 < Z.log2_up d <= bits.
@@ -218,11 +218,11 @@ Qed.
Lemma division_shrinks (a b c : Z) (Hb : 0 < b) (H : 0 <= a < c) :
a / b < c.
-Proof. Z.div_mod_to_quot_rem; nia. Qed.
+Proof. Z.div_mod_to_quot_rem_in_goal; nia. Qed.
Lemma mul_div_ceil_ge (a b : Z) (Hb : 0 < b) :
a <= b * ((a + b - 1) / b).
-Proof. Z.div_mod_to_quot_rem; nia. Qed.
+Proof. Z.div_mod_to_quot_rem_in_goal; nia. Qed.
(** This is the main theorem this algorithm relies on. *)
Lemma division_algorithm (bits n d k : Z)
@@ -380,6 +380,6 @@ Proof.
(* And finish with the main theorem. *)
rewrite (division_algorithm 32) by lia;
- Z.div_mod_to_quot_rem;
+ Z.div_mod_to_quot_rem_in_goal;
nia.
Qed.
diff --git a/src/Arithmetic/Saturated/MontgomeryAPI.v b/src/Arithmetic/Saturated/MontgomeryAPI.v
index 5b5ec1748..6dee1d22b 100644
--- a/src/Arithmetic/Saturated/MontgomeryAPI.v
+++ b/src/Arithmetic/Saturated/MontgomeryAPI.v
@@ -395,7 +395,7 @@ Section API.
eapply small_left_append; eauto.
rewrite @B.Positional.sat_add_div by omega.
repeat match goal with H:_|-_=> unique pose proof (eval_small _ _ H) end.
- cbv [eval] in *; Z.div_mod_to_quot_rem; nia.
+ cbv [eval] in *; Z.div_mod_to_quot_rem_in_goal; nia.
Qed.
Lemma small_join0 {n} b : small b -> small (@join0 n b).
diff --git a/src/Experiments/NewPipeline/Arithmetic.v b/src/Experiments/NewPipeline/Arithmetic.v
index af5c2a766..0433bcda0 100644
--- a/src/Experiments/NewPipeline/Arithmetic.v
+++ b/src/Experiments/NewPipeline/Arithmetic.v
@@ -175,7 +175,7 @@ Module Associational.
| _ => progress nsatz end. Qed.
Lemma eval_splitQ s p (s_nz:Qnum s<>0) :
eval (fst (splitQ s p)) + (Qnum s * eval (snd (splitQ s p))) / Zpos (Qden s) = eval p.
- Proof. rewrite eval_snd_splitQ, eval_fst_partition by assumption; cbv [splitQ Let_In]; cbn [fst snd]; Z.div_mod_to_quot_rem; nia. Qed.
+ Proof. rewrite eval_snd_splitQ, eval_fst_partition by assumption; cbv [splitQ Let_In]; cbn [fst snd]; Z.div_mod_to_quot_rem_in_goal; nia. Qed.
Lemma eval_splitQ_mul s p (s_nz:Qnum s<>0) :
eval (fst (splitQ s p)) * Zpos (Qden s) + (Qnum s * eval (snd (splitQ s p))) = eval p * Zpos (Qden s).
Proof. rewrite eval_snd_splitQ, eval_fst_partition by assumption; cbv [splitQ Let_In]; cbn [fst snd]; nia. Qed.
@@ -270,7 +270,7 @@ Module Associational.
Lemma eval_map_mul_div' s a b c (s_nz:s <> 0) (a_mod : (a*a) mod s = 0)
: eval (map (fun x => (((a * a) * fst x) / s, (b * b) * snd x)) c) = ((a * a) / s) * (b * b) * eval c.
- Proof. rewrite <- eval_map_mul_div by assumption; f_equal; apply map_ext; intro; Z.div_mod_to_quot_rem; f_equal; nia. Qed.
+ Proof. rewrite <- eval_map_mul_div by assumption; f_equal; apply map_ext; intro; Z.div_mod_to_quot_rem_in_goal; f_equal; nia. Qed.
Hint Rewrite eval_map_mul_div' using solve [ auto ] : push_eval.
Lemma eval_flat_map_if A (f : A -> bool) g h p
@@ -932,7 +932,7 @@ Section mod_ops.
cut (1 < weight 1); [ lia | ].
cbv [weight Z.of_nat]; autorewrite with zsimplify_fast.
apply Z.pow_gt_1; [ omega | ].
- Z.div_mod_to_quot_rem; nia.
+ Z.div_mod_to_quot_rem_in_goal; nia.
Qed.
Derive carry_mulmod
@@ -1183,7 +1183,7 @@ Module Saturated.
Lemma div_step a b c d : 0 < a -> 0 < b ->
(c / a + d) / b = (a * d + c) / (a * b).
- Proof. intros; Z.div_mod_to_quot_rem; nia. Qed.
+ Proof. intros; Z.div_mod_to_quot_rem_in_goal; nia. Qed.
Lemma add_mod_div_multiple a b n m:
n > 0 ->
@@ -2662,10 +2662,10 @@ Section freeze_mod_ops.
transitivity (weight n); [ omega | ].
cbv [weight bytes_n].
Z.peel_le.
- rewrite Z.log2_up_pow2 by (Z.div_mod_to_quot_rem; nia).
+ rewrite Z.log2_up_pow2 by (Z.div_mod_to_quot_rem_in_goal; nia).
autorewrite with push_Zof_nat.
- rewrite Z2Nat.id by (Z.div_mod_to_quot_rem; nia).
- Z.div_mod_to_quot_rem; nia. }
+ rewrite Z2Nat.id by (Z.div_mod_to_quot_rem_in_goal; nia).
+ Z.div_mod_to_quot_rem_in_goal; nia. }
{ cbv [to_bytesmod].
rewrite Rows.flatten_partitions' by eauto using wprops, Rows.length_from_associational.
rewrite Rows.eval_from_associational by (cbv [bytes_n]; eauto with omega).
diff --git a/src/Experiments/NewPipeline/Toplevel1.v b/src/Experiments/NewPipeline/Toplevel1.v
index 57c717e7c..e802c2dd7 100644
--- a/src/Experiments/NewPipeline/Toplevel1.v
+++ b/src/Experiments/NewPipeline/Toplevel1.v
@@ -2441,10 +2441,10 @@ Module BarrettReduction.
Proof.
cbv [mul_high Let_In]; rewrite Z.pow_add_r, Z.pow_1_r by omega; intros.
assert (4 <= 2 ^ k) by (transitivity (Z.pow 2 2); auto with zarith).
- assert (0 <= x * y / 2^k < 2^k*2^k) by (Z.div_mod_to_quot_rem; nia).
+ assert (0 <= x * y / 2^k < 2^k*2^k) by (Z.div_mod_to_quot_rem_in_goal; nia).
rewrite mul_high_idea with (a:=x) (b:=y) (a0 := low a) (a1 := high a) (b0 := low b) (b1 := high b) in *
- by (push_rep; Z.div_mod_to_quot_rem; lia).
+ by (push_rep; Z.div_mod_to_quot_rem_in_goal; lia).
push_rep. subst a0b1.
assert (y / 2 ^ k < 2) by (apply Z.div_lt_upper_bound; omega).
@@ -2453,7 +2453,7 @@ Module BarrettReduction.
eapply represents_trans.
{ repeat (apply wideadd_represents;
- [ | apply represents_small; Z.div_mod_to_quot_rem; nia| ]).
+ [ | apply represents_small; Z.div_mod_to_quot_rem_in_goal; nia| ]).
erewrite represents_high; [ | apply widemul_represents; solve [ auto with zarith ] ].
{ apply represents_add; try reflexivity; solve [auto with zarith]. }
{ match goal with H : 0 <= ?x + ?y < ?z |- 0 <= ?x < ?z =>
@@ -2518,7 +2518,7 @@ Module BarrettReduction.
(* assertions to help arith tactics *)
pose proof x_bounds.
assert (2^k * M < 2 ^ (2*k)) by (rewrite <-Z.add_diag, Z.pow_add_r; nia).
- assert (0 <= x / (2 ^ k * (2 ^ k / 2)) < 2) by (Z.div_mod_to_quot_rem; auto with nia).
+ assert (0 <= x / (2 ^ k * (2 ^ k / 2)) < 2) by (Z.div_mod_to_quot_rem_in_goal; auto with nia).
assert (0 < 2 ^ k / 2) by Z.zero_bounds.
assert (2 ^ (k - 1) <> 0) by auto with zarith.
assert (2 < 2 ^ k) by (eapply Z.le_lt_trans with (m:=2 ^ 1); auto with zarith).
diff --git a/src/Experiments/SimplyTypedArithmetic.v b/src/Experiments/SimplyTypedArithmetic.v
index 4c8830795..3745e59ff 100644
--- a/src/Experiments/SimplyTypedArithmetic.v
+++ b/src/Experiments/SimplyTypedArithmetic.v
@@ -526,7 +526,7 @@ Section mod_ops.
cut (1 < weight 1); [ lia | ].
cbv [weight Z.of_nat]; autorewrite with zsimplify_fast.
apply Z.pow_gt_1; [ omega | ].
- Z.div_mod_to_quot_rem; nia.
+ Z.div_mod_to_quot_rem_in_goal; nia.
Qed.
Derive carry_mulmod
@@ -748,7 +748,7 @@ Module Saturated.
Lemma div_step a b c d : 0 < a -> 0 < b ->
(c / a + d) / b = (a * d + c) / (a * b).
- Proof. intros; Z.div_mod_to_quot_rem; nia. Qed.
+ Proof. intros; Z.div_mod_to_quot_rem_in_goal; nia. Qed.
Lemma add_mod_div_multiple a b n m:
n > 0 ->
@@ -11096,10 +11096,10 @@ Module BarrettReduction.
Proof.
cbv [mul_high Let_In]; rewrite Z.pow_add_r, Z.pow_1_r by omega; intros.
assert (4 <= 2 ^ k) by (transitivity (Z.pow 2 2); auto with zarith).
- assert (0 <= x * y / 2^k < 2^k*2^k) by (Z.div_mod_to_quot_rem; nia).
+ assert (0 <= x * y / 2^k < 2^k*2^k) by (Z.div_mod_to_quot_rem_in_goal; nia).
rewrite mul_high_idea with (a:=x) (b:=y) (a0 := low a) (a1 := high a) (b0 := low b) (b1 := high b) in *
- by (push_rep; Z.div_mod_to_quot_rem; lia).
+ by (push_rep; Z.div_mod_to_quot_rem_in_goal; lia).
push_rep. subst a0b1.
assert (y / 2 ^ k < 2) by (apply Z.div_lt_upper_bound; omega).
@@ -11108,7 +11108,7 @@ Module BarrettReduction.
eapply represents_trans.
{ repeat (apply wideadd_represents;
- [ | apply represents_small; Z.div_mod_to_quot_rem; nia| ]).
+ [ | apply represents_small; Z.div_mod_to_quot_rem_in_goal; nia| ]).
erewrite represents_high; [ | apply widemul_represents; solve [ auto with zarith ] ].
{ apply represents_add; try reflexivity; solve [auto with zarith]. }
{ match goal with H : 0 <= ?x + ?y < ?z |- 0 <= ?x < ?z =>
@@ -11173,7 +11173,7 @@ Module BarrettReduction.
(* assertions to help arith tactics *)
pose proof x_bounds.
assert (2^k * M < 2 ^ (2*k)) by (rewrite <-Z.add_diag, Z.pow_add_r; nia).
- assert (0 <= x / (2 ^ k * (2 ^ k / 2)) < 2) by (Z.div_mod_to_quot_rem; auto with nia).
+ assert (0 <= x / (2 ^ k * (2 ^ k / 2)) < 2) by (Z.div_mod_to_quot_rem_in_goal; auto with nia).
assert (0 < 2 ^ k / 2) by Z.zero_bounds.
assert (2 ^ (k - 1) <> 0) by auto with zarith.
assert (2 < 2 ^ k) by (eapply Z.le_lt_trans with (m:=2 ^ 1); auto with zarith).
diff --git a/src/LegacyArithmetic/Double/Proofs/Multiply.v b/src/LegacyArithmetic/Double/Proofs/Multiply.v
index 8fed917d9..98692ed7f 100644
--- a/src/LegacyArithmetic/Double/Proofs/Multiply.v
+++ b/src/LegacyArithmetic/Double/Proofs/Multiply.v
@@ -89,7 +89,7 @@ Section tuple2.
Z.rewrite_mod_small.
push_Zmod; pull_Zmod.
apply f_equal2; [ | reflexivity ].
- Z.div_mod_to_quot_rem; nia.
+ Z.div_mod_to_quot_rem_in_goal; nia.
Qed.
Lemma decode_mul_double_function x y
diff --git a/src/LegacyArithmetic/Double/Proofs/RippleCarryAddSub.v b/src/LegacyArithmetic/Double/Proofs/RippleCarryAddSub.v
index d0514db57..4f6a79e8d 100644
--- a/src/LegacyArithmetic/Double/Proofs/RippleCarryAddSub.v
+++ b/src/LegacyArithmetic/Double/Proofs/RippleCarryAddSub.v
@@ -56,11 +56,11 @@ Proof.
assert (0 < 2 ^ k) by auto with zarith.
assert (0 < 2^n * 2^k) by nia.
autorewrite with Zshift_to_pow push_Zpow.
- rewrite <- (Zmod_small ((z0 mod _) + _) (2^k * 2^n)) by (Z.div_mod_to_quot_rem; nia).
+ rewrite <- (Zmod_small ((z0 mod _) + _) (2^k * 2^n)) by (Z.div_mod_to_quot_rem_in_goal; nia).
rewrite <- !Z.mul_mod_distr_r by lia.
rewrite !(Z.mul_comm (2^k)); pull_Zmod.
split; [ | apply f_equal2 ];
- Z.div_mod_to_quot_rem; nia.
+ Z.div_mod_to_quot_rem_in_goal; nia.
Qed.
Section carry_sub_is_good.
Context (n k z0 z1 : Z)
@@ -93,10 +93,10 @@ Section carry_sub_is_good.
assert (0 < 2 ^ k) by auto with zarith.
assert (0 < 2^n * 2^k) by nia.
autorewrite with Zshift_to_pow push_Zpow.
- rewrite <- (Zmod_small ((z0 mod _) + _) (2^k * 2^n)) by (Z.div_mod_to_quot_rem; nia).
+ rewrite <- (Zmod_small ((z0 mod _) + _) (2^k * 2^n)) by (Z.div_mod_to_quot_rem_in_goal; nia).
rewrite <- !Z.mul_mod_distr_r by lia.
rewrite !(Z.mul_comm (2^k)); pull_Zmod.
- apply f_equal2; Z.div_mod_to_quot_rem; break_match; Z.ltb_to_lt; try reflexivity;
+ apply f_equal2; Z.div_mod_to_quot_rem_in_goal; break_match; Z.ltb_to_lt; try reflexivity;
match goal with
| [ q : Z |- _ = _ :> Z ]
=> first [ cut (q = -1); [ intro; subst; ring | nia ]
diff --git a/src/Util/QUtil.v b/src/Util/QUtil.v
index 86dabd13e..dbdf4fba0 100644
--- a/src/Util/QUtil.v
+++ b/src/Util/QUtil.v
@@ -6,23 +6,23 @@ Local Open Scope Z_scope.
Lemma Qfloor_le_add a b : Qfloor a + Qfloor b <= Qfloor (a + b).
destruct a as [x y], b as [a b]; cbv [Qceiling Qfloor Qplus Qopp QArith_base.Qden QArith_base.Qnum].
- Z.div_mod_to_quot_rem; nia.
+ Z.div_mod_to_quot_rem_in_goal; nia.
Qed.
Lemma Qceiling_le_add a b : Qceiling (a + b) <= Qceiling a + Qceiling b.
destruct a as [x y], b as [a b]; cbv [Qceiling Qfloor Qplus Qopp QArith_base.Qden QArith_base.Qnum].
- Z.div_mod_to_quot_rem. nia.
+ Z.div_mod_to_quot_rem_in_goal. nia.
Qed.
Lemma add_floor_l_le_ceiling a b : Qfloor a + Qceiling b <= Qceiling (a + b).
destruct a as [x y], b as [a b]; cbv [Qceiling Qfloor Qplus Qopp QArith_base.Qden QArith_base.Qnum].
- Z.div_mod_to_quot_rem; nia.
+ Z.div_mod_to_quot_rem_in_goal; nia.
Qed.
Lemma Zle_floor_ceiling a : Z.le (Qfloor a) (Qceiling a).
pose proof Qle_floor_ceiling.
destruct a as [x y]; cbv [Qceiling Qfloor Qplus Qopp QArith_base.Qden QArith_base.Qnum].
- Z.div_mod_to_quot_rem; nia.
+ Z.div_mod_to_quot_rem_in_goal; nia.
Qed.
Section pow_ceil_mul_nat.
diff --git a/src/Util/ZUtil.v b/src/Util/ZUtil.v
index 2abfa7398..270bd0c90 100644
--- a/src/Util/ZUtil.v
+++ b/src/Util/ZUtil.v
@@ -891,7 +891,7 @@ Module Z.
Hint Rewrite sub_mod_mod_0 : zsimplify.
Lemma div_between n a b : 0 <= n -> b <> 0 -> n * b <= a < (1 + n) * b -> a / b = n.
- Proof. intros; Z.div_mod_to_quot_rem; nia. Qed.
+ Proof. intros; Z.div_mod_to_quot_rem_in_goal; nia. Qed.
Hint Rewrite div_between using zutil_arith : zsimplify.
Lemma mod_small_n n a b : 0 <= n -> b <> 0 -> n * b <= a < (1 + n) * b -> a mod b = a - n * b.
@@ -1371,7 +1371,7 @@ Module Z.
=> solve [ transitivity (-0); auto with zarith ]
end.
{ repeat match goal with H : context[_ mod _] |- _ => revert H end;
- Z.div_mod_to_quot_rem; nia. }
+ Z.div_mod_to_quot_rem_in_goal; nia. }
Qed.
Lemma shiftl_le_Proper1 x
@@ -1424,7 +1424,7 @@ Module Z.
assert (Hn : x <> y) by congruence;
assert (x < y) by omega; clear H Hn
| _ => solve [ repeat match goal with H : context[_ mod _] |- _ => revert H end;
- Z.div_mod_to_quot_rem; subst;
+ Z.div_mod_to_quot_rem_in_goal; subst;
lazymatch goal with
| [ |- _ <= (?a * ?q + ?r) * ?q' ]
=> transitivity (q * (a * q') + r * q');
@@ -1438,10 +1438,10 @@ Module Z.
assert (1 < 2^(y'-y)) by auto with zarith.
assert (0 < x / 2^y)
by (repeat match goal with H : context[_ mod _] |- _ => revert H end;
- Z.div_mod_to_quot_rem; nia).
+ Z.div_mod_to_quot_rem_in_goal; nia).
assert (2^y <= x)
by (repeat match goal with H : context[_ / _] |- _ => revert H end;
- Z.div_mod_to_quot_rem; nia).
+ Z.div_mod_to_quot_rem_in_goal; nia).
match goal with
| [ |- ?x + 1 <= ?y ] => cut (x < y); [ omega | ]
end.
diff --git a/src/Util/ZUtil/AddGetCarry.v b/src/Util/ZUtil/AddGetCarry.v
index 5b8cbf13e..49b3e6332 100644
--- a/src/Util/ZUtil/AddGetCarry.v
+++ b/src/Util/ZUtil/AddGetCarry.v
@@ -38,7 +38,7 @@ Module Z.
reflexivity. }
{ f_equal.
{ push_Zmod; pull_Zmod; apply f_equal2; omega. }
- { Z.div_mod_to_quot_rem; nia. } }
+ { Z.div_mod_to_quot_rem_in_goal; nia. } }
{ subst; autorewrite with zsimplify; f_equal; omega. }
Qed.
diff --git a/src/Util/ZUtil/CC.v b/src/Util/ZUtil/CC.v
index fb2fb1b93..4a130a9f2 100644
--- a/src/Util/ZUtil/CC.v
+++ b/src/Util/ZUtil/CC.v
@@ -27,6 +27,6 @@ Module Z.
| _ => apply Z.div_lt_upper_bound
| _ => solve [Z.zero_bounds]
end.
- Z.div_mod_to_quot_rem; lia.
+ Z.div_mod_to_quot_rem_in_goal; lia.
Qed.
End Z. \ No newline at end of file
diff --git a/src/Util/ZUtil/Div.v b/src/Util/ZUtil/Div.v
index 4616a6090..a9fc4aae0 100644
--- a/src/Util/ZUtil/Div.v
+++ b/src/Util/ZUtil/Div.v
@@ -201,7 +201,7 @@ Module Z.
destruct c', d; cbn [Z.abs Z.sgn];
rewrite ?Zdiv_0_r, ?Z.mul_0_r, ?Z.mul_0_l, ?Z.mul_1_l, ?Z.mul_1_r;
try lia; intros ?? H;
- Z.div_mod_to_quot_rem;
+ Z.div_mod_to_quot_rem_in_goal;
subst.
all: repeat match goal with
| [ H : context[_ * -1] |- _ ] => rewrite (Z.mul_add_distr_r _ _ (-1)), <- ?(Z.mul_comm (-1)), ?Z.mul_assoc in H
@@ -213,10 +213,10 @@ Module Z.
all:lazymatch goal with
| [ H : (Z.pos ?p * ?q + ?r) * Z.pos ?p' <= (Z.pos ?p' * ?q' + ?r') * Z.pos ?p |- _ ]
=> let H' := fresh in
- assert (H' : q <= q' + (r' * Z.pos p - r * Z.pos p') / (Z.pos p * Z.pos p')) by (Z.div_mod_to_quot_rem; nia);
+ assert (H' : q <= q' + (r' * Z.pos p - r * Z.pos p') / (Z.pos p * Z.pos p')) by (Z.div_mod_to_quot_rem_in_goal; nia);
revert H'
end.
- all:Z.div_mod_to_quot_rem; nia.
+ all:Z.div_mod_to_quot_rem_in_goal; nia.
Qed.
Lemma div_positive_gt_0 : forall a b, a > 0 -> b > 0 -> a mod b = 0 ->
diff --git a/src/Util/ZUtil/Div/Bootstrap.v b/src/Util/ZUtil/Div/Bootstrap.v
new file mode 100644
index 000000000..3b9338073
--- /dev/null
+++ b/src/Util/ZUtil/Div/Bootstrap.v
@@ -0,0 +1,12 @@
+(** Basic lemmas about [Z.div] for bootstrapping various tactics *)
+Require Import Coq.ZArith.ZArith.
+Require Import Coq.micromega.Lia.
+Require Import Crypto.Util.ZUtil.Hints.Core.
+Local Open Scope Z_scope.
+
+Module Z.
+ Lemma div_0_r_eq a b : b = 0 -> a / b = 0.
+ Proof. intro; subst; auto with zarith. Qed.
+ Hint Resolve div_0_r_eq : zarith.
+ Hint Rewrite div_0_r_eq using assumption : zsimplify.
+End Z.
diff --git a/src/Util/ZUtil/Modulo.v b/src/Util/ZUtil/Modulo.v
index 953b3b2f3..be513eb3c 100644
--- a/src/Util/ZUtil/Modulo.v
+++ b/src/Util/ZUtil/Modulo.v
@@ -159,7 +159,7 @@ Module Z.
+ if c <? 0 then - X ((a / b) mod c) (a mod (c * b)) ((a mod (c * b)) / b) a b c (a / b) else 0.
Proof.
intros; break_match; Z.ltb_to_lt; rewrite ?Z.sub_0_r, ?Z.add_0_r;
- assert (0 <> c * b) by nia; Z.div_mod_to_quot_rem; subst;
+ assert (0 <> c * b) by nia; Z.div_mod_to_quot_rem_in_goal; subst;
destruct_head'_or; destruct_head'_and;
try assert (b < 0) by omega;
try assert (c < 0) by omega;
@@ -259,7 +259,7 @@ Module Z.
Proof.
destruct (Z_dec d 0) as [ [?|?] | ? ];
try solve [ subst; autorewrite with zsimplify; simpl; split; reflexivity
- | repeat first [ progress Z.div_mod_to_quot_rem
+ | repeat first [ progress Z.div_mod_to_quot_rem_in_goal
| progress subst
| progress break_innermost_match
| progress Z.ltb_to_lt
@@ -282,7 +282,7 @@ Module Z.
Lemma mod_mod_0_0_eq x y : x mod y = 0 -> y mod x = 0 -> x = y \/ x = - y \/ x = 0 \/ y = 0.
Proof.
destruct (Z_zerop x), (Z_zerop y); eauto.
- Z.div_mod_to_quot_rem; subst.
+ Z.div_mod_to_quot_rem_in_goal; subst.
rewrite ?Z.add_0_r in *.
match goal with
| [ H : ?x = ?x * ?q * ?q' |- _ ]
diff --git a/src/Util/ZUtil/Modulo/Bootstrap.v b/src/Util/ZUtil/Modulo/Bootstrap.v
new file mode 100644
index 000000000..668aaa331
--- /dev/null
+++ b/src/Util/ZUtil/Modulo/Bootstrap.v
@@ -0,0 +1,22 @@
+(** Basic lemmas about [Z.modulo] for bootstrapping various tactics *)
+Require Import Coq.ZArith.ZArith.
+Require Import Coq.micromega.Lia.
+Require Import Crypto.Util.ZUtil.Hints.Core.
+Local Open Scope Z_scope.
+
+Module Z.
+ Lemma mod_0_r_eq a b : b = 0 -> a mod b = 0.
+ Proof. intro; subst; auto with zarith. Qed.
+ Hint Resolve mod_0_r_eq : zarith.
+ Hint Rewrite mod_0_r_eq using assumption : zsimplify.
+
+ Lemma div_mod_cases x y : ((x = y * (x / y) + x mod y /\ (y < x mod y <= 0 \/ 0 <= x mod y < y))
+ \/ (y = 0 /\ x / y = 0 /\ x mod y = 0)).
+ Proof.
+ destruct (Z_zerop y); [ right; subst; auto with zarith | left ]; subst.
+ split; [ apply Z.div_mod; assumption | ].
+ destruct (Z_dec' y 0) as [ [H|H] | H]; [ left | right | congruence ].
+ { apply Z.mod_neg_bound; assumption. }
+ { apply Z.mod_pos_bound; assumption. }
+ Qed.
+End Z.
diff --git a/src/Util/ZUtil/Tactics/DivModToQuotRem.v b/src/Util/ZUtil/Tactics/DivModToQuotRem.v
index 178844d3b..a52798d20 100644
--- a/src/Util/ZUtil/Tactics/DivModToQuotRem.v
+++ b/src/Util/ZUtil/Tactics/DivModToQuotRem.v
@@ -1,4 +1,6 @@
Require Import Coq.ZArith.ZArith.
+Require Import Crypto.Util.ZUtil.Div.Bootstrap.
+Require Import Crypto.Util.ZUtil.Modulo.Bootstrap.
Require Import Crypto.Util.ZUtil.Hints.Core.
Local Open Scope Z_scope.
@@ -12,18 +14,22 @@ Module Z.
Ltac generalize_div_eucl x y :=
let H := fresh in
let H' := fresh in
- assert (H' : y <> 0) by div_mod_to_quot_rem_inequality_solver;
- generalize (Z.div_mod x y H'); clear H';
- first [ assert (H' : 0 < y) by div_mod_to_quot_rem_inequality_solver;
- generalize (Z.mod_pos_bound x y H'); clear H'
- | assert (H' : y < 0) by div_mod_to_quot_rem_inequality_solver;
- generalize (Z.mod_neg_bound x y H'); clear H'
- | assert (H' : y < 0 \/ 0 < y) by (apply Z.neg_pos_cases; div_mod_to_quot_rem_inequality_solver);
- let H'' := fresh in
- assert (H'' : y < x mod y <= 0 \/ 0 <= x mod y < y)
- by (destruct H'; [ left; apply Z.mod_neg_bound; assumption
- | right; apply Z.mod_pos_bound; assumption ]);
- clear H'; revert H'' ];
+ first
+ [ assert (H' : y <> 0) by div_mod_to_quot_rem_inequality_solver;
+ generalize (Z.div_mod x y H'); clear H';
+ first [ assert (H' : 0 < y) by div_mod_to_quot_rem_inequality_solver;
+ generalize (Z.mod_pos_bound x y H'); clear H'
+ | assert (H' : y < 0) by div_mod_to_quot_rem_inequality_solver;
+ generalize (Z.mod_neg_bound x y H'); clear H'
+ | assert (H' : y = 0) by div_mod_to_quot_rem_inequality_solver;
+ generalize (Z.div_0_r_eq x y H') (Z.mod_0_r_eq x y H'); clear H'
+ | assert (H' : y < 0 \/ 0 < y) by (apply Z.neg_pos_cases; div_mod_to_quot_rem_inequality_solver);
+ let H'' := fresh in
+ assert (H'' : y < x mod y <= 0 \/ 0 <= x mod y < y)
+ by (destruct H'; [ left; apply Z.mod_neg_bound; assumption
+ | right; apply Z.mod_pos_bound; assumption ]);
+ clear H'; revert H'' ]
+ | generalize (Z.div_mod_cases x y) ];
let q := fresh "q" in
let r := fresh "r" in
set (q := x / y) in *;
@@ -36,5 +42,12 @@ Module Z.
| [ |- context[?x mod ?y] ] => generalize_div_eucl x y
end.
- Ltac div_mod_to_quot_rem := repeat div_mod_to_quot_rem_step; intros.
+ Ltac div_mod_to_quot_rem_hyps_step :=
+ match goal with
+ | [ H : context[?x / ?y] |- _ ] => generalize_div_eucl x y
+ | [ H : context[?x mod ?y] |- _ ] => generalize_div_eucl x y
+ end.
+
+ Ltac div_mod_to_quot_rem := repeat first [ div_mod_to_quot_rem_step | div_mod_to_quot_rem_hyps_step ]; intros.
+ Ltac div_mod_to_quot_rem_in_goal := repeat div_mod_to_quot_rem_step; intros.
End Z.
diff --git a/src/Util/ZUtil/Tactics/RewriteModSmall.v b/src/Util/ZUtil/Tactics/RewriteModSmall.v
index 45598b0c5..6b3b05a41 100644
--- a/src/Util/ZUtil/Tactics/RewriteModSmall.v
+++ b/src/Util/ZUtil/Tactics/RewriteModSmall.v
@@ -20,7 +20,7 @@ Module Z.
| [ H : context[(_ mod _)%Z] |- _ ]
=> revert H
end.
- Z.div_mod_to_quot_rem.
+ Z.div_mod_to_quot_rem_in_goal.
lazymatch goal with
| [ H : a = (?x * ?n * ?q) + _, H' : a = (?n * ?q') + _ |- _ ]
=> assert (q' = x * q) by nia; subst q'; nia
diff --git a/src/Util/ZUtil/ZSimplify/Autogenerated.v b/src/Util/ZUtil/ZSimplify/Autogenerated.v
index b3b6d36b6..df2abfe33 100644
--- a/src/Util/ZUtil/ZSimplify/Autogenerated.v
+++ b/src/Util/ZUtil/ZSimplify/Autogenerated.v
@@ -5,7 +5,7 @@ Local Open Scope Z_scope.
Module Z.
Local Ltac simplify_div_tac :=
- intros; Z.div_mod_to_quot_rem; nia.
+ intros; Z.div_mod_to_quot_rem_in_goal; nia.
(* Naming Convention: [X] for thing being divided by, [p] for plus,
[m] for minus, [d] for div, and [_] to separate parentheses and
multiplication. *)
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-23 18:56:47 +0000