Moved N lemmas from Ed25519 and IterAssocOp into new NUtil file

4 files changed, 113 insertions, 107 deletions

diff --git a/_CoqProject b/_CoqProject
index ad5fd28b5..f13bf2b2c 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -459,6 +459,7 @@ src/Util/Logic.v
 src/Util/NatUtil.v
 src/Util/Notations.v
 src/Util/NumTheoryUtil.v
+src/Util/NUtil.v
 src/Util/Option.v
 src/Util/PartiallyReifiedProp.v
 src/Util/PointedProp.v
diff --git a/src/Experiments/Ed25519.v b/src/Experiments/Ed25519.v
index 825fe541e..123c72e2c 100644
--- a/src/Experiments/Ed25519.v
+++ b/src/Experiments/Ed25519.v
@@ -8,6 +8,7 @@ Require Import Crypto.Util.Decidable.
 Require Import Crypto.Util.ListUtil.
 Require Import Crypto.Util.Tactics.
 Require Import Crypto.Util.Option.
+Require Import Crypto.Util.NUtil.
 Require Crypto.Specific.GF25519.
 Require Crypto.Specific.GF25519Bounded.
 Require Crypto.Specific.SC25519.
@@ -248,35 +249,6 @@ Proof.
   assumption.
 Qed.
 
-(* MOVE: I think this is all just generic N stuff? *)
-Module N.
-  Lemma size_le a b : (a <= b -> N.size a <= N.size b)%N.
-  Proof.
-    destruct (dec (a=0)%N), (dec (b=0)%N); subst; auto using N.le_0_l.
-    { destruct a; auto. }
-    { rewrite !N.size_log2 by assumption.
-      rewrite <-N.succ_le_mono.
-      apply N.log2_le_mono. }
-  Qed.
-
-  Lemma le_to_nat a b : (a <= b)%N <-> (N.to_nat a <= N.to_nat b)%nat.
-  Proof.
-    rewrite <-N.lt_succ_r.
-    rewrite <-Nat.lt_succ_r.
-    rewrite <-Nnat.N2Nat.inj_succ.
-    rewrite <-NatUtil.Nat2N_inj_lt.
-    rewrite !Nnat.N2Nat.id.
-    reflexivity.
-  Qed.
-
-  Lemma size_nat_le a b : (a <= b)%N -> (N.size_nat a <= N.size_nat b)%nat.
-  Proof.
-    rewrite !IterAssocOp.Nsize_nat_equiv.
-    rewrite <-le_to_nat.
-    apply size_le.
-  Qed.
-End N.
-
 Section SRepERepMul.
   Import Coq.Setoids.Setoid Coq.Classes.Morphisms Coq.Classes.Equivalence.
   Import Coq.NArith.NArith Coq.PArith.BinPosDef.
@@ -323,7 +295,7 @@ Section SRepERepMul.
       apply Z2N.inj_lt in Hu; try (eauto || vm_decide); [];
         apply Z2N.inj_le in Hl; try (eauto || vm_decide); [].
       clear Hl; generalize dependent (Z.to_N z); intro x; intros.
-      rewrite Nsize_nat_equiv.
+      rewrite N.size_nat_equiv.
       destruct (dec (x = 0%N)); subst; try vm_decide; [];
         rewrite N.size_log2 by assumption.
       rewrite N2Nat.inj_succ; assert (N.to_nat (N.log2 x) < ll); try omega.
diff --git a/src/Util/IterAssocOp.v b/src/Util/IterAssocOp.v
index d630698e7..85868f33f 100644
--- a/src/Util/IterAssocOp.v
+++ b/src/Util/IterAssocOp.v
@@ -1,8 +1,8 @@
 Require Import Coq.Setoids.Setoid Coq.Classes.Morphisms Coq.Classes.Equivalence.
 Require Import Coq.NArith.NArith Coq.PArith.BinPosDef.
 Require Import Coq.Numbers.Natural.Peano.NPeano.
-Require Import Crypto.Algebra.
-Import Monoid.
+Require Import Crypto.Algebra. Import Monoid.
+Require Import Crypto.Util.NUtil.
 
 Local Open Scope equiv_scope.
 
@@ -64,56 +64,6 @@ Section IterAssocOp.
   Definition test_and_op_inv a (s : nat * T) :=
     snd s === nat_iter_op (N.to_nat (N.shiftr_nat x (fst s))) a.
 
