Add a tactic for field inequalities

Pair programming with Andres, a better proof of unifiedAddM1'_rep, some
progress on twistedAddAssoc.

5 files changed, 131 insertions, 48 deletions

diff --git a/_CoqProject b/_CoqProject
index 1d65a7564..ea5503260 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -16,8 +16,8 @@ src/ModularArithmetic/ModularBaseSystem.v
 src/ModularArithmetic/ModularBaseSystemProofs.v
 src/ModularArithmetic/Pre.v
 src/ModularArithmetic/PrimeFieldTheorems.v
-src/ModularArithmetic/PseudoMersenneBaseParams.v
 src/ModularArithmetic/PseudoMersenneBaseParamProofs.v
+src/ModularArithmetic/PseudoMersenneBaseParams.v
 src/ModularArithmetic/PseudoMersenneBaseRep.v
 src/ModularArithmetic/Tutorial.v
 src/Spec/CompleteEdwardsCurve.v
@@ -34,5 +34,6 @@ src/Util/IterAssocOp.v
 src/Util/ListUtil.v
 src/Util/NatUtil.v
 src/Util/NumTheoryUtil.v
+src/Util/Tactics.v
 src/Util/WordUtil.v
 src/Util/ZUtil.v
diff --git a/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v b/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v
index 3740f5a29..6ea5ec283 100644
--- a/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v
+++ b/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v
@@ -57,8 +57,26 @@ Section CompleteEdwardsCurveTheorems.
   Proof.
     (* The Ltac takes ~15s, the Qed no longer takes longer than I have had patience for *)
     Edefn; F_field_simplify_eq; try abstract (rewrite ?@F_pow_2_r in *; clear_prm; F_nsatz);
-      repeat split; match goal with [ |- _ = 0%F -> False ] => admit end;
-        fail "unreachable".
+      pose proof (@edwardsAddCompletePlus _ _ _ _ two_lt_q nonzero_a square_a nonsquare_d);
+      pose proof (@edwardsAddCompleteMinus _ _ _ _ two_lt_q nonzero_a square_a nonsquare_d);
+      cbv beta iota in *;
+      repeat split.
+    { field_nonzero idtac. }
+    { field_nonzero idtac. }
+    2: field_nonzero idtac.
+    2: field_nonzero idtac.
+    3: field_nonzero idtac.
+    3: field_nonzero idtac.
+    4: field_nonzero idtac.
+    4: field_nonzero idtac.
+    4:field_nonzero idtac.
+    3:field_nonzero idtac.
+    2:field_nonzero idtac.
+    1:field_nonzero idtac.
+    admit.
+    admit.
+    admit.
+    admit.
   Qed.
 
   Lemma zeroIsIdentity : forall P, (P + zero = P)%E.
diff --git a/src/CompleteEdwardsCurve/ExtendedCoordinates.v b/src/CompleteEdwardsCurve/ExtendedCoordinates.v
index 976fe59c1..a9fbf5e40 100644
--- a/src/CompleteEdwardsCurve/ExtendedCoordinates.v
+++ b/src/CompleteEdwardsCurve/ExtendedCoordinates.v
@@ -3,7 +3,7 @@ Require Import Crypto.CompleteEdwardsCurve.CompleteEdwardsCurveTheorems.
 Require Import Crypto.ModularArithmetic.PrimeFieldTheorems.
 Require Import Crypto.ModularArithmetic.FField.
 Require Import Crypto.Tactics.VerdiTactics.
-Require Import Util.IterAssocOp BinNat NArith. 
+Require Import Util.IterAssocOp BinNat NArith.
 Require Import Coq.Setoids.Setoid Coq.Classes.Morphisms Coq.Classes.Equivalence.
 Local Open Scope equiv_scope.
 Local Open Scope F_scope.
@@ -19,10 +19,10 @@ Section ExtendedCoordinates.
      postprocess [Fpostprocess; try exact Fq_1_neq_0; try assumption],
      constants [Fconstant],
      div (@Fmorph_div_theory q),
-     power_tac (@Fpower_theory q) [Fexp_tac]). 
+     power_tac (@Fpower_theory q) [Fexp_tac]).
 
   Add Field Ffield_notConstant : (OpaqueFieldTheory q)
