diff options
author | Jason Gross <jgross@mit.edu> | 2018-02-19 19:47:27 -0500 |
---|---|---|
committer | Jason Gross <jgross@mit.edu> | 2018-02-19 19:47:27 -0500 |
commit | 12c945d2d16053ee959430a60793f1db29ee2aaa (patch) | |
tree | 9687aa22219376190e0db9a0c6ed5c877db9a829 | |
parent | 861a5245adb27d3beb7579d5fe38e344a6a17f07 (diff) |
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.
-rw-r--r-- | src/Experiments/SimplyTypedArithmetic.v | 14 |
1 files changed, 9 insertions, 5 deletions
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. |