Refactor ModularArithmetic into Zmod, expand Decidable

ModularArithmetic now uses Algebra lemmas in various places instead of
custom manual proofs. Similarly, Util.Decidable is used to state and
prove the relevant decidability results.

Backwards-incompatible changes:

F_some_lemma -> Zmod.some_lemma
Arguments ZToField _%Z _%Z : clear implicits.
inv_spec says inv x * x = 1, not x * inv x = 1

1 files changed, 154 insertions, 551 deletions

diff --git a/src/ModularArithmetic/PrimeFieldTheorems.v b/src/ModularArithmetic/PrimeFieldTheorems.v
index 8d47e36ed..c97bde495 100644
--- a/src/ModularArithmetic/PrimeFieldTheorems.v
+++ b/src/ModularArithmetic/PrimeFieldTheorems.v
@@ -10,568 +10,171 @@ Require Import Coq.ZArith.BinInt Coq.NArith.BinNat Coq.ZArith.ZArith Coq.ZArith.
 Require Import Coq.Logic.Eqdep_dec.
 Require Import Crypto.Util.NumTheoryUtil Crypto.Util.ZUtil.
 Require Import Crypto.Util.Tactics.
+Require Import Crypto.Util.Decidable.
 Require Export Crypto.Util.FixCoqMistakes.
 Require Crypto.Algebra.
+Import Crypto.ModularArithmetic.ModularArithmeticTheorems.Zmod.
 
 Existing Class prime.
 
