From 4e336857231e909b4384a8b575affbe39179aa39 Mon Sep 17 00:00:00 2001 From: jadep Date: Tue, 23 Aug 2016 13:42:35 -0400 Subject: Updated AdditionChainExponentiation.v such that the exponentiation correctness is in terms of N rather than nat; this allows us to compute the correctness proof for large exponents. --- src/Util/AdditionChainExponentiation.v | 19 +++++++++++-------- 1 file changed, 11 insertions(+), 8 deletions(-) (limited to 'src/Util/AdditionChainExponentiation.v') diff --git a/src/Util/AdditionChainExponentiation.v b/src/Util/AdditionChainExponentiation.v index 6a028dda8..39e2a2770 100644 --- a/src/Util/AdditionChainExponentiation.v +++ b/src/Util/AdditionChainExponentiation.v @@ -1,4 +1,5 @@ Require Import Coq.Lists.List Coq.Lists.SetoidList. Import ListNotations. +Require Import Coq.Numbers.BinNums Coq.NArith.BinNat. Require Import Crypto.Util.ListUtil. Require Import Algebra. Import Monoid ScalarMult. Require Import VerdiTactics. @@ -30,25 +31,27 @@ Section AddChainExp. 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. + Local Open Scope N_scope. + SearchAbout (N -> nat). + Local Notation "n * P" := (scalarmult (N.to_nat n) P) (only parsing). 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) + (H:forall i, nth_default id acc i = (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. + fold_chain id op is acc = (fold_chain 0 N.add is ref) * x. Proof. induction is; intros; simpl @fold_chain. - { repeat break_match; specialize (H 0); rewrite ?nth_default_cons, ?nth_default_cons_S in H; + { repeat break_match; specialize (H 0%nat); 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 + { repeat break_match. eapply IHis; intros; [|auto with distr_length]; []. + 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 ] + solve [ apply H | rewrite !H, <-scalarmult_add_l, Nnat.N2Nat.inj_add; reflexivity ] end. } - { auto with distr_length. } } Qed. - Lemma fold_chain_exp x is: fold_chain id op is [x] = scalarmult (fold_chain 0 plus is [1]) x. + Lemma fold_chain_exp x is: fold_chain id op is [x] = (fold_chain 0 N.add is [1]) * x. Proof. eapply fold_chain_exp'; intros; trivial. destruct i; try destruct i; rewrite ?nth_default_cons_S, ?nth_default_cons, ?nth_default_nil; -- cgit v1.2.3