port CompleteEdwardsCurveTheorems (builds again)

1 files changed, 48 insertions, 22 deletions

diff --git a/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v b/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v
index cc6234762..66dbf86da 100644
--- a/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v
+++ b/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v
@@ -6,8 +6,7 @@ Require Import Coq.Logic.Eqdep_dec.
 Require Import Crypto.Tactics.VerdiTactics.
 Require Import Coq.Classes.Morphisms.
 Require Import Relation_Definitions.
-Require Import Crypto.Util.Tuple.
-Require Import Crypto.Util.Notations.
+Require Import Crypto.Util.Tuple Crypto.Util.Notations Crypto.Util.Tactics.
 
 Module E.
   Import Group ScalarMult Ring Field CompleteEdwardsCurve.E.
@@ -37,49 +36,75 @@ Module E.
                destruct p as [[x y] pf]
              end.
 
-    Local Obligation Tactic := intros; destruct_points; simpl; field_algebra.
+    Local Obligation Tactic := intros; destruct_points; simpl; super_nsatz.
     Program Definition opp (P:point) : point :=
       exist _ (let '(x, y) := coordinates P in (Fopp x, y) ) _.
 
+    (* all nonzero-denominator goals here require proofs that are not
+    trivially implied by field axioms. Posing all such proofs at once
+    and then solving the nonzero-denominator goal using [super_nsatz]
+    is too slow because the context contains many assumed nonzero
+    expressions and the product of all of them is a very large
+    polynomial. However, we never need to use more than one
+    nonzero-ness assumption for a given nonzero-denominator goal, so
+    we can try them separately one-by-one. *)
+
+    Ltac apply_field_nonzero H :=
+      match goal with |- not (Feq _ 0) => idtac | _ => fail "not a nonzero goal" end;
+      try solve [exact H];
+      let Hx := fresh "H" in
+      intro Hx;
+      apply H;
+      try conservative_common_denominator;
+      [rewrite <-Hx; ring | ..].
+      
     Ltac bash_step :=
+      let addCompletePlus := constr:(edwardsAddCompletePlus(char_gt_2:=char_gt_2)(d_nonsquare:=nonsquare_d)(a_square:=square_a)(a_nonzero:=nonzero_a)) in
+      let addCompleteMinus := constr:(edwardsAddCompleteMinus(char_gt_2:=char_gt_2)(d_nonsquare:=nonsquare_d)(a_square:=square_a)(a_nonzero:=nonzero_a)) in
+      let addOnCurve := constr:(unifiedAdd'_onCurve(char_gt_2:=char_gt_2)(d_nonsquare:=nonsquare_d)(a_square:=square_a)(a_nonzero:=nonzero_a)) in
       match goal with
       | |- _ => progress intros
       | [H: _ /\ _ |- _ ] => destruct H
+      | [H: ?a = ?b |- _ ] => is_var a; is_var b; repeat rewrite <-H in *; clear H b (* fast path *)
       | |- _ => progress destruct_points
       | |- _ => progress cbv [fst snd coordinates proj1_sig eq fieldwise fieldwise' add zero opp] in *
       | |- _ => split
-      | |- Feq _ _ => field_algebra
+      | [H:Feq (a*_^2+_^2) (1 + d*_^2*_^2) |- _ <> 0]
+        => apply_field_nonzero (addCompletePlus _ _ _ _ H H) ||
+           apply_field_nonzero (addCompleteMinus _ _ _ _ H H)
+      | [A:Feq (a*_^2+_^2) (1 + d*_^2*_^2),
+           B:Feq (a*_^2+_^2) (1 + d*_^2*_^2) |- _ <> 0]
+        => apply_field_nonzero (addCompletePlus _ _ _ _ A B) ||
+           apply_field_nonzero (addCompleteMinus _ _ _ _ A B)
+      | [A:Feq (a*_^2+_^2) (1 + d*_^2*_^2),
+           B:Feq (a*_^2+_^2) (1 + d*_^2*_^2),
+             C:Feq (a*_^2+_^2) (1 + d*_^2*_^2) |- _ <> 0]
+        => apply_field_nonzero (addCompleteMinus _ _ _ _ A (addOnCurve (_, _) (_, _) B C)) ||
+           apply_field_nonzero (addCompletePlus _ _ _ _ A (addOnCurve (_, _) (_, _) B C))
+      | |- ?x <> 0 => let H := fresh "H" in assert (x = 1) as H by ring; rewrite H; exact one_neq_zero
+      | |- Feq _ _ => progress conservative_common_denominator
+      | |- Feq _ _ => nsatz
+      | |- _ => exact _ (* typeclass instances *)
       end.
 
     Ltac bash := repeat bash_step.
 
-    Global Instance Proper_add : Proper (eq==>eq==>eq) add.
-    Proof. bash.
-           pose proof edwardsAddCompletePlus(char_gt_2:=char_gt_2)(d_nonsquare:=nonsquare_d)(a_square:=square_a)(a_nonzero:=nonzero_a) as Hxy.
-           specialize (Hxy _ _ _ _ pfx pfy).
-           pose proof (edwardsAddCompletePlus(char_gt_2:=char_gt_2)(d_nonsquare:=nonsquare_d)(a_square:=square_a)(a_nonzero:=nonzero_a) _ _ _ _ pfx pfy).
-    Qed.
+    Global Instance Proper_add : Proper (eq==>eq==>eq) add. Proof. bash. Qed.
     Global Instance Proper_opp : Proper (eq==>eq) opp. Proof. bash. Qed.
     Global Instance Proper_coordinates : Proper (eq==>fieldwise (n:=2) Feq) coordinates. Proof. bash. Qed.
-
     Global Instance edwards_acurve_abelian_group : abelian_group (eq:=eq)(op:=add)(id:=zero)(inv:=opp).
     Proof.
       bash.
-      (* TODO: port denominator-nonzero proofs for associativity *)
-      match goal with | |- _ <> 0 => admit end.
-      match goal with | |- _ <> 0 => admit end.
-      match goal with | |- _ <> 0 => admit end.
-      match goal with | |- _ <> 0 => admit end.
-    Admitted.
+    Qed.
 
     Global Instance Proper_mul : Proper (Logic.eq==>eq==>eq) mul.
     Proof.
-      intros n m Hnm P Q HPQ. rewrite <-Hnm; clear Hnm m.
-      induction n; simpl; rewrite ?IHn, ?HPQ; reflexivity.
+      intros n n'; repeat intro; subst n'.
+      induction n; (reflexivity || eapply Proper_add; eauto).
     Qed.
 
     Global Instance mul_is_scalarmult : @is_scalarmult point eq add zero mul.
-    Proof. split; intros; reflexivity || typeclasses eauto. Qed.
+    Proof. unfold mul; split; intros; (reflexivity || exact _). Qed.
 
     Section PointCompression.
       Local Notation "x ^ 2" := (x*x).
@@ -89,12 +114,13 @@ Module E.
       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.
+        destruct (eq_dec y 0); [apply nonzero_a | apply nonsquare_d with (sqrt_a/y)]; super_nsatz.
       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.
+        unfold solve_for_x2; simpl; split; intros;
+          (conservative_common_denominator_all; [nsatz | auto using a_d_y2_nonzero]).
       Qed.
     End PointCompression.
   End CompleteEdwardsCurveTheorems.