-    (constants [notConstant]). 
+    (constants [notConstant]).
 
   (** [extended] represents a point on an elliptic curve using extended projective
   * Edwards coordinates with twist a=-1 (see <https://eprint.iacr.org/2008/522.pdf>). *)
@@ -44,8 +44,8 @@ Section ExtendedCoordinates.
   Local Hint Unfold twistedToExtended extendedToTwisted rep.
   Local Notation "P '~=' rP" := (rep P rP) (at level 70).
 
-  Ltac unfoldExtended := 
-    repeat progress (autounfold; unfold onCurve, unifiedAdd, unifiedAdd', rep in *; intros); 
+  Ltac unfoldExtended :=
+    repeat progress (autounfold; unfold onCurve, unifiedAdd, unifiedAdd', rep in *; intros);
     repeat match goal with
       | [ p : (F q*F q)%type |- _ ] =>
           let x := fresh "x" p in
@@ -61,7 +61,7 @@ Section ExtendedCoordinates.
       | [ H: @eq (F q * F q)%type _ _ |- _ ] => invcs H
       | [ H: @eq F q ?x _ |- _ ] => isVar x; rewrite H; clear H
   end.
-  
+
   Ltac solveExtended := unfoldExtended;
     repeat match goal with
       | [ |- _ /\ _ ] => split
@@ -137,6 +137,8 @@ Section ExtendedCoordinates.
       (X3, Y3, Z3, T3).
     Local Hint Unfold unifiedAdd.
 
+    Local Ltac tnz := repeat apply Fq_mul_nonzero_nonzero; auto using (@char_gt_2 q two_lt_q).
+
     Lemma unifiedAddM1'_rep: forall P Q rP rQ, onCurve rP -> onCurve rQ ->
       P ~= rP -> Q ~= rQ -> (unifiedAddM1' P Q) ~= (unifiedAdd' rP rQ).
     Proof.
@@ -146,31 +148,8 @@ Section ExtendedCoordinates.
       unfoldExtended; rewrite a_eq_minus1 in *; simpl in *.
         repeat split; repeat apply (f_equal2 pair); try F_field; repeat split; auto;
         repeat rewrite ?F_add_0_r, ?F_add_0_l, ?F_sub_0_l, ?F_sub_0_r,
-           ?F_mul_0_r, ?F_mul_0_l, ?F_mul_1_l, ?F_mul_1_r, ?F_div_1_r.
-
-    Ltac tnz := repeat apply Fq_mul_nonzero_nonzero; auto using (@char_gt_2 q two_lt_q).
-    (* If we we had reasoning modulo associativity and commutativity,
-    *  the following tactic would probably solve all remaining goals here:
-    repeat match goal with [H1: @eq (F p) _ _, H2: @eq (F p) _ _ |- _ ] =>
-      let H := fresh "H" in ( 
-        pose proof (edwardsAddCompletePlus _ _ _ _ H1 H2) as H;
-        match type of H with ?xs <> 0 => ac_rewrite (eq_refl xs) end
-      ) || (
-        pose proof (edwardsAddCompleteMinus _ _ _ _ H1 H2) as H;
-        match type of H with ?xs <> 0 => ac_rewrite (eq_refl xs) end
-      ); tnz
-    end. *)
-
-      - replace (ZP * ZQ * ZP * ZQ + d * XP * XQ * YP * YQ) with (ZQ*ZQ*ZP*ZP* (1 + d * (XQ / ZQ) * (XP / ZP) * (YQ / ZQ) * (YP / ZP))) by (field; tnz); tnz.
-      - replace (ZP * ZToField 2 * ZQ * (ZP * ZQ)  + XP * YP * ZToField 2 * d * (XQ * YQ)) with (ZToField 2*ZQ*ZQ*ZP*ZP* (1 + d * (XQ / ZQ)  * (XP / ZP) * (YQ / ZQ)  * (YP / ZP))) by (field; tnz); tnz.
-      - replace (ZP * ZToField 2 * ZQ * (ZP * ZQ)  - XP * YP * ZToField 2 * d * (XQ * YQ)) with (ZToField 2*ZQ*ZQ*ZP*ZP* (1 - d * (XQ / ZQ)  * (XP / ZP) * (YQ / ZQ)  * (YP / ZP))) by (field; tnz); tnz.
-      - replace (ZP * ZQ * ZP * ZQ - d * XP * XQ * YP * YQ) with (ZQ*ZQ*ZP*ZP* (1 - d * (XQ / ZQ)  * (XP / ZP) * (YQ / ZQ)  * (YP / ZP))) by (field; tnz); tnz.
-      - replace (ZP * ZToField 2 * ZQ * (ZP * ZQ)  + XP * YP * ZToField 2 * d * (XQ * YQ)) with (ZToField 2*ZQ*ZQ*ZP*ZP* (1 + d * (XQ / ZQ)  * (XP / ZP) * (YQ / ZQ)  * (YP / ZP))) by (field; tnz); tnz.
-      - replace (ZP * ZToField 2 * ZQ * (ZP * ZQ)  - XP * YP * ZToField 2 * d * (XQ * YQ)) with (ZToField 2*ZQ*ZQ*ZP*ZP* (1 - d * (XQ / ZQ)  * (XP / ZP) * (YQ / ZQ)  * (YP / ZP))) by (field; tnz); tnz.
-      - replace (ZP * ZToField 2 * ZQ - XP * YP / ZP * ZToField 2 * d * (XQ * YQ / ZQ) ) with (ZToField 2*ZQ*ZP* (1 - d * (XQ / ZQ)  * (XP / ZP) * (YQ / ZQ)  * (YP / ZP))) by (field; tnz); tnz.
-        replace (ZP * ZToField 2 * ZQ + XP * YP / ZP * ZToField 2 * d * (XQ * YQ / ZQ) ) with (ZToField 2*ZQ*ZP* (1 + d * (XQ / ZQ)  * (XP / ZP) * (YQ / ZQ)  * (YP / ZP))) by (field; tnz); tnz.
-      - replace (ZP * ZToField 2 * ZQ * (ZP * ZQ)  + XP * YP * ZToField 2 * d * (XQ * YQ)) with (ZToField 2*ZQ*ZQ*ZP*ZP* (1 + d * (XQ / ZQ)  * (XP / ZP) * (YQ / ZQ)  * (YP / ZP))) by (field; tnz); tnz.
-      - replace (ZP * ZToField 2 * ZQ * (ZP * ZQ)  - XP * YP * ZToField 2 * d * (XQ * YQ)) with (ZToField 2*ZQ*ZQ*ZP*ZP* (1 - d * (XQ / ZQ)  * (XP / ZP) * (YQ / ZQ)  * (YP / ZP))) by (field; tnz); tnz.
+           ?F_mul_0_r, ?F_mul_0_l, ?F_mul_1_l, ?F_mul_1_r, ?F_div_1_r;
+        field_nonzero tnz.
     Qed.
 
     Lemma unifiedAdd'_onCurve : forall P Q, onCurve P -> onCurve Q -> onCurve (unifiedAdd' P Q).
@@ -238,4 +217,4 @@ Section ExtendedCoordinates.
 
   End TwistMinus1.
 
-End ExtendedCoordinates.
\ No newline at end of file
+End ExtendedCoordinates.
diff --git a/src/ModularArithmetic/PrimeFieldTheorems.v b/src/ModularArithmetic/PrimeFieldTheorems.v
index 77d84c455..130f85c84 100644
--- a/src/ModularArithmetic/PrimeFieldTheorems.v
+++ b/src/ModularArithmetic/PrimeFieldTheorems.v
@@ -9,6 +9,7 @@ Require Import Coq.Classes.Morphisms Coq.Setoids.Setoid.
 Require Import Coq.ZArith.BinInt Coq.NArith.BinNat Coq.ZArith.ZArith Coq.ZArith.Znumtheory Coq.NArith.NArith. (* import Zdiv before Znumtheory *)
 Require Import Coq.Logic.Eqdep_dec.
 Require Import Crypto.Util.NumTheoryUtil Crypto.Util.ZUtil.
+Require Import Crypto.Util.Tactics.
 
 Existing Class prime.
 
@@ -67,7 +68,7 @@ Module FieldModulo (Import M : PrimeModulus).
      postprocess [Fpostprocess],
      constants [Fconstant],
      div morph_div_theory_modulo,
-     power_tac power_theory_modulo [Fexp_tac]). 
+     power_tac power_theory_modulo [Fexp_tac]).
 End FieldModulo.
 
 Section VariousModPrime.
@@ -79,8 +80,8 @@ Section VariousModPrime.
      postprocess [Fpostprocess; try exact Fq_1_neq_0; try assumption],
      constants [Fconstant],
      div (@Fmorph_div_theory q),
-     power_tac (@Fpower_theory q) [Fexp_tac]). 
-  
+     power_tac (@Fpower_theory q) [Fexp_tac]).
+
   Lemma Fq_mul_eq : forall x y z : F q, z <> 0 -> x * z = y * z -> x = y.
   Proof.
     intros ? ? ? z_nonzero mul_z_eq.
