Stream: math-comp users

Topic: Algebra tactics for stdlib fields


view this post on Zulip Bas Spitters (Jun 01 2023 at 12:46):

I seem to recall that algebra tactics also work for stdlib rings/fields. However, rereading the documentation, this does not seem to be the case.
Am I misremembering? Is there another standard solution?
https://github.com/math-comp/algebra-tactics

view this post on Zulip Pierre Roux (Jun 01 2023 at 12:50):

I'm not sure I understand the question, algebra-tactics is for matchomp not for stdlib. You can still equip the stdlib types with mathcomp structures to get some compatibility but otherwise I don't think it's expected to work out of the box (some of these structures, for Z, may already exist in mczify though).

view this post on Zulip Kazuhiko Sakaguchi (Jun 01 2023 at 14:35):

At least ring and field of Algebra Tactics provide a special treatment for Z: https://github.com/math-comp/algebra-tactics/blob/master/theories/ring.elpi#L205 (If you read the paper, I guess this is what you "misremember.")

view this post on Zulip Kazuhiko Sakaguchi (Jun 01 2023 at 14:38):

You can embed Z to any ring through the int_of_Z morphism and _%:~R. Algebra Tactics can recognize these morphisms.

view this post on Zulip Bas Spitters (Jun 02 2023 at 07:22):

Thanks. Yes, I was thinking of some mczify type of preprocessing.


Last updated: Jul 15 2024 at 20:02 UTC