1 files changed, 25 insertions, 23 deletions

diff --git a/src/CompleteEdwardsCurve/Pre.v b/src/CompleteEdwardsCurve/Pre.v
index fea4a99b3..f10e587d6 100644
--- a/src/CompleteEdwardsCurve/Pre.v
+++ b/src/CompleteEdwardsCurve/Pre.v
@@ -1,9 +1,11 @@
 Require Import Coq.ZArith.BinInt Coq.ZArith.Znumtheory Crypto.Tactics.VerdiTactics.
+Require Import Coq.omega.Omega.
 
 Require Import Crypto.Spec.ModularArithmetic.
 Require Import Crypto.ModularArithmetic.PrimeFieldTheorems.
+Local Open Scope Z_scope.
 Local Open Scope F_scope.
-  
+
 Section Pre.
   Context {q : BinInt.Z}.
   Context {a : F q}.
@@ -20,8 +22,8 @@ Section Pre.
      postprocess [Fpostprocess],
      constants [Fconstant],
      div (@Fmorph_div_theory q),
-     power_tac (@Fpower_theory q) [Fexp_tac]). 
-  
+     power_tac (@Fpower_theory q) [Fexp_tac]).
+
   (* the canonical definitions are in Spec *)
   Local Notation onCurve P := (let '(x, y) := P in a*x^2 + y^2 = 1 + d*x^2*y^2).
   Local Notation unifiedAdd' P1' P2' := (
@@ -29,7 +31,7 @@ Section Pre.
     let '(x2, y2) := P2' in
     (((x1*y2  +  y1*x2)/(1 + d*x1*x2*y1*y2)) , ((y1*y2 - a*x1*x2)/(1 - d*x1*x2*y1*y2)))
   ).
-  
+
   Lemma char_gt_2 : ZToField 2 <> (0: F q).
     intro; find_injection.
     pose proof two_lt_q.
@@ -38,7 +40,7 @@ Section Pre.
 
   Ltac rewriteAny := match goal with [H: _ = _ |- _ ] => rewrite H end.
   Ltac rewriteLeftAny := match goal with [H: _ = _ |- _ ] => rewrite <- H end.
-  
+
   Ltac whatsNotZero :=
     repeat match goal with
     | [H: ?lhs = ?rhs |- _ ] =>
@@ -67,11 +69,11 @@ Section Pre.
     (d*x1*x2*y1*y2)^2 <> 1.
   Proof.
     intros Hc1 Hc2 Hcontra; simpl in Hc1, Hc2; whatsNotZero.
