Zulip Chat Archive

Stream: lean4

Topic: ring


view this post on Zulip Daniel Selsam (Feb 05 2021 at 02:57):

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

view this post on Zulip Mario Carneiro (Feb 05 2021 at 02:58):

yes, that's ring2

view this post on Zulip Mario Carneiro (Feb 05 2021 at 02:58):

well it doesn't use dsimp

view this post on Zulip Mario Carneiro (Feb 05 2021 at 02:58):

I'm not sure how that would be better

view this post on Zulip Mario Carneiro (Feb 05 2021 at 02:59):

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

view this post on Zulip Mario Carneiro (Feb 05 2021 at 02:59):

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

view this post on Zulip 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.

view this post on Zulip Daniel Selsam (Feb 05 2021 at 03:00):

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

view this post on Zulip Mario Carneiro (Feb 05 2021 at 03:01):

It was modest, something like 1.5x

view this post on Zulip 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)

view this post on Zulip Mario Carneiro (Feb 05 2021 at 03:02):

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

view this post on Zulip 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