Credits

[pi8027]

• I'd like to put a paragraph in README that makes clear the source of Lemma from_sander and its relation to elliptic curves. I also suggest separating this example to from_sander.v. @amahboubi, Could you take care of the former part? (I mean, could you write down a paragraph explaining these points?)
• I'd like to indicate there were significant contributions by @gares and @amahboubi. I'm fine to include both of you as coauthors. Otherwise, I'd like to put a paragraph in README to give you credit. What do you think?

[gares]

Give me credit in the readme, or nothing at all (github already says I did contribute a few commits)

[amahboubi]

I have no strong opinion about where to put credit.

[amahboubi]

Where would you like me to write something about the "large" example?

[pi8027]

Where would you like me to write something about the "large" example?

@amahboubi Please write that as a comment here. Then I will reflect it to the last section of README.

[amahboubi]

This example was given to me by Sander Dahmen. It is related to a computational proof that elliptic curves are endowed with a group law. As suggested by @thery a while ago, this problem is a good benchmark for proof systems. Laurent Théry and Guillaume Hanrot formally verified this property in Coq in 2007, see the paper.

[thery]

good does this mean that II will soon be able to move my elliptic proof to mathcomp :smile: ?

[pi8027]

@amahboubi Thanks. I updated README in #51 (based on your comment, with slight modifications).

@thery I hope so, although I don't have time to check that at the moment. BTW, isn't it already done in elliptic-curves-ssr?

[thery]

@pi8027 no Pierre Yves's proof is a completly different one,

[thery]

@pi8027 do you support ring[H1 .. Hn] and field[H1 .. Hn]?

[pi8027]

@pi8027 do you support ring[H1 .. Hn] and field[H1 .. Hn]?

@thery Yes, but in ssreflect-like syntax: ring: H1 .. Hn.

[thery]

@pi8027 Just did the port from of the elliptic file in Coprime to its mathcomp equivalent with your tactics. This is pretty intensive (~50 calls to field). It works pretty well :fireworks: but it is a bit slower :disappointed: Before

real    0m7.975s
user    0m7.641s
sys 0m0.310s

with mathcomp

real    0m22.157s
user    0m21.680s
sys 0m0.402s

Did you already notice this kind of slow down?

[pi8027]

@thery I thought Algebra Tactics are slower than the original ring and field tactics because of conversion checking and preprocessing, but do not think x3 slowdown is a reasonable price to pay. I have some potential ways to mitigate this slowdown in my mind. But, it will never be faster than the original ring and field tactics, and I do not have time to try them right now.

Anyway, could you open a new issue for this? I will think about it later.

[pi8027]

Also please make sure that you are using the right version of Coq-Elpi (1.13.0 or later) since there was a significant performance improvement in 1.13.0.