@@ -139,27 +140,27 @@ Section VariousModPrime.
       apply ZToField_eqmod.
       demod; reflexivity.
   Qed.
- 
+
   Lemma Fq_mul_zero_why : forall a b : F q, a*b = 0 -> a = 0 \/ b = 0.
     intros.
     assert (Z := F_eq_dec a 0); destruct Z.
-  
+
     - left; intuition.
-  
+
     - assert (a * b / a = 0) by
         ( rewrite H; field; intuition ).
-  
+
       replace (a*b/a) with (b) in H0 by (field; trivial).
       right; intuition.
   Qed.
-  
+
   Lemma Fq_mul_nonzero_nonzero : forall a b : F q, a <> 0 -> b <> 0 -> a*b <> 0.
     intros; intuition; subst.
     apply Fq_mul_zero_why in H1.
     destruct H1; subst; intuition.
   Qed.
   Hint Resolve Fq_mul_nonzero_nonzero.
-  
+
   Lemma Fq_pow_zero : forall (p: N), p <> 0%N -> (0^p = @ZToField q 0)%F.
     induction p using N.peano_ind;
     rewrite <-?N.add_1_l, ?(proj2 (@F_pow_spec q _) _), ?(proj1 (@F_pow_spec q _)).
@@ -232,7 +233,7 @@ Section VariousModPrime.
       left.
       eapply Fq_square_mul; eauto.
       instantiate (1 := x).
