aboutsummaryrefslogtreecommitdiff
path: root/src/Util/ZUtil
diff options
context:
space:
mode:
Diffstat (limited to 'src/Util/ZUtil')
-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
9 files changed, 70 insertions, 23 deletions
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-06-14 14:31:10 +0000