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.
Admitted.
```

Any pointers would be appreciated!

`field`

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

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`

?

1 != 0 holds for any `ringType`

in MathComp https://math-comp.github.io/htmldoc/mathcomp.algebra.ssralg.html#GRing.oner_neq0

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

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

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)

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!

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!

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

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.
```

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

notation does.

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