diff options
| author |  Andres Erbsen <andreser@mit.edu> | 2016-07-28 18:40:28 -0400 |
|---|---|---|
| committer | Andres Erbsen <andreser@mit.edu> | 2016-08-04 11:47:51 -0400 |
| commit | 4964f1ff2d40ba08573deddca56140c4ac4b19eb (patch) | |
| tree | 61b24623e414dfa3e09a32cf62e8acd1909dae37 /src | |
| parent | fbb0f64892560322ed9dcd0f664e730e74de9b4e (diff) | |
Refactor ModularArithmetic into Zmod, expand Decidable
ModularArithmetic now uses Algebra lemmas in various places instead of
custom manual proofs. Similarly, Util.Decidable is used to state and
prove the relevant decidability results.
Backwards-incompatible changes:
F_some_lemma -> Zmod.some_lemma
Arguments ZToField _%Z _%Z : clear implicits.
inv_spec says inv x * x = 1, not x * inv x = 1
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) |