## Stream: lean4

### Topic: ring

#### Daniel Selsam (Feb 05 2021 at 02:57):

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

#### Mario Carneiro (Feb 05 2021 at 02:58):

yes, that's ring2

#### Mario Carneiro (Feb 05 2021 at 02:58):

well it doesn't use dsimp

#### Mario Carneiro (Feb 05 2021 at 02:58):

I'm not sure how that would be better

#### Mario Carneiro (Feb 05 2021 at 02:59):

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

#### Mario Carneiro (Feb 05 2021 at 02:59):

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

#### Daniel Selsam (Feb 05 2021 at 03:00):

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

#### Daniel Selsam (Feb 05 2021 at 03:00):

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

#### Mario Carneiro (Feb 05 2021 at 03:01):

It was modest, something like 1.5x

#### Mario Carneiro (Feb 05 2021 at 03:02):

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

#### Mario Carneiro (Feb 05 2021 at 03:02):

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

#### Mario Carneiro (Feb 05 2021 at 03:04):

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

Last updated: May 07 2021 at 12:15 UTC