Library mathcomp.algebra.zmodp
(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.
Distributed under the terms of CeCILL-B. *)
From HB Require Import structures.
From mathcomp Require Import ssreflect ssrfun ssrbool choice eqtype ssrnat seq div.
From mathcomp Require Import fintype bigop finset prime fingroup.
From mathcomp Require Import ssralg finalg countalg.
Distributed under the terms of CeCILL-B. *)
From HB Require Import structures.
From mathcomp Require Import ssreflect ssrfun ssrbool choice eqtype ssrnat seq div.
From mathcomp Require Import fintype bigop finset prime fingroup.
From mathcomp Require Import ssralg finalg countalg.
Definition of the additive group and ring Zp, represented as 'I_p
Definitions:
From fintype.v:
'I_p == the subtype of integers less than p, taken here as the type of
the integers mod p.
This file:
inZp == the natural projection from nat into the integers mod p,
represented as 'I_p. Here p is implicit, but MUST be of the
form n.+1.
The operations:
Zp0 == the identity element for addition
Zp1 == the identity element for multiplication, and a generator of
additive group
Zp_opp == inverse function for addition
Zp_add == addition
Zp_mul == multiplication
Zp_inv == inverse function for multiplication
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. To mitigate the issues caused by the
trivial "ring" (which is, indeed is NOT a ring in the ssralg/finalg
formalization), we define additional notation:
'Z_p == the type of integers mod (max p 2); this is always a proper
ring, by constructions. Note that 'Z_p is provably equal to
'I_p if p > 1, and convertible to 'I_p if p is of the form
n.+2.
Zp p == the subgroup of integers mod (max p 1) in 'Z_p; this is thus
all of 'Z_p if p > 1, and else the trivial group.
units_Zp p == the group of all units of 'Z_p -- i.e., the group of
(multiplicative) automorphisms of Zp p.
We show that Zp and units_Zp are abelian, and compute their orders.
We use a similar technique to represent the prime fields:
'F_p == the finite field of integers mod the first prime divisor of
maxn p 2. This is provably equal to 'Z_p and 'I_p if p is
provably prime, and indeed convertible to the above if p is
a concrete prime such as 2, 5 or 23.
Note finally that due to the canonical structures it is possible to use
0%R instead of Zp0, and 1%R instead of Zp1 (for the latter, p must be of
the form n.+2, and 1%R : nat will simplify to 1%N).
Mod p arithmetic on the finite set {0, 1, 2, ..., p - 1}
Operations on 'I_p without constraint on p.
Section Generic.
Variable p : nat.
Implicit Types i j : 'I_p.
Lemma Zp_opp_subproof i : (p - i) %% p < p.
Definition Zp_opp i := Ordinal (Zp_opp_subproof i).
Lemma Zp_add_subproof i j : (i + j) %% p < p.
Definition Zp_add i j := Ordinal (Zp_add_subproof i j).
Lemma Zp_mul_subproof i j : (i × j) %% p < p.
Definition Zp_mul i j := Ordinal (Zp_mul_subproof i j).
Lemma Zp_inv_subproof i : (egcdn i p).1 %% p < p.
Definition Zp_inv i := if coprime p i then Ordinal (Zp_inv_subproof i) else i.
Lemma Zp_addA : associative Zp_add.
Lemma Zp_addC : commutative Zp_add.
Lemma Zp_mulC : commutative Zp_mul.
Lemma Zp_mulA : associative Zp_mul.
Lemma Zp_mul_addr : right_distributive Zp_mul Zp_add.
Lemma Zp_mul_addl : left_distributive Zp_mul Zp_add.
Lemma Zp_inv_out i : ~~ coprime p i → Zp_inv i = i.
End Generic.
Arguments Zp_opp {p}.
Arguments Zp_add {p}.
Arguments Zp_mul {p}.
Arguments Zp_inv {p}.
Variable p' : nat.
Local Notation p := p'.+1.
Implicit Types x y z : 'I_p.
Variable p : nat.
Implicit Types i j : 'I_p.
Lemma Zp_opp_subproof i : (p - i) %% p < p.
Definition Zp_opp i := Ordinal (Zp_opp_subproof i).
Lemma Zp_add_subproof i j : (i + j) %% p < p.
Definition Zp_add i j := Ordinal (Zp_add_subproof i j).
Lemma Zp_mul_subproof i j : (i × j) %% p < p.
Definition Zp_mul i j := Ordinal (Zp_mul_subproof i j).
Lemma Zp_inv_subproof i : (egcdn i p).1 %% p < p.
Definition Zp_inv i := if coprime p i then Ordinal (Zp_inv_subproof i) else i.
Lemma Zp_addA : associative Zp_add.
Lemma Zp_addC : commutative Zp_add.
Lemma Zp_mulC : commutative Zp_mul.
Lemma Zp_mulA : associative Zp_mul.
Lemma Zp_mul_addr : right_distributive Zp_mul Zp_add.
Lemma Zp_mul_addl : left_distributive Zp_mul Zp_add.
Lemma Zp_inv_out i : ~~ coprime p i → Zp_inv i = i.
End Generic.
Arguments Zp_opp {p}.
Arguments Zp_add {p}.
Arguments Zp_mul {p}.
Arguments Zp_inv {p}.
Variable p' : nat.
Local Notation p := p'.+1.
Implicit Types x y z : 'I_p.
Standard injection; val (inZp i) = i %% p
Definition inZp i := Ordinal (ltn_pmod i (ltn0Sn p')).
Lemma modZp x : x %% p = x.
Lemma valZpK x : inZp x = x.
Lemma modZp x : x %% p = x.
Lemma valZpK x : inZp x = x.
Operations
Additive group structure.
Ring operations
Lemma Zp_mul1z : left_id Zp1 Zp_mul.
Lemma Zp_mulz1 : right_id Zp1 Zp_mul.
Lemma Zp_mulVz x : coprime p x → Zp_mul (Zp_inv x) x = Zp1.
Lemma Zp_mulzV x : coprime p x → Zp_mul x (Zp_inv x) = Zp1.
Lemma Zp_intro_unit x y : Zp_mul y x = Zp1 → coprime p x.
Lemma Zp_mulrn x n : x *+ n = inZp (x × n).
Import GroupScope.
Lemma Zp_mulgC : @commutative 'I_p _ mulg.
Lemma Zp_abelian : abelian [set: 'I_p].
Lemma Zp_expg x n : x ^+ n = inZp (x × n).
Lemma Zp1_expgz x : Zp1 ^+ x = x.
Lemma Zp_cycle : setT = <[Zp1]>.
Lemma order_Zp1 : #[Zp1] = p.
End ZpDef.
Arguments Zp0 {p'}.
Arguments Zp1 {p'}.
Arguments inZp {p'} i.
Arguments valZpK {p'} x.
We redefine fintype.ord1 to specialize it with 0 instead of ord0
since 'I_n is now canonically a zmodType
Lemma ord1 : all_equal_to (0 : 'I_1).
Lemma lshift0 m n : lshift m (0 : 'I_n.+1) = (0 : 'I_(n + m).+1).
Lemma rshift1 n : @rshift 1 n =1 lift (0 : 'I_n.+1).
Lemma split1 n i :
split (i : 'I_(1 + n)) = oapp (@inr _ _) (inl _ 0) (unlift 0 i).
Lemma lshift0 m n : lshift m (0 : 'I_n.+1) = (0 : 'I_(n + m).+1).
Lemma rshift1 n : @rshift 1 n =1 lift (0 : 'I_n.+1).
Lemma split1 n i :
split (i : 'I_(1 + n)) = oapp (@inr _ _) (inl _ 0) (unlift 0 i).
TODO: bigop is imported after zmodp in matrix.v and intdiv.v to prevent
these warnings from triggering. We should restore the order of imports when
these are removed.
#[deprecated(since="mathcomp 2.3.0", note="Use bigop.big_ord1 instead.")]
Notation big_ord1 := big_ord1 (only parsing).
#[deprecated(since="mathcomp 2.3.0", note="Use bigop.big_ord1_cond instead.")]
Notation big_ord1_cond := big_ord1_cond (only parsing).
Section ZpRing.
Variable p' : nat.
Local Notation p := p'.+2.
Lemma Zp_nontrivial : Zp1 != 0 :> 'I_p.
Lemma Zp_nat n : n%:R = inZp n :> 'I_p.
Lemma natr_Zp (x : 'I_p) : x%:R = x.
Lemma natr_negZp (x : 'I_p) : (- x)%:R = - x.
Import GroupScope.
Lemma unit_Zp_mulgC : @commutative {unit 'I_p} _ mulg.
Lemma unit_Zp_expg (u : {unit 'I_p}) n :
val (u ^+ n) = inZp (val u ^ n) :> 'I_p.
End ZpRing.
Definition Zp_trunc p := p.-2.
Notation "''Z_' p" := 'I_(Zp_trunc p).+2
(at level 8, p at level 2, format "''Z_' p") : type_scope.
Notation "''F_' p" := 'Z_(pdiv p)
(at level 8, p at level 2, format "''F_' p") : type_scope.
Arguments natr_Zp {p'} x.
Section ZpRing.
Import GRing.Theory.
Lemma add_1_Zp p (x : 'Z_p) : 1 + x = ordS x.
Lemma add_Zp_1 p (x : 'Z_p) : x + 1 = ordS x.
Lemma sub_Zp_1 p (x : 'Z_p) : x - 1 = ord_pred x.
Lemma add_N1_Zp p (x : 'Z_p) : -1 + x = ord_pred x.
End ZpRing.
Section Groups.
Variable p : nat.
Definition Zp := if p > 1 then [set: 'Z_p] else 1%g.
Definition units_Zp := [set: {unit 'Z_p}].
Lemma Zp_cast : p > 1 → (Zp_trunc p).+2 = p.
Lemma val_Zp_nat (p_gt1 : p > 1) n : (n%:R : 'Z_p) = (n %% p)%N :> nat.
Lemma Zp_nat_mod (p_gt1 : p > 1)m : (m %% p)%:R = m%:R :> 'Z_p.
Lemma char_Zp : p > 1 → p%:R = 0 :> 'Z_p.
Lemma unitZpE x : p > 1 → ((x%:R : 'Z_p) \is a GRing.unit) = coprime p x.
Lemma Zp_group_set : group_set Zp.
Notation big_ord1 := big_ord1 (only parsing).
#[deprecated(since="mathcomp 2.3.0", note="Use bigop.big_ord1_cond instead.")]
Notation big_ord1_cond := big_ord1_cond (only parsing).
Section ZpRing.
Variable p' : nat.
Local Notation p := p'.+2.
Lemma Zp_nontrivial : Zp1 != 0 :> 'I_p.
Lemma Zp_nat n : n%:R = inZp n :> 'I_p.
Lemma natr_Zp (x : 'I_p) : x%:R = x.
Lemma natr_negZp (x : 'I_p) : (- x)%:R = - x.
Import GroupScope.
Lemma unit_Zp_mulgC : @commutative {unit 'I_p} _ mulg.
Lemma unit_Zp_expg (u : {unit 'I_p}) n :
val (u ^+ n) = inZp (val u ^ n) :> 'I_p.
End ZpRing.
Definition Zp_trunc p := p.-2.
Notation "''Z_' p" := 'I_(Zp_trunc p).+2
(at level 8, p at level 2, format "''Z_' p") : type_scope.
Notation "''F_' p" := 'Z_(pdiv p)
(at level 8, p at level 2, format "''F_' p") : type_scope.
Arguments natr_Zp {p'} x.
Section ZpRing.
Import GRing.Theory.
Lemma add_1_Zp p (x : 'Z_p) : 1 + x = ordS x.
Lemma add_Zp_1 p (x : 'Z_p) : x + 1 = ordS x.
Lemma sub_Zp_1 p (x : 'Z_p) : x - 1 = ord_pred x.
Lemma add_N1_Zp p (x : 'Z_p) : -1 + x = ord_pred x.
End ZpRing.
Section Groups.
Variable p : nat.
Definition Zp := if p > 1 then [set: 'Z_p] else 1%g.
Definition units_Zp := [set: {unit 'Z_p}].
Lemma Zp_cast : p > 1 → (Zp_trunc p).+2 = p.
Lemma val_Zp_nat (p_gt1 : p > 1) n : (n%:R : 'Z_p) = (n %% p)%N :> nat.
Lemma Zp_nat_mod (p_gt1 : p > 1)m : (m %% p)%:R = m%:R :> 'Z_p.
Lemma char_Zp : p > 1 → p%:R = 0 :> 'Z_p.
Lemma unitZpE x : p > 1 → ((x%:R : 'Z_p) \is a GRing.unit) = coprime p x.
Lemma Zp_group_set : group_set Zp.
FIX ME : is this ok something similar is done in fingroup
Canonical Zp_group := Group Zp_group_set.
Lemma card_Zp : p > 0 → #|Zp| = p.
Lemma mem_Zp x : p > 1 → x \in Zp.
Canonical units_Zp_group := [group of units_Zp].
Lemma card_units_Zp : p > 0 → #|units_Zp| = totient p.
Lemma units_Zp_abelian : abelian units_Zp.
End Groups.
Lemma card_Zp : p > 0 → #|Zp| = p.
Lemma mem_Zp x : p > 1 → x \in Zp.
Canonical units_Zp_group := [group of units_Zp].
Lemma card_units_Zp : p > 0 → #|units_Zp| = totient p.
Lemma units_Zp_abelian : abelian units_Zp.
End Groups.
Field structure for primes.
Section PrimeField.
Open Scope ring_scope.
Variable p : nat.
Section F_prime.
Hypothesis p_pr : prime p.
Lemma Fp_Zcast : Zp_trunc (pdiv p) = Zp_trunc p.
Lemma Fp_cast : (Zp_trunc (pdiv p)).+2 = p.
Lemma card_Fp : #|'F_p| = p.
Lemma val_Fp_nat n : (n%:R : 'F_p) = (n %% p)%N :> nat.
Lemma Fp_nat_mod m : (m %% p)%:R = m%:R :> 'F_p.
Lemma char_Fp : p \in [char 'F_p].
Lemma char_Fp_0 : p%:R = 0 :> 'F_p.
Lemma unitFpE x : ((x%:R : 'F_p) \is a GRing.unit) = coprime p x.
End F_prime.
Lemma Fp_fieldMixin : GRing.ComUnitRing_isField 'F_p.
End PrimeField.