Skip to content

Commit 78721f6

Browse files
andres-erbsenandres-erbsen
committed
add Nsatz support for Zmod
1 parent 0fb9f60 commit 78721f6

File tree

11 files changed

+150
-25
lines changed

11 files changed

+150
-25
lines changed

‎doc/changelog/02-added/156-zmod-nsatz.rst‎

Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,14 @@
1+
- in `ZmodNsatz` and `Zmod`
2+
3+
+ Added support for the `nsatz` tactic on `Zmod`
4+
(`#156 <https://github.com/coq/stdlib/pull/156>`_,
5+
by Andres Erbsen).
6+
7+
- in `Ncring_tac`
8+
9+
+ Added extension-point typeclass `extra_reify` that is only resolved on
10+
non-variables for which built-in syntax-directed reification did not find a
11+
match
12+
(`#156 <https://github.com/coq/stdlib/pull/156>`_,
13+
by Andres Erbsen).
14+

‎doc/stdlib/index-list.html.template‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -323,6 +323,7 @@ through the <tt>From Stdlib Require Import</tt> command.</p>
323323
(theories/Zmod/ZmodBase.v)
324324
(theories/Zmod/ZstarBase.v)
325325
(theories/Zmod/ZmodInv.v)
326+
(theories/Zmod/ZmodNsatz.v)
326327
</dd>
327328

328329
<dt> <a name="unicode"></a><b>Unicode</b>:

‎test-suite/success/Nsatz.v‎

Lines changed: 31 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,5 @@
11
(* This file takes 9 seconds to process on a 2023 gaming computer *)
2-
From Stdlib Require Import List BinNat BinInt QArith_base Rbase RNsatz ZNsatz QNsatz.
3-
Import List.ListNotations.
2+
From Stdlib Require Import List BinNat ZArith Zdivisibility Zmod QArith Rbase RNsatz.
43

54
(* Example with a generic domain *)
65

@@ -15,6 +14,18 @@ Lemma example3_Z : forall (x y z : Z), (
1514
x*y*z=0 -> x*x*x=0)%Z.
1615
Proof. nsatz. Qed.
1716

