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, 36 insertions, 81 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