-Lemma F_inv_spec : forall {m}, inv 0%F = (0%F : F m)
-      /\ (prime m -> forall a0 : F m, a0 <> 0%F -> (a0 * inv a0)%F = 1%F).
-Proof.
-  intros m.
-  pose (@inv_with_spec m) as H.
-  change (@inv m) with (proj1_sig H).
-  destruct H; eauto.
-Qed.
-
-Section FieldModuloPre.
-  Context {q:Z} {prime_q:prime q}.
-  Local Open Scope F_scope.
-
-  Lemma Fq_1_neq_0 : (1:F q) <> (0:F q).
-  Proof.
-    pose proof prime_ge_2 q _.
-    rewrite F_eq, !FieldToZ_ZToField, !Zmod_small by omega; congruence.
-  Qed.
-
-  Lemma F_mul_inv_r : forall x : F q, x <> 0 -> x * inv x = 1.
-  Proof.
-    intros.
-    edestruct @F_inv_spec; eauto.
-  Qed.
-
-  Lemma F_mul_inv_l : forall x : F q, x <> 0 -> inv x * x = 1.
-  Proof.
-    intros.
-    edestruct @F_inv_spec as [Ha Hb]; eauto.
-    erewrite <-Hb; eauto.
-    Fdefn.
-  Qed.
-
-  (* Add an abstract field (without modifiers) *)
-  Definition Ffield_theory : field_theory 0%F 1%F (@add q) (@mul q) (@sub q) (@opp q) (@div q) (@inv q) eq.
-  Proof.
-    constructor; auto using Fring_theory, Fq_1_neq_0, F_mul_inv_l.
-  Qed.
-
-  Global Instance field_modulo : @Algebra.field (F q) Logic.eq (ZToField 0) (ZToField 1) opp add sub mul inv div.
-  Proof.
-    constructor; try solve_proper.
-    - apply commutative_ring_modulo.
-    - split. auto using F_mul_inv_l.
-    - split. auto using Fq_1_neq_0.
-  Qed.
-End FieldModuloPre.
-
-Module Type PrimeModulus.
-  Parameter modulus : Z.
-  Parameter prime_modulus : prime modulus.
-End PrimeModulus.
-
-Module FieldModulo (Import M : PrimeModulus).
-  (* Add our field with all the fixin's *)
-  Module Import RingM := RingModulo M.
-  Definition field_theory_modulo := @Ffield_theory modulus prime_modulus.
-  Add Field Ffield_Z : field_theory_modulo
-    (morphism ring_morph_modulo,
-     preprocess [Fpreprocess],
-     postprocess [Fpostprocess],
-     constants [Fconstant],
-     div morph_div_theory_modulo,
-     power_tac power_theory_modulo [Fexp_tac]).
-End FieldModulo.
-
-Section VariousModPrime.
-  Context {q:Z} {prime_q:prime q}.
-  Local Open Scope F_scope.
-  Add Field Ffield_Z : (@Ffield_theory q _)
-    (morphism (@Fring_morph q),
-     preprocess [Fpreprocess],
-     postprocess [Fpostprocess; try exact Fq_1_neq_0; try assumption],
-     constants [Fconstant],
-     div (@Fmorph_div_theory q),
-     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.
-    assert (x * z * inv z = y * z * inv z) as H by (rewrite mul_z_eq; reflexivity).
-    replace (x * z * inv z) with (x * (z * inv z)) in H by (field; trivial).
-    replace (y * z * inv z) with (y * (z * inv z)) in H by (field; trivial).
-    rewrite F_mul_inv_r in H by assumption.
-    replace (x * 1) with x in H by field.
-    replace (y * 1) with y in H by field.
-    trivial.
-  Qed.
-
-  Lemma Fq_mul_eq_l : forall x y z : F q, z <> 0 -> z * x = z * y -> x = y.
-  Proof.
-    intros ? ? ? Hz Heq.
-    apply (Fq_mul_eq _ _ z); auto.
-    apply (Fq_sub_eq _ _ _ _ Heq); ring.
-  Qed.
-
-  Lemma Fq_inv_unique' : forall
-      inv1 (inv1ok: inv1 0 = 0 /\ forall x : F q, x <> 0 ->  x * inv1 x = 1)
-      inv2 (inv2ok: inv2 0 = 0 /\ forall x : F q, x <> 0 ->  x * inv2 x = 1),
-      forall x, inv1 x = inv2 x.
-  Proof.
-    intros inv1 [inv1_0 inv1_x] inv2 [inv2_0 inv2_x] x.
-    destruct (F_eq_dec x 0) as [H|H]; [congruence|].
-    apply (Fq_mul_eq_l _ _ x H). rewrite inv1_x, inv2_x; trivial.
-  Qed.
-
-  Lemma Fq_inv_unique : forall
-      inv' (inv'ok: inv' 0 = 0 /\ forall x : F q, x <> 0 -> x * inv' x = 1),
-      forall x, inv x = inv' x.
-  Proof.
-    intros ? [? ?] ?.
-    pose proof (@F_inv_spec q) as [? ?].
-    eauto using Fq_inv_unique'.
-  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 _)).
-    - intuition.
-    - intro H. apply F_mul_0_l.
-  Qed.
-
-  Lemma Fq_root_zero : forall (x: F q) (p: N), x^p = 0 -> x = 0.
-    induction p using N.peano_ind;
-    rewrite <-?N.add_1_l, ?(proj2 (@F_pow_spec q _) _), ?(proj1 (@F_pow_spec q _)).
-    - intros; destruct Fq_1_neq_0; auto.
-    - intro H; destruct (Fq_mul_zero_why x (x^p) H); auto.
-  Qed.
-
-  Lemma Fq_root_nonzero : forall (x:F q) p, x^p <> 0 -> (p <> 0)%N -> x <> 0.
-    induction p using N.peano_ind;
-    rewrite <-?N.add_1_l, ?(proj2 (@F_pow_spec q _) _), ?(proj1 (@F_pow_spec q _)).
-    - intuition.
-    - destruct (N.eq_dec p 0); intro H; intros; subst.
-      + rewrite (proj1 (@F_pow_spec q _)) in H; replace (x*1) with (x) in H by ring; trivial.
-      + apply IHp; auto. intro Hz; rewrite Hz in *. apply H, F_mul_0_r.
-  Qed.
-
-  Lemma Fq_pow_nonzero : forall (x : F q) p, x <> 0 -> x^p <> 0.
-  Proof.
-    induction p using N.peano_ind;
-    rewrite <-?N.add_1_l, ?(proj2 (@F_pow_spec q _) _), ?(proj1 (@F_pow_spec q _)).
-    - intuition. auto using Fq_1_neq_0.
-    - intros H Hc. destruct (Fq_mul_zero_why _ _ Hc).
-      + intuition.
-      + apply IHp; auto.
-  Qed.
-
-  Lemma F_inv_0 : inv 0 = (0 : F q).
-  Proof.
-    destruct (@F_inv_spec q); auto.
-  Qed.
-
-  Definition inv_fermat (x:F q) : F q := x ^ Z.to_N (q - 2)%Z.
-  Lemma Fq_inv_fermat: 2 < q -> forall x : F q, inv x = x ^ Z.to_N (q - 2)%Z.
-  Proof.
-    intros.
-    erewrite (Fq_inv_unique inv_fermat); trivial; split; intros; unfold inv_fermat.
-    { replace 2%N with (Z.to_N (Z.of_N 2))%N by auto.
-      rewrite Fq_pow_zero. reflexivity. intro.
-      assert (Z.of_N (Z.to_N (q-2)) = 0%Z) by (rewrite H0; eauto); rewrite Z2N.id in *; omega. }
-    { clear x. rename x0 into x. pose proof (fermat_inv _ _ x) as Hf; forward Hf.
-      { pose proof @ZToField_FieldToZ; pose proof @ZToField_mod; congruence. }
-      specialize (Hf H1); clear H1.
-      rewrite <-(ZToField_FieldToZ x).
-      rewrite ZToField_pow.
-      replace (Z.of_N (Z.to_N (q - 2))) with (q-2)%Z by (rewrite Z2N.id ; omega).
-      rewrite <-ZToField_mul.
-      apply ZToField_eqmod.
-      rewrite Hf, Zmod_small by omega; reflexivity.
-    }
-  Qed.
-  Lemma Fq_inv_fermat_correct : 2 < q -> forall x : F q, inv_fermat x = inv x.
-  Proof.
-    unfold inv_fermat; intros. rewrite Fq_inv_fermat; auto.
-  Qed.
-
-  Let inv_fermat_powmod (x:Z) : Z := powmod q x (Z.to_N (q-2)).
-  Lemma FieldToZ_inv_efficient : 2 < q ->
-                                 forall x : F q, FieldToZ (inv x) = inv_fermat_powmod x.
-  Proof.
-    unfold inv_fermat_powmod; intros.
-    rewrite Fq_inv_fermat, powmod_Zpow_mod, <-FieldToZ_pow_Zpow_mod; auto.
-  Qed.
+Module Zmod.
+  Section Field.
+    Context (q:Z) {prime_q:prime q}.
+    Lemma inv_spec : inv 0%F = (0%F : F q) 
+                     /\ (prime q -> forall x : F q, x <> 0%F -> (inv x * x)%F = 1%F).
+    Proof. change (@inv q) with (proj1_sig (@inv_with_spec q)); destruct (@inv_with_spec q); eauto. Qed.
+
+    Lemma inv_0 : inv 0 = ZToField q 0. Proof. destruct inv_spec; auto. Qed.
+    Lemma inv_nonzero (x:F q) : (x <> 0 -> inv x * x%F = 1)%F. Proof. destruct inv_spec; auto. Qed.
+
+    Global Instance field_modulo : @Algebra.field (F q) Logic.eq 0%F 1%F opp add sub mul inv div.
+    Proof.
+      repeat match goal with
+             | _ => solve [ solve_proper
+                          | apply commutative_ring_modulo
+                          | apply inv_nonzero
+                          | cbv [not]; pose proof prime_ge_2 q prime_q;
+                            rewrite Zmod.eq_FieldToZ_iff, !Zmod.FieldToZ_ZToField, !Zmod_small; omega ]
+             | _ => split
+             end.
+    Qed.
 
