From f5c1d1e55617000d79ef4bedb899f410f09d1e4f Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Sat, 9 Jul 2016 17:21:48 -0400 Subject: remove field_algebra --- src/CompleteEdwardsCurve/ExtendedCoordinates.v | 16 ++++++---------- src/CompleteEdwardsCurve/Pre.v | 13 +++++++------ 2 files changed, 13 insertions(+), 16 deletions(-) (limited to 'src/CompleteEdwardsCurve') diff --git a/src/CompleteEdwardsCurve/ExtendedCoordinates.v b/src/CompleteEdwardsCurve/ExtendedCoordinates.v index 263582508..d8efb82f3 100644 --- a/src/CompleteEdwardsCurve/ExtendedCoordinates.v +++ b/src/CompleteEdwardsCurve/ExtendedCoordinates.v @@ -33,6 +33,7 @@ Module Extended. Create HintDb bash discriminated. Local Hint Unfold E.eq fst snd fieldwise fieldwise' coordinates E.coordinates proj1_sig Pre.onCurve : bash. Ltac bash := + pose proof E.char_gt_2; repeat match goal with | |- Proper _ _ => intro | _ => progress intros @@ -43,15 +44,11 @@ Module Extended. | |- _ /\ _ => split | _ => solve [neq01] | _ => solve [eauto] - | _ => solve [intuition] + | _ => solve [intuition eauto] | _ => solve [etransitivity; eauto] - | |- Feq _ _ => field_algebra - | |- _ <> 0 => apply mul_nonzero_nonzero - | [ H : _ <> 0 |- _ <> 0 ] => - intro; apply H; - field_algebra; - solve [ apply Ring.opp_nonzero_nonzero, E.char_gt_2 - | apply E.char_gt_2] + | |- _*_ <> 0 => apply mul_nonzero_nonzero + | [H: _ |- _ ] => solve [intro; apply H; super_nsatz] + | |- Feq _ _ => super_nsatz end. Obligation Tactic := bash. @@ -63,8 +60,7 @@ Module Extended. (let '(X,Y,Z,T) := coordinates P in ((X/Z), (Y/Z))) _. Definition eq (P Q:point) := E.eq (to_twisted P) (to_twisted Q). - Global Instance DecidableRel_eq : Decidable.DecidableRel eq. - Proof. typeclasses eauto. Qed. + Global Instance DecidableRel_eq : Decidable.DecidableRel eq := _. Local Hint Unfold from_twisted to_twisted eq : bash. diff --git a/src/CompleteEdwardsCurve/Pre.v b/src/CompleteEdwardsCurve/Pre.v index 432e834aa..a83c85b02 100644 --- a/src/CompleteEdwardsCurve/Pre.v +++ b/src/CompleteEdwardsCurve/Pre.v @@ -50,24 +50,25 @@ Section Pre. => apply d_nonsquare with (sqrt_d:= (f (sqrt_a * x1) (d * x1 * x2 * y1 * y2 * y1)) /(f (sqrt_a * x2) y2 * x1 * y1 )) | _ => apply a_nonzero - end; field_algebra; auto using Ring.opp_nonzero_nonzero; nsatz_contradict. + end; super_nsatz. Qed. Lemma edwardsAddCompletePlus x1 y1 x2 y2 : onCurve (x1, y1) -> onCurve (x2, y2) -> (1 + d*x1*x2*y1*y2) <> 0. - Proof. intros H1 H2 ?. apply (edwardsAddComplete' _ _ _ _ H1 H2); field_algebra. Qed. + Proof. intros H1 H2 ?. apply (edwardsAddComplete' _ _ _ _ H1 H2); super_nsatz. Qed. Lemma edwardsAddCompleteMinus x1 y1 x2 y2 : onCurve (x1, y1) -> onCurve (x2, y2) -> (1 - d*x1*x2*y1*y2) <> 0. - Proof. intros H1 H2 ?. apply (edwardsAddComplete' _ _ _ _ H1 H2); field_algebra. Qed. + Proof. intros H1 H2 ?. apply (edwardsAddComplete' _ _ _ _ H1 H2); super_nsatz. Qed. - Lemma zeroOnCurve : onCurve (0, 1). Proof. simpl. field_algebra. Qed. + Lemma zeroOnCurve : onCurve (0, 1). Proof. simpl. super_nsatz. Qed. Lemma unifiedAdd'_onCurve : forall P1 P2, onCurve P1 -> onCurve P2 -> onCurve (unifiedAdd' P1 P2). Proof. - unfold onCurve, unifiedAdd'; intros [x1 y1] [x2 y2] H1 H2. - field_algebra; auto using edwardsAddCompleteMinus, edwardsAddCompletePlus. + unfold onCurve, unifiedAdd'; intros [x1 y1] [x2 y2] ? ?. + conservative_common_denominator; [ | auto using edwardsAddCompleteMinus, edwardsAddCompletePlus..]. + nsatz. Qed. End Pre. -- cgit v1.2.3