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

3 files changed, 55 insertions, 86 deletions

diff --git a/src/Util/AdditionChainExponentiation.v b/src/Util/AdditionChainExponentiation.v
index ca1394115..6a028dda8 100644
--- a/src/Util/AdditionChainExponentiation.v
+++ b/src/Util/AdditionChainExponentiation.v
@@ -5,98 +5,53 @@ Require Import VerdiTactics.
 Require Import Crypto.Util.Option.
 
 Section AddChainExp.
-  Function add_chain (is:list (nat*nat)) : list nat :=
+  Function fold_chain {T} (id:T) (op:T->T->T) (is:list (nat*nat)) (acc:list T) {struct is} : T :=
     match is with
-    | nil => nil
+    | nil =>
+      match acc with
+      | nil => id
+      | ret::_ => ret
+      end
     | (i,j)::is' =>
-      let chain' := add_chain is' in
-      nth_default 1 chain' i + nth_default 1 chain' j::chain'
+      let ijx := op (nth_default id acc i) (nth_default id acc j) in
+      fold_chain id op is' (ijx::acc)
     end.
 
-Example wikipedia_addition_chain : add_chain (rev [
-(0, 0); (* 2 = 1 + 1 *) (* the indices say how far back the chain to look *)
-(0, 1); (* 3 = 2 + 1 *)
-(0, 0); (* 6 = 3 + 3 *)
-(0, 0); (* 12 = 6 + 6 *)
-(0, 0); (* 24 = 12 + 12 *)
-(0, 2); (* 30 = 24 + 6 *)
-(0, 6)] (* 31 = 30 + 1 *)
-) = [31; 30; 24; 12; 6; 3; 2]. reflexivity. Qed.
+  Example wikipedia_addition_chain : fold_chain 0 plus [
+  (0, 0); (* 2 = 1 + 1 *) (* the indices say how far back the chain to look *)
+  (0, 1); (* 3 = 2 + 1 *)
+  (0, 0); (* 6 = 3 + 3 *)
+  (0, 0); (* 12 = 6 + 6 *)
+  (0, 0); (* 24 = 12 + 12 *)
+  (0, 2); (* 30 = 24 + 6 *)
+  (0, 6)] (* 31 = 30 + 1 *)
+  [1] = 31. reflexivity. Qed.
 
   Context {G eq op id} {monoid:@Algebra.monoid G eq op id}.
+  Context {scalarmult} {is_scalarmult:@ScalarMult.is_scalarmult G eq op id scalarmult}.
   Local Infix "=" := eq : type_scope.
 
-  Function add_chain_exp (is : list (nat*nat)) (x : G) : list G :=
-    match is with
-    | nil => nil
-    | (i,j)::is' =>
-      let chain' := add_chain_exp is' x in
-      op (nth_default x chain' i) (nth_default x chain' j) ::chain'
-    end.
-
-  Fixpoint scalarmult n (x : G) : G := match n with
-    | O    => id
-    | S n' => op x (scalarmult n' x)
-    end.
-
-  Lemma add_chain_exp_step : forall i j is x,
-    (forall n, nth_default x (add_chain_exp is x) n = scalarmult (nth_default 1 (add_chain is) n) x) ->
-    (eqlistA eq)
-    (add_chain_exp ((i,j) :: is) x)
-      (op (scalarmult (nth_default 1 (add_chain is) i) x)
-         (scalarmult (nth_default 1 (add_chain is) j) x) :: add_chain_exp is x).
-  Proof.
-    intros.
-    unfold add_chain_exp; fold add_chain_exp.
-    apply eqlistA_cons; [ | reflexivity].
-    f_equiv; auto.
-  Qed.
-
-  Lemma scalarmult_same : forall c x y, eq x y -> eq (scalarmult c x) (scalarmult c y).
-  Proof.
-    induction c; intros.
-    + reflexivity.
-    + simpl. f_equiv; auto.
-  Qed.
-
-  Lemma scalarmult_pow_add : forall a b x, scalarmult (a + b) x = op (scalarmult a x) (scalarmult b x).
+  Lemma fold_chain_exp' : forall (x:G) is acc ref
+      (H:forall i, nth_default id acc i = scalarmult (nth_default 0 ref i) x)
+      (Hl:Logic.eq (length acc) (length ref)),
+      fold_chain id op is acc = scalarmult (fold_chain 0 plus is ref) x.
   Proof.