17+
Lemma example3_Zmod3 : forall (x y z : Zmod 3), (
18+
x+y+z=0 ->
19+
x*y+x*z+y*z=0->
20+
x*y*z=0 -> x^3=0)%Zmod.
21+
Proof. nsatz. Qed.
22+
23+
Lemma example3_Zmodp : forall p (x y z : Zmod p), Z.prime p -> (
24+
x+y+z=0 ->
25+
x*y+x*z+y*z=0->
26+
x*y*z=0 -> x^3=0)%Zmod.
27+
Proof. nsatz. Qed.
28+
1829
Lemma example3_Q : forall (x y z : Q), (
1930
x+y+z==0 ->
2031
x*y+x*z+y*z==0->
@@ -27,6 +38,23 @@ Lemma example3_R : forall (x y z : R), (
2738
x*y*z=0 -> x*x*x=0)%R.
2839
Proof. nsatz. Qed.
2940

41+
Lemma example_contradiction_Zmod3 : forall (x : Zmod 3), (
42+
x = Zmod.of_Z _ 2 ->
43+
x = Zmod.of_Z _ 1 ->
44+
0 = 1 :> Zmod 3)%Zmod.
45+
Proof. nsatz. Qed.
46+
47+
Lemma example_contradiction_Zmodp : forall p (x : Zmod p), Z.prime p -> (
48+
x = Zmod.of_Z _ 2 ->
49+
x = Zmod.of_Z _ 1 ->
50+
0 = 1 :> Zmod p)%Zmod.
51+
Proof.
52+
intros.
53+
assert_succeeds (nsatz; []). (* (1+1)%Zmod is not converitble with (Zmod.of_Z p 2) *)
54+
pose proof @Zmod.of_Z_add p 1 1.
55+
nsatz.
56+
Qed.
57+
3058
Import Integral_domain Algebra_syntax.
3159

3260
Context {A:Type}`{Aid:Integral_domain A}.
@@ -64,7 +92,7 @@ Proof. nsatz. Qed.
6492
End test.
6593

6694
Section Geometry.
67-
Import Algebra_syntax.
95+
Import Algebra_syntax List.ListNotations.
6896
Local Open Scope R_scope.
6997
Local Coercion IZR : Z >-> R.
7098

‎theories/All/All.v‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -579,3 +579,4 @@ From Stdlib Require Export Zmod.Zstar.
579579
From Stdlib Require Export Zmod.ZstarDef.
580580
From Stdlib Require Export Zmod.ZstarBase.
581581
From Stdlib Require Export Zmod.Bits.
582+
From Stdlib Require Export Zmod.ZmodNsatz.

‎theories/Make.zmod‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -6,5 +6,6 @@ Zmod/ZmodInv.v
66
Zmod/Zstar.v
77
Zmod/ZstarBase.v
88
Zmod/ZstarDef.v
9+
Zmod/ZmodNsatz.v
910

1011
-Q Zmod Stdlib.Zmod

‎theories/Reals/RNsatz.v‎

Lines changed: 6 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -15,15 +15,13 @@ From Stdlib Require Import Raxioms RIneq DiscrR.
1515

1616
Ltac nsatz_internal_discrR ::= discrR.
1717

18-
Ltac Ncring_tac.extra_reify term ::=
19-
lazymatch term with
20-
| IZR ?z =>
21-
lazymatch isZcst z with
22-
| true => open_constr:(PEc z)
23-
| false => open_constr:(tt)
24-
end
25-
| _ => open_constr:(tt)
18+
Local Ltac extra_reify :=
19+
lazymatch goal with |- Ncring_tac.extra_reify _ (IZR ?z) =>
20+
lazymatch isZcst z with
21+
| true => exact (PEc z)
22+
end
2623
end.
24+
#[export] Hint Extern 1 (Ncring_tac.extra_reify _ _) => extra_reify : typeclass_instances.
2725

2826
#[export] Instance Rops: @Ring_ops R 0%R 1%R Rplus Rmult Rminus Ropp (@eq R) := {}.
2927

‎theories/ZArith/Zdivisibility.v‎

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -92,6 +92,7 @@ Proof. symmetry. apply coprime_pow_r; try symmetry; trivial. Qed.
9292

9393

9494
Definition prime p := 1 < p /\ forall n, 1 < n < p -> ~ (n|p).
95+
Existing Class prime.
9596

9697
Lemma not_prime_0 : not (prime 0).
9798
Proof. intros []. lia. Qed.
@@ -227,3 +228,6 @@ Proof. cbv [extgcd proj1_sig]. case extgcd_rec as (([],?),?). intuition congruen
227228
End extended_euclid_algorithm.
228229

229230
End Z.
231+
232+
#[export] Hint Extern 0 (Z.prime 2) => exact Z.prime_2 : typeclass_instances.
233+
#[export] Hint Extern 0 (Z.prime 3) => exact Z.prime_3 : typeclass_instances.

‎theories/Zmod/Zmod.v‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -3,3 +3,4 @@ From Stdlib Require Export ZArith ZModOffset Lia.
33
From Stdlib Require Export Zmod.ZmodDef.
44
From Stdlib Require Export Zmod.ZmodBase.
55
From Stdlib Require Export Zmod.ZmodInv.
6+
From Stdlib Require Export Zmod.ZmodNsatz.

‎theories/Zmod/ZmodDef.v‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -160,6 +160,8 @@ End bits.
160160
Declare Scope Zmod_scope.
161161
Delimit Scope Zmod_scope with Zmod.
162162
Bind Scope Zmod_scope with Zmod.
163+
Notation "0" := Zmod.zero : Zmod_scope.
164+
Notation "1" := Zmod.one : Zmod_scope.
163165
Infix "+" := Zmod.add : Zmod_scope.
164166
Infix "-" := Zmod.sub : Zmod_scope.
165167
Notation "- x" := (Zmod.opp x) : Zmod_scope.

‎theories/Zmod/ZmodNsatz.v‎

Lines changed: 59 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,59 @@
1+
Require Export (ltac.notations) NsatzTactic.
2+
3+
Require Import Zdivisibility Lia NsatzTactic.
4+
Require Import ZmodDef ZmodBase ZmodInv.
5+
6+
#[export]
7+
Instance Ring_ops_Zmod m : @Ring_ops (Zmod m) Zmod.zero Zmod.one Zmod.add Zmod.mul Zmod.sub Zmod.opp Logic.eq := {}.
8+
9+
#[export]
10+
Instance Ring_Zmod m : Ring (Ro:=Ring_ops_Zmod m).
11+
Proof.
12+
split.
13+
{ apply eq_equivalence. }
14+
1,2,3,4 : Morphisms.solve_proper.
15+
{ apply Zmod.add_0_l. }
16+
{ apply Zmod.add_comm. }
17+
{ apply Zmod.add_assoc. }
18+
{ apply Zmod.mul_1_l. }
19+
{ apply Zmod.mul_1_r. }
20+
{ apply Zmod.mul_assoc. }
21+
{ apply Zmod.mul_add_l. }
22+
{ intros ? ? ?. apply Zmod.mul_add_r. }
23+
{ symmetry; apply Zmod.add_opp_r. }
24+
{ apply Zmod.add_opp_same_r. }
25+
Qed.
26+
27+
#[export]
28+
Instance Cring_ZMod m : Cring (Rr:=Ring_Zmod m).
29+
Proof.
30+
cbv [Cring].
31+
apply Zmod.mul_comm.
32+
Qed.
33+
34+
#[export]
35+
Instance Integral_domain_Zmod m : Z.prime m -> Integral_domain (Rr:=Ring_Zmod m).
36+
Proof.
37+
intros H; split.
38+
{ apply Zmod.mul_0_iff_prime, H. }
39+
{ apply Zmod.one_neq_zero. pose proof Z.prime_ge_2 _ H. lia. }
40+
Qed.
41+
42+
Local Ltac extra_reify_of_Z :=
43+
lazymatch goal with |- Ncring_tac.extra_reify _ (@Zmod.of_Z ?m ?z) =>
44+
constr_eq true ltac:(isZcst m);
45+
constr_eq true ltac:(isZcst z);
46+
exact (PEc z)
47+
end.
48+
49+
Local Ltac extra_reify_pow_pos :=
50+
lazymatch goal with |- @Ncring_tac.extra_reify ?R ?ring0 ?ring1 ?add ?mul ?sub ?opp ?lvar (Zmod.pow ?t (Z.pos ?p)) =>
51+
constr_eq true ltac:(isPcst p);
52+
let et := Ncring_tac.reify_term R ring0 ring1 add mul sub opp lvar t in
53+
exact (PEpow et (BinNat.N.pos p))
54+
end.
55+
56+
#[export] Hint Extern 1 (Ncring_tac.extra_reify _ (Zmod.of_Z ?m ?z)) => extra_reify_of_Z : typeclass_instances.
57+
#[export] Hint Extern 1 (Ncring_tac.extra_reify _ (Zmod.pow _ (Z.pos _))) => extra_reify_pow_pos : typeclass_instances.
58+
#[export] Hint Extern 1 (Ncring_tac.extra_reify _ (Zmod.pow _ Z0)) => exact (PEc 0%Z) : typeclass_instances.
59+
(* [Zmod.pow _ (Z.neg) = Zmod.inv (Zmod.pow _ _)] can't be reified directly *)

0 commit comments

Comments
 (0)