From 12c945d2d16053ee959430a60793f1db29ee2aaa Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Mon, 19 Feb 2018 19:47:27 -0500 Subject: Fix balance on sub With some help from @jadephilipoom Previously, the carrying was removing the effect of `coef`, and we were getting too small a balance. --- src/Experiments/SimplyTypedArithmetic.v | 14 +++++++++----- 1 file changed, 9 insertions(+), 5 deletions(-) (limited to 'src/Experiments') diff --git a/src/Experiments/SimplyTypedArithmetic.v b/src/Experiments/SimplyTypedArithmetic.v index 1e9a5d5b7..53f661b68 100644 --- a/src/Experiments/SimplyTypedArithmetic.v +++ b/src/Experiments/SimplyTypedArithmetic.v @@ -332,8 +332,13 @@ Module Positional. Section Positional. let negA := Associational.negate_snd A in from_associational n negA. + Definition scmul (x:Z) (a:list Z) : list Z + := let A := to_associational n a in + let R := Associational.mul A [(1, x)] in + from_associational n R. + Definition balance : list Z - := encode n s c (coef * (s - Associational.eval c)). + := scmul coef (encode n s c (s - Associational.eval c)). Definition sub (a b:list Z) : list Z := let ca := add n balance a in @@ -346,16 +351,15 @@ Module Positional. Section Positional. = (eval n a - eval n b) mod (s - Associational.eval c). Proof. destruct (zerop n); subst; try reflexivity. - intros; cbv [sub balance negate_snd]; push; repeat distr_length; + intros; cbv [sub balance scmul negate_snd]; push; repeat distr_length; eauto with omega. - push_Zmod; push; push_Zmod; pull_Zmod; distr_length; eauto. - f_equal; omega. + push_Zmod; push; pull_Zmod; push_Zmod; pull_Zmod; distr_length; eauto. Qed. Hint Rewrite eval_sub : push_eval. Lemma length_sub a b : length a = n -> length b = n -> length (sub a b) = n. - Proof. intros; cbv [sub balance negate_snd]; repeat distr_length. Qed. + Proof. intros; cbv [sub balance scmul negate_snd]; repeat distr_length. Qed. Hint Rewrite length_sub : distr_length. Definition opp (a:list Z) : list Z := sub (zeros n) a. -- cgit v1.2.3