-    intros; eapply scalarmult_add_l.
-    Grab Existential Variables.
-    2:eauto.
-    econstructor; try reflexivity.
-    repeat intro; subst.
-    auto using scalarmult_same.
+    induction is; intros; simpl @fold_chain.
+    { repeat break_match; specialize (H 0); rewrite ?nth_default_cons, ?nth_default_cons_S in H;
+      solve [ simpl length in *; discriminate | apply H | rewrite scalarmult_0_l; reflexivity ]. }
+    { repeat break_match. eapply IHis; intros.
+      { match goal with
+          [H:context [nth_default _ ?l _] |- context[nth_default _ (?h::?l) ?i] ]
+          => destruct i; rewrite ?nth_default_cons, ?nth_default_cons_S;
+             solve [ apply H | rewrite !H, <-scalarmult_add_l; reflexivity ]
+        end. }
+      { auto with distr_length. } }
   Qed.
 
-  Lemma add_chain_exp_spec : forall is x,
-    (forall n, nth_default x (add_chain_exp is x) n = scalarmult (nth_default 1 (add_chain is) n) x).
+  Lemma fold_chain_exp x is: fold_chain id op is [x] = scalarmult (fold_chain 0 plus is [1]) x.
   Proof.
-    induction is; intros.
-    + simpl; rewrite !nth_default_nil. cbv.
-      symmetry; apply right_identity.
-    + destruct a.
-      rewrite add_chain_exp_step by auto.
-      unfold add_chain; fold add_chain.
-      destruct n.
-      - rewrite !nth_default_cons, scalarmult_pow_add. reflexivity.
-      - rewrite !nth_default_cons_S; auto.
+    eapply fold_chain_exp'; intros; trivial.
+    destruct i; try destruct i; rewrite ?nth_default_cons_S, ?nth_default_cons, ?nth_default_nil;
+      rewrite ?scalarmult_1_l, ?scalarmult_0_l; reflexivity.
   Qed.
-
-  Lemma add_chain_exp_answer : forall is x n, Logic.eq (head (add_chain is)) (Some n) ->
-    option_eq eq (Some (scalarmult n x)) (head (add_chain_exp is x)).
-  Proof.
-    intros.
-    change head with (fun {T} (xs : list T) => nth_error xs 0) in *.
-    cbv beta in *.
-    cbv [option_eq].
-    destruct is; [ discriminate | ].
-    destruct p.
-    simpl in *.
-    injection H; clear H; intro H.
-    subst n.
-    rewrite !add_chain_exp_spec.
-    apply scalarmult_pow_add.
-  Qed.
-
 End AddChainExp.
\ No newline at end of file
diff --git a/src/Util/Decidable.v b/src/Util/Decidable.v
index 8488ad303..3988701a8 100644
--- a/src/Util/Decidable.v
+++ b/src/Util/Decidable.v
@@ -4,10 +4,13 @@ Require Import Coq.Logic.Eqdep_dec.
 Require Import Crypto.Util.Sigma.
 Require Import Crypto.Util.HProp.
 Require Import Crypto.Util.Equality.
+Require Import Coq.ZArith.BinInt.
+Require Import Coq.NArith.BinNat.
 
 Local Open Scope type_scope.
 
 Class Decidable (P : Prop) := dec : {P} + {~P}.
+Arguments dec _%type_scope {_}.
 
 Notation DecidableRel R := (forall x y, Decidable (R x y)).
 
