From 45a6a17c06f45e81cadf18ef984ec7cdd94c11c1 Mon Sep 17 00:00:00 2001 From: Jade Philipoom Date: Tue, 16 Feb 2016 18:18:59 -0500 Subject: proved most of point encoding admits, fixed some build system issues (dead imports of PointFormats and Galois things) --- src/ModularArithmetic/PrimeFieldTheorems.v | 18 ++++++++++++++++++ 1 file changed, 18 insertions(+) (limited to 'src/ModularArithmetic') diff --git a/src/ModularArithmetic/PrimeFieldTheorems.v b/src/ModularArithmetic/PrimeFieldTheorems.v index 889b4fa3d..fe0398ff4 100644 --- a/src/ModularArithmetic/PrimeFieldTheorems.v +++ b/src/ModularArithmetic/PrimeFieldTheorems.v @@ -197,6 +197,24 @@ Section VariousModPrime. Proof. intros; field. (* TODO: Warning: Collision between bound variables ... *) Qed. + + Lemma F_eq_opp_zero : forall x : F q, 2 < q -> (x = opp x <-> x = 0). + Proof. + split; intro A. + + pose proof (F_opp_spec x) as opp_spec. + rewrite <- A in opp_spec. + replace (x + x) with (ZToField 2 * x) in opp_spec by ring. + apply Fq_mul_zero_why in opp_spec. + destruct opp_spec as [eq_2_0 | ?]; auto. + apply F_eq in eq_2_0. + rewrite FieldToZ_ZToField in eq_2_0. + replace (FieldToZ 0) with 0%Z in eq_2_0 by auto. + replace (2 mod q) with 2 in eq_2_0; try discriminate. + symmetry; apply Z.mod_small; omega. + + subst. + rewrite <- (F_opp_spec 0) at 1. + ring. + Qed. Lemma euler_criterion_F : forall (a : F q) (q_odd : 2 < q) (a_nonzero : a <> 0), (a ^ (Z.to_N (q / 2)) = 1) <-> isSquare a. -- cgit v1.2.3