Library mathcomp.algebra.zmodp
+ +
+(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.
+ Distributed under the terms of CeCILL-B. *)
+Require Import mathcomp.ssreflect.ssreflect.
+ +
+
+
++ Distributed under the terms of CeCILL-B. *)
+Require Import mathcomp.ssreflect.ssreflect.
+ +
+
+ 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
+ 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}
+
+
+
+
+
+ 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
+
+
+Definition Zp0 : 'I_p := ord0.
+Definition Zp1 := inZp 1.
+Definition Zp_opp x := inZp (p - x).
+Definition Zp_add x y := inZp (x + y).
+Definition Zp_mul x y := inZp (x × y).
+Definition Zp_inv x := if coprime p x then inZp (egcdn x p).1 else x.
+ +
+
+
++Definition Zp1 := inZp 1.
+Definition Zp_opp x := inZp (p - x).
+Definition Zp_add x y := inZp (x + y).
+Definition Zp_mul x y := inZp (x × y).
+Definition Zp_inv x := if coprime p x then inZp (egcdn x p).1 else x.
+ +
+
+ Additive group structure.
+
+
+
+
+Lemma Zp_add0z : left_id Zp0 Zp_add.
+ +
+Lemma Zp_addNz : left_inverse Zp0 Zp_opp Zp_add.
+ +
+Lemma Zp_addA : associative Zp_add.
+ +
+Lemma Zp_addC : commutative Zp_add.
+ +
+Definition Zp_zmodMixin := ZmodMixin Zp_addA Zp_addC Zp_add0z Zp_addNz.
+Canonical Zp_zmodType := Eval hnf in ZmodType 'I_p Zp_zmodMixin.
+Canonical Zp_finZmodType := Eval hnf in [finZmodType of 'I_p].
+Canonical Zp_baseFinGroupType := Eval hnf in [baseFinGroupType of 'I_p for +%R].
+Canonical Zp_finGroupType := Eval hnf in [finGroupType of 'I_p for +%R].
+ +
+
+
++Lemma Zp_add0z : left_id Zp0 Zp_add.
+ +
+Lemma Zp_addNz : left_inverse Zp0 Zp_opp Zp_add.
+ +
+Lemma Zp_addA : associative Zp_add.
+ +
+Lemma Zp_addC : commutative Zp_add.
+ +
+Definition Zp_zmodMixin := ZmodMixin Zp_addA Zp_addC Zp_add0z Zp_addNz.
+Canonical Zp_zmodType := Eval hnf in ZmodType 'I_p Zp_zmodMixin.
+Canonical Zp_finZmodType := Eval hnf in [finZmodType of 'I_p].
+Canonical Zp_baseFinGroupType := Eval hnf in [baseFinGroupType of 'I_p for +%R].
+Canonical Zp_finGroupType := Eval hnf in [finGroupType of 'I_p for +%R].
+ +
+
+ Ring operations
+
+
+
+
+Lemma Zp_mul1z : left_id Zp1 Zp_mul.
+ +
+Lemma Zp_mulC : commutative Zp_mul.
+ +
+Lemma Zp_mulz1 : right_id Zp1 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_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_inv_out x : ~~ coprime p x → Zp_inv x = 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.
+ +
+ +
+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 big_ord1 R idx (op : @Monoid.law R idx) F :
+ \big[op/idx]_(i < 1) F i = F 0.
+ +
+Lemma big_ord1_cond R idx (op : @Monoid.law R idx) P F :
+ \big[op/idx]_(i < 1 | P i) F i = if P 0 then F 0 else idx.
+ +
+Section ZpRing.
+ +
+Variable p' : nat.
+ +
+Lemma Zp_nontrivial : Zp1 != 0 :> 'I_p.
+ +
+Definition Zp_ringMixin :=
+ ComRingMixin (@Zp_mulA _) (@Zp_mulC _) (@Zp_mul1z _) (@Zp_mul_addl _)
+ Zp_nontrivial.
+Canonical Zp_ringType := Eval hnf in RingType 'I_p Zp_ringMixin.
+Canonical Zp_finRingType := Eval hnf in [finRingType of 'I_p].
+Canonical Zp_comRingType := Eval hnf in ComRingType 'I_p (@Zp_mulC _).
+Canonical Zp_finComRingType := Eval hnf in [finComRingType of 'I_p].
+ +
+Definition Zp_unitRingMixin :=
+ ComUnitRingMixin (@Zp_mulVz _) (@Zp_intro_unit _) (@Zp_inv_out _).
+Canonical Zp_unitRingType := Eval hnf in UnitRingType 'I_p Zp_unitRingMixin.
+Canonical Zp_finUnitRingType := Eval hnf in [finUnitRingType of 'I_p].
+Canonical Zp_comUnitRingType := Eval hnf in [comUnitRingType of 'I_p].
+Canonical Zp_finComUnitRingType := Eval hnf in [finComUnitRingType of '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.
+ +
+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.
+ 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 Zp_mul1z : left_id Zp1 Zp_mul.
+ +
+Lemma Zp_mulC : commutative Zp_mul.
+ +
+Lemma Zp_mulz1 : right_id Zp1 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_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_inv_out x : ~~ coprime p x → Zp_inv x = 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.
+ +
+ +
+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 big_ord1 R idx (op : @Monoid.law R idx) F :
+ \big[op/idx]_(i < 1) F i = F 0.
+ +
+Lemma big_ord1_cond R idx (op : @Monoid.law R idx) P F :
+ \big[op/idx]_(i < 1 | P i) F i = if P 0 then F 0 else idx.
+ +
+Section ZpRing.
+ +
+Variable p' : nat.
+ +
+Lemma Zp_nontrivial : Zp1 != 0 :> 'I_p.
+ +
+Definition Zp_ringMixin :=
+ ComRingMixin (@Zp_mulA _) (@Zp_mulC _) (@Zp_mul1z _) (@Zp_mul_addl _)
+ Zp_nontrivial.
+Canonical Zp_ringType := Eval hnf in RingType 'I_p Zp_ringMixin.
+Canonical Zp_finRingType := Eval hnf in [finRingType of 'I_p].
+Canonical Zp_comRingType := Eval hnf in ComRingType 'I_p (@Zp_mulC _).
+Canonical Zp_finComRingType := Eval hnf in [finComRingType of 'I_p].
+ +
+Definition Zp_unitRingMixin :=
+ ComUnitRingMixin (@Zp_mulVz _) (@Zp_intro_unit _) (@Zp_inv_out _).
+Canonical Zp_unitRingType := Eval hnf in UnitRingType 'I_p Zp_unitRingMixin.
+Canonical Zp_finUnitRingType := Eval hnf in [finUnitRingType of 'I_p].
+Canonical Zp_comUnitRingType := Eval hnf in [comUnitRingType of 'I_p].
+Canonical Zp_finComUnitRingType := Eval hnf in [finComUnitRingType of '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.
+ +
+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.
+ 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.
+ +
+
+ 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)).+2 = (Zp_trunc p).+2.
+ +
+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.Field.mixin_of [the unitRingType of 'F_p].
+ +
+Definition Fp_idomainMixin := FieldIdomainMixin Fp_fieldMixin.
+ +
+Canonical Fp_idomainType := Eval hnf in IdomainType 'F_p Fp_idomainMixin.
+Canonical Fp_finIdomainType := Eval hnf in [finIdomainType of 'F_p].
+Canonical Fp_fieldType := Eval hnf in FieldType 'F_p Fp_fieldMixin.
+Canonical Fp_finFieldType := Eval hnf in [finFieldType of 'F_p].
+Canonical Fp_decFieldType :=
+ Eval hnf in [decFieldType of 'F_p for Fp_finFieldType].
+ +
+End PrimeField.
+
++Section PrimeField.
+ +
+Open Scope ring_scope.
+ +
+Variable p : nat.
+ +
+Section F_prime.
+ +
+Hypothesis p_pr : prime p.
+ +
+Lemma Fp_Zcast : (Zp_trunc (pdiv p)).+2 = (Zp_trunc p).+2.
+ +
+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.Field.mixin_of [the unitRingType of 'F_p].
+ +
+Definition Fp_idomainMixin := FieldIdomainMixin Fp_fieldMixin.
+ +
+Canonical Fp_idomainType := Eval hnf in IdomainType 'F_p Fp_idomainMixin.
+Canonical Fp_finIdomainType := Eval hnf in [finIdomainType of 'F_p].
+Canonical Fp_fieldType := Eval hnf in FieldType 'F_p Fp_fieldMixin.
+Canonical Fp_finFieldType := Eval hnf in [finFieldType of 'F_p].
+Canonical Fp_decFieldType :=
+ Eval hnf in [decFieldType of 'F_p for Fp_finFieldType].
+ +
+End PrimeField.
+