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:
Hypothesis p_pr : prime p.
'F_p
always builds a field, it takes the first prime divisor of p
or 2.
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: Mar 29 2024 at 12:02 UTC