search

math-comp / algebra-tactics

Ring, field, lra, nra, and psatz tactics for Mathematical Components
33 stars 2 forks source link

Compare variables by conversion or keyed matching #18

Open pi8027 opened 3 years ago

pi8027 commented 3 years ago

Although it may lead to some performance issues.

gares commented 3 years ago

you can pass the tactic an option in that case

pi8027 commented 3 years ago

@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?

gares commented 3 years ago

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.

pi8027 commented 3 years ago

@gares Thanks. That's indeed desirable.

pi8027 commented 3 years ago

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

pi8027 commented 1 month ago

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.