From 67004987959e1c9e46e879f06da00d567547482e Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Fri, 12 Feb 2016 22:22:36 -0500 Subject: workaround field with typeclass modulus --- .../ExtendedCoordinatesIssue.v | 24 ++++++++++------------ 1 file changed, 11 insertions(+), 13 deletions(-) (limited to 'src/CompleteEdwardsCurve/ExtendedCoordinatesIssue.v') diff --git a/src/CompleteEdwardsCurve/ExtendedCoordinatesIssue.v b/src/CompleteEdwardsCurve/ExtendedCoordinatesIssue.v index 37bc8cca5..8d24f2cd2 100644 --- a/src/CompleteEdwardsCurve/ExtendedCoordinatesIssue.v +++ b/src/CompleteEdwardsCurve/ExtendedCoordinatesIssue.v @@ -4,22 +4,19 @@ Require Import Crypto.Spec.CompleteEdwardsCurve. Section ExtendedCoordinates. Local Open Scope F_scope. - (* - Context {prm:TwistedEdwardsParams}. (* DOESN'T WORK *) - *) - Context {q:BinInt.Z} {prime_q:Znumtheory.prime q}. (* WORKS OKAY-ish *) - - Check q : BinInt.Z. - Check prime_q : Znumtheory.prime q. - Existing Instance prime_q. + Context {prm:TwistedEdwardsParams}. + Context {p:BinInt.Z} {p_eq_q:p = q}. + Lemma prime_p : Znumtheory.prime p. + rewrite p_eq_q; exact prime_q. + Qed. - Add Field Ffield_Z : (@Ffield_theory q _) - (morphism (@Fring_morph q), + Add Field Ffield_Z : (@Ffield_theory p prime_p) + (morphism (@Fring_morph p), preprocess [Fpreprocess], postprocess [Fpostprocess], constants [Fconstant], - div (@Fmorph_div_theory q), - power_tac (@Fpower_theory q) [Fexp_tac]). + div (@Fmorph_div_theory p), + power_tac (@Fpower_theory p) [Fexp_tac]). Lemma biggerFraction : forall XP YP ZP XQ YQ ZQ d : F q, ZQ <> 0 -> @@ -34,7 +31,8 @@ Section ExtendedCoordinates. (ZP * ZToField 2 * ZQ + XP * YP / ZP * ZToField 2 * d * (XQ * YQ / ZQ))) = (XP / ZP * (YQ / ZQ) + YP / ZP * (XQ / ZQ)) / (1 + d * (XP / ZP) * (XQ / ZQ) * (YP / ZP) * (YQ / ZQ)). Proof. + rewrite <-p_eq_q. intros. - field; assumption. + abstract (field; assumption). Qed. End ExtendedCoordinates. \ No newline at end of file -- cgit v1.2.3