Library Stdlib.Zmod.ZstarBase

From Stdlib Require Import ZArith ZModOffset Zcong Lia Zdivisibility.
From Stdlib Require Import Bool.Bool Lists.List Lists.Finite Sorting.Permutation.
Import ListNotations.

From Stdlib Require Import Zmod.ZmodDef Zmod.ZmodBase Zmod.ZstarDef.
#[local] Open Scope Z_scope.
#[local] Coercion ZmodDef.Zmod.to_Z : Zmod >-> Z.
#[local] Coercion Zstar.to_Zmod : Zstar.Zstar >-> Zmod.Zmod.

#[local] Hint Extern 0 (?x <-> ?x) => reflexivity : core.

Module Zstar.
Import ZmodDef.Zmod ZmodBase.Zmod ZstarDef.Zstar.

Lemma coprime_to_Zmod [m] (a : Zstar m) : Z.coprime (to_Zmod a) m.
Notation to_Zmod_range := coprime_to_Zmod (only parsing).

Lemma to_Zmod_inj [m] (x y : Zstar m) : to_Zmod x = to_Zmod y -> x = y.

Lemma to_Zmod_inj_iff [m] (x y : Zstar m) : to_Zmod x = to_Zmod y <-> x = y.

Lemma to_Zmod_of_coprime_Zmod [m] (x : Zmod m) pf : to_Zmod (of_coprime_Zmod_dep x pf) = x.

Lemma to_Zmod_of_Zmod' [m] (x : Zmod m) :
  to_Zmod (of_Zmod x) = if Z.eqb (Z.gcd x m) 1 then x else Zmod.one.

Lemma to_Zmod_of_Zmod [m] (x : Zmod m) (H : Z.coprime x m) : to_Zmod (of_Zmod x) = x.

Lemma of_Zmod_to_Zmod [m] x : @of_Zmod m (to_Zmod x) = x.

Lemma to_Zmod_1 m : @to_Zmod m one = Zmod.one.

Lemma of_Zmod_inj [m] (x y : Zmod m) :
  Z.coprime x m -> Z.coprime y m -> of_Zmod x = of_Zmod y -> x = y.

Lemma to_Zmod_0_iff [m] (a : Zstar m) : to_Zmod a = zero <-> Z.abs m = 1.

Lemma to_Zmod_nz [m] (a : Zstar m) (Hm : 2 <= m) : to_Zmod a <> zero.

Lemma eqb_spec [m] (x y : Zstar m) : BoolSpec (x = y) (x <> y) (eqb x y).

Lemma eqb_eq [m] (x y : Zstar m) : eqb x y = true <-> x = y.

Lemma eqb_refl [m] (x : Zstar m) : eqb x x = true.

Lemma hprop_Zstar_1 (a b : Zstar 1) : a = b.

Lemma hprop_Zstar_2 (a b : Zstar 2) : a = b.

Lemma wlog_eq_Zstar_3_pos [m] (a b : Zstar m) (Hm : 0 < m) (k : 3 <= m -> a = b) : a = b.
Lemma of_Zmod_1 m : @of_Zmod m Zmod.one = one.

Lemma to_Z_0_iff [m] (a : Zstar m) : to_Z a = 0 <-> Z.abs m = 1.

Lemma to_Z_nz_iff [m] (a : Zstar m) : to_Z a <> 0 <-> Z.abs m <> 1.

Lemma to_Z_nz [m] (a : Zstar m) : Z.abs m <> 1 -> to_Z a <> 0.

Lemma to_Zmod_opp [m] (a : Zstar m) : to_Zmod (opp a) = Zmod.opp a.

Lemma opp_opp [m] (a : Zstar m) : opp (opp a) = a.

Lemma opp_inj [m] (a b : Zstar m) : opp a = opp b -> a = b.

