diff options
Diffstat (limited to 'src/Util/ZUtil')
-rw-r--r-- | src/Util/ZUtil/AddGetCarry.v | 2 | ||||
-rw-r--r-- | src/Util/ZUtil/CC.v | 2 | ||||
-rw-r--r-- | src/Util/ZUtil/Div.v | 6 | ||||
-rw-r--r-- | src/Util/ZUtil/Div/Bootstrap.v | 12 | ||||
-rw-r--r-- | src/Util/ZUtil/Modulo.v | 6 | ||||
-rw-r--r-- | src/Util/ZUtil/Modulo/Bootstrap.v | 22 | ||||
-rw-r--r-- | src/Util/ZUtil/Tactics/DivModToQuotRem.v | 39 | ||||
-rw-r--r-- | src/Util/ZUtil/Tactics/RewriteModSmall.v | 2 | ||||
-rw-r--r-- | src/Util/ZUtil/ZSimplify/Autogenerated.v | 2 |
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. *) |