From c2df47be85f640255dfdee86144932084dad059b Mon Sep 17 00:00:00 2001 From: jadep Date: Fri, 15 Jul 2016 15:12:29 -0400 Subject: proved an admit in field homomorphisms that turned out to be unprovable; I added another precondition and pushed it through everywhere but one place in ExtendedCoordinates, where I was stuck. --- src/Algebra.v | 63 ++++++++++++++++++---- .../CompleteEdwardsCurveTheorems.v | 20 ++++--- src/CompleteEdwardsCurve/ExtendedCoordinates.v | 6 ++- src/CompleteEdwardsCurve/Pre.v | 8 +-- 4 files changed, 74 insertions(+), 23 deletions(-) (limited to 'src') diff --git a/src/Algebra.v b/src/Algebra.v index cb9103b52..d47fc6acd 100644 --- a/src/Algebra.v +++ b/src/Algebra.v @@ -438,7 +438,7 @@ Module Ring. Local Notation "0" := zero. Local Notation "1" := one. Local Infix "+" := add. Local Infix "-" := sub. Local Infix "*" := mul. - Lemma mul_0_r : forall x, 0 * x = 0. + Lemma mul_0_l : forall x, 0 * x = 0. Proof. intros. assert (0*x = 0*x) as Hx by reflexivity. @@ -447,7 +447,7 @@ Module Ring. rewrite !ring_sub_definition, <-associative, right_inverse, right_identity in Hxx; exact Hxx. Qed. - Lemma mul_0_l : forall x, x * 0 = 0. + Lemma mul_0_r : forall x, x * 0 = 0. Proof. intros. assert (x*0 = x*0) as Hx by reflexivity. @@ -462,7 +462,7 @@ Module Ring. Lemma mul_opp_r x y : x * opp y = opp (x * y). Proof. assert (Ho:x*(opp y) + x*y = 0) - by (rewrite <-left_distributive, left_inverse, mul_0_l; reflexivity). + by (rewrite <-left_distributive, left_inverse, mul_0_r; reflexivity). rewrite <-(left_identity (opp (x*y))), <-Ho; clear Ho. rewrite <-!associative, right_inverse, right_identity; reflexivity. Qed. @@ -470,7 +470,7 @@ Module Ring. Lemma mul_opp_l x y : opp x * y = opp (x * y). Proof. assert (Ho:opp x*y + x*y = 0) - by (rewrite <-right_distributive, left_inverse, mul_0_r; reflexivity). + by (rewrite <-right_distributive, left_inverse, mul_0_l; reflexivity). rewrite <-(left_identity (opp (x*y))), <-Ho; clear Ho. rewrite <-!associative, right_inverse, right_identity; reflexivity. Qed. @@ -596,8 +596,8 @@ Module IntegralDomain. Proof. split. { intro H0; split; intro H1; apply H0; rewrite H1. - { apply Ring.mul_0_r. } - { apply Ring.mul_0_l. } } + { apply Ring.mul_0_l. } + { apply Ring.mul_0_r. } } { intros [? ?] ?; edestruct mul_nonzero_nonzero_cases; eauto with nocore. } Qed. @@ -619,10 +619,15 @@ Module Field. Local Notation "0" := zero. Local Notation "1" := one. Local Infix "+" := add. Local Infix "*" := mul. + Lemma right_multiplicative_inverse : forall x : T, ~ eq x zero -> eq (mul x (inv x)) one. + Proof. + intros. rewrite commutative. auto using left_multiplicative_inverse. + Qed. + Global Instance is_mul_nonzero_nonzero : @is_mul_nonzero_nonzero T eq 0 mul. Proof. constructor. intros x y Hx Hy Hxy. - assert (0 = (inv y * (inv x * x)) * y) as H00. (rewrite <-!associative, Hxy, !Ring.mul_0_l; reflexivity). + assert (0 = (inv y * (inv x * x)) * y) as H00. (rewrite <-!associative, Hxy, !Ring.mul_0_r; reflexivity). rewrite left_multiplicative_inverse in H00 by assumption. rewrite right_identity in H00. rewrite left_multiplicative_inverse in H00 by assumption. @@ -634,6 +639,16 @@ Module Field. split; auto using field_commutative_ring, field_domain_is_zero_neq_one, is_mul_nonzero_nonzero. Qed. + Lemma inv_unique x ix : ix * x = one -> ix = inv x. + Proof. + intro Hix. + assert (ix*x*inv x = inv x). + - rewrite Hix, left_identity; reflexivity. + - rewrite <-associative, right_multiplicative_inverse, right_identity in H0; trivial. + intro eq_x_0. rewrite eq_x_0, Ring.mul_0_r in Hix. + apply zero_neq_one. assumption. + Qed. + Require Coq.setoid_ring.Field_theory. Lemma field_theory_for_stdlib_tactic : Field_theory.field_theory 0 1 add mul sub opp div inv eq. Proof. @@ -714,7 +729,6 @@ Module Field. Proof. repeat split; eauto with core typeclass_instances; intros; repeat rewrite ?EQ_opp, ?EQ_inv, ?EQ_add, ?EQ_sub, ?EQ_mul, ?EQ_div, ?EQ_zero, ?EQ_one; - 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, right_inverse, (left_distributive (add := add)), (right_distributive (add := add)), @@ -734,12 +748,39 @@ Module Field. Local Infix "=" := eq. Local Infix "=" := eq : type_scope. Context `{@Ring.is_homomorphism F EQ ONE ADD MUL K eq one add mul phi}. - Lemma homomorphism_multiplicative_inverse : forall x, phi (INV x) = inv (phi x). Admitted. + Lemma homomorphism_multiplicative_inverse_complete + : forall x, (EQ x ZERO -> phi (INV x) = inv (phi x)) + -> phi (INV x) = inv (phi x). + Proof. + intros. + destruct (eq_dec x ZERO); auto. + assert (phi (MUL (INV x) x) = one) as A. { + rewrite left_multiplicative_inverse; auto using Ring.homomorphism_one. + } + rewrite Ring.homomorphism_mul in A. + apply inv_unique in A. assumption. + Qed. - Lemma homomorphism_div : forall x y, phi (DIV x y) = div (phi x) (phi y). + Lemma homomorphism_multiplicative_inverse + : forall x, not (EQ x ZERO) + -> phi (INV x) = inv (phi x). + Proof. + intros. apply homomorphism_multiplicative_inverse_complete. contradiction. + Qed. + + Lemma homomorphism_div_complete + : forall x y, (EQ y ZERO -> phi (INV y) = inv (phi y)) + -> phi (DIV x y) = div (phi x) (phi y). Proof. intros. rewrite !field_div_definition. - rewrite Ring.homomorphism_mul, homomorphism_multiplicative_inverse. reflexivity. + rewrite Ring.homomorphism_mul, homomorphism_multiplicative_inverse_complete. reflexivity. trivial. + Qed. + + Lemma homomorphism_div + : forall x y, not (EQ y ZERO) + -> phi (DIV x y) = div (phi x) (phi y). + Proof. + intros. apply homomorphism_div_complete. contradiction. Qed. End Homomorphism. End Field. diff --git a/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v b/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v index a160d8dab..1d8b730cb 100644 --- a/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v +++ b/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v @@ -124,19 +124,20 @@ Module E. Qed. End PointCompression. End CompleteEdwardsCurveTheorems. - Section Homomorphism. Context {F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv Fa Fd} - {fieldF:@field F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv} + {field:@field F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv} {Fprm:@twisted_edwards_params F Feq Fzero Fone Fadd Fmul Fa Fd}. Context {K Keq Kzero Kone Kopp Kadd Ksub Kmul Kinv Kdiv Ka Kd} - {fieldK:@field K Keq Kzero Kone Kopp Kadd Ksub Kmul Kinv Kdiv} + {fieldK: @Algebra.field K Keq Kzero Kone Kopp Kadd Ksub Kmul Kinv Kdiv} {Kprm:@twisted_edwards_params K Keq Kzero Kone Kadd Kmul Ka Kd}. Context {phi:F->K} {Hphi:@Ring.is_homomorphism F Feq Fone Fadd Fmul K Keq Kone Kadd Kmul phi}. Context {Ha:Keq (phi Fa) Ka} {Hd:Keq (phi Fd) Kd}. - Local Notation Fpoint := (@point F Feq Fone Fadd Fmul Fa Fd). - Local Notation Kpoint := (@point K Keq Kone Kadd Kmul Ka Kd). + Local Notation Fpoint := (@E.point F Feq Fone Fadd Fmul Fa Fd). + Local Notation Kpoint := (@E.point K Keq Kone Kadd Kmul Ka Kd). + Local Notation FonCurve := (@onCurve F Feq Fone Fadd Fmul Fa Fd). + Local Notation KonCurve := (@onCurve K Keq Kone Kadd Kmul Ka Kd). Create HintDb field_homomorphism discriminated. Hint Rewrite <- @@ -149,6 +150,7 @@ Module E. Hd : field_homomorphism. + Obligation Tactic := idtac. Program Definition ref_phi (P:Fpoint) : Kpoint := exist _ ( let (x, y) := coordinates P in (phi x, phi y)) _. Next Obligation. @@ -159,7 +161,7 @@ Module E. Context {point_phi:Fpoint->Kpoint} {point_phi_Proper:Proper (eq==>eq) point_phi} - {point_phi_correct: forall (P:Fpoint), eq (point_phi P) (ref_phi P)}. + {point_phi_correct: forall (P:point), eq (point_phi P) (ref_phi P)}. Lemma lift_homomorphism : @Group.is_homomorphism Fpoint eq add Kpoint eq add point_phi. Proof. @@ -174,7 +176,11 @@ Module E. | |- Keq ?x ?x => reflexivity | |- Keq ?x ?y => rewrite_strat bottomup hints field_homomorphism | [ H : Feq _ _ |- Keq (phi _) (phi _)] => solve [f_equiv; intuition] - end. + end; + assert (FonCurve (f1,f2)) as FonCurve1 by assumption; + assert (FonCurve (f,f0)) as FonCurve2 by assumption; + [ eapply (@edwardsAddCompleteMinus F) with (x1 := f1); destruct Fprm; eauto + | eapply (@edwardsAddCompletePlus F) with (x1 := f1); destruct Fprm; eauto]. Qed. End Homomorphism. End E. diff --git a/src/CompleteEdwardsCurve/ExtendedCoordinates.v b/src/CompleteEdwardsCurve/ExtendedCoordinates.v index d8efb82f3..f3820aeac 100644 --- a/src/CompleteEdwardsCurve/ExtendedCoordinates.v +++ b/src/CompleteEdwardsCurve/ExtendedCoordinates.v @@ -205,6 +205,8 @@ Module Extended. Context {Hd:Keq (phi Fd) Kd} {Kdd Fdd} {HKdd:Keq Kdd (Kadd Kd Kd)} {HFdd:Feq Fdd (Fadd Fd Fd)}. Local Notation Fpoint := (@point F Feq Fzero Fone Fadd Fmul Fdiv Fa Fd). Local Notation Kpoint := (@point K Keq Kzero Kone Kadd Kmul Kdiv Ka Kd). + Local Notation FonCurve := (@onCurve F Feq Fone Fadd Fmul Fa Fd). + Local Notation KonCurve := (@onCurve K Keq Kone Kadd Kmul Ka Kd). Lemma Ha : Keq (phi Fa) Ka. Proof. rewrite HFa, HKa, <-homomorphism_one. eapply homomorphism_opp. Qed. @@ -228,7 +230,7 @@ Module Extended. let '(X, Y, Z, T) := coordinates P in (phi X, phi Y, phi Z, phi T)) _. Next Obligation. destruct P as [[[[] ?] ?] [? [? ?]]]; unfold onCurve in *; simpl. - rewrite_strat bottomup hints field_homomorphism. + (rewrite_strat bottomup hints field_homomorphism); try assumption. eauto 10 using is_homomorphism_phi_proper, phi_nonzero. Qed. @@ -250,6 +252,6 @@ Module Extended. | |- Keq ?x ?y => rewrite_strat bottomup hints field_homomorphism | [ H : Feq _ _ |- Keq (phi _) (phi _)] => solve [f_equiv; intuition] end. - Qed. + Admitted. (* TODO(jadep or andreser) *) End Homomorphism. End Extended. diff --git a/src/CompleteEdwardsCurve/Pre.v b/src/CompleteEdwardsCurve/Pre.v index c74e9a321..76dd97c72 100644 --- a/src/CompleteEdwardsCurve/Pre.v +++ b/src/CompleteEdwardsCurve/Pre.v @@ -100,14 +100,16 @@ Section RespectsFieldHomomorphism. d_ok : field_homomorphism. - Lemma morphism_unidiedAdd' : forall P Q:F*F, + Lemma morphism_unifiedAdd' : forall P Q:F*F, + (~ EQ (ADD ONE (MUL (MUL (MUL (MUL D (fst P)) (fst Q)) (snd P)) (snd Q))) ZERO) -> + (~ EQ (SUB ONE (MUL (MUL (MUL (MUL D (fst P)) (fst Q)) (snd P)) (snd Q))) ZERO) -> eqp (phip (unifiedAdd'(F:=F)(one:=ONE)(add:=ADD)(sub:=SUB)(mul:=MUL)(div:=DIV)(a:=A)(d:=D) P Q)) (unifiedAdd'(F:=K)(one:=one)(add:=add)(sub:=sub)(mul:=mul)(div:=div)(a:=a)(d:=d) (phip P) (phip Q)). Proof. - intros [x1 y1] [x2 y2]. + intros [x1 y1] [x2 y2] Hnonzero1 Hnonzero2; cbv [unifiedAdd' phip eqp]; apply conj; - (rewrite_strat topdown hints field_homomorphism); reflexivity. + (rewrite_strat topdown hints field_homomorphism); try assumption; reflexivity. Qed. End RespectsFieldHomomorphism. -- cgit v1.2.3