-  Lemma F_minus_swap : forall x y : F q, x - y = 0 -> y - x = 0.
-  Proof.
-    intros ? ? eq_zero.
-    replace x with (x - y + y); try ring.
-    rewrite eq_zero.
-    ring.
-  Qed.
+    Definition field_theory : field_theory 0%F 1%F add mul sub opp div inv eq
+      := Algebra.Field.field_theory_for_stdlib_tactic.
+  End Field.
+
+  (** A field tactic hook that can be imported *)
+  Module Type PrimeModulus.
+    Parameter modulus : Z.
+    Parameter prime_modulus : prime modulus.
+  End PrimeModulus.
+  Module FieldModulo (Export M : PrimeModulus).
+    Module Import RingM := RingModulo M.
+    Add Field _field : (field_theory modulus)
+                         (morphism (ring_morph modulus),
+                          constants [is_constant],
+                          div (morph_div_theory modulus),
+                          power_tac (power_theory modulus) [is_pow_constant]).
+  End FieldModulo.
+
+  Section NumberThoery.
+    Context {q:Z} {prime_q:prime q} {two_lt_q: 2 < q}.
+    Local Open Scope F_scope.
+    Add Field _field : (field_theory q)
+                         (morphism (ring_morph q),
+                          constants [is_constant],
+                          div (morph_div_theory q),
+                          power_tac (power_theory q) [is_pow_constant]).
+
+    Lemma FieldToZ_1 : @FieldToZ q 1 = 1%Z.
+    Proof. simpl. rewrite Zmod_small; omega. Qed.
+
+    Lemma Fq_inv_fermat (x:F q) : inv x = x ^ Z.to_N (q - 2)%Z.
+    Proof.
+      destruct (dec (x = 0%F)) as [?|Hnz]; [subst x; rewrite inv_0|].
+      { admit. }
+      erewrite <-Algebra.Field.inv_unique; try reflexivity.
+      rewrite eq_FieldToZ_iff, FieldToZ_mul, FieldToZ_pow, Z2N.id, FieldToZ_1 by omega.
+      apply (fermat_inv q _ (FieldToZ x)); rewrite mod_FieldToZ; eapply FieldToZ_nonzero; trivial.
+    Qed.
 
