From 0ae5f6871b29d20f48b5df6dab663b5a44162d01 Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Mon, 20 Jun 2016 15:07:03 -0400 Subject: remove trailing whitespace from src/ --- .../CompleteEdwardsCurveTheorems.v | 34 +++++++++++----------- src/CompleteEdwardsCurve/ExtendedCoordinates.v | 10 +++---- src/CompleteEdwardsCurve/Pre.v | 22 +++++++------- 3 files changed, 33 insertions(+), 33 deletions(-) (limited to 'src/CompleteEdwardsCurve') diff --git a/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v b/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v index 89984027f..99029a671 100644 --- a/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v +++ b/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v @@ -23,10 +23,10 @@ Module E. Local Notation onCurve := (@onCurve F Feq Fone Fadd Fmul a d). Add Field _edwards_curve_theorems_field : (field_theory_for_stdlib_tactic (H:=field)). - + Definition eq (P Q:point) := fieldwise (n:=2) Feq (coordinates P) (coordinates Q). Infix "=" := eq : E_scope. - + (* TODO: decide whether we still want something like this, then port Local Ltac t := unfold point_eqb; @@ -41,41 +41,41 @@ Module E. | [H: _ |- _ ] => apply F_eqb_eq in H | _ => rewrite F_eqb_refl end; eauto. - + Lemma point_eqb_sound : forall p1 p2, point_eqb p1 p2 = true -> p1 = p2. Proof. t. Qed. - + Lemma point_eqb_complete : forall p1 p2, p1 = p2 -> point_eqb p1 p2 = true. Proof. t. Qed. - + Lemma point_eqb_neq : forall p1 p2, point_eqb p1 p2 = false -> p1 <> p2. Proof. intros. destruct (point_eqb p1 p2) eqn:Hneq; intuition. apply point_eqb_complete in H0; congruence. Qed. - + Lemma point_eqb_neq_complete : forall p1 p2, p1 <> p2 -> point_eqb p1 p2 = false. Proof. intros. destruct (point_eqb p1 p2) eqn:Hneq; intuition. apply point_eqb_sound in Hneq. congruence. Qed. - + Lemma point_eqb_refl : forall p, point_eqb p p = true. Proof. t. Qed. - + Definition point_eq_dec (p1 p2:E.point) : {p1 = p2} + {p1 <> p2}. destruct (point_eqb p1 p2) eqn:H; match goal with | [ H: _ |- _ ] => apply point_eqb_sound in H | [ H: _ |- _ ] => apply point_eqb_neq in H end; eauto. Qed. - + Lemma point_eqb_correct : forall p1 p2, point_eqb p1 p2 = if point_eq_dec p1 p2 then true else false. Proof. intros. destruct (point_eq_dec p1 p2); eauto using point_eqb_complete, point_eqb_neq_complete. @@ -86,7 +86,7 @@ Module E. Lemma decide_and : forall P Q, {P}+{not P} -> {Q}+{not Q} -> {P/\Q}+{not(P/\Q)}. Proof. intros; repeat match goal with [H:{_}+{_}|-_] => destruct H end; intuition. Qed. - Ltac destruct_points := + Ltac destruct_points := repeat match goal with | [ p : point |- _ ] => let x := fresh "x" p in @@ -104,7 +104,7 @@ Module E. Local Hint Resolve nonsquare_d. Local Hint Resolve @edwardsAddCompletePlus. Local Hint Resolve @edwardsAddCompleteMinus. - + Program Definition opp (P:point) : point := exist _ (let '(x, y) := coordinates P in (Fopp x, y) ) _. Solve All Obligations using intros; destruct_points; simpl; field_algebra. @@ -158,14 +158,14 @@ Module E. Section PointCompression. Local Notation "x ^2" := (x*x). Definition solve_for_x2 (y : F) := ((y^2 - 1) / (d * (y^2) - a)). - + Lemma a_d_y2_nonzero : forall y, d * y^2 - a <> 0. 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)]; field_algebra. Qed. - + Lemma solve_correct : forall x y, onCurve (x, y) <-> (x^2 = solve_for_x2 y). Proof. unfold solve_for_x2; simpl; split; intros; field_algebra; auto using a_d_y2_nonzero. @@ -189,10 +189,10 @@ Module E. Create HintDb field_homomorphism discriminated. Hint Rewrite <- homomorphism_one - homomorphism_add - homomorphism_sub - homomorphism_mul - homomorphism_div + homomorphism_add + homomorphism_sub + homomorphism_mul + homomorphism_div Ha Hd : field_homomorphism. diff --git a/src/CompleteEdwardsCurve/ExtendedCoordinates.v b/src/CompleteEdwardsCurve/ExtendedCoordinates.v index 49c5d5041..25af83a0a 100644 --- a/src/CompleteEdwardsCurve/ExtendedCoordinates.v +++ b/src/CompleteEdwardsCurve/ExtendedCoordinates.v @@ -127,7 +127,7 @@ Module Extended. destruct Hrep as [HA HB]. rewrite <-!HA, <-!HB; clear HA HB. split; reflexivity. Qed. - + Global Instance Proper_add : Proper (eq==>eq==>eq) add. Proof. unfold eq. intros x y H x0 y0 H0. @@ -204,10 +204,10 @@ Module Extended. Create HintDb field_homomorphism discriminated. Hint Rewrite <- homomorphism_one - homomorphism_add - homomorphism_sub - homomorphism_mul - homomorphism_div + homomorphism_add + homomorphism_sub + homomorphism_mul + homomorphism_div Ha Hd Hdd diff --git a/src/CompleteEdwardsCurve/Pre.v b/src/CompleteEdwardsCurve/Pre.v index 397a6259c..5314ee37c 100644 --- a/src/CompleteEdwardsCurve/Pre.v +++ b/src/CompleteEdwardsCurve/Pre.v @@ -16,14 +16,14 @@ Section Pre. Context {a:F} {a_nonzero : a<>0} {a_square : exists sqrt_a, sqrt_a^2 = a}. Context {d:F} {d_nonsquare : forall sqrt_d, sqrt_d^2 <> d}. Context {char_gt_2 : 1+1 <> 0}. - + (* the canonical definitions are in Spec *) Definition onCurve (P:F*F) := let (x, y) := P in a*x^2 + y^2 = 1 + d*x^2*y^2. Definition unifiedAdd' (P1' P2':F*F) : F*F := let (x1, y1) := P1' in let (x2, y2) := P2' in pair (((x1*y2 + y1*x2)/(1 + d*x1*x2*y1*y2))) (((y1*y2 - a*x1*x2)/(1 - d*x1*x2*y1*y2))). - + Ltac use_sqrt_a := destruct a_square as [sqrt_a a_square']; rewrite <-a_square' in *. Lemma edwardsAddComplete' x1 y1 x2 y2 : @@ -44,13 +44,13 @@ Section Pre. 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. - + 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. - + Lemma zeroOnCurve : onCurve (0, 1). Proof. simpl. field_algebra. Qed. - + Lemma unifiedAdd'_onCurve : forall P1 P2, onCurve P1 -> onCurve P2 -> onCurve (unifiedAdd' P1 P2). Proof. @@ -71,7 +71,7 @@ Section RespectsFieldHomomorphism. Let phip := fun (P':F*F) => let (x, y) := P' in (phi x, phi y). - Let eqp := fun (P1' P2':K*K) => + Let eqp := fun (P1' P2':K*K) => let (x1, y1) := P1' in let (x2, y2) := P2' in and (eq x1 x2) (eq y1 y2). @@ -79,11 +79,11 @@ Section RespectsFieldHomomorphism. Create HintDb field_homomorphism discriminated. Hint Rewrite homomorphism_one - homomorphism_add - homomorphism_sub - homomorphism_mul - homomorphism_div - a_ok + homomorphism_add + homomorphism_sub + homomorphism_mul + homomorphism_div + a_ok d_ok : field_homomorphism. -- cgit v1.2.3