Lemma opp_distinct_odd [m] (Hm : m mod 2 = 1) (Hm' : 3 <= m) a :
  a <> opp a :> Zstar m.

Lemma opp_1_neq_1 [m] (Hm : 3 <= Z.abs m) : opp one <> one :> Zstar m.

Lemma to_Zmod_abs [m] (a : Zstar m) : to_Zmod (abs a) = Zmod.abs a.

Lemma abs_1 m : @abs m one = one.

Lemma abs_nonneg [m] (x : Zstar m) : 0 <= @signed m x -> abs x = x.

Lemma abs_neg [m] (x : Zstar m) : @signed m x < 0 -> abs x = opp x.

Lemma abs_pos [m] (x : Zstar m) : 0 < @signed m x -> abs x = x.

Lemma abs_opp [m] x : @abs m (opp x) = abs x.

Lemma abs_abs [m] (x : Zstar m) : abs (abs x) = abs x.

Lemma abs_overflow [m] (Hm : m mod 2 = 0)
  (x : Zstar m) (Hx : signed x = -m/2) : abs x = x.

Lemma to_Zmod_mul [m] (a b : Zstar m) : @to_Zmod m (mul a b) = Zmod.mul a b.

Lemma of_Zmod_mul [m] (a b : Zmod m) (Ha : Z.coprime a m) (Hb : Z.coprime b m) :
  @of_Zmod m (Zmod.mul a b) = mul (of_Zmod a) (of_Zmod b).

Lemma mul_assoc [m] a b c : @mul m a (mul b c) = mul (mul a b) c.
Lemma mul_comm [m] a b : @mul m a b = mul b a.
Lemma mul_1_l [m] a : @mul m one a = a. Lemma mul_1_r [m] a : @mul m a one = a.
Lemma mul_m1_l [m] a : @mul m (opp one) a = opp a.
Lemma mul_m1_r [m] a : @mul m a (opp one) = opp a.

Lemma mul_opp_l [m] (a b : Zstar m) : mul (opp a) b = opp (mul a b).
Lemma mul_opp_r [m] (a b : Zstar m) : mul a (opp b) = opp (mul a b).
Lemma mul_opp_opp [m] a b : @mul m (opp a) (opp b) = mul a b.

Lemma abs_mul_abs_l [m] (x y : Zstar m) : abs (mul (abs x) y) = abs (mul x y).

Lemma abs_mul_abs_r [m] (x y : Zstar m) : abs (mul x (abs y)) = abs (mul x y).

Lemma abs_mul_abs_abs [m] (x y : Zstar m) : abs (mul (abs x) (abs y)) = abs (mul x y).

Lemma to_Zmod_inv [m] x : to_Zmod (@inv m x) = Zmod.inv x.

Lemma not_of_Zmod_inv (m := 6) (x := Zmod.of_Z _ 4) : of_Zmod (@Zmod.inv m x) <> inv (of_Zmod x).

Lemma to_Zmod_div [m] x y : to_Zmod (@div m x y) = Zmod.mdiv x y.

Lemma mul_inv_l [m] x y : mul (@inv m y) x = div x y.

Lemma mul_inv_r [m] x y : mul x (@inv m y) = div x y.

Lemma div_same [m] (a : Zstar m) : div a a = one.

Lemma div_mul_l [m] (a b c : Zstar m) : div (mul a b) c = mul a (div b c).

Lemma mul_inv_same_l [m] x : mul (@inv m x) x = one.

Lemma mul_inv_same_r [m] x : mul x (@inv m x) = one.

Lemma inv_inv [m] x : inv (@inv m x) = x.

Lemma inv_1 m : @inv m one = one.

Lemma div_1_r [m] x : @div m x one = x.

Lemma mul_cancel_l [m] (a b c : Zstar m) (H : mul a b = mul a c) : b = c.

Lemma mul_cancel_l_iff [m] (a b c : Zstar m) : mul a b = mul a c <-> b = c.

Lemma mul_cancel_r [m] (a b c : Zstar m) (H : mul b a = mul c a) : b = c.

Lemma mul_cancel_r_iff [m] (a b c : Zstar m) : mul b a = mul c a <-> b = c.

Lemma mul_div_r_same_r [m] (a b : Zstar m) : mul a (div b a) = b.

Lemma inv_mul [m] (a b : Zstar m) : inv (mul a b) = mul (inv a) (inv b).

Lemma div_div_r_same [m] (a b : Zstar m) : div a (div a b) = b.

Lemma inv_div [m] (x y : Zstar m) : inv (div x y) = div y x.

Lemma eq_inv_iff [m] (x y : Zstar m) : inv x = y <-> mul x y = one.

Lemma inv_opp [m] (x : Zstar m) : inv (opp x) = opp (inv x).

Lemma prod_nil m : prod [] = @one m.

Lemma prod_cons [m] (x : Zstar m) xs : prod (x::xs) = mul x (prod xs).

Lemma prod_singleton [m] (x : Zstar m) : prod [x] = x.

Lemma prod_Permutation [m] (xs ys : list (Zstar m)) (H : Permutation xs ys) :
  prod xs = prod ys.

Lemma prod_app [m] xs ys : prod (xs ++ ys) = mul (prod xs) (prod ys) :> Zstar m.

Lemma prod_flat_map [A] [m] (f : A -> _) (xs : list A) :
  prod (flat_map f xs) = prod (map (fun x => prod (f x)) xs) :> Zstar m.

Lemma prod_concat [m] (xss : list (list (Zstar m))) :
  prod (concat xss) = prod ((map (fun xs => prod xs)) xss) :> Zstar m.

Lemma prod_rev [m] (xs : list (Zstar m)) : prod (rev xs) = prod xs.

Lemma to_Zmod_pow [m] (a : Zstar m) z : @to_Zmod m (pow a z) = Zmod.pow a z.
Lemma pow_0_r [m] x : @pow m x 0 = one.

Lemma pow_1_r [m] x : @pow m x 1 = x.

Lemma pow_2_r [m] x : @pow m x 2 = mul x x.

Lemma pow_opp_2 [m] (x : Zstar m) : pow (opp x) 2 = pow x 2.

Lemma pow_abs_2 [m] (x : Zstar m) : pow (abs x) 2 = pow x 2.

Lemma eq_abs_iff m (x y : Zstar m) : abs x = abs y <-> (y = x \/ y = opp x).

Lemma Private_coprime_Zmodpow [m] (a : Zstar m) z (H : 0 <= z ) : Z.coprime (Zmod.pow a z) m.

Lemma pow_opp_r [m] a (z : Z) : @pow m a (-z) = inv (pow a z).
#[local] Lemma Private_pow_succ_r_nonneg [m] (x : Zstar m) z (H : 0 <= z) :
  pow x (Z.succ z) = mul x (pow x z).

Lemma pow_succ_r [m] (x : Zstar m) z : pow x (Z.succ z) = mul x (pow x z).

Lemma pow_pred_r [m] (x : Zstar m) z : pow x (Z.pred z) = div (pow x z) x.

Lemma pow_1_l [m] z : @pow m one z = one.

Lemma pow_add_r [m] (x : Zstar m) a b : pow x (a+b) = mul (pow x a) (pow x b).

Lemma pow_sub_r [m] (x : Zstar m) a b : pow x (a-b) = div (pow x a) (pow x b).

Lemma pow_mul_r [m] (x : Zstar m) a b : pow x (a*b) = pow (pow x a) b.

Lemma pow_mul_l [m] (x y : Zstar m) n : pow (mul x y) n = mul (pow x n) (pow y n).

Lemma inv_pow_m1 m n : @inv m (pow (opp one) n) = pow (opp one) n.

Lemma prod_repeat [m] (a : Zstar m) n : prod (repeat a n) = pow a (Z.of_nat n).

Lemma prod_map_mul [m] (a : Zstar m) xs :
  prod (List.map (mul a) xs) = mul (pow a (Z.of_nat (length xs))) (prod xs).

Lemma prod_pow [m] z xs : prod (map (fun x => pow x z) xs) = pow (prod xs) z :> Zstar m.

Lemma prod_opp [m] xs : prod (map (@opp m) xs) = mul (pow (opp one) (Z.of_nat (length xs))) (prod xs).

Lemma in_of_Zmod_filter [m] x (l : list (Zmod m)) :
  In x (map of_Zmod (filter (fun y : Zmod m => Z.gcd y m =? 1) l)) <-> In (to_Zmod x) l.

Lemma in_elements [m] (x : Zstar m) : In x (elements m).

Lemma NoDup_elements m : NoDup (elements m).

Lemma to_Zmod_elements m : List.map to_Zmod (elements m) = Zmod.invertibles m.

Lemma elements_by_sign [m] (Hm : 2 <= Z.abs m) : elements m = positives m ++ negatives m.

Lemma in_positives [m] (x : Zstar m) (Hm : m <> 0) : In x (positives m) <-> 0 < signed x.

Lemma in_negatives [m] (x : Zstar m) (Hm : m <> 0) : In x (negatives m) <-> signed x < 0.

Lemma negatives_as_positives_odd m (Hm : m mod 2 = 1) :
  negatives m = map opp (rev (positives m)).

Lemma NoDup_positives m : NoDup (positives m).

Lemma NoDup_negatives m : NoDup (negatives m).

#[local] Hint Unfold Injective List.incl : core.
Lemma Permutation_mul_elements [m] (a : Zstar m) :
  Permutation (List.map (mul a) (elements m)) (elements m).

Theorem euler [m] (a : Zstar m) : pow a (Z.of_nat (length (elements m))) = one.

Lemma to_Zmod_elements_prime p (H : Z.prime p) :
  List.map to_Zmod (elements p) = List.tl (Zmod.elements p).

Lemma length_elements_prime p (H : Z.prime p) : length (elements p) = Z.to_nat (p-1).

Lemma length_positives_length_negatives_odd m (Hm : m mod 2 = 1) :
  length (positives m) = length (negatives m).

Lemma length_positives_odd [m] (H : m mod 2 = 1) :
  length (positives m) = (length (elements m) / 2)%nat.

Lemma length_negatives_odd [m] (H : m mod 2 = 1) :
  length (negatives m) = (length (elements m) / 2)%nat.

#[local] Lemma Private_odd_prime (p : Z) : Z.prime p -> 3 <= p -> p mod 2 = 1.

Lemma length_positives_prime [m] (H : Z.prime m) :
  length (positives m) = Z.to_nat ((m-1) / 2).

Lemma length_negatives_prime [m] (H : Z.prime m) :
  length (negatives m) = Z.to_nat (m / 2).

Theorem fermat [m] (a : Zstar m) (H : Z.prime m) : pow a (Z.pred m) = one.

Theorem fermat_inv [m] (a : Zstar m) (H : Z.prime m) : pow a (m-2) = inv a.

Theorem euler_criterion_square [p] (Hp : Z.prime p)
  (a sqrt_a : Zstar p) (Ha : pow sqrt_a 2 = a) : pow a ((p-1)/2) = one.

End Zstar.