From 17f9fb3f28e450be8f09efe0d787393beaede697 Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Thu, 29 Feb 2024 22:18:35 +0000 Subject: [PATCH] adapt to coq/coq#18730 --- rupicola | 2 +- src/Arithmetic/BarrettReduction.v | 2 +- src/Arithmetic/BarrettReduction/HAC.v | 1 + src/Arithmetic/Core.v | 4 +- src/Arithmetic/SolinasReduction.v | 18 +- src/Arithmetic/WordByWordMontgomery.v | 3 +- src/Curves/TableMult/TableMult.v | 2 +- src/Util/NumTheoryUtil.v | 1 + src/Util/SideConditions/Autosolve.v | 4 +- src/Util/SideConditions/ModInvPackage.v | 24 -- src/Util/ZUtil/ModInv.v | 408 ++---------------------- 11 files changed, 45 insertions(+), 424 deletions(-) delete mode 100644 src/Util/SideConditions/ModInvPackage.v diff --git a/rupicola b/rupicola index b285278aed..e0472756de 160000 --- a/rupicola +++ b/rupicola @@ -1 +1 @@ -Subproject commit b285278aeda3f74de5f3cf0bff1bc3b3c8c6327c +Subproject commit e0472756de5bba67a38a4c87d9edfa6fd0365caf diff --git a/src/Arithmetic/BarrettReduction.v b/src/Arithmetic/BarrettReduction.v index 2f0945a32d..89173e4e1c 100644 --- a/src/Arithmetic/BarrettReduction.v +++ b/src/Arithmetic/BarrettReduction.v @@ -314,7 +314,7 @@ Module Fancy. Proof. intros. subst a b. autorewrite with push_Zmul. ring_simplify_subterms. rewrite Z.pow_2_r. - rewrite Z.div_add_exact by (push_Zmod; autorewrite with zsimplify; lia). + rewrite Z.div_add_exact by (push_Zmod; rewrite ?Zmod_0_l; lia). repeat match goal with | |- context [d * ?a * ?b * ?c] => replace (d * a * b * c) with (a * b * c * d) by ring diff --git a/src/Arithmetic/BarrettReduction/HAC.v b/src/Arithmetic/BarrettReduction/HAC.v index 21a41db9a4..98fae91d78 100644 --- a/src/Arithmetic/BarrettReduction/HAC.v +++ b/src/Arithmetic/BarrettReduction/HAC.v @@ -61,6 +61,7 @@ Section barrett. Lemma r_mod_3m_eq_orig : r_mod_3m = r_mod_3m_orig. Proof using base_pos k_big_enough m_pos m_small offset_nonneg r1 r2. + clear μ_good x_nonneg. assert (0 <= r1 < b^(k+offset)) by (subst r1; auto with zarith). assert (0 <= r2 < b^(k+offset)) by (subst r2; auto with zarith). subst r_mod_3m r_mod_3m_orig; cbv zeta. diff --git a/src/Arithmetic/Core.v b/src/Arithmetic/Core.v index 4ee559970d..b554c37fd5 100644 --- a/src/Arithmetic/Core.v +++ b/src/Arithmetic/Core.v @@ -1106,7 +1106,7 @@ Module Positional. Lemma length_sub a b : length a = n -> length b = n -> length (sub a b) = n. - Proof using length_balance. intros; cbv [sub scmul negate_snd]; repeat distr_length. Qed. + Proof using length_balance. clear dependent s. intros; cbv [sub scmul negate_snd]; repeat distr_length. Qed. Hint Rewrite length_sub : distr_length. Definition opp (a:list Z) : list Z := sub (zeros n) a. @@ -1119,7 +1119,7 @@ Module Positional. Proof using m_nz s_nz weight_0 weight_nz eval_balance length_balance. intros; cbv [opp]; push; distr_length; auto. Qed. Lemma length_opp a : length a = n -> length (opp a) = n. - Proof using length_balance. cbv [opp]; intros; repeat distr_length. Qed. + Proof using length_balance. clear dependent s. cbv [opp]; intros; repeat distr_length. Qed. End sub. Hint Rewrite @eval_scmul @eval_opp @eval_sub : push_eval. Hint Rewrite @length_scmul @length_sub @length_opp : distr_length. diff --git a/src/Arithmetic/SolinasReduction.v b/src/Arithmetic/SolinasReduction.v index 07bcbead50..0c4b34ad05 100644 --- a/src/Arithmetic/SolinasReduction.v +++ b/src/Arithmetic/SolinasReduction.v @@ -1215,6 +1215,7 @@ Module SolinasReduction. eval weight (2 * n) (mul_no_reduce base n p q) = eval weight n p * Positional.eval weight n q. Proof using base_nz n_gt_1 wprops. + clear dependent s. intros p q. cbv [mul_no_reduce]. break_match. @@ -1260,6 +1261,7 @@ Module SolinasReduction. Theorem length_mul_no_reduce : forall p q, length (mul_no_reduce base n p q) = (2 * n)%nat. Proof using base_nz n_gt_1 wprops. + clear dependent s. intros; unfold mul_no_reduce; break_match; push. Qed. Hint Rewrite length_mul_no_reduce : push_length. @@ -1322,6 +1324,7 @@ Module SolinasReduction. (combine (map weight (seq 0 n)) (firstn n p), (combine (map weight (seq 0 (m1 - n))) (skipn n p))). Proof using n_gt_1 wprops. + clear dependent s. intros m1 p ? ?. replace m1 with (n + (m1 - n))%nat at 1 by lia. rewrite <-(firstn_skipn n p) at 1. @@ -2432,13 +2435,13 @@ Module SolinasReduction. Lemma sat_mul_comm (p q : list (Z * Z)) : Associational.eval (Associational.sat_mul base p q) = Associational.eval (Associational.sat_mul base q p). - Proof using base_nz n_gt_1. push; lia. Qed. + Proof using base_nz n_gt_1. clear dependent s. push; lia. Qed. Lemma sat_mul_distr (p q1 q2 : list (Z * Z)) : Associational.eval (Associational.sat_mul base p (q1 ++ q2)) = Associational.eval (Associational.sat_mul base p q1) + Associational.eval (Associational.sat_mul base p q2). - Proof using base_nz n_gt_1. push; lia. Qed. + Proof using base_nz n_gt_1. clear dependent s. push; lia. Qed. Lemma cons_to_app {A} a (p : list A) : a :: p = [a] ++ p. @@ -2451,6 +2454,7 @@ Module SolinasReduction. eval weight m (fst (Rows.flatten' weight state inp)) = (Rows.eval weight m inp + eval weight m (fst state) + weight m * snd state) mod weight m. Proof using n_gt_1 wprops. + clear dependent s. intros. rewrite Rows.flatten'_correct with (n:=m) by auto. push. @@ -2463,13 +2467,14 @@ Module SolinasReduction. Lemma sum_one x : sum [x] = x. - Proof. cbn; lia. Qed. + Proof. clear dependent s; cbn; lia. Qed. Lemma square_indiv_cons (p : list (Z * Z)) (a : Z * Z) : Associational.eval (sqr_indiv base (a :: p)) = Associational.eval (sqr_indiv base [a]) + Associational.eval (sqr_indiv base p). Proof using base_nz n_gt_1. + clear dependent s. cbv [sqr_indiv sqr_indiv']. cbn [fold_right]. push. @@ -2480,6 +2485,7 @@ Module SolinasReduction. Associational.eval (sqr_indiv base (p ++ q)) = Associational.eval (sqr_indiv base p) + Associational.eval (sqr_indiv base q). Proof using base_nz n_gt_1. + clear dependent s. generalize dependent q. induction p as [| a p IHp] using rev_ind; intros q. push. @@ -2497,6 +2503,7 @@ Module SolinasReduction. (Associational.eval (sat_mul base [(weight 2, x1)] [(weight 2, x1)]) + Associational.eval (sat_mul base [(weight 3, x2)] [(weight 3, x2)])))). Proof using base_nz wprops n_gt_1. + clear dependent s. intros x x0 x1 x2 q H. rewrite H. cbv [to_associational]. @@ -2519,6 +2526,7 @@ Module SolinasReduction. p = x :: x0 :: x1 :: x2 :: q -> length (square1 base (to_associational weight 4 p)) = 8%nat. Proof using base_nz wprops n_gt_1. + clear dependent s. intros x x0 x1 x2 q H. cbv [square1]. push. @@ -2547,6 +2555,7 @@ Module SolinasReduction. (Associational.eval (sat_mul base [(weight 3, x2)] [(weight 1, x0)]) + Associational.eval (sat_mul base [(weight 3, x2)] [(weight 2, x1)]))). Proof using base_nz wprops n_gt_1. + clear dependent s. intros x x0 x1 x2 q bound H H1. rewrite H1. cbv [to_associational]. @@ -2612,6 +2621,7 @@ Module SolinasReduction. p = x :: x0 :: x1 :: x2 :: q -> 0 <= eval weight 8 (square1 base (to_associational weight 4 p)) < weight 7. Proof using base_nz wprops n_gt_1. + clear dependent s. intros x x0 x1 x2 q bound H H0. erewrite eval_square1; [| eauto | eauto]. rewrite H0 in H. @@ -2635,6 +2645,7 @@ Module SolinasReduction. Theorem eval_square_no_reduce (p : list Z) : eval weight (2 * n) (square_no_reduce base n p) = (eval weight n p) * (eval weight n p). Proof using base_nz wprops n_gt_1. + clear dependent s. rewrite <-eval_mul_no_reduce with (base:=base) by lia. cbv [square_no_reduce]. break_match. @@ -2729,6 +2740,7 @@ Module SolinasReduction. Theorem length_square_no_reduce (p : list Z): length (square_no_reduce base n p) = (2 * n)%nat. Proof using base_nz wprops n_gt_1. + clear dependent s. cbv [square_no_reduce]. break_match. rewrite Nat.eqb_eq in Heqb. diff --git a/src/Arithmetic/WordByWordMontgomery.v b/src/Arithmetic/WordByWordMontgomery.v index 191f3593b3..173815f3ec 100644 --- a/src/Arithmetic/WordByWordMontgomery.v +++ b/src/Arithmetic/WordByWordMontgomery.v @@ -1020,11 +1020,12 @@ Module WordByWordMontgomery. Qed. Lemma sub_bound : 0 <= eval (sub Av Bv) < eval N. Proof using small_Bv small_Av R_numlimbs_nz Bv_bound Av_bound small_N r_big' partition_Proper lgr_big N_nz N_lt_R. + clear dependent ri; clear dependent k. generalize eval_sub; break_innermost_match; Z.ltb_to_lt; lia. Qed. Lemma opp_bound : 0 <= eval (opp Av) < eval N. Proof using small_Av R_numlimbs_nz Av_bound small_N r_big' partition_Proper lgr_big N_nz N_lt_R. - clear Bv small_Bv Bv_bound. + clear Bv small_Bv Bv_bound k k_correct ri ri_correct. generalize eval_opp; break_innermost_match; Z.ltb_to_lt; lia. Qed. End add_sub. diff --git a/src/Curves/TableMult/TableMult.v b/src/Curves/TableMult/TableMult.v index 1a2006fe90..7e682ae0ab 100644 --- a/src/Curves/TableMult/TableMult.v +++ b/src/Curves/TableMult/TableMult.v @@ -1243,7 +1243,7 @@ Section TableMult. intros. unfold positify. pose proof oddify_bounds e. - intuition. + intuition auto with core. - apply Z.div_pos; lia. - apply Z.div_lt_upper_bound; lia. Qed. diff --git a/src/Util/NumTheoryUtil.v b/src/Util/NumTheoryUtil.v index 88bb721812..641445b28d 100644 --- a/src/Util/NumTheoryUtil.v +++ b/src/Util/NumTheoryUtil.v @@ -58,6 +58,7 @@ Lemma x_nonneg: 0 <= x. Proof using prime_p x_id. clear -prime_p x_id. Z.prime_b Lemma x_id_inv : x = (p - 1) / 2. Proof using x_id. + clear neq_p_2. intros; apply Zeq_plus_swap in x_id. replace (p - 1) with (2 * ((p - 1) / 2)) in x_id by (symmetry; apply Z_div_exact_2; [lia | rewrite <- x_id; apply Z_mod_mult]). diff --git a/src/Util/SideConditions/Autosolve.v b/src/Util/SideConditions/Autosolve.v index 99a8db4964..8261465de7 100644 --- a/src/Util/SideConditions/Autosolve.v +++ b/src/Util/SideConditions/Autosolve.v @@ -1,17 +1,15 @@ Require Import Crypto.Util.Decidable. Require Import Crypto.Util.SideConditions.CorePackages. -Require Import Crypto.Util.SideConditions.ModInvPackage. Require Import Crypto.Util.SideConditions.ReductionPackages. Require Import Crypto.Util.SideConditions.RingPackage. Ltac autosolve_gen autosolve_tac ring_intros_tac else_tac := CorePackages.preautosolve (); CorePackages.Internal.autosolve ltac:(fun _ => - ModInvPackage.autosolve ltac:(fun _ => ReductionPackages.autosolve autosolve_tac ltac:(fun _ => RingPackage.autosolve_gen_intros ring_intros_tac ltac:(fun _ => CorePackages.autosolve else_tac - )))). + ))). Ltac autosolve_gen_intros ring_intros_tac else_tac := autosolve_gen ltac:(autosolve_gen_intros ring_intros_tac) ring_intros_tac else_tac. diff --git a/src/Util/SideConditions/ModInvPackage.v b/src/Util/SideConditions/ModInvPackage.v deleted file mode 100644 index 8aef3cb75e..0000000000 --- a/src/Util/SideConditions/ModInvPackage.v +++ /dev/null @@ -1,24 +0,0 @@ -Require Import Coq.ZArith.ZArith. -Require Import Crypto.Util.Option. -Require Import Crypto.Util.ZUtil.ModInv. -Require Import Crypto.Util.SideConditions.CorePackages. - -Local Open Scope Z_scope. - -Definition modinv_evar_package (modinv_fuel : nat) (a modulus : Z) - := evar_Prop_package - (fun a' => (a * a') mod modulus = 1). - -Ltac autosolve else_tac := - lazymatch goal with - | [ |- modinv_evar_package ?modinv_fuel ?a ?modulus ] - => let v0 := constr:(Option.invert_Some (Z.modinv_fueled modinv_fuel a modulus)) in - let v := (eval vm_compute in v0) in - let v := lazymatch type of v with (* if the computation failed, display a reasonable error message about the attempted computation *) - | Z => v - | _ => (eval cbv -[Option.invert_Some Z.modinv_fueled] in v0) - end in - let v := (eval vm_compute in (v <: Z)) in - (exists v); vm_compute; reflexivity - | _ => else_tac () - end. diff --git a/src/Util/ZUtil/ModInv.v b/src/Util/ZUtil/ModInv.v index fcff5c8e84..bad00b0c7b 100644 --- a/src/Util/ZUtil/ModInv.v +++ b/src/Util/ZUtil/ModInv.v @@ -23,408 +23,40 @@ Require Import Crypto.Util.Wf1. Local Open Scope Z_scope. Module Z. - (** Quoting https://stackoverflow.com/a/9758173: -<< -def egcd(a, b): - if a == 0: - return (b, 0, 1) - else: - g, y, x = egcd(b % a, a) - return (g, x - (b // a) * y, y) + Import Znumtheory. + Definition invmod a m := fst (fst (extgcd a m)) mod m. + Notation modinv := invmod (only parsing). -def modinv(a, m): - g, x, y = egcd(a, m) - if g != 1: - raise Exception('modular inverse does not exist') - else: - return x % m ->> *) - (** We run on fuel, because the well-foundedness lemmas for [Z] are - opaque, so we can't use them to compute. *) - Fixpoint egcd (fuel : nat) (a b : Z) : option (Z * Z * Z) - := match fuel with - | O => None - | S fuel' - => if a Some (g, x - (b / a) * y, y) - | None => None - end - end. - Definition egcd_by_wf_step (a : Z) (egcd : forall y : Z, 0 <= y < a -> Z -> option (Z * Z * Z)) (b : Z) : option (Z * Z * Z) - := (if (0 _) - then fun pf - => match @egcd (b mod a) (Z.mod_pos_bound _ _ (proj1 (Z.ltb_lt _ _) ltac:(eassumption))) a with - | Some (g, y, x) => Some (g, x - (b / a) * y, y) - | None => None - end - else fun _ - => if a =? 0 - then Some (b, 0, 1) - else None) eq_refl. - Definition egcd_by_wf (wf : well_founded (fun x y => 0 <= x < y)) (a b : Z) : option (Z * Z * Z) - := Fix wf (fun _ => Z -> option (Z * Z * Z)) egcd_by_wf_step a b. - Definition modinv_of_egcd (egcd : Z -> Z -> option (Z * Z * Z)) (a m : Z) : option Z - := if a if negb (g =? 1) - then None - else Some ((-x) mod m) - | None => None - end - else match egcd a m with - | Some (g, x, y) - => if negb (g =? 1) - then None - else Some (x mod m) - | None => None - end. - Definition modinv_fueled (fuel : nat) (a m : Z) : option Z - := modinv_of_egcd (egcd fuel) a m. - Definition modinv_by_wf (wf : well_founded (fun x y => 0 <= x < y)) (a m : Z) : option Z - := modinv_of_egcd (egcd_by_wf wf) a m. - Definition modinv_by_wf_fuel (fuel : nat) (a m : Z) : option Z - := modinv_by_wf (Acc_intro_generator fuel (Z.lt_wf 0)) a m. - (** We way over-estimate the fuel by taking [max a m]. We can assume - that [Z.to_nat (Z.log2_up (max a m))] is fast, because we already - have a ~unary representation of [Z.log2_up a] and [Z.log2_up m]. It is - empirically the case that pulling successors off [2^k] is fast, so - we can use that for fuel. *) - Definition modinv' (a m : Z) : option Z - := modinv_fueled (S (2^Z.to_nat (Z.log2_up (Z.max (Z.abs a) m)))) a m. - (** For the actual version, which we want to perform well under - [cbv], we will simply add the log2 representations of [a] and - [m]. We expect to pull at least about 1 bit off the top each - round of the gcd calculation. *) - Definition modinv_opt (a m : Z) : option Z - := modinv_by_wf (Acc_intro_generator (S (S (Z.to_nat (Z.log2_up (Z.abs a) + Z.log2_up (Z.abs m))))) (Z.lt_wf 0)) a m. - Definition modinv (a m : Z) : Z - := Option.value (modinv_opt a m) 0. + Lemma invmod_0_l m : invmod 0 m = 0. Proof. reflexivity. Qed. - Lemma egcd_by_wf_step_ext x f g (Hext : forall (y : Z) (p : 0 <= y < x) (a : Z), f y p a = g y p a) - : forall a, egcd_by_wf_step x f a = egcd_by_wf_step x g a. + Lemma invmod_ok a m (Hm : m <> 0) : invmod a m * a mod m = Z.gcd a m mod m. Proof. - cbv [egcd_by_wf_step]. - repeat first [ progress intros - | progress subst - | reflexivity - | progress Z.ltb_to_lt - | progress inversion_option - | progress inversion_prod - | break_innermost_match_step - | exfalso; lia - | match goal with - | [ H1 : ?x = ?y :> bool, H2 : ?x = ?y :> bool |- _ ] - => assert (H1 = H2) by (apply UIP_dec; decide equality); subst H2 - | [ H : forall y p a, ?f y p a = ?g y p a, H1 : ?f _ _ _ = _, H2 : ?g _ _ _ = _ |- _ ] - => rewrite H in H1; rewrite H1 in H2; clear H1 - | [ H : context[proj1 (Z.ltb_lt ?x ?y) ?v] |- _ ] - => generalize dependent (proj1 (Z.ltb_lt x y) v); clear v; intros - end ]. + cbv [invmod]; destruct extgcd as [[u v]g] eqn:H. + eapply extgcd_correct in H; case H as [[]]; subst; cbn [fst snd]. + rewrite Z.mul_mod_idemp_l by trivial. + erewrite <-Z.mod_add, H; trivial. Qed. - Lemma egcd_by_wf_None : forall wf a b, egcd_by_wf wf a b = None -> a < 0. - Proof. - intros wf a b. - cbv [egcd_by_wf]. - apply (@Fix1_rect _ _ _ wf _ egcd_by_wf_step); [ | now apply egcd_by_wf_step_ext ]. - generalize (Fix wf _ egcd_by_wf_step); cbv [egcd_by_wf_step]; intro egcd. - repeat first [ progress intros - | progress break_innermost_match_hyps - | progress Z.ltb_to_lt - | assumption - | congruence - | lia - | match goal with - | [ H : forall y, _ -> forall a, egcd y a = _ -> y < 0, H' : egcd ?v1 ?v2 = _ |- _ ] - => specialize (fun pf => H v1 pf v2 H'); Z.div_mod_to_quot_rem; nia - end ]. - Qed. - - Lemma egcd_by_wf_bezout : forall wf a b g x y, egcd_by_wf wf a b = Some (g, x, y) -> Z.abs g = Z.gcd a b /\ (0 <= a -> 0 <= b -> 0 <= g) /\ x * a + y * b = g. - Proof. - intros wf a b. - cbv [egcd_by_wf]. - apply (@Fix1_rect _ _ _ wf _ egcd_by_wf_step); [ | now apply egcd_by_wf_step_ext ]. - generalize (Fix wf _ egcd_by_wf_step); cbv [egcd_by_wf_step]; intro egcd. - repeat first [ progress intros - | progress break_innermost_match_hyps - | progress Z.ltb_to_lt - | progress inversion_option - | progress inversion_prod - | progress destruct_head'_and - | progress subst - | progress rewrite ?Z.gcd_mod in * by lia - | rewrite Z.gcd_0_r - | rewrite Z.gcd_0_l - | apply Z.gcd_0_l - | lia - | match goal with - | [ H : forall y, _ -> forall a g x' y', egcd y a = _ -> _, H' : egcd ?v1 ?v2 = _ |- _ ] - => specialize (fun pf => H _ pf _ _ _ _ H'); try specialize (H ltac:(Z.div_mod_to_quot_rem; nia)) - end - | Z.div_mod_to_quot_rem; nia - | apply conj ]. - Qed. - - Lemma egcd_bezout : forall fuel a b g x y, egcd fuel a b = Some (g, x, y) -> Z.abs g = Z.gcd a b /\ (0 <= a -> 0 <= b -> 0 <= g) /\ x * a + y * b = g. - Proof. - induction fuel as [|fuel IH]; cbn [egcd]; [ congruence | ]. - repeat first [ progress intros - | progress break_innermost_match_hyps - | progress Z.ltb_to_lt - | progress inversion_option - | progress inversion_prod - | progress destruct_head'_and - | progress subst - | progress rewrite ?Z.gcd_mod in * by lia - | apply Z.gcd_0_l - | lia - | match goal with - | [ H : forall _ _ _ _ _, egcd _ _ _ = _ -> _, H' : egcd _ _ _ = _ |- _ ] - => specialize (H _ _ _ _ _ H'); try specialize (H ltac:(Z.div_mod_to_quot_rem; nia)) - end - | Z.div_mod_to_quot_rem; nia - | apply conj ]. - Qed. - - Lemma egcd_None : forall fuel a b, Z.egcd fuel a b = None -> (fuel <= (if b x))%Z (Z.to_nat (Z.min a b)))%nat \/ a < 0 \/ b < 0. - Proof. - induction fuel as [|fuel IH]; cbn; [ intros; break_innermost_match; lia | ]. - intros; break_innermost_match_hyps; Z.ltb_to_lt; auto; try congruence. - specialize (IH _ _ ltac:(eassumption)). - destruct_head'_or; [ | solve [ auto | exfalso; Z.div_mod_to_quot_rem; nia ] .. ]. - destruct (Z_lt_dec b 0); auto; []. - left. - rewrite Z.min_l in * |- by (Z.div_mod_to_quot_rem; nia). - break_innermost_match_hyps; break_innermost_match; Z.ltb_to_lt; rewrite ?Z.min_r, ?Z.min_l by lia; - try (Z.div_mod_to_quot_rem; zify; rewrite ?Z2Nat.id in * by lia; lia); []. - Z.rewrite_mod_small_in_all; lia. - Qed. - - Lemma modinv_of_egcd_None egcd P a m - (Hegcd_None : forall a b, egcd a b = None -> P a b \/ a < 0 \/ b < 0) - (Hegcd_Some : forall a b g x y, egcd a b = Some (g, x, y) -> Z.abs g = Z.gcd a b /\ (0 <= a -> 0 <= b -> 0 <= g) /\ x * a + y * b = g) - : modinv_of_egcd egcd a m = None -> P (Z.abs a) m \/ m < 0 \/ Z.gcd (Z.abs a) m <> 1. - Proof. - destruct (Z_lt_dec m 0); [ now auto | ]. - cbv [modinv_of_egcd]; break_innermost_match; rewrite ?Bool.negb_true_iff in *; Z.ltb_to_lt. - all: lazymatch goal with - | [ Hegcd_Some : forall a b g x y, ?egcd a b = Some _ -> _, Hedgc_None : forall a b, ?egcd a b = None -> _, H : ?egcd _ _ = _ |- _ ] - => first [ apply Hegcd_Some in H | apply Hegcd_None in H ]; clear Hegcd_None Hegcd_Some - end. - all: repeat first [ progress intros - | progress Z.replace_all_neg_with_pos - | progress destruct_head'_and - | progress destruct_head'_or - | progress break_innermost_match_hyps - | progress Z.ltb_to_lt - | progress rewrite Z.abs_opp in * - | progress rewrite ?Z.abs_eq in * by nia - | progress subst - | progress specialize_by lia - | congruence - | solve [ auto ] - | exfalso; lia ]. - Qed. - - Lemma bezout_modinv a m x y - (Hbezout : x * a + y * m = 1) - : (a * x) mod m = 1 mod m. - Proof. - replace (a * x) with (1 - (y * m)) by lia. - push_Zmod; autorewrite with zsimplify_fast; reflexivity. - Qed. + Lemma invmod_coprime' a m (Hm : m <> 0) (H : Z.gcd a m = 1) : invmod a m * a mod m = 1 mod m. + Proof. rewrite invmod_ok, H; trivial. Qed. - Lemma bezout_modinv_rev a m x - (Hm : 0 < m) - (H : (a * x) mod m = 1 mod m) - : exists y, x * a + y * m = 1. - Proof. - exists ((1 - a * x) / m). - assert ((1 - a * x) mod m = 0) - by (revert H; push_Zmod; intro H; rewrite H; autorewrite with zsimplify_const; reflexivity). - Z.div_mod_to_quot_rem; nia. - Qed. + Lemma invmod_coprime a m (Hm : 2 <= m) (H : Z.gcd a m = 1) : invmod a m * a mod m = 1. + Proof. rewrite invmod_coprime', Z.mod_1_l; trivial. Admitted. - Lemma modinv_of_egcd_Some egcd P a m - (Hegcd_None : forall a b, egcd a b = None -> P a b \/ a < 0 \/ b < 0) - (Hegcd_Some : forall a b g x y, egcd a b = Some (g, x, y) -> Z.abs g = Z.gcd a b /\ (0 <= a -> 0 <= b -> 0 <= g) /\ x * a + y * b = g) - (Hm : 0 < m) - : forall a', modinv_of_egcd egcd a m = Some a' -> (a * a') mod m = 1 mod m /\ 0 <= a' < m. + Lemma invmod_prime a m (Hm : prime m) (H : a mod m <> 0) : invmod a m * a mod m = 1. Proof. - cbv [modinv_of_egcd]; break_innermost_match; rewrite ?Bool.negb_true_iff in *; Z.ltb_to_lt. - all: lazymatch goal with - | [ Hegcd_Some : forall a b g x y, ?egcd a b = Some _ -> _, Hedgc_None : forall a b, ?egcd a b = None -> _, H : ?egcd _ _ = _ |- _ ] - => first [ apply Hegcd_Some in H | apply Hegcd_None in H ]; clear Hegcd_None Hegcd_Some - end. - all: repeat first [ progress intros - | progress Z.replace_all_neg_with_pos - | progress destruct_head'_and - | progress destruct_head'_or - | progress break_innermost_match_hyps - | progress rewrite ?Bool.negb_true_iff in * - | progress rewrite ?Bool.negb_false_iff in * - | progress Z.ltb_to_lt - | progress rewrite Z.abs_opp in * - | progress rewrite ?Z.abs_eq in * by nia - | rewrite Z.mul_opp_r - | rewrite Z.opp_involutive - | progress subst - | progress specialize_by lia - | progress inversion_option - | congruence - | solve [ auto ] - | exfalso; lia - | apply conj - | Z.div_mod_to_quot_rem; nia - | progress (push_Zmod; pull_Zmod) ]. - all: generalize dependent (Z.gcd a m); intros; subst; erewrite bezout_modinv by eassumption; reflexivity. + pose proof prime_ge_2 _ Hm as Hm'. + rewrite Z.mod_divide in H (* by lia *) by (intro; subst m; auto using not_prime_0). + apply invmod_coprime, Zgcd_1_rel_prime, rel_prime_sym, prime_rel_prime; auto. Qed. - Lemma modinv_of_egcd_Some_rev egcd P a m - (Hegcd_None : forall a b, egcd a b = None -> P a b \/ a < 0 \/ b < 0) - (Hegcd_Some : forall a b g x y, egcd a b = Some (g, x, y) -> Z.abs g = Z.gcd a b /\ (0 <= a -> 0 <= b -> 0 <= g) /\ x * a + y * b = g) - (Hm : 0 < m) - : ~P (Z.abs a) m -> forall a', (a * a') mod m = 1 mod m -> modinv_of_egcd egcd a m <> None. - Proof. - intros nP a' Ha'. - apply bezout_modinv_rev in Ha'; [ | assumption ]; destruct Ha' as [? Ha']. - destruct (modinv_of_egcd egcd a m) eqn:H; [ eapply modinv_of_egcd_Some in H | eapply modinv_of_egcd_None in H ]; - try eassumption; [ try congruence | exfalso ]. - all: repeat first [ progress destruct_head'_and - | progress destruct_head'_or - | tauto - | lia - | rewrite <- ?Z.mul_assoc, ?(Z.mul_comm (Z.sgn _) (Z.abs _)), Z.abs_sgn - | match goal with - | [ H : Z.gcd (Z.abs ?a) ?b <> 1, H' : ?x * ?a + ?y * ?b = 1 |- False ] - => apply H, Z.bezout_1_gcd; clear H; exists (x * Z.sgn a), y; rewrite <- H'; clear - end ]. - Qed. - - Lemma modinv_fueled_None fuel a m - : modinv_fueled fuel a m = None -> (fuel <= (if m x))%Z (Z.to_nat (Z.min (Z.abs a) m)))%nat \/ m < 0 \/ Z.gcd (Z.abs a) m <> 1. - Proof. now apply (modinv_of_egcd_None (egcd fuel) _ a m (egcd_None fuel) (egcd_bezout fuel)). Qed. - Lemma modinv_fueled_Some fuel a m - (Hm : 0 < m) - : forall a', modinv_fueled fuel a m = Some a' -> (a * a') mod m = 1 mod m /\ 0 <= a' < m. - Proof. now apply (modinv_of_egcd_Some (egcd fuel) _ a m (egcd_None fuel) (egcd_bezout fuel)). Qed. - Lemma modinv_fueled_Some_rev fuel a m - (Hm : 0 < m) - : ~(fuel <= (if m x))%Z (Z.to_nat (Z.min (Z.abs a) m)))%nat -> forall a', (a * a') mod m = 1 mod m -> modinv_fueled fuel a m <> None. - Proof. now apply (modinv_of_egcd_Some_rev (egcd fuel) _ a m (egcd_None fuel) (egcd_bezout fuel)). Qed. - - Lemma modinv_by_wf_None wf a m - : modinv_by_wf wf a m = None -> m < 0 \/ Z.gcd (Z.abs a) m <> 1. - Proof. - intro. - pose proof (egcd_by_wf_None wf). - pose proof (egcd_by_wf_bezout wf). - destruct (modinv_of_egcd_None (egcd_by_wf wf) (fun _ _ => False) a m). - all: cbv beta in *. - all: intuition eauto. - Qed. - Lemma modinv_by_wf_Some wf a m - (Hm : 0 < m) - : forall a', modinv_by_wf wf a m = Some a' -> (a * a') mod m = 1 mod m /\ 0 <= a' < m. - Proof. - pose proof (egcd_by_wf_None wf). - pose proof (egcd_by_wf_bezout wf). - apply (modinv_of_egcd_Some (egcd_by_wf wf) (fun _ _ => False) a m). - all: cbv beta in *. - all: intuition eauto. - Qed. - Lemma modinv_by_wf_Some_rev wf a m - (Hm : 0 < m) - : forall a', (a * a') mod m = 1 mod m -> modinv_by_wf wf a m <> None. - Proof. - pose proof (egcd_by_wf_None wf). - pose proof (egcd_by_wf_bezout wf). - apply (modinv_of_egcd_Some_rev (egcd_by_wf wf) (fun _ _ => False) a m). - all: cbv beta in *. - all: intuition eauto. - Qed. - - Lemma modinv_by_wf_fuel_None fuel a m - : modinv_by_wf_fuel fuel a m = None -> m < 0 \/ Z.gcd (Z.abs a) m <> 1. - Proof. now apply modinv_by_wf_None. Qed. - Lemma modinv_by_wf_fuel_Some fuel a m (Hm : 0 < m) - : forall a', modinv_by_wf_fuel fuel a m = Some a' -> (a * a') mod m = 1 mod m /\ 0 <= a' < m. - Proof. now apply modinv_by_wf_Some. Qed. - Lemma modinv_by_wf_fuel_Some_rev fuel a m (Hm : 0 < m) - : forall a', (a * a') mod m = 1 mod m -> modinv_by_wf_fuel fuel a m <> None. - Proof. now apply modinv_by_wf_Some_rev. Qed. - - Lemma modinv'_fuel_good a m - : ((if (m x) (Z.to_nat (Z.min (Z.abs a) m)) < S (2 ^ Z.to_nat (Z.log2_up (Z.max (Z.abs a) m))))%nat. - Proof. - assert (0 <= Z.log2_up (if Z_lt_dec a 0 then -a else a)) by auto with zarith. - assert (0 <= Z.log2_up m) by auto with zarith. - destruct (Z_lt_dec a 0), (Z_zerop a), (Z_lt_dec m 0); subst; Z.replace_all_neg_with_pos; rewrite ?Z.abs_opp, ?Z.abs_eq in * by lia. - all: break_innermost_match; Z.ltb_to_lt. - all: repeat first [ rewrite Z.min_l by lia - | rewrite Z.min_r by lia - | rewrite Z.max_l by lia - | rewrite Z.max_r by lia - | exfalso; lia - | lia - | progress change ((2^Z.to_nat (Z.log2_up 0))%nat) with 1%nat - | match goal with - | [ |- context[Z.to_nat ?x] ] => rewrite (Z2Nat.inj_nonpos x) by lia - end ]. - all: change 2%nat with (Z.to_nat 2). - all: eapply Nat.lt_le_trans; - [ - | apply le_n_S; zify; set_evars; autorewrite with push_Zof_nat; rewrite ?Z2Nat.id by lia; subst_evars; - etransitivity; [ | apply Z.log2_log2_up_spec; change (2^Z.log2 1) with 1 in *; zify; rewrite ?Z2Nat.id by lia; lia ]; - rewrite Z2Nat.id; [ reflexivity | change (2^Z.log2 1) with 1 in *; zify; rewrite ?Z2Nat.id by lia; lia ] ]. - all: zify; rewrite ?Z2Nat.id by lia; lia. - Qed. - - Lemma modinv'_None a m - : modinv' a m = None -> m < 0 \/ Z.gcd (Z.abs a) m <> 1. - Proof. - intro H. - pose proof (modinv'_fuel_good a m). - pose proof (modinv_fueled_None _ a m H); destruct_head'_or; auto; try (exfalso; lia). - Qed. - Lemma modinv'_Some a m (Hm : 0 < m) - : forall a', modinv' a m = Some a' -> (a * a') mod m = 1 mod m /\ 0 <= a' < m. - Proof. now apply modinv_fueled_Some. Qed. - Lemma modinv'_Some_rev a m (Hm : 0 < m) - : forall a', (a * a') mod m = 1 mod m -> modinv' a m <> None. - Proof. - pose proof (modinv'_fuel_good a m). - apply modinv_fueled_Some_rev; try assumption; lia. - Qed. - - Lemma modinv_opt_None a m - : modinv_opt a m = None -> m < 0 \/ Z.gcd (Z.abs a) m <> 1. - Proof. apply modinv_by_wf_None. Qed. - Lemma modinv_opt_Some a m (Hm : 0 < m) - : forall a', modinv_opt a m = Some a' -> (a * a') mod m = 1 mod m /\ 0 <= a' < m. - Proof. now apply modinv_by_wf_Some. Qed. - Lemma modinv_opt_Some_rev a m (Hm : 0 < m) - : forall a', (a * a') mod m = 1 mod m -> modinv_opt a m <> None. - Proof. now apply modinv_by_wf_Some_rev. Qed. - Lemma modinv_correct a m (Hm : 0 < m) (Hgcd : Z.gcd (Z.abs a) m = 1) : (a * modinv a m) mod m = 1 mod m /\ 0 <= modinv a m < m. Proof. - pose proof (modinv_opt_None a m) as H0. - pose proof (modinv_opt_Some a m Hm) as H1. - pose proof (modinv_opt_Some_rev a m Hm) as H2. - cbv [modinv]; edestruct modinv_opt. - { now apply H1. } - { specialize (H0 eq_refl). - exfalso; lia. } + rewrite Z.gcd_abs_l in Hgcd. + rewrite Z.mul_comm, invmod_coprime'; + cbv [invmod]; repeat split; try (Z.div_mod_to_equations; lia). Qed. End Z.