diff options
author | Jason Gross <jgross@mit.edu> | 2016-06-11 16:18:21 -0400 |
---|---|---|
committer | Jason Gross <jgross@mit.edu> | 2016-06-11 16:18:21 -0400 |
commit | c49c3e9bb79af608218a528560065cc9f24037f0 (patch) | |
tree | 3308014dd21329cd5e2797ecb99ff1736dd2da07 /src/Specific/GF25519.v | |
parent | 7a163ef981507f254dd6b5d343acdedc331274c7 (diff) |
Work around bug #4811 (slow f_equal)
This is https://coq.inria.fr/bugs/show_bug.cgi?id=4811, [f_equal]
loops(?) in 8.5pl1 (fixed already in 8.5.dev)
Diffstat (limited to 'src/Specific/GF25519.v')
-rw-r--r-- | src/Specific/GF25519.v | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/src/Specific/GF25519.v b/src/Specific/GF25519.v index 8aaf8caf6..68278ce4c 100644 --- a/src/Specific/GF25519.v +++ b/src/Specific/GF25519.v @@ -132,7 +132,7 @@ Lemma F25519_mul_OK : RepBinOpOK F25519RepConversions ModularArithmetic.mul F255 destruct x as [[[[[[[[[x9 x8] x7] x6] x5] x4] x3] x2] x1] x0]. destruct y as [[[[[[[[[y9 y8] y7] y6] y5] y4] y3] y2] y1] y0]. let E := constr:(GF25519Base25Point5_mul_reduce_formula x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 y0 y1 y2 y3 y4 y5 y6 y7 y8 y9) in - transitivity (ModularBaseSystem.decode (proj1_sig E)); [|solve[simpl;f_equal]]; + transitivity (ModularBaseSystem.decode (proj1_sig E)); [|solve[simpl; apply f_equal; reflexivity]]; destruct E as [? r]; cbv [proj1_sig]. cbv [rep ModularBaseSystem.rep PseudoMersenneBase modulus] in r; edestruct r; eauto. Qed. @@ -164,7 +164,7 @@ Lemma F25519_add_OK : RepBinOpOK F25519RepConversions ModularArithmetic.add F255 destruct x as [[[[[[[[[x9 x8] x7] x6] x5] x4] x3] x2] x1] x0]. destruct y as [[[[[[[[[y9 y8] y7] y6] y5] y4] y3] y2] y1] y0]. let E := constr:(GF25519Base25Point5_add_formula x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 y0 y1 y2 y3 y4 y5 y6 y7 y8 y9) in - transitivity (ModularBaseSystem.decode (proj1_sig E)); [|solve[simpl;f_equal]]; + transitivity (ModularBaseSystem.decode (proj1_sig E)); [|solve[simpl; apply f_equal; reflexivity]]; destruct E as [? r]; cbv [proj1_sig]. cbv [rep ModularBaseSystem.rep PseudoMersenneBase modulus] in r; edestruct r; eauto. Qed. @@ -174,7 +174,7 @@ Lemma F25519_sub_OK : RepBinOpOK F25519RepConversions ModularArithmetic.sub F255 destruct x as [[[[[[[[[x9 x8] x7] x6] x5] x4] x3] x2] x1] x0]. destruct y as [[[[[[[[[y9 y8] y7] y6] y5] y4] y3] y2] y1] y0]. let E := constr:(GF25519Base25Point5_sub_formula x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 y0 y1 y2 y3 y4 y5 y6 y7 y8 y9) in - transitivity (ModularBaseSystem.decode (proj1_sig E)); [|solve[simpl;f_equal]]; + transitivity (ModularBaseSystem.decode (proj1_sig E)); [|solve[simpl; apply f_equal; reflexivity]]; destruct E as [? r]; cbv [proj1_sig]. cbv [rep ModularBaseSystem.rep PseudoMersenneBase modulus] in r; edestruct r; eauto. -Qed.
\ No newline at end of file +Qed. |