Commit 0a78441e authored by Benoit Viguier's avatar Benoit Viguier
Browse files

make the High Zmodp2 clearer

parent 09970ac6
Set Warnings "-notation-overridden,-parsing".
From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq choice.
From mathcomp Require Import fintype ssralg finalg.
Import GRing.Theory.
Set Implicit Arguments.
Unset Strict Implicit.
Open Scope ring_scope.
Import GRing.Theory.
Ltac ring_unfold:=
repeat match goal with
| _ => progress rewrite /GRing.mul
| _ => progress rewrite /GRing.add
| _ => progress rewrite /GRing.opp
end; move => /=.
Ltac ring_simplify_this :=
repeat match goal with
| _ => rewrite GRing.expr0
| _ => rewrite GRing.exprS
| _ => rewrite GRing.mul1r
| _ => rewrite GRing.mulr1
| _ => rewrite GRing.mul0r
| _ => rewrite GRing.mulr0
| _ => rewrite GRing.mulr0n
| _ => rewrite GRing.add0r
| _ => rewrite GRing.oppr0
| _ => rewrite GRing.addr0
| _ => done
end.
Close Scope ring_scope.
\ No newline at end of file
......@@ -436,6 +436,13 @@ apply modZp.
Qed.
Open Scope ring_scope.
Lemma pi_2 : Zmodp.pi 2 = 2%:R.
Proof. by apply/eqP ; zmodp_compute. Qed.
Lemma pi_3 : Zmodp.pi 3 = 3%:R.
Proof. by apply/eqP ; zmodp_compute. Qed.
Lemma add_eq_mul2: forall (x:Zmodp.type),
2%:R * x = x + x.
Proof.
......@@ -456,4 +463,16 @@ Lemma mult_xy_eq_0: forall (x y: Zmodp.type),
x * y = 0 -> x = 0 \/ y = 0.
Proof. by move => x y/eqP; rewrite mulf_eq0 ; move/orP => []/eqP -> ; [left|right]. Qed.
Ltac Zmodp_ringify := repeat match goal with
| [ |- context[Zmodp.pi 2]] => rewrite pi_2
| [ |- context[Zmodp.pi 3]] => rewrite pi_3
| [ |- context[Zmodp.mul ?a ?b]] => have ->: (Zmodp.mul a b) = a * b => //
| [ |- context[Zmodp.add ?a (Zmodp.opp ?b)]] => have ->: (Zmodp.add a (Zmodp.opp b)) = a - b => //
| [ |- context[Zmodp.opp ?a]] => have ->: Zmodp.opp a = -a => //
| [ |- context[Zmodp.add ?a ?b]] => have ->: (Zmodp.add a b) = a + b => //
| [ |- context[Zmodp.one] ] => have ->: Zmodp.one = 1 => //
| [ |- context[Zmodp.zero] ] => have ->: Zmodp.zero = 0 => //
end.
Close Scope ring_scope.
......@@ -2,7 +2,7 @@ Set Warnings "-notation-overridden,-parsing".
From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq choice.
From mathcomp Require Import fintype ssralg finalg.
Require Import ZArith.
From Tweetnacl.High Require Import Zmodp Zmodp_Ring.
From Tweetnacl.High Require Import Zmodp Zmodp_Ring GRing_tools.
Set Implicit Arguments.
Unset Strict Implicit.
......@@ -17,16 +17,14 @@ Module Zmodp2.
Inductive type := Zmodp2 (x: Zmodp.type) (y:Zmodp.type).
Definition pi (x : Zmodp.type * Zmodp.type) : type := Zmodp2 x.1 x.2.
Definition piZ (x : Z * Z) : type := Zmodp2 (Zmodp (Z_mod_betweenb x.1 Hp_gt0)) (Zmodp (Z_mod_betweenb x.2 Hp_gt0)).
Coercion repr (x : type) : Zmodp.type*Zmodp.type := let: Zmodp2 u v := x in (u, v).
Coercion reprZ (x : type) : Z*Z := let: Zmodp2 (@Zmodp u _) (@Zmodp v _) := x in (u, v).
Definition zero : type := pi (Zmodp.zero, 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 add (x y : type) : type := pi (Zmodp.add x.1 y.1, Zmodp.add x.2 y.2).
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.add (Zmodp.mul x.1 y.1) (Zmodp.mul (Zmodp.pi 2) (Zmodp.mul x.2 y.2)), Zmodp.add (Zmodp.mul x.1 y.2) (Zmodp.mul x.2 y.1)).
Definition zero : type := pi (0%:R, 0%:R).
Definition one : type := pi (1, 0%:R).
Definition opp (x : type) : type := pi (- x.1 , - x.2).
Definition add (x y : type) : type := pi (x.1 + y.1, x.2 + y.2).
Definition sub (x y : type) : type := pi (x.1 - y.1, x.2 - y.2).
Definition mul (x y : type) : type := pi ((x.1 * y.1) + (2%:R * (x.2 * y.2)), (x.1 * y.2) + (x.2 * y.1)).
Lemma pi_of_reprK : cancel repr pi.
Proof. by case. Qed.
......@@ -52,6 +50,8 @@ Qed.
Lemma Zmodp2_inv : forall a b c d, Zmodp2 a c = Zmodp2 b d -> a = b /\ c = d.
Proof. by move => a b c d H; inversion H. Qed.
Ltac Zmodp2_unfold := rewrite /mul /sub /add /opp /zero /one.
End Zmodp2.
Import Zmodp2.
......@@ -76,51 +76,47 @@ Proof. by case x. Qed.
Lemma piK (x : Zmodp.type*Zmodp.type) : repr (pi x) = x.
Proof. by case x. Qed.
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.
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. *)
Local Ltac solve_this :=
repeat match goal with
| _ => progress Zmodp2_unfold; ring_unfold
| [ |- context[Zmodp2 ?A ?B]] => have ->: Zmodp2 A B = Zmodp2.pi (A,B) => //
| _ => solve[f_equal ; f_equal ; ring]
| _ => solve[f_equal ; f_equal ; Zmodp_ringify ; ring_simplify_this]
end.
Module Zmodp2_zmod.
Lemma add_comm : commutative add.
Proof.
move=> [x1 x2] [y1 y2] ; rewrite /add /= ; f_equal; f_equal ; ring.
move=> [x1 x2] [y1 y2].
solve_this.
Qed.
Lemma add_left_id : left_id zero add.
Proof. move => [x1 x2]. rewrite /add /=.
rewrite Zmodp_zmod.add_left_id.
rewrite Zmodp_zmod.add_left_id.
reflexivity.
Proof. move => [x1 x2].
solve_this.
Qed.
Lemma add_left_inv : left_inverse zero opp add.
Proof. move => [x1 x2]. rewrite /add /=.
Proof. move => [x1 x2].
solve_this.
rewrite Zmodp_zmod.add_left_inv.
rewrite Zmodp_zmod.add_left_inv.
reflexivity.
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.
Proof. move=> [x1 x2] [y1 y2] [z1 z2].
solve_this.
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.
solve_this.
Qed.
Module Exports.
......@@ -145,16 +141,19 @@ Proof. by unlock p; rewrite Z.gt_lt_iff; apply/Z.ltb_spec0. Qed.
Module Zmodp2_ring.
Lemma mul_comm : commutative mul.
Proof. move=> [x1 x2] [y1 y2] ; rewrite /mul /=.
f_equal; f_equal; ring.
Proof. move=> [x1 x2] [y1 y2].
solve_this.
Qed.
Lemma mul_assoc : associative mul.
Proof.
move=> [x1 x2] [y1 y2] [z1 z2] ; rewrite /mul /= . f_equal.
move=> [x1 x2] [y1 y2] [z1 z2].
solve_this.
(* Zmodp2_unfold; ring_unfold.
f_equal.
f_equal.
+ ring.
+ ring.
+ ring. *)
(* ; apply val_inj => /=.
+ rewrite Zminus_mod_idemp_r.
rewrite -(Zplus_mod (y1 * z1)).
......@@ -196,22 +195,24 @@ Qed.
Lemma mul_left_id : left_id one mul.
Proof.
move=> [x1 x2]. rewrite /mul /=.
move=> [x1 x2].
solve_this.
(* Zmodp2_unfold; ring_unfold.
rewrite Zmodp_ring.mul_left_id.
rewrite Zmodp_ring.mul_left_id.
have ->: Zmodp.mul Zmodp.zero x2 = Zmodp.zero => //.
have ->: Zmodp.mul Zmodp.zero x1 = Zmodp.zero => //.
have ->: Zmodp.add x1 (Zmodp.mul (Zmodp.pi 2) Zmodp.zero) = x1 by ring.
have ->: Zmodp.add x2 Zmodp.zero = x2 by ring.
reflexivity.
have ->: Zmodp2 x1 x2 = pi (x1,x2) => //.
f_equal ; f_equal ; Zmodp_ringify ; ring_simplify_this. *)
Qed.
Lemma mul_left_distr : left_distributive mul add.
Proof.
move=> [x1 x2] [y1 y2] [z1 z2]. rewrite /mul /add /=. f_equal.
move=> [x1 x2] [y1 y2] [z1 z2].
solve_this.
(* rewrite /mul /add /GRing.add /=. f_equal.
f_equal.
ring.
ring.
*)
(* + apply val_inj => /=.
rewrite Zmult_mod_idemp_l.
rewrite Zmult_mod_idemp_l.
......@@ -275,20 +276,14 @@ Import Zmodp2_ring.Exports.
Lemma Zmodp2_mulE x y : (pi x * pi y)%R = pi (x.1 * y.1 + (Zmodp.pi 2) * (x.2 * y.2), x.1 * y.2 + x.2 * y.1).
Proof.
apply/eqP; rewrite eqE; apply/eqP=> /=.
apply: esym. f_equal; apply val_inj => /=.
apply/eqP; rewrite pi_2 eqE; apply/eqP=> //=.
Qed.
Inductive Zinv_spec (x : type) : Type :=
| Zinv_spec_zero : x = zero -> Zinv_spec x
| Zinv_spec_unit : x <> zero -> forall y, (y * x)%R = one -> Zinv_spec x.
Local Lemma pi_2 : Zmodp.pi 2 = 2%:R.
Proof. by apply/eqP ; zmodp_compute. Qed.
Local Lemma pi_3 : Zmodp.pi 3 = 3%:R.
Proof. by apply/eqP ; zmodp_compute. Qed.
Local Ltac ringify := repeat match goal with
(* Local Ltac ringify := repeat match goal with
| [ |- context[Zmodp.pi 2]] => rewrite pi_2
| [ |- context[Zmodp.mul ?a ?b]] => have ->: (Zmodp.mul a b) = a * b => //
| [ |- context[Zmodp.add ?a (Zmodp.opp ?b)]] => have ->: (Zmodp.add a (Zmodp.opp b)) = a - b => //
......@@ -297,7 +292,7 @@ Local Ltac ringify := repeat match goal with
| [ |- context[Zmodp.one] ] => have ->: Zmodp.one = 1 => //
| [ |- context[Zmodp.zero] ] => have ->: Zmodp.zero = 0 => //
end.
*)
Lemma Zinv x : Zinv_spec x.
Proof.
case_eq (eqb x zero) ; move/eqb_spec.
......@@ -305,7 +300,7 @@ case_eq (eqb x zero) ; move/eqb_spec.
+ destruct x as [x y] => Hxy.
apply (@Zinv_spec_unit (Zmodp2 x y) Hxy (Zmodp2 (x/(x^+2-2%:R*y^+2)) (-y/(x^+2-2%:R*y^+2)))).
rewrite /GRing.mul /= /mul /=.
ringify.
Zmodp_ringify.
have ->: x / (x ^+ 2 - 2%:R * y ^+ 2) * x + 2%:R * (- y / (x ^+ 2 - 2%:R * y ^+ 2) * y) = (x ^+2 - 2%:R * y^+2) / (x ^+ 2 - 2%:R * y ^+ 2).
remember (x ^+ 2 - 2%:R * y ^+ 2) as M.
by rewrite (mulrC x) (mulrC (-y)) ?mulrA (mulrC (2%:R)) -?mulrA -mulrDr mulrC mulNr mulrN HeqM ?expr2.
......@@ -411,4 +406,17 @@ move => x. rewrite Zmodp2_zmod.add_comm Zmodp2_zmod.add_left_inv //.
Defined.
Add Ring Zmodp2_ring : Zmodp2_ring.
Add Ring Zmodp2_ring2 : Zmodp2_ring2.
\ No newline at end of file
Add Ring Zmodp2_ring2 : Zmodp2_ring2.
Open Scope ring_scope.
Ltac Zmodp2_ringify := repeat match goal with
| [ |- context[Zmodp2.mul ?a ?b]] => have ->: (Zmodp2.mul a b) = a * b => //
| [ |- context[Zmodp2.add ?a (Zmodp2.opp ?b)]] => have ->: (Zmodp2.add a (Zmodp2.opp b)) = a - b => //
| [ |- context[Zmodp2.opp ?a]] => have ->: Zmodp2.opp a = -a => //
| [ |- context[Zmodp2.add ?a ?b]] => have ->: (Zmodp2.add a b) = a + b => //
| [ |- context[Zmodp2.one] ] => have ->: Zmodp2.one = 1 => //
| [ |- context[Zmodp2.zero] ] => have ->: Zmodp2.zero = 0 => //
end.
Close Scope ring_scope.
\ No newline at end of file
......@@ -3,6 +3,7 @@ From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq choice.
From mathcomp Require Import fintype ssralg finalg.
From Tweetnacl.High Require Import Zmodp.
From Tweetnacl.High Require Import Zmodp2.
From Tweetnacl.High Require Import GRing_tools.
Require Import Ring.
Open Scope ring_scope.
......@@ -10,16 +11,16 @@ Import GRing.Theory.
Import Zmodp2.
Import BinInt.
Lemma expr3 : forall x:Zmodp2.type, x^+3 = x*x*x :> Zmodp2.type.
Proof. move => x; rewrite ?exprSr expr0 GRing.mul1r //. Qed.
(* Lemma expr3 : forall x:Zmodp2.type, x^+3 = x*x*x :> Zmodp2.type. *)
(* Proof. move => x; rewrite ?exprSr expr0 GRing.mul1r //. Qed. *)
Lemma expr3' : forall x:Zmodp.type, (x^+3 = x*x*x)%R.
Proof. move => x; rewrite ?exprSr expr0 GRing.mul1r //. Qed.
(* Lemma expr3' : forall x:Zmodp.type, (x^+3 = x*x*x)%R. *)
(* Proof. move => x; rewrite ?exprSr expr0 GRing.mul1r //. Qed. *)
Ltac ring_simplify_this :=
(* Ltac ring_simplify_this :=
repeat match goal with
| _ => rewrite expr2
| _ => rewrite expr3
| _ => rewrite GRing.exprS
| _ => rewrite GRing.expr0
| _ => rewrite GRing.mul1r
| _ => rewrite GRing.mulr1
| _ => rewrite GRing.mul0r
......@@ -29,49 +30,29 @@ Ltac ring_simplify_this :=
| _ => rewrite GRing.addr0
| _ => done
end.
*)
Local Ltac unfolds := ring_unfold; Zmodp2_unfold.
Ltac ringify := Zmodp_ringify ; Zmodp2_ringify.
Lemma pi_2 : Zmodp.pi 2 = 2%:R.
Proof. by apply/eqP ; zmodp_compute. Qed.
Ltac ringify := repeat match goal with
| [ |- context[Zmodp.pi 2]] => rewrite pi_2
| [ |- context[Zmodp.mul ?a ?b]] => have ->: (Zmodp.mul a b) = a * b => //
| [ |- context[Zmodp.add ?a (Zmodp.opp ?b)]] => have ->: (Zmodp.add a (Zmodp.opp b)) = a - b => //
| [ |- context[Zmodp.opp ?a]] => have ->: Zmodp.opp a = -a => //
| [ |- context[Zmodp.add ?a ?b]] => have ->: (Zmodp.add a b) = a + b => //
| [ |- context[Zmodp2.mul ?a ?b]] => have ->: (Zmodp2.mul a b) = a * b => //
| [ |- context[Zmodp2.add ?a ?b]] => have ->: (Zmodp2.add a b) = a + b => //
| [ |- context[Zmodp.one] ] => have ->: Zmodp.one = 1 => //
| [ |- context[Zmodp.zero] ] => have ->: Zmodp.zero = 0 => //
end.
Ltac do_ := unfolds ; ringify ; ring_simplify_this.
(*
* Operations of the form (a , 0) op (b , 0)
*)
Lemma Zmodp2_add_Zmodp_a0 a b: Zmodp2 a 0 + Zmodp2 b 0 = Zmodp2 (a + b) 0.
Proof.
rewrite /GRing.add /= /add /=.
ringify ; ring_simplify_this.
Qed.
Proof. do_. Qed.
Lemma Zmodp2_opp_Zmodp_a0 a: - Zmodp2 a 0 = Zmodp2 (-a) 0.
Proof.
rewrite /GRing.opp /= /opp /=.
ringify ; ring_simplify_this.
Qed.
Proof. do_. Qed.
Lemma Zmodp2_sub_Zmodp_a0 a b: Zmodp2 a 0 - Zmodp2 b 0 = Zmodp2 (a - b) 0.
Proof.
rewrite /GRing.add /= /add /=.
ringify ; ring_simplify_this.
Qed.
Proof. do_. Qed.
Lemma Zmodp2_mul_Zmodp_a0 a b :Zmodp2 a 0 * Zmodp2 b 0 = Zmodp2 (a * b) 0.
Proof.
rewrite /GRing.mul /= /mul /=.
ringify ; ring_simplify_this.
Qed.
Proof. do_. Qed.
Lemma Zmodp2_pow_Zmodp_a0 : forall n a, (Zmodp2 a 0) ^+ n = Zmodp2 (a^+n) 0.
Proof.
......@@ -95,30 +76,16 @@ Qed.
* Operations of the form (a , 0) op (b , 0)
*)
Lemma Zmodp2_add_Zmodp_0a a b: Zmodp2 0 a + Zmodp2 0 b = Zmodp2 0 (a + b).
Proof.
rewrite /GRing.add /= /add /=.
ringify ; ring_simplify_this.
Qed.
Proof. do_. Qed.
Lemma Zmodp2_opp_Zmodp_0a a: - Zmodp2 0 a = Zmodp2 0 (-a).
Proof.
rewrite /GRing.opp /= /opp /=.
ringify ; ring_simplify_this.
Qed.
Proof. do_. Qed.
Lemma Zmodp2_sub_Zmodp_0a a b: Zmodp2 0 a - Zmodp2 0 b = Zmodp2 0 (a - b).
Proof.
rewrite /GRing.add /= /add /=.
ringify ; ring_simplify_this.
Qed.
Proof. do_. Qed.
Lemma Zmodp2_mul_Zmodp_0a a b: Zmodp2 0 a * Zmodp2 0 b = Zmodp2 (2%:R * a * b) 0.
Proof.
rewrite /GRing.mul /= /mul /=.
ringify ; ring_simplify_this.
by rewrite GRing.mulrA.
Qed.
Proof. by do_; rewrite GRing.mulrA. Qed.
Lemma Zmodp2_inv_Zmodp_0a a :(Zmodp2 0 a)^-1 = Zmodp2 0 ((2%:R * a)^-1).
Proof.
......@@ -140,30 +107,13 @@ Qed.
Lemma Zmodp2_mul_Zmodp_ab1 a b: Zmodp2 a 0 * Zmodp2 0 b = Zmodp2 0 (a * b).
Proof.
rewrite /GRing.mul /= /mul /=.
ringify ; ring_simplify_this.
Qed.
Proof. do_. Qed.
Lemma Zmodp2_mul_Zmodp_ab2 a b: Zmodp2 0 a * Zmodp2 b 0 = Zmodp2 0 (a * b).
Proof.
rewrite /GRing.mul /= /mul /=.
ringify ; ring_simplify_this.
Qed.
Proof. do_. Qed.
Lemma Zmodp_mul_comm_2 (a:Zmodp.type) : 2%:R * a = a * 2%:R.
Proof. by rewrite /GRing.mul /= Zmodp_ring.mul_comm. Qed.
Proof. by rewrite GRing.mulrC. Qed.
(*
* Big rewrite tactic
......
......@@ -2,7 +2,7 @@ Set Warnings "-notation-overridden,-parsing".
From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq choice.
From mathcomp Require Import fintype ssralg finalg.
Require Import ZArith ZArith.Znumtheory.
From Tweetnacl.High Require Import prime_and_legendre Zmodp.
From Tweetnacl.High Require Import prime_and_legendre Zmodp GRing_tools.
From Reciprocity Require Import Reciprocity.Reciprocity.
Import BinInt.
......@@ -94,8 +94,6 @@ Qed.
Open Scope Z.
Local Notation "Z.R A" := (Zmodp.repr A) (at level 30).
Lemma x_square_minus_x: forall (x:Zmodp.type),
exists (y:Zmodp.type), (y^+2 = x \/ (Zmodp.pi 2)* y^+2 = x)%R.
Proof.
......@@ -129,7 +127,7 @@ Proof.
* exfalso.
clear Eulers_Criterion Eulers_Criterion2 n0 Prime2.
rewrite modZp in n.
have HP : 0 <= (Z.R x) < p by rewrite -modZp ; apply Z.mod_pos_bound ; rewrite /p -lock.
have HP : 0 <= (Zmodp.repr x) < p by rewrite -modZp ; apply Z.mod_pos_bound ; rewrite /p -lock.
move: n.
have Hp : p <> 0 by rewrite /p -lock.
have : Znumtheory.rel_prime p 28948022309329048855892746252171976963317496166410141009864396001978282409975.
......@@ -137,13 +135,13 @@ Proof.
apply Znumtheory.rel_prime_le_prime => //=.
by rewrite /p -lock.
move: e.
move/(Znumtheory.Zmod_divide (28948022309329048855892746252171976963317496166410141009864396001978282409975 * Z.R x) p Hp).
move/(Znumtheory.Zmod_divide (28948022309329048855892746252171976963317496166410141009864396001978282409975 * Zmodp.repr x) p Hp).
move/Znumtheory.Gauss.
move=> H/H.
move/Znumtheory.Zdivide_bounds.
move=> H'/H'.
have ->: Z.abs p = p by rewrite /p -lock.
have ->: Z.abs (Z.R x) = (Z.R x).
have ->: Z.abs (Zmodp.repr x) = (Zmodp.repr x).
rewrite Z.abs_eq_iff; omega.
move => H''.
omega.
......@@ -185,19 +183,6 @@ Qed.
Close Scope Z.
Local Ltac ring_simplify_this :=
repeat match goal with
| _ => rewrite expr2
| _ => rewrite GRing.mul1r
| _ => rewrite GRing.mulr1
| _ => rewrite GRing.mul0r
| _ => rewrite GRing.mulr0
| _ => rewrite GRing.add0r
| _ => rewrite GRing.oppr0
| _ => rewrite GRing.addr0
| _ => done
end.
Lemma forall_x_2_0_sqrt (x:Zmodp.type) : x ^+ 2 = 0 -> x = 0.
Proof.
move/eqP.
......
......@@ -17,7 +17,6 @@ Proof. exact: oner_neq0. Qed.
Lemma asq_neq4 : (a ^+ 2 != 4%:R).
Proof.
rewrite expr2 /a.
change (Zmodp2.piZ (486662, 0%Z)) with (Zmodp2.pi (Zmodp.pi 486662, Zmodp.pi 0)).
rewrite Zmodp2_mulE /=.
apply/eqP => H.
inversion H ; clear H.
......
......@@ -10,6 +10,7 @@ From Tweetnacl.High Require Import Zmodp2_rules.
From Tweetnacl.High Require Import curve25519_Fp2.
From Tweetnacl.High Require Import curve25519_Fp_twist25519_Fp_eq.
From Tweetnacl.High Require Import Zmodp.
From Tweetnacl.High Require Import GRing_tools.
Require Import Ring.
Require Import ZArith.
......@@ -33,13 +34,12 @@ oncurve curve25519_Fp_mcuType (EC_In x y) ->
Proof.
move => x y /=.
rewrite /a /b.
rewrite ?expr2 ?expr3 ?expr3'.
ring_simplify_this.
rewrite ?Zmodp2_mulE /= ?Zmodp2_addE /=.
rewrite /curve25519_Fp.a /curve25519_Fp.b.
ring_simplify_this.
move/eqP => -> /=.
apply/eqP.
f_equal.
apply eq_refl.
Qed.
Local Lemma on_curve_Fp_to_Fp2 : forall (p: point Zmodp.type),
......@@ -95,7 +95,7 @@ Proof.
move => p q.
have [p' Hp']: exists (p': mc curve25519_Fp2_mcuType), p' = curve25519_Fp_to_Fp2 p by exists (curve25519_Fp_to_Fp2 p).
have [q' Hq']: exists (q': mc curve25519_Fp2_mcuType), q' = curve25519_Fp_to_Fp2 q by exists (curve25519_Fp_to_Fp2 q).
rewrite /GRing.add /=.
ring_unfold.
apply mc_eq.
rewrite -(curve25519_add_Fp_to_Fp2' _ _ _ _ Hp' Hq') Hp' Hq'.
reflexivity.
......@@ -105,7 +105,7 @@ Lemma nP_is_nP2 : forall (n:nat) (p: mc curve25519_Fp_mcuType),
curve25519_Fp_to_Fp2 (p *+ n) = (curve25519_Fp_to_Fp2 p) *+n.
Proof.
elim => [|n IHn] p.
rewrite ?GRing.mulr0n => /=.
ring_simplify_this.
exact: mc_eq.
by rewrite ?GRing.mulrS -IHn curve25519_add_Fp_to_Fp2.
Qed.
......
......@@ -16,6 +16,7 @@ From Tweetnacl.High Require Import curve25519_Fp_twist25519_Fp_eq.
From Tweetnacl.High Require Import curve25519_Fp_incl_Fp2.
From Tweetnacl.High Require Import twist25519_Fp_incl_Fp2.
From Tweetnacl.High Require Import Zmodp.
From Tweetnacl.High Require Import GRing_tools.
Require Import Ring.
Require Import ZArith.
......@@ -85,21 +86,21 @@ Local Notation "p '/p'" := (Fp_to_Fp2 p) (at level 40).
Local Lemma temp: forall x xp yp1 yp2,
xp = Zmodp2.Zmodp2 x 0 ->
oncurve curve25519_Fp2_mcuType (|xp, Zmodp2.Zmodp2 yp1 yp2|) ->
yp1 ^+ 2 + 2%:R * yp2 ^+ 2 = x * x * x + Zmodp.pi 486662 * (x * x) + x /\
yp1 ^+ 2 + 2%:R * yp2 ^+ 2 = x * (x * x) + Zmodp.pi 486662 * (x * x) + x /\
2%:R * (yp1 * yp2) = 0.
Proof.
move => x xp yp1 yp2 Hx.
rewrite /oncurve /= /a /b => Hp'.
have : (Zmodp2.Zmodp2 yp1 yp2) ^+ 2 == (Zmodp2.Zmodp2 x 0) ^+ 3 + Zmodp2.pi (Zmodp.pi 486662, 0) * (Zmodp2.Zmodp2 x 0) ^+ 2 + (Zmodp2.Zmodp2 x 0).
rewrite -Hx -(GRing.mul1r (Zmodp2.Zmodp2 yp1 yp2 ^+ 2)) //.
rewrite expr3 ?expr2.
ring_simplify_this.
Zmodpify => /=.
have ->: Zmodp2.Zmodp2 yp1 yp2 * Zmodp2.Zmodp2 yp1 yp2 = Zmodp2.Zmodp2 (yp1^+2 + 2%:R * yp2^+2) (2%:R * yp1 * yp2).