-      assert (x ^ 2 = z * y ^ 2 - x ^ 2 + x ^ 2) as plus_minus_x2 by 
+      assert (x ^ 2 = z * y ^ 2 - x ^ 2 + x ^ 2) as plus_minus_x2 by
         (rewrite <- eq_zero_sub; ring).
       rewrite plus_minus_x2; ring.
     }
@@ -352,6 +353,22 @@ Section VariousModPrime.
   Proof.
     econstructor; eauto using Fq_mul_zero_why, Fq_1_neq_0.
   Qed.
+
+  Lemma add_cancel_mul_r_nonzero {y : F q} (H : y <> 0) (x z : F q)
+    : x * y + z = (x + (z * (inv y))) * y.
+  Proof. field. Qed.
+
+  Lemma sub_cancel_mul_r_nonzero {y : F q} (H : y <> 0) (x z : F q)
+    : x * y - z = (x - (z * (inv y))) * y.
+  Proof. field. Qed.
+
+  Lemma add_cancel_l_nonzero {y : F q} (H : y <> 0) (z : F q)
+    : y + z = (1 + (z * (inv y))) * y.
+  Proof. field. Qed.
+
+  Lemma sub_cancel_l_nonzero {y : F q} (H : y <> 0) (z : F q)
+    : y - z = (1 - (z * (inv y))) * y.
+  Proof. field. Qed.
 End VariousModPrime.
 
 Section SquareRootsPrime5Mod8.
@@ -367,7 +384,7 @@ Section SquareRootsPrime5Mod8.
      postprocess [Fpostprocess; try exact Fq_1_neq_0; try assumption],
      constants [Fconstant],
      div (@Fmorph_div_theory q),
-     power_tac (@Fpower_theory q) [Fexp_tac]). 
+     power_tac (@Fpower_theory q) [Fexp_tac]).
 
   (* This is only the square root of -1 if q mod 8 is 3 or 5 *)
   Definition sqrt_minus1 : F q :=  ZToField 2 ^ Z.to_N (q / 4).
