aboutsummaryrefslogtreecommitdiff
path: root/src/Util
diff options
context:
space:
mode:
Diffstat (limited to 'src/Util')
-rw-r--r--src/Util/AdditionChainExponentiation.v117
-rw-r--r--src/Util/Decidable.v16
-rw-r--r--src/Util/NumTheoryUtil.v8
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.
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-06 11:58:06 +0000