Ssreflect Users Discussion List

[Yves Bertot <>]

Hello,

I always had the feeling that using the tactic ring with the 
mathematical components library is complicated and unpredictable. 
Lately, I came up with an example formula that contains a large sum with 
a hundred terms that should cancel out, and using other approaches than 
ring would impose proof times in the order of 8 minutes.  As I discussed 
the problem around, Maxime Dénès urged me to give one more try to ring.  
It turned out that finding a solution was not too time-consuming, but 
still a little brittle.

As a way to improve the situation, I would like to provoke some 
discussion on the topic.  For now, my experiment is visible in a blog 
page: 
https://project.inria.fr/coqexchange/cramers-formula-using-ring-with-mathematical-components/ 
, I know that other experiments have already been performed, links to 
the developments might be useful.  You can either add them yourself or 
keep me informed.

Yves