leanprover/lean — pull request #375 by avigad (2014-12-13 00:43:52+00:00)
Title: feat(library/algebra/ordered_ring): start on ordered_ring, and minor changes elsewhere

There is a proof that takes a long time in ordered_ring:

https://github.com/avigad/lean/blob/master/library/algebra/ordered_ring.lean#L252-L333

I don't know what the performance bottleneck is, other than that it is somewhat long. There are no instances of calc. I wrote another version with tactics, to see if that would be faster, but it wasn't.

(By the way, my "timing" tests amount to using C-c C-l to run Lean on the file. Does it use the cache? Would it be more informative if I deleted the cache?)

The slow proof is not a problem, but I commented it in the file in case it is helpful for optimization later.