-  Hint Rewrite
-    N.succ_double_spec
-    N.add_1_r
-    Nat2N.inj_succ
-    Nat2N.inj_mul
-    N2Nat.id: N_nat_conv
- .
-
-  Lemma Nsucc_double_to_nat : forall n,
-    N.succ_double n = N.of_nat (S (2 * N.to_nat n)).
-  Proof.
-    intros.
-    replace 2 with (N.to_nat 2) by auto.
-    autorewrite with N_nat_conv.
-    reflexivity.
-  Qed.
-
-  Lemma Ndouble_to_nat : forall n,
-    N.double n = N.of_nat (2 * N.to_nat n).
-  Proof.
-    intros.
-    replace 2 with (N.to_nat 2) by auto.
-    autorewrite with N_nat_conv.
-    reflexivity.
-  Qed.
-
-  Lemma Nshiftr_succ : forall n i,
-    N.to_nat (N.shiftr_nat n i) =
-    if N.testbit_nat n i
-    then S (2 * N.to_nat (N.shiftr_nat n (S i)))
-    else (2 * N.to_nat (N.shiftr_nat n (S i))).
-  Proof.
-    intros.
-    rewrite Nshiftr_nat_S.
-    case_eq (N.testbit_nat n i); intro testbit_i;
-      pose proof (Nshiftr_nat_spec n i 0) as shiftr_n_odd;
-      rewrite Nbit0_correct in shiftr_n_odd; simpl in shiftr_n_odd;
-      rewrite testbit_i in shiftr_n_odd.
-    + pose proof (Ndiv2_double_plus_one (N.shiftr_nat n i) shiftr_n_odd) as Nsucc_double_shift.
-      rewrite Nsucc_double_to_nat in Nsucc_double_shift.
-      apply Nat2N.inj.
-      rewrite Nsucc_double_shift.
-      apply N2Nat.id.
-    + pose proof (Ndiv2_double (N.shiftr_nat n i) shiftr_n_odd) as Nsucc_double_shift.
-      rewrite Ndouble_to_nat in Nsucc_double_shift.
-      apply Nat2N.inj.
-      rewrite Nsucc_double_shift.
-      apply N2Nat.id.
-  Qed.
-
   Lemma test_and_op_inv_step : forall a s,
     test_and_op_inv a s ->
     test_and_op_inv a (test_and_op a s).
@@ -122,7 +72,7 @@ Section IterAssocOp.
     unfold test_and_op_inv, test_and_op; simpl; intro Hpre.
     destruct i; [ apply Hpre | ].
     simpl.
-    rewrite Nshiftr_succ.
+    rewrite N.shiftr_succ.
     rewrite sel_correct.
     case_eq (testbit i); intro testbit_eq; simpl;
       rewrite testbit_correct in testbit_eq; rewrite testbit_eq;
@@ -157,29 +107,6 @@ Section IterAssocOp.
     reflexivity.
   Qed.
 
-  Lemma Nsize_nat_equiv : forall n, N.size_nat n = N.to_nat (N.size n).
-  Proof.
-    destruct n; auto; simpl; induction p; simpl; auto; rewrite IHp, Pnat.Pos2Nat.inj_succ; reflexivity.
-  Qed.
-
-  Lemma Nshiftr_size : forall n bound, N.size_nat n <= bound ->
-    N.shiftr_nat n bound = 0%N.
-  Proof.
-    intros.
-    rewrite <- (Nat2N.id bound).
-    rewrite Nshiftr_nat_equiv.
-    destruct (N.eq_dec n 0); subst; [apply N.shiftr_0_l|].
-    apply N.shiftr_eq_0.
-    rewrite Nsize_nat_equiv in *.
-    rewrite N.size_log2 in * by auto.
-    apply N.le_succ_l.
-    rewrite <- N.compare_le_iff.
-    rewrite N2Nat.inj_compare.
-    rewrite <- Compare_dec.nat_compare_le.
-    rewrite Nat2N.id.
-    auto.
-  Qed.
-
   Lemma iter_op_correct : forall a bound, N.size_nat x <= bound ->
     iter_op bound a === nat_iter_op (N.to_nat x) a.
   Proof.
@@ -188,7 +115,7 @@ Section IterAssocOp.
     apply test_and_op_inv_holds.
     unfold test_and_op_inv.
     simpl.
-    rewrite Nshiftr_size by auto.
+    rewrite N.shiftr_size by auto.
     reflexivity.
   Qed.
 End IterAssocOp.
