Library Stdlib.Zmod.ZstarBase

From Stdlib Require Import NArith ZArith ZModOffset Zcong Lia Zdivisibility.
From Stdlib Require Import Bool.Bool Lists.List 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 FinFun.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.