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, 4 insertions, 4 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.