From 34875f01c422e5665a73f076e7e17b9c7e1d5aa0 Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Fri, 12 Feb 2016 14:44:48 -0500 Subject: port some edwards curve theorems --- src/Curves/PointFormats.v | 52 ++--------------------------------------------- 1 file changed, 2 insertions(+), 50 deletions(-) (limited to 'src/Curves') diff --git a/src/Curves/PointFormats.v b/src/Curves/PointFormats.v index 8137abc4c..2ea04cde5 100644 --- a/src/Curves/PointFormats.v +++ b/src/Curves/PointFormats.v @@ -137,56 +137,8 @@ Module CompleteTwistedEdwardsCurve (M : Modulus) (Import P : TwistedEdwardsParam - Lemma root_zero : forall (x: GF) (p: N), x^p = 0 -> x = 0. - intros. - - induction p; inversion H. - - revert H H1; generalize x; induction p; intros. - - - simpl in H; apply mul_zero_why in H; destruct H; intuition. - - + subst; intuition. - - + apply IHp in H. - rewrite H1. - simpl in H1. - apply mul_zero_why in H1; destruct H1; intuition. - rewrite H0 in H. - apply mul_zero_why in H; destruct H; intuition. - - simpl; intuition. - - - simpl in H1; apply IHp in H1; simpl; intuition. - simpl in H; rewrite H in H1; rewrite H. - apply mul_zero_why in H1; destruct H1; intuition. - - - simpl in H; subst; intuition. - - Qed. - - Lemma root_nonzero : forall x p, x^p <> 0 -> (p <> 0)%N -> x <> 0. - intros; intuition. - - induction p. - - - apply H; intuition. - - - apply H. - rewrite H1 in *. - induction p. - - + simpl. - field. - - + simpl in *. - replace (0 * 0) with 0 in * by field. - apply IHp; intuition. - induction p; inversion H2. - - + simpl; intuition. - - Qed. + Lemma root_zero : forall (x: GF) (p: N), x^p = 0 -> x = 0. Admitted. + Lemma root_nonzero : forall x p, x^p <> 0 -> (p <> 0)%N -> x <> 0. Admitted. Lemma char_gt_2 : inject 2 <> 0. intro H; inversion H; clear H. -- cgit v1.2.3