-  Lemma Fq_square_mul : forall x y z : F q, (y <> 0) ->
-    x ^ 2 = z * y ^ 2 -> exists sqrt_z, sqrt_z ^ 2 = z.
-  Proof.
-    intros ? ? ? y_nonzero A.
-    exists (x / y).
-    assert ((x / y) ^ 2 = x ^ 2 / y ^ 2) as square_distr_div by (field; trivial).
-    assert (y ^ 2 <> 0) as y2_nonzero by (
-      change (2%N) with (1+(1+0))%N;
-      rewrite !(proj2 (@F_pow_spec q _) _), !(proj1 (@F_pow_spec q _));
-      auto 10 using Fq_mul_nonzero_nonzero, Fq_1_neq_0).
-    rewrite (Fq_mul_eq _ z (y ^ 2)); auto.
-    rewrite <- A.
-    field; trivial.
-  Qed.
+    (* TODO: move to number thoery util *)
+    Lemma odd_as_div a : Z.odd a = true -> a = (2*(a/2) + 1)%Z.
+    Proof.
+      rewrite Zodd_mod, <-Zeq_is_eq_bool; intro H_1; rewrite <-H_1.
+      apply Z_div_mod_eq; reflexivity.
+    Qed.
+    
+    Lemma euler_criterion (a : F q) (a_nonzero : a <> 0) :
+      (a ^ (Z.to_N (q / 2)) = 1) <-> (exists b, b*b = a).
+    Proof.
+      pose proof FieldToZ_nonzero_range a; pose proof (odd_as_div q).
+      specialize_by ltac:(destruct (Z.prime_odd_or_2 _ prime_q); try omega; trivial).
+      rewrite eq_FieldToZ_iff, !FieldToZ_pow, !FieldToZ_1, !Z2N.id by omega.
+      rewrite square_iff, <-(euler_criterion (q/2)) by (trivial || omega); reflexivity.
+    Qed.
 
