To play this document inside your browser use ALT-N and ALT-P. If you get stack overflow errors, try to use Google Chrome or Chromium with the command line option --js-flags="--harmony-tailcalls".

You can save your edits inside your browser and load them back (edits are also saved when you close the window). Finally you can download the file for offline editing.

Preliminaries

In this exercise session, we will use complex algebraic numbers instead of complex numbers. This is for a technical reason, please think of algebraic numbers as if they were complex numbers, since they enjoy the same first order theory.

Let's extend the library of algebraic numbers with some easy lemmas first.

Question 1: prove that if a sum of natural numbers is 1 then one of its term is 0 and the other is 1

Note that we do not consider nat but the copy of nat which is embeded in the algebraic numbers algC. The theorem is easy to prove for nat, so we suggest you use a compatibility lemma numbers between nat and Cnat

Question 2: The real part of product

Question 3: The imaginary part of product

(it's the same proof except for 2 characters, don't do it if takes more than 5s)

The ring of Gaussian integers

References:

Gaussian integers are complex numbers of the form (n + i m) where n and m are integers. We will prove they form a ring, and determine the units of this ring.

  • First we define a predicate for the algebraic numbers which are Gaussian integers.

  • You need to use qualifE to reduce (x \ in gaussInteger) to its definition.

Question 4: Prove that integers are Gaussian integers

Question 5: Prove that Gaussian integers form a subring

  • There follows the boilerplate to use the proof GI_subring in order to canonically provide a subring structure to the predicate gaussInteger.

  • Finally, we define the type of Gaussian Integer, as a sigma type of algebraic numbers. We soon prove that this is in fact a sub type.

  • We provide the subtype property, this makes it possible to use the generic operator val to get an algC from a Gaussian Integer.

  • We deduce that the real and imaginary parts of a GI are integers

  • We provide a ring structure to the type GI, using the subring canonical property for the predicate gaussInteger

  • Now we build the unitRing and comUnitRing structure of gauss integers. Contrarily to the previous structures, the operator is not the same as on algebraics. Indeed the invertible algebraics are not necessarily invertible Gaussian integers.

  • Hence, we define the inverse of Gaussian integers as follow : if the algebraic inverse happens to be a Gaussian integer we recover the proof and package it together with the element and get a gauss integer, otherwise, we default to the identity.

  • A Gaussian integer is invertible if the algbraic inverse is a gauss integer.

Question 6: prove a few facts in order to find a comUnitRingMixin for GI, and then instantiate the interfaces of unitRingType and comUnitRingType.

Do only one of the following proofs.

Question 7: Show that Gaussian integers are stable by conjugation.

  • We use this fact to build the conjugation of a Gaussian Integers

  • We now define the norm (stasm) for Gaussian integer, we don't need to specialize it to Gaussian integer so we define it over algebraic numbers instead.

Question 8: Show that the gaussNorm of x is the square of the complex modulus of x

Hint: only one rewrite with the right theorem.

Question 9: Show that the gaussNorm of an Gaussian integer is a natural number.

Question 10: Show that gaussNorm is multiplicative (on all algC).

Hint: use morphism lemmas rmorph1 and rmorphM

Question 11 (hard): Find the invertible elements of GI

Do unitGI_norm1 first, and come back to side lemmas later.