Code Review: $\mathbb{Z}[\sqrt{-2}]$ is an integral domain

Question

I proved that $\mathbb{Z}[\sqrt{-2}]$ is an integral domain; I would like a review of this proof.

My by hand argument is in Appendix A. It is not the original argument I used. I made a stupid mistake factoring $2bd^2 + bc^2$ originally, which Coq caught. It does, however, have the same branching structure in terms of case analysis as the Coq proof.

Anyway, this proof script has many problems, but the most serious is over-reliance on sauto for proving intermediate goals, which makes performance terrible.

Here's an excerpt of the output of coqc -profile-ltac intdomain.v.

─assert (H1 : (a * Z.pos p - 2 * b * d)%   0.0%  73.6%       2    7.239s
└sauto (sauto_opts) --------------------   1.3%  73.6%       2    7.239s

Here's the proof intdomain.v.

From Coq Require Import ZArith.
From Coq Require Import Lia.

From Hammer Require Import Tactics.

(* Built in tactic Lia can do this. *)
Theorem natural_number_no_zero_divisors : forall a b : nat, a * b = 0 -> a = 0 \/ b = 0.
Proof. lia. Qed.

(* This one too *)
Theorem integers_are_integral_domain : forall a b : Z, (a * b = 0 -> a = 0 \/ b = 0)%Z.
Proof. lia. Defined.

(*
Z[sqrt(-2)] is an integral domain.

call this ring ZS.

The definition of addition doesn't play a role in whether ZS is an integral domain
or not, we only need to look at multiplication.
 *)

Definition zs_mul (p p' : Z * Z) :=
  let (a, b) := p in
  let (c, d) := p' in
  (a * c - 2 * b * d, b * c + a * d)%Z.

Definition zs_zero := (0, 0)%Z.

(* This lemmas are trivial, they're only here so I can prevent + and * from unfolding into match expressions inside simpl *)
Lemma z_add_zero : forall x, (0 + x= x)%Z.
Proof. easy. Qed.
Lemma z_add_zero_r : forall x, (x + 0 = x)%Z.
Proof. lia. Qed.
Lemma z_mul_zero_r : forall x, (x * 0 = 0)%Z.
Proof. lia. Qed.


(* This proof uses too much sauto, and sauto is very unpredictable.

Also, everything is duplicated between the positive and negative versions
which is unfortunate.

 *)
Theorem zs_is_integral_domain : forall x y, zs_mul x y = zs_zero -> x = zs_zero \/ y = zs_zero.
Proof.
  intros x y.
  destruct x as (a, b).
  destruct y as (c, d).
  unfold zs_zero.
  unfold zs_mul.
  induction c.
  {
    repeat rewrite z_mul_zero_r.
    induction d.
    {
      repeat rewrite z_mul_zero_r.
      intuition.
    }
    {
      rewrite z_add_zero.
      intro H.
      assert (a = 0)%Z by sauto.
      assert (b = 0)%Z by sauto.
      sauto.
    }
    {
      rewrite z_add_zero.
      intro H.
      assert (a = 0)%Z by sauto.
      assert (b = 0)%Z by sauto.
      sauto.
    }
  }
  {
    intros H.
    assert (H1:(a * Z.pos p - 2 * b * d = 0)%Z) by sauto.
    assert (H2:(a * d + b * Z.pos p = 0)%Z) by sauto.
    assert (H3:(a * Z.pos p = 2 * b * d)%Z) by sauto.
    assert (H4:(2 * b * d * d + b * Z.pos p * Z.pos p = 0)%Z).
    { induction a. induction b. all:sauto. }
    sauto.
  }
  {
    intros H.
    assert (H1:(a * Z.pos p - 2 * b * d = 0)%Z) by sauto.
    assert (H2:(a * d + b * Z.pos p = 0)%Z) by sauto.
    assert (H3:(a * Z.pos p = 2 * b * d)%Z) by sauto.
    assert (H4:(2 * b * d * d + b * Z.pos p * Z.pos p = 0)%Z).
    { induction a. induction b. all:sauto. }
    sauto.
  }
Qed.

---

Appendix A: By hand argument

(Alternatively, one could note that $\mathbb{Z}$ is a subring of $\mathbb{C}$ and a subring of an integral domain is an integral domain)

Represent an element of $\mathbb{Z}[\sqrt{-2}]$ as $(a+bx)$ where $a$ and $b$ are integers.

Define $(a+bx)(c+dx)$ to be $(ac-2bd) + (ad+bc)x$.

The ring $\mathbb{Z}[\sqrt{-2}]$ has zero divisors if and only if the following system of integer equations has a nontrivial solution (i.e. one where $\{0\} \not\in \{\{a, b\}, \{c, d\}\}$).

$$ ac - 2bd = 0 \\ ad + bc = 0 $$

Suppose $c$ is not equal to zero.

I will show that this equation has no nontrivial rational solutions and hence no nontrivial integer solutions.

It holds that $a = \frac{2bd}{c}$.

Substituting into the other equation we get $\frac{2bd}{c}d + bc = 0$ which is equivalent to $2bd^2 + bc^2 = 0$ by clearing denominators.

This factors as $b(c^2 + 2d^2)$.

If $b$ is zero, $a$ would be zero since $a = \frac{2bd}{c}$.

If $b$ is not zero then $c^2+2d^2$ must be zero, but $c$ is not zero and so this whole expression must be positive.

Thus there are no rational solutions and hence no integer solutions when $c \neq 0$.

Suppose $c$ is zero.

Then our system of equations simplifies to $-2bd = 0$ and $ad = 0$.

If $d=0$, then we're done. If $d$ is not zero, then $a$ and $b$ are both zero.

Answer 1

I would start from the system of equations $$ ac - 2bd = 0 \\ ad + bc = 0 $$ which gives us two additional equations: $$ (a^2 + 2b^2)cd = 0, \quad (c^2 + 2d^2)ab = 0. $$ Next, it is easy to show that $x^2 + 2y^2 = 0$ iff $(x, y) = (0, 0)$. Then, a case analysis leaves us with two equations: $$ cd = 0, \quad ab = 0. $$ So, we can finish the proof by considering pairs $\{a = 0, c = 0\}$, $\{a = 0, d = 0\}$, and so on. The proof is formalized in the following way:

From Coq Require Import ZArith Lia.

Open Scope Z_scope.

Definition zs_mul (p p' : Z * Z) :=
  let (a, b) := p in
  let (c, d) := p' in
  (a * c - 2 * b * d, b * c + a * d)%Z.

Definition zs_zero := (0, 0)%Z.

Lemma zs_norm_zero : forall x y,
    x * x + 2 * y * y = 0 <-> (x, y) = (0, 0).
Proof.
  intros x y. split.
  - intro. apply pair_equal_spec.
    destruct (Z_zerop x), (Z_zerop y); lia.
  - intros [??]%pair_equal_spec. lia.
Qed.

Theorem zs_is_integral_domain : forall x y,
    zs_mul x y = zs_zero -> x = zs_zero \/ y = zs_zero.
Proof.
  intros (a, b) (c, d). unfold zs_zero, zs_mul.
  intros [??]%pair_equal_spec.
  assert ((a * a + 2 * b * b) * (c * d) = 0).
  { enough (a * c * (a * d) + b * c * (2 * b * d) = 0) by lia.
    replace (a * d) with (- b * c) by lia.
    replace (2 * b * d) with (a * c); lia. }
  assert ((c * c + 2 * d * d) * (a * b) = 0).
  { enough (c * a * (b * c) + a * d * (2 * b * d) = 0) by lia.
    replace (b * c) with (- a * d) by lia.
    replace (2 * b * d) with (a * c); lia. }
  apply Zmult_integral in H1, H2.
  destruct H1. { left. now apply zs_norm_zero. }
  destruct H2. { right. now apply zs_norm_zero. }
  apply Zmult_integral in H1, H2.
  destruct H1, H2; subst.
  - assert (b * d = 0) by lia. apply Zmult_integral in H1.
    destruct H1; subst; [left | right]; reflexivity.
  - assert (a * d = 0) by lia. apply Zmult_integral in H1.
    destruct H1; subst; [left | right]; reflexivity.
  - assert (b * c = 0) by lia. apply Zmult_integral in H1.
    destruct H1; subst; [left | right]; reflexivity.
  - assert (a * c = 0) by lia. apply Zmult_integral in H1.
    destruct H1; subst; [left | right]; reflexivity.
Qed.

Answer 2

Here's a proof using fewer invocations of sauto. (Edit: borrowing from @Vladimir Ivanov's answer to eliminate sauto entirely.)

From Coq Require Import Utf8 ZArith Lia.

Definition Zsqrtneg2 := (Z * Z)%type.

Definition zs_mul (p q : Zsqrtneg2) : Zsqrtneg2 :=
  (fst p * fst q - 2 * snd p * snd q, snd p * fst q + fst p * snd q)%Z.

Definition zs_zero := (0, 0)%Z : Zsqrtneg2.

Declare Scope Z2_scope.
Delimit Scope Z2_scope with Z2.
Open Scope Z2_scope.
Bind Scope Z2_scope with Zsqrtneg2.

Notation "0" := zs_zero : Z2_scope.
Infix "*" := zs_mul : Z2_scope.

Definition zs_norm (p : Zsqrtneg2) : Z := ((fst p)^2 + 2 * (snd p)^2)%Z.

Theorem norm_multiplicative : ∀ p q : Zsqrtneg2,
    zs_norm (p * q) = (zs_norm p * zs_norm q)%Z.
Proof.
  unfold zs_norm, zs_mul, fst, snd.
  intros [] [].
  ring.
Qed.

Theorem norm_zero : ∀ p : Zsqrtneg2, zs_norm p = 0%Z ↔ p = 0.
Proof.
  intros [??].
  unfold zs_zero, zs_norm, fst, snd.
  setoid_rewrite pair_equal_spec.
  lia.
Qed.

Theorem zs_is_integral_domain : ∀ x y : Zsqrtneg2, x * y = 0 → x = 0 ∨ y = 0.
Proof.
  intros ??.
  now rewrite <-? norm_zero, norm_multiplicative, Z.mul_eq_0.
Qed.

If you are willing to rely on sauto, you can do it with only sauto.

From Hammer Require Import Tactics.

Theorem zs_is_integral_domain : ∀ x y : Zsqrtneg2, x * y = 0 → x = 0 ∨ y = 0.
Proof.
  sauto.
Qed.