Prove relationship between `xzladderstep` and M.add (#162)

* hopefully all proofs we need about xzladderstep

* Better automation in xzproofs

* Speed up xzproofs with heuristic clearing

* Remove useless hypotheses

* XZProofs cleanup

* fix "group by isomorphism" proofs, use in XZProofs

3 files changed, 19 insertions, 144 deletions

diff --git a/src/Curves/Edwards/AffineProofs.v b/src/Curves/Edwards/AffineProofs.v
index 2d1db7126..e77e39f50 100644
--- a/src/Curves/Edwards/AffineProofs.v
+++ b/src/Curves/Edwards/AffineProofs.v
@@ -51,7 +51,7 @@ Module E.
       | _ => solve [trivial | exact _ ]
       | _ => intro
       | |- Equivalence _ => split
-      | |- abelian_group => split | |- group => split | |- monoid => split
+      | |- commutative_group => split | |- group => split | |- monoid => split
       | |- is_associative => split | |- is_commutative => split
       | |- is_left_inverse => split | |- is_right_inverse => split
       | |- is_left_identity => split | |- is_right_identity => split
@@ -80,7 +80,7 @@ Module E.
       { intro. eapply H0. field_simplify_eq; repeat split; trivial. IntegralDomain.nsatz. }
     Qed.
 
-    Global Instance edwards_curve_abelian_group : abelian_group (eq:=eq)(op:=add)(id:=zero)(inv:=opp).
+    Global Instance edwards_curve_commutative_group : commutative_group (eq:=eq)(op:=add)(id:=zero)(inv:=opp).
     Proof using Type. t. Qed.
 
     Global Instance Proper_coordinates : Proper (eq==>fieldwise (n:=2) Feq) coordinates. Proof using Type. repeat t_step. Qed.
diff --git a/src/Curves/Edwards/Montgomery.v b/src/Curves/Edwards/Montgomery.v
deleted file mode 100644
index d274356c9..000000000
--- a/src/Curves/Edwards/Montgomery.v
+++ /dev/null
@@ -1,114 +0,0 @@
-Require Import Crypto.Curves.Edwards.AffineProofs.
-Require Import Crypto.Spec.MontgomeryCurve Crypto.Curves.Montgomery.AffineProofs.
-Require Import Crypto.Curves.Montgomery.Affine.
-
-Require Import Crypto.Util.Notations Crypto.Util.Decidable.
-Require Import (*Crypto.Util.Tactics*) Crypto.Util.Sum Crypto.Util.Prod.
-Require Import Crypto.Algebra.Field.
-Import BinNums.
-
-Module E.
-  Section EdwardsMontgomery.
-    Context {F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv}
-            {field:@Algebra.Hierarchy.field F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv}
-            {char_ge_28 : @Ring.char_ge F Feq Fzero Fone Fopp Fadd Fsub Fmul 28}
-            {Feq_dec:DecidableRel Feq}.
-    Local Infix "=" := Feq : type_scope. Local Notation "a <> b" := (not (a = b)) : type_scope.
-    Local Notation "0" := Fzero.  Local Notation "1" := Fone.
-    Local Infix "+" := Fadd. Local Infix "*" := Fmul.
-    Local Infix "-" := Fsub. Local Infix "/" := Fdiv.
-    Local Notation "x ^ 2" := (x*x).
-
-    Let char_ge_12 : @Ring.char_ge F Feq Fzero Fone Fopp Fadd Fsub Fmul 12.
-    Proof. eapply Algebra.Hierarchy.char_ge_weaken; eauto. vm_decide. Qed.
-    Let char_ge_3 : @Ring.char_ge F Feq Fzero Fone Fopp Fadd Fsub Fmul 3.
-    Proof. eapply Algebra.Hierarchy.char_ge_weaken; eauto. vm_decide. Qed.
-
-    Context {a d: F}
-            {nonzero_a : a <> 0}
-            {square_a : exists sqrt_a, sqrt_a^2 = a}
-            {nonsquare_d : forall x, x^2 <> d}.
-    Local Notation Epoint := (@E.point F Feq Fone Fadd Fmul a d).
-    Local Notation Ezero  := (E.zero(nonzero_a:=nonzero_a)(d:=d)).
-    Local Notation Eadd   := (E.add(char_ge_3:=char_ge_3)(nonzero_a:=nonzero_a)(square_a:=square_a)(nonsquare_d:=nonsquare_d)).
-    Local Notation Eopp   := (E.opp(nonzero_a:=nonzero_a)(d:=d)).
-
-    Let a_neq_d : a <> d.
-    Proof. intro X.
-           edestruct square_a. eapply nonsquare_d.
-           rewrite <-X. eassumption. Qed.
-
-    
-    Local Notation "2" := (1+1). Local Notation "4" := (1+1+1+1).
-    Local Notation MontgomeryA := (2*(a+d)/(a-d)).
-    Local Notation MontgomeryB := (4/(a-d)).
-
-    Let b_nonzero : MontgomeryB <> 0. Proof. fsatz. Qed.
-
-    Local Notation Mpoint := (@M.point F Feq Fadd Fmul MontgomeryA MontgomeryB).
-    Local Notation Madd := (@M.add F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv field Feq_dec char_ge_3 MontgomeryA MontgomeryB b_nonzero).
-    Local Notation "'∞'" := (inr tt) : core_scope.
-
-    Ltac t_step :=
-        match goal with
-        | _ => solve [ contradiction | trivial ]
-        | _ => progress intros
-        | _ => progress subst
-        | _ => progress Tactics.DestructHead.destruct_head' @M.point
-        | _ => progress Tactics.DestructHead.destruct_head' @prod
-        | _ => progress Tactics.DestructHead.destruct_head' @sum
-        | _ => progress Tactics.DestructHead.destruct_head' @and
-        | _ => progress Sum.inversion_sum
-        | _ => progress Prod.inversion_prod
-        | _ => progress Tactics.BreakMatch.break_match_hyps
-        | _ => progress Tactics.BreakMatch.break_match
-        | _ => progress cbv [E.coordinates M.coordinates E.add M.add E.zero M.zero E.eq M.eq E.opp M.opp proj1_sig fst snd] in *
-        | |- _ /\ _ => split
-        end.
-    Ltac t := repeat t_step.
-
-    Program Definition to_Montgomery (P:Epoint) : Mpoint :=
-      match E.coordinates P return F*F+_ with
-      | (x, y) => 
-        if dec (y <> 1 /\ x <> 0)
-        then inl ((1+y)/(1-y), (1+y)/(x-x*y))
-        else ∞
-      end.
-    Next Obligation. Proof. t. fsatz. Qed.
-
-    (* The exceptional cases are tricky. *)
-    (* See https://eprint.iacr.org/2008/013.pdf page 5 before continuing *)
-
-    Program Definition of_Montgomery (P:Mpoint) : Epoint :=
-      match M.coordinates P return F*F with
-      | inl (x,y) =>
-        if dec (y = 0)
-        then (0, Fopp 1)
-        else (x/y, (x-1)/(x+1))
-      | ∞ => pair 0 1
-      end.
-    Next Obligation.
-    Proof.
-      t; try fsatz.
-      assert (f1 <> Fopp 1) by admit (* ad, d are nonsero *); fsatz.
-    Admitted.
-
-    Program Definition _EM (discr_nonzero:id _) : _ /\ _ /\ _ :=
-      @Group.group_from_redundant_representation
-        Mpoint M.eq Madd M.zero M.opp
-        (M.group discr_nonzero)
-        Epoint E.eq Eadd Ezero Eopp
-        of_Montgomery
-        to_Montgomery
-        _ _ _ _ _
-    .
-    Next Obligation. Proof. Admitted. (* M->E->M *)
-    Next Obligation. Proof. Admitted. (* equivalences match *)
-    Next Obligation. Proof. Admitted. (* add *)
-    Next Obligation. Proof. Admitted. (* opp *)
-    Next Obligation. Proof. cbv [of_Montgomery to_Montgomery]; t; fsatz. Qed.
-
-    Global Instance homomorphism_of_Montgomery discr_nonzero : Monoid.is_homomorphism(phi:=of_Montgomery) := proj1 (proj2 (_EM discr_nonzero)).
-    Global Instance homomorphism_to_Montgomery discr_nonzero : Monoid.is_homomorphism(phi:=to_Montgomery) := proj2 (proj2 (_EM discr_nonzero)).
-  End EdwardsMontgomery.
-End E.
diff --git a/src/Curves/Edwards/XYZT.v b/src/Curves/Edwards/XYZT.v
index 160866b64..2b126dfcb 100644
--- a/src/Curves/Edwards/XYZT.v
+++ b/src/Curves/Edwards/XYZT.v
@@ -107,34 +107,23 @@ Module Extended.
         end.
       Next Obligation. pose proof (E.denominator_nonzero _ nonzero_a square_a _ nonsquare_d _ _ (proj2_sig (to_twisted P1))  _ _  (proj2_sig (to_twisted P2))); t. Qed.
 
-      Program Definition _group_proof nonzero_a' square_a' nonsquare_d' : Algebra.Hierarchy.group /\ _ /\ _ :=
-                 @Group.group_from_redundant_representation
-                   _ _ _ _ _
-                   ((E.edwards_curve_abelian_group(a:=a)(d:=d)(nonzero_a:=nonzero_a')(square_a:=square_a')
-                                                  (nonsquare_d:=nonsquare_d')).(Algebra.Hierarchy.abelian_group_group))
-                   _
-                   eq
-                   m1add
-                   zero
-                   opp
-                   from_twisted
-                   to_twisted
-                   to_twisted_from_twisted
-                   _ _ _ _.
-      Next Obligation. cbv [to_twisted]. t. Qed.
-      Next Obligation.
-        match goal with
-        | |- context[E.add ?P ?Q] =>
-          unique pose proof (E.denominator_nonzero _ nonzero_a square_a _ nonsquare_d _ _  (proj2_sig P)  _ _  (proj2_sig Q))
-        end. cbv [to_twisted m1add]. t. Qed.
-      Next Obligation. cbv [to_twisted opp]. t. Qed.
-      Next Obligation. cbv [to_twisted zero]. t. Qed.
-      Global Instance group x y z
-        : Algebra.Hierarchy.group := proj1 (_group_proof x y z).
-      Global Instance homomorphism_from_twisted x y z :
-        Monoid.is_homomorphism := proj1 (proj2 (_group_proof x y z)).
-      Global Instance homomorphism_to_twisted x y z :
-        Monoid.is_homomorphism := proj2 (proj2 (_group_proof x y z)).
+      Global Instance isomorphic_commutative_group_m1 :
+        @Group.isomorphic_commutative_groups
+          Epoint E.eq
+            (E.add(nonzero_a:=nonzero_a)(square_a:=square_a)(nonsquare_d:=nonsquare_d))
+            (E.zero(nonzero_a:=nonzero_a))
+            (E.opp(nonzero_a:=nonzero_a))
+          point eq m1add zero opp
+          from_twisted to_twisted.
+      Proof.
+        eapply Group.commutative_group_by_isomorphism; try exact _.
+        par: abstract
+               (cbv [to_twisted from_twisted zero opp m1add]; intros;
+                repeat match goal with
+                       | |- context[E.add ?P ?Q] =>
+                         unique pose proof (E.denominator_nonzero _ nonzero_a square_a _ nonsquare_d _ _  (proj2_sig P)  _ _  (proj2_sig Q)) end;
+                t).
+      Qed.
     End TwistMinusOne.
   End ExtendedCoordinates.
 End Extended.