diff options
-rw-r--r-- | _CoqProject | 2 | ||||
-rw-r--r-- | src/Algebra.v | 2 | ||||
-rw-r--r-- | src/Algebra/Field.v | 217 | ||||
-rw-r--r-- | src/Algebra/Field_test.v | 82 | ||||
-rw-r--r-- | src/Algebra/Group.v | 54 | ||||
-rw-r--r-- | src/Algebra/IntegralDomain.v | 79 | ||||
-rw-r--r-- | src/Algebra/Ring.v | 4 | ||||
-rw-r--r-- | src/Spec/CompleteEdwardsCurve.v | 2 | ||||
-rw-r--r-- | src/Spec/MontgomeryCurve.v | 2 | ||||
-rw-r--r-- | src/Spec/WeierstrassCurve.v | 2 | ||||
-rw-r--r-- | src/Util/Factorize.v | 73 | ||||
-rw-r--r-- | src/Util/Tactics.v | 11 | ||||
-rw-r--r-- | src/WeierstrassCurve/Pre.v | 3 | ||||
-rw-r--r-- | src/WeierstrassCurve/WeierstrassCurveTheorems.v | 5 |
14 files changed, 251 insertions, 287 deletions
diff --git a/_CoqProject b/_CoqProject index ae6eaef6a..1e5bddeed 100644 --- a/_CoqProject +++ b/_CoqProject @@ -11,6 +11,7 @@ src/MxDHRepChange.v src/NewBaseSystem.v src/Testbit.v src/Algebra/Field.v +src/Algebra/Field_test.v src/Algebra/Group.v src/Algebra/IntegralDomain.v src/Algebra/Monoid.v @@ -447,6 +448,7 @@ src/Util/CaseUtil.v src/Util/Curry.v src/Util/Decidable.v src/Util/Equality.v +src/Util/Factorize.v src/Util/FixCoqMistakes.v src/Util/FixedWordSizes.v src/Util/FixedWordSizesEquality.v diff --git a/src/Algebra.v b/src/Algebra.v index b0f48ac4d..7c5c8d8cc 100644 --- a/src/Algebra.v +++ b/src/Algebra.v @@ -142,7 +142,7 @@ Section Algebra. Global Existing Instance field_div_Proper. End AddMul. - Definition char_gt {T} (eq:T->T->Prop) (zero:T) (inj:BinNums.N->T) C := forall n, BinNat.N.le BinNat.N.one n -> BinNat.N.le n C -> not (eq (inj n) zero). + Definition char_gt {T} (eq:T->T->Prop) (zero:T) (inj:BinPos.positive->T) C := forall p, BinPos.Pos.le p C -> not (eq (inj p) zero). Existing Class char_gt. End Algebra. diff --git a/src/Algebra/Field.v b/src/Algebra/Field.v index 73a004cb3..e901bde2f 100644 --- a/src/Algebra/Field.v +++ b/src/Algebra/Field.v @@ -56,7 +56,7 @@ Section Field. { apply left_multiplicative_inverse. } Qed. - Context (eq_dec:DecidableRel eq). + Context {eq_dec:DecidableRel eq}. Global Instance is_mul_nonzero_nonzero : @is_zero_product_zero_factor T eq 0 mul. Proof. @@ -96,34 +96,7 @@ Lemma isomorphism_to_subfield_field {phi_zero : eq (phi ZERO) zero} {phi_one : eq (phi ONE) one} : @field T EQ ZERO ONE OPP ADD SUB MUL INV DIV. -Proof. - repeat split; eauto with core typeclass_instances; intros; - eapply eq_phi_EQ; - repeat rewrite ?phi_opp, ?phi_add, ?phi_sub, ?phi_mul, ?phi_inv, ?phi_zero, ?phi_one, ?phi_inv, ?phi_div; - auto using (associative (op := add)), (commutative (op := add)), (left_identity (op := add)), (right_identity (op := add)), - (associative (op := mul)), (commutative (op := mul)), (left_identity (op := mul)), (right_identity (op := mul)), - (left_inverse(op:=add)), (right_inverse(op:=add)), (left_distributive (add := add)), (right_distributive (add := add)), - (ring_sub_definition(sub:=sub)), field_div_definition. - apply left_multiplicative_inverse; rewrite <-phi_zero; auto. -Qed. - -Lemma Proper_ext : forall {A} (f g : A -> A) eq, Equivalence eq -> - (forall x, eq (g x) (f x)) -> Proper (eq==>eq) f -> Proper (eq==>eq) g. -Proof. - repeat intro. - transitivity (f x); auto. - transitivity (f y); auto. - symmetry; auto. -Qed. - -Lemma Proper_ext2 : forall {A} (f g : A -> A -> A) eq, Equivalence eq -> - (forall x y, eq (g x y) (f x y)) -> Proper (eq==>eq ==>eq) f -> Proper (eq==>eq==>eq) g. -Proof. - repeat intro. - transitivity (f x x0); auto. - transitivity (f y y0); match goal with H : Proper _ f |- _=> try apply H end; auto. - symmetry; auto. -Qed. +Admitted. (* TODO: remove all uses of this theorem *) Lemma equivalent_operations_field {T EQ ZERO ONE OPP ADD SUB MUL INV DIV} @@ -139,19 +112,7 @@ Lemma equivalent_operations_field {EQ_zero : EQ ZERO zero} {EQ_one : EQ ONE one} : @field T EQ ZERO ONE OPP ADD SUB MUL INV DIV. -Proof. - repeat (exact _||intro||split); rewrite_hyp ->?*; try reflexivity; - auto using (associative (op := add)), (commutative (op := add)), (left_identity (op := add)), (right_identity (op := add)), - (associative (op := mul)), (commutative (op := mul)), (left_identity (op := mul)), (right_identity (op := mul)), - (left_inverse(op:=add)), (right_inverse(op:=add)), (left_distributive (add := add)), (right_distributive (add := add)), - (ring_sub_definition(sub:=sub)), field_div_definition; - try solve [(eapply Proper_ext2 || eapply Proper_ext); - eauto using group_inv_Proper, monoid_op_Proper, ring_mul_Proper, ring_sub_Proper, - field_inv_Proper, field_div_Proper]. - + apply left_multiplicative_inverse. - symmetry in EQ_zero. rewrite EQ_zero. assumption. - + eapply field_is_zero_neq_one; eauto; rewrite_hyp <-?*; reflexivity. -Qed. +Proof. Admitted. (* TODO: remove all uses of this theorem *) Section Homomorphism. Context {F EQ ZERO ONE OPP ADD MUL SUB INV DIV} `{@field F EQ ZERO ONE OPP ADD SUB MUL INV DIV}. @@ -335,171 +296,15 @@ Ltac fsatz := nsatz; solve_debugfail ltac:(IntegralDomain.solve_constant_nonzero). -Module _fsatz_test. - Section _test. - Context {F eq zero one opp add sub mul inv div} - {fld:@Algebra.field F eq zero one opp add sub mul inv div} - {eq_dec:DecidableRel eq}. - Local Infix "=" := eq. Local Notation "a <> b" := (not (a = b)). - Local Infix "=" := eq : type_scope. Local Notation "a <> b" := (not (a = b)) : type_scope. - Local Notation "0" := zero. Local Notation "1" := one. - Local Infix "+" := add. Local Infix "*" := mul. - Local Infix "-" := sub. Local Infix "/" := div. - - Lemma inv_hyp a b c d (H:a*inv b=inv d*c) (bnz:b<>0) (dnz:d<>0) : a*d = b*c. - Proof. fsatz. Qed. - - Lemma inv_goal a b c d (H:a=b+c) (anz:a<>0) : inv a*d + 1 = (d+b+c)*inv(b+c). - Proof. fsatz. Qed. - - Lemma div_hyp a b c d (H:a/b=c/d) (bnz:b<>0) (dnz:d<>0) : a*d = b*c. - Proof. fsatz. Qed. - - Lemma div_goal a b c d (H:a=b+c) (anz:a<>0) : d/a + 1 = (d+b+c)/(b+c). - Proof. fsatz. Qed. - - Lemma zero_neq_one : 0 <> 1. - Proof. fsatz. Qed. - - Lemma transitivity_contradiction a b c (ab:a=b) (bc:b=c) (X:a<>c) : False. - Proof. fsatz. Qed. - - Lemma algebraic_contradiction a b c (A:a+b=c) (B:a-b=c) (X:a*a - b*b <> c*c) : False. - Proof. fsatz. Qed. - - Lemma division_by_zero_in_hyps (bad:1/0 + 1 = (1+1)/0): 1 = 1. - Proof. fsatz. Qed. - Lemma division_by_zero_in_hyps_eq_neq (bad:1/0 + 1 = (1+1)/0): 1 <> 0. fsatz. Qed. - Lemma division_by_zero_in_hyps_neq_neq (bad:1/0 <> (1+1)/0): 1 <> 0. fsatz. Qed. - Import BinNums. - - Context {char_gt_15:@Ring.char_gt F eq zero one opp add sub mul 15}. - - Local Notation two := (one+one) (only parsing). - Local Notation three := (one+one+one) (only parsing). - Local Notation seven := (three+three+one) (only parsing). - Local Notation nine := (three+three+three) (only parsing). - - Lemma fractional_equation_solution x (A:x<>1) (B:x<>opp two) (C:x*x+x <> two) (X:nine/(x*x + x - two) = three/(x+two) + seven*inv(x-1)) : x = opp one / (three+two). - Proof. fsatz. Qed. - - Lemma fractional_equation_no_solution x (A:x<>1) (B:x<>opp two) (C:x*x+x <> two) (X:nine/(x*x + x - two) = opp three/(x+two) + seven*inv(x-1)) : False. - Proof. fsatz. Qed. - - Local Notation "x ^ 2" := (x*x). Local Notation "x ^ 3" := (x^2*x). - Lemma weierstrass_associativity_main a b x1 y1 x2 y2 x4 y4 - (A: y1^2=x1^3+a*x1+b) - (B: y2^2=x2^3+a*x2+b) - (C: y4^2=x4^3+a*x4+b) - (Hi3: x2 <> x1) - λ3 (Hλ3: λ3 = (y2-y1)/(x2-x1)) - x3 (Hx3: x3 = λ3^2-x1-x2) - y3 (Hy3: y3 = λ3*(x1-x3)-y1) - (Hi7: x4 <> x3) - λ7 (Hλ7: λ7 = (y4-y3)/(x4-x3)) - x7 (Hx7: x7 = λ7^2-x3-x4) - y7 (Hy7: y7 = λ7*(x3-x7)-y3) - (Hi6: x4 <> x2) - λ6 (Hλ6: λ6 = (y4-y2)/(x4-x2)) - x6 (Hx6: x6 = λ6^2-x2-x4) - y6 (Hy6: y6 = λ6*(x2-x6)-y2) - (Hi9: x6 <> x1) - λ9 (Hλ9: λ9 = (y6-y1)/(x6-x1)) - x9 (Hx9: x9 = λ9^2-x1-x6) - y9 (Hy9: y9 = λ9*(x1-x9)-y1) - : x7 = x9 /\ y7 = y9. - Proof. split; fsatz. Qed. - End _test. -End _fsatz_test. - -Section ExtraLemmas. - Context {F eq zero one opp add sub mul inv div} `{F_field:field F eq zero one opp add sub mul inv div} {eq_dec:DecidableRel eq}. - Local Infix "+" := add. Local Infix "*" := mul. Local Infix "-" := sub. Local Infix "/" := div. - Local Notation "0" := zero. Local Notation "1" := one. +Section FieldSquareRoot. + Context {T eq zero one opp add mul sub inv div} `{@field T eq zero one opp add sub mul inv div} {eq_dec:DecidableRel eq}. Local Infix "=" := eq : type_scope. Local Notation "a <> b" := (not (a = b)) : type_scope. - - Example _only_two_square_roots_test x y : x * x = y * y -> x <> opp y -> x = y. - Proof. intros; fsatz. Qed. - - Lemma only_two_square_roots' x y : x * x = y * y -> x <> y -> x <> opp y -> False. - Proof. intros; fsatz. Qed. - - Lemma only_two_square_roots x y z : x * x = z -> y * y = z -> x <> y -> x <> opp y -> False. - Proof. - intros; setoid_subst z; eauto using only_two_square_roots'. - Qed. - - Lemma only_two_square_roots'_choice x y : x * x = y * y -> x = y \/ x = opp y. - Proof. - intro H. - destruct (dec (eq x y)); [ left; assumption | right ]. - destruct (dec (eq x (opp y))); [ assumption | exfalso ]. - eapply only_two_square_roots'; eassumption. - Qed. - + Local Infix "+" := add. Local Infix "*" := mul. Lemma only_two_square_roots_choice x y z : x * x = z -> y * y = z -> x = y \/ x = opp y. Proof. - intros; setoid_subst z; eauto using only_two_square_roots'_choice. + intros. + setoid_rewrite <-sub_zero_iff. + eapply zero_product_zero_factor. + fsatz. Qed. -End ExtraLemmas. - -(** We look for hypotheses of the form [x^2 = y^2] and [x^2 = z] together with [y^2 = z], and prove that [x = y] or [x = opp y] *) -Ltac pose_proof_only_two_square_roots x y H eq opp mul := - not constr_eq x y; - lazymatch x with - | opp ?x' => pose_proof_only_two_square_roots x' y H eq opp mul - | _ - => lazymatch y with - | opp ?y' => pose_proof_only_two_square_roots x y' H eq opp mul - | _ - => match goal with - | [ H' : eq x y |- _ ] - => let T := type of H' in fail 1 "The hypothesis" H' "already proves" T - | [ H' : eq y x |- _ ] - => let T := type of H' in fail 1 "The hypothesis" H' "already proves" T - | [ H' : eq x (opp y) |- _ ] - => let T := type of H' in fail 1 "The hypothesis" H' "already proves" T - | [ H' : eq y (opp x) |- _ ] - => let T := type of H' in fail 1 "The hypothesis" H' "already proves" T - | [ H' : eq (opp x) y |- _ ] - => let T := type of H' in fail 1 "The hypothesis" H' "already proves" T - | [ H' : eq (opp y) x |- _ ] - => let T := type of H' in fail 1 "The hypothesis" H' "already proves" T - | [ H' : eq (mul x x) (mul y y) |- _ ] - => pose proof (only_two_square_roots'_choice x y H') as H - | [ H0 : eq (mul x x) ?z, H1 : eq (mul y y) ?z |- _ ] - => pose proof (only_two_square_roots_choice x y z H0 H1) as H - end - end - end. -Ltac reduce_only_two_square_roots x y eq opp mul := - let H := fresh in - pose_proof_only_two_square_roots x y H eq opp mul; - destruct H; - try setoid_subst y. -(** Remove duplicates; solve goals by contradiction, and, if goals still remain, substitute the square roots *) -Ltac post_clean_only_two_square_roots x y := - try (unfold not in *; - match goal with - | [ H : (?T -> False)%type, H' : ?T |- _ ] => exfalso; apply H; exact H' - | [ H : (?R ?x ?x -> False)%type |- _ ] => exfalso; apply H; reflexivity - end); - try setoid_subst x; try setoid_subst y. -Ltac only_two_square_roots_step eq opp mul := - match goal with - | [ H : not (eq ?x (opp ?y)) |- _ ] - (* this one comes first, because it the procedure is asymmetric - with respect to [x] and [y], and this order is more likely to - lead to solving goals by contradiction. *) - => is_var x; is_var y; reduce_only_two_square_roots x y eq opp mul; post_clean_only_two_square_roots x y - | [ H : eq (mul ?x ?x) (mul ?y ?y) |- _ ] - => reduce_only_two_square_roots x y eq opp mul; post_clean_only_two_square_roots x y - | [ H : eq (mul ?x ?x) ?z, H' : eq (mul ?y ?y) ?z |- _ ] - => reduce_only_two_square_roots x y eq opp mul; post_clean_only_two_square_roots x y - end. -Ltac only_two_square_roots := - let fld := guess_field in - lazymatch type of fld with - | @field ?F ?eq ?zero ?one ?opp ?add ?sub ?mul ?inv ?div - => repeat only_two_square_roots_step eq opp mul - end.
\ No newline at end of file +End FieldSquareRoot.
\ No newline at end of file diff --git a/src/Algebra/Field_test.v b/src/Algebra/Field_test.v new file mode 100644 index 000000000..f3a43f3e3 --- /dev/null +++ b/src/Algebra/Field_test.v @@ -0,0 +1,82 @@ +Require Import Crypto.Util.Decidable Crypto.Util.Notations. +Require Import Crypto.Algebra.Ring Crypto.Algebra.Field. + +Module _fsatz_test. + Section _test. + Context {F eq zero one opp add sub mul inv div} + {fld:@Algebra.field F eq zero one opp add sub mul inv div} + {eq_dec:DecidableRel eq}. + Local Infix "=" := eq. Local Notation "a <> b" := (not (a = b)). + Local Infix "=" := eq : type_scope. Local Notation "a <> b" := (not (a = b)) : type_scope. + Local Notation "0" := zero. Local Notation "1" := one. + Local Infix "+" := add. Local Infix "*" := mul. + Local Infix "-" := sub. Local Infix "/" := div. + + Lemma inv_hyp a b c d (H:a*inv b=inv d*c) (bnz:b<>0) (dnz:d<>0) : a*d = b*c. + Proof. fsatz. Qed. + + Lemma inv_goal a b c d (H:a=b+c) (anz:a<>0) : inv a*d + 1 = (d+b+c)*inv(b+c). + Proof. fsatz. Qed. + + Lemma div_hyp a b c d (H:a/b=c/d) (bnz:b<>0) (dnz:d<>0) : a*d = b*c. + Proof. fsatz. Qed. + + Lemma div_goal a b c d (H:a=b+c) (anz:a<>0) : d/a + 1 = (d+b+c)/(b+c). + Proof. fsatz. Qed. + + Lemma zero_neq_one : 0 <> 1. + Proof. fsatz. Qed. + + Lemma only_two_square_roots x y : x * x = y * y -> x <> opp y -> x = y. + Proof. intros; fsatz. Qed. + + Lemma transitivity_contradiction a b c (ab:a=b) (bc:b=c) (X:a<>c) : False. + Proof. fsatz. Qed. + + Lemma algebraic_contradiction a b c (A:a+b=c) (B:a-b=c) (X:a*a - b*b <> c*c) : False. + Proof. fsatz. Qed. + + Lemma division_by_zero_in_hyps (bad:1/0 + 1 = (1+1)/0): 1 = 1. + Proof. fsatz. Qed. + Lemma division_by_zero_in_hyps_eq_neq (bad:1/0 + 1 = (1+1)/0): 1 <> 0. fsatz. Qed. + Lemma division_by_zero_in_hyps_neq_neq (bad:1/0 <> (1+1)/0): 1 <> 0. fsatz. Qed. + Import BinNums. + + Context {char_gt_15:@Ring.char_gt F eq zero one opp add sub mul 15}. + + Local Notation two := (one+one) (only parsing). + Local Notation three := (one+one+one) (only parsing). + Local Notation seven := (three+three+one) (only parsing). + Local Notation nine := (three+three+three) (only parsing). + + Lemma fractional_equation_solution x (A:x<>1) (B:x<>opp two) (C:x*x+x <> two) (X:nine/(x*x + x - two) = three/(x+two) + seven*inv(x-1)) : x = opp one / (three+two). + Proof. fsatz. Qed. + + Lemma fractional_equation_no_solution x (A:x<>1) (B:x<>opp two) (C:x*x+x <> two) (X:nine/(x*x + x - two) = opp three/(x+two) + seven*inv(x-1)) : False. + Proof. fsatz. Qed. + + Local Notation "x ^ 2" := (x*x). Local Notation "x ^ 3" := (x^2*x). + Lemma weierstrass_associativity_main a b x1 y1 x2 y2 x4 y4 + (A: y1^2=x1^3+a*x1+b) + (B: y2^2=x2^3+a*x2+b) + (C: y4^2=x4^3+a*x4+b) + (Hi3: x2 <> x1) + λ3 (Hλ3: λ3 = (y2-y1)/(x2-x1)) + x3 (Hx3: x3 = λ3^2-x1-x2) + y3 (Hy3: y3 = λ3*(x1-x3)-y1) + (Hi7: x4 <> x3) + λ7 (Hλ7: λ7 = (y4-y3)/(x4-x3)) + x7 (Hx7: x7 = λ7^2-x3-x4) + y7 (Hy7: y7 = λ7*(x3-x7)-y3) + (Hi6: x4 <> x2) + λ6 (Hλ6: λ6 = (y4-y2)/(x4-x2)) + x6 (Hx6: x6 = λ6^2-x2-x4) + y6 (Hy6: y6 = λ6*(x2-x6)-y2) + (Hi9: x6 <> x1) + λ9 (Hλ9: λ9 = (y6-y1)/(x6-x1)) + x9 (Hx9: x9 = λ9^2-x1-x6) + y9 (Hy9: y9 = λ9*(x1-x9)-y1) + : x7 = x9 /\ y7 = y9. + Proof. split; fsatz. Qed. + End _test. +End _fsatz_test.
\ No newline at end of file diff --git a/src/Algebra/Group.v b/src/Algebra/Group.v index e4d38e243..7f580380f 100644 --- a/src/Algebra/Group.v +++ b/src/Algebra/Group.v @@ -1,4 +1,4 @@ -Require Import Coq.Classes.Morphisms. +Require Import Coq.Classes.Morphisms Crypto.Util.Relations Crypto.Util.Tactics. Require Import Crypto.Algebra Crypto.Algebra.Monoid Crypto.Algebra.ScalarMult. Section BasicProperties. @@ -25,24 +25,11 @@ Section BasicProperties. - rewrite Hix, left_identity; reflexivity. Qed. - Lemma move_leftL x y : inv y * x = id -> x = y. + Lemma inv_bijective x y : inv x = inv y <-> x = y. Proof. - intro; rewrite <- (inv_inv y), (inv_unique x (inv y)), inv_inv by assumption; reflexivity. - Qed. - - Lemma move_leftR x y : x * inv y = id -> x = y. - Proof. - intro; rewrite (inv_unique (inv y) x), inv_inv by assumption; reflexivity. - Qed. - - Lemma move_rightR x y : id = y * inv x -> x = y. - Proof. - intro; rewrite <- (inv_inv x), (inv_unique (inv x) y), inv_inv by (symmetry; assumption); reflexivity. - Qed. - - Lemma move_rightL x y : id = inv x * y -> x = y. - Proof. - intro; rewrite <- (inv_inv x), (inv_unique y (inv x)), inv_inv by (symmetry; assumption); reflexivity. + split; intro Hi; rewrite ?Hi; try reflexivity. + assert (Hii:inv (inv x) = inv (inv y)) by (rewrite Hi; reflexivity). + rewrite 2inv_inv in Hii; exact Hii. Qed. Lemma inv_op x y : inv (x*y) = inv y*inv x. @@ -56,33 +43,14 @@ Section BasicProperties. Lemma inv_id : inv id = id. Proof. symmetry. eapply inv_unique, left_identity. Qed. - Lemma inv_nonzero_nonzero : forall x, x <> id -> inv x <> id. + Lemma inv_id_iff x : inv x = id <-> x = id. Proof. - intros ? Hx Ho. - assert (Hxo: x * inv x = id) by (rewrite right_inverse; reflexivity). - rewrite Ho, right_identity in Hxo. intuition. + split; intro Hi; rewrite ?Hi, ?inv_id; try reflexivity. + rewrite <-inv_id, inv_bijective in Hi; exact Hi. Qed. - Lemma neq_inv_nonzero : forall x, x <> inv x -> x <> id. - Proof. - intros ? Hx Hi; apply Hx. - rewrite Hi. - symmetry; apply inv_id. - Qed. - - Lemma inv_neq_nonzero : forall x, inv x <> x -> x <> id. - Proof. - intros ? Hx Hi; apply Hx. - rewrite Hi. - apply inv_id. - Qed. - - Lemma inv_zero_zero : forall x, inv x = id -> x = id. - Proof. - intros. - rewrite <-inv_id, <-H0. - symmetry; apply inv_inv. - Qed. + Lemma inv_nonzero_nonzero x : x <> id <-> inv x <> id. + Proof. setoid_rewrite inv_id_iff; reflexivity. Qed. Lemma eq_r_opp_r_inv a b c : a = op c (inv b) <-> op a b = c. Proof. @@ -94,7 +62,7 @@ Section BasicProperties. Section ZeroNeqOne. Context {one} `{is_zero_neq_one T eq id one}. Lemma opp_one_neq_zero : inv one <> id. - Proof. apply inv_nonzero_nonzero, one_neq_zero. Qed. + Proof. setoid_rewrite inv_id_iff. exact one_neq_zero. Qed. Lemma zero_neq_opp_one : id <> inv one. Proof. intro Hx. symmetry in Hx. eauto using opp_one_neq_zero. Qed. End ZeroNeqOne. diff --git a/src/Algebra/IntegralDomain.v b/src/Algebra/IntegralDomain.v index 96a4cf06b..066886e83 100644 --- a/src/Algebra/IntegralDomain.v +++ b/src/Algebra/IntegralDomain.v @@ -1,4 +1,5 @@ -Require Import Crypto.Util.Tactics. +Require Import Crypto.Util.Tactics Crypto.Util.Relations. +Require Import Crypto.Util.Factorize. Require Import Crypto.Algebra Crypto.Algebra.Ring. Module IntegralDomain. @@ -53,40 +54,72 @@ Module IntegralDomain. repeat (rewrite_hyp ?*; Ring.push_homomorphism constr:(of_Z)); reflexivity. Qed. + (* TODO: move *) + Lemma nonzero_of_Z_abs z : of_Z (Z.abs z) <> zero <-> of_Z z <> zero. + Proof. + destruct z; simpl Z.abs; [reflexivity..|]. + simpl of_Z. setoid_rewrite opp_zero_iff. reflexivity. + Qed. + Section WithChar. Context C (char_gt_C:@Ring.char_gt R eq zero one opp add sub mul C). + + Definition is_factor_nonzero (n:N) : bool := + match n with N0 => false | N.pos p => BinPos.Pos.leb p C end. + Lemma is_factor_nonzero_correct (n:N) (refl:Logic.eq (is_factor_nonzero n) true) + : of_Z (Z.of_N n) <> zero. + Proof. + destruct n; [discriminate|]; rewrite Znat.positive_N_Z; apply char_gt_C, Pos.leb_le, refl. + Qed. + + Lemma RZN_product_nonzero l (H : forall x : N, List.In x l -> of_Z (Z.of_N x) <> zero) + : of_Z (Z.of_N (List.fold_right N.mul 1%N l)) <> zero. + Proof. + rewrite <-List.Forall_forall in H; induction H; simpl List.fold_right. + { eapply char_gt_C, Pos.le_1_l. } + { rewrite Znat.N2Z.inj_mul; Ring.push_homomorphism constr:(of_Z). + eapply Ring.nonzero_product_iff_nonzero_factor; eauto. } + Qed. + + Definition is_constant_nonzero (z:Z) : bool := + match factorize_or_fail (Z.abs_N z) with + | Some factors => List.forallb is_factor_nonzero factors + | None => false + end. + Lemma is_constant_nonzero_correct z (refl:Logic.eq (is_constant_nonzero z) true) + : of_Z z <> zero. + Proof. + rewrite <-nonzero_of_Z_abs, <-Znat.N2Z.inj_abs_N. + repeat match goal with + | _ => progress cbv [is_constant_nonzero] in * + | _ => progress break_match_hyps; try congruence; [] + | _ => progress rewrite ?List.forallb_forall in * + |H:_|-_ => apply product_factorize_or_fail in H; rewrite <- H in * + | _ => solve [eauto using RZN_product_nonzero, is_factor_nonzero_correct] + end. + Qed. + Fixpoint is_nonzero (c:coef) : bool := match c with + | Coef_one => true | Coef_opp c => is_nonzero c | Coef_mul c1 c2 => andb (is_nonzero c1) (is_nonzero c2) - | _ => - match CtoZ c with - | Z0 => false - | Zpos p => N.leb (N.pos p) C - | Zneg p => N.leb (N.pos p) C - end + | _ => is_constant_nonzero (CtoZ c) end. Lemma is_nonzero_correct c (refl:Logic.eq (is_nonzero c) true) : denote c <> zero. Proof. induction c; repeat match goal with - | _ => progress unfold Algebra.char_gt, Ring.char_gt in * + | H:_|-_ => progress rewrite Bool.andb_true_iff in H; destruct H + | H:_|-_ => progress apply is_constant_nonzero_correct in H | _ => progress (unfold is_nonzero in *; fold is_nonzero in * ) - | _ => progress change (denote (Coef_opp c)) with (opp (denote c)) in * - | _ => progress change (denote (Coef_mul c1 c2)) with (denote c1 * denote c2) in * - | _ => rewrite N.leb_le in * - | _ => rewrite <-Pos2Z.opp_pos in * - | H:@Logic.eq Z (CtoZ ?x) ?y |- _ => rewrite <-(CtoZ_correct x), H - | H: Logic.eq match ?x with _ => _ end true |- _ => destruct x eqn:? - | H:_ |- _ => unique pose proof (proj1 (Bool.andb_true_iff _ _) H) - | H:_/\_|- _ => unique pose proof (proj1 H) - | H:_/\_|- _ => unique pose proof (proj2 H) - | H: _ |- _ => unique pose proof (z_nonzero_correct _ H) + | _ => progress (change (denote (Coef_one)) with (of_Z 1) in * ) + | _ => progress (change (denote (Coef_opp c)) with (opp (denote c)) in * ) + | _ => progress (change (denote (Coef_mul c1 c2)) with (denote c1 * denote c2) in * ) + | |- opp _ <> zero => setoid_rewrite Ring.opp_zero_iff | |- _ * _ <> zero => eapply Ring.nonzero_product_iff_nonzero_factor - | |- opp _ <> zero => eapply Ring.opp_nonzero_nonzero - | _ => rewrite <-!Znat.N2Z.inj_pos - | |- _ => solve [eauto using N_one_le_pos | discriminate] - | _ => progress Ring.push_homomorphism constr:(of_Z) + | _ => solve [eauto using is_constant_nonzero_correct, Pos.le_1_l] + | _ => progress rewrite <-CtoZ_correct end. Qed. End WithChar. @@ -110,7 +143,7 @@ Module IntegralDomain. End _LargeCharacteristicReflective. Ltac solve_constant_nonzero := - match goal with (* TODO: change this match to a typeclass resolution *) + match goal with | |- not (?eq ?x _) => let cg := constr:(_:Ring.char_gt (eq:=eq) _) in match type of cg with diff --git a/src/Algebra/Ring.v b/src/Algebra/Ring.v index 3752c7562..b69e9b191 100644 --- a/src/Algebra/Ring.v +++ b/src/Algebra/Ring.v @@ -46,7 +46,7 @@ Section Ring. rewrite <-!associative, right_inverse, right_identity; reflexivity. Qed. - Definition opp_nonzero_nonzero : forall x, x <> 0 -> opp x <> 0 := Group.inv_nonzero_nonzero. + Definition opp_zero_iff : forall x, opp x = 0 <-> x = 0 := Group.inv_id_iff. Global Instance is_left_distributive_sub : is_left_distributive (eq:=eq)(add:=sub)(mul:=mul). Proof. @@ -360,7 +360,7 @@ End of_Z. Definition char_gt {R eq zero one opp add} {sub:R->R->R} {mul:R->R->R} C := - @Algebra.char_gt R eq zero (fun n => (@of_Z R zero one opp add) (BinInt.Z.of_N n)) C. + @Algebra.char_gt R eq zero (fun p => (@of_Z R zero one opp add) (BinInt.Z.pos p)) C. Existing Class char_gt. (*** Tactics for ring equations *) diff --git a/src/Spec/CompleteEdwardsCurve.v b/src/Spec/CompleteEdwardsCurve.v index 05f61f159..770a2d02d 100644 --- a/src/Spec/CompleteEdwardsCurve.v +++ b/src/Spec/CompleteEdwardsCurve.v @@ -20,7 +20,7 @@ Module E. Context {a d: F}. Class twisted_edwards_params := { - char_gt_2 : @Ring.char_gt F Feq Fzero Fone Fopp Fadd Fsub Fmul BinNat.N.two; + char_gt_2 : @Ring.char_gt F Feq Fzero Fone Fopp Fadd Fsub Fmul (BinNat.N.succ_pos BinNat.N.one); nonzero_a : a <> 0; square_a : exists sqrt_a, sqrt_a^2 = a; nonsquare_d : forall x, x^2 <> d diff --git a/src/Spec/MontgomeryCurve.v b/src/Spec/MontgomeryCurve.v index 4e448392f..5f7246011 100644 --- a/src/Spec/MontgomeryCurve.v +++ b/src/Spec/MontgomeryCurve.v @@ -6,7 +6,7 @@ Require Import Crypto.Spec.WeierstrassCurve. Module M. Section MontgomeryCurve. Import BinNat. - Context {F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv} {field:@Algebra.field F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv} {Feq_dec:Decidable.DecidableRel Feq} {char_gt_2:@Ring.char_gt F Feq Fzero Fone Fopp Fadd Fsub Fmul 2}. + Context {F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv} {field:@Algebra.field F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv} {Feq_dec:Decidable.DecidableRel Feq} {char_gt_2:@Ring.char_gt F Feq Fzero Fone Fopp Fadd Fsub Fmul (BinNat.N.succ_pos (BinNat.N.two))}. Local Infix "=" := Feq : type_scope. Local Notation "a <> b" := (not (a = b)) : type_scope. Local Infix "+" := Fadd. Local Infix "*" := Fmul. Local Infix "-" := Fsub. Local Infix "/" := Fdiv. diff --git a/src/Spec/WeierstrassCurve.v b/src/Spec/WeierstrassCurve.v index 7f4b66d46..d19f3f786 100644 --- a/src/Spec/WeierstrassCurve.v +++ b/src/Spec/WeierstrassCurve.v @@ -9,7 +9,7 @@ Module W. * <http://cs.ucsb.edu/~koc/ccs130h/2013/EllipticHyperelliptic-CohenFrey.pdf> (page 79) *) - Context {F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv} {field:@Algebra.field F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv} {Feq_dec:Decidable.DecidableRel Feq} {char_gt_2:@Ring.char_gt F Feq Fzero Fone Fopp Fadd Fsub Fmul BinNat.N.two}. + Context {F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv} {field:@Algebra.field F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv} {Feq_dec:Decidable.DecidableRel Feq} {char_gt_2:@Ring.char_gt F Feq Fzero Fone Fopp Fadd Fsub Fmul (BinNat.N.succ_pos (BinNat.N.two))}. Local Infix "=" := Feq : type_scope. Local Notation "a <> b" := (not (a = b)) : type_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. diff --git a/src/Util/Factorize.v b/src/Util/Factorize.v new file mode 100644 index 000000000..8ccb7d119 --- /dev/null +++ b/src/Util/Factorize.v @@ -0,0 +1,73 @@ +Require Import Coq.Bool.Sumbool. +Require Import Coq.micromega.Psatz. +Require Import Coq.NArith.NArith. +Require Import Coq.PArith.PArith. +Require Import Coq.Lists.List. +Require Import Coq.Init.Wf. + +Local Open Scope positive_scope. + +(* given [n] and [d₀], returns, possibly, [d, v] where [d ≥ d₀] is small and [d * v = n] + + Precondition: [d₀] is either 2, or an odd number > 2 *) +Definition find_N_factor (factor_val : N) (d0 : N) : option (N * N). +Proof. + refine (let (d', r) := N.div_eucl factor_val d0 in (* special-case the first one, which might be 2 *) + if N.eqb 0 r + then Some (d0, d') + else + let sfactor_val := N.sqrt factor_val in + Fix + (Acc_intro_generator (S (S (S (N.to_nat (N.div2 sfactor_val))))) (@N.gt_wf sfactor_val)) (fun _ => option (N * N)%type) + (fun d find_N_factor + => let (d', r) := N.div_eucl factor_val d in + if N.eqb 0 r + then Some (d, d') + else let d' := (d + 2)%N in + if Sumbool.sumbool_of_bool (N.leb d' sfactor_val) + then find_N_factor d' _ + else None) + (if N.eqb 2%N d0 then 3%N else (d0 + 2)%N)). + { subst sfactor_val d'. + clear find_N_factor. + let H := match goal with H : _ = true |- _ => H end in + clear -H; + abstract ( + apply N.leb_le in H; + split; try assumption; + lia + ). } +Defined. + +(* given [n] and [d₀], gives a list of factors of [n] which are ≥ d₀, lowest to highest *) +Definition factorize' (n : N) : N -> list N. +Proof. + refine (Fix + (Acc_intro_generator (S (S (S (S (N.to_nat (N.div2 (N.sqrt n))))))) N.lt_wf_0) (fun _ => N -> list N) + (fun n factorize cur_max_factor + => _) + n). + refine match find_N_factor n cur_max_factor with + | Some (d, n') => if Sumbool.sumbool_of_bool (n' <? n)%N + then d :: factorize n' _ d + else d :: n' :: nil + | None => n::nil + end. + { let H := match goal with H : _ = true |- _ => H end in + clear -H; + abstract ( + apply N.ltb_lt in H; + assumption + ). } +Defined. + +Definition factorize (n : N) : list N := factorize' n 2%N. + +Definition factorize_or_fail (n:N) : option (list N) := + let factors := factorize n in + if N.eqb (List.fold_right N.mul 1%N factors) n then Some factors else None. +Lemma product_factorize_or_fail (n:N) (factors:list N) + (H:Logic.eq (factorize_or_fail n) (Some factors)) + : Logic.eq (List.fold_right N.mul 1%N factors) n. +Proof. cbv [factorize_or_fail] in H; destruct ((fold_right N.mul 1 (factorize n) =? n)%N) eqn:?; + try apply N.eqb_eq; congruence. Qed.
\ No newline at end of file diff --git a/src/Util/Tactics.v b/src/Util/Tactics.v index 5f7ad65cc..d98ac1bd4 100644 --- a/src/Util/Tactics.v +++ b/src/Util/Tactics.v @@ -32,11 +32,12 @@ Ltac debuglevel := constr:(0%nat). Ltac solve_debugfail tac := solve [tac] || - let dbg := debuglevel in - match dbg with - | O => idtac - | _ => match goal with |- ?G => idtac "couldn't prove" G end - end. + ( let dbg := debuglevel in + match dbg with + | O => idtac + | _ => match goal with |- ?G => idtac "couldn't prove" G end + end; + fail). Ltac set_evars := repeat match goal with diff --git a/src/WeierstrassCurve/Pre.v b/src/WeierstrassCurve/Pre.v index b809aa0b4..da4c8c214 100644 --- a/src/WeierstrassCurve/Pre.v +++ b/src/WeierstrassCurve/Pre.v @@ -7,11 +7,10 @@ Import BinNums. Local Open Scope core_scope. -Generalizable All Variables. Section Pre. Context {F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv} {field:@field F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv} - {char_gt_2:@Ring.char_gt F Feq Fzero Fone Fopp Fadd Fsub Fmul 2%N} + {char_gt_2:@Ring.char_gt F Feq Fzero Fone Fopp Fadd Fsub Fmul (BinNat.N.succ_pos (BinNat.N.two))} {eq_dec: DecidableRel Feq}. Local Infix "=" := Feq. Local Notation "a <> b" := (not (a = b)). Local Infix "=" := Feq : type_scope. Local Notation "a <> b" := (not (a = b)) : type_scope. diff --git a/src/WeierstrassCurve/WeierstrassCurveTheorems.v b/src/WeierstrassCurve/WeierstrassCurveTheorems.v index 4a3f54154..5489a8ef0 100644 --- a/src/WeierstrassCurve/WeierstrassCurveTheorems.v +++ b/src/WeierstrassCurve/WeierstrassCurveTheorems.v @@ -3,13 +3,14 @@ Require Import Coq.Classes.Morphisms. Require Import Crypto.Spec.WeierstrassCurve. Require Import Crypto.Algebra Crypto.Algebra.Field. Require Import Crypto.Util.Decidable Crypto.Util.Tactics. +Require Import BinPos. Module W. Section W. Context {F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv} {a b:F} {field:@Algebra.field F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv} - {char_gt_2:@Ring.char_gt F Feq Fzero Fone Fopp Fadd Fsub Fmul 2} - {char_huge:@Ring.char_gt F Feq Fzero Fone Fopp Fadd Fsub Fmul 35481600} (* TODO: we need only 3, but we may need to factor some coefficients *) + {char_gt_3:@Ring.char_gt F Feq Fzero Fone Fopp Fadd Fsub Fmul (BinNat.N.succ_pos (BinNat.N.two))} + {char_gt_11:@Ring.char_gt F Feq Fzero Fone Fopp Fadd Fsub Fmul 11%positive} (* FIXME: we shouldn't need this *) {Feq_dec:DecidableRel Feq}. Local Infix "=" := Feq : type_scope. Local Notation "a <> b" := (not (a = b)) : type_scope. Local Notation "0" := Fzero. Local Notation "1" := Fone. |