Stream: Coq users

Topic: Number theory libraries

view this post on Zulip Jake Zweifler (Oct 06 2022 at 01:35):

Hello! Does anyone know of any more advanced number theory/algebra libraries in Coq? Specifically, one that defines quotient rings and more advanced subsets of C such as Z[sqrt(2)]? I am trying to prove some facts about matrices over Z[1/sqrt(2), i] and (Z/2Z)[1/sqrt(2), i]. Note that I am using Coquelicot's complex numbers which are represented as ordered pairs (R, R). My idea is to have a separate type represent these sets, but there could also be a predicate that returns true for complex numbers that are members of Z[1/sqrt(2), i]. But then how should I define Z/2Z and more generally Z/nZ? Does anyone have any suggestions? Thanks so much!

view this post on Zulip Pierre Roux (Oct 06 2022 at 05:52):

I don't know if that would fit you need but MathComp (hence MathComp Analysis) has more algebra, and machinery for quotients, than the stdlib (and Coquelicot).

view this post on Zulip Karl Palmskog (Oct 06 2022 at 07:20):

there is that uses Coquelicot, but I guess it's not exactly chock-full of algebra. (coq-num-analysis package in opam)

Last updated: Jan 31 2023 at 13:02 UTC