diff --git a/src/Util/NUtil.v b/src/Util/NUtil.v
new file mode 100644
index 000000000..309272a90
--- /dev/null
+++ b/src/Util/NUtil.v
@@ -0,0 +1,106 @@
+Require Import Coq.NArith.NArith.
+Require Import Coq.Numbers.Natural.Peano.NPeano.
+Require Import Crypto.Util.NatUtil Crypto.Util.Decidable.
+
+Module N.
+  Lemma size_le a b : (a <= b -> N.size a <= N.size b)%N.
+  Proof.
+    destruct (dec (a=0)%N), (dec (b=0)%N); subst; auto using N.le_0_l.
+    { destruct a; auto. }
+    { rewrite !N.size_log2 by assumption.
+      rewrite <-N.succ_le_mono.
+      apply N.log2_le_mono. }
+  Qed.
+
+  Lemma le_to_nat a b : (a <= b)%N <-> (N.to_nat a <= N.to_nat b)%nat.
+  Proof.
+    rewrite <-N.lt_succ_r.
+    rewrite <-Nat.lt_succ_r.
+    rewrite <-Nnat.N2Nat.inj_succ.
+    rewrite <-NatUtil.Nat2N_inj_lt.
+    rewrite !Nnat.N2Nat.id.
+    reflexivity.
+  Qed.
+
+  Lemma size_nat_equiv : forall n, N.size_nat n = N.to_nat (N.size n).
+  Proof.
+    destruct n; auto; simpl; induction p; simpl; auto; rewrite IHp, Pnat.Pos2Nat.inj_succ; reflexivity.
+  Qed.
+
+  Lemma size_nat_le a b : (a <= b)%N -> (N.size_nat a <= N.size_nat b)%nat.
+  Proof.
+    rewrite !size_nat_equiv.
+    rewrite <-le_to_nat.
+    apply size_le.
+  Qed.
+
+  Lemma shiftr_size : forall n bound, N.size_nat n <= bound ->
+    N.shiftr_nat n bound = 0%N.
+  Proof.
+    intros.
+    rewrite <- (Nat2N.id bound).
+    rewrite Nshiftr_nat_equiv.
+    destruct (N.eq_dec n 0); subst; [apply N.shiftr_0_l|].
+    apply N.shiftr_eq_0.
+    rewrite size_nat_equiv in *.
+    rewrite N.size_log2 in * by auto.
+    apply N.le_succ_l.
+    rewrite <- N.compare_le_iff.
+    rewrite N2Nat.inj_compare.
+    rewrite <- Compare_dec.nat_compare_le.
+    rewrite Nat2N.id.
+    auto.
+  Qed.
+
+  Hint Rewrite
+    N.succ_double_spec
+    N.add_1_r
+    Nat2N.inj_succ
+    Nat2N.inj_mul
+    N2Nat.id: N_nat_conv
+ .
+
+  Lemma succ_double_to_nat : forall n,
+    N.succ_double n = N.of_nat (S (2 * N.to_nat n)).
+  Proof.
+    intros.
+    replace 2 with (N.to_nat 2) by auto.
+    autorewrite with N_nat_conv.
+    reflexivity.
+  Qed.
+
+  Lemma double_to_nat : forall n,
+    N.double n = N.of_nat (2 * N.to_nat n).
+  Proof.
+    intros.
+    replace 2 with (N.to_nat 2) by auto.
+    autorewrite with N_nat_conv.
+    reflexivity.
+  Qed.
+
+  Lemma shiftr_succ : forall n i,
+    N.to_nat (N.shiftr_nat n i) =
+    if N.testbit_nat n i
+    then S (2 * N.to_nat (N.shiftr_nat n (S i)))
+    else (2 * N.to_nat (N.shiftr_nat n (S i))).
+  Proof.
+    intros.
+    rewrite Nshiftr_nat_S.
+    case_eq (N.testbit_nat n i); intro testbit_i;
+      pose proof (Nshiftr_nat_spec n i 0) as shiftr_n_odd;
+      rewrite Nbit0_correct in shiftr_n_odd; simpl in shiftr_n_odd;
+      rewrite testbit_i in shiftr_n_odd.
+    + pose proof (Ndiv2_double_plus_one (N.shiftr_nat n i) shiftr_n_odd) as Nsucc_double_shift.
+      rewrite succ_double_to_nat in Nsucc_double_shift.
+      apply Nat2N.inj.
+      rewrite Nsucc_double_shift.
+      apply N2Nat.id.
+    + pose proof (Ndiv2_double (N.shiftr_nat n i) shiftr_n_odd) as Nsucc_double_shift.
+      rewrite double_to_nat in Nsucc_double_shift.
+      apply Nat2N.inj.
+      rewrite Nsucc_double_shift.
+      apply N2Nat.id.
+  Qed.
+
+
+End N.