From af5141847d7888e502e90b56646959fbf1070b76 Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Thu, 16 Feb 2017 23:56:47 -0500 Subject: WIP --- src/WeierstrassCurve/WeierstrassCurveTheorems.v | 126 +++--------------------- 1 file changed, 13 insertions(+), 113 deletions(-) (limited to 'src/WeierstrassCurve') diff --git a/src/WeierstrassCurve/WeierstrassCurveTheorems.v b/src/WeierstrassCurve/WeierstrassCurveTheorems.v index 5489a8ef0..bff8c2bc2 100644 --- a/src/WeierstrassCurve/WeierstrassCurveTheorems.v +++ b/src/WeierstrassCurve/WeierstrassCurveTheorems.v @@ -26,6 +26,13 @@ Module W. Local Notation "x ^ 2" := (x*x) (at level 30). Local Notation "x ^ 3" := (x*x^2) (at level 30). Context {discriminant_nonzero:4*a^3 + 27*b^2 <> 0}. + Program Definition inv (P:point) : point + := match W.coordinates P return F*F+_ with + | inl (x1, y1) => inl (x1, Fopp y1) + | _ => P + end. + Next Obligation. destruct P as [[[??]|[]]?]; cbv; trivial; fsatz. Qed. + Lemma same_x_same_y (xA yA : F) (A : yA ^ 2 = xA ^ 3 + a * xA + b) @@ -36,16 +43,14 @@ Module W. : yB = yA. Proof. fsatz. Qed. - Definition is_redundant {T} (x:T) := x. - Global Arguments is_redundant : simpl never. + Let is_redundant {T} (x:T) := x. Ltac clear_marked_redundant := repeat match goal with [H:?P, Hr:is_redundant ?P |- _] => clear H Hr end. - Ltac t_step := match goal with - | _ => exact _ + | _ => solve [ contradiction | trivial | exact _ ] | _ => intro | [ A : ?yA ^ 2 = ?xA ^ 3 + a * ?xA + b, B : ?yB ^ 2 = ?xB ^ 3 + a * ?xB + b, @@ -65,119 +70,14 @@ Module W. | |- context[?P] => unique pose proof (proj2_sig P); unique pose proof (proj2_sig P:(is_redundant _)) - | _ => progress cbv [eq W.eq W.add W.coordinates proj1_sig] in * - | _ => progress simpl in * + | _ => progress cbv [inv W.eq W.zero W.add W.coordinates proj1_sig] in * | _ => progress break_match | |- _ /\ _ => split | |- _ <-> _ => split - | _ => abstract (trivial || contradiction || clear_marked_redundant; fsatz) end. - Ltac t := repeat t_step. - - Program Definition inv (P:point) : point - := exist - _ - (match W.coordinates P return _ with - | inl (x1, y1) => inl (x1, Fopp y1) - | _ => P - end) - _. - Next Obligation. t. Qed. + Ltac t := repeat t_step; clear_marked_redundant. Global Instance commutative_group : abelian_group(eq:=W.eq)(op:=W.add)(id:=W.zero)(inv:=inv). - Proof. Time t. Time Qed. + Proof. t. all:try (abstract fsatz). Qed. + End W. End W. - -(* -Times for individual subgoal of the associativity proof: -Finished transaction in 0.169 secs (0.17u,0.s) (successful) -Finished transaction in 0.16 secs (0.159u,0.s) (successful) -Finished transaction in 0.722 secs (0.723u,0.s) (successful) -Finished transaction in 3.375 secs (3.373u,0.003s) (successful) -Finished transaction in 7.166 secs (7.166u,0.s) (successful) -Finished transaction in 1.862 secs (1.856u,0.003s) (successful) -Finished transaction in 3.6 secs (3.603u,0.s) (successful) -Finished transaction in 0.571 secs (0.569u,0.s) (successful) -Finished transaction in 1.956 secs (1.959u,0.s) (successful) -Finished transaction in 3.186 secs (3.186u,0.s) (successful) -Finished transaction in 1.265 secs (1.266u,0.s) (successful) -Finished transaction in 1.884 secs (1.883u,0.s) (successful) -Finished transaction in 0.762 secs (0.763u,0.s) (successful) -Finished transaction in 2.431 secs (2.433u,0.s) (successful) -Finished transaction in 1.662 secs (1.663u,0.s) (successful) -Finished transaction in 1.846 secs (1.846u,0.s) (successful) -Finished transaction in 1.853 secs (1.853u,0.s) (successful) -Finished transaction in 1.727 secs (1.73u,0.s) (successful) -Finished transaction in 1.771 secs (1.769u,0.s) (successful) -Finished transaction in 2.07 secs (2.073u,0.s) (successful) -Finished transaction in 5.765 secs (5.766u,0.s) (successful) -Finished transaction in 9.965 secs (9.966u,0.s) (successful) -Finished transaction in 3.917 secs (3.916u,0.s) (successful) -Finished transaction in 6.101 secs (6.099u,0.003s) (successful) -Finished transaction in 2.042 secs (2.043u,0.s) (successful) -Finished transaction in 5.398 secs (5.399u,0.s) (successful) -Finished transaction in 6.346 secs (6.346u,0.s) (successful) -Finished transaction in 4.726 secs (4.726u,0.s) (successful) -Finished transaction in 5.872 secs (5.876u,0.s) (successful) -Finished transaction in 1.852 secs (1.853u,0.s) (successful) -Finished transaction in 3.189 secs (3.189u,0.s) (successful) -Finished transaction in 1.489 secs (1.49u,0.s) (successful) -Finished transaction in 6.602 secs (6.603u,0.s) (successful) -Finished transaction in 12.172 secs (12.169u,0.003s) (successful) -Finished transaction in 4.668 secs (4.669u,0.s) (successful) -Finished transaction in 8.451 secs (8.449u,0.003s) (successful) -Finished transaction in 1.304 secs (1.303u,0.s) (successful) -Finished transaction in 4.818 secs (4.816u,0.003s) (successful) -Finished transaction in 7.557 secs (7.559u,0.s) (successful) -Finished transaction in 4.435 secs (4.436u,0.s) (successful) -Finished transaction in 7.915 secs (7.916u,0.s) (successful) -Finished transaction in 0.623 secs (0.623u,0.s) (successful) -Finished transaction in 2.145 secs (2.146u,0.s) (successful) -Finished transaction in 1.436 secs (1.436u,0.s) (successful) -Finished transaction in 2.091 secs (2.09u,0.s) (successful) -Finished transaction in 1.459 secs (1.46u,0.s) (successful) -Finished transaction in 1.371 secs (1.373u,0.s) (successful) -Finished transaction in 1.417 secs (1.416u,0.s) (successful) -Finished transaction in 1.757 secs (1.756u,0.s) (successful) -Finished transaction in 5.275 secs (5.276u,0.s) (successful) -Finished transaction in 8.736 secs (8.736u,0.s) (successful) -Finished transaction in 3.415 secs (3.416u,0.s) (successful) -Finished transaction in 5.508 secs (5.506u,0.003s) (successful) -Finished transaction in 1.881 secs (1.883u,0.s) (successful) -Finished transaction in 21.631 secs (21.629u,0.003s) (successful) -Finished transaction in 312.734 secs (312.723u,0.036s) (successful) -Finished transaction in 4.439 secs (4.436u,0.s) (successful) -Finished transaction in 6.267 secs (6.266u,0.003s) (successful) -Finished transaction in 1.241 secs (1.24u,0.s) (successful) -Finished transaction in 1.603 secs (1.603u,0.s) (successful) -Finished transaction in 1.824 secs (1.823u,0.s) (successful) -Finished transaction in 8.099 secs (8.099u,0.s) (successful) -Finished transaction in 16.461 secs (16.456u,0.003s) (successful) -Finished transaction in 4.722 secs (4.723u,0.s) (successful) -Finished transaction in 9.305 secs (9.306u,0.s) (successful) -Finished transaction in 1.398 secs (1.396u,0.s) (successful) -Finished transaction in 4.721 secs (4.723u,0.s) (successful) -Finished transaction in 7.226 secs (7.226u,0.s) (successful) -Finished transaction in 3.282 secs (3.283u,0.s) (successful) -Finished transaction in 4.536 secs (4.539u,0.s) (successful) -Finished transaction in 0.379 secs (0.38u,0.s) (successful) -Finished transaction in 0.438 secs (0.436u,0.s) (successful) -Finished transaction in 0.323 secs (0.326u,0.s) (successful) -Finished transaction in 0.372 secs (0.369u,0.s) (successful) -Finished transaction in 0.378 secs (0.376u,0.s) (successful) -Finished transaction in 0.438 secs (0.44u,0.s) (successful) -Finished transaction in 0.33 secs (0.329u,0.s) (successful) -Finished transaction in 0.368 secs (0.369u,0.s) (successful) -Finished transaction in 0.088 secs (0.086u,0.s) (successful) -Finished transaction in 0.087 secs (0.09u,0.s) (successful) -Finished transaction in 0.371 secs (0.369u,0.s) (successful) -Finished transaction in 0.441 secs (0.44u,0.s) (successful) -Finished transaction in 0.322 secs (0.319u,0.s) (successful) -Finished transaction in 0.37 secs (0.373u,0.s) (successful) -Finished transaction in 0.089 secs (0.086u,0.s) (successful) -Finished transaction in 0.091 secs (0.093u,0.s) (successful) -Finished transaction in 0.088 secs (0.089u,0.s) (successful) -Finished transaction in 0.086 secs (0.086u,0.s) (successful) - -Finished transaction in 268.648 secs (268.609u,0.096s) (successful) -*) \ No newline at end of file -- cgit v1.2.3