diff options
Diffstat (limited to 'src/Util')
-rw-r--r-- | src/Util/AdditionChainExponentiation.v | 117 | ||||
-rw-r--r-- | src/Util/Decidable.v | 16 | ||||
-rw-r--r-- | src/Util/NumTheoryUtil.v | 8 |
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. |