Stream: Beginner Questions

Topic: semiring_modulo for a factorial_semiring + comm_ring


view this post on Zulip Jakub Kądziołka (Jan 28 2021 at 13:25):

I have a 'a::{factorial_semiring, comm_ring}. I would like to derive the semiring_modulo class for it, by defining a mod b = a - a div b. Is this possible?

view this post on Zulip Manuel Eberl (Jan 28 2021 at 13:32):

Not generically, no. But you can probably do it for a particular instance.

view this post on Zulip Manuel Eberl (Jan 28 2021 at 13:33):

Our of curiosity, what type is it that you have?

view this post on Zulip Jakub Kądziołka (Jan 28 2021 at 13:48):

I just want to prove some theorems for an arbitrary UFD

view this post on Zulip Manuel Eberl (Jan 28 2021 at 14:57):

Yeah then you probably have to assume a type class that has modulo if you want modulo to be available.

view this post on Zulip Manuel Eberl (Jan 28 2021 at 14:57):

The only other way I can think of is to define a type 'a ufdmod that is basically a copy of 'a except that it also has a modulo operation defined the way you just said.

view this post on Zulip Manuel Eberl (Jan 28 2021 at 14:58):

Then you can pull all the results that don't use mod over from 'a ufdmod to 'a using e.g. the transfer tool.

view this post on Zulip Manuel Eberl (Jan 28 2021 at 14:58):

Might not be worth it though.

view this post on Zulip Manuel Eberl (Jan 28 2021 at 14:58):

Might be easier to just not use mod.

view this post on Zulip Manuel Eberl (Jan 28 2021 at 14:59):

What you could also do is interpret the semiring_modulo locale with that particular definition of mod.

view this post on Zulip Manuel Eberl (Jan 28 2021 at 14:59):

I've done that sort of thing before. It's a little bit messy, but it does the job.


Last updated: Aug 13 2022 at 06:26 UTC