@@ -382,7 +399,7 @@ Section SquareRootsPrime5Mod8.
   Qed.
 
   (* square root mod q relies on the fact that q is 5 mod 8 *)
-  Definition sqrt_mod_q (a : F q) := 
+  Definition sqrt_mod_q (a : F q) :=
     let b := a ^ Z.to_N (q / 8 + 1) in
     (match (F_eq_dec (b ^ 2) a) with
     | left A => b
@@ -445,4 +462,47 @@ Section SquareRootsPrime5Mod8.
     field.
   Qed.
 
-End SquareRootsPrime5Mod8.
\ No newline at end of file
+End SquareRootsPrime5Mod8.
+
+Local Open Scope F_scope.
+(** Tactics for solving inequalities. *)
+Ltac solve_cancel_by_field y tnz :=
+  solve [ generalize dependent y; intros;
+          field; tnz ].
+
+Ltac cancel_nonzero_factors' tnz :=
+  idtac;
+  match goal with
+  | [ |- ?x = 0 -> False ]
+    => change (x <> 0)
+  | [ |- ?x * ?y <> 0 ]
+    => apply Fq_mul_nonzero_nonzero
+  | [ H : ?y <> 0 |- _ ]
+    => progress rewrite ?(add_cancel_mul_r_nonzero H), ?(sub_cancel_mul_r_nonzero H), ?(add_cancel_l_nonzero H), ?(sub_cancel_l_nonzero H);
+       apply Fq_mul_nonzero_nonzero; [ | assumption ]
+  | [ |- ?op (?y * (ZToField (m := ?q) ?n)) ?z <> 0 ]
+    => unique assert (ZToField (m := q) n <> 0) by tnz;
+       generalize dependent (ZToField (m := q) n); intros
+  | [ |- ?op (?x * (?y * ?z)) _ <> 0 ]
+    => rewrite F_mul_assoc
+  end.
+Ltac cancel_nonzero_factors tnz := repeat cancel_nonzero_factors' tnz.
+Ltac specialize_quantified_equalities :=
+  repeat match goal with
+         | [ H : forall _ _ _ _, _ = _ -> _, H' : _ = _ |- _ ]
+           => unique pose proof (fun x2 y2 => H _ _ x2 y2 H')
+         | [ H : forall _ _, _ = _ -> _, H' : _ = _ |- _ ]
+           => unique pose proof (H _ _ H')
+         end.
+Ltac finish_inequality tnz :=
+  idtac;
+  match goal with
+  | [ H : ?x <> 0 |- ?y <> 0 ]
+    => replace y with x by (field; tnz); exact H
+  end.
+Ltac field_nonzero tnz :=
+  cancel_nonzero_factors tnz;
+  try (specialize_quantified_equalities;
+       progress cancel_nonzero_factors tnz);
+  try solve [ specialize_quantified_equalities;
+              finish_inequality tnz ].
diff --git a/src/Util/Tactics.v b/src/Util/Tactics.v
new file mode 100644
index 000000000..08ebfe13e
--- /dev/null
+++ b/src/Util/Tactics.v
@@ -0,0 +1,25 @@
+(** * Generic Tactics *)
+
+(* [pose proof defn], but only if no hypothesis of the same type exists.
+   most useful for proofs of a proposition *)
+Tactic Notation "unique" "pose" "proof" constr(defn) :=
+  let T := type of defn in
+  match goal with
+  | [ H : T |- _ ] => fail 1
+  | _ => pose proof defn
+  end.
+(* [assert T], but only if no hypothesis of the same type exists.
+   most useful for proofs of a proposition *)
+Tactic Notation "unique" "assert" constr(T) :=
+  match goal with
+  | [ H : T |- _ ] => fail 1
+  | _ => assert T
+  end.
+
+(* [assert T], but only if no hypothesis of the same type exists.
+   most useful for proofs of a proposition *)
+Tactic Notation "unique" "assert" constr(T) "by" tactic3(tac) :=
+  match goal with
+  | [ H : T |- _ ] => fail 1
+  | _ => assert T by tac
+  end.