diff options
author | Andres Erbsen <andreser@mit.edu> | 2016-02-14 15:55:44 -0500 |
---|---|---|
committer | Andres Erbsen <andreser@mit.edu> | 2016-02-14 15:55:44 -0500 |
commit | 094ccf074fc64cc8256278d26cca46107b9cc813 (patch) | |
tree | a8875e5d5ddf7695335262e5c9948f0d38eeecb3 | |
parent | 0c52350824d510abe30518d8c66c8d3492267db9 (diff) |
update F Coercions and tutorial
-rw-r--r-- | src/ModularArithmetic/ModularArithmeticTheorems.v | 57 | ||||
-rw-r--r-- | src/ModularArithmetic/Tutorial.v | 59 | ||||
-rw-r--r-- | src/Spec/ModularArithmetic.v | 22 |
3 files changed, 101 insertions, 37 deletions
diff --git a/src/ModularArithmetic/ModularArithmeticTheorems.v b/src/ModularArithmetic/ModularArithmeticTheorems.v index 7501bfa23..24bf49dc9 100644 --- a/src/ModularArithmetic/ModularArithmeticTheorems.v +++ b/src/ModularArithmetic/ModularArithmeticTheorems.v @@ -6,29 +6,34 @@ Require Import BinInt Zdiv Znumtheory NArith. (* import Zdiv before Znumtheory * Require Import Coq.Classes.Morphisms Setoid. Require Export Ring_theory Field_theory Field_tac. -Theorem F_eq: forall {m} (x y : F m), x = y <-> FieldToZ x = FieldToZ y. -Proof. - destruct x, y; intuition; simpl in *; try congruence. - subst_max. - f_equal. - eapply UIP_dec, Z.eq_dec. -Qed. - -Lemma F_opp_spec : forall {m} (a:F m), add a (opp a) = ZToField 0. - intros m a. - pose (@opp_with_spec m) as H. - change (@opp m) with (proj1_sig H). - destruct H; eauto. -Qed. +Section ModularArithmeticPreliminaries. + Context {m:Z}. + Local Coercion ZToFm := ZToField : BinNums.Z -> F m. Hint Unfold ZToFm. -Lemma F_pow_spec : forall {m} (a:F m), - pow a 0%N = 1%F /\ forall x, pow a (1 + x)%N = mul a (pow a x). -Proof. - intros m a. - pose (@pow_with_spec m) as H. - change (@pow m) with (proj1_sig H). - destruct H; eauto. -Qed. + Theorem F_eq: forall (x y : F m), x = y <-> FieldToZ x = FieldToZ y. + Proof. + destruct x, y; intuition; simpl in *; try congruence. + subst_max. + f_equal. + eapply UIP_dec, Z.eq_dec. + Qed. + + Lemma F_opp_spec : forall (a:F m), add a (opp a) = 0. + intros a. + pose (@opp_with_spec m) as H. + change (@opp m) with (proj1_sig H). + destruct H; eauto. + Qed. + + Lemma F_pow_spec : forall (a:F m), + pow a 0%N = 1%F /\ forall x, pow a (1 + x)%N = mul a (pow a x). + Proof. + intros a. + pose (@pow_with_spec m) as H. + change (@pow m) with (proj1_sig H). + destruct H; eauto. + Qed. +End ModularArithmeticPreliminaries. (* Fails iff the input term does some arithmetic with mod'd values. *) Ltac notFancy E := @@ -77,7 +82,6 @@ end. Ltac Fdefn := intros; - unfold unfoldFm; rewrite ?F_opp_spec; repeat match goal with [ x : F _ |- _ ] => destruct x end; try eq_remove_proofs; @@ -239,6 +243,7 @@ End FandZ. Section RingModuloPre. Context {m:Z}. + Local Coercion ZToFm := ZToField : Z -> F m. Hint Unfold ZToFm. (* Substitution to prove all Compats *) Ltac compat := repeat intro; subst; trivial. @@ -311,8 +316,8 @@ Section RingModuloPre. Qed. (***** Division Theory *****) - Definition Fquotrem(a b: F m): F m * F m := - let '(q, r) := (Z.quotrem a b) in (ZToField q, ZToField r). + Definition Fquotrem(a b: F m): F m * F m := + let '(q, r) := (Z.quotrem a b) in (q : F m, r : F m). Lemma Fdiv_theory : div_theory eq (@add m) (@mul m) (@id _) Fquotrem. Proof. constructor; intros; unfold Fquotrem, id. @@ -346,7 +351,7 @@ Section RingModuloPre. 0%Z 1%Z Z.add Z.mul Z.sub Z.opp Z.eqb (@ZToField m). Proof. - constructor; intros; try Fdefn; unfold id, unfoldFm; + constructor; intros; try Fdefn; unfold id; try (apply gf_eq; simpl; intuition). - apply sub_intersperse_modulus. diff --git a/src/ModularArithmetic/Tutorial.v b/src/ModularArithmetic/Tutorial.v index ae2b63bad..c80decdcf 100644 --- a/src/ModularArithmetic/Tutorial.v +++ b/src/ModularArithmetic/Tutorial.v @@ -1,6 +1,65 @@ Require Import BinInt Zpower ZArith Znumtheory. Require Import Spec.ModularArithmetic ModularArithmetic.PrimeFieldTheorems. + +(* Example for modular arithmetic with a concrete modulus in a section *) +Section Mod24. + (* Set notations + - * / refer to F operations *) + Local Open Scope F_scope. + + (* Specify modulus *) + Let q := 24. + + (* Boilerplate for letting Z numbers be interpreted as field elements *) + Local Coercion ZToFq := ZToField : BinNums.Z -> F q. Hint Unfold ZToFq. + + (* Boilerplate for [ring]. Similar boilerplate works for [field] if + the modulus is prime . *) + Add Ring Ffield_q : (@Fring_theory q) + (morphism (@Fring_morph q), + preprocess [unfold ZToFq; Fpreprocess], + postprocess [Fpostprocess; try exact Fq_1_neq_0; try assumption], + constants [Fconstant], + div (@Fmorph_div_theory q), + power_tac (@Fpower_theory q) [Fexp_tac]). + + Lemma sumOfSquares : forall a b: F q, (a+b)^2 = a^2 + ZToField 2*a*b + b^2. + Proof. + intros. + ring. + Qed. +End Mod24. + +(* Example for modular arithmetic with an abstract modulus in a section *) +Section Modq. + Context {q:Z} {prime_q:prime q}. + Existing Instance prime_q. + + (* Set notations + - * / refer to F operations *) + Local Open Scope F_scope. + + (* Boilerplate for letting Z numbers be interpreted as field elements *) + Local Coercion ZToFq := ZToField : BinNums.Z -> F q. Hint Unfold ZToFq. + + (* Boilerplate for [field]. Similar boilerplate works for [ring] if + the modulus is not prime . *) + Add Field Ffield_q' : (@Ffield_theory q _) + (morphism (@Fring_morph q), + preprocess [unfold ZToFq; Fpreprocess], + postprocess [Fpostprocess; try exact Fq_1_neq_0; try assumption], + constants [Fconstant], + div (@Fmorph_div_theory q), + power_tac (@Fpower_theory q) [Fexp_tac]). + + Lemma sumOfSquares' : forall a b: F q, (a+b)^2 = a^2 + ZToField 2*a*b + b^2. + Proof. + intros. + field. + Qed. +End Modq. + +(*** The old way: Modules ***) + Module Modulus31 <: PrimeModulus. Definition modulus := 2^5 - 1. Lemma prime_modulus : prime modulus. diff --git a/src/Spec/ModularArithmetic.v b/src/Spec/ModularArithmetic.v index 5f8b9ed38..da6a62ada 100644 --- a/src/Spec/ModularArithmetic.v +++ b/src/Spec/ModularArithmetic.v @@ -19,33 +19,33 @@ Infix "mod" := BinInt.Z.modulo (at level 40, no associativity) : Z_scope. Local Open Scope Z_scope. Definition F (modulus : BinInt.Z) := { z : BinInt.Z | z = z mod modulus }. +Definition ZToField {m} (a:BinNums.Z) : F m := exist _ (a mod m) (Pre.Z_mod_mod a m). Coercion FieldToZ {m} (a:F m) : BinNums.Z := proj1_sig a. Section FieldOperations. Context {m : BinInt.Z}. - Let Fm := F m. (* Note: if inlined, coercions say "anomaly please report" *) - Coercion unfoldFm (a:Fm) : F m := a. - Coercion ZToField (a:BinNums.Z) : Fm := exist _ (a mod m) (Pre.Z_mod_mod a m). + (* Coercion without Context {m} --> non-uniform inheritance --> Anomalies *) + Local Coercion ZToFm := ZToField : BinNums.Z -> F m. - Definition add (a b:Fm) : Fm := ZToField (a + b). - Definition mul (a b:Fm) : Fm := ZToField (a * b). + Definition add (a b:F m) : F m := ZToField (a + b). + Definition mul (a b:F m) : F m := ZToField (a * b). - Definition opp_with_spec : { opp : Fm -> Fm + Definition opp_with_spec : { opp : F m -> F m | forall x, add x (opp x) = 0 } := Pre.opp_impl. Definition opp : F m -> F m := Eval hnf in proj1_sig opp_with_spec. - Definition sub (a b:Fm) : Fm := add a (opp b). + Definition sub (a b:F m) : F m := add a (opp b). - Definition inv_with_spec : { inv : Fm -> Fm + Definition inv_with_spec : { inv : F m -> F m | inv 0 = 0 /\ ( Znumtheory.prime m -> - forall (a:Fm), a <> 0 -> mul a (inv a) = 1 ) + forall (a:F m), a <> 0 -> mul a (inv a) = 1 ) } := Pre.inv_impl. Definition inv : F m -> F m := Eval hnf in proj1_sig inv_with_spec. - Definition div (a b:Fm) : Fm := mul a (inv b). + Definition div (a b:F m) : F m := mul a (inv b). - Definition pow_with_spec : { pow : Fm -> BinNums.N -> Fm + Definition pow_with_spec : { pow : F m -> BinNums.N -> F m | forall a, pow a 0%N = 1 /\ forall x, pow a (1 + x)%N = mul a (pow a x) } := Pre.pow_impl. |