From f997c539d69e1d73f0ab4d76113b22729d49ed0b Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Fri, 24 Nov 2017 14:14:24 -0500 Subject: [demo] Replace (max (length a) (length b)) with explicit nat arg --- src/Experiments/SimplyTypedArithmetic.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Experiments/SimplyTypedArithmetic.v b/src/Experiments/SimplyTypedArithmetic.v index 0ec92fdba..5a839a842 100644 --- a/src/Experiments/SimplyTypedArithmetic.v +++ b/src/Experiments/SimplyTypedArithmetic.v @@ -167,11 +167,11 @@ Module Positional. Section Positional. let b_a := to_associational n b in let ab_a := Associational.mul a_a b_a in let abm_a := Associational.reduce s c ab_a in - from_associational (max (length a) (length b)) abm_a. + from_associational n abm_a. Lemma eval_mulmod n (f g:list Z) (Hf : length f = n) (Hg : length g = n) : eval n (mulmod n f g) mod m = (eval n f * eval n g) mod m. - Proof. cbv [mulmod]; rewrite Hm, Hf, Hg in *; push; trivial. + Proof. cbv [mulmod]; rewrite Hm in *; push; trivial. destruct f, g; simpl in *; [ right; subst n | left; try omega.. ]. clear; cbv -[Associational.reduce]. induction c as [|?? IHc]; simpl; trivial. Qed. -- cgit v1.2.3