diff options
author | Andres Erbsen <andreser@mit.edu> | 2016-03-03 16:09:34 -0500 |
---|---|---|
committer | Robert Sloan <varomodt@gmail.com> | 2016-06-22 13:42:16 -0400 |
commit | 4fa76e9d403d0d4f7ce8969acbe9612aa8fc3f56 (patch) | |
tree | 12d65cad1264f6fca8c13251c95cfb8d6ae19e36 /src | |
parent | b0293a7fef2ed784f30fb81dcd8c835f435d71eb (diff) |
CompleteEdwardsCurveTheorems: associativity proof that times out on Qed
Diffstat (limited to 'src')
-rw-r--r-- | src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v | 162 | ||||
-rw-r--r-- | src/ModularArithmetic/FNsatz.v | 40 | ||||
-rw-r--r-- | src/ModularArithmetic/ModularArithmeticTheorems.v | 10 | ||||
-rw-r--r-- | src/ModularArithmetic/PrimeFieldTheorems.v | 8 |
4 files changed, 65 insertions, 155 deletions
diff --git a/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v b/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v index 5e6fd7b42..01b3584c0 100644 --- a/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v +++ b/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v @@ -1,6 +1,7 @@ Require Export Crypto.Spec.CompleteEdwardsCurve. Require Import Crypto.ModularArithmetic.FField. +Require Import Crypto.ModularArithmetic.FNsatz. Require Import Crypto.CompleteEdwardsCurve.Pre. Require Import Crypto.ModularArithmetic.PrimeFieldTheorems. Require Import Eqdep_dec. @@ -22,6 +23,12 @@ Section CompleteEdwardsCurveTheorems. Add Field Ffield_notConstant : (OpaqueFieldTheory q) (constants [notConstant]). + Ltac clear_prm := + generalize dependent a; intro a; intros; + generalize dependent d; intro d; intros; + generalize dependent prime_q; intro prime_q; intros; + generalize dependent q; intro q; intros; + clear prm. Lemma point_eq : forall p1 p2, p1 = p2 -> forall pf1 pf2, mkPoint p1 pf1 = mkPoint p2 pf2. @@ -48,157 +55,10 @@ Section CompleteEdwardsCurveTheorems. Lemma twistedAddAssoc : forall A B C, (A+(B+C) = (A+B)+C)%E. Proof. - intros; Edefn; F_field_simplify_eq. - - (* nsatz. *) (* requires IntegralDomain (F q), then gives stack overflow *) - admit. (*sage -c " -R.<d,a,xA,yA,xB,yB,xC,yC> = PolynomialRing(QQ,8,order='invlex') -I = R.ideal([ - (a * (xA * xA) + yA * yA) - (1 + d * (xA * xA) * (yA * yA)), - (a * (xB * xB) + yB * yB) - (1 + d * (xB * xB) * (yB * yB)), - (a * (xC * xC) + yC * yC) - (1 + d * (xC * xC) * (yC * yC)) -]) - -print ((- xA * xA * xA * yB * yB * yB * yB * yC * yC * xB * xB * xB * xC * d * d * d * yA * yA - - xA * xA * xA * yB * yB * yB * yC * yC * yC * a * xB * xB * xC * xC * d * d + - xA * xA * xA * yB * yB * yB * yC * a * xB * xB * xB * xB * xC * xC * d * d * d * yA * yA - - xA * xA * xA * yB * yB * yB * yC * xB * xB * d * d * yA * yA + - xA * xA * xA * yB * yB * yC * yC * a * a * xB * xB * xB * xC * xC * xC * d * d - - xA * xA * xA * yB * yB * yC * yC * a * xB * xC * d + - xA * xA * xA * yB * yB * a * xB * xB * xB * xC * d * d * yA * yA + - xA * xA * xA * yB * yC * a * a * xB * xB * xC * xC * d + - xA * xA * yB * yB * yB * yB * yC * yC * yC * xB * xC * xC * d * d * yA + - xA * xA * yB * yB * yB * yB * yC * xB * xB * xB * xC * xC * d * d * d * yA * yA * yA + - xA * xA * yB * yB * yB * yC * yC * xB * xB * xB * xB * xC * d * d * d * yA * yA * yA + - xA * xA * yB * yB * yB * yC * yC * xC * d * yA - - xA * xA * yB * yB * yB * xB * xB * xC * d * d * yA * yA * yA - - (1 + 1) * xA * xA * yB * yB * yC * a * xB * xC * xC * d * yA - - xA * xA * yB * yB * yC * xB * xB * xB * d * d * yA * yA * yA + - xA * xA * yB * yC * yC * a * a * xB * xB * xB * xB * xC * xC * xC * d * d * yA - - (1 + 1) * xA * xA * yB * yC * yC * a * xB * xB * xC * d * yA + - xA * xA * yC * a * a * xB * xB * xB * xC * xC * d * yA - - xA * yB * yB * yB * yB * yC * yC * xB * xC * xC * xC * d * d * yA * yA + - xA * yB * yB * yB * yC * xC * xC * d * yA * yA + - xA * yB * yB * yC * yC * xB * xC * d + (1 + 1) * xA * yB * yB * yC * yC * xB * xC * d * yA * yA + - xA * yB * yC * yC * yC * a * xB * xB * xB * xB * xC * xC * d * d * yA * yA - - xA * yB * yC * a * xB * xB * xC * xC * d - (1 + 1) * xA * yB * yC * a * xB * xB * xC * xC * d * yA * yA + - xA * yB * yC - xA * yC * yC * a * xB * xB * xB * xC * d * yA * yA - - xA * a * xB * xC - yB * yB * yB * yC * yC * xB * xB * xC * xC * xC * d * d * yA * yA * yA - - yB * yB * yC * yC * yC * xB * xB * xB * xC * xC * d * d * yA * yA * yA - - yB * yB * yC * xB * xC * xC * d * yA + yB * yB * yC * xB * xC * xC * d * yA * yA * yA - - yB * yC * yC * xB * xB * xC * d * yA + yB * yC * yC * xB * xB * xC * d * yA * yA * yA + - yB * xC * yA + yC * xB * yA - ( - - xA * xA * xA * yB * yB * yB * yB * yC * yC * xB * xC * d * d * yA * yA - - xA * xA * xA * yB * yB * yB * yC * yC * yC * xB * xB * d * d * yA * yA + - xA * xA * xA * yB * yB * a * a * xB * xB * xB * xC * xC * xC * d * d * yA * yA + - xA * xA * xA * yB * yC * a * a * xB * xB * xB * xB * xC * xC * d * d * yA * yA + - xA * xA * yB * yB * yB * yB * yC * yC * yC * xB * xB * xB * xC * xC * d * d * d * yA + - xA * xA * yB * yB * yB * yB * yC * xB * xC * xC * d * d * yA * yA * yA + - xA * xA * yB * yB * yB * yC * yC * a * xB * xB * xB * xB * xC * xC * xC * d * d * d * yA + - xA * xA * yB * yB * yB * yC * yC * xC * d * yA - - xA * xA * yB * yB * yB * a * xB * xB * xC * xC * xC * d * d * yA * yA * yA - - xA * xA * yB * yB * yC * yC * yC * xB * xB * xB * d * d * yA * yA * yA + - xA * xA * yB * yB * yC * yC * yC * xB * d * yA - - (1 + 1) * xA * xA * yB * yB * yC * a * xB * xC * xC * d * yA - - xA * xA * yB * yB * yC * xB * d * yA + - xA * xA * yB * yC * yC * a * xB * xB * xB * xB * xC * d * d * yA * yA * yA - - (1 + 1) * xA * xA * yB * yC * yC * a * xB * xB * xC * d * yA + - xA * xA * yB * a * a * xB * xB * xC * xC * xC * d * yA - - xA * xA * yB * a * xB * xB * xC * d * yA + xA * xA * yC * a * a * xB * xB * xB * xC * xC * d * yA - - xA * yB * yB * yB * yB * yC * yC * xB * xB * xB * xC * xC * xC * d * d * d * yA * yA + - xA * yB * yB * yB * yC * yC * yC * xB * xB * xB * xB * xC * xC * d * d * d * yA * yA - - xA * yB * yB * yB * yC * yC * yC * xB * xB * xC * xC * d * d + - xA * yB * yB * yB * yC * xC * xC * d * yA * yA + - xA * yB * yB * yC * yC * a * xB * xB * xB * xC * xC * xC * d * d + - (1 + 1) * xA * yB * yB * yC * yC * xB * xC * d * yA * yA - - xA * yB * yB * a * xB * xC * xC * xC * d * yA * yA + - xA * yB * yB * xB * xC * d * yA * yA + xA * yB * yC * yC * yC * xB * xB * d * yA * yA - - (1 + 1) * xA * yB * yC * a * xB * xB * xC * xC * d * yA * yA - - xA * yB * yC * xB * xB * d * yA * yA + xA * yB * yC - - xA * yC * yC * a * xB * xB * xB * xC * d * yA * yA - - xA * a * xB * xC - yB * yB * yB * yC * yC * xB * xB * xC * xC * xC * d * d * yA - - yB * yB * yC * yC * yC * xB * xB * xB * xC * xC * d * d * yA + - yB * xC * yA + yC * xB * yA)) - in I)"*) - - admit. (* nonzero demonimator conditions, to be resolved as in ExtendedCoordinates.v *) - - (* nsatz. *) (* requires IntegralDomain (F q), then gives stack overflow *) - admit. (* sage -c " -R.<d,a,xA,yA,xB,yB,xC,yC> = PolynomialRing(QQ,8,order='invlex') -I = R.ideal([ - (a * (xA * xA) + yA * yA) - (1 + d * (xA * xA) * (yA * yA)), - (a * (xB * xB) + yB * yB) - (1 + d * (xB * xB) * (yB * yB)), - (a * (xC * xC) + yC * yC) - (1 + d * (xC * xC) * (yC * yC)) -]) - -print (((- yA * yA * yA * yB * yB * yB * yB * yC * yC * xB * xB * xB * xC * 1 * d * d * d * xA * xA - - yA * yA * yA * yB * yB * yB * yC * yC * yC * xB * xB * xC * xC * d * d + - yA * yA * yA * yB * yB * yB * yC * a * xB * xB * xB * xB * xC * xC * 1 * d * d * d * xA * xA - - yA * yA * yA * yB * yB * yB * yC * xB * xB * 1 * 1 * d * d * xA * xA + - yA * yA * yA * yB * yB * yC * yC * a * xB * xB * xB * xC * xC * xC * d * d - - yA * yA * yA * yB * yB * yC * yC * xB * xC * 1 * d + - yA * yA * yA * yB * yB * a * xB * xB * xB * xC * 1 * 1 * d * d * xA * xA + - yA * yA * yA * yB * yC * a * xB * xB * xC * xC * 1 * d - - yA * yA * yB * yB * yB * yB * yC * yC * yC * xB * xC * xC * d * d * xA - - yA * yA * yB * yB * yB * yB * yC * a * xB * xB * xB * xC * xC * 1 * d * d * d * xA * xA * xA - - yA * yA * yB * yB * yB * yC * yC * a * xB * xB * xB * xB * xC * 1 * d * d * d * xA * xA * xA - - yA * yA * yB * yB * yB * yC * yC * xC * 1 * d * xA + - yA * yA * yB * yB * yB * a * xB * xB * xC * 1 * 1 * d * d * xA * xA * xA + - yA * yA * yB * yB * yC * a * xB * xB * xB * 1 * 1 * d * d * xA * xA * xA + - (1 + 1) * yA * yA * yB * yB * yC * a * xB * xC * xC * 1 * d * xA - - yA * yA * yB * yC * yC * a * a * xB * xB * xB * xB * xC * xC * xC * d * d * xA + - (1 + 1) * yA * yA * yB * yC * yC * a * xB * xB * xC * 1 * d * xA - - yA * yA * yC * a * a * xB * xB * xB * xC * xC * 1 * d * xA - - yA * yB * yB * yB * yB * yC * yC * a * xB * xC * xC * xC * d * d * xA * xA + - yA * yB * yB * yB * yC * a * xC * xC * 1 * d * xA * xA + - (1 + 1) * yA * yB * yB * yC * yC * a * xB * xC * 1 * d * xA * xA + - yA * yB * yB * yC * yC * xB * xC * 1 * 1 * 1 * d + - yA * yB * yC * yC * yC * a * a * xB * xB * xB * xB * xC * xC * d * d * xA * xA - - (1 + 1) * yA * yB * yC * a * a * xB * xB * xC * xC * 1 * d * xA * xA - - yA * yB * yC * a * xB * xB * xC * xC * 1 * 1 * 1 * d + - yA * yB * yC * 1 * 1 * 1 * 1 - yA * yC * yC * a * a * xB * xB * xB * xC * 1 * d * xA * xA - - yA * a * xB * xC * 1 * 1 * 1 * 1 + - yB * yB * yB * yC * yC * a * a * xB * xB * xC * xC * xC * d * d * xA * xA * xA + - yB * yB * yC * yC * yC * a * a * xB * xB * xB * xC * xC * d * d * xA * xA * xA - - yB * yB * yC * a * a * xB * xC * xC * 1 * d * xA * xA * xA + - yB * yB * yC * a * xB * xC * xC * 1 * 1 * 1 * d * xA - - yB * yC * yC * a * a * xB * xB * xC * 1 * d * xA * xA * xA + - yB * yC * yC * a * xB * xB * xC * 1 * 1 * 1 * d * xA - - yB * a * xC * 1 * 1 * 1 * 1 * xA - yC * a * xB * 1 * 1 * 1 * 1 * xA) - - (- yA * yA * yA * yB * yB * yB * yB * yC * yC * xB * xC * d * d * xA * xA - - yA * yA * yA * yB * yB * yB * yC * yC * yC * xB * xB * d * d * xA * xA + - yA * yA * yA * yB * yB * a * a * xB * xB * xB * xC * xC * xC * d * d * xA * xA + - yA * yA * yA * yB * yC * a * a * xB * xB * xB * xB * xC * xC * d * d * xA * xA - - yA * yA * yB * yB * yB * yB * yC * yC * yC * xB * xB * xB * xC * xC * 1 * d * d * d * xA - - yA * yA * yB * yB * yB * yB * yC * a * xB * xC * xC * d * d * xA * xA * xA - - yA * yA * yB * yB * yB * yC * yC * a * xB * xB * xB * xB * xC * xC * xC * 1 * d * d * d * xA - - yA * yA * yB * yB * yB * yC * yC * xC * 1 * d * xA + - yA * yA * yB * yB * yB * a * a * xB * xB * xC * xC * xC * d * d * xA * xA * xA + - yA * yA * yB * yB * yC * yC * yC * a * xB * xB * xB * d * d * xA * xA * xA - - yA * yA * yB * yB * yC * yC * yC * xB * 1 * d * xA + - (1 + 1) * yA * yA * yB * yB * yC * a * xB * xC * xC * 1 * d * xA + - yA * yA * yB * yB * yC * xB * 1 * 1 * 1 * d * xA - - yA * yA * yB * yC * yC * a * a * xB * xB * xB * xB * xC * d * d * xA * xA * xA + - (1 + 1) * yA * yA * yB * yC * yC * a * xB * xB * xC * 1 * d * xA - - yA * yA * yB * a * a * xB * xB * xC * xC * xC * 1 * d * xA + - yA * yA * yB * a * xB * xB * xC * 1 * 1 * 1 * d * xA - - yA * yA * yC * a * a * xB * xB * xB * xC * xC * 1 * d * xA - - yA * yB * yB * yB * yB * yC * yC * a * xB * xB * xB * xC * xC * xC * 1 * d * d * d * xA * xA + - yA * yB * yB * yB * yC * yC * yC * a * xB * xB * xB * xB * xC * xC * 1 * d * d * d * xA * xA - - yA * yB * yB * yB * yC * yC * yC * xB * xB * xC * xC * 1 * 1 * d * d + - yA * yB * yB * yB * yC * a * xC * xC * 1 * d * xA * xA + - yA * yB * yB * yC * yC * a * xB * xB * xB * xC * xC * xC * 1 * 1 * d * d + - (1 + 1) * yA * yB * yB * yC * yC * a * xB * xC * 1 * d * xA * xA - - yA * yB * yB * a * a * xB * xC * xC * xC * 1 * d * xA * xA + - yA * yB * yB * a * xB * xC * 1 * 1 * 1 * d * xA * xA + - yA * yB * yC * yC * yC * a * xB * xB * 1 * d * xA * xA - - (1 + 1) * yA * yB * yC * a * a * xB * xB * xC * xC * 1 * d * xA * xA - - yA * yB * yC * a * xB * xB * 1 * 1 * 1 * d * xA * xA + - yA * yB * yC * 1 * 1 * 1 * 1 - yA * yC * yC * a * a * xB * xB * xB * xC * 1 * d * xA * xA - - yA * a * xB * xC * 1 * 1 * 1 * 1 + - yB * yB * yB * yC * yC * a * xB * xB * xC * xC * xC * 1 * 1 * d * d * xA + - yB * yB * yC * yC * yC * a * xB * xB * xB * xC * xC * 1 * 1 * d * d * xA - - yB * a * xC * 1 * 1 * 1 * 1 * xA - yC * a * xB * 1 * 1 * 1 * 1 * xA)) in I)" -*) - - admit. (* nonzero demonimator conditions, to be resolved as in ExtendedCoordinates.v *) + (* The Ltac takes ~15s, the Qed takes longer than I have had patience for *) + Edefn; F_field_simplify_eq; try abstract (rewrite ?@F_pow_2_r in *; clear_prm; F_nsatz); + repeat split; match goal with [ |- _ = 0%F -> False ] => admit end; + fail "unreachable". Admitted. Lemma zeroIsIdentity : forall P, (P + zero = P)%E. diff --git a/src/ModularArithmetic/FNsatz.v b/src/ModularArithmetic/FNsatz.v new file mode 100644 index 000000000..a0f34073d --- /dev/null +++ b/src/ModularArithmetic/FNsatz.v @@ -0,0 +1,40 @@ +Require Import Crypto.ModularArithmetic.PrimeFieldTheorems. +Require Export Crypto.ModularArithmetic.FField. +Require Import Nsatz. + +Ltac FqAsIntegralDomain := + lazymatch goal with [H:Znumtheory.prime ?q |- _ ] => + pose proof (_:@Integral_domain.Integral_domain (F q) _ _ _ _ _ _ _ _ _ _) as FqIntegralDomain; + lazymatch type of FqIntegralDomain with @Integral_domain.Integral_domain _ _ _ _ _ _ _ _ ?ringOps ?ringOk ?ringComm => + generalize dependent ringComm; intro Cring; + generalize dependent ringOk; intro Ring; + generalize dependent ringOps; intro RingOps; + lazymatch type of RingOps with @Ncring.Ring_ops ?t ?z ?o ?a ?m ?s ?p ?e => + generalize dependent e; intro equiv; + generalize dependent p; intro opp; + generalize dependent s; intro sub; + generalize dependent m; intro mul; + generalize dependent a; intro add; + generalize dependent o; intro one; + generalize dependent z; intro zero; + generalize dependent t; intro R + end + end; intros; + clear q H + end. + +Ltac fixed_equality_to_goal H x y := generalize (psos_r1 x y H); clear H. +Ltac fixed_equalities_to_goal := + match goal with + | H:?x == ?y |- _ => fixed_equality_to_goal H x y + | H:_ ?x ?y |- _ => fixed_equality_to_goal H x y + | H:_ _ ?x ?y |- _ => fixed_equality_to_goal H x y + | H:_ _ _ ?x ?y |- _ => fixed_equality_to_goal H x y + | H:_ _ _ _ ?x ?y |- _ => fixed_equality_to_goal H x y + end. +Ltac fixed_nsatz := + intros; try apply psos_r1b; + lazymatch goal with + | |- @equality ?T _ _ _ => repeat fixed_equalities_to_goal; nsatz_generic 6%N 1%Z (@nil T) (@nil T) + end. +Ltac F_nsatz := abstract (FqAsIntegralDomain; fixed_nsatz). diff --git a/src/ModularArithmetic/ModularArithmeticTheorems.v b/src/ModularArithmetic/ModularArithmeticTheorems.v index 4602e8781..f39cc4176 100644 --- a/src/ModularArithmetic/ModularArithmeticTheorems.v +++ b/src/ModularArithmetic/ModularArithmeticTheorems.v @@ -581,6 +581,16 @@ Section VariousModulo. Fdefn. Qed. + Lemma F_pow_2_r : forall x : F m, x^2 = x*x. + Proof. + intros. ring. + Qed. + + Lemma F_pow_3_r : forall x : F m, x^3 = x*x*x. + Proof. + intros. ring. + Qed. + Lemma F_pow_add : forall (x : F m) k j, x ^ j * x ^ k = x ^ (j + k). Proof. intros. diff --git a/src/ModularArithmetic/PrimeFieldTheorems.v b/src/ModularArithmetic/PrimeFieldTheorems.v index 2e778dc5f..c41a64111 100644 --- a/src/ModularArithmetic/PrimeFieldTheorems.v +++ b/src/ModularArithmetic/PrimeFieldTheorems.v @@ -324,8 +324,8 @@ Section VariousModPrime. apply F_add_reg_l in opp_spec; auto. Qed. - Instance Fq_Ring_ops : @Ring_ops (F q) 0 1 add mul sub opp eq. - Instance Fq_Ring: @Ring (F q) 0 1 add mul sub opp eq Fq_Ring_ops. + Global Instance Fq_Ring_ops : @Ring_ops (F q) 0 1 add mul sub opp eq. + Global Instance Fq_Ring: @Ring (F q) 0 1 add mul sub opp eq Fq_Ring_ops. Proof. econstructor; eauto with typeclass_instances; unfold R2, equality, eq_notation, addition, add_notation, one, one_notation, @@ -333,12 +333,12 @@ Section VariousModPrime. sub_notation, opposite, opp_notation; intros; ring. Qed. - Instance Fq_Cring: @Cring (F q) 0 1 add mul sub opp eq Fq_Ring_ops Fq_Ring. + Global Instance Fq_Cring: @Cring (F q) 0 1 add mul sub opp eq Fq_Ring_ops Fq_Ring. Proof. repeat intro. apply F_mul_comm. Qed. - Instance Fq_Integral_domain : @Integral_domain (F q) 0 1 add mul sub opp eq Fq_Ring_ops Fq_Ring Fq_Cring. + Global Instance Fq_Integral_domain : @Integral_domain (F q) 0 1 add mul sub opp eq Fq_Ring_ops Fq_Ring Fq_Cring. Proof. econstructor; eauto using Fq_mul_zero_why, Fq_1_neq_0. Qed. |