diff options
| author |  Andres Erbsen <andreser@mit.edu> | 2017-04-28 20:28:08 -0400 |
|---|---|---|
| committer |  GitHub <noreply@github.com> | 2017-04-28 20:28:08 -0400 |
| commit | 08be7fa27881cf4bef5bede9d07feaaa9025b9a4 (patch) | |
| tree | 18b19422c585001f784ab9066627f66940791494 /src/Curves/Weierstrass | |
| parent | e7a7d3cf71a9170ce8ce0022a7e1ae46e012b3a6 (diff) | |
Prove relationship between `xzladderstep` and M.add (#162)
* hopefully all proofs we need about xzladderstep
* Better automation in xzproofs
* Speed up xzproofs with heuristic clearing
* Remove useless hypotheses
* XZProofs cleanup
* fix "group by isomorphism" proofs, use in XZProofs
Diffstat (limited to 'src/Curves/Weierstrass')
| -rw-r--r-- | src/Curves/Weierstrass/AffineProofs.v | 15 |
1 files changed, 8 insertions, 7 deletions
diff --git a/src/Curves/Weierstrass/AffineProofs.v b/src/Curves/Weierstrass/AffineProofs.v index be76cee90..3401d7b31 100644 --- a/src/Curves/Weierstrass/AffineProofs.v +++ b/src/Curves/Weierstrass/AffineProofs.v @@ -9,10 +9,7 @@ Module W. Section W. Context {F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv} {a b:F} {field:@Algebra.Hierarchy.field F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv} - {Feq_dec:DecidableRel Feq} - {char_ge_12:@Ring.char_ge F Feq Fzero Fone Fopp Fadd Fsub Fmul 12%positive}. (* FIXME: shouldn't need we need 4, not 12? *) - Let char_ge_3 : @Ring.char_ge F Feq Fzero Fone Fopp Fadd Fsub Fmul 3. - Proof. eapply Algebra.Hierarchy.char_ge_weaken; eauto; vm_decide. Qed. + {Feq_dec:DecidableRel Feq}. Local Infix "=" := Feq : type_scope. Local Notation "a <> b" := (not (a = b)) : type_scope. Local Notation "0" := Fzero. Local Notation "1" := Fone. Local Infix "+" := Fadd. Local Infix "-" := Fsub. Local Infix "*" := Fmul. @@ -24,7 +21,7 @@ Module W. | |- Equivalence _ => split; [intros ? | intros ??? | intros ????? ] | |- monoid => split | |- group => split - | |- abelian_group => split + | |- commutative_group => split | |- is_associative => split; intros ??? | |- is_commutative => split; intros ?? | |- is_left_inverse => split; intros ? @@ -33,8 +30,12 @@ Module W. | |- is_right_identity => split; intros ? end. - Global Instance commutative_group {discriminant_nonzero:id(4*a*a*a + 27*b*b <> 0)} : abelian_group(eq:=W.eq(a:=a)(b:=b))(op:=W.add(char_ge_3:=char_ge_3))(id:=W.zero)(inv:=W.opp). - Proof using Type. + Global Instance commutative_group + char_ge_3 + {char_ge_12:@Ring.char_ge F Feq Fzero Fone Fopp Fadd Fsub Fmul 12%positive} (* FIXME: shouldn't need we need 4, not 12? *) + {discriminant_nonzero:id(4*a*a*a + 27*b*b <> 0)} + : commutative_group(eq:=W.eq(a:=a)(b:=b))(op:=W.add(char_ge_3:=char_ge_3))(id:=W.zero)(inv:=W.opp). + Proof using Type. Time cbv [W.opp W.eq W.zero W.add W.coordinates proj1_sig]; repeat match goal with |