@@ -86,11 +89,13 @@ Hint Extern 0 (Decidable (~?A)) => apply (@dec_not A) : typeclass_instances.
 Global Instance dec_eq_unit : DecidableRel (@eq unit) | 10. exact _. Defined.
 Global Instance dec_eq_bool : DecidableRel (@eq bool) | 10. exact _. Defined.
 Global Instance dec_eq_Empty_set : DecidableRel (@eq Empty_set) | 10. exact _. Defined.
-Global Instance dec_eq_nat : DecidableRel (@eq nat) | 10. exact _. Defined.
 Global Instance dec_eq_prod {A B} `{DecidableRel (@eq A), DecidableRel (@eq B)} : DecidableRel (@eq (A * B)) | 10. exact _. Defined.
 Global Instance dec_eq_sum {A B} `{DecidableRel (@eq A), DecidableRel (@eq B)} : DecidableRel (@eq (A + B)) | 10. exact _. Defined.
 Global Instance dec_eq_sigT_hprop {A P} `{DecidableRel (@eq A), forall a : A, IsHProp (P a)} : DecidableRel (@eq (@sigT A P)) | 10. exact _. Defined.
 Global Instance dec_eq_sig_hprop {A} {P : A -> Prop} `{DecidableRel (@eq A), forall a : A, IsHProp (P a)} : DecidableRel (@eq (@sig A P)) | 10. exact _. Defined.
+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 Decidable_respects_iff A B (H : A <-> B) : (Decidable A -> Decidable B) * (Decidable B -> Decidable A).
 Proof. solve_decidable_transparent. Defined.
@@ -101,5 +106,14 @@ Proof. solve_decidable_transparent. Defined.
 Lemma Decidable_iff_to_flip_impl A B (H : A <-> B) : Decidable B -> Decidable A.
 Proof. solve_decidable_transparent. Defined.
 
+Lemma dec_bool : forall {P} {Pdec:Decidable P}, (if dec P then true else false) = true -> P.
+Proof. intros. destruct dec; solve [ auto | discriminate ]. Qed.
+
+Ltac vm_decide := apply dec_bool; vm_compute; reflexivity.
+Ltac lazy_decide := apply dec_bool; lazy; reflexivity.
+
+Ltac vm_decide_no_check := apply dec_bool; vm_cast_no_check (eq_refl true).
+Ltac lazy_decide_no_check := apply dec_bool; exact_no_check (eq_refl true).
+
 (** For dubious compatibility with [eauto using]. *)
 Hint Extern 2 (Decidable _) => progress unfold Decidable : typeclass_instances core.
diff --git a/src/Util/NumTheoryUtil.v b/src/Util/NumTheoryUtil.v
index 29fedaa9b..8b8595bb7 100644
--- a/src/Util/NumTheoryUtil.v
+++ b/src/Util/NumTheoryUtil.v
@@ -95,13 +95,13 @@ Proof.
   apply in_mod_ZPGroup; auto.
 Qed.
 
-Lemma fermat_inv : forall a, a mod p <> 0 -> (a * (a^(p-2) mod p)) mod p = 1.
+Lemma fermat_inv : forall a, a mod p <> 0 -> ((a^(p-2) mod p) * a) mod p = 1.
 Proof.
   intros.
   pose proof (prime_ge_2 _ prime_p).
-  rewrite Zmult_mod_idemp_r.
-  replace (a * a ^ (p - 2)) with (a^(p-1)).
-    2:replace (a * a ^ (p - 2)) with (a^1 * a ^ (p - 2)) by ring.
+  rewrite Zmult_mod_idemp_l.
+  replace (a ^ (p - 2) * a) with (a^(p-1)).
+    2:replace (a ^ (p - 2) * a) with (a^1 * a ^ (p - 2)) by ring.
     2:rewrite <-Zpower_exp; try f_equal; omega.
   auto using fermat_little.
 Qed.