address code review comments

7 files changed, 71 insertions, 82 deletions

diff --git a/src/Algebra.v b/src/Algebra.v
index adbf5b86b..5601b9d28 100644
--- a/src/Algebra.v
+++ b/src/Algebra.v
@@ -365,12 +365,14 @@ Module ScalarMult.
 
     Global Instance Proper_scalarmult_ref : Proper (Logic.eq==>eq==>eq) scalarmult_ref.
     Proof.
-      repeat intro; subst.
-      match goal with [n:nat |- _ ] => induction n; simpl @scalarmult_ref; [reflexivity|] end.
-      repeat match goal with [H:_ |- _ ] => rewrite H end; reflexivity.
+      repeat intro; subst; 
+        match goal with [n:nat |- _ ] =>
+                        solve [induction n; simpl scalarmult_ref; rewrite_hyp ?*; reflexivity]
+        end.
     Qed.
 
     Lemma scalarmult_ext : forall n P, mul n P = scalarmult_ref n P.
+    Proof.
       induction n; simpl @scalarmult_ref; intros; rewrite <-?IHn; (apply scalarmult_0_l || apply scalarmult_S_l).
     Qed.
 
diff --git a/src/Encoding/ModularWordEncodingTheorems.v b/src/Encoding/ModularWordEncodingTheorems.v
index 03f98b2ca..c42dd8c6f 100644
--- a/src/Encoding/ModularWordEncodingTheorems.v
+++ b/src/Encoding/ModularWordEncodingTheorems.v
@@ -6,6 +6,7 @@ Require Import Bedrock.Word.
 Require Import Crypto.Tactics.VerdiTactics Crypto.Util.Tactics.
 Require Import Crypto.Spec.Encoding.
 Require Import Crypto.Util.ZUtil.
+Require Import Crypto.Util.FixCoqMistakes.
 Require Import Crypto.Spec.ModularWordEncoding.
 
 
@@ -35,13 +36,11 @@ Section SignBit.
     rewrite sign_bit_parity; auto.
   Qed.
 
-  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.
     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.
+    rewrite !sign_bit_parity, Zmod.FieldToZ_opp, Z_mod_nz_opp_full, Zmod_small,
+      Z.odd_sub, (NumTheoryUtil.p_odd m), (Bool.xorb_true_l (Z.odd x));
+      try eapply Zrel_prime_neq_mod_0, rel_prime_le_prime; intuition omega.
   Qed.
 End SignBit.
diff --git a/src/Experiments/SpecEd25519.v b/src/Experiments/SpecEd25519.v
index 6d6de9dcb..aca633fe2 100644
--- a/src/Experiments/SpecEd25519.v
+++ b/src/Experiments/SpecEd25519.v
@@ -12,7 +12,7 @@ Require Import Coq.Logic.Decidable Crypto.Util.Decidable.
 Require Import Coq.omega.Omega.
 
 (* TODO: move to PrimeFieldTheorems *)
-Lemma minus1_is_square {q} :  prime q -> (q mod 4)%Z = 1%Z -> (exists y, y*y  = opp (ZToField q 1))%F.
+Lemma minus1_is_square {q} : prime q -> (q mod 4)%Z = 1%Z -> (exists y, y*y = opp (ZToField q 1))%F.
   intros; pose proof prime_ge_2 q _.
   rewrite Zmod.square_iff.
   destruct (minus1_square_1mod4 q) as [b b_id]; trivial; exists b.
@@ -31,16 +31,6 @@ Lemma square_a : exists b, (b*b=a)%F.
 Proof. pose (@Zmod.Decidable_square q _ two_lt_q a); vm_decide_no_check. Qed.
 Definition d : F q := (opp (ZToField _ 121665) / (ZToField _ 121666))%F.
 
-(* TODO: move to Decidable *)
-Lemma not_not P {d:Decidable P} : not (not P) <-> P.
-Proof. destruct (dec P); intuition. Qed.
-  
-Global Instance dec_ex_forall_not T (P:T->Prop) {d:Decidable (exists b, P b)} : Decidable (forall b, ~ P b).
-Proof.
-  destruct (dec (~ exists b, P b)) as [Hd|Hd]; [left|right];
-    [abstract eauto | abstract (rewrite not_not in Hd by eauto; destruct Hd; eauto) ].
-Defined.
-
 Lemma nonsquare_d : forall x, (x*x <> d)%F.
 Proof. pose (@Zmod.Decidable_square q _ two_lt_q d). vm_decide_no_check. Qed.
 
