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

2 files changed, 13 insertions, 20 deletions

diff --git a/src/Encoding/ModularWordEncodingPre.v b/src/Encoding/ModularWordEncodingPre.v
index 417344b43..aea22f4f5 100644
--- a/src/Encoding/ModularWordEncodingPre.v
+++ b/src/Encoding/ModularWordEncodingPre.v
@@ -16,18 +16,18 @@ Section ModularWordEncodingPre.
   Let Fm_dec (x_ : word sz) : option (F m) :=
     let z := Z.of_N (wordToN (x_)) in
     if Z_lt_dec z m
-      then Some (ZToField z)
+      then Some (ZToField _ z)
       else None
   .
 
   Lemma Fm_encoding_valid : forall x, Fm_dec (Fm_enc x) = Some x.
   Proof.
     unfold Fm_dec, Fm_enc; intros.
-    pose proof (FieldToZ_range x m_pos).
+    pose proof (Zmod.FieldToZ_range x m_pos).
     rewrite wordToN_NToWord_idempotent by (apply bound_check_nat_N;
      assert (Z.to_nat x < Z.to_nat m) by (apply Z2Nat.inj_lt; omega); omega).
     rewrite Z2N.id by omega.
-    rewrite ZToField_idempotent.
+    rewrite Zmod.ZToField_FieldToZ.
     break_if; auto; omega.
   Qed.
 
@@ -36,7 +36,7 @@ Section ModularWordEncodingPre.
     unfold Fm_dec, Fm_enc; intros ? ? dec_Some.
     break_if; [ | congruence ].
     inversion dec_Some.
-    rewrite FieldToZ_ZToField.
+    rewrite Zmod.FieldToZ_ZToField.
     rewrite Z.mod_small by (pose proof (N2Z.is_nonneg (wordToN w)); try omega).
     rewrite N2Z.id.
     apply NToWord_wordToN.
diff --git a/src/Encoding/ModularWordEncodingTheorems.v b/src/Encoding/ModularWordEncodingTheorems.v
index 033e99665..03f98b2ca 100644
--- a/src/Encoding/ModularWordEncodingTheorems.v
+++ b/src/Encoding/ModularWordEncodingTheorems.v
@@ -3,7 +3,7 @@ Require Import Coq.Numbers.Natural.Peano.NPeano.
 Require Import Crypto.CompleteEdwardsCurve.CompleteEdwardsCurveTheorems.
 Require Import Crypto.ModularArithmetic.PrimeFieldTheorems Crypto.ModularArithmetic.ModularArithmeticTheorems.
 Require Import Bedrock.Word.
-Require Import Crypto.Tactics.VerdiTactics.
+Require Import Crypto.Tactics.VerdiTactics Crypto.Util.Tactics.
 Require Import Crypto.Spec.Encoding.
 Require Import Crypto.Util.ZUtil.
 Require Import Crypto.Spec.ModularWordEncoding.
@@ -24,7 +24,7 @@ Section SignBit.
       assert (m < 1)%Z by (apply Z2Nat.inj_lt; try omega; assumption).
       omega.
     + assert (0 < m)%Z as m_pos by (pose proof prime_ge_2 m prime_m; omega).
-      pose proof (FieldToZ_range x m_pos).
+      pose proof (Zmod.FieldToZ_range x m_pos).
       destruct (FieldToZ x); auto.
       - destruct p; auto.
       - pose proof (Pos2Z.neg_is_neg p); omega.
@@ -35,20 +35,13 @@ Section SignBit.
     rewrite sign_bit_parity; auto.
   Qed.
 
-  Lemma sign_bit_opp : forall (x : F m), x <> 0 -> negb (@sign_bit m sz x) = @sign_bit m sz (opp x).
+  Lemma odd_m : Z.odd m = true. Admitted.
+
+  Lemma sign_bit_opp (x : F m) (Hnz:x <> 0) : negb (@sign_bit m sz x) = @sign_bit m sz (opp x).
   Proof.
-    intros.
-    pose proof sign_bit_zero as sign_zero.
-    rewrite !sign_bit_parity in *.
-    pose proof (F_opp_spec x) as opp_spec_x.
-    apply F_eq in opp_spec_x.
-    rewrite FieldToZ_add in opp_spec_x.
-    rewrite <-opp_spec_x, Z.odd_mod in sign_zero by (pose proof prime_ge_2 m prime_m; omega).
-    replace (Z.odd m) with true in sign_zero by (destruct (Z.prime_odd_or_2 m prime_m); auto || omega).
-    rewrite Z.odd_add, F_FieldToZ_add_opp, Z.div_same, Bool.xorb_true_r in sign_zero by assumption || omega.
-    apply Bool.xorb_eq.
-    rewrite <-Bool.negb_xorb_l.
-    assumption.
+    pose proof Zmod.FieldToZ_nonzero_range x Hnz; specialize_by omega.
+    rewrite !sign_bit_parity, Zmod.FieldToZ_opp, Z_mod_nz_opp_full,
+      Zmod_small, Z.odd_sub, odd_m, (Bool.xorb_true_l (Z.odd x)) by
+       (omega || rewrite Zmod_small by omega; auto using Zmod.FieldToZ_nonzero); trivial.
   Qed.
-
 End SignBit.