Stream: math-comp users

Topic: field/nsatz tactic with ZmodP


view this post on Zulip 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.
Admitted.

Any pointers would be appreciated!

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip 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!

view this post on Zulip 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!

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Kazuhiko Sakaguchi (Apr 20 2022 at 13:21):

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

view this post on Zulip Laurent Théry (Apr 20 2022 at 18:45):

Very good this works, just two remarks:

Hypothesis p_pr : prime p.

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


Last updated: Jan 29 2023 at 18:03 UTC