algebra-tactics Compare variables by conversion or keyed matching

Although it may lead to some performance issues.

Oct 01 '21 08:10 pi8027

you can pass the tactic an option in that case

Oct 01 '21 10:10 gares

@gares I think now I need to do the same for the second item of https://github.com/math-comp/algebra-tactics/pull/22#issuecomment-935858368, and it would be nice if we can set/unset these options globally. Do you think it is possible?

Oct 06 '21 09:10 pi8027

Hum, one thing I could do is to let one access the option tables you can alter with [Un]Set FooBar [int|string] but it is a bit unclear to me how to make one register options here... I mean, it should be done only once and in one place... I'll have to check if this is possible.

Oct 06 '21 12:10 gares

@gares Thanks. That's indeed desirable.

Oct 06 '21 15:10 pi8027

It seems to me that this feature will be useful in apery. https://github.com/math-comp/apery/blob/c484e1f869526b78a81f0a10e1a657096eac35bb/theories/field_tactics.v#L198-L205

Oct 06 '21 15:10 pi8027

Before addressing this issue, I wish to have a cache mechanism for conversion checking (based on union-find). That would also apply to the comparisons of instances and reduce the time spent on readback.

Oct 10 '24 13:10 pi8027