aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar Andres Erbsen <andreser@mit.edu>2016-02-14 15:55:44 -0500
committerGravatar Andres Erbsen <andreser@mit.edu>2016-02-14 15:55:44 -0500
commit094ccf074fc64cc8256278d26cca46107b9cc813 (patch)
treea8875e5d5ddf7695335262e5c9948f0d38eeecb3
parent0c52350824d510abe30518d8c66c8d3492267db9 (diff)
update F Coercions and tutorial
-rw-r--r--src/ModularArithmetic/ModularArithmeticTheorems.v57
-rw-r--r--src/ModularArithmetic/Tutorial.v59
-rw-r--r--src/Spec/ModularArithmetic.v22
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.