super_nsatz: Handle x^2 = y^2 -> x <> -y -> x = y

After    | File Name                                         | Before   || Change
------------------------------------------------------------------------------------
2m38.35s | Total                                             | 2m36.78s || +0m01.57s
------------------------------------------------------------------------------------
0m27.68s | Specific/GF25519                                  | 0m27.26s || +0m00.41s
0m25.00s | CompleteEdwardsCurve/ExtendedCoordinates          | 0m24.87s || +0m00.12s
0m24.96s | ModularArithmetic/ModularBaseSystemProofs         | 0m24.84s || +0m00.12s
0m21.55s | Experiments/SpecEd25519                           | 0m21.39s || +0m00.16s
0m19.82s | CompleteEdwardsCurve/CompleteEdwardsCurveTheorems | 0m19.65s || +0m00.17s
0m08.29s | ModularArithmetic/PrimeFieldTheorems              | 0m08.30s || -0m00.01s
0m07.13s | Specific/GF1305                                   | 0m06.69s || +0m00.43s
0m03.75s | ModularArithmetic/Tutorial                        | 0m03.77s || -0m00.02s
0m03.69s | ModularArithmetic/ModularBaseSystemOpt            | 0m03.71s || -0m00.02s
0m03.64s | CompleteEdwardsCurve/Pre                          | 0m03.67s || -0m00.02s
0m02.11s | Algebra                                           | 0m01.96s || +0m00.14s
0m01.81s | Experiments/DerivationsOptionRectLetInEncoding    | 0m01.83s || -0m00.02s
0m01.73s | Experiments/EdDSARefinement                       | 0m01.71s || +0m00.02s
0m01.67s | ModularArithmetic/ModularArithmeticTheorems       | 0m01.65s || +0m00.02s
0m00.91s | ModularArithmetic/ExtendedBaseVector              | 0m00.92s || -0m00.01s
0m00.80s | ModularArithmetic/PseudoMersenneBaseParamProofs   | 0m00.85s || -0m00.04s
0m00.60s | Encoding/ModularWordEncodingPre                   | 0m00.59s || +0m00.01s
0m00.59s | Encoding/ModularWordEncodingTheorems              | 0m00.61s || -0m00.02s
0m00.58s | ModularArithmetic/ModularBaseSystem               | 0m00.52s || +0m00.05s
0m00.57s | Spec/ModularWordEncoding                          | 0m00.53s || +0m00.03s
0m00.56s | Spec/EdDSA                                        | 0m00.56s || +0m00.00s
0m00.56s | ModularArithmetic/PseudoMersenneBaseRep           | 0m00.54s || +0m00.02s
0m00.36s | Spec/CompleteEdwardsCurve                         | 0m00.36s || +0m00.00s

1 files changed, 27 insertions, 10 deletions

diff --git a/src/Algebra.v b/src/Algebra.v
index 473571824..62b216b92 100644
--- a/src/Algebra.v
+++ b/src/Algebra.v
@@ -1038,32 +1038,49 @@ Ltac super_nsatz_post_clean_inequalities :=
   try assumption;
   prensatz_contradict; nsatz_inequality_to_equality;
   try nsatz.
+Ltac nsatz_equality_to_inequality_by_decide_equality :=
+  lazymatch goal with
+  | [ H : not (?R _ _) |- ?R _ _ ] => idtac
+  | [ H : (?R _ _ -> False)%type |- ?R _ _ ] => idtac
+  | [ |- ?R _ _ ] => fail 0 "No hypothesis exists which negates the relation" R
+  | [ |- ?G ] => fail 0 "The goal is not a binary relation:" G
+  end;
+  lazymatch goal with
+  | [ |- ?R ?x ?y ]
+    => destruct (@dec (R x y) _); [ assumption | exfalso ]
+  end.
 (** Handles inequalities and fractions *)
-Ltac super_nsatz :=
+Ltac super_nsatz_internal nsatz_alternative :=
   (* [nsatz] gives anomalies on duplicate hypotheses, so we strip them *)
   clear_algebraic_duplicates;
   prensatz_contradict;
   (* Each goal left over by [prensatz_contradict] is separate (and
      there might not be any), so we handle them all separately *)
   [ try conservative_common_denominator_equality_inequality_all;
-    [ try nsatz_inequality_to_equality; try nsatz;
-      (* [nstaz] might leave over side-conditions; we handle them if they are inequalities *)
-      try super_nsatz_post_clean_inequalities
+    [ try nsatz_inequality_to_equality;
+      try first [ nsatz;
+                  (* [nstaz] might leave over side-conditions; we handle them if they are inequalities *)
+                  try super_nsatz_post_clean_inequalities
+                | nsatz_alternative ]
     | super_nsatz_post_clean_inequalities.. ].. ].
 
+Ltac super_nsatz :=
+  super_nsatz_internal
+    (* if [nsatz] fails, we try turning the goal equality into an inequality and trying again *)
+    ltac:(nsatz_equality_to_inequality_by_decide_equality;
+          super_nsatz_internal idtac).
+
 Section ExtraLemmas.
   Context {F eq zero one opp add sub mul inv div} `{F_field:field F eq zero one opp add sub mul inv div}.
   Local Infix "+" := add. Local Infix "*" := mul. Local Infix "-" := sub. Local Infix "/" := div.
   Local Notation "0" := zero. Local Notation "1" := one.
   Local Infix "=" := eq : type_scope. Local Notation "a <> b" := (not (a = b)) : type_scope.
 
+  Example _only_two_square_roots_test x y : x * x = y * y -> x <> opp y -> x = y.
+  Proof. intros; super_nsatz. Qed.
+
   Lemma only_two_square_roots' x y : x * x = y * y -> x <> y -> x <> opp y -> False.
-  Proof.
-    intros.
-    canonicalize_field_equalities; canonicalize_field_inequalities.
-    assert (H' : (x + y) * (x - y) <> 0) by (apply mul_nonzero_nonzero; assumption).
-    apply H'; nsatz.
-  Qed.
+  Proof. intros; super_nsatz. Qed.
 
   Lemma only_two_square_roots x y z : x * x = z -> y * y = z -> x <> y -> x <> opp y -> False.
   Proof.