Commit 3b55aafb authored by Benoit Viguier's avatar Benoit Viguier
Browse files

Fix Zmodp2

parent f6ee0272
From Tweetnacl.Libs Require Import Export. From Tweetnacl.Libs Require Import Export.
From Tweetnacl.Gen Require Import AMZubSqSel. From Tweetnacl.Gen Require Import AMZubSqSel.
From Tweetnacl.Gen Require Import UPIC.
Class Ops_Mod_P {T T' U:Type} {Mod:U -> U} {ModT:T -> T} `(Ops T T' ModT) `(Ops U U Mod) := Class Ops_Mod_P {T T' U:Type} {Mod:U -> U} {ModT:T -> T} `(Ops T T' ModT) `(Ops U U Mod) :=
{ {
......
...@@ -79,7 +79,7 @@ Module Zmodp. ...@@ -79,7 +79,7 @@ Module Zmodp.
Inductive type := Zmodp x of betweenb 0 p x. Inductive type := Zmodp x of betweenb 0 p x.
Lemma Z_mod_betweenb x y : y > 0 -> betweenb 0 y (x mod y). Lemma Z_mod_betweenb x y : y > 0 -> betweenb 0 y (x mod y).
Proof. by move=> H; apply/betweenbP; apply: Z_mod_lt. Qed. Proof. by move=> H; apply/betweenbP; apply: Z_mod_lt. Defined.
Definition pi (x : Z) : type := Zmodp (Z_mod_betweenb x Hp_gt0). Definition pi (x : Z) : type := Zmodp (Z_mod_betweenb x Hp_gt0).
Coercion repr (x : type) : Z := let: @Zmodp x _ := x in x. Coercion repr (x : type) : Z := let: @Zmodp x _ := x in x.
...@@ -91,6 +91,21 @@ Definition add (x y : type) : type := pi (x + y). ...@@ -91,6 +91,21 @@ Definition add (x y : type) : type := pi (x + y).
Definition sub (x y : type) : type := pi (x - y). Definition sub (x y : type) : type := pi (x - y).
Definition mul (x y : type) : type := pi (x * y). Definition mul (x y : type) : type := pi (x * y).
Definition eqb x y := match x, y with
| Zmodp x _ , Zmodp y _ => Z.eqb x y
end.
Lemma Zeqb_eqb x y : Z.eqb x y -> eqb (pi x) (pi y).
Proof.
move/Z.eqb_spec ->.
rewrite /eqb.
case (pi y) => yi _.
apply Z.eqb_refl.
Qed.
Lemma Zeqb_eq x y : Z.eqb x y -> pi x = pi y.
Proof. by move/Z.eqb_spec ->. Qed.
End Zmodp. End Zmodp.
Import Zmodp. Import Zmodp.
...@@ -192,6 +207,47 @@ End Exports. ...@@ -192,6 +207,47 @@ End Exports.
End Zmodp_zmod. End Zmodp_zmod.
Import Zmodp_zmod.Exports. Import Zmodp_zmod.Exports.
Module Refl.
Lemma eqb_Zeqb x y : eqb x y -> Z.eqb x y.
Proof.
move=> H.
rewrite -(reprK x).
rewrite -(reprK y).
apply/Z.eqb_spec.
move: H.
simpl.
rewrite /eqb.
case_eq y => yi Hyi Heqyi.
case_eq x => xi Hxi Heqxi /=.
by move/Z.eqb_spec ->.
Qed.
Lemma eqb_spec (x y: type) : reflect (x = y) (eqb x y).
Proof.
apply Bool.iff_reflect.
split.
+ move => ->.
rewrite /eqb.
case x => xi Hxi.
case y => yi Hyi.
by apply Z.eqb_refl.
+
move=> H.
rewrite -(reprK x).
rewrite -(reprK y).
move: H.
rewrite /eqb.
case x.
case y.
move=> xi Hxi yi Hyi /=.
by move/Zeqb_eq.
Qed.
End Refl.
Import Refl.
Lemma Zmodp_addE x y : (pi x + pi y)%R = pi (x + y). Lemma Zmodp_addE x y : (pi x + pi y)%R = pi (x + y).
Proof. Proof.
apply/eqP; rewrite eqE; apply/eqP=> /=. apply/eqP; rewrite eqE; apply/eqP=> /=.
...@@ -223,7 +279,7 @@ Proof. by move=> x y; apply: val_inj; rewrite /= Zmult_comm. Qed. ...@@ -223,7 +279,7 @@ Proof. by move=> x y; apply: val_inj; rewrite /= Zmult_comm. Qed.
Lemma mul_left_id : left_id one mul. Lemma mul_left_id : left_id one mul.
Proof. Proof.
move=> x; apply: val_inj. rewrite /=. move=> x. apply: val_inj. rewrite /=.
rewrite Z.mod_1_l; last exact: Z.gt_lt Hp_gt1. rewrite Z.mod_1_l; last exact: Z.gt_lt Hp_gt1.
by rewrite Z.mul_1_l; apply: modZp. by rewrite Z.mul_1_l; apply: modZp.
Qed. Qed.
...@@ -373,4 +429,4 @@ apply Zmodp_zmod.add_sub. ...@@ -373,4 +429,4 @@ apply Zmodp_zmod.add_sub.
move => x. rewrite Zmodp_zmod.add_comm Zmodp_zmod.add_left_inv //. move => x. rewrite Zmodp_zmod.add_comm Zmodp_zmod.add_left_inv //.
Defined. Defined.
Add Ring Zmodp_ring : Zmodp_ring. Add Ring Zmodp_ring : Zmodp_ring.
\ No newline at end of file
...@@ -9,23 +9,12 @@ Set Implicit Arguments. ...@@ -9,23 +9,12 @@ Set Implicit Arguments.
Unset Strict Implicit. Unset Strict Implicit.
Open Scope Z. Open Scope Z.
Import Zmodp.
Open Scope ring_scope. Open Scope ring_scope.
Import GRing.Theory. Import GRing.Theory.
Import Zmodp.
Module Zmodp2. Module Zmodp2.
(* Lemma prime_p : prime.prime (Z.to_nat p).
Proof. apply prime_ssrprime. rewrite Z_of_nat_to_nat_p /p -lock; apply primo. Qed.
Lemma pow2_pos : is_true (leq (S O) (S (S O))).
Proof. done. Qed.
Check sval.
Definition GFp2 := sval (PrimePowerField prime_p pow2_pos).
*)
Inductive type := Zmodp2 (x: Zmodp.type) (y:Zmodp.type). Inductive type := Zmodp2 (x: Zmodp.type) (y:Zmodp.type).
Definition pi (x : Zmodp.type * Zmodp.type) : type := Zmodp2 x.1 x.2. Definition pi (x : Zmodp.type * Zmodp.type) : type := Zmodp2 x.1 x.2.
...@@ -36,17 +25,35 @@ Coercion reprZ (x : type) : Z*Z := let: Zmodp2 (@Zmodp u _) (@Zmodp v _) := x in ...@@ -36,17 +25,35 @@ Coercion reprZ (x : type) : Z*Z := let: Zmodp2 (@Zmodp u _) (@Zmodp v _) := x in
Definition zero : type := pi (Zmodp.zero, Zmodp.zero). Definition zero : type := pi (Zmodp.zero, Zmodp.zero).
Definition one : type := pi (Zmodp.one, Zmodp.zero). Definition one : type := pi (Zmodp.one, Zmodp.zero).
Definition opp (x : type) : type := pi (Zmodp.opp x.1 , Zmodp.opp x.2). Definition opp (x : type) : type := pi (Zmodp.opp x.1 , Zmodp.opp x.2).
Definition add (x y : type) : type := pi (x.1 + y.1, x.2 + y.2). Definition add (x y : type) : type := pi (Zmodp.add x.1 y.1, Zmodp.add x.2 y.2).
Definition mul (x y : type) : type := pi (x.1 * y.1 - x.2 * y.2 , x.1 * y.2 + x.2 * y.1). Definition sub (x y : type) : type := pi (Zmodp.sub x.1 y.1, Zmodp.sub x.2 y.2).
Definition mul (x y : type) : type := pi (Zmodp.sub (Zmodp.mul x.1 y.1) (Zmodp.mul x.2 y.2), Zmodp.add (Zmodp.mul x.1 y.2) (Zmodp.mul x.2 y.1)).
Lemma pi_of_reprK : cancel repr pi. Lemma pi_of_reprK : cancel repr pi.
Proof. by case. Qed. Proof. by case. Qed.
Definition eqb (x y : type) := match x, y with
| Zmodp2 x1 x2, Zmodp2 y1 y2 => Zmodp.eqb x1 y1 && Zmodp.eqb x2 y2
end.
Lemma eqb_spec (x y: type) : reflect (x = y) (eqb x y).
Proof.
apply Bool.iff_reflect.
split.
+ move => ->.
rewrite /eqb.
case y => y1 y2.
by apply/andP ; split ; apply /Refl.eqb_spec.
+ rewrite /eqb.
case x => x1 x2.
case y => y1 y2.
by move/andP => [] /Refl.eqb_spec -> /Refl.eqb_spec ->.
Qed.
End Zmodp2. End Zmodp2.
Import Zmodp2. Import Zmodp2.
Definition Zmodp2_eqMixin := CanEqMixin pi_of_reprK. Definition Zmodp2_eqMixin := CanEqMixin pi_of_reprK.
Canonical Structure Zmodp2_eqType := Eval hnf in EqType type Zmodp2_eqMixin. Canonical Structure Zmodp2_eqType := Eval hnf in EqType type Zmodp2_eqMixin.
Definition Zmodp2_choiceMixin := CanChoiceMixin pi_of_reprK. Definition Zmodp2_choiceMixin := CanChoiceMixin pi_of_reprK.
...@@ -70,38 +77,50 @@ Proof. by case x. Qed. ...@@ -70,38 +77,50 @@ Proof. by case x. Qed.
Lemma piZK (x : Z*Z) : betweenb 0 p x.1 -> betweenb 0 p x.2 -> reprZ (piZ x) = x. Lemma piZK (x : Z*Z) : betweenb 0 p x.1 -> betweenb 0 p x.2 -> reprZ (piZ x) = x.
Proof. by case x => u v /= ; move/betweenbP => Hu /betweenbP => Hv /= ; f_equal; apply: Zmod_small. Qed. Proof. by case x => u v /= ; move/betweenbP => Hu /betweenbP => Hv /= ; f_equal; apply: Zmod_small. Qed.
Lemma Zmodp2_const x1 x2 y1 y2: x1 = y1 -> x2 = y2 -> Zmodp2 x1 x2 = Zmodp2 y1 y2.
Proof. move=> -> -> //. Qed.
(* Lemma type_dec x : x = zero \/ x <> zero.
Proof.
case x => [x1 x2].
case_eq (Zmodp.eqb x1 Zmodp.zero); move/Refl.eqb_spec.
case_eq (Zmodp.eqb x2 Zmodp.zero); move/Refl.eqb_spec.
by move=> -> -> ; left => //.
by move=> Hx2 Hx1 ; right => H ; apply Hx2 ; inversion H.
by move=> Hx1 ; right => H ; apply Hx1 ; inversion H.
Qed. *)
Module Zmodp2_zmod. Module Zmodp2_zmod.
Lemma add_assoc : associative add.
Proof.
move=> [x1 x2] [y1 y2] [z1 z2] ; rewrite /add /= ; f_equal; f_equal; apply Zmodp_zmod.add_assoc.
Qed.
Lemma add_comm : commutative add. Lemma add_comm : commutative add.
Proof. Proof.
move=> [x1 x2] [y1 y2] ; rewrite /add /= ; f_equal; f_equal; apply Zmodp_zmod.add_comm. move=> [x1 x2] [y1 y2] ; rewrite /add /= ; f_equal; f_equal ; ring.
Qed. Qed.
Lemma add_left_id : left_id zero add. Lemma add_left_id : left_id zero add.
Proof. move => [x1 x2]. rewrite /add /=. Proof. move => [x1 x2]. rewrite /add /=.
have ->: Zmodp.zero + x1 = x1. rewrite Zmodp_zmod.add_left_id.
by apply Zmodp_zmod.add_left_id. rewrite Zmodp_zmod.add_left_id.
have ->: Zmodp.zero + x2 = x2.
by apply Zmodp_zmod.add_left_id.
reflexivity. reflexivity.
Qed. Qed.
Lemma add_left_inv : left_inverse zero opp add. Lemma add_left_inv : left_inverse zero opp add.
Proof. move => [x1 x2]. rewrite /add /=. Proof. move => [x1 x2]. rewrite /add /=.
have ->: Zmodp.opp x1 + x1 = 0. rewrite Zmodp_zmod.add_left_inv.
by apply Zmodp_zmod.add_left_inv. rewrite Zmodp_zmod.add_left_inv.
have ->: Zmodp.opp x2 + x2 = 0.
by apply Zmodp_zmod.add_left_inv.
reflexivity. reflexivity.
Qed. Qed.
Lemma add_assoc : associative add.
Proof. move=> [x1 x2] [y1 y2] [z1 z2] ; rewrite /add /= ; f_equal; f_equal; apply Zmodp_zmod.add_assoc. Qed.
Lemma add_sub : forall (x y:type), sub x y = add x (opp y).
Proof.
move=> x y.
rewrite /sub /add /opp.
f_equal; f_equal => /= ; ring.
Qed.
Module Exports. Module Exports.
Definition Zmodp_zmodMixin := Definition Zmodp_zmodMixin :=
ZmodMixin add_assoc add_comm add_left_id add_left_inv. ZmodMixin add_assoc add_comm add_left_id add_left_inv.
...@@ -112,10 +131,10 @@ End Exports. ...@@ -112,10 +131,10 @@ End Exports.
End Zmodp2_zmod. End Zmodp2_zmod.
Import Zmodp2_zmod.Exports. Import Zmodp2_zmod.Exports.
Lemma Zmodp2_addE x y : (pi x + pi y)%R = pi (x + y). Lemma Zmodp2_addE x y : (pi x + pi y)%R = pi (x.1 + y.1, x.2 + y.2).
Proof. reflexivity. Qed. Proof. reflexivity. Qed.
Lemma Zmodp_oppE x : (-pi x)%R = pi (-x). Lemma Zmodp2_oppE x : (-pi x)%R = pi (-x).
Proof. reflexivity. Qed. Proof. reflexivity. Qed.
Fact Hp_gt1 : p > 1. Fact Hp_gt1 : p > 1.
...@@ -125,18 +144,16 @@ Module Zmodp2_ring. ...@@ -125,18 +144,16 @@ Module Zmodp2_ring.
Lemma mul_comm : commutative mul. Lemma mul_comm : commutative mul.
Proof. move=> [x1 x2] [y1 y2] ; rewrite /mul /=. Proof. move=> [x1 x2] [y1 y2] ; rewrite /mul /=.
have Hab: forall a b:Zmodp.type, a + b = b + a. f_equal; f_equal; ring.
by apply Zmodp_zmod.add_comm.
rewrite (Hab (y1 * x2) _ ).
f_equal ; f_equal ; f_equal; [|f_equal| | ];
apply Zmodp_ring.mul_comm.
Qed. Qed.
Lemma mul_assoc : associative mul. Lemma mul_assoc : associative mul.
Proof. Proof.
move=> [x1 x2] [y1 y2] [z1 z2] ; rewrite /mul /= . f_equal. move=> [x1 x2] [y1 y2] [z1 z2] ; rewrite /mul /= . f_equal.
f_equal ; apply val_inj => /=. f_equal.
+ ring.
+ ring.
(* ; apply val_inj => /=.
+ rewrite Zminus_mod_idemp_r. + rewrite Zminus_mod_idemp_r.
rewrite -(Zplus_mod (y1 * z1)). rewrite -(Zplus_mod (y1 * z1)).
rewrite Zmult_mod_idemp_r. rewrite Zmult_mod_idemp_r.
...@@ -172,48 +189,31 @@ f_equal ; apply val_inj => /=. ...@@ -172,48 +189,31 @@ f_equal ; apply val_inj => /=.
x1 * (y1 * z2 + y2 * z1) + x2 * (y1 * z1 + ( - y2 * z2)) + (x2 * p))%Z by ring. x1 * (y1 * z2 + y2 * z1) + x2 * (y1 * z1 + ( - y2 * z2)) + (x2 * p))%Z by ring.
have ->: ((x1 * y1 + (p - x2 * y2)) * z2 + (x1 * y2 + x2 * y1) * z1 = have ->: ((x1 * y1 + (p - x2 * y2)) * z2 + (x1 * y2 + x2 * y1) * z1 =
x1 * (y1 * z2 + y2 * z1) + x2 * (y1 * z1 + ( - y2 * z2)) + (z2 * p))%Z by ring. x1 * (y1 * z2 + y2 * z1) + x2 * (y1 * z1 + ( - y2 * z2)) + (z2 * p))%Z by ring.
by rewrite ?Z_mod_plus_full. by rewrite ?Z_mod_plus_full. *)
Qed. Qed.
Lemma mul_left_id : left_id one mul. Lemma mul_left_id : left_id one mul.
Proof. Proof.
move=> [x1 x2]. rewrite /mul /=. move=> [x1 x2]. rewrite /mul /=.
have ->: Zmodp.one * x1 = x1. rewrite Zmodp_ring.mul_left_id.
by apply Zmodp_ring.mul_left_id. rewrite Zmodp_ring.mul_left_id.
have ->: Zmodp.one * x2 = x2. have ->: Zmodp.mul Zmodp.zero x2 = Zmodp.zero => //.
by apply Zmodp_ring.mul_left_id. have ->: Zmodp.mul Zmodp.zero x1 = Zmodp.zero => //.
have ->: Zmodp.zero * x2 = Zmodp.zero. rewrite Zmodp_zmod.add_sub.
reflexivity. have ->: Zmodp.opp Zmodp.zero = Zmodp.zero by ring.
have ->: Zmodp.zero * x1 = Zmodp.zero. have ->: Zmodp.add x1 Zmodp.zero = x1 by ring.
reflexivity. have ->: Zmodp.add x2 Zmodp.zero = x2 by ring.
have ->: -Zmodp.zero = Zmodp.zero. reflexivity.
apply val_inj => /=.
rewrite Zminus_mod_idemp_r.
rewrite -Zminus_mod_idemp_l.
rewrite Z_mod_same_full.
reflexivity.
have ->: x1 + Zmodp.zero = Zmodp.zero + x1.
apply val_inj => /=.
rewrite Zmod_0_l.
rewrite Z.add_0_r.
reflexivity.
have ->: x2 + Zmodp.zero = Zmodp.zero + x2.
apply val_inj => /=.
rewrite Zmod_0_l.
rewrite Z.add_0_r.
reflexivity.
have ->: Zmodp.zero + x1 = x1.
by apply Zmodp_zmod.add_left_id.
have ->: Zmodp.zero + x2 = x2.
by apply Zmodp_zmod.add_left_id.
reflexivity.
Qed. Qed.
Lemma mul_left_distr : left_distributive mul add. Lemma mul_left_distr : left_distributive mul add.
Proof. Proof.
move=> [x1 x2] [y1 y2] [z1 z2]. rewrite /mul /add /=. f_equal. move=> [x1 x2] [y1 y2] [z1 z2]. rewrite /mul /add /=. f_equal.
f_equal; apply val_inj => /=. f_equal.
+ rewrite Zmult_mod_idemp_l. ring.
ring.
(* + apply val_inj => /=.
rewrite Zmult_mod_idemp_l.
rewrite Zmult_mod_idemp_l. rewrite Zmult_mod_idemp_l.
rewrite Zminus_mod_idemp_r. rewrite Zminus_mod_idemp_r.
rewrite -Zplus_mod. rewrite -Zplus_mod.
...@@ -227,14 +227,15 @@ f_equal; apply val_inj => /=. ...@@ -227,14 +227,15 @@ f_equal; apply val_inj => /=.
have ->: (x1 * z1 + (p - x2 * z2) + (y1 * z1 + (p - y2 * z2)) = have ->: (x1 * z1 + (p - x2 * z2) + (y1 * z1 + (p - y2 * z2)) =
(x1 + y1) * z1 + - (x2 + y2) * z2 + 2 * p)%Z by ring. (x1 + y1) * z1 + - (x2 + y2) * z2 + 2 * p)%Z by ring.
by rewrite ?Z_mod_plus_full. by rewrite ?Z_mod_plus_full.
+ rewrite Zmult_mod_idemp_l. + apply val_inj => /=.
rewrite Zmult_mod_idemp_l.
rewrite Zmult_mod_idemp_l. rewrite Zmult_mod_idemp_l.
rewrite -Zplus_mod. rewrite -Zplus_mod.
rewrite -(Zplus_mod (x1 * z2)). rewrite -(Zplus_mod (x1 * z2)).
rewrite -(Zplus_mod (y1 * z2)). rewrite -(Zplus_mod (y1 * z2)).
rewrite -Zplus_mod. rewrite -Zplus_mod.
f_equal. f_equal.
ring. ring. *)
Qed. Qed.
Lemma one_neq_zero : one != zero. Lemma one_neq_zero : one != zero.
...@@ -244,121 +245,142 @@ apply/eqP => H ; inversion H; move: H1. ...@@ -244,121 +245,142 @@ apply/eqP => H ; inversion H; move: H1.
by rewrite Zmod_0_l Zmod_1_l; last exact: Z.gt_lt Hp_gt1. by rewrite Zmod_0_l Zmod_1_l; last exact: Z.gt_lt Hp_gt1.
Qed. Qed.
Lemma two_neq_zero : (one + one) != zero.
Proof.
rewrite /one /zero; f_equal.
zmodp_compute.
apply/eqP => H ; inversion H; clear H; move: H1.
rewrite /p -lock.
by compute.
Qed.
Lemma three_neq_zero : (one + one + one) != zero.
Proof.
rewrite /one /zero; f_equal.
zmodp_compute.
apply/eqP => H ; inversion H; clear H; move: H1.
rewrite /p -lock.
by compute.
Qed.
Module Exports. Module Exports.
Definition Zmodp_ringMixin := Eval hnf in ComRingMixin mul_assoc mul_comm mul_left_id mul_left_distr one_neq_zero. Definition Zmodp2_ringMixin := Eval hnf in ComRingMixin mul_assoc mul_comm mul_left_id mul_left_distr one_neq_zero.
Canonical Structure Zmodp_ringType := Eval hnf in RingType type Zmodp_ringMixin. Canonical Structure Zmodp2_ringType := Eval hnf in RingType type Zmodp2_ringMixin.
Canonical Structure Zmodp_comRingType := Eval hnf in ComRingType type mul_comm. Canonical Structure Zmodp2_comRingType := Eval hnf in ComRingType type mul_comm.
End Exports. End Exports.
End Zmodp2_ring. End Zmodp2_ring.
Import Zmodp2_ring.Exports. Import Zmodp2_ring.Exports.
Lemma Zmodp_mulE x y : (pi x * pi y)%R = pi (x.1 * y.1 - x.2 * y.2, x.1 * y.2 + x.2 * y.1). Lemma Zmodp2_mulE x y : (pi x * pi y)%R = pi (x.1 * y.1 - x.2 * y.2, x.1 * y.2 + x.2 * y.1).
Proof. Proof.
apply/eqP; rewrite eqE; apply/eqP=> /=. apply/eqP; rewrite eqE; apply/eqP=> /=.
reflexivity. rewrite Zmodp_zmod.add_sub.
(* apply: esym. f_equal; apply val_inj => /=. apply: esym. f_equal; apply val_inj => /=.
apply: Z.mul_mod. Qed.
apply val_inj.
by apply: esym; apply: Z.mul_mod; apply: Hp_neq0.
*)Qed.
Fact Hp_prime : prime p. Fact Hp_prime : prime p.
Proof. by unlock p; apply: primo. Qed. Proof. by unlock p; apply: primo. Qed.
(* Inductive Zinv_spec (x : Z) : Set := Inductive Zinv_spec (x : type) : Type :=
| Zinv_spec_zero : x = zero -> Zinv_spec x | Zinv_spec_zero : x = zero -> Zinv_spec x
| Zinv_spec_unit : x mod p <> 0 -> forall y, (y * x) mod p = 1 -> Zinv_spec x. | Zinv_spec_unit : x <> zero -> forall y, (y * x)%R = one -> Zinv_spec x.
*)
(* TODO: I don't like the use of the opaque [euclid]. *) Fixpoint pow (n:nat) (x:type) := match n with
(* Lemma Zinv x : Zinv_spec x. | 0%nat => one
| S n => (x * pow n x)%R
end.
Axiom Zinv_pow : forall (x :type), x <> zero -> pow (Z.to_nat (Z.pow p 2 - 1)%Z) x = one.
Lemma Zinv x : Zinv_spec x.
Proof. Proof.
case: (Z.eqb_spec (x mod p) 0); first exact: Zinv_spec_zero. case_eq (eqb x zero) ; move/eqb_spec.
move=> Hx. + move => -> ; exact: Zinv_spec_zero.
have [u v d Euv Hgcd]: Euclid (x mod p) p by apply: euclid. + move=> Hx.
wlog: u v d Euv Hgcd / (0 <= d) => [|Hd]. apply (@Zinv_spec_unit x Hx (pow (Z.to_nat (Z.pow p 2 - 2)) x)).
case: (Z.leb_spec0 0 d) => Hd; first by apply; first exact: Euv. have := Zinv_pow Hx.
apply Z.nle_gt in Hd. have ->: Z.to_nat (p ^ 2 - 1)%Z = (Z.to_nat (p ^ 2 - 2 + 1)%Z) by f_equal ; omega.
have Hd2 : 0 <= -d by omega. change (p ^2 - 2 + 1)%Z with (Z.succ (p^2 -2))%Z.
have Hgcd2 : Zis_gcd (x mod p) p (-d) rewrite Z2Nat.inj_succ /=.
by apply: Zis_gcd_opp; apply: Zis_gcd_sym. 2: by rewrite /p -lock ; compute.
apply; [| exact: Hgcd2 | exact: Hd2]. move => <-.
rewrite -Euv Z.opp_add_distr -!Z.mul_opp_l. apply Zmodp2_ring.mul_comm.
by congr (_ + _). Qed.
apply: (@Zinv_spec_unit _ Hx u).
rewrite -Z.mul_mod_idemp_r; last exact: Hp_neq0. Definition Zmodp2_inv (x : type) : type :=
apply: Zdivide_mod_minus; first by move: Hp_gt1=> ?; omega.
rewrite /Z.divide; exists (-v).
rewrite Z.mul_opp_l -Z.add_move_0_r -Z.add_sub_swap Z.sub_move_0_r Euv.
rewrite -(Zis_gcd_gcd _ _ _ _ Hgcd); last exact: Hd.
rewrite Zgcd_1_rel_prime.
apply: rel_prime_le_prime; first exact: Hp_prime.
suff: 0 <= x mod p < p
by move=> ?; omega.
by apply: Z.mod_pos_bound; apply: Z.gt_lt; apply: Hp_gt0.
Qed. *)(*
Definition Zmodp_inv (x : type) : type :=
match Zinv x with match Zinv x with
| Zinv_spec_zero _ => zero | Zinv_spec_zero _ => zero
| @Zinv_spec_unit _ _ y _ => pi (Z.modulo y p) | @Zinv_spec_unit _ _ y _ => pi y
end. end.
Lemma modZp0 (x : type) : x mod p = 0 -> x == 0%R. Module Zmodp2_field.
Proof. by rewrite modZp => Hx_eq0; rewrite -[x]reprK Hx_eq0. Qed.
Module Zmodp_field. Lemma mulVx : GRing.Field.axiom Zmodp2_inv.
Lemma mulVx : GRing.Field.axiom Zmodp_inv.
Proof. Proof.
move=> x Hx_neq0. move=> x Hx_neq0.
rewrite /Zmodp_inv; case: (Zinv x); first by move/modZp0/eqP; move/eqP: Hx_neq0. rewrite /Zmodp2_inv.
move=> Hxmodp_neq0 y Exy. case: (Zinv x).
apply/eqP; rewrite eqE; apply/eqP=> /=. + by move/eqP: Hx_neq0.
have HP:= Hp_gt1. + move=> Hxx_neq0 y.
rewrite ?Z.mul_mod_idemp_l; last exact: Hp_neq0. done.
by rewrite [1 mod p]Z.mod_small ; last by move: Hp_gt1=> ?; omega.
omega.
Qed. Qed.