aboutsummaryrefslogtreecommitdiff
path: root/src/ModularArithmetic/Tutorial.v
diff options
context:
space:
mode:
Diffstat (limited to 'src/ModularArithmetic/Tutorial.v')
-rw-r--r--src/ModularArithmetic/Tutorial.v77
1 files changed, 40 insertions, 37 deletions
diff --git a/src/ModularArithmetic/Tutorial.v b/src/ModularArithmetic/Tutorial.v
index 7d354ab3e..999c61971 100644
--- a/src/ModularArithmetic/Tutorial.v
+++ b/src/ModularArithmetic/Tutorial.v
@@ -11,17 +11,16 @@ Section Mod24.
Let q := 24.
(* Boilerplate for letting Z numbers be interpreted as field elements *)
- Let ZToFq := ZToField : BinNums.Z -> F q. Hint Unfold ZToFq. Local Coercion ZToFq : Z >-> F.
+ Let ZToFq := ZToField _ : BinNums.Z -> F q. Hint Unfold ZToFq. Local Coercion ZToFq : Z >-> F.
(* Boilerplate for [ring]. Similar boilerplate works for [field] if
the modulus is prime . *)
- Add Ring Fring_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]).
+ Add Ring _theory : (Zmod.ring_theory q)
+ (morphism (Zmod.ring_morph q),
+ preprocess [unfold ZToFq],
+ constants [Zmod.is_constant],
+ div (Zmod.morph_div_theory q),
+ power_tac (Zmod.power_theory q) [Zmod.is_pow_constant]).
Lemma sumOfSquares : forall a b: F q, (a+b)^2 = a^2 + 2*a*b + b^2.
Proof.
@@ -39,34 +38,33 @@ Section Modq.
Local Open Scope F_scope.
(* Boilerplate for letting Z numbers be interpreted as field elements *)
- Let ZToFq := ZToField : BinNums.Z -> F q. Hint Unfold ZToFq. Local Coercion ZToFq : Z >-> F.
+ Let ZToFq := ZToField _ : BinNums.Z -> F q. Hint Unfold ZToFq. Local Coercion ZToFq : Z >-> F.
(* 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 c: F q, c <> 0 -> ((a+b)/c)^2 = a^2/c^2 + ZToField 2*(a/c)*(b/c) + b^2/c^2.
+ Add Field _theory' : (Zmod.field_theory q)
+ (morphism (Zmod.ring_morph q),
+ preprocess [unfold ZToFq],
+ constants [Zmod.is_constant],
+ div (Zmod.morph_div_theory q),
+ power_tac (Zmod.power_theory q) [Zmod.is_pow_constant]).
+
+ Lemma sumOfSquares' : forall a b c: F q, c <> 0 -> ((a+b)/c)^2 = a^2/c^2 + 2*(a/c)*(b/c) + b^2/c^2.
Proof.
intros.
- field.
+ field; trivial.
Qed.
End Modq.
(*** The old way: Modules ***)
-Module Modulus31 <: PrimeModulus.
+Module Modulus31 <: Zmod.PrimeModulus.
Definition modulus := 2^5 - 1.
Lemma prime_modulus : prime modulus.
Admitted.
End Modulus31.
-Module Modulus127 <: PrimeModulus.
+Module Modulus127 <: Zmod.PrimeModulus.
Definition modulus := 2^127 - 1.
Lemma prime_modulus : prime modulus.
Admitted.
@@ -74,14 +72,14 @@ End Modulus127.
Module Example31.
(* Then we can construct a field with that modulus *)
- Module Import Field := FieldModulo Modulus31.
+ Module Import Field := Zmod.FieldModulo Modulus31.
Import Modulus31.
(* And pull in the appropriate notations *)
Local Open Scope F_scope.
(* First, let's solve a ring example*)
- Lemma ring_example: forall x: F modulus, x * (ZToField 2) = x + x.
+ Lemma ring_example: forall x: F modulus, x * (ZToField _ 2) = x + x.
Proof.
intros.
ring.
@@ -92,7 +90,7 @@ Module Example31.
Therefore, it is necessary to explicitly rewrite the modulus
(usually hidden by implicitn arguments) match the one passed to
[FieldModulo]. *)
- Lemma ring_example': forall x: F (2^5-1), x * (ZToField 2) = x + x.
+ Lemma ring_example': forall x: F (2^5-1), x * (ZToField _ 2) = x + x.
Proof.
intros.
change (2^5-1)%Z with modulus.
@@ -108,7 +106,7 @@ Module Example31.
Qed.
(* Then an example with exponentiation *)
- Lemma exp_example: forall x: F modulus, x ^ 2 + ZToField 2 * x + 1 = (x + 1) ^ 2.
+ Lemma exp_example: forall x: F modulus, x ^ 2 + ZToField _ 2 * x + 1 = (x + 1) ^ 2.
Proof.
intros; simpl.
field; trivial.
@@ -143,7 +141,7 @@ End Example31.
(* Notice that the field tactics work whether we know what the modulus is *)
Module TimesZeroTransparentTestModule.
- Module Import Theory := FieldModulo Modulus127.
+ Module Import Theory := Zmod.FieldModulo Modulus127.
Import Modulus127.
Local Open Scope F_scope.
@@ -153,9 +151,13 @@ Module TimesZeroTransparentTestModule.
Qed.
End TimesZeroTransparentTestModule.
-(* Or if we don't (i.e. it's opaque) *)
-Module TimesZeroParametricTestModule (M: PrimeModulus).
- Module Theory := FieldModulo M.
+(* An opaque modulus causes the field tactic to expand all constants
+ into matches on the modulus. Goals can still be proven, but with
+ significant overhead. Consider using an entirely abstract
+ [Algebra.field] instead. *)
+
+Module TimesZeroParametricTestModule (M: Zmod.PrimeModulus).
+ Module Theory := Zmod.FieldModulo M.
Import Theory M.
Local Open Scope F_scope.
@@ -164,26 +166,27 @@ Module TimesZeroParametricTestModule (M: PrimeModulus).
field.
Qed.
- Lemma realisticFraction : forall x y d : F modulus, (x * 1 + y * 0) / (1 + d * x * 0 * y * 1) = x.
+ Lemma realisticFraction : forall x y d : F modulus, 1 <> ZToField modulus 0 -> (x * 1 + y * 0) / (1 + d * x * 0 * y * 1) = x.
Proof.
intros.
- field; try exact Fq_1_neq_0.
+ field; assumption.
Qed.
Lemma biggerFraction : forall XP YP ZP TP XQ YQ ZQ TQ d : F modulus,
+ 1 <> ZToField modulus 0 ->
ZQ <> 0 ->
ZP <> 0 ->
ZP * ZQ * ZP * ZQ + d * XP * XQ * YP * YQ <> 0 ->
- ZP * ZToField 2 * ZQ * (ZP * ZQ) + XP * YP * ZToField 2 * d * (XQ * YQ) <> 0 ->
- ZP * ZToField 2 * ZQ * (ZP * ZQ) - XP * YP * ZToField 2 * d * (XQ * YQ) <> 0 ->
+ ZP * ZToField _ 2 * ZQ * (ZP * ZQ) + XP * YP * ZToField _ 2 * d * (XQ * YQ) <> 0 ->
+ ZP * ZToField _ 2 * ZQ * (ZP * ZQ) - XP * YP * ZToField _ 2 * d * (XQ * YQ) <> 0 ->
((YP + XP) * (YQ + XQ) - (YP - XP) * (YQ - XQ)) *
- (ZP * ZToField 2 * ZQ - XP * YP / ZP * ZToField 2 * d * (XQ * YQ / ZQ)) /
- ((ZP * ZToField 2 * ZQ - XP * YP / ZP * ZToField 2 * d * (XQ * YQ / ZQ)) *
- (ZP * ZToField 2 * ZQ + XP * YP / ZP * ZToField 2 * d * (XQ * YQ / ZQ))) =
+ (ZP * ZToField _ 2 * ZQ - XP * YP / ZP * ZToField _ 2 * d * (XQ * YQ / ZQ)) /
+ ((ZP * ZToField _ 2 * ZQ - XP * YP / ZP * ZToField _ 2 * d * (XQ * YQ / ZQ)) *
+ (ZP * ZToField _ 2 * ZQ + XP * YP / ZP * ZToField _ 2 * d * (XQ * YQ / ZQ))) =
(XP / ZP * (YQ / ZQ) + YP / ZP * (XQ / ZQ)) / (1 + d * (XP / ZP) * (XQ / ZQ) * (YP / ZP) * (YQ / ZQ)).
Proof.
intros.
- field; assumption.
+ field; repeat split; assumption.
Qed.
End TimesZeroParametricTestModule.
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-23 11:40:20 +0000