-  Lemma Fq_square_mul_sub : forall x y z : F q,
-    0 = z * y ^ 2 - x ^ 2 -> (exists sqrt_z, sqrt_z ^ 2 = z) \/ x = 0.
-  Proof.
-    intros ? ? ? eq_zero_sub.
-    destruct (F_eq_dec y 0). {
+    Global Instance Decidable_square (x:F q) : Decidable (exists y, y*y = x).
+    Proof.
+      destruct (dec (x = 0)).
+      { left. abstract (exists 0; subst; ring). }
+      { eapply Decidable_iff_to_impl; [eapply euler_criterion; assumption | exact _]. }
+    Defined.
+  End NumberThoery.
+
+  Section SquareRootsPrime5Mod8.
+    Context {q:Z} {prime_q: prime q} {q_5mod8 : q mod 8 = 5}.
+
+    (* This is always true, but easier to check by computation than to prove *)
+    Context (sqrt_minus1_valid : ((ZToField q 2 ^ Z.to_N (q / 4)) ^ 2 = opp 1)%F).
+    Local Open Scope F_scope.
+    Add Field _field2 : (field_theory q)
+                          (morphism (ring_morph q),
+                           constants [is_constant],
+                           div (morph_div_theory q),
+                           power_tac (power_theory q) [is_pow_constant]).
+
+    Let sqrt_minus1 : F q :=  ZToField _ 2 ^ Z.to_N (q / 4).
+
+    Lemma two_lt_q_5mod8 : 2 < q.
+    Proof.
+      pose proof (prime_ge_2 q _) as two_le_q.
+      apply Zle_lt_or_eq in two_le_q.
+      destruct two_le_q; auto.
       subst_max.
-      rewrite Fq_pow_zero in eq_zero_sub by congruence.
-      rewrite F_mul_0_r in eq_zero_sub.
-      assert (x ^ 2 = 0 - x ^ 2 + x ^ 2) as minus_plus_x2 by (rewrite <- eq_zero_sub; ring).
-      assert (x ^ 2 = 0) as x2_zero by (rewrite minus_plus_x2; ring).
-      apply Fq_root_zero in x2_zero.
-      right; auto.
-    } {
-      left.
-      eapply Fq_square_mul; eauto.
-      instantiate (1 := x).
-      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.
-    }
-  Qed.
-
-  Lemma F_div_mul : forall x y z : F q, y <> 0 -> (z = (x / y) <-> z * y = x).
-  Proof.
-    split; intros; subst; field.
-  Qed.
-
-  Lemma F_div_1_r : forall x : F q, (x/1)%F = x.
-  Proof.
-    intros; field. (* TODO: Warning: Collision between bound variables ... *)
-  Qed.
-
-  Lemma F_div_opp_1 : forall x y : F q, (opp x / y = opp (x / y))%F.
-  Proof.
-    intros; destruct (F_eq_dec y 0); [subst;unfold div;rewrite !F_inv_0|]; field.
-  Qed.
-
-  Lemma F_eq_opp_zero : forall x : F q, 2 < q -> (x = opp x <-> x = 0).
-  Proof.
-    split; intro A.
-    + pose proof (F_opp_spec x) as opp_spec.
-      rewrite <- A in opp_spec.
-      replace (x + x) with (ZToField 2 * x) in opp_spec by ring.
-      apply Fq_mul_zero_why in opp_spec.
-      destruct opp_spec as [eq_2_0 | ?]; auto.
-      apply F_eq in eq_2_0.
-      rewrite FieldToZ_ZToField in eq_2_0.
-      replace (FieldToZ 0) with 0%Z in eq_2_0 by auto.
-      replace (2 mod q) with 2 in eq_2_0; try discriminate.
-      symmetry; apply Z.mod_small; omega.
-    + subst.
-      rewrite <- (F_opp_spec 0) at 1.
-      ring.
-  Qed.
-
-  Lemma euler_criterion_F : forall (a : F q) (q_odd : 2 < q) (a_nonzero : a <> 0),
-    (a ^ (Z.to_N (q / 2)) = 1) <-> isSquare a.
-  Proof.
-    (*pose proof q_odd.*)
-    split; intros A. {
-      apply square_Zmod_F; auto.
-      eapply euler_criterion; omega || auto.
-      + apply div2_p_1mod4; auto; omega.
-      + pose proof (FieldToZ_nonzero_range a a_nonzero); omega.
-      + replace (q / 2)%Z with (Z.of_N (Z.to_N (q / 2)))
-          by (apply Z2N.id; apply Z.div_pos; prime_bound).
-        rewrite FieldToZ_pow_Zpow_mod by omega.
-        rewrite A.
-        replace (FieldToZ 1) with (1 mod q) by auto.
-        apply Z.mod_1_l; omega.
-    } {
-      apply F_eq.
-      rewrite <- FieldToZ_pow_Zpow_mod by omega.
-      rewrite Z2N.id by (apply Z.div_pos; omega).
-      replace (FieldToZ 1) with 1%Z
-        by (rewrite FieldToZ_ZToField at 1; symmetry; apply Zmod_1_l; omega).
-      apply euler_criterion; try prime_bound; auto.
-      + apply div2_p_1mod4; auto; omega.
-      + pose proof (FieldToZ_nonzero_range a a_nonzero); omega.
-      + apply square_Zmod_F; auto.
-    }
-  Qed.
-
-  Lemma euler_criterion_if' : forall (a : F q) (q_odd : 2 < q),
-    if (orb (F_eqb a 0) (F_eqb (a ^ (Z.to_N (q / 2))) 1))
-    then (isSquare a) else (forall b, b ^ 2 <> a).
-  Proof.
-    unfold orb; intros.
-    rewrite <- if_F_eq_dec_if_F_eqb.
-    do 2 break_if; try congruence.
-    + subst; exists 0; apply Fq_pow_zero; congruence.
-    + unfold isSquare; apply F_eqb_eq in Heqb; apply euler_criterion_F; eauto.
-    + intros b b_id.
-      apply F_eqb_neq in Heqb.
-      assert (isSquare a) as a_square by (eexists; eauto).
-      apply euler_criterion_F in a_square; auto.
-  Qed.
-
-  Lemma euler_criterion_if : forall (a : F q) (q_odd : 2 < q),
-    if (a =? 0) || (powmod q a (Z.to_N (q / 2)) =? 1)
-    then (isSquare a) else (forall b, b ^ 2 <> a).
-  Proof.
-    intros.
-    pose proof (euler_criterion_if' a q_odd) as H.
-    unfold F_eqb in H.
-    rewrite !FieldToZ_ZToField, !@FieldToZ_pow_efficient, !Zmod_small in H by omega; assumption.
-  Qed.
-
-  Lemma sqrt_solutions : forall x y : F q, y ^ 2 = x ^ 2 -> y = x \/ y = opp x.
-  Proof.
-    intros ? ? squares_eq.
-    remember (y - x) as z.
-    replace y with (x + z) in * by (rewrite Heqz; ring).
-    replace (x ^ 2) with (0 + x ^ 2) in squares_eq by ring.
-    replace ((x + z) ^ 2) with (z * (x + (x + z)) + x ^ 2) in squares_eq by ring.
-    apply F_add_reg_r in squares_eq.
-    apply Fq_mul_zero_why in squares_eq.
-    destruct squares_eq as [? | z_2x_0]; [ left; subst; ring | right ].
-    pose proof (F_opp_spec x) as opp_spec.
-    rewrite <- z_2x_0 in opp_spec.
-    apply F_add_reg_l in opp_spec; auto.
-  Qed.
-
-  Global Instance Fq_Ring_ops : @Ring_ops (F q) 0 1 add mul sub opp eq.
-  Global Instance Fq_Ring: @Ring (F q) 0 1 add mul sub opp eq Fq_Ring_ops.
-  Proof.
-    econstructor; eauto with typeclass_instances;
-      unfold R2, equality, eq_notation, addition, add_notation, one, one_notation,
-      multiplication, mul_notation, zero, zero_notation, subtraction,
-      sub_notation, opposite, opp_notation; intros; ring.
+      discriminate.
     Qed.
 
-  Global Instance Fq_Cring: @Cring (F q) 0 1 add mul sub opp eq Fq_Ring_ops Fq_Ring.
-  Proof.
-    repeat intro. apply F_mul_comm.
-  Qed.
-
-  Global Instance Fq_Integral_domain : @Integral_domain (F q) 0 1 add mul sub opp eq Fq_Ring_ops Fq_Ring Fq_Cring.
-  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.
-  Context {q:Z} {prime_q: prime q} {q_5mod8 : q mod 8 = 5}.
-
-  (* This is always true, but easier to check by computation than to prove *)
-  Context (sqrt_minus1_valid : ((ZToField 2 ^ Z.to_N (q / 4)) ^ 2 = @opp q 1)%F).
-
-  Local Open Scope F_scope.
-  Add Field Ffield_8mod5 : (@Ffield_theory q _)
-    (morphism (@Fring_morph q),
-     preprocess [Fpreprocess],
-     postprocess [Fpostprocess; try exact Fq_1_neq_0; try assumption],
-     constants [Fconstant],
-     div (@Fmorph_div_theory q),
-     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).
-
-  Lemma two_lt_q_5mod8 : 2 < q.
-  Proof.
-    pose proof (prime_ge_2 q _) as two_le_q.
-    apply Zle_lt_or_eq in two_le_q.
-    destruct two_le_q; auto.
-    subst_max.
-    discriminate.
-  Qed.
-
-  (* square root mod q relies on the fact that q is 5 mod 8 *)
-  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
-    | right A => (sqrt_minus1 * b)%F
-    end).
-
-  Lemma eq_b4_a2 : forall x : F q, isSquare x ->
-    ((x ^ Z.to_N (q / 8 + 1)) ^ 2) ^ 2 = x ^ 2.
-  Proof.
-    intros.
-    destruct (F_eq_dec x 0). {
-      subst.
-      repeat rewrite Fq_pow_zero; try (intuition; discriminate).
-      intro false_eq.
-      assert (0 <= q / 8)%Z by zero_bounds.
-      assert (0 < q / 8 + 1) by omega.
-      replace 0%N with (Z.to_N 0) in * by auto.
-      apply Z2N.inj in false_eq; omega.
-    } {
-      rewrite F_pow_compose.
-      replace (2 * 2)%N with 4%N by auto.
-      rewrite F_pow_compose.
-      replace (4 * Z.to_N (q / 8 + 1))%N with (Z.to_N (q / 2 + 2))%N.
+    Definition sqrt_5mod8 (a : F q) : F q :=
+      let b := a ^ Z.to_N (q / 8 + 1) in
+      if dec (b ^ 2 = a)
+      then b
+      else sqrt_minus1 * b.
+    
+    Lemma eq_b4_a2 (x : F q) (Hex:exists y, y*y = x) :
+      ((x ^ Z.to_N (q / 8 + 1)) ^ 2) ^ 2 = x ^ 2.
+    Proof.
+      pose proof two_lt_q_5mod8.
+      assert (0 <= q/8)%Z by (apply Z.div_le_lower_bound; rewrite ?Z.mul_0_r; omega).
+      assert (Z.to_N (q / 8 + 1) <> 0%N) by
+          (intro Hbad; change (0%N) with (Z.to_N 0%Z) in Hbad; rewrite Z2N.inj_iff in Hbad; omega).
+      destruct (dec (x = 0)); [subst; rewrite !pow_0_l by (trivial || lazy_decide); reflexivity|].
+      rewrite !pow_pow_l.
+
+      replace (Z.to_N (q / 8 + 1) * (2*2))%N with (Z.to_N (q / 2 + 2))%N.
+      Focus 2. { (* this is a boring but gnarly proof :/ *)
+        change (2*2)%N with (Z.to_N 4).
+        rewrite <- Z2N.inj_mul by zero_bounds.
+        apply Z2N.inj_iff; try zero_bounds.
+        rewrite <- Z.mul_cancel_l with (p := 2) by omega.
+        ring_simplify.
+        rewrite Z.mul_div_eq by omega.
+        rewrite Z.mul_div_eq by omega.
+        rewrite (Zmod_div_mod 2 8 q) by
+            (try omega; apply Zmod_divide; omega || auto).
+        rewrite q_5mod8.
+        replace (5 mod 2)%Z with 1%Z by auto.
+        ring.
+      } Unfocus.
+
+      rewrite Z2N.inj_add, pow_add_r by zero_bounds.
+      replace (x ^ Z.to_N (q / 2)) with (@ZToField q 1) by
+          (symmetry; apply @euler_criterion; eauto).
+      change (Z.to_N 2) with 2%N; ring.
+    Qed.
 
-      Focus 2.
-      replace 4%N with (Z.to_N 4) by auto.
-      rewrite <- Z2N.inj_mul by zero_bounds.
-      apply Z2N.inj_iff; try zero_bounds.
-      rewrite <- Z.mul_cancel_l with (p := 2) by omega.
+    Lemma sqrt_5mod8_valid : forall x, (exists y, y*y = x) ->
+                                       (sqrt_5mod8 x)*(sqrt_5mod8 x) = x.
+    Proof.
+      intros x x_square.
+      pose proof (eq_b4_a2 x x_square) as Hyy; rewrite !pow_2_r in Hyy.
+      destruct (Algebra.only_two_square_roots_choice _ x (x*x) Hyy eq_refl) as [Hb|Hb]; clear Hyy;
+        unfold sqrt_5mod8; break_if; rewrite !@pow_2_r in *; intuition.
       ring_simplify.
-      rewrite Z.mul_div_eq by omega.
-      rewrite Z.mul_div_eq by omega.
-      rewrite (Zmod_div_mod 2 8 q) by
-        (try omega; apply Zmod_divide; omega || auto).
-      rewrite q_5mod8.
-      replace (5 mod 2)%Z with 1%Z by auto.
-      ring.
-      (* End Focus *)
-
-      rewrite Z2N.inj_add by zero_bounds.
-      rewrite <- F_pow_add by zero_bounds.
-      replace (x ^ Z.to_N (q / 2)) with (@ZToField q 1).
-      replace (Z.to_N 2) with 2%N by auto.
-      ring.
-
-      symmetry; apply euler_criterion_F; auto using two_lt_q_5mod8.
-    }
-  Qed.
-
-  Lemma sqrt_mod_q_valid : forall x, isSquare x ->
-    (sqrt_mod_q x) ^ 2 = x.
-  Proof.
-    intros x x_square.
-    destruct (sqrt_solutions x _ (eq_b4_a2 x x_square)) as [? | eq_b2_oppx];
-      unfold sqrt_mod_q; break_if; intuition.
-    ring_simplify.
-    unfold sqrt_minus1.
-    rewrite sqrt_minus1_valid.
-    rewrite eq_b2_oppx.
-    field.
-  Qed.
-
-  Lemma sqrt_mod_q_of_0 : sqrt_mod_q 0 = 0.
-  Proof.
-    unfold sqrt_mod_q.
-    rewrite !Fq_pow_zero.
-    break_if; ring.
-
-    congruence.
-    intro false_eq.
-    rewrite <-(N2Z.id 0) in false_eq.
-    rewrite N2Z.inj_0 in false_eq.
-    pose proof (prime_ge_2 q prime_q).
-    apply Z2N.inj in false_eq; zero_bounds.
-    assert (0 < q / 8 + 1)%Z.
-    apply Z.add_nonneg_pos; zero_bounds.
-    omega.
-  Qed.
-
-  Lemma sqrt_mod_q_root_0 : forall x : F q, sqrt_mod_q x = 0 -> x = 0.
-  Proof.
-    unfold sqrt_mod_q; intros.
-    break_if.
-    - match goal with [ H : ?sqrt_x ^ 2 = x, H' : ?sqrt_x = 0 |- _ ] => rewrite <-H, H' end.
+      unfold sqrt_minus1; rewrite @pow_2_r.
+      rewrite sqrt_minus1_valid; rewrite @pow_2_r.
+      rewrite Hb.
       ring.
-    - match goal with
-      | [H : sqrt_minus1 * _ = 0 |- _ ]=>
-         apply Fq_mul_zero_why in H; destruct H as [sqrt_minus1_zero | ? ];
-         [ | eapply Fq_root_zero; eauto ]
-      end.
-      unfold sqrt_minus1 in sqrt_minus1_zero.
-      rewrite sqrt_minus1_zero in sqrt_minus1_valid.
-      exfalso.
-      pose proof (@F_opp_spec q 1) as opp_spec_1.
-      rewrite <-sqrt_minus1_valid in opp_spec_1.
-      assert (((1 + 0 ^ 2) : F q) = (1 : F q)) as ring_subst by ring.
-      rewrite ring_subst in *.
-      apply Fq_1_neq_0; assumption.
-  Qed.
-
-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 ].
+    Qed.
+  End SquareRootsPrime5Mod8.
+End Zmod.
\ No newline at end of file