diff options
Diffstat (limited to 'src/ModularArithmetic')
-rw-r--r-- | src/ModularArithmetic/ModularBaseSystem.v | 4 | ||||
-rw-r--r-- | src/ModularArithmetic/ModularBaseSystemOpt.v | 16 | ||||
-rw-r--r-- | src/ModularArithmetic/ModularBaseSystemProofs.v | 23 |
3 files changed, 36 insertions, 7 deletions
diff --git a/src/ModularArithmetic/ModularBaseSystem.v b/src/ModularArithmetic/ModularBaseSystem.v index 2f264fa6c..6534c31b5 100644 --- a/src/ModularArithmetic/ModularBaseSystem.v +++ b/src/ModularArithmetic/ModularBaseSystem.v @@ -43,8 +43,8 @@ Section ModularBaseSystem. Definition one : digits := encode (F.of_Z _ 1). - (* Placeholder *) - Definition opp (x : digits) : digits := encode (F.opp (decode x)). + Definition opp (modulus_multiple x : digits) : + digits := sub modulus_multiple zero x. Definition pow (x : digits) (chain : list (nat * nat)) : digits := fold_chain one mul chain (x :: nil). diff --git a/src/ModularArithmetic/ModularBaseSystemOpt.v b/src/ModularArithmetic/ModularBaseSystemOpt.v index 000f2599c..31fab7cd8 100644 --- a/src/ModularArithmetic/ModularBaseSystemOpt.v +++ b/src/ModularArithmetic/ModularBaseSystemOpt.v @@ -441,6 +441,22 @@ Section Subtraction. Definition sub_opt_correct us vs : sub_opt us vs = sub coeff us vs := proj2_sig (sub_opt_sig us vs). + + Definition opp_opt_sig (us : digits) : { b : digits | b = opp coeff us }. + Proof. + eexists. + cbv [opp]. + rewrite <-sub_opt_correct. + reflexivity. + Defined. + + Definition opp_opt (us : digits) : digits + := Eval cbv [proj1_sig opp_opt_sig] in proj1_sig (opp_opt_sig us). + + Definition opp_opt_correct us + : opp_opt us = opp coeff us + := proj2_sig (opp_opt_sig us). + End Subtraction. Section Multiplication. diff --git a/src/ModularArithmetic/ModularBaseSystemProofs.v b/src/ModularArithmetic/ModularBaseSystemProofs.v index 5c9bdc52c..2d5f5a0c5 100644 --- a/src/ModularArithmetic/ModularBaseSystemProofs.v +++ b/src/ModularArithmetic/ModularBaseSystemProofs.v @@ -204,6 +204,19 @@ Section FieldOperationProofs. rewrite mm_spec. rewrite Algebra.left_identity. f_equal; assumption. Qed. + + Lemma opp_rep : forall u x, u ~= x -> opp mm u ~= F.opp x. + Proof. + cbv [opp rep]; intros. + rewrite sub_rep by (apply encode_rep || eassumption). + apply F.eq_to_Z_iff. + rewrite F.to_Z_opp. + rewrite <-Z.sub_0_l. + pose proof @F.of_Z_sub. + transitivity (F.to_Z (F.of_Z modulus (0 - F.to_Z x))); + [ rewrite F.of_Z_sub, F.of_Z_to_Z; reflexivity | ]. + rewrite F.to_Z_of_Z. reflexivity. + Qed. End Subtraction. Section PowInv. @@ -252,13 +265,13 @@ Section FieldOperationProofs. rewrite !encode_rep. assumption. Qed. - Global Instance opp_Proper : Proper (eq ==> eq) opp. + Global Instance opp_Proper : Proper (Logic.eq ==> eq ==> eq) opp. Admitted. Global Instance add_Proper : Proper (eq ==> eq ==> eq) add. Admitted. - - Global Instance sub_Proper : Proper (eq ==> eq ==> eq ==> eq) sub. + + Global Instance sub_Proper : Proper (Logic.eq ==> eq ==> eq ==> eq) sub. Admitted. Global Instance mul_Proper : Proper (eq ==> eq ==> eq) mul. @@ -284,7 +297,7 @@ Section FieldOperationProofs. Qed. Lemma modular_base_system_field : - @field digits eq zero one opp add (sub coeff) mul (inv chain chain_correct) div. + @field digits eq zero one (opp coeff) add (sub coeff) mul (inv chain chain_correct) div. Proof. eapply (Field.isomorphism_to_subfield_field (phi := decode) (fieldR := @F.field_modulo modulus prime_modulus)). Grab Existential Variables. @@ -295,7 +308,7 @@ Section FieldOperationProofs. + intros; eapply mul_rep; auto. + intros; eapply sub_rep; auto using coeff_mod. + intros; eapply add_rep; auto. - + intros; eapply encode_rep. + + intros; eapply opp_rep; auto using coeff_mod. + eapply _zero_neq_one. + trivial. Qed. |