Email Gateway (Aug 22 2022 at 21:12): Email Gateway (Aug 22 2022 at 21:12):From: Christian Weinz <christian.weinz@stud.uni-goettingen.de>
Hello,
For a project in my university I'm working on a formalization of the
Gaussian integers in Isabelle. Eventually, I want to use that for
number theoretic proofs within Isabelle.
My first approach was to look how the complex numbers were introduced
in Isabelle and to copy that for the Gaussian integers, basically just
replacing real for int. That worked fine, and I went on to show class
instantiations for my Gaussian integers.
The Gaussian integers form a euclidean domain. For now, I'd be happy to
show that the Gaussian integers allow unique factorizations into prime
factors up to a unit factor, i.e. that they are a factorial ring, so I
aimed for the class "factorial_ring_gcd" in
"/HOL/Computational_Algebra/Factorial_Ring.thy".
However, that did not work out because the path "factorial_ring_gcd ->
factorial_semiring_gcd -> factorial_semiring -> normalization_semidom
-> semidom_divide_unit_factor" in the class hierarchy forces me to
define the functions "unit_factor" and "normalize" for the Gaussian
integers satisfying the class definition of
"semidom_divide_unit_factor" in "/HOL/Rings.thy". I see no way to
normalize the Gaussian integers that way.
My next approach would be to define the Gaussian integer as a
ring_scheme and use "/HOL/Algebra/Ring_Divisibility.thy". From that I
would get the "factorization_property" from the same file, but that
formalization looks less intuitive and less practical for my purposes.
That is why I'm writing here. Is the class hierarchy not suitable for
formalizing what I need to achieve? Am I just overlooking something? It
might be possible that I have a mistake in my understand of the
Gaussian Integers. I'm thankful for any ideas.
Thanks and happy new year,
Christian
Email Gateway (Aug 22 2022 at 21:15):From: Christian Weinz <christian.weinz@stud.uni-goettingen.de>
Thank you, and let me be so frank to directly take up that offer.
I started working with HOL-Algebra to show the properties of the
Gaussian Integers that I need. However, I very early ran into a problem
about "duplicate fact declarations".
Below is a relatively small theory that shows the problem. As well
given below is the error message that is shown in the output panel
after the proof of the instantiation.
It might very well be that I use "HOL-Algebra" incorrectly. In any
case, a workaround would be very welcome.
---- theory ----
theory GaussianIntegers
imports
"HOL-Algebra.Multiplicative_Group"
begin
codatatype gaussian_integer = Gaussian_Integer (Re: int) (Im: int)
lemma gaussian_integer_eq_iff: "x = y ⟷ Re x = Re y ∧ Im x = Im y"
by (auto intro: gaussian_integer.expand)
abbreviation gaussian_integer_ring :: "gaussian_integer ring"
where "gaussian_integer_ring ≡
⦇carrier = UNIV,
mult = (λx y. Gaussian_Integer (Re x * Re y - Im x * Im y)
(Re x * Im y + Im x * Re y)),
one = Gaussian_Integer 1 0,
zero = Gaussian_Integer 0 0,
add = (λx y. Gaussian_Integer (Re x + Re y) (Im x + Im y))⦈"
interpretation cring gaussian_integer_ring
unfolding cring_def ring_def abelian_group_def abelian_monoid_def
monoid_def comm_monoid_def comm_monoid_axioms_def ring_axioms_def
abelian_group_axioms_def comm_group_def group_def group_axioms_def
Units_def
apply (simp add: add.commute distrib_right distrib_left
gaussian_integer_eq_iff right_diff_distrib left_diff_distrib)
proof -
have "⋀g. Re (g) + Re (Gaussian_Integer (- Re g) (- Im g)) = 0
∧ Im (g) + Im (Gaussian_Integer (- Re g) (- Im g)) = 0"
by simp
then show "UNIV ⊆ {y. ∃x. gaussian_integer.Re y
+ gaussian_integer.Re x = 0
∧ gaussian_integer.Im y
+ gaussian_integer.Im x = 0}"
by blast
qed
end
---- error message ----
Duplicate fact declaration "GaussianIntegers.add.is_monoid" vs.
"GaussianIntegers.add.is_monoid"⌂
The above error(s) occurred while activating locale instance
add : Group.group "add_monoid gaussian_integer_ring"
Kind regards,
Christian
Email Gateway (Aug 22 2022 at 21:15):From: Christian Weinz <christian.weinz@stud.uni-goettingen.de>
I feel I might be able to contribute to that. Is this effort organized
somewhere?
Best,
Christian
Email Gateway (Aug 22 2022 at 21:15):From: Manuel Eberl <eberlm@in.tum.de>
I started working with HOL-Algebra to show the properties of the
Gaussian Integers that I need. However, I very early ran into a problem
about "duplicate fact declarations".
The problem is the theorem "comm_monoid.is_monoid" in
HOL-Algebra.Multiplicative_Group. This theorem is completely unnecessary
and it leads to a name clash when interpreting the locale. No idea why
nobody noticed this before. We should really remove this before the next
release.
Since you will want to use Euclidean domains, there really is no way
past this, since the theory in which they are defined in HOL-Algebra
depends on Multiplicative_Group. The only workaround I can offer is to
locally remove the theorem "is_monoid" on lines 649-650 of
Multiplicative_Group.thy in your local Isabelle installation /or/ to
wait until I removed it from the development version (will probably do
that later today) and work with the development version
(http://isabelle.in.tum.de/repos/isabelle).
Sorry about this – HOL-Algebra is not used very much and is /really/ messy.
I think I'll have a shot at cleaning up the type classes enough to be
usable in your case during the next few weeks. I can't say yet if it
will work out though, but hopefully this will be done by the next
release (which I guess will be some time around April or May).
It might very well be that I use "HOL-Algebra" incorrectly. In any
case, a workaround would be very welcome.
There are quite a few things that I think should be done differently:
Locale interpretations are typically done with the "unfold_locales"
command. That makes things much easier.
I would advise against calling your constructors "Re" and "Im",
because they will then clash with the "Re" and "Im" from the complex
numbers.
It is good to keep names short, especially ones you will use a lot.
Perhaps "gauss_int" instead of "gaussian_integer" etc.
I think it will be much more pleasant for you to go as far as
possible using the typeclass, i.e. instantiate all the appropriate
typeclasses (at least up "idom") for your Gaussian integers. Then you
can still easily move into the HOL-Algebra setting by defining something
like
definition Gauss_Ints :: "gauss_int ring"
where "gaussian_integer_ring ≡ ⦇carrier = UNIV,
mult = (*), one = 1, zero = 0, add = (+)⦈"
Then you can get the properties you need (unique factorisation etc) from
HOL-Algebra and pull them out to the type-class-based setting again.
Ideally, you should also first define a Euclidean norm on the Gaussian
integers with all its properties. This will allow you to easily switch
to the type class-based Euclidean rings later on.
Cheers,
Manuel
Email Gateway (Aug 23 2022 at 08:11):From: Manuel Eberl <eberlm@in.tum.de>
I removed the problematic lemma as of isabelle-dev/a3f7f00b4fd8 (cf.
http://isabelle.in.tum.de/repos/isabelle/rev/a3f7f00b4fd8).
The interpretation of the ring locale should work now.
Manuel
Email Gateway (Aug 23 2022 at 08:11):From: Manuel Eberl <eberlm@in.tum.de>
However, that did not work out because the path "factorial_ring_gcd ->
factorial_semiring_gcd -> factorial_semiring -> normalization_semidom
-> semidom_divide_unit_factor" in the class hierarchy forces me to
define the functions "unit_factor" and "normalize" for the Gaussian
integers satisfying the class definition of
"semidom_divide_unit_factor" in "/HOL/Rings.thy". I see no way to
normalize the Gaussian integers that way.
Yes, sorry, that's my fault.
The purpose of normalize/unit_factor is to have a canonical
representative for each association class in a ring. The obvious choice
for Gaussian integers is to define "normalize (a + i * b) = abs a + i *
abs b". Unfortunately, this doesn't work because the typeclass
(semidom_divide_unit_factor) requires "unit_factor" (and thereby
"normalize") to be multiplicative. This requirement simple developed
from the fact that "normalize" is multiplicative for all the examples we
had back when we introduced these classes, and it makes many theorems
(e.g. about GCDs) much nicer to state.
It is always possible to define a multiplicative "normalize" for a ring
with unique factorisation (simply pick whatever canonical representative
you want for any prime element and then lift it up to general ring
elements by multiplicativity), but of course that is not something one
really wants to do. Especially because one often wants to show that
something is a Euclidean domain in order to get unique factorisation for
free.
The proper solution would be to remove the multiplicativity condition
from semidom_divide_unit_factor. I tried that once but it turned out to
be quite a bit of work, so I gave up again. Perhaps it would be worth
giving it another shot now.
My next approach would be to define the Gaussian integer as a
ring_scheme and use "/HOL/Algebra/Ring_Divisibility.thy". From that I
would get the "factorization_property" from the same file, but that
formalization looks less intuitive and less practical for my purposes.
Using HOL-Algebra is definititely also possible. You have to jump
through a few more hoops. You would have to interpret the
euclidean_domain locale for your Gaussian integer type and an
appropriate Euclidean measure function, and then you get the theorem
"factorization_property", which you can polish a bit to get it into a
more readable form.
That is why I'm writing here. Is the class hierarchy not suitable for
formalizing what I need to achieve?
You want to use the typeclass-based stuff whenever you can. However, the
typeclass-based approach to algebra in Isabelle
("HOL-Computational_Algebra") is very much geared towards pragmaticism:
It was designed to work well for the use concrete cases that we had
(naturals, integers, polynomials, formal power series), and it does that
fairly well. But for Gaussian integers, it does not work in the current
form, and for others (p-adic numbers) will probably never work without a
considerable amount of effort.
My suggestion would be to prove unique factorisation using HOL-Algebra
for now, and if I get around to removing multiplicativity from that type
class at some point (hopefully before the next release), you should be
able to switch over to that without much effort.
Feel free to ask if you need help with any more concrete questions about
how to use HOL-Algebra.
Cheers,
Manuel
Email Gateway (Aug 23 2022 at 08:13):From: Manuel Eberl <eberlm@in.tum.de>
Good news, as of isabelle-dev/e0237f2eb49d, normalization_semidom does
not require "unit_factor" (or alternatively "normalize") to be
multiplicative anymore. The property was replaced with
"is_unit u ==> unit_factor (u * a) = u * unit_factor a"
This is a much weaker property that is equivalent to the following: Two
elements that are associated will normalize to the same canonical
representative, i.e.
"a dvd b ==> b dvd a ==> normalize a = normalize b"
With this, it is now possible to prove that the Gaussian integers are a
Euclidean ring.
There are also a few other related classes that slap on the
multiplicativity assumption to restore the previous behaviour (the most
important examples of normalization_semidoms all fulfil it!). Some
things (most notably polynomial GCD and related concepts) still require
multiplicative normalization. It would probably be possible to remove
that in the future as well, but let's take this one step at a time.
While I was at it, I also introduced a class "field_gcd" that subsumes a
number of previous classes that all essentially meant "a field that also
has the trivial GCD defined on it".
NEWS entry will follow.
https://isabelle.in.tum.de/repos/isabelle/rev/e0237f2eb49d
Cheers,
Manuel
Email Gateway (Aug 23 2022 at 08:14):From: Christian Weinz <christian.weinz@stud.uni-goettingen.de>
Thanks for this work Manel. Meanwhile I'm pretty sure I figured out a
way how to define a multiplicative unit_factor on the Gaussian
integers; You first recursively divide by 1+i whenever the number is
divisible by that, and then take the rest mod 2+2*i. The result is a
unit and that process is multiplicative. I have formalized and proved
most of it in Isabelle already, I intend to finish that.
I am aiming for a clean formalization suitable for upstreaming, so I
tried to use the existing typeclasses as much as possible, and slightly
modifying existing ones, where needed. I ran very early into a problem
during that, which I presented in another email to this list.
What would be a good approach to encapsulate the the relation between
the complex numbers and the Gaussian integers in Isabelle?
Specifically, that the Gaussian integers are a subset and should be
easily coercable to complex, and that the conjugation "cn", the
functions "Re" and "Im" and the imaginary unit "i" should be usable
when working with either.
Email Gateway (Aug 23 2022 at 08:15):From: Manuel Eberl <eberlm@in.tum.de>
Thanks for this work Manel. Meanwhile I'm pretty sure I figured out a
way how to define a multiplicative unit_factor on the Gaussian
integers; You first recursively divide by 1+i whenever the number is
divisible by that, and then take the rest mod 2+2*i. The result is a
unit and that process is multiplicative. I have formalized and proved
most of it in Isabelle already, I intend to finish that.
Hm, okay. I have no intuition for what this means. Not sure if this is the best way to go; it seems to me that it makes more sense to have an intuitively clear concept of what a normalised Gaussian integer is (e.g. either 0 or real part > 0, imaginary part ≥ 0).
I am aiming for a clean formalization suitable for upstreaming, so I
tried to use the existing typeclasses as much as possible, and slightly
modifying existing ones, where needed. I ran very early into a problem
during that, which I presented in another email to this list.
I would advise against modifying type classes. Even small changes lead to a huge amount of merge work. Much of the Isabelle distribution and the AFP is affected by such changes, so I would only make them if absolutely necessary.
What would be a good approach to encapsulate the the relation between
the complex numbers and the Gaussian integers in Isabelle?
Specifically, that the Gaussian integers are a subset and should be
easily coercable to complex, and that the conjugation "cn", the
functions "Re" and "Im" and the imaginary unit "i" should be usable
when working with either.
Similarly to nat and real, I would say: Just define an injective homomorphism "complex_of_gauss_int :: gauss_int ⇒ complex" (or something like that). Using "Re", "Im", and "i" with both complex numbers and Gaussian integers is not that easy. There are a few possible options:
– Pick a different name (e.g. "ReZ", "ImZ" for Gaussian integers; the "Z" standing for the integers)
– Simply declare "Re" as additional notation. This will lead to syntax ambiguity warnings due to multiple parse trees.
– Use ad-hoc overloading. That might, however, require some changes to the existing syntax, and I don't think Gaussian integers are important enough to justify going to such lengths.
Personally, I would recommend going for the first option, and then /perhaps/ switching on some optional extra syntax for these things to make them nicer to look at.
As I said to you privately, I do have a proof-of-concept implementation of Gaussian integers from years ago that does pretty much exactly that.
Cheers,
Manuel
Last updated: Apr 19 2024 at 16:20 UTC