diff --git a/src/ModularArithmetic/ModularArithmeticTheorems.v b/src/ModularArithmetic/ModularArithmeticTheorems.v
index 5cbc4aa3c..cf0d9eed3 100644
--- a/src/ModularArithmetic/ModularArithmeticTheorems.v
+++ b/src/ModularArithmetic/ModularArithmeticTheorems.v
@@ -9,52 +9,51 @@ Require Export Coq.setoid_ring.Ring_theory Coq.setoid_ring.Ring_tac.
 Require Import Crypto.Algebra Crypto.Util.Decidable.
 Require Export Crypto.Util.FixCoqMistakes.
 
-(* Fails iff the input term does some arithmetic with mod'd values. *)
-Ltac notFancy E :=
-  match E with
-  | - (_ mod _) => idtac
-  | context[_ mod _] => fail 1
-  | _ => idtac
-  end.
-
-(* Remove redundant [mod] operations from the conclusion. *)
-Ltac demod :=
-  repeat match goal with
-         | [ |- context[(?x mod _ + _) mod _] ] =>
-           notFancy x; rewrite (Zplus_mod_idemp_l x)
-         | [ |- context[(_ + ?y mod _) mod _] ] =>
-           notFancy y; rewrite (Zplus_mod_idemp_r y)
-         | [ |- context[(?x mod _ - _) mod _] ] =>
-           notFancy x; rewrite (Zminus_mod_idemp_l x)
-         | [ |- context[(_ - ?y mod _) mod _] ] =>
-           notFancy y; rewrite (Zminus_mod_idemp_r _ y)
-         | [ |- context[(?x mod _ * _) mod _] ] =>
-           notFancy x; rewrite (Zmult_mod_idemp_l x)
-         | [ |- context[(_ * (?y mod _)) mod _] ] =>
-           notFancy y; rewrite (Zmult_mod_idemp_r y)
-         | [ |- context[(?x mod _) mod _] ] =>
-           notFancy x; rewrite (Zmod_mod x)
-         end.
-
-Ltac unwrap_F :=
-  intros;
-  repeat match goal with [ x : F _ |- _ ] => destruct x end;
-  lazy iota beta delta [add sub mul opp FieldToZ ZToField proj1_sig] in *;
-  try apply eqsig_eq;
-  demod.
-
-(* FIXME: remove the pose proof once [monoid] no longer contains decidable equality *)
-Global Instance eq_dec {m} : DecidableRel (@eq (F m)). pose proof dec_eq_Z. exact _. Defined.
-
-Global Instance commutative_ring_modulo m
-  : @Algebra.commutative_ring (F m) Logic.eq 0%F 1%F opp add sub mul.
-Proof.
-  repeat (split || intro); unwrap_F;
-    autorewrite with zsimplify; solve [ exact _ | auto with zarith | congruence].
-Qed.
-
-
 Module Zmod.
+  (* Fails iff the input term does some arithmetic with mod'd values. *)
+  Ltac notFancy E :=
+    match E with
+    | - (_ mod _) => idtac
+    | context[_ mod _] => fail 1
+    | _ => idtac
+    end.
+  
+  (* Remove redundant [mod] operations from the conclusion. *)
+  Ltac demod :=
+    repeat match goal with
+           | [ |- context[(?x mod _ + _) mod _] ] =>
+             notFancy x; rewrite (Zplus_mod_idemp_l x)
+           | [ |- context[(_ + ?y mod _) mod _] ] =>
+             notFancy y; rewrite (Zplus_mod_idemp_r y)
+           | [ |- context[(?x mod _ - _) mod _] ] =>
+             notFancy x; rewrite (Zminus_mod_idemp_l x)
+           | [ |- context[(_ - ?y mod _) mod _] ] =>
+             notFancy y; rewrite (Zminus_mod_idemp_r _ y)
+           | [ |- context[(?x mod _ * _) mod _] ] =>
+             notFancy x; rewrite (Zmult_mod_idemp_l x)
+           | [ |- context[(_ * (?y mod _)) mod _] ] =>
+             notFancy y; rewrite (Zmult_mod_idemp_r y)
+           | [ |- context[(?x mod _) mod _] ] =>
+             notFancy x; rewrite (Zmod_mod x)
+           end.
+  
+  Ltac unwrap_F :=
+    intros;
+    repeat match goal with [ x : F _ |- _ ] => destruct x end;
+    lazy iota beta delta [add sub mul opp FieldToZ ZToField proj1_sig] in *;
+    try apply eqsig_eq;
+    demod.
+  
+  (* FIXME: remove the pose proof once [monoid] no longer contains decidable equality *)
+  Global Instance eq_dec {m} : DecidableRel (@eq (F m)). pose proof dec_eq_Z. exact _. Defined.
+  
+  Global Instance commutative_ring_modulo m
+    : @Algebra.commutative_ring (F m) Logic.eq 0%F 1%F opp add sub mul.
+  Proof.
+    repeat (split || intro); unwrap_F;
+      autorewrite with zsimplify; solve [ exact _ | auto with zarith | congruence].
+  Qed.
+
   Lemma pow_spec {m} a : pow a 0%N = 1%F :> F m /\ forall x, pow a (1 + x)%N = mul a (pow a x).
   Proof. change (@pow m) with (proj1_sig (@pow_with_spec m)); destruct (@pow_with_spec m); eauto. Qed.
 
@@ -165,17 +164,6 @@ Module Zmod.
       - eauto.
       - exists (ZToField _ x'); rewrite !FieldToZ_ZToField; demod; auto.
     Qed.
-
-    (* TODO: move to ZUtil *)
-    Lemma sub_intersperse_modulus : forall x y, ((x - y) mod m = (x + (m - y)) mod m)%Z.
-    Proof.
-      intros.
-      replace (x + (m - y))%Z with (m+(x-y))%Z by omega.
-      rewrite Zplus_mod.
-      rewrite Z_mod_same_full; simpl Z.add.
-      rewrite Zmod_mod.
-      reflexivity.
-    Qed.
   End FandZ.
 
   Section RingTacticGadgets.
diff --git a/src/ModularArithmetic/PrimeFieldTheorems.v b/src/ModularArithmetic/PrimeFieldTheorems.v
index e0c778456..f30472911 100644
--- a/src/ModularArithmetic/PrimeFieldTheorems.v
+++ b/src/ModularArithmetic/PrimeFieldTheorems.v
@@ -78,13 +78,6 @@ Module Zmod.
       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.
-
-    (* 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).
diff --git a/src/Util/Decidable.v b/src/Util/Decidable.v
index e19e23ca4..7b412caf0 100644
--- a/src/Util/Decidable.v
+++ b/src/Util/Decidable.v
@@ -1,6 +1,7 @@
 (** Typeclass for decidable propositions *)
 
 Require Import Coq.Logic.Eqdep_dec.
+Require Import Crypto.Util.FixCoqMistakes.
 Require Import Crypto.Util.Sigma.
 Require Import Crypto.Util.HProp.
 Require Import Crypto.Util.Equality.
@@ -97,6 +98,15 @@ Global Instance dec_eq_nat : DecidableRel (@eq nat) | 10. exact _. Defined.
 Global Instance dec_eq_N : DecidableRel (@eq N) | 10 := N.eq_dec.
 Global Instance dec_eq_Z : DecidableRel (@eq Z) | 10 := Z.eq_dec.
 
+Lemma not_not P {d:Decidable P} : not (not P) <-> P.
+Proof. destruct (dec P); intuition. Qed.
+  
+Global Instance dec_ex_forall_not T (P:T->Prop) {d:Decidable (exists b, P b)} : Decidable (forall b, ~ P b).
+Proof.
+  destruct (dec (~ exists b, P b)) as [Hd|Hd]; [left|right];
+    [abstract eauto | abstract (rewrite not_not in Hd by eauto; destruct Hd; eauto) ].
+Defined.
+
 Lemma eqsig_eq {T} {U} {Udec:DecidableRel (@eq U)} (f g:T->U) (x x':T) pf pf' :
   (exist (fun x => f x = g x) x pf) = (exist (fun x => f x = g x) x' pf') <-> (x = x').
 Proof. apply path_sig_hprop_iff; auto using UIP_dec, Udec. Qed.
diff --git a/src/Util/NumTheoryUtil.v b/src/Util/NumTheoryUtil.v
index 8b8595bb7..f89eb6996 100644
--- a/src/Util/NumTheoryUtil.v
+++ b/src/Util/NumTheoryUtil.v
@@ -298,3 +298,10 @@ Proof.
   + prime_bound.
   + apply minus1_even_pow; [apply divide2_1mod4 | | apply Z_div_pos]; prime_bound.
 Qed.
+
+
+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.
\ No newline at end of file