-  
-    pose proof char_gt_2. pose proof a_nonzero as Ha_nonzero. 
+
+    pose proof char_gt_2. pose proof a_nonzero as Ha_nonzero.
     destruct a_square as [sqrt_a a_square'].
     rewrite <-a_square' in *.
-  
+
     (* Furthermore... *)
     pose proof (eq_refl (d*x1^2*y1^2*(sqrt_a^2*x2^2 + y2^2))) as Heqt.
     rewrite Hc2 in Heqt at 2.
@@ -80,7 +82,7 @@ Section Pre.
     rewrite Hcontra in Heqt.
     replace (d * x1 ^ 2 * y1 ^ 2 + 1) with (1 + d * x1 ^ 2 * y1 ^ 2) in Heqt by field.
     rewrite <-Hc1 in Heqt.
-  
+
     (* main equation for both potentially nonzero denominators *)
     destruct (F_eq_dec (sqrt_a*x2 + y2) 0); destruct (F_eq_dec (sqrt_a*x2 - y2) 0);
       try lazymatch goal with [H: ?f (sqrt_a * x2)  y2 <> 0 |- _ ] =>
@@ -97,11 +99,11 @@ Section Pre.
             destruct (d_nonsquare (n/l)); (remember n; rewriteAny; field; auto)
         end
       end.
-  
+
     assert (Hc: (sqrt_a * x2 + y2) + (sqrt_a * x2 - y2) = 0) by (repeat rewriteAny; field).
-  
+
     replace (sqrt_a * x2 + y2 + (sqrt_a * x2 - y2)) with (ZToField 2 * sqrt_a * x2) in Hc by field.
-  
+
     (* contradiction: product of nonzero things is zero *)
     destruct (Fq_mul_zero_why _ _ Hc) as [Hcc|Hcc]; subst; intuition.
     destruct (Fq_mul_zero_why _ _ Hcc) as [Hccc|Hccc]; subst; intuition.
@@ -119,7 +121,7 @@ Section Pre.
     - replace (d * x1 * x2 * y1 * y2) with (1+d * x1 * x2 * y1 * y2-1) in H by field.
       intro Hz; rewrite Hz in H; intuition.
   Qed.
-  
+
   Lemma edwardsAddCompleteMinus x1 y1 x2 y2 :
     onCurve (x1, y1) ->
     onCurve (x2, y2) ->
@@ -130,27 +132,27 @@ Section Pre.
     - replace (d * x1 * x2 * y1 * y2) with ((1-(1-d * x1 * x2 * y1 * y2))) in H by field.
       intro Hz; rewrite Hz in H; apply H; field.
   Qed.
-  
+
   Definition zeroOnCurve : onCurve (0, 1).
     simpl. field.
   Qed.
-  
+
   Lemma unifiedAdd'_onCurve' x1 y1 x2 y2 x3 y3
     (H: (x3, y3) = unifiedAdd' (x1, y1) (x2, y2)) :
     onCurve (x1, y1) -> onCurve (x2, y2) -> onCurve (x3, y3).
   Proof.
     (* https://eprint.iacr.org/2007/286.pdf Theorem 3.1;
-      * c=1 and an extra a in front of x^2 *) 
-  
-    injection H; clear H; intros.
-  
+      * c=1 and an extra a in front of x^2 *)
+
+    injection H; cbv beta iota; clear H; intros.
+
     Ltac t x1 y1 x2 y2 :=
       assert ((a*x2^2 + y2^2)*d*x1^2*y1^2
              = (1 + d*x2^2*y2^2) * d*x1^2*y1^2) by (rewriteAny; auto);
       assert (a*x1^2 + y1^2 - (a*x2^2 + y2^2)*d*x1^2*y1^2
              = 1 - d^2*x1^2*x2^2*y1^2*y2^2) by (repeat rewriteAny; field).
     t x1 y1 x2 y2; t x2 y2 x1 y1.
-  
+
     remember ((a*x1^2 + y1^2 - (a*x2^2+y2^2)*d*x1^2*y1^2)*(a*x2^2 + y2^2 -
       (a*x1^2 + y1^2)*d*x2^2*y2^2)) as T.
     assert (HT1: T = (1 - d^2*x1^2*x2^2*y1^2*y2^2)^2) by (repeat rewriteAny; field).
@@ -158,7 +160,7 @@ Section Pre.
     (y1 * y2 - a * x1 * x2) * (1 + d * x1 * x2 * y1 * y2)) ^ 2 -d * ((x1 *
      y2 + y1 * x2)* (y1 * y2 - a * x1 * x2))^2)) by (subst; field).
     replace (1:F q) with (a*x3^2 + y3^2 -d*x3^2*y3^2); [field|]; subst x3 y3.
-  
+
     match goal with [ |- ?x = 1 ] => replace x with
     ((a * ((x1 * y2 + y1 * x2) * (1 - d * x1 * x2 * y1 * y2)) ^ 2 +
      ((y1 * y2 - a * x1 * x2) * (1 + d * x1 * x2 * y1 * y2)) ^ 2 -
@@ -175,7 +177,7 @@ Section Pre.
       auto using Fq_pow_nonzero, Fq_mul_nonzero_nonzero,
         edwardsAddCompleteMinus, edwardsAddCompletePlus.
   Qed.
-  
+
   Lemma unifiedAdd'_onCurve : forall P1 P2, onCurve P1 -> onCurve P2 ->
     onCurve (unifiedAdd' P1 P2).
   Proof.
@@ -183,4 +185,4 @@ Section Pre.
     remember (unifiedAdd' (f, f0) (f1, f2)) as r; destruct r.
     eapply unifiedAdd'_onCurve'; eauto.
   Qed.
-End Pre.
\ No newline at end of file
+End Pre.