ring

Stream: lean4

[Daniel Selsam]

@Mario Carneiro have you tried a reflection-based ring tactic but using dsimp for the computation?

[Mario Carneiro]

yes, that's ring2

[Mario Carneiro]

well it doesn't use dsimp

[Mario Carneiro]

I'm not sure how that would be better

[Mario Carneiro]

simp has a lot of performance problems when it is (ab)used as an evaluator

[Mario Carneiro]

I haven't done anything re: ring in lean 4 though

[Daniel Selsam]

I remember during Certigrad, we got a gagillion-X speedup by making dsimp produce a detailed rfl proof.

[Daniel Selsam]

Do you have any idea how much slower ring2 is than ring in lean3?

[Mario Carneiro]

It was modest, something like 1.5x

[Mario Carneiro]

but you have to bend over backwards to write kernel computations that compute well (see the other thread)

[Mario Carneiro]

I found it to be more robust to just generate proof terms

[Mario Carneiro]

Also the reflection approach is less flexible wrt "optional features" like negation in your (semi)ring expression