diff options
Diffstat (limited to 'src')
24 files changed, 677 insertions, 1494 deletions
diff --git a/src/Algebra.v b/src/Algebra.v index 9bd3cac5e..adbf5b86b 100644 --- a/src/Algebra.v +++ b/src/Algebra.v @@ -12,17 +12,10 @@ Module Import ModuloCoq8485. Infix "mod" := modulo. End ModuloCoq8485. -Notation is_eq_dec := (DecidableRel _) (only parsing). -Notation "@ 'is_eq_dec' T R" := (DecidableRel (R:T->T->Prop)) (only parsing). -Notation eq_dec x y := (@dec (_ x y) _) (only parsing). -Notation "x =? y" := (eq_dec x y) : type_scope. - Section Algebra. Context {T:Type} {eq:T->T->Prop}. Local Infix "=" := eq : type_scope. Local Notation "a <> b" := (not (a = b)) : type_scope. - Local Notation is_eq_dec := (@is_eq_dec T eq). - Section SingleOperation. Context {op:T->T->T}. @@ -41,7 +34,7 @@ Section Algebra. monoid_op_Proper: Proper (respectful eq (respectful eq eq)) op; monoid_Equivalence : Equivalence eq; - monoid_is_eq_dec : is_eq_dec + monoid_is_eq_dec : DecidableRel eq }. Global Existing Instance monoid_is_associative. Global Existing Instance monoid_is_left_identity. @@ -364,6 +357,23 @@ Module ScalarMult. Global Existing Instance scalarmult_Proper. Context `{is_scalarmult}. + Fixpoint scalarmult_ref (n:nat) (P:G) {struct n} := + match n with + | O => zero + | S n' => add P (scalarmult_ref n' P) + end. + + Global Instance Proper_scalarmult_ref : Proper (Logic.eq==>eq==>eq) scalarmult_ref. + Proof. + repeat intro; subst. + match goal with [n:nat |- _ ] => induction n; simpl @scalarmult_ref; [reflexivity|] end. + repeat match goal with [H:_ |- _ ] => rewrite H end; reflexivity. + Qed. + + Lemma scalarmult_ext : forall n P, mul n P = scalarmult_ref n P. + induction n; simpl @scalarmult_ref; intros; rewrite <-?IHn; (apply scalarmult_0_l || apply scalarmult_S_l). + Qed. + Lemma scalarmult_1_l : forall P, 1*P = P. Proof. intros. rewrite scalarmult_S_l, scalarmult_0_l, right_identity; reflexivity. Qed. @@ -402,6 +412,10 @@ Module ScalarMult. rewrite scalarmult_add_l, scalarmult_1_l, Group.inv_op, scalarmult_S_l, Group.cancel_left; eauto. } Qed. End ScalarMultProperties. + + Global Instance scalarmult_ref_is_scalarmult {G eq add zero} `{@monoid G eq add zero} + : @is_scalarmult G eq add zero (@scalarmult_ref G add zero). + Proof. split; try exact _; intros; reflexivity. Qed. End ScalarMult. Require Coq.nsatz.Nsatz. @@ -588,7 +602,7 @@ Module IntegralDomain. : eq (mul x y) zero -> eq x zero \/ eq y zero. Proof. pose proof mul_nonzero_nonzero x y. - destruct (eq_dec x zero); destruct (eq_dec y zero); intuition. + destruct (dec (eq x zero)); destruct (dec (eq y zero)); intuition. Qed. Lemma mul_nonzero_nonzero_iff (x y : T) @@ -663,7 +677,7 @@ Module Field. Lemma isomorphism_to_subfield_field {T EQ ZERO ONE OPP ADD SUB MUL INV DIV} - {Equivalence_EQ: @Equivalence T EQ} {eq_dec: forall x y, {EQ x y} + {~ EQ x y} } + {Equivalence_EQ: @Equivalence T EQ} {eq_dec: DecidableRel EQ} {Proper_OPP:Proper(EQ==>EQ)OPP} {Proper_ADD:Proper(EQ==>EQ==>EQ)ADD} {Proper_SUB:Proper(EQ==>EQ==>EQ)SUB} @@ -673,7 +687,7 @@ Module Field. {R eq zero one opp add sub mul inv div} {fieldR:@field R eq zero one opp add sub mul inv div} {phi} {eq_phi_EQ: forall x y, eq (phi x) (phi y) -> EQ x y} - {neq_zero_one : (EQ ZERO ONE -> False)} + {neq_zero_one : (not (EQ ZERO ONE))} {phi_opp : forall a, eq (phi (OPP a)) (opp (phi a))} {phi_add : forall a b, eq (phi (ADD a b)) (add (phi a) (phi b))} {phi_sub : forall a b, eq (phi (SUB a b)) (sub (phi a) (phi b))} @@ -753,7 +767,7 @@ Module Field. -> phi (INV x) = inv (phi x). Proof. intros. - destruct (eq_dec x ZERO); auto. + destruct (dec (EQ x ZERO)); auto. assert (phi (MUL (INV x) x) = one) as A. { rewrite left_multiplicative_inverse; auto using Ring.homomorphism_one. } @@ -1223,8 +1237,8 @@ Section ExtraLemmas. Lemma only_two_square_roots'_choice x y : x * x = y * y -> x = y \/ x = opp y. Proof. intro H. - destruct (eq_dec x y); [ left; assumption | right ]. - destruct (eq_dec x (opp y)); [ assumption | exfalso ]. + destruct (dec (eq x y)); [ left; assumption | right ]. + destruct (dec (eq x (opp y))); [ assumption | exfalso ]. eapply only_two_square_roots'; eassumption. Qed. diff --git a/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v b/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v index 716d72b3e..4a443fd77 100644 --- a/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v +++ b/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v @@ -1,6 +1,6 @@ Require Export Crypto.Spec.CompleteEdwardsCurve. -Require Import Crypto.Algebra Crypto.Algebra. +Require Import Crypto.Algebra Crypto.Algebra Crypto.Util.Decidable. Require Import Crypto.CompleteEdwardsCurve.Pre. Require Import Coq.Logic.Eqdep_dec. Require Import Crypto.Tactics.VerdiTactics. @@ -115,7 +115,7 @@ Module E. Proof. intros ? eq_zero. destruct square_a as [sqrt_a sqrt_a_id]; rewrite <- sqrt_a_id in eq_zero. - destruct (eq_dec y 0); [apply nonzero_a | apply nonsquare_d with (sqrt_a/y)]; super_nsatz. + destruct (dec (y=0)); [apply nonzero_a | apply nonsquare_d with (sqrt_a/y)]; super_nsatz. Qed. Lemma solve_correct : forall x y, onCurve (x, y) <-> (x^2 = solve_for_x2 y). diff --git a/src/CompleteEdwardsCurve/Pre.v b/src/CompleteEdwardsCurve/Pre.v index 76dd97c72..705597e15 100644 --- a/src/CompleteEdwardsCurve/Pre.v +++ b/src/CompleteEdwardsCurve/Pre.v @@ -1,6 +1,6 @@ Require Import Coq.Classes.Morphisms. Require Coq.Setoids.Setoid. Require Import Crypto.Algebra Crypto.Algebra. -Require Import Crypto.Util.Notations. +Require Import Crypto.Util.Notations Crypto.Util.Decidable. Generalizable All Variables. Section Pre. @@ -44,7 +44,7 @@ Section Pre. (d*x1*x2*y1*y2)^2 <> 1. Proof. unfold onCurve, not; use_sqrt_a; intros. - destruct (eq_dec (sqrt_a*x2 + y2) 0); destruct (eq_dec (sqrt_a*x2 - y2) 0); + destruct (dec ((sqrt_a*x2 + y2) = 0)); destruct (dec ((sqrt_a*x2 - y2) = 0)); lazymatch goal with | [H: not (eq (?f (sqrt_a * x2) y2) 0) |- _ ] => apply d_nonsquare with (sqrt_d:= (f (sqrt_a * x1) (d * x1 * x2 * y1 * y2 * y1)) diff --git a/src/Encoding/ModularWordEncodingPre.v b/src/Encoding/ModularWordEncodingPre.v index 417344b43..aea22f4f5 100644 --- a/src/Encoding/ModularWordEncodingPre.v +++ b/src/Encoding/ModularWordEncodingPre.v @@ -16,18 +16,18 @@ Section ModularWordEncodingPre. Let Fm_dec (x_ : word sz) : option (F m) := let z := Z.of_N (wordToN (x_)) in if Z_lt_dec z m - then Some (ZToField z) + then Some (ZToField _ z) else None . Lemma Fm_encoding_valid : forall x, Fm_dec (Fm_enc x) = Some x. Proof. unfold Fm_dec, Fm_enc; intros. - pose proof (FieldToZ_range x m_pos). + pose proof (Zmod.FieldToZ_range x m_pos). rewrite wordToN_NToWord_idempotent by (apply bound_check_nat_N; assert (Z.to_nat x < Z.to_nat m) by (apply Z2Nat.inj_lt; omega); omega). rewrite Z2N.id by omega. - rewrite ZToField_idempotent. + rewrite Zmod.ZToField_FieldToZ. break_if; auto; omega. Qed. @@ -36,7 +36,7 @@ Section ModularWordEncodingPre. unfold Fm_dec, Fm_enc; intros ? ? dec_Some. break_if; [ | congruence ]. inversion dec_Some. - rewrite FieldToZ_ZToField. + rewrite Zmod.FieldToZ_ZToField. rewrite Z.mod_small by (pose proof (N2Z.is_nonneg (wordToN w)); try omega). rewrite N2Z.id. apply NToWord_wordToN. diff --git a/src/Encoding/ModularWordEncodingTheorems.v b/src/Encoding/ModularWordEncodingTheorems.v index 033e99665..03f98b2ca 100644 --- a/src/Encoding/ModularWordEncodingTheorems.v +++ b/src/Encoding/ModularWordEncodingTheorems.v @@ -3,7 +3,7 @@ Require Import Coq.Numbers.Natural.Peano.NPeano. Require Import Crypto.CompleteEdwardsCurve.CompleteEdwardsCurveTheorems. Require Import Crypto.ModularArithmetic.PrimeFieldTheorems Crypto.ModularArithmetic.ModularArithmeticTheorems. Require Import Bedrock.Word. -Require Import Crypto.Tactics.VerdiTactics. +Require Import Crypto.Tactics.VerdiTactics Crypto.Util.Tactics. Require Import Crypto.Spec.Encoding. Require Import Crypto.Util.ZUtil. Require Import Crypto.Spec.ModularWordEncoding. @@ -24,7 +24,7 @@ Section SignBit. assert (m < 1)%Z by (apply Z2Nat.inj_lt; try omega; assumption). omega. + assert (0 < m)%Z as m_pos by (pose proof prime_ge_2 m prime_m; omega). - pose proof (FieldToZ_range x m_pos). + pose proof (Zmod.FieldToZ_range x m_pos). destruct (FieldToZ x); auto. - destruct p; auto. - pose proof (Pos2Z.neg_is_neg p); omega. @@ -35,20 +35,13 @@ Section SignBit. rewrite sign_bit_parity; auto. Qed. - Lemma sign_bit_opp : forall (x : F m), x <> 0 -> negb (@sign_bit m sz x) = @sign_bit m sz (opp x). + Lemma odd_m : Z.odd m = true. Admitted. + + Lemma sign_bit_opp (x : F m) (Hnz:x <> 0) : negb (@sign_bit m sz x) = @sign_bit m sz (opp x). Proof. - intros. - pose proof sign_bit_zero as sign_zero. - rewrite !sign_bit_parity in *. - pose proof (F_opp_spec x) as opp_spec_x. - apply F_eq in opp_spec_x. - rewrite FieldToZ_add in opp_spec_x. - rewrite <-opp_spec_x, Z.odd_mod in sign_zero by (pose proof prime_ge_2 m prime_m; omega). - replace (Z.odd m) with true in sign_zero by (destruct (Z.prime_odd_or_2 m prime_m); auto || omega). - rewrite Z.odd_add, F_FieldToZ_add_opp, Z.div_same, Bool.xorb_true_r in sign_zero by assumption || omega. - apply Bool.xorb_eq. - rewrite <-Bool.negb_xorb_l. - assumption. + pose proof Zmod.FieldToZ_nonzero_range x Hnz; specialize_by omega. + rewrite !sign_bit_parity, Zmod.FieldToZ_opp, Z_mod_nz_opp_full, + Zmod_small, Z.odd_sub, odd_m, (Bool.xorb_true_l (Z.odd x)) by + (omega || rewrite Zmod_small by omega; auto using Zmod.FieldToZ_nonzero); trivial. Qed. - End SignBit. diff --git a/src/Experiments/DerivationsOptionRectLetInEncoding.v b/src/Experiments/DerivationsOptionRectLetInEncoding.v index 3ae1daa75..de5e0191f 100644 --- a/src/Experiments/DerivationsOptionRectLetInEncoding.v +++ b/src/Experiments/DerivationsOptionRectLetInEncoding.v @@ -267,7 +267,7 @@ Lemma unfoldDiv : forall {m} (x y:F m), (x/y = x * inv y)%F. Proof. unfold div. Definition FieldToN {m} (x:F m) := Z.to_N (FieldToZ x). Lemma FieldToN_correct {m} (x:F m) : FieldToN (m:=m) x = Z.to_N (FieldToZ x). reflexivity. Qed. -Definition natToField {m} x : F m := ZToField (Z.of_nat x). +Definition natToField {m} x : F m := ZToField _ (Z.of_nat x). Definition FieldToNat {m} (x:F m) : nat := Z.to_nat (FieldToZ x). Section with_unqualified_modulo2. @@ -275,11 +275,6 @@ Import NPeano Nat. Local Infix "mod" := modulo : nat_scope. Lemma FieldToNat_natToField {m} : m <> 0 -> forall x, x mod m = FieldToNat (natToField (m:=Z.of_nat m) x). unfold natToField, FieldToNat; intros. - rewrite (FieldToZ_ZToField), <-mod_Zmod, Nat2Z.id; trivial. -Qed. -End with_unqualified_modulo2. - -Lemma F_eqb_iff {q} : forall x y : F q, F_eqb x y = true <-> x = y. -Proof. - split; eauto using F_eqb_eq, F_eqb_complete. + rewrite (Zmod.FieldToZ_ZToField), <-mod_Zmod, Nat2Z.id; trivial. Qed. +End with_unqualified_modulo2.
\ No newline at end of file diff --git a/src/Experiments/SpecEd25519.v b/src/Experiments/SpecEd25519.v index f107e4497..6d6de9dcb 100644 --- a/src/Experiments/SpecEd25519.v +++ b/src/Experiments/SpecEd25519.v @@ -8,44 +8,43 @@ Require Import Crypto.ModularArithmetic.PrimeFieldTheorems Crypto.ModularArithme Require Import Crypto.Util.NatUtil Crypto.Util.ZUtil Crypto.Util.WordUtil Crypto.Util.NumTheoryUtil. Require Import Bedrock.Word. Require Import Crypto.Tactics.VerdiTactics. -Require Import Coq.Logic.Decidable. +Require Import Coq.Logic.Decidable Crypto.Util.Decidable. Require Import Coq.omega.Omega. (* TODO: move to PrimeFieldTheorems *) -Lemma minus1_is_square {q} : prime q -> (q mod 4)%Z = 1%Z -> isSquare (opp 1 : F q)%F. +Lemma minus1_is_square {q} : prime q -> (q mod 4)%Z = 1%Z -> (exists y, y*y = opp (ZToField q 1))%F. intros; pose proof prime_ge_2 q _. - apply square_Zmod_F. - destruct (minus1_square_1mod4 q) as [b b_id]; trivial. - exists b; rewrite b_id. - rewrite opp_ZToField, !FieldToZ_ZToField, !Z.mod_small; omega. -Qed. - -Lemma euler_criterion_nonsquare {q} (prime_q:prime q) (two_lt_q:(2<q)%Z) (d:F q) : - ((d =? 0)%Z || (Pre.powmod q d (Z.to_N (q / 2)) =? 1)%Z)%bool = false -> - forall x : F q, (x ^ 2)%F <> d. -Proof. - pose proof @euler_criterion_if q prime_q d two_lt_q; - break_if; intros; try discriminate; eauto. + rewrite Zmod.square_iff. + destruct (minus1_square_1mod4 q) as [b b_id]; trivial; exists b. + rewrite b_id, Zmod.FieldToZ_opp, Zmod.FieldToZ_ZToField, Z.mod_opp_l_nz, !Zmod_small; + (repeat (omega || rewrite Zmod_small)). Qed. Definition q : Z := (2 ^ 255 - 19)%Z. Global Instance prime_q : prime q. Admitted. Lemma two_lt_q : (2 < q)%Z. Proof. reflexivity. Qed. -Lemma char_gt_2 : (1 + 1 <> (0:F q))%F. Proof. rewrite F_eq; compute; discriminate. Qed. +Lemma char_gt_2 : (1 + 1 <> (0:F q))%F. vm_decide_no_check. Qed. Definition a : F q := opp 1%F. -Lemma nonzero_a : a <> 0%F. Proof. rewrite F_eq; compute; discriminate. Qed. +Lemma nonzero_a : a <> 0%F. Proof. vm_decide_no_check. Qed. Lemma square_a : exists b, (b*b=a)%F. -Proof. setoid_rewrite <-F_pow_2_r. apply (minus1_is_square _); reflexivity. Qed. +Proof. pose (@Zmod.Decidable_square q _ two_lt_q a); vm_decide_no_check. Qed. +Definition d : F q := (opp (ZToField _ 121665) / (ZToField _ 121666))%F. + +(* TODO: move to Decidable *) +Lemma not_not P {d:Decidable P} : not (not P) <-> P. +Proof. destruct (dec P); intuition. Qed. + +Global Instance dec_ex_forall_not T (P:T->Prop) {d:Decidable (exists b, P b)} : Decidable (forall b, ~ P b). +Proof. + destruct (dec (~ exists b, P b)) as [Hd|Hd]; [left|right]; + [abstract eauto | abstract (rewrite not_not in Hd by eauto; destruct Hd; eauto) ]. +Defined. -Definition d : F q := (opp (ZToField 121665) / (ZToField 121666))%F. Lemma nonsquare_d : forall x, (x*x <> d)%F. -Proof. - intros; rewrite <-F_pow_2_r. - apply (euler_criterion_nonsquare prime_q two_lt_q); vm_cast_no_check (eq_refl false). -Qed. (* 3s *) +Proof. pose (@Zmod.Decidable_square q _ two_lt_q d). vm_decide_no_check. Qed. -Instance curve25519params : @E.twisted_edwards_params (F q) eq (ZToField 0) (ZToField 1) add mul a d := +Instance curve25519params : @E.twisted_edwards_params (F q) eq 0%F 1%F add mul a d := { nonzero_a := nonzero_a; char_gt_2 := char_gt_2; @@ -112,10 +111,10 @@ Definition FlEncoding : canonical encoding of F (Z.of_nat l) as word b := Lemma q_5mod8 : (q mod 8 = 5)%Z. cbv; reflexivity. Qed. Lemma sqrt_minus1_valid : ((@ZToField q 2 ^ Z.to_N (q / 4)) ^ 2 = opp 1)%F. -Proof. apply F_eq; vm_compute; reflexivity. Qed. +Proof. vm_decide_no_check. Qed. -Local Notation point := (@E.point (F q) eq (ZToField 1) add mul a d). -Local Notation zero := (E.zero(H:=field_modulo)). +Local Notation point := (@E.point (F q) eq 1%F add mul a d). +Local Notation zero := (E.zero(H:=Zmod.field_modulo q)). Local Notation add := (E.add(H0:=curve25519params)). Local Infix "*" := (E.mul(H0:=curve25519params)). Axiom H : forall n : nat, word n -> word (b + b). diff --git a/src/ModularArithmetic/ModularArithmeticTheorems.v b/src/ModularArithmetic/ModularArithmeticTheorems.v index be9307b50..e36d15c8b 100644 --- a/src/ModularArithmetic/ModularArithmeticTheorems.v +++ b/src/ModularArithmetic/ModularArithmeticTheorems.v @@ -2,54 +2,20 @@ Require Import Coq.omega.Omega. Require Import Crypto.Spec.ModularArithmetic. Require Import Crypto.ModularArithmetic.Pre. -Require Import Coq.Logic.Eqdep_dec. -Require Import Crypto.Tactics.VerdiTactics. Require Import Coq.ZArith.BinInt Coq.ZArith.Zdiv Coq.ZArith.Znumtheory Coq.NArith.NArith. (* import Zdiv before Znumtheory *) Require Import Coq.Classes.Morphisms Coq.Setoids.Setoid. -Require Export Coq.setoid_ring.Ring_theory Coq.setoid_ring.Field_theory Coq.setoid_ring.Field_tac. -Require Export Crypto.Util.IterAssocOp. +Require Export Coq.setoid_ring.Ring_theory Coq.setoid_ring.Ring_tac. +Require Import Crypto.Algebra Crypto.Util.Decidable. Require Export Crypto.Util.FixCoqMistakes. -Section ModularArithmeticPreliminaries. - Context {m:Z}. - Let ZToFm := ZToField : BinNums.Z -> F m. Hint Unfold ZToFm. Local Coercion ZToFm : Z >-> F. - - Theorem F_eq: forall (x y : F m), x = y <-> FieldToZ x = FieldToZ y. - Proof. - destruct x, y; intuition; simpl in *; try congruence. - subst_max. - f_equal. - eapply UIP_dec, Z.eq_dec. - Qed. - - Lemma F_pow_spec : forall (a:F m), - pow a 0%N = 1%F /\ forall x, pow a (1 + x)%N = mul a (pow a x). - Proof. - intros a. - pose (@pow_with_spec m) as H. - change (@pow m) with (proj1_sig H). - destruct H; eauto. - Qed. -End ModularArithmeticPreliminaries. - (* Fails iff the input term does some arithmetic with mod'd values. *) Ltac notFancy E := -match E with -| - (_ mod _) => idtac -| context[_ mod _] => fail 1 -| _ => idtac -end. - -Lemma Zplus_neg : forall n m, n + -m = n - m. -Proof. - auto. -Qed. - -Lemma Zmod_eq : forall a b n, a = b -> a mod n = b mod n. -Proof. - intros; rewrite H; trivial. -Qed. + match E with + | - (_ mod _) => idtac + | context[_ mod _] => fail 1 + | _ => idtac + end. (* Remove redundant [mod] operations from the conclusion. *) Ltac demod := @@ -68,680 +34,325 @@ Ltac demod := notFancy y; rewrite (Zmult_mod_idemp_r y) | [ |- context[(?x mod _) mod _] ] => notFancy x; rewrite (Zmod_mod x) - | _ => rewrite Zplus_neg in * || rewrite Z.sub_diag in * end. -(* Remove exists under equals: we do this a lot *) -Ltac eq_remove_proofs := lazymatch goal with -| [ |- @eq (F _) ?a ?b ] => - assert (Q := F_eq a b); - simpl in *; apply Q; clear Q -end. - -(** TODO FIXME(from jgross): This tactic is way too powerful for - arcane reasons. It should not be using so many databases with - [intuition]. *) -Ltac Fdefn := +Ltac unwrap_F := intros; repeat match goal with [ x : F _ |- _ ] => destruct x end; - try eq_remove_proofs; - demod; - rewrite ?Z.mul_1_l; - intuition auto with zarith lia relations typeclass_instances; demod; try solve [ f_equal; intuition auto with zarith lia relations typeclass_instances ]. - -Local Open Scope F_scope. - -Section FEquality. - Context {m:Z}. - - (** Equality **) - Definition F_eqb (x y : F m) : bool := Z.eqb x y. - - Lemma F_eqb_eq x y : F_eqb x y = true -> x = y. - Proof. - unfold F_eqb; Fdefn; apply Z.eqb_eq; trivial. - Qed. - - Lemma F_eqb_complete : forall x y: F m, x = y -> F_eqb x y = true. - Proof. - intros; subst; apply Z.eqb_refl. - Qed. - - Lemma F_eqb_refl : forall x, F_eqb x x = true. - Proof. - intros; apply F_eqb_complete; trivial. - Qed. - - Lemma F_eqb_neq x y : F_eqb x y = false -> x <> y. - Proof. - intuition; subst y. - pose proof (F_eqb_refl x). - congruence. - Qed. - - Lemma F_eqb_neq_complete x y : x <> y -> F_eqb x y = false. - Proof. - intros. - case_eq (F_eqb x y); intros; trivial. - pose proof (F_eqb_eq x y); intuition. - Qed. - - Lemma F_eq_dec : forall x y : F m, {x = y} + {x <> y}. - Proof. - intros; case_eq (F_eqb x y); [left|right]; auto using F_eqb_eq, F_eqb_neq. - Qed. - - Lemma if_F_eq_dec_if_F_eqb : forall {T} x y (a b:T), (if F_eq_dec x y then a else b) = (if F_eqb x y then a else b). - Proof. - intros; intuition; break_if. - - rewrite F_eqb_complete; trivial. - - rewrite F_eqb_neq_complete; trivial. - Defined. -End FEquality. - -Section FandZ. - Context {m:Z}. - - Lemma ZToField_small_nonzero : forall z, (0 < z < m)%Z -> ZToField z <> (0:F m). - Proof. - intuition; find_inversion; rewrite ?Z.mod_0_l, ?Z.mod_small in *; intuition auto with zarith. - Qed. - - Require Crypto.Algebra. - Global Instance commutative_ring_modulo : @Algebra.commutative_ring (F m) Logic.eq (ZToField 0) (ZToField 1) opp add sub mul. - Proof. - repeat split; Fdefn; try apply F_eq_dec. - { rewrite Z.add_0_r. auto. } - { rewrite Z.mul_1_r. auto. } - Qed. - - Lemma F_opp_spec : forall (a:F m), add a (opp a) = 0. - Fdefn. - Qed. - - Lemma ZToField_0 : @ZToField m 0 = 0. - Proof. - Fdefn. - Qed. - - Lemma FieldToZ_ZToField : forall z, FieldToZ (@ZToField m z) = z mod m. - Proof. - Fdefn. - Qed. - - Lemma mod_FieldToZ : forall x, (@FieldToZ m x) mod m = FieldToZ x. - Proof. - Fdefn. - Qed. - - (** ZToField distributes over operations **) - Lemma ZToField_add : forall (x y : Z), - @ZToField m (x + y) = ZToField x + ZToField y. - Proof. - Fdefn. - Qed. - - Lemma FieldToZ_add : forall x y : F m, - FieldToZ (x + y) = ((FieldToZ x + FieldToZ y) mod m)%Z. - Proof. - Fdefn. - Qed. - - Lemma FieldToZ_mul : forall x y : F m, - FieldToZ (x * y) = ((FieldToZ x * FieldToZ y) mod m)%Z. - Proof. - Fdefn. - Qed. - - Lemma FieldToZ_pow_Zpow_mod : forall (x : F m) n, - (FieldToZ x ^ Z.of_N n mod m = FieldToZ (x ^ n)%F)%Z. - Proof. - intros. - induction n using N.peano_ind; - destruct (F_pow_spec x) as [pow_0 pow_succ] . { - rewrite pow_0. - rewrite Z.pow_0_r; auto. - } { - rewrite N2Z.inj_succ. - rewrite Z.pow_succ_r by apply N2Z.is_nonneg. - rewrite <- N.add_1_l. - rewrite pow_succ. - rewrite <- Zmult_mod_idemp_r. - rewrite IHn. - apply FieldToZ_mul. - } - Qed. - - Lemma FieldToZ_pow_efficient : forall (x : F m) n, FieldToZ (x^n) = powmod m (FieldToZ x) n. - Proof. - intros. - rewrite powmod_Zpow_mod. - rewrite <-FieldToZ_pow_Zpow_mod. - reflexivity. - Qed. - - Lemma pow_nat_iter_op_correct: forall (x:F m) n, (@nat_iter_op _ mul 1) (N.to_nat n) x = x^n. - Proof. - induction n using N.peano_ind; - destruct (F_pow_spec x) as [pow_0 pow_succ]; - rewrite ?N2Nat.inj_succ, ?pow_0, <-?N.add_1_l, ?pow_succ; - simpl; congruence. - Qed. - - Lemma mod_plus_zero_subproof a b : 0 mod m = (a + b) mod m -> - b mod m = (- a) mod m. - Proof. - rewrite <-Z.sub_0_l; intros. - replace (0-a)%Z with (b-(a + b))%Z by omega. - rewrite Zminus_mod. - rewrite <- H. - rewrite Zmod_0_l. - replace (b mod m - 0)%Z with (b mod m) by omega. - rewrite Zmod_mod. - reflexivity. - Qed. - - Lemma FieldToZ_opp' : forall x, FieldToZ (@opp m x) mod m = -x mod m. - Proof. - intros. - pose proof (FieldToZ_add x (opp x)) as H. - rewrite F_opp_spec, FieldToZ_ZToField in H. - auto using mod_plus_zero_subproof. - Qed. - - Lemma FieldToZ_opp : forall x, FieldToZ (@opp m x) = -x mod m. - Proof. - intros. - pose proof (FieldToZ_opp' x) as H; rewrite mod_FieldToZ in H; trivial. - Qed. - - Lemma sub_intersperse_modulus : forall x y, ((x - y) mod m = (x + (m - y)) mod m)%Z. - Proof. - intros. - replace (x + (m - y))%Z with (m+(x-y))%Z by omega. - rewrite Zplus_mod. - rewrite Z_mod_same_full; simpl Z.add. - rewrite Zmod_mod. - reflexivity. - Qed. - - (* Compatibility between inject and subtraction *) - Lemma ZToField_sub : forall (x y : Z), - @ZToField m (x - y) = ZToField x - ZToField y. - Proof. - Fdefn. - Qed. - - (* Compatibility between inject and multiplication *) - Lemma ZToField_mul : forall (x y : Z), - @ZToField m (x * y) = ZToField x * ZToField y. - Proof. - Fdefn. - Qed. - - (* Compatibility between inject and GFtoZ *) - Lemma ZToField_idempotent : forall (x : F m), ZToField x = x. - Proof. - Fdefn. - Qed. - Definition ZToField_FieldToZ := ZToField_idempotent. (* alias *) - - (* Compatibility between inject and mod *) - Lemma ZToField_mod : forall x, @ZToField m x = ZToField (x mod m). - Proof. - Fdefn. - Qed. - - (* Compatibility between inject and pow *) - Lemma ZToField_pow : forall x n, - @ZToField m x ^ n = ZToField (x ^ (Z.of_N n) mod m). - Proof. - intros. - induction n using N.peano_ind; - destruct (F_pow_spec (@ZToField m x)) as [pow_0 pow_succ] . { - rewrite pow_0. - Fdefn. - } { - rewrite N2Z.inj_succ. - rewrite Z.pow_succ_r by apply N2Z.is_nonneg. - rewrite <- N.add_1_l. - rewrite pow_succ. - rewrite IHn. - Fdefn. - } - Qed. - - Lemma ZToField_eqmod : forall x y : Z, x mod m = y mod m -> ZToField x = @ZToField m y. - Fdefn. - Qed. - - Lemma FieldToZ_nonzero: - forall x0 : F m, x0 <> 0 -> FieldToZ x0 <> 0%Z. - Proof. - intros x0 Hnz Hz. - rewrite <- Hz, ZToField_FieldToZ in Hnz; auto. - Qed. - -End FandZ. - -Section RingModuloPre. - Context {m:Z}. - Let ZToFm := ZToField : Z -> F m. Hint Unfold ZToFm. Local Coercion ZToFm : Z >-> F. - (* Substitution to prove all Compats *) - Ltac compat := repeat intro; subst; trivial. - - Instance Fplus_compat : Proper (eq==>eq==>eq) (@add m). - Proof. - compat. - Qed. - - Instance Fminus_compat : Proper (eq==>eq==>eq) (@sub m). - Proof. - compat. - Qed. - - Instance Fmult_compat : Proper (eq==>eq==>eq) (@mul m). - Proof. - compat. - Qed. - - Instance Fopp_compat : Proper (eq==>eq) (@opp m). - Proof. - compat. - Qed. - - Instance Finv_compat : Proper (eq==>eq) (@inv m). - Proof. - compat. - Qed. - - Instance Fdiv_compat : Proper (eq==>eq==>eq) (@div m). - Proof. - compat. - Qed. - - (***** Ring Theory *****) - Definition Fring_theory : ring_theory 0%F 1%F (@add m) (@mul m) (@sub m) (@opp m) eq. - Proof. - constructor; Fdefn. - Qed. - - Lemma F_mul_1_r: - forall x : F m, x * 1 = x. - Proof. - Fdefn; rewrite Z.mul_1_r; auto. - Qed. - - Lemma F_mul_assoc: - forall x y z : F m, x * (y * z) = x * y * z. - Proof. - Fdefn. - Qed. - - Lemma F_pow_pow_N (x : F m) : forall (n : N), (x ^ id n)%F = pow_N 1%F mul x n. - Proof. - destruct (F_pow_spec x) as [HO HS]; intros. - destruct n; auto; unfold id. - rewrite Pre.N_pos_1plus at 1. - rewrite HS. - simpl. - induction p using Pos.peano_ind. - - simpl. rewrite HO; apply F_mul_1_r. - - rewrite (@pow_pos_succ (F m) (@mul m) eq _ _ F_mul_assoc x). - rewrite <-IHp, Pos.pred_N_succ, Pre.N_pos_1plus, HS. - f_equal. - Qed. - - (***** Power theory *****) - Lemma Fpower_theory : power_theory 1%F (@mul m) eq id (@pow m). - Proof. - constructor; apply F_pow_pow_N. - Qed. - - (***** Division Theory *****) - Definition Fquotrem(a b: F m): F m * F m := - let '(q, r) := (Z.quotrem a b) in (q : F m, r : F m). - Lemma Fdiv_theory : div_theory eq (@add m) (@mul m) (@id _) Fquotrem. - Proof. - constructor; intros; unfold Fquotrem, id. - - replace (Z.quotrem a b) with (Z.quot a b, Z.rem a b) by - try (unfold Z.quot, Z.rem; rewrite <- surjective_pairing; trivial). - - Fdefn; rewrite <-Z.quot_rem'; trivial. - Qed. - - Lemma Z_mul_mod_modulus_r : forall x m, ((x*m) mod m = 0)%Z. - intros. - rewrite Zmult_mod, Z_mod_same_full. - rewrite Z.mul_0_r, Zmod_0_l. - reflexivity. - Qed. - - Lemma Z_mod_opp_equiv : forall x y m, x mod m = (-y) mod m -> - (-x) mod m = y mod m. - Proof. - intros. - rewrite <-Z.sub_0_l. - rewrite Zminus_mod. rewrite H. - rewrite ?Zminus_mod_idemp_l, ?Zminus_mod_idemp_r; f_equal. - destruct y; auto. - Qed. - - Lemma Z_opp_opp : forall x : Z, (-(-x)) = x. - destruct x; auto. - Qed. - - Lemma Z_mod_opp : forall x m, (- x) mod m = (- (x mod m)) mod m. - intros. - apply Z_mod_opp_equiv. - rewrite Z_opp_opp. - demod; auto. - Qed. - - (* Define a "ring morphism" between GF and Z, i.e. an equivalence - * between 'inject (ZFunction (X))' and 'GFFunction (inject (X))'. - * - * Doing this allows us to do our coefficient manipulations in Z - * rather than GF, because we know it's equivalent to inject the - * result afterward. - *) - Lemma Fring_morph: - ring_morph 0%F 1%F (@add m) (@mul m) (@sub m) (@opp m) eq - 0%Z 1%Z Z.add Z.mul Z.sub Z.opp Z.eqb - (@ZToField m). - Proof. - constructor; intros; try Fdefn; unfold id; - try (apply gf_eq; simpl; intuition). - - apply Z_mod_opp_equiv; rewrite Z_opp_opp, Zmod_mod; reflexivity. - - rewrite (proj1 (Z.eqb_eq x y)); trivial. - Qed. - - (* Redefine our division theory under the ring morphism *) - Lemma Fmorph_div_theory: + lazy iota beta delta [add sub mul opp FieldToZ ZToField proj1_sig] in *; + try apply eqsig_eq; + demod. + +Global Instance eq_dec {m} : DecidableRel (@eq (F m)). exact _. Defined. + +Global Instance commutative_ring_modulo m + : @Algebra.commutative_ring (F m) Logic.eq 0%F 1%F opp add sub mul. +Proof. + repeat (split || intro); unwrap_F; + autorewrite with zsimplify; solve [ exact _ | auto with zarith | congruence]. +Qed. + + +Module Zmod. + Lemma pow_spec {m} a : pow a 0%N = 1%F :> F m /\ forall x, pow a (1 + x)%N = mul a (pow a x). + Proof. change (@pow m) with (proj1_sig (@pow_with_spec m)); destruct (@pow_with_spec m); eauto. Qed. + + Section FandZ. + Context {m:Z}. + Local Open Scope F_scope. + + Theorem eq_FieldToZ_iff (x y : F m) : x = y <-> FieldToZ x = FieldToZ y. + Proof. destruct x, y; intuition; simpl in *; try apply (eqsig_eq _ _); congruence. Qed. + + Lemma eq_ZToField_iff : forall x y : Z, x mod m = y mod m <-> ZToField m x = ZToField m y. + Proof. split; unwrap_F; congruence. Qed. + + + Lemma FieldToZ_ZToField : forall z, FieldToZ (@ZToField m z) = z mod m. + Proof. unwrap_F; trivial. Qed. + + Lemma ZToField_FieldToZ x : ZToField m (FieldToZ x) = x :> F m. + Proof. unwrap_F; congruence. Qed. + + + Lemma ZToField_mod : forall x, ZToField m x = ZToField m (x mod m). + Proof. unwrap_F; trivial. Qed. + + Lemma mod_FieldToZ : forall (x:F m), FieldToZ x mod m = FieldToZ x. + Proof. unwrap_F. congruence. Qed. + + Lemma FieldToZ_0 : FieldToZ (0:F m) = 0%Z. + Proof. unwrap_F. apply Zmod_0_l. Qed. + + Lemma ZToField_small_nonzero z : (0 < z < m)%Z -> ZToField m z <> 0. + Proof. intros Hrange Hnz. inversion Hnz. rewrite Zmod_small, Zmod_0_l in *; omega. Qed. + + Lemma FieldToZ_nonzero (x:F m) : x <> 0 -> FieldToZ x <> 0%Z. + Proof. intros Hnz Hz. rewrite <- Hz, ZToField_FieldToZ in Hnz; auto. Qed. + + Lemma FieldToZ_range (x : F m) : 0 < m -> 0 <= x < m. + Proof. intros. rewrite <- mod_FieldToZ. apply Z.mod_pos_bound. trivial. Qed. + + Lemma FieldToZ_nonzero_range (x : F m) : (x <> 0) -> 0 < m -> (1 <= x < m)%Z. + Proof. + unfold not; intros Hnz Hlt. + rewrite eq_FieldToZ_iff, FieldToZ_0 in Hnz; pose proof (FieldToZ_range x Hlt). + omega. + Qed. + + Lemma ZToField_add : forall (x y : Z), + ZToField m (x + y) = ZToField m x + ZToField m y. + Proof. unwrap_F; trivial. Qed. + + Lemma FieldToZ_add : forall x y : F m, + FieldToZ (x + y) = ((FieldToZ x + FieldToZ y) mod m)%Z. + Proof. unwrap_F; trivial. Qed. + + Lemma ZToField_mul x y : ZToField m (x * y) = ZToField _ x * ZToField _ y :> F m. + Proof. unwrap_F. trivial. Qed. + + Lemma FieldToZ_mul : forall x y : F m, + FieldToZ (x * y) = ((FieldToZ x * FieldToZ y) mod m)%Z. + Proof. unwrap_F; trivial. Qed. + + Lemma ZToField_sub x y : ZToField _ (x - y) = ZToField _ x - ZToField _ y :> F m. + Proof. unwrap_F. trivial. Qed. + + Lemma FieldToZ_opp : forall x, FieldToZ (@opp m x) = -x mod m. + Proof. unwrap_F; trivial. Qed. + + Lemma ZToField_pow x n : ZToField _ x ^ n = ZToField _ (x ^ (Z.of_N n) mod m) :> F m. + Proof. + intros. + induction n using N.peano_ind; + destruct (pow_spec (@ZToField m x)) as [pow_0 pow_succ] . { + rewrite pow_0. + unwrap_F; trivial. + } { + rewrite N2Z.inj_succ. + rewrite Z.pow_succ_r by apply N2Z.is_nonneg. + rewrite <- N.add_1_l. + rewrite pow_succ. + rewrite IHn. + unwrap_F; trivial. + } + Qed. + + Lemma FieldToZ_pow : forall (x : F m) n, + FieldToZ (x ^ n)%F = (FieldToZ x ^ Z.of_N n mod m)%Z. + Proof. + intros. + symmetry. + induction n using N.peano_ind; + destruct (pow_spec x) as [pow_0 pow_succ] . { + rewrite pow_0, Z.pow_0_r; auto. + } { + rewrite N2Z.inj_succ. + rewrite Z.pow_succ_r by apply N2Z.is_nonneg. + rewrite <- N.add_1_l. + rewrite pow_succ. + rewrite <- Zmult_mod_idemp_r. + rewrite IHn. + apply FieldToZ_mul. + } + Qed. + + Lemma square_iff (x:F m) : + (exists y : F m, y * y = x) <-> (exists y : Z, y * y mod m = x)%Z. + Proof. + setoid_rewrite eq_FieldToZ_iff; setoid_rewrite FieldToZ_mul; split; intro H; destruct H as [x' H]. + - eauto. + - exists (ZToField _ x'); rewrite !FieldToZ_ZToField; demod; auto. + Qed. + + (* TODO: move to ZUtil *) + Lemma sub_intersperse_modulus : forall x y, ((x - y) mod m = (x + (m - y)) mod m)%Z. + Proof. + intros. + replace (x + (m - y))%Z with (m+(x-y))%Z by omega. + rewrite Zplus_mod. + rewrite Z_mod_same_full; simpl Z.add. + rewrite Zmod_mod. + reflexivity. + Qed. + End FandZ. + + Section RingTacticGadgets. + Context (m:Z). + + Definition ring_theory : ring_theory 0%F 1%F (@add m) (@mul m) (@sub m) (@opp m) eq + := Algebra.Ring.ring_theory_for_stdlib_tactic. + + Lemma pow_pow_N (x : F m) : forall (n : N), (x ^ id n)%F = pow_N 1%F mul x n. + Proof. + destruct (pow_spec x) as [HO HS]; intros. + destruct n; auto; unfold id. + rewrite Pre.N_pos_1plus at 1. + rewrite HS. + simpl. + induction p using Pos.peano_ind. + - simpl. rewrite HO. apply Algebra.right_identity. + - rewrite (@pow_pos_succ (F m) (@mul m) eq _ _ associative x). + rewrite <-IHp, Pos.pred_N_succ, Pre.N_pos_1plus, HS. + trivial. + Qed. + + Lemma power_theory : power_theory 1%F (@mul m) eq id (@pow m). + Proof. split; apply pow_pow_N. Qed. + + (***** Division Theory *****) + Definition quotrem(a b: F m): F m * F m := + let '(q, r) := (Z.quotrem a b) in (ZToField _ q , ZToField _ r). + Lemma Fdiv_theory : div_theory eq (@add m) (@mul m) (@id _) quotrem. + Proof. + constructor; intros; unfold quotrem, id. + + replace (Z.quotrem a b) with (Z.quot a b, Z.rem a b) by + try (unfold Z.quot, Z.rem; rewrite <- surjective_pairing; trivial). + + unwrap_F; rewrite <-Z.quot_rem'; trivial. + Qed. + + Lemma Z_mod_opp_equiv : forall x y m, x mod m = (-y) mod m -> + (-x) mod m = y mod m. + Proof. + intros. + rewrite <-Z.sub_0_l. + rewrite Zminus_mod. rewrite H. + rewrite ?Zminus_mod_idemp_l, ?Zminus_mod_idemp_r; f_equal. + destruct y; auto. + Qed. + + Lemma Z_opp_opp : forall x : Z, (-(-x)) = x. + destruct x; auto. + Qed. + + Lemma Z_mod_opp : forall x m, (- x) mod m = (- (x mod m)) mod m. + intros. + apply Z_mod_opp_equiv. + rewrite Z_opp_opp. + demod; auto. + Qed. + + (* Define a "ring morphism" between GF and Z, i.e. an equivalence + * between 'inject (ZFunction (X))' and 'GFFunction (inject (X))'. + * + * Doing this allows the [ring] tactic to do coefficient + * manipulations in Z rather than F, because we know it's equivalent + * to inject the result afterward. *) + Lemma ring_morph: ring_morph 0%F 1%F (@add m) (@mul m) (@sub m) (@opp m) eq + 0%Z 1%Z Z.add Z.mul Z.sub Z.opp Z.eqb (@ZToField m). + Proof. split; intros; unwrap_F; solve [ auto | rewrite (proj1 (Z.eqb_eq x y)); trivial]. Qed. + + (* Redefine our division theory under the ring morphism *) + Lemma morph_div_theory: div_theory eq Zplus Zmult (@ZToField m) Z.quotrem. - Proof. - constructor; intros; intuition. - replace (Z.quotrem a b) with (Z.quot a b, Z.rem a b); - try (unfold Z.quot, Z.rem; rewrite <- surjective_pairing; trivial). - - eq_remove_proofs; demod; - rewrite <- (Z.quot_rem' a b); - destruct a; simpl; trivial. - Qed. - - Lemma ZToField_1 : @ZToField m 1 = 1. - Proof. - Fdefn. - Qed. -End RingModuloPre. - -Ltac Fconstant t := match t with @ZToField _ ?x => x | _ => NotConstant end. -Ltac Fexp_tac t := Ncst t. -Ltac Fpreprocess := rewrite <-?ZToField_0, ?ZToField_1. -Ltac Fpostprocess := repeat split; - repeat match goal with [ |- context[exist ?a ?b (Pre.Z_mod_mod ?x ?q)] ] => - change (exist a b (Pre.Z_mod_mod x q)) with (@ZToField q x%Z) end; - rewrite ?ZToField_0, ?ZToField_1. - -Module Type Modulus. - Parameter modulus : Z. -End Modulus. - -(* Example of how to instantiate the ring tactic *) -Module RingModulo (Export M : Modulus). - Definition ring_theory_modulo := @Fring_theory modulus. - Definition ring_morph_modulo := @Fring_morph modulus. - Definition morph_div_theory_modulo := @Fmorph_div_theory modulus. - Definition power_theory_modulo := @Fpower_theory modulus. - - Add Ring GFring_Z : ring_theory_modulo - (morphism ring_morph_modulo, - constants [Fconstant], - div morph_div_theory_modulo, - power_tac power_theory_modulo [Fexp_tac]). -End RingModulo. - -Section VariousModulo. - Context {m:Z}. - - Add Ring GFring_Z : (@Fring_theory m) - (morphism (@Fring_morph m), - constants [Fconstant], - div (@Fmorph_div_theory m), - power_tac (@Fpower_theory m) [Fexp_tac]). - - Lemma F_mul_0_l : forall x : F m, 0 * x = 0. - Proof. - intros; ring. - Qed. - - Lemma F_mul_0_r : forall x : F m, x * 0 = 0. - Proof. - intros; ring. - Qed. - - Lemma F_mul_nonzero_l : forall a b : F m, a*b <> 0 -> a <> 0. - intros; intuition; subst. - assert (0 * b = 0) by ring; intuition. - Qed. - - Lemma F_mul_nonzero_r : forall a b : F m, a*b <> 0 -> b <> 0. - intros; intuition; subst. - assert (a * 0 = 0) by ring; intuition. - Qed. - - Lemma F_pow_distr_mul : forall (x y:F m) z, (0 <= z)%N -> - (x ^ z) * (y ^ z) = (x * y) ^ z. - Proof. - intros. - replace z with (Z.to_N (Z.of_N z)) by apply N2Z.id. - apply natlike_ind with (x := Z.of_N z); simpl; [ ring | | - replace 0%Z with (Z.of_N 0%N) by auto; apply N2Z.inj_le; auto]. - intros z' z'_nonneg IHz'. - rewrite Z2N.inj_succ by auto. - rewrite <-N.add_1_l. - rewrite !(proj2 (@F_pow_spec m _) _). - rewrite <- IHz'. - ring. - Qed. - - Lemma F_opp_0 : opp (0 : F m) = 0%F. - Proof. - intros; ring. - Qed. - - Lemma F_opp_swap : forall x y : F m, opp x = y <-> x = opp y. - Proof. - split; intro; subst; ring. - Qed. - - Lemma F_opp_involutive : forall x : F m, opp (opp x) = x. - Proof. - intros; ring. - Qed. - - Lemma F_square_opp : forall x : F m, (opp x ^ 2 = x ^ 2)%F. - Proof. - intros; ring. - Qed. - - Lemma F_mul_opp_r : forall x y : F m, (x * opp y = opp (x * y))%F. - intros; ring. - Qed. - - Lemma F_mul_opp_l : forall x y : F m, (opp x * y = opp (x * y))%F. - intros; ring. - Qed. - - Lemma F_mul_opp_both : forall x y : F m, (opp x * opp y = x * y)%F. - intros; ring. - Qed. - - Lemma F_add_0_r : forall x : F m, (x + 0)%F = x. - Proof. - intros; ring. - Qed. - - Lemma F_add_0_l : forall x : F m, (0 + x)%F = x. - Proof. - intros; ring. - Qed. - - Lemma F_add_reg_r : forall x y z : F m, y + x = z + x -> y = z. - Proof. - intros ? ? ? A. - replace y with (y + x - x) by ring. - rewrite A; ring. - Qed. - - Lemma F_add_reg_l : forall x y z : F m, x + y = x + z -> y = z. - Proof. - intros ? ? ? A. - replace y with (x + y - x) by ring. - rewrite A; ring. - Qed. - - Lemma F_sub_0_r : forall x : F m, (x - 0)%F = x. - Proof. - intros; ring. - Qed. - - Lemma F_sub_0_l : forall x : F m, (0 - x)%F = opp x. - Proof. - intros; ring. - Qed. - - Lemma F_mul_1_l : forall x : F m, (1 * x)%F = x. - Proof. - intros; ring. - Qed. - - Lemma F_ZToField_m : ZToField m = @ZToField m 0. - Proof. - Fdefn. - rewrite Zmod_0_l. - apply Z_mod_same_full. - Qed. - - Lemma F_sub_m_l : forall x : F m, opp x = ZToField m - x. - Proof. - rewrite F_ZToField_m. - symmetry. - apply F_sub_0_l. - Qed. - - Lemma opp_ZToField : forall x : Z, opp (ZToField x) = @ZToField m (m - x). - Proof. - Fdefn. - rewrite Zminus_mod, Z_mod_same_full, (Z.sub_0_l (x mod m)); reflexivity. - Qed. - - Lemma F_pow_2_r : forall x : F m, x^2 = x*x. - Proof. - intros. ring. - Qed. - - Lemma F_pow_3_r : forall x : F m, x^3 = x*x*x. - Proof. - intros. ring. - Qed. - - Lemma F_pow_add : forall (x : F m) k j, x ^ j * x ^ k = x ^ (j + k). - Proof. - intros. - destruct (F_pow_spec x) as [exp_zero exp_succ]. - induction j using N.peano_ind. - + rewrite exp_zero. - ring_simplify; eauto. - + - rewrite N.add_succ_l. - do 2 rewrite <- N.add_1_l. - do 2 rewrite exp_succ by apply N.neq_succ_0. - rewrite <- IHj. - ring. - Qed. - - Lemma F_pow_compose : forall (x : F m) k j, (x ^ j) ^ k = x ^ (k * j). - Proof. - intros. - induction k using N.peano_ind; [rewrite Nmult_0_l; ring | ]. - rewrite Nmult_Sn_m. - rewrite <- F_pow_add. - rewrite <- IHk. - rewrite <- N.add_1_l. - rewrite (proj2 (F_pow_spec _)). - ring. - Qed. - - Lemma F_sub_add_swap : forall w x y z : F m, w - x = y - z <-> w + z = y + x. - Proof. - split; intro A; - [ replace w with (w - x + x) by ring - | replace w with (w + z - z) by ring ]; rewrite A; ring. - Qed. - - Definition isSquare (x : F m) := exists sqrt_x, sqrt_x ^ 2 = x. - - Lemma square_Zmod_F : forall (a : F m), isSquare a <-> - (exists b : Z, ((b * b) mod m)%Z = a). - Proof. - split; intro A; destruct A as [sqrt_a sqrt_a_id]. { - exists sqrt_a. - rewrite <- FieldToZ_mul. - apply F_eq. - ring_simplify; auto. - } { - exists (ZToField sqrt_a). - rewrite ZToField_pow. - replace (Z.of_N 2) with 2%Z by auto. - rewrite Z.pow_2_r. - rewrite sqrt_a_id. - apply ZToField_FieldToZ. - } - Qed. - - Lemma FieldToZ_range : forall x : F m, 0 < m -> 0 <= x < m. - Proof. - intros. - rewrite <- mod_FieldToZ. - apply Z.mod_pos_bound. - omega. - Qed. - - Lemma FieldToZ_nonzero_range : forall x : F m, (x <> 0) -> 0 < m -> - (1 <= x < m)%Z. - Proof. - intros. - pose proof (FieldToZ_range x). - unfold not in *. - rewrite F_eq in H. - replace (FieldToZ 0) with 0%Z in H by auto. - omega. - Qed. - - Lemma F_mul_comm : forall x y : F m, x*y = y*x. - intros; ring. - Qed. - - Lemma Fq_sub_eq : forall x y a b : F m, a = b -> x-a = y-b -> x = y. - Proof. - intros x y a b Hab Hxayb; subst. - replace x with ((x - b) + b) by ring. - replace y with ((y - b) + b) by ring. - rewrite Hxayb; ring. - Qed. - - Lemma F_FieldToZ_add_opp : forall x : F m, x <> 0 -> (FieldToZ x + FieldToZ (opp x) = m)%Z. - Proof. - intros. - rewrite FieldToZ_opp. - rewrite Z_mod_nz_opp_full, mod_FieldToZ; try omega. - rewrite mod_FieldToZ. - replace 0%Z with (@FieldToZ m 0) by auto. - intro false_eq. - rewrite <-F_eq in false_eq. - congruence. - Qed. - -End VariousModulo. + Proof. + split; intros. + replace (Z.quotrem a b) with (Z.quot a b, Z.rem a b); + try (unfold Z.quot, Z.rem; rewrite <- surjective_pairing; trivial). + unwrap_F; rewrite <- (Z.quot_rem' a b); trivial. + Qed. + + End RingTacticGadgets. + + Ltac is_constant t := match t with @ZToField _ ?x => x | _ => NotConstant end. + Ltac is_pow_constant t := Ncst t. + + Module Type Modulus. Parameter modulus : Z. End Modulus. + + (* Example of how to instantiate the ring tactic *) + Module RingModulo (Export M : Modulus). + Add Ring _theory : (ring_theory modulus) + (morphism (ring_morph modulus), + constants [is_constant], + div (morph_div_theory modulus), + power_tac (power_theory modulus) [is_pow_constant]). + + Example ring_modulo_example : forall x y z, x*z + z*y = z*(x+y). + Proof. intros. ring. Qed. + End RingModulo. + + Section VariousModulo. + Context {m:Z}. + Local Open Scope F_scope. + + Add Ring _theory : (ring_theory m) + (morphism (ring_morph m), + constants [is_constant], + div (morph_div_theory m), + power_tac (power_theory m) [is_pow_constant]). + + Lemma mul_nonzero_l : forall a b : F m, a*b <> 0 -> a <> 0. + Proof. intros a b Hnz Hz. rewrite Hz in Hnz; apply Hnz; ring. Qed. + + Lemma mul_nonzero_r : forall a b : F m, a*b <> 0 -> b <> 0. + Proof. intros a b Hnz Hz. rewrite Hz in Hnz; apply Hnz; ring. Qed. + End VariousModulo. + + Section Pow. + Context {m:Z}. + Add Ring _theory' : (ring_theory m) + (morphism (ring_morph m), + constants [is_constant], + div (morph_div_theory m), + power_tac (power_theory m) [is_pow_constant]). + Local Open Scope F_scope. + + Import Algebra.ScalarMult. + Global Instance pow_is_scalarmult + : is_scalarmult (G:=F m) (eq:=eq) (add:=mul) (zero:=1%F) (mul := fun n x => x ^ (N.of_nat n)). + Proof. + split; intros; rewrite ?Nat2N.inj_succ, <-?N.add_1_l; + match goal with + | [x:F m |- _ ] => solve [destruct (@pow_spec m P); auto] + | |- Proper _ _ => solve_proper + end. + Qed. + + (* TODO: move this somewhere? *) + Create HintDb nat2N discriminated. + Hint Rewrite Nat2N.inj_iff + (eq_refl _ : (0%N = N.of_nat 0)) + (eq_refl _ : (1%N = N.of_nat 1)) + (eq_refl _ : (2%N = N.of_nat 2)) + (eq_refl _ : (3%N = N.of_nat 3)) + : nat2N. + Hint Rewrite <- Nat2N.inj_double Nat2N.inj_succ_double Nat2N.inj_succ + Nat2N.inj_add Nat2N.inj_mul Nat2N.inj_sub Nat2N.inj_pred + Nat2N.inj_div2 Nat2N.inj_max Nat2N.inj_min Nat2N.id + : nat2N. + + Ltac pow_to_scalarmult_ref := + repeat (autorewrite with nat2N; + match goal with + | |- context [ (_^?n)%F ] => + rewrite <-(N2Nat.id n); generalize (N.to_nat n); clear n; + let m := fresh n in intro m + | |- context [ (_^N.of_nat ?n)%F ] => + let rw := constr:(scalarmult_ext(zero:=ZToField m 1) n) in + setoid_rewrite rw (* rewriting moduloa reduction *) + end). + + Lemma pow_0_r (x:F m) : x^0 = 1. + Proof. pow_to_scalarmult_ref. apply scalarmult_0_l. Qed. + + Lemma pow_add_r (x:F m) (a b:N) : x^(a+b) = x^a * x^b. + Proof. pow_to_scalarmult_ref; apply scalarmult_add_l. Qed. + + Lemma pow_0_l (n:N) : n <> 0%N -> 0^n = 0 :> F m. + Proof. pow_to_scalarmult_ref; destruct n; simpl; intros; [congruence|ring]. Qed. + + Lemma pow_pow_l (x:F m) (a b:N) : (x^a)^b = x^(a*b). + Proof. pow_to_scalarmult_ref. apply scalarmult_assoc. Qed. + + Lemma pow_1_r (x:F m) : x^1 = x. + Proof. pow_to_scalarmult_ref; simpl; ring. Qed. + + Lemma pow_2_r (x:F m) : x^2 = x*x. + Proof. pow_to_scalarmult_ref; simpl; ring. Qed. + + Lemma pow_3_r (x:F m) : x^3 = x*x*x. + Proof. pow_to_scalarmult_ref; simpl; ring. Qed. + End Pow. +End Zmod. diff --git a/src/ModularArithmetic/ModularBaseSystem.v b/src/ModularArithmetic/ModularBaseSystem.v index 4fd881e1e..f80ce05f8 100644 --- a/src/ModularArithmetic/ModularBaseSystem.v +++ b/src/ModularArithmetic/ModularBaseSystem.v @@ -37,9 +37,9 @@ Section ModularBaseSystem. from_list (sub [[modulus_multiple]] [[us]] [[vs]]) (length_sub length_to_list length_to_list length_to_list). - Definition zero : digits := encode (ZToField 0). + Definition zero : digits := encode (ZToField _ 0). - Definition one : digits := encode (ZToField 1). + Definition one : digits := encode (ZToField _ 1). (* Placeholder *) Definition opp (x : digits) : digits := encode (ModularArithmetic.opp (decode x)). diff --git a/src/ModularArithmetic/ModularBaseSystemField.v b/src/ModularArithmetic/ModularBaseSystemField.v index f5bedd644..b26ca027d 100644 --- a/src/ModularArithmetic/ModularBaseSystemField.v +++ b/src/ModularArithmetic/ModularBaseSystemField.v @@ -11,6 +11,7 @@ Local Open Scope Z_scope. Section ModularBaseSystemField. Context `{prm : PseudoMersenneBaseParams} {sc : SubtractionCoefficient modulus prm} (k_ c_ : Z) (k_subst : k = k_) (c_subst : c = c_). + Local Existing Instance prime_modulus. Local Notation base := (Pow2Base.base_from_limb_widths limb_widths). Local Notation digits := (tuple Z (length limb_widths)). @@ -35,17 +36,13 @@ Section ModularBaseSystemField. apply carry_mul_rep; apply decode_rep. Qed. - Lemma zero_neq_one : eq zero one -> False. - Proof. - cbv [eq zero one]. erewrite !encode_rep. intro A. - eapply (PrimeFieldTheorems.Fq_1_neq_0 (prime_q := prime_modulus)). - congruence. - Qed. + Lemma _zero_neq_one : not (eq zero one). + Proof. cbv [eq zero one]. erewrite !encode_rep; apply zero_neq_one. Qed. Lemma modular_base_system_field : @field digits eq zero one opp add_opt sub_opt (carry_mul_opt k_ c_) inv div. Proof. - eapply (Field.isomorphism_to_subfield_field (phi := decode) (fieldR := PrimeFieldTheorems.field_modulo (prime_q := prime_modulus))). + eapply (Field.isomorphism_to_subfield_field (phi := decode)). Grab Existential Variables. + intros; eapply encode_rep. + intros; eapply encode_rep. @@ -55,9 +52,7 @@ Section ModularBaseSystemField. + intros; eapply sub_decode. + intros; eapply add_decode. + intros; eapply encode_rep. - + cbv [eq zero one]. erewrite !encode_rep. intro A. - eapply (PrimeFieldTheorems.Fq_1_neq_0 (prime_q := prime_modulus)). - congruence. + + eapply _zero_neq_one. + trivial. + repeat intro. cbv [div]. congruence. + repeat intro. cbv [inv]. congruence. @@ -65,7 +60,6 @@ Section ModularBaseSystemField. + repeat intro. cbv [eq]. erewrite !sub_decode. congruence. + repeat intro. cbv [eq]. erewrite !add_decode. congruence. + repeat intro. cbv [opp]. congruence. - + cbv [eq]. auto using ModularArithmeticTheorems.F_eq_dec. Qed. End ModularBaseSystemField.
\ No newline at end of file diff --git a/src/ModularArithmetic/ModularBaseSystemList.v b/src/ModularArithmetic/ModularBaseSystemList.v index c556427b9..f8d78a438 100644 --- a/src/ModularArithmetic/ModularBaseSystemList.v +++ b/src/ModularArithmetic/ModularBaseSystemList.v @@ -16,7 +16,7 @@ Section Defs. Local Notation base := (base_from_limb_widths limb_widths). Local Notation "u [ i ]" := (nth_default 0 u i). - Definition decode (us : digits) : F modulus := ZToField (BaseSystem.decode base us). + Definition decode (us : digits) : F modulus := ZToField _ (BaseSystem.decode base us). Definition encode (x : F modulus) := encodeZ limb_widths x. diff --git a/src/ModularArithmetic/ModularBaseSystemProofs.v b/src/ModularArithmetic/ModularBaseSystemProofs.v index d740cca17..720fa8ea1 100644 --- a/src/ModularArithmetic/ModularBaseSystemProofs.v +++ b/src/ModularArithmetic/ModularBaseSystemProofs.v @@ -21,6 +21,8 @@ Require Export Crypto.Util.FixCoqMistakes. Local Open Scope Z_scope. Local Opaque add_to_nth carry_simple. +Local Arguments ZToField {_} _. +Import ModularArithmeticTheorems.Zmod PrimeFieldTheorems.Zmod. Section PseudoMersenneProofs. Context `{prm :PseudoMersenneBaseParams}. @@ -232,7 +234,7 @@ Section PseudoMersenneProofs. rewrite BaseSystemProofs.sub_rep, BaseSystemProofs.add_rep. rewrite ZToField_sub, ZToField_add, ZToField_mod. apply Fdecode_decode_mod in mm_spec; cbv [BaseSystem.decode] in *. - rewrite mm_spec, F_add_0_l. + rewrite mm_spec. rewrite Algebra.left_identity. f_equal; assumption. Qed. @@ -297,11 +299,11 @@ Section CarryProofs. specialize_by eauto. cbv [ModularBaseSystemList.carry]. break_if; subst; eauto. - apply F_eq. + apply eq_ZToField_iff. rewrite to_list_from_list. apply carry_decode_eq_reduce. auto. cbv [ModularBaseSystemList.decode]. - apply ZToField_eqmod. + apply eq_ZToField_iff. rewrite to_list_from_list, carry_simple_decode_eq; try omega; distr_length; auto. Qed. Hint Resolve carry_rep. diff --git a/src/ModularArithmetic/Pre.v b/src/ModularArithmetic/Pre.v index 8566d30ab..7320b16bf 100644 --- a/src/ModularArithmetic/Pre.v +++ b/src/ModularArithmetic/Pre.v @@ -119,8 +119,8 @@ Program Definition inv_impl {m : BinNums.Z} : forall a : {z : BinNums.Z | z = z mod m}, a <> exist (fun z : BinNums.Z => z = z mod m) (0 mod m) (Z_mod_mod 0 m) -> exist (fun z : BinNums.Z => z = z mod m) - ((proj1_sig a * proj1_sig (inv0 a)) mod m) - (Z_mod_mod (proj1_sig a * proj1_sig (inv0 a)) m) = + ((proj1_sig (inv0 a) * proj1_sig a) mod m) + (Z_mod_mod (proj1_sig (inv0 a) * proj1_sig a) m) = exist (fun z : BinNums.Z => z = z mod m) (1 mod m) (Z_mod_mod 1 m))} := mod_inv_sig. Next Obligation. @@ -130,7 +130,7 @@ Next Obligation. assert (Hm':0 <= m - 2) by (pose proof prime_ge_2 m Hm; omega). assert (Ha:a mod m<>0) by (intro; apply Ha', exist_reduced_eq; congruence). cbv [proj1_sig mod_inv_sig]. - transitivity ((a*powmod m a (Z.to_N (m - 2))) mod m); [destruct a; congruence|]. + transitivity ((a*powmod m a (Z.to_N (m - 2))) mod m); [destruct a; f_equal; ring|]. rewrite !powmod_Zpow_mod. rewrite Z2N.id by assumption. rewrite Zmult_mod_idemp_r. diff --git a/src/ModularArithmetic/PrimeFieldTheorems.v b/src/ModularArithmetic/PrimeFieldTheorems.v index 8d47e36ed..c97bde495 100644 --- a/src/ModularArithmetic/PrimeFieldTheorems.v +++ b/src/ModularArithmetic/PrimeFieldTheorems.v @@ -10,568 +10,171 @@ Require Import Coq.ZArith.BinInt Coq.NArith.BinNat Coq.ZArith.ZArith Coq.ZArith. Require Import Coq.Logic.Eqdep_dec. Require Import Crypto.Util.NumTheoryUtil Crypto.Util.ZUtil. Require Import Crypto.Util.Tactics. +Require Import Crypto.Util.Decidable. Require Export Crypto.Util.FixCoqMistakes. Require Crypto.Algebra. +Import Crypto.ModularArithmetic.ModularArithmeticTheorems.Zmod. Existing Class prime. -Lemma F_inv_spec : forall {m}, inv 0%F = (0%F : F m) - /\ (prime m -> forall a0 : F m, a0 <> 0%F -> (a0 * inv a0)%F = 1%F). -Proof. - intros m. - pose (@inv_with_spec m) as H. - change (@inv m) with (proj1_sig H). - destruct H; eauto. -Qed. - -Section FieldModuloPre. - Context {q:Z} {prime_q:prime q}. - Local Open Scope F_scope. - - Lemma Fq_1_neq_0 : (1:F q) <> (0:F q). - Proof. - pose proof prime_ge_2 q _. - rewrite F_eq, !FieldToZ_ZToField, !Zmod_small by omega; congruence. - Qed. - - Lemma F_mul_inv_r : forall x : F q, x <> 0 -> x * inv x = 1. - Proof. - intros. - edestruct @F_inv_spec; eauto. - Qed. - - Lemma F_mul_inv_l : forall x : F q, x <> 0 -> inv x * x = 1. - Proof. - intros. - edestruct @F_inv_spec as [Ha Hb]; eauto. - erewrite <-Hb; eauto. - Fdefn. - Qed. - - (* Add an abstract field (without modifiers) *) - Definition Ffield_theory : field_theory 0%F 1%F (@add q) (@mul q) (@sub q) (@opp q) (@div q) (@inv q) eq. - Proof. - constructor; auto using Fring_theory, Fq_1_neq_0, F_mul_inv_l. - Qed. - - Global Instance field_modulo : @Algebra.field (F q) Logic.eq (ZToField 0) (ZToField 1) opp add sub mul inv div. - Proof. - constructor; try solve_proper. - - apply commutative_ring_modulo. - - split. auto using F_mul_inv_l. - - split. auto using Fq_1_neq_0. - Qed. -End FieldModuloPre. - -Module Type PrimeModulus. - Parameter modulus : Z. - Parameter prime_modulus : prime modulus. -End PrimeModulus. - -Module FieldModulo (Import M : PrimeModulus). - (* Add our field with all the fixin's *) - Module Import RingM := RingModulo M. - Definition field_theory_modulo := @Ffield_theory modulus prime_modulus. - Add Field Ffield_Z : field_theory_modulo - (morphism ring_morph_modulo, - preprocess [Fpreprocess], - postprocess [Fpostprocess], - constants [Fconstant], - div morph_div_theory_modulo, - power_tac power_theory_modulo [Fexp_tac]). -End FieldModulo. - -Section VariousModPrime. - Context {q:Z} {prime_q:prime q}. - Local Open Scope F_scope. - Add Field Ffield_Z : (@Ffield_theory q _) - (morphism (@Fring_morph q), - preprocess [Fpreprocess], - postprocess [Fpostprocess; try exact Fq_1_neq_0; try assumption], - constants [Fconstant], - div (@Fmorph_div_theory q), - power_tac (@Fpower_theory q) [Fexp_tac]). - - Lemma Fq_mul_eq : forall x y z : F q, z <> 0 -> x * z = y * z -> x = y. - Proof. - intros ? ? ? z_nonzero mul_z_eq. - assert (x * z * inv z = y * z * inv z) as H by (rewrite mul_z_eq; reflexivity). - replace (x * z * inv z) with (x * (z * inv z)) in H by (field; trivial). - replace (y * z * inv z) with (y * (z * inv z)) in H by (field; trivial). - rewrite F_mul_inv_r in H by assumption. - replace (x * 1) with x in H by field. - replace (y * 1) with y in H by field. - trivial. - Qed. - - Lemma Fq_mul_eq_l : forall x y z : F q, z <> 0 -> z * x = z * y -> x = y. - Proof. - intros ? ? ? Hz Heq. - apply (Fq_mul_eq _ _ z); auto. - apply (Fq_sub_eq _ _ _ _ Heq); ring. - Qed. - - Lemma Fq_inv_unique' : forall - inv1 (inv1ok: inv1 0 = 0 /\ forall x : F q, x <> 0 -> x * inv1 x = 1) - inv2 (inv2ok: inv2 0 = 0 /\ forall x : F q, x <> 0 -> x * inv2 x = 1), - forall x, inv1 x = inv2 x. - Proof. - intros inv1 [inv1_0 inv1_x] inv2 [inv2_0 inv2_x] x. - destruct (F_eq_dec x 0) as [H|H]; [congruence|]. - apply (Fq_mul_eq_l _ _ x H). rewrite inv1_x, inv2_x; trivial. - Qed. - - Lemma Fq_inv_unique : forall - inv' (inv'ok: inv' 0 = 0 /\ forall x : F q, x <> 0 -> x * inv' x = 1), - forall x, inv x = inv' x. - Proof. - intros ? [? ?] ?. - pose proof (@F_inv_spec q) as [? ?]. - eauto using Fq_inv_unique'. - Qed. - - Lemma Fq_mul_zero_why : forall a b : F q, a*b = 0 -> a = 0 \/ b = 0. - intros. - assert (Z := F_eq_dec a 0); destruct Z. - - - left; intuition. - - - assert (a * b / a = 0) by - ( rewrite H; field; intuition ). - - replace (a*b/a) with (b) in H0 by (field; trivial). - right; intuition. - Qed. - - Lemma Fq_mul_nonzero_nonzero : forall a b : F q, a <> 0 -> b <> 0 -> a*b <> 0. - intros; intuition; subst. - apply Fq_mul_zero_why in H1. - destruct H1; subst; intuition. - Qed. - Hint Resolve Fq_mul_nonzero_nonzero. - - Lemma Fq_pow_zero : forall (p: N), p <> 0%N -> (0^p = @ZToField q 0)%F. - induction p using N.peano_ind; - rewrite <-?N.add_1_l, ?(proj2 (@F_pow_spec q _) _), ?(proj1 (@F_pow_spec q _)). - - intuition. - - intro H. apply F_mul_0_l. - Qed. - - Lemma Fq_root_zero : forall (x: F q) (p: N), x^p = 0 -> x = 0. - induction p using N.peano_ind; - rewrite <-?N.add_1_l, ?(proj2 (@F_pow_spec q _) _), ?(proj1 (@F_pow_spec q _)). - - intros; destruct Fq_1_neq_0; auto. - - intro H; destruct (Fq_mul_zero_why x (x^p) H); auto. - Qed. - - Lemma Fq_root_nonzero : forall (x:F q) p, x^p <> 0 -> (p <> 0)%N -> x <> 0. - induction p using N.peano_ind; - rewrite <-?N.add_1_l, ?(proj2 (@F_pow_spec q _) _), ?(proj1 (@F_pow_spec q _)). - - intuition. - - destruct (N.eq_dec p 0); intro H; intros; subst. - + rewrite (proj1 (@F_pow_spec q _)) in H; replace (x*1) with (x) in H by ring; trivial. - + apply IHp; auto. intro Hz; rewrite Hz in *. apply H, F_mul_0_r. - Qed. - - Lemma Fq_pow_nonzero : forall (x : F q) p, x <> 0 -> x^p <> 0. - Proof. - induction p using N.peano_ind; - rewrite <-?N.add_1_l, ?(proj2 (@F_pow_spec q _) _), ?(proj1 (@F_pow_spec q _)). - - intuition. auto using Fq_1_neq_0. - - intros H Hc. destruct (Fq_mul_zero_why _ _ Hc). - + intuition. - + apply IHp; auto. - Qed. - - Lemma F_inv_0 : inv 0 = (0 : F q). - Proof. - destruct (@F_inv_spec q); auto. - Qed. - - Definition inv_fermat (x:F q) : F q := x ^ Z.to_N (q - 2)%Z. - Lemma Fq_inv_fermat: 2 < q -> forall x : F q, inv x = x ^ Z.to_N (q - 2)%Z. - Proof. - intros. - erewrite (Fq_inv_unique inv_fermat); trivial; split; intros; unfold inv_fermat. - { replace 2%N with (Z.to_N (Z.of_N 2))%N by auto. - rewrite Fq_pow_zero. reflexivity. intro. - assert (Z.of_N (Z.to_N (q-2)) = 0%Z) by (rewrite H0; eauto); rewrite Z2N.id in *; omega. } - { clear x. rename x0 into x. pose proof (fermat_inv _ _ x) as Hf; forward Hf. - { pose proof @ZToField_FieldToZ; pose proof @ZToField_mod; congruence. } - specialize (Hf H1); clear H1. - rewrite <-(ZToField_FieldToZ x). - rewrite ZToField_pow. - replace (Z.of_N (Z.to_N (q - 2))) with (q-2)%Z by (rewrite Z2N.id ; omega). - rewrite <-ZToField_mul. - apply ZToField_eqmod. - rewrite Hf, Zmod_small by omega; reflexivity. - } - Qed. - Lemma Fq_inv_fermat_correct : 2 < q -> forall x : F q, inv_fermat x = inv x. - Proof. - unfold inv_fermat; intros. rewrite Fq_inv_fermat; auto. - Qed. - - Let inv_fermat_powmod (x:Z) : Z := powmod q x (Z.to_N (q-2)). - Lemma FieldToZ_inv_efficient : 2 < q -> - forall x : F q, FieldToZ (inv x) = inv_fermat_powmod x. - Proof. - unfold inv_fermat_powmod; intros. - rewrite Fq_inv_fermat, powmod_Zpow_mod, <-FieldToZ_pow_Zpow_mod; auto. - Qed. +Module Zmod. + Section Field. + Context (q:Z) {prime_q:prime q}. + Lemma inv_spec : inv 0%F = (0%F : F q) + /\ (prime q -> forall x : F q, x <> 0%F -> (inv x * x)%F = 1%F). + Proof. change (@inv q) with (proj1_sig (@inv_with_spec q)); destruct (@inv_with_spec q); eauto. Qed. + + Lemma inv_0 : inv 0 = ZToField q 0. Proof. destruct inv_spec; auto. Qed. + Lemma inv_nonzero (x:F q) : (x <> 0 -> inv x * x%F = 1)%F. Proof. destruct inv_spec; auto. Qed. + + Global Instance field_modulo : @Algebra.field (F q) Logic.eq 0%F 1%F opp add sub mul inv div. + Proof. + repeat match goal with + | _ => solve [ solve_proper + | apply commutative_ring_modulo + | apply inv_nonzero + | cbv [not]; pose proof prime_ge_2 q prime_q; + rewrite Zmod.eq_FieldToZ_iff, !Zmod.FieldToZ_ZToField, !Zmod_small; omega ] + | _ => split + end. + Qed. - Lemma F_minus_swap : forall x y : F q, x - y = 0 -> y - x = 0. - Proof. - intros ? ? eq_zero. - replace x with (x - y + y); try ring. - rewrite eq_zero. - ring. - Qed. + Definition field_theory : field_theory 0%F 1%F add mul sub opp div inv eq + := Algebra.Field.field_theory_for_stdlib_tactic. + End Field. + + (** A field tactic hook that can be imported *) + Module Type PrimeModulus. + Parameter modulus : Z. + Parameter prime_modulus : prime modulus. + End PrimeModulus. + Module FieldModulo (Export M : PrimeModulus). + Module Import RingM := RingModulo M. + Add Field _field : (field_theory modulus) + (morphism (ring_morph modulus), + constants [is_constant], + div (morph_div_theory modulus), + power_tac (power_theory modulus) [is_pow_constant]). + End FieldModulo. + + Section NumberThoery. + Context {q:Z} {prime_q:prime q} {two_lt_q: 2 < q}. + Local Open Scope F_scope. + Add Field _field : (field_theory q) + (morphism (ring_morph q), + constants [is_constant], + div (morph_div_theory q), + power_tac (power_theory q) [is_pow_constant]). + + Lemma FieldToZ_1 : @FieldToZ q 1 = 1%Z. + Proof. simpl. rewrite Zmod_small; omega. Qed. + + Lemma Fq_inv_fermat (x:F q) : inv x = x ^ Z.to_N (q - 2)%Z. + Proof. + destruct (dec (x = 0%F)) as [?|Hnz]; [subst x; rewrite inv_0|]. + { admit. } + erewrite <-Algebra.Field.inv_unique; try reflexivity. + rewrite eq_FieldToZ_iff, FieldToZ_mul, FieldToZ_pow, Z2N.id, FieldToZ_1 by omega. + apply (fermat_inv q _ (FieldToZ x)); rewrite mod_FieldToZ; eapply FieldToZ_nonzero; trivial. + Qed. - Lemma Fq_square_mul : forall x y z : F q, (y <> 0) -> - x ^ 2 = z * y ^ 2 -> exists sqrt_z, sqrt_z ^ 2 = z. - Proof. - intros ? ? ? y_nonzero A. - exists (x / y). - assert ((x / y) ^ 2 = x ^ 2 / y ^ 2) as square_distr_div by (field; trivial). - assert (y ^ 2 <> 0) as y2_nonzero by ( - change (2%N) with (1+(1+0))%N; - rewrite !(proj2 (@F_pow_spec q _) _), !(proj1 (@F_pow_spec q _)); - auto 10 using Fq_mul_nonzero_nonzero, Fq_1_neq_0). - rewrite (Fq_mul_eq _ z (y ^ 2)); auto. - rewrite <- A. - field; trivial. - Qed. + (* TODO: move to number thoery util *) + Lemma odd_as_div a : Z.odd a = true -> a = (2*(a/2) + 1)%Z. + Proof. + rewrite Zodd_mod, <-Zeq_is_eq_bool; intro H_1; rewrite <-H_1. + apply Z_div_mod_eq; reflexivity. + Qed. + + Lemma euler_criterion (a : F q) (a_nonzero : a <> 0) : + (a ^ (Z.to_N (q / 2)) = 1) <-> (exists b, b*b = a). + Proof. + pose proof FieldToZ_nonzero_range a; pose proof (odd_as_div q). + specialize_by ltac:(destruct (Z.prime_odd_or_2 _ prime_q); try omega; trivial). + rewrite eq_FieldToZ_iff, !FieldToZ_pow, !FieldToZ_1, !Z2N.id by omega. + rewrite square_iff, <-(euler_criterion (q/2)) by (trivial || omega); reflexivity. + Qed. - Lemma Fq_square_mul_sub : forall x y z : F q, - 0 = z * y ^ 2 - x ^ 2 -> (exists sqrt_z, sqrt_z ^ 2 = z) \/ x = 0. - Proof. - intros ? ? ? eq_zero_sub. - destruct (F_eq_dec y 0). { + Global Instance Decidable_square (x:F q) : Decidable (exists y, y*y = x). + Proof. + destruct (dec (x = 0)). + { left. abstract (exists 0; subst; ring). } + { eapply Decidable_iff_to_impl; [eapply euler_criterion; assumption | exact _]. } + Defined. + End NumberThoery. + + Section SquareRootsPrime5Mod8. + Context {q:Z} {prime_q: prime q} {q_5mod8 : q mod 8 = 5}. + + (* This is always true, but easier to check by computation than to prove *) + Context (sqrt_minus1_valid : ((ZToField q 2 ^ Z.to_N (q / 4)) ^ 2 = opp 1)%F). + Local Open Scope F_scope. + Add Field _field2 : (field_theory q) + (morphism (ring_morph q), + constants [is_constant], + div (morph_div_theory q), + power_tac (power_theory q) [is_pow_constant]). + + Let sqrt_minus1 : F q := ZToField _ 2 ^ Z.to_N (q / 4). + + Lemma two_lt_q_5mod8 : 2 < q. + Proof. + pose proof (prime_ge_2 q _) as two_le_q. + apply Zle_lt_or_eq in two_le_q. + destruct two_le_q; auto. subst_max. - rewrite Fq_pow_zero in eq_zero_sub by congruence. - rewrite F_mul_0_r in eq_zero_sub. - assert (x ^ 2 = 0 - x ^ 2 + x ^ 2) as minus_plus_x2 by (rewrite <- eq_zero_sub; ring). - assert (x ^ 2 = 0) as x2_zero by (rewrite minus_plus_x2; ring). - apply Fq_root_zero in x2_zero. - right; auto. - } { - left. - eapply Fq_square_mul; eauto. - instantiate (1 := x). - assert (x ^ 2 = z * y ^ 2 - x ^ 2 + x ^ 2) as plus_minus_x2 by - (rewrite <- eq_zero_sub; ring). - rewrite plus_minus_x2; ring. - } - Qed. - - Lemma F_div_mul : forall x y z : F q, y <> 0 -> (z = (x / y) <-> z * y = x). - Proof. - split; intros; subst; field. - Qed. - - Lemma F_div_1_r : forall x : F q, (x/1)%F = x. - Proof. - intros; field. (* TODO: Warning: Collision between bound variables ... *) - Qed. - - Lemma F_div_opp_1 : forall x y : F q, (opp x / y = opp (x / y))%F. - Proof. - intros; destruct (F_eq_dec y 0); [subst;unfold div;rewrite !F_inv_0|]; field. - Qed. - - Lemma F_eq_opp_zero : forall x : F q, 2 < q -> (x = opp x <-> x = 0). - Proof. - split; intro A. - + pose proof (F_opp_spec x) as opp_spec. - rewrite <- A in opp_spec. - replace (x + x) with (ZToField 2 * x) in opp_spec by ring. - apply Fq_mul_zero_why in opp_spec. - destruct opp_spec as [eq_2_0 | ?]; auto. - apply F_eq in eq_2_0. - rewrite FieldToZ_ZToField in eq_2_0. - replace (FieldToZ 0) with 0%Z in eq_2_0 by auto. - replace (2 mod q) with 2 in eq_2_0; try discriminate. - symmetry; apply Z.mod_small; omega. - + subst. - rewrite <- (F_opp_spec 0) at 1. - ring. - Qed. - - Lemma euler_criterion_F : forall (a : F q) (q_odd : 2 < q) (a_nonzero : a <> 0), - (a ^ (Z.to_N (q / 2)) = 1) <-> isSquare a. - Proof. - (*pose proof q_odd.*) - split; intros A. { - apply square_Zmod_F; auto. - eapply euler_criterion; omega || auto. - + apply div2_p_1mod4; auto; omega. - + pose proof (FieldToZ_nonzero_range a a_nonzero); omega. - + replace (q / 2)%Z with (Z.of_N (Z.to_N (q / 2))) - by (apply Z2N.id; apply Z.div_pos; prime_bound). - rewrite FieldToZ_pow_Zpow_mod by omega. - rewrite A. - replace (FieldToZ 1) with (1 mod q) by auto. - apply Z.mod_1_l; omega. - } { - apply F_eq. - rewrite <- FieldToZ_pow_Zpow_mod by omega. - rewrite Z2N.id by (apply Z.div_pos; omega). - replace (FieldToZ 1) with 1%Z - by (rewrite FieldToZ_ZToField at 1; symmetry; apply Zmod_1_l; omega). - apply euler_criterion; try prime_bound; auto. - + apply div2_p_1mod4; auto; omega. - + pose proof (FieldToZ_nonzero_range a a_nonzero); omega. - + apply square_Zmod_F; auto. - } - Qed. - - Lemma euler_criterion_if' : forall (a : F q) (q_odd : 2 < q), - if (orb (F_eqb a 0) (F_eqb (a ^ (Z.to_N (q / 2))) 1)) - then (isSquare a) else (forall b, b ^ 2 <> a). - Proof. - unfold orb; intros. - rewrite <- if_F_eq_dec_if_F_eqb. - do 2 break_if; try congruence. - + subst; exists 0; apply Fq_pow_zero; congruence. - + unfold isSquare; apply F_eqb_eq in Heqb; apply euler_criterion_F; eauto. - + intros b b_id. - apply F_eqb_neq in Heqb. - assert (isSquare a) as a_square by (eexists; eauto). - apply euler_criterion_F in a_square; auto. - Qed. - - Lemma euler_criterion_if : forall (a : F q) (q_odd : 2 < q), - if (a =? 0) || (powmod q a (Z.to_N (q / 2)) =? 1) - then (isSquare a) else (forall b, b ^ 2 <> a). - Proof. - intros. - pose proof (euler_criterion_if' a q_odd) as H. - unfold F_eqb in H. - rewrite !FieldToZ_ZToField, !@FieldToZ_pow_efficient, !Zmod_small in H by omega; assumption. - Qed. - - Lemma sqrt_solutions : forall x y : F q, y ^ 2 = x ^ 2 -> y = x \/ y = opp x. - Proof. - intros ? ? squares_eq. - remember (y - x) as z. - replace y with (x + z) in * by (rewrite Heqz; ring). - replace (x ^ 2) with (0 + x ^ 2) in squares_eq by ring. - replace ((x + z) ^ 2) with (z * (x + (x + z)) + x ^ 2) in squares_eq by ring. - apply F_add_reg_r in squares_eq. - apply Fq_mul_zero_why in squares_eq. - destruct squares_eq as [? | z_2x_0]; [ left; subst; ring | right ]. - pose proof (F_opp_spec x) as opp_spec. - rewrite <- z_2x_0 in opp_spec. - apply F_add_reg_l in opp_spec; auto. - Qed. - - Global Instance Fq_Ring_ops : @Ring_ops (F q) 0 1 add mul sub opp eq. - Global Instance Fq_Ring: @Ring (F q) 0 1 add mul sub opp eq Fq_Ring_ops. - Proof. - econstructor; eauto with typeclass_instances; - unfold R2, equality, eq_notation, addition, add_notation, one, one_notation, - multiplication, mul_notation, zero, zero_notation, subtraction, - sub_notation, opposite, opp_notation; intros; ring. + discriminate. Qed. - Global Instance Fq_Cring: @Cring (F q) 0 1 add mul sub opp eq Fq_Ring_ops Fq_Ring. - Proof. - repeat intro. apply F_mul_comm. - Qed. - - Global Instance Fq_Integral_domain : @Integral_domain (F q) 0 1 add mul sub opp eq Fq_Ring_ops Fq_Ring Fq_Cring. - Proof. - econstructor; eauto using Fq_mul_zero_why, Fq_1_neq_0. - Qed. - - Lemma add_cancel_mul_r_nonzero {y : F q} (H : y <> 0) (x z : F q) - : x * y + z = (x + (z * (inv y))) * y. - Proof. field. Qed. - - Lemma sub_cancel_mul_r_nonzero {y : F q} (H : y <> 0) (x z : F q) - : x * y - z = (x - (z * (inv y))) * y. - Proof. field. Qed. - - Lemma add_cancel_l_nonzero {y : F q} (H : y <> 0) (z : F q) - : y + z = (1 + (z * (inv y))) * y. - Proof. field. Qed. - - Lemma sub_cancel_l_nonzero {y : F q} (H : y <> 0) (z : F q) - : y - z = (1 - (z * (inv y))) * y. - Proof. field. Qed. -End VariousModPrime. - -Section SquareRootsPrime5Mod8. - Context {q:Z} {prime_q: prime q} {q_5mod8 : q mod 8 = 5}. - - (* This is always true, but easier to check by computation than to prove *) - Context (sqrt_minus1_valid : ((ZToField 2 ^ Z.to_N (q / 4)) ^ 2 = @opp q 1)%F). - - Local Open Scope F_scope. - Add Field Ffield_8mod5 : (@Ffield_theory q _) - (morphism (@Fring_morph q), - preprocess [Fpreprocess], - postprocess [Fpostprocess; try exact Fq_1_neq_0; try assumption], - constants [Fconstant], - div (@Fmorph_div_theory q), - power_tac (@Fpower_theory q) [Fexp_tac]). - - (* This is only the square root of -1 if q mod 8 is 3 or 5 *) - Definition sqrt_minus1 : F q := ZToField 2 ^ Z.to_N (q / 4). - - Lemma two_lt_q_5mod8 : 2 < q. - Proof. - pose proof (prime_ge_2 q _) as two_le_q. - apply Zle_lt_or_eq in two_le_q. - destruct two_le_q; auto. - subst_max. - discriminate. - Qed. - - (* square root mod q relies on the fact that q is 5 mod 8 *) - Definition sqrt_mod_q (a : F q) := - let b := a ^ Z.to_N (q / 8 + 1) in - (match (F_eq_dec (b ^ 2) a) with - | left A => b - | right A => (sqrt_minus1 * b)%F - end). - - Lemma eq_b4_a2 : forall x : F q, isSquare x -> - ((x ^ Z.to_N (q / 8 + 1)) ^ 2) ^ 2 = x ^ 2. - Proof. - intros. - destruct (F_eq_dec x 0). { - subst. - repeat rewrite Fq_pow_zero; try (intuition; discriminate). - intro false_eq. - assert (0 <= q / 8)%Z by zero_bounds. - assert (0 < q / 8 + 1) by omega. - replace 0%N with (Z.to_N 0) in * by auto. - apply Z2N.inj in false_eq; omega. - } { - rewrite F_pow_compose. - replace (2 * 2)%N with 4%N by auto. - rewrite F_pow_compose. - replace (4 * Z.to_N (q / 8 + 1))%N with (Z.to_N (q / 2 + 2))%N. + Definition sqrt_5mod8 (a : F q) : F q := + let b := a ^ Z.to_N (q / 8 + 1) in + if dec (b ^ 2 = a) + then b + else sqrt_minus1 * b. + + Lemma eq_b4_a2 (x : F q) (Hex:exists y, y*y = x) : + ((x ^ Z.to_N (q / 8 + 1)) ^ 2) ^ 2 = x ^ 2. + Proof. + pose proof two_lt_q_5mod8. + assert (0 <= q/8)%Z by (apply Z.div_le_lower_bound; rewrite ?Z.mul_0_r; omega). + assert (Z.to_N (q / 8 + 1) <> 0%N) by + (intro Hbad; change (0%N) with (Z.to_N 0%Z) in Hbad; rewrite Z2N.inj_iff in Hbad; omega). + destruct (dec (x = 0)); [subst; rewrite !pow_0_l by (trivial || lazy_decide); reflexivity|]. + rewrite !pow_pow_l. + + replace (Z.to_N (q / 8 + 1) * (2*2))%N with (Z.to_N (q / 2 + 2))%N. + Focus 2. { (* this is a boring but gnarly proof :/ *) + change (2*2)%N with (Z.to_N 4). + rewrite <- Z2N.inj_mul by zero_bounds. + apply Z2N.inj_iff; try zero_bounds. + rewrite <- Z.mul_cancel_l with (p := 2) by omega. + ring_simplify. + rewrite Z.mul_div_eq by omega. + rewrite Z.mul_div_eq by omega. + rewrite (Zmod_div_mod 2 8 q) by + (try omega; apply Zmod_divide; omega || auto). + rewrite q_5mod8. + replace (5 mod 2)%Z with 1%Z by auto. + ring. + } Unfocus. + + rewrite Z2N.inj_add, pow_add_r by zero_bounds. + replace (x ^ Z.to_N (q / 2)) with (@ZToField q 1) by + (symmetry; apply @euler_criterion; eauto). + change (Z.to_N 2) with 2%N; ring. + Qed. - Focus 2. - replace 4%N with (Z.to_N 4) by auto. - rewrite <- Z2N.inj_mul by zero_bounds. - apply Z2N.inj_iff; try zero_bounds. - rewrite <- Z.mul_cancel_l with (p := 2) by omega. + Lemma sqrt_5mod8_valid : forall x, (exists y, y*y = x) -> + (sqrt_5mod8 x)*(sqrt_5mod8 x) = x. + Proof. + intros x x_square. + pose proof (eq_b4_a2 x x_square) as Hyy; rewrite !pow_2_r in Hyy. + destruct (Algebra.only_two_square_roots_choice _ x (x*x) Hyy eq_refl) as [Hb|Hb]; clear Hyy; + unfold sqrt_5mod8; break_if; rewrite !@pow_2_r in *; intuition. ring_simplify. - rewrite Z.mul_div_eq by omega. - rewrite Z.mul_div_eq by omega. - rewrite (Zmod_div_mod 2 8 q) by - (try omega; apply Zmod_divide; omega || auto). - rewrite q_5mod8. - replace (5 mod 2)%Z with 1%Z by auto. - ring. - (* End Focus *) - - rewrite Z2N.inj_add by zero_bounds. - rewrite <- F_pow_add by zero_bounds. - replace (x ^ Z.to_N (q / 2)) with (@ZToField q 1). - replace (Z.to_N 2) with 2%N by auto. - ring. - - symmetry; apply euler_criterion_F; auto using two_lt_q_5mod8. - } - Qed. - - Lemma sqrt_mod_q_valid : forall x, isSquare x -> - (sqrt_mod_q x) ^ 2 = x. - Proof. - intros x x_square. - destruct (sqrt_solutions x _ (eq_b4_a2 x x_square)) as [? | eq_b2_oppx]; - unfold sqrt_mod_q; break_if; intuition. - ring_simplify. - unfold sqrt_minus1. - rewrite sqrt_minus1_valid. - rewrite eq_b2_oppx. - field. - Qed. - - Lemma sqrt_mod_q_of_0 : sqrt_mod_q 0 = 0. - Proof. - unfold sqrt_mod_q. - rewrite !Fq_pow_zero. - break_if; ring. - - congruence. - intro false_eq. - rewrite <-(N2Z.id 0) in false_eq. - rewrite N2Z.inj_0 in false_eq. - pose proof (prime_ge_2 q prime_q). - apply Z2N.inj in false_eq; zero_bounds. - assert (0 < q / 8 + 1)%Z. - apply Z.add_nonneg_pos; zero_bounds. - omega. - Qed. - - Lemma sqrt_mod_q_root_0 : forall x : F q, sqrt_mod_q x = 0 -> x = 0. - Proof. - unfold sqrt_mod_q; intros. - break_if. - - match goal with [ H : ?sqrt_x ^ 2 = x, H' : ?sqrt_x = 0 |- _ ] => rewrite <-H, H' end. + unfold sqrt_minus1; rewrite @pow_2_r. + rewrite sqrt_minus1_valid; rewrite @pow_2_r. + rewrite Hb. ring. - - match goal with - | [H : sqrt_minus1 * _ = 0 |- _ ]=> - apply Fq_mul_zero_why in H; destruct H as [sqrt_minus1_zero | ? ]; - [ | eapply Fq_root_zero; eauto ] - end. - unfold sqrt_minus1 in sqrt_minus1_zero. - rewrite sqrt_minus1_zero in sqrt_minus1_valid. - exfalso. - pose proof (@F_opp_spec q 1) as opp_spec_1. - rewrite <-sqrt_minus1_valid in opp_spec_1. - assert (((1 + 0 ^ 2) : F q) = (1 : F q)) as ring_subst by ring. - rewrite ring_subst in *. - apply Fq_1_neq_0; assumption. - Qed. - -End SquareRootsPrime5Mod8. - -Local Open Scope F_scope. -(** Tactics for solving inequalities. *) -Ltac solve_cancel_by_field y tnz := - solve [ generalize dependent y; intros; - field; tnz ]. - -Ltac cancel_nonzero_factors' tnz := - idtac; - match goal with - | [ |- ?x = 0 -> False ] - => change (x <> 0) - | [ |- ?x * ?y <> 0 ] - => apply Fq_mul_nonzero_nonzero - | [ H : ?y <> 0 |- _ ] - => progress rewrite ?(add_cancel_mul_r_nonzero H), ?(sub_cancel_mul_r_nonzero H), ?(add_cancel_l_nonzero H), ?(sub_cancel_l_nonzero H); - apply Fq_mul_nonzero_nonzero; [ | assumption ] - | [ |- ?op (?y * (ZToField (m := ?q) ?n)) ?z <> 0 ] - => unique assert (ZToField (m := q) n <> 0) by tnz; - generalize dependent (ZToField (m := q) n); intros - | [ |- ?op (?x * (?y * ?z)) _ <> 0 ] - => rewrite F_mul_assoc - end. -Ltac cancel_nonzero_factors tnz := repeat cancel_nonzero_factors' tnz. -Ltac specialize_quantified_equalities := - repeat match goal with - | [ H : forall _ _ _ _, _ = _ -> _, H' : _ = _ |- _ ] - => unique pose proof (fun x2 y2 => H _ _ x2 y2 H') - | [ H : forall _ _, _ = _ -> _, H' : _ = _ |- _ ] - => unique pose proof (H _ _ H') - end. -Ltac finish_inequality tnz := - idtac; - match goal with - | [ H : ?x <> 0 |- ?y <> 0 ] - => replace y with x by (field; tnz); exact H - end. -Ltac field_nonzero tnz := - cancel_nonzero_factors tnz; - try (specialize_quantified_equalities; - progress cancel_nonzero_factors tnz); - try solve [ specialize_quantified_equalities; - finish_inequality tnz ]. + Qed. + End SquareRootsPrime5Mod8. +End Zmod.
\ No newline at end of file diff --git a/src/ModularArithmetic/Tutorial.v b/src/ModularArithmetic/Tutorial.v index 7d354ab3e..999c61971 100644 --- a/src/ModularArithmetic/Tutorial.v +++ b/src/ModularArithmetic/Tutorial.v @@ -11,17 +11,16 @@ Section Mod24. Let q := 24. (* Boilerplate for letting Z numbers be interpreted as field elements *) - Let ZToFq := ZToField : BinNums.Z -> F q. Hint Unfold ZToFq. Local Coercion ZToFq : Z >-> F. + Let ZToFq := ZToField _ : BinNums.Z -> F q. Hint Unfold ZToFq. Local Coercion ZToFq : Z >-> F. (* Boilerplate for [ring]. Similar boilerplate works for [field] if the modulus is prime . *) - Add Ring Fring_q : (@Fring_theory q) - (morphism (@Fring_morph q), - preprocess [unfold ZToFq; Fpreprocess], - postprocess [Fpostprocess; try exact Fq_1_neq_0; try assumption], - constants [Fconstant], - div (@Fmorph_div_theory q), - power_tac (@Fpower_theory q) [Fexp_tac]). + Add Ring _theory : (Zmod.ring_theory q) + (morphism (Zmod.ring_morph q), + preprocess [unfold ZToFq], + constants [Zmod.is_constant], + div (Zmod.morph_div_theory q), + power_tac (Zmod.power_theory q) [Zmod.is_pow_constant]). Lemma sumOfSquares : forall a b: F q, (a+b)^2 = a^2 + 2*a*b + b^2. Proof. @@ -39,34 +38,33 @@ Section Modq. Local Open Scope F_scope. (* Boilerplate for letting Z numbers be interpreted as field elements *) - Let ZToFq := ZToField : BinNums.Z -> F q. Hint Unfold ZToFq. Local Coercion ZToFq : Z >-> F. + Let ZToFq := ZToField _ : BinNums.Z -> F q. Hint Unfold ZToFq. Local Coercion ZToFq : Z >-> F. (* Boilerplate for [field]. Similar boilerplate works for [ring] if the modulus is not prime . *) - Add Field Ffield_q' : (@Ffield_theory q _) - (morphism (@Fring_morph q), - preprocess [unfold ZToFq; Fpreprocess], - postprocess [Fpostprocess; try exact Fq_1_neq_0; try assumption], - constants [Fconstant], - div (@Fmorph_div_theory q), - power_tac (@Fpower_theory q) [Fexp_tac]). - - Lemma sumOfSquares' : forall a b c: F q, c <> 0 -> ((a+b)/c)^2 = a^2/c^2 + ZToField 2*(a/c)*(b/c) + b^2/c^2. + Add Field _theory' : (Zmod.field_theory q) + (morphism (Zmod.ring_morph q), + preprocess [unfold ZToFq], + constants [Zmod.is_constant], + div (Zmod.morph_div_theory q), + power_tac (Zmod.power_theory q) [Zmod.is_pow_constant]). + + Lemma sumOfSquares' : forall a b c: F q, c <> 0 -> ((a+b)/c)^2 = a^2/c^2 + 2*(a/c)*(b/c) + b^2/c^2. Proof. intros. - field. + field; trivial. Qed. End Modq. (*** The old way: Modules ***) -Module Modulus31 <: PrimeModulus. +Module Modulus31 <: Zmod.PrimeModulus. Definition modulus := 2^5 - 1. Lemma prime_modulus : prime modulus. Admitted. End Modulus31. -Module Modulus127 <: PrimeModulus. +Module Modulus127 <: Zmod.PrimeModulus. Definition modulus := 2^127 - 1. Lemma prime_modulus : prime modulus. Admitted. @@ -74,14 +72,14 @@ End Modulus127. Module Example31. (* Then we can construct a field with that modulus *) - Module Import Field := FieldModulo Modulus31. + Module Import Field := Zmod.FieldModulo Modulus31. Import Modulus31. (* And pull in the appropriate notations *) Local Open Scope F_scope. (* First, let's solve a ring example*) - Lemma ring_example: forall x: F modulus, x * (ZToField 2) = x + x. + Lemma ring_example: forall x: F modulus, x * (ZToField _ 2) = x + x. Proof. intros. ring. @@ -92,7 +90,7 @@ Module Example31. Therefore, it is necessary to explicitly rewrite the modulus (usually hidden by implicitn arguments) match the one passed to [FieldModulo]. *) - Lemma ring_example': forall x: F (2^5-1), x * (ZToField 2) = x + x. + Lemma ring_example': forall x: F (2^5-1), x * (ZToField _ 2) = x + x. Proof. intros. change (2^5-1)%Z with modulus. @@ -108,7 +106,7 @@ Module Example31. Qed. (* Then an example with exponentiation *) - Lemma exp_example: forall x: F modulus, x ^ 2 + ZToField 2 * x + 1 = (x + 1) ^ 2. + Lemma exp_example: forall x: F modulus, x ^ 2 + ZToField _ 2 * x + 1 = (x + 1) ^ 2. Proof. intros; simpl. field; trivial. @@ -143,7 +141,7 @@ End Example31. (* Notice that the field tactics work whether we know what the modulus is *) Module TimesZeroTransparentTestModule. - Module Import Theory := FieldModulo Modulus127. + Module Import Theory := Zmod.FieldModulo Modulus127. Import Modulus127. Local Open Scope F_scope. @@ -153,9 +151,13 @@ Module TimesZeroTransparentTestModule. Qed. End TimesZeroTransparentTestModule. -(* Or if we don't (i.e. it's opaque) *) -Module TimesZeroParametricTestModule (M: PrimeModulus). - Module Theory := FieldModulo M. +(* An opaque modulus causes the field tactic to expand all constants + into matches on the modulus. Goals can still be proven, but with + significant overhead. Consider using an entirely abstract + [Algebra.field] instead. *) + +Module TimesZeroParametricTestModule (M: Zmod.PrimeModulus). + Module Theory := Zmod.FieldModulo M. Import Theory M. Local Open Scope F_scope. @@ -164,26 +166,27 @@ Module TimesZeroParametricTestModule (M: PrimeModulus). field. Qed. - Lemma realisticFraction : forall x y d : F modulus, (x * 1 + y * 0) / (1 + d * x * 0 * y * 1) = x. + Lemma realisticFraction : forall x y d : F modulus, 1 <> ZToField modulus 0 -> (x * 1 + y * 0) / (1 + d * x * 0 * y * 1) = x. Proof. intros. - field; try exact Fq_1_neq_0. + field; assumption. Qed. Lemma biggerFraction : forall XP YP ZP TP XQ YQ ZQ TQ d : F modulus, + 1 <> ZToField modulus 0 -> ZQ <> 0 -> ZP <> 0 -> ZP * ZQ * ZP * ZQ + d * XP * XQ * YP * YQ <> 0 -> - ZP * ZToField 2 * ZQ * (ZP * ZQ) + XP * YP * ZToField 2 * d * (XQ * YQ) <> 0 -> - ZP * ZToField 2 * ZQ * (ZP * ZQ) - XP * YP * ZToField 2 * d * (XQ * YQ) <> 0 -> + ZP * ZToField _ 2 * ZQ * (ZP * ZQ) + XP * YP * ZToField _ 2 * d * (XQ * YQ) <> 0 -> + ZP * ZToField _ 2 * ZQ * (ZP * ZQ) - XP * YP * ZToField _ 2 * d * (XQ * YQ) <> 0 -> ((YP + XP) * (YQ + XQ) - (YP - XP) * (YQ - XQ)) * - (ZP * ZToField 2 * ZQ - XP * YP / ZP * ZToField 2 * d * (XQ * YQ / ZQ)) / - ((ZP * ZToField 2 * ZQ - XP * YP / ZP * ZToField 2 * d * (XQ * YQ / ZQ)) * - (ZP * ZToField 2 * ZQ + XP * YP / ZP * ZToField 2 * d * (XQ * YQ / ZQ))) = + (ZP * ZToField _ 2 * ZQ - XP * YP / ZP * ZToField _ 2 * d * (XQ * YQ / ZQ)) / + ((ZP * ZToField _ 2 * ZQ - XP * YP / ZP * ZToField _ 2 * d * (XQ * YQ / ZQ)) * + (ZP * ZToField _ 2 * ZQ + XP * YP / ZP * ZToField _ 2 * d * (XQ * YQ / ZQ))) = (XP / ZP * (YQ / ZQ) + YP / ZP * (XQ / ZQ)) / (1 + d * (XP / ZP) * (XQ / ZQ) * (YP / ZP) * (YQ / ZQ)). Proof. intros. - field; assumption. + field; repeat split; assumption. Qed. End TimesZeroParametricTestModule. diff --git a/src/Spec/ModularArithmetic.v b/src/Spec/ModularArithmetic.v index fc506f61d..16584c683 100644 --- a/src/Spec/ModularArithmetic.v +++ b/src/Spec/ModularArithmetic.v @@ -35,7 +35,7 @@ Section FieldOperations. Definition inv_with_spec : { inv : F m -> F m | inv zero = zero /\ ( Znumtheory.prime m -> - forall a, a <> zero -> mul a (inv a) = one ) + forall a, a <> zero -> mul (inv a) a = one ) } := Pre.inv_impl. Definition inv : F m -> F m := Eval hnf in proj1_sig inv_with_spec. Definition div (a b:F m) : F m := mul a (inv b). @@ -49,7 +49,7 @@ End FieldOperations. Delimit Scope F_scope with F. Arguments F _%Z. -Arguments ZToField {_} _%Z : simpl never. +Arguments ZToField _%Z _%Z : simpl never, clear implicits. Arguments add {_} _%F _%F : simpl never. Arguments mul {_} _%F _%F : simpl never. Arguments sub {_} _%F _%F : simpl never. @@ -57,11 +57,10 @@ Arguments div {_} _%F _%F : simpl never. Arguments pow {_} _%F _%N : simpl never. Arguments inv {_} _%F : simpl never. Arguments opp {_} _%F : simpl never. -Local Open Scope F_scope. Infix "+" := add : F_scope. Infix "*" := mul : F_scope. Infix "-" := sub : F_scope. Infix "/" := div : F_scope. Infix "^" := pow : F_scope. -Notation "0" := (ZToField 0) : F_scope. -Notation "1" := (ZToField 1) : F_scope. +Notation "0" := (ZToField _ 0) : F_scope. +Notation "1" := (ZToField _ 1) : F_scope.
\ No newline at end of file diff --git a/src/Spec/ModularWordEncoding.v b/src/Spec/ModularWordEncoding.v index acd2bedbd..86546a22f 100644 --- a/src/Spec/ModularWordEncoding.v +++ b/src/Spec/ModularWordEncoding.v @@ -18,7 +18,7 @@ Section ModularWordEncoding. Definition Fm_dec (x_ : word sz) : option (F m) := let z := Z.of_N (wordToN (x_)) in if Z_lt_dec z m - then Some (ZToField z) + then Some (ZToField m z) else None . @@ -37,4 +37,4 @@ Section ModularWordEncoding. @ModularWordEncodingPre.Fm_encoding_canonical m sz bound_check }. -End ModularWordEncoding. +End ModularWordEncoding.
\ No newline at end of file diff --git a/src/Spec/WeierstrassCurve.v b/src/Spec/WeierstrassCurve.v index 7ec5d99ec..e2c99a8fe 100644 --- a/src/Spec/WeierstrassCurve.v +++ b/src/Spec/WeierstrassCurve.v @@ -11,8 +11,8 @@ Module E. Context {F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv} `{Algebra.field F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv}. Local Infix "=" := Feq : type_scope. Local Notation "a <> b" := (not (a = b)) : type_scope. - Local Infix "=?" := Algebra.eq_dec (at level 70, no associativity) : type_scope. - Local Notation "x =? y" := (Sumbool.bool_of_sumbool (Algebra.eq_dec x y)) : bool_scope. + Local Notation "x =? y" := (Decidable.dec (Feq x y)) (at level 70, no associativity) : type_scope. + Local Notation "x =? y" := (Sumbool.bool_of_sumbool (Decidable.dec (Feq x y))) : bool_scope. Local Infix "+" := Fadd. Local Infix "*" := Fmul. Local Infix "-" := Fsub. Local Infix "/" := Fdiv. Local Notation "- x" := (Fopp x). diff --git a/src/Specific/GF1305.v b/src/Specific/GF1305.v index fba77a4a8..b1500b5c9 100644 --- a/src/Specific/GF1305.v +++ b/src/Specific/GF1305.v @@ -11,6 +11,7 @@ Require Import Crypto.Tactics.VerdiTactics. Require Import Crypto.Util.ZUtil. Require Import Crypto.Util.Tuple. Require Import Crypto.Util.Notations. +Require Import Crypto.Util.Decidable. Require Import Crypto.Algebra. Import ListNotations. Require Import Coq.ZArith.ZArith Coq.ZArith.Zpower Coq.ZArith.ZArith Coq.ZArith.Znumtheory. @@ -35,8 +36,7 @@ Definition mul2modulus : fe1305 := Instance subCoeff : SubtractionCoefficient modulus params1305. apply Build_SubtractionCoefficient with (coeff := mul2modulus). - apply ZToField_eqmod. - cbv; reflexivity. + vm_decide. Defined. Definition freezePreconditions1305 : freezePreconditions params1305 int_width. diff --git a/src/Specific/GF25519.v b/src/Specific/GF25519.v index 7ece3a5da..b0323c4a0 100644 --- a/src/Specific/GF25519.v +++ b/src/Specific/GF25519.v @@ -11,6 +11,7 @@ Require Import Crypto.Tactics.VerdiTactics. Require Import Crypto.Util.ZUtil. Require Import Crypto.Util.Tuple. Require Import Crypto.Util.Notations. +Require Import Crypto.Util.Decidable. Require Import Crypto.Algebra. Import ListNotations. Require Import Coq.ZArith.ZArith Coq.ZArith.Zpower Coq.ZArith.ZArith Coq.ZArith.Znumtheory. @@ -33,8 +34,7 @@ Definition mul2modulus : fe25519 := Instance subCoeff : SubtractionCoefficient modulus params25519. apply Build_SubtractionCoefficient with (coeff := mul2modulus). - apply ZToField_eqmod. - cbv; reflexivity. + vm_decide. Defined. Definition freezePreconditions25519 : freezePreconditions params25519 int_width. diff --git a/src/Util/AdditionChainExponentiation.v b/src/Util/AdditionChainExponentiation.v index ca1394115..6a028dda8 100644 --- a/src/Util/AdditionChainExponentiation.v +++ b/src/Util/AdditionChainExponentiation.v @@ -5,98 +5,53 @@ Require Import VerdiTactics. Require Import Crypto.Util.Option. Section AddChainExp. - Function add_chain (is:list (nat*nat)) : list nat := + Function fold_chain {T} (id:T) (op:T->T->T) (is:list (nat*nat)) (acc:list T) {struct is} : T := match is with - | nil => nil + | nil => + match acc with + | nil => id + | ret::_ => ret + end | (i,j)::is' => - let chain' := add_chain is' in - nth_default 1 chain' i + nth_default 1 chain' j::chain' + let ijx := op (nth_default id acc i) (nth_default id acc j) in + fold_chain id op is' (ijx::acc) end. -Example wikipedia_addition_chain : add_chain (rev [ -(0, 0); (* 2 = 1 + 1 *) (* the indices say how far back the chain to look *) -(0, 1); (* 3 = 2 + 1 *) -(0, 0); (* 6 = 3 + 3 *) -(0, 0); (* 12 = 6 + 6 *) -(0, 0); (* 24 = 12 + 12 *) -(0, 2); (* 30 = 24 + 6 *) -(0, 6)] (* 31 = 30 + 1 *) -) = [31; 30; 24; 12; 6; 3; 2]. reflexivity. Qed. + Example wikipedia_addition_chain : fold_chain 0 plus [ + (0, 0); (* 2 = 1 + 1 *) (* the indices say how far back the chain to look *) + (0, 1); (* 3 = 2 + 1 *) + (0, 0); (* 6 = 3 + 3 *) + (0, 0); (* 12 = 6 + 6 *) + (0, 0); (* 24 = 12 + 12 *) + (0, 2); (* 30 = 24 + 6 *) + (0, 6)] (* 31 = 30 + 1 *) + [1] = 31. reflexivity. Qed. Context {G eq op id} {monoid:@Algebra.monoid G eq op id}. + Context {scalarmult} {is_scalarmult:@ScalarMult.is_scalarmult G eq op id scalarmult}. Local Infix "=" := eq : type_scope. - Function add_chain_exp (is : list (nat*nat)) (x : G) : list G := - match is with - | nil => nil - | (i,j)::is' => - let chain' := add_chain_exp is' x in - op (nth_default x chain' i) (nth_default x chain' j) ::chain' - end. - - Fixpoint scalarmult n (x : G) : G := match n with - | O => id - | S n' => op x (scalarmult n' x) - end. - - Lemma add_chain_exp_step : forall i j is x, - (forall n, nth_default x (add_chain_exp is x) n = scalarmult (nth_default 1 (add_chain is) n) x) -> - (eqlistA eq) - (add_chain_exp ((i,j) :: is) x) - (op (scalarmult (nth_default 1 (add_chain is) i) x) - (scalarmult (nth_default 1 (add_chain is) j) x) :: add_chain_exp is x). - Proof. - intros. - unfold add_chain_exp; fold add_chain_exp. - apply eqlistA_cons; [ | reflexivity]. - f_equiv; auto. - Qed. - - Lemma scalarmult_same : forall c x y, eq x y -> eq (scalarmult c x) (scalarmult c y). - Proof. - induction c; intros. - + reflexivity. - + simpl. f_equiv; auto. - Qed. - - Lemma scalarmult_pow_add : forall a b x, scalarmult (a + b) x = op (scalarmult a x) (scalarmult b x). + Lemma fold_chain_exp' : forall (x:G) is acc ref + (H:forall i, nth_default id acc i = scalarmult (nth_default 0 ref i) x) + (Hl:Logic.eq (length acc) (length ref)), + fold_chain id op is acc = scalarmult (fold_chain 0 plus is ref) x. Proof. - intros; eapply scalarmult_add_l. - Grab Existential Variables. - 2:eauto. - econstructor; try reflexivity. - repeat intro; subst. - auto using scalarmult_same. + induction is; intros; simpl @fold_chain. + { repeat break_match; specialize (H 0); rewrite ?nth_default_cons, ?nth_default_cons_S in H; + solve [ simpl length in *; discriminate | apply H | rewrite scalarmult_0_l; reflexivity ]. } + { repeat break_match. eapply IHis; intros. + { match goal with + [H:context [nth_default _ ?l _] |- context[nth_default _ (?h::?l) ?i] ] + => destruct i; rewrite ?nth_default_cons, ?nth_default_cons_S; + solve [ apply H | rewrite !H, <-scalarmult_add_l; reflexivity ] + end. } + { auto with distr_length. } } Qed. - Lemma add_chain_exp_spec : forall is x, - (forall n, nth_default x (add_chain_exp is x) n = scalarmult (nth_default 1 (add_chain is) n) x). + Lemma fold_chain_exp x is: fold_chain id op is [x] = scalarmult (fold_chain 0 plus is [1]) x. Proof. - induction is; intros. - + simpl; rewrite !nth_default_nil. cbv. - symmetry; apply right_identity. - + destruct a. - rewrite add_chain_exp_step by auto. - unfold add_chain; fold add_chain. - destruct n. - - rewrite !nth_default_cons, scalarmult_pow_add. reflexivity. - - rewrite !nth_default_cons_S; auto. + eapply fold_chain_exp'; intros; trivial. + destruct i; try destruct i; rewrite ?nth_default_cons_S, ?nth_default_cons, ?nth_default_nil; + rewrite ?scalarmult_1_l, ?scalarmult_0_l; reflexivity. Qed. - - Lemma add_chain_exp_answer : forall is x n, Logic.eq (head (add_chain is)) (Some n) -> - option_eq eq (Some (scalarmult n x)) (head (add_chain_exp is x)). - Proof. - intros. - change head with (fun {T} (xs : list T) => nth_error xs 0) in *. - cbv beta in *. - cbv [option_eq]. - destruct is; [ discriminate | ]. - destruct p. - simpl in *. - injection H; clear H; intro H. - subst n. - rewrite !add_chain_exp_spec. - apply scalarmult_pow_add. - Qed. - End AddChainExp.
\ No newline at end of file diff --git a/src/Util/Decidable.v b/src/Util/Decidable.v index 8488ad303..3988701a8 100644 --- a/src/Util/Decidable.v +++ b/src/Util/Decidable.v @@ -4,10 +4,13 @@ Require Import Coq.Logic.Eqdep_dec. Require Import Crypto.Util.Sigma. Require Import Crypto.Util.HProp. Require Import Crypto.Util.Equality. +Require Import Coq.ZArith.BinInt. +Require Import Coq.NArith.BinNat. Local Open Scope type_scope. Class Decidable (P : Prop) := dec : {P} + {~P}. +Arguments dec _%type_scope {_}. Notation DecidableRel R := (forall x y, Decidable (R x y)). @@ -86,11 +89,13 @@ Hint Extern 0 (Decidable (~?A)) => apply (@dec_not A) : typeclass_instances. Global Instance dec_eq_unit : DecidableRel (@eq unit) | 10. exact _. Defined. Global Instance dec_eq_bool : DecidableRel (@eq bool) | 10. exact _. Defined. Global Instance dec_eq_Empty_set : DecidableRel (@eq Empty_set) | 10. exact _. Defined. -Global Instance dec_eq_nat : DecidableRel (@eq nat) | 10. exact _. Defined. Global Instance dec_eq_prod {A B} `{DecidableRel (@eq A), DecidableRel (@eq B)} : DecidableRel (@eq (A * B)) | 10. exact _. Defined. Global Instance dec_eq_sum {A B} `{DecidableRel (@eq A), DecidableRel (@eq B)} : DecidableRel (@eq (A + B)) | 10. exact _. Defined. Global Instance dec_eq_sigT_hprop {A P} `{DecidableRel (@eq A), forall a : A, IsHProp (P a)} : DecidableRel (@eq (@sigT A P)) | 10. exact _. Defined. Global Instance dec_eq_sig_hprop {A} {P : A -> Prop} `{DecidableRel (@eq A), forall a : A, IsHProp (P a)} : DecidableRel (@eq (@sig A P)) | 10. exact _. Defined. +Global Instance dec_eq_nat : DecidableRel (@eq nat) | 10. exact _. Defined. +Global Instance dec_eq_N : DecidableRel (@eq N) | 10 := N.eq_dec. +Global Instance dec_eq_Z : DecidableRel (@eq Z) | 10 := Z.eq_dec. Lemma Decidable_respects_iff A B (H : A <-> B) : (Decidable A -> Decidable B) * (Decidable B -> Decidable A). Proof. solve_decidable_transparent. Defined. @@ -101,5 +106,14 @@ Proof. solve_decidable_transparent. Defined. Lemma Decidable_iff_to_flip_impl A B (H : A <-> B) : Decidable B -> Decidable A. Proof. solve_decidable_transparent. Defined. +Lemma dec_bool : forall {P} {Pdec:Decidable P}, (if dec P then true else false) = true -> P. +Proof. intros. destruct dec; solve [ auto | discriminate ]. Qed. + +Ltac vm_decide := apply dec_bool; vm_compute; reflexivity. +Ltac lazy_decide := apply dec_bool; lazy; reflexivity. + +Ltac vm_decide_no_check := apply dec_bool; vm_cast_no_check (eq_refl true). +Ltac lazy_decide_no_check := apply dec_bool; exact_no_check (eq_refl true). + (** For dubious compatibility with [eauto using]. *) Hint Extern 2 (Decidable _) => progress unfold Decidable : typeclass_instances core. diff --git a/src/Util/NumTheoryUtil.v b/src/Util/NumTheoryUtil.v index 29fedaa9b..8b8595bb7 100644 --- a/src/Util/NumTheoryUtil.v +++ b/src/Util/NumTheoryUtil.v @@ -95,13 +95,13 @@ Proof. apply in_mod_ZPGroup; auto. Qed. -Lemma fermat_inv : forall a, a mod p <> 0 -> (a * (a^(p-2) mod p)) mod p = 1. +Lemma fermat_inv : forall a, a mod p <> 0 -> ((a^(p-2) mod p) * a) mod p = 1. Proof. intros. pose proof (prime_ge_2 _ prime_p). - rewrite Zmult_mod_idemp_r. - replace (a * a ^ (p - 2)) with (a^(p-1)). - 2:replace (a * a ^ (p - 2)) with (a^1 * a ^ (p - 2)) by ring. + rewrite Zmult_mod_idemp_l. + replace (a ^ (p - 2) * a) with (a^(p-1)). + 2:replace (a ^ (p - 2) * a) with (a^1 * a ^ (p - 2)) by ring. 2:rewrite <-Zpower_exp; try f_equal; omega. auto using fermat_little. Qed. diff --git a/src/WeierstrassCurve/Pre.v b/src/WeierstrassCurve/Pre.v index c51c82e89..aeffc3a2b 100644 --- a/src/WeierstrassCurve/Pre.v +++ b/src/WeierstrassCurve/Pre.v @@ -2,6 +2,7 @@ Require Import Coq.Classes.Morphisms. Require Coq.Setoids.Setoid. Require Import Crypto.Algebra. Require Import Crypto.Util.Tactics. Require Import Crypto.Util.Notations. +Require Import Crypto.Util.Decidable. Local Open Scope core_scope. @@ -34,8 +35,8 @@ Section Pre. Definition unifiedAdd' (P1' P2':F*F + ∞) : F*F + ∞ := match P1', P2' with | (x1, y1), (x2, y2) - => if x1 =? x2 then - if y2 =? -y1 then + => if dec (x1 = x2) then + if dec (y2 = -y1) then ∞ else ((3*x1^2+a)^2 / (2*y1)^2 - x1 - x1, (2*x1+x1)*(3*x1^2+a) / (2*y1) - (3*x1^2+a)^3/(2*y1)^3-y1) |