The Coq mailing list

[Daniel de Rauglaudre <daniel.de_rauglaudre AT inria.fr>]

Hi all,

I am trying to prove that a rotation matrix on the unit sphere in ℝ³
has two fixpoints (on the rotation axis and if not zero rotation), and
I am blocked. I am going to explain. Please let me know when I am wrong.

I started with a 3x3 matrix M, which is a rotation one iff
    det (M) = 1
    M * t(M) = I        (t = transposition)

And a supposed fixpoint (one of the two points on the rotation axis on
the sphere) is (x/r, y/r, z/r) such that
   x = m₃₂ - m₂₃
   y = m₁₃ - m₃₁
   z = m₂₁ - m₁₂
   r = √ (x² + y² + z²)

First: is it correct?

I am trying to prove that this supposed fixpoint is indeed a fixpoint.

The hypothesis det (M) = 1 is written
  Hd : (m₁₁ * m₂₂ * m₃₃ - m₁₁ * m₂₃ * m₃₂ + m₁₂ * m₂₃ * m₃₁ - m₁₂ * m₂₁ * m₃₃ 
+
        m₁₃ * m₂₁ * m₃₂ - m₁₃ * m₂₂ * m₃₁)%R = 1%R

The hypothesis M * t(M) = I gives
  H₉ : (m₁₁² + m₁₂² + m₁₃²)%R = 1%R
  H₅ : (m₂₁² + m₂₂² + m₂₃²)%R = 1%R
  H₁ : (m₃₁² + m₃₂² + m₃₃²)%R = 1%R
  H₆ : (m₁₁ * m₂₁ + m₁₂ * m₂₂ + m₁₃ * m₂₃)%R = 0%R
  H₂ : (m₂₁ * m₃₁ + m₂₂ * m₃₂ + m₂₃ * m₃₃)%R = 0%R
  H₃ : (m₃₁ * m₁₁ + m₃₂ * m₁₂ + m₃₃ * m₁₃)%R = 0%R

Now, when I am trying to prove that the supposed fixpoint is a fixpoint,
And I get the following goals, after simplification
  ((m₁₁ - 1) * (m₃₂ - m₂₃) + m₁₃ * m₂₁ - m₁₂ * m₃₁)%R = 0%R
  ((m₂₂ - 1) * (m₁₃ - m₃₁) + m₂₁ * m₃₂ - m₂₃ * m₁₂)%R = 0%R
  ((m₃₃ - 1) * (m₂₁ - m₁₂) + m₃₂ * m₁₃ - m₂₃ * m₃₁)%R = 0%R

And now, impossible to prove them with the hypotheses. However I made
some tests with some examples, they seem true.

Am I missing something? Can someone help?

Thanks.

-- 
Daniel de Rauglaudre
http://pauillac.inria.fr/~ddr/