## Stream: math-comp users

### Topic: field/nsatz tactic with ZmodP

#### Jan Spakula (Apr 20 2022 at 07:34):

Probably a very beginner question... I am trying to get to the point when I can use the 'field' and 'nsatz' tactics from coq in Z/(p) fields. I think I need to add a new field structure for that. Most of the axioms for that are readily available in `zmodp`, except "1≠0" and multiplicative inverses.
But I can't even prove that "1≠0" in a concrete `'F_3`, let alone `'F_p`; I think I am missing something rather basic.

``````From mathcomp Require Import ssreflect.
From mathcomp Require Import zmodp.

Lemma F3_nontrivial : Zp1 <> Zp0 :> 'F_3.
Proof.
have H: Zp1 <> (@inZp 2 0).
apply (@Zp_nontrivial 2).
Abort.

Lemma F3_inverses (x : 'F_3) : x <> Zp0 -> Zp_mul (Zp_inv x) x = Zp1.
Proof.
``````

Any pointers would be appreciated!

#### Karl Palmskog (Apr 20 2022 at 07:36):

`field` will not work out of the box with MathComp, see instead: https://github.com/math-comp/algebra-tactics

#### Jan Spakula (Apr 20 2022 at 07:44):

Thank you; but that would mean no `nsatz` which is another one I would like to use.
Do I understand correctly that even with proving the Lemmas like above, then defining a `field_theory`, and finally using `Add Field` would not make Z/p from MathComp available to `nsatz`?

#### Kazuhiko Sakaguchi (Apr 20 2022 at 07:51):

1 != 0 holds for any `ringType` in MathComp https://math-comp.github.io/htmldoc/mathcomp.algebra.ssralg.html#GRing.oner_neq0

#### Pierre Roux (Apr 20 2022 at 07:55):

FYI, there is a support for nsatz in Analysis https://github.com/math-comp/analysis/blob/master/theories/nsatz_realtype.v although it is for realType

#### Kazuhiko Sakaguchi (Apr 20 2022 at 07:56):

I never used zmodp seriously, but its header documentation says that:

Note that while 'I_n.+1 has canonical finZmodType and finGroupType structures, only 'I_n.+2 has a canonical ring structure (it has, in fact, a canonical finComUnitRing structure), and hence an associated multiplicative unit finGroupType.

https://math-comp.github.io/htmldoc/mathcomp.algebra.zmodp.html

#### Kazuhiko Sakaguchi (Apr 20 2022 at 07:58):

I think that the field tactic of Algebra Tactics does not automatically find the witness that `p` in `'I_p` is a prime number, and thus does not work... (not tested)

#### Jan Spakula (Apr 20 2022 at 07:59):

Pierre Roux said:

FYI, there is a support for nsatz in Analysis https://github.com/math-comp/analysis/blob/master/theories/nsatz_realtype.v although it is for realType

Yes, I am trying to achieve something like this for Z/p. Thank you for pointing this out!

#### Jan Spakula (Apr 20 2022 at 11:56):

Well - I managed to do `Add Field` for `'F_3`, and the `field` tactic still does not work. I do not understand why, but presumably this is not a way to go. On jscoq/hastebin.
I will study the resources you pointed out (nsatz in Analysis, and algebra-tactics) and try it that way. Thank you for your help!

#### Kazuhiko Sakaguchi (Apr 20 2022 at 12:03):

the `field` tactic still does not work. I do not understand why,

If you need to know the reason, Section 3.1 of this paper explains it: https://arxiv.org/pdf/2202.04330.pdf

#### Jan Spakula (Apr 20 2022 at 13:09):

Kazuhiko Sakaguchi said:

I think that the field tactic of Algebra Tactics does not automatically find the witness that `p` in `'I_p` is a prime number, and thus does not work... (not tested)

Seems to actually work for me?

``````From mathcomp Require Import all_ssreflect all_algebra zmodp ring.
Local Open Scope ring_scope.
Variable p : nat.
Hypothesis p_pr : prime p.
Lemma foo5: forall (x y : 'F_p), y != 0 -> y = x -> x / y = 1.
Proof. move=> x y y_neq0. by field. Qed.
``````

#### Kazuhiko Sakaguchi (Apr 20 2022 at 13:21):

Aha, that's good news! I just didn't know what `'F_p` notation does.

#### Laurent Théry (Apr 20 2022 at 18:45):

Very good this works, just two remarks:

• you don't need this asssumpion
``````Hypothesis p_pr : prime p.
``````

`'F_p` always builds a field, it takes the first prime divisor of `p` or 2.

• the `ring` and `field` are connected 'generically'. for `'F_p` so it can be used to prove generic statement but this will not prove `forall x: 'F_2, x + x = 0`. It is possible (this is called customized ring) but this is not available at the moment.

Last updated: Jul 23 2024 at 20:01 UTC