Set of quaternions that square to -1

Stream: maths

[Mark Andrew Gerads]

import Mathlib

open Quaternion Classical

--declare a Set Of Quaternions That Square To Negative 1
def soqtstn1₀ : Set ℍ[ℝ] := {q₀ : ℍ[ℝ] | -1 = q₀ * q₀}
def soqtstn1₁ : Set ℍ[ℝ] := {q₀ : ℍ[ℝ] | ∃ (rx ry rz : ℝ), (q₀ = ⟨0, rx, ry, rz⟩ ∧ rx*rx + ry*ry + rz*rz = 1)}

lemma equalSets : soqtstn1₀ = soqtstn1₁ := by
  refine Set.ext ?h
  intros q₀
  simp [soqtstn1₀, soqtstn1₁]
  sorry

A guide to the proof is here: https://www.quora.com/What-is-the-square-root-of-1-in-a-quaternionic-number-system
I am having trouble (I don't even know how to split the goal from 'a<->b' into the 2 goals 'a->b' and 'b->a' ), so I want to know that.

[Newell Jensen]

constructor will split it

[Eric Wieser]

This seems like a good start:

lemma equalSets : soqtstn1₀ = soqtstn1₁ := by
  ext ⟨r, x, y, z⟩
  dsimp [soqtstn1₀, soqtstn1₁]
  simp [Quaternion.ext_iff]
  sorry

[Mark Andrew Gerads]

I made some progress.

lemma equalSets : soqtstn1₀ = soqtstn1₁ := by
  ext ⟨r, x, y, z⟩
  dsimp [soqtstn1₀, soqtstn1₁]
  simp [Quaternion.ext_iff]
  constructor
  intros ha
  use x
  use y
  use z
  simp only [and_self, and_true]
  rcases ha with ⟨hSphere3,h0x,h0y,h0z⟩
  sorry
  intros h₀
  ring_nf
  rcases h₀ with ⟨rx,ry,rz,hx⟩
  rcases hx with ⟨hx₀,hSphere⟩
  rcases hx₀ with ⟨hr,hrx,hry,hrz⟩
  simp_rw [hr]
  simp only [ne_eq, zero_pow', zero_sub, zero_mul, and_self, and_true]
  simp_rw [hrx,hry,hrz]
  let hSphere2 := congrArg (λ (xk : ℝ) => -xk) hSphere
  simp only [neg_add_rev] at hSphere2
  rw [←hSphere2]
  ring

image.png
Is there any way to use the ring tactic on a hypothesis instead of a goal? I want to simplify h0x, h0y, and h0z.
I plan to show r=0 through proof by contradiction after that.

[Scott Morrison]

Does ring_nf at h work?

[Mark Andrew Gerads]

It does. Thanks.

[Scott Morrison]

• ring_nf means: rewrite ring expressions into a normal form.
• ring means: close the goal, by using ring_nf

With this in mind, you can see why ring at h is not supported.

[Mark Andrew Gerads]

Okay, I proved the first lemma, and part of the second lemma. Here is a MWE of the second lemma:

import Mathlib
open Quaternion Classical

--declare a Set Of Quaternions That Square To Negative 1
def soqtstn1₁ : Set ℍ[ℝ] := {q₁ : ℍ[ℝ] | ∃ (rx ry rz : ℝ), (q₁ = ⟨0, rx, ry, rz⟩ ∧ rx*rx + ry*ry + rz*rz = 1)}
def soqtstn1₂ : Set ℍ[ℝ] := {q₂ : ℍ[ℝ] | ‖q₂‖ = 1 ∧ q₂.re = 0}


lemma equalSetsSoqtstn1₁AndSoqtstn1₂ : soqtstn1₁ = soqtstn1₂ := by
  ext ⟨r, x, y, z⟩
  dsimp [soqtstn1₁, soqtstn1₂]
  simp [Quaternion.ext_iff]
  constructor
  intros h
  rcases h with ⟨rx,ry,rz,hx,hSphere⟩
  rcases hx with ⟨hr0, hxrx, hyry, hzrz⟩
  constructor
  sorry
  exact hr0
  intros h₀
  rcases h₀ with ⟨hNorm1, hr0⟩
  use x
  use y
  use z
  simp only [hr0, and_self, true_and]
  sorry

image.png
I ran into a problem: I don't know how to simplify the norm of a quaternion. Can I or someone just define the norm if no one else has done it yet?

[Mark Andrew Gerads]

It looks like maybe I need to square it to simplify it? I saw Quaternion.normSq exists.

[Mark Andrew Gerads]

I don't know. I'll try again later after I get a chance for advice.

[Eric Wieser]

The norm has already been defined, else you would never end up with it in your goal in the first place

[Eric Wieser]

I would guess you want the lemma saying norm x = sqrt (inner x x)

[Mark Andrew Gerads]

I made some progress and defeated a sorry.
The Moogle.ai math search engine was quite helpful.

lemma equalSetsSoqtstn1₁AndSoqtstn1₂ : soqtstn1₁ = soqtstn1₂ := by
  ext ⟨r, x, y, z⟩
  dsimp [soqtstn1₁, soqtstn1₂]
  simp [Quaternion.ext_iff]
  constructor
  intros h
  rcases h with ⟨rx,ry,rz,hx,hSphere⟩
  rcases hx with ⟨hr0, hxrx, hyry, hzrz⟩
  simp_rw [hr0]
  simp only [and_true]
  sorry
  intros h₀
  rcases h₀ with ⟨hNorm1, hr0⟩
  use x
  use y
  use z
  simp only [hr0, and_self, true_and]
  let hNormSquare1 := congrArg (λ (r₀ : ℝ)=>r₀*r₀) hNorm1
  simp only [mul_one] at hNormSquare1
  rw [←Quaternion.normSq_eq_norm_mul_self, hr0, Quaternion.normSq_def'] at hNormSquare1
  rw [←hNormSquare1]
  simp only [ne_eq, OfNat.ofNat_ne_zero, not_false_eq_true, zero_pow', zero_add]
  ring_nf

The state of the remaining sorry is
image.png

[Eric Wieser]

The obvious next step is to eliminate the last three equalities, with rw or cases or subst

[Mark Andrew Gerads]

I'm done. The complete code is at https://github.com/Nazgand/NazgandLean4/blob/master/NazgandLean4/quaternionLemma.lean

[Eric Wieser]

I strongly recommend you use · to mark where each subgoal begins

[Eric Wieser]

constructor
· all of the
  forward direction
· and now the
  reverse direction

[Mark Andrew Gerads]

Done. I was wondering about that, since there was something similar in Lean3.