diff options
author | Andres Erbsen <andreser@mit.edu> | 2017-03-02 08:18:01 -0500 |
---|---|---|
committer | Andres Erbsen <andreser@mit.edu> | 2017-03-02 13:37:14 -0500 |
commit | 7f0ba34481f59db0cf430d7a08b8b65d953eb803 (patch) | |
tree | 4624191d9c9fd7923688ea6be391ead2259e6be6 | |
parent | 90b9f8d4f1273a78f8ffddb958c628593f0408b8 (diff) |
fixup NewBasesystem
-rw-r--r-- | src/NewBaseSystem.v | 26 |
1 files changed, 14 insertions, 12 deletions
diff --git a/src/NewBaseSystem.v b/src/NewBaseSystem.v index 628a406c9..6f1ac11e3 100644 --- a/src/NewBaseSystem.v +++ b/src/NewBaseSystem.v @@ -284,14 +284,14 @@ Local Ltac prove_eval := | _ => nsatz end. -Definition mod_eq m a b := a mod m = b mod m. +Definition mod_eq (m:positive) a b := a mod m = b mod m. Global Instance mod_eq_equiv m : RelationClasses.Equivalence (mod_eq m). Proof. constructor; congruence. Qed. Definition mod_eq_dec m a b : {mod_eq m a b} + {~ mod_eq m a b} := Z.eq_dec _ _. Lemma mod_eq_Z2F_iff m a b : mod_eq m a b <-> Logic.eq (F.of_Z m a) (F.of_Z m b). -Proof. rewrite <-F.eq_of_Z_iff. reflexivity. Qed. +Proof. rewrite <-F.eq_of_Z_iff; reflexivity. Qed. Delimit Scope runtime_scope with RT. @@ -388,15 +388,17 @@ Module B. Hint Opaque reduce : uncps. Hint Rewrite reduce_cps_id : uncps. - Lemma reduction_rule a b s c (modulus_nonzero:s-c<>0) : - (a + s * b) mod (s - c) = (a + c * b) mod (s - c). - Proof. replace (a + s * b) with ((a + c*b) + b*(s-c)) by nsatz. - rewrite Z.add_mod, Z_mod_mult, Z.add_0_r, Z.mod_mod; trivial. Qed. - Lemma eval_reduce s c p (s_nonzero:s<>0) (modulus_nonzero:s-eval c<>0): - mod_eq (s - eval c) (eval (reduce s c p)) (eval p). + Lemma reduction_rule a b s c m (m_eq:Z.pos m = s - c): + (a + s * b) mod m = (a + c * b) mod m. Proof. - cbv [reduce reduce_cps mod_eq]; prove_eval; - rewrite <-reduction_rule by auto; prove_eval. + rewrite m_eq. assert (Z.pos m <> 0) by (intro; discriminate). clear m_eq. + replace (a + s * b) with ((a + c*b) + b*(s-c)) by nsatz. + rewrite Z.add_mod, Z_mod_mult, Z.add_0_r, Z.mod_mod; trivial. Admitted. + Lemma eval_reduce s c p (s_nonzero:s<>0) m (m_eq : Z.pos m = s - eval c) : + mod_eq m (eval (reduce s c p)) (eval p). + Proof. + cbv [reduce reduce_cps mod_eq]; prove_eval. + erewrite <-reduction_rule by eauto; prove_eval. Qed. Hint Rewrite eval_reduce using (omega || assumption) : push_basesystem_eval. (* Why TF does this hint get picked up outside the section (while other eval_ hints do not?) *) @@ -740,7 +742,7 @@ Module B. (* Lemmas about converting to/from F. Will be useful in proving that basesystem is isomorphic to F.commutative_ring_modulo.*) Section F. - Context {sz:nat} {sz_nonzero : sz<>0%nat} {m :Z}. + Context {sz:nat} {sz_nonzero : sz<>0%nat} {m :positive}. Context (weight_divides : forall i : nat, weight (S i) / weight i <> 0). Context {modulo div:Z->Z->Z} {div_mod : forall a b:Z, b <> 0 -> @@ -906,7 +908,7 @@ Section Ops. Let carry_chain := (seq 0 sz) ++ ([0;1])%nat. (* These `Lets` are inferred from those above *) - Let m := Eval compute in s - Associational.eval c. (* modulus *) + Let m := Eval compute in Z.to_pos (s - Associational.eval c). (* modulus *) Let sz2 := Eval compute in ((sz * 2) - 1)%nat. Let coef := Eval vm_compute in (@Positional.encode wt modulo div sz (coef_div_modulus * (s-Associational.eval c))). (* subtraction coefficient *) Let coef_mod : mod_eq m (Positional.eval (n:=sz) wt coef) 0 := eq_refl. |