旋轉矩陣的 product 是給定角度的相加 [ag-000E]

{-# OPTIONS --without-K #-}
module ag-000E where

open import MLTT.Spartan hiding (_+_; _×_)
open import MLTT.Fin

因為不想引入太多其餘結構，把實數跟三角函數的一些性質直接公理化來用

module _ (ℝ : 𝓤₀ ̇) where
  variable
    a b : ℝ
  postulate
    cos : ℝ → ℝ
    sin : ℝ → ℝ
    -_  : ℝ → ℝ
    _+_ : ℝ → ℝ → ℝ
    _×_ : ℝ → ℝ → ℝ

    tri1 : cos (a + b) ＝ cos a × cos b + - (sin a × sin b)
    tri2 : sin (a + b) ＝ sin a × cos b + sin b × cos a

    ℝ-neg-1 : a × - b ＝ - (a × b)
    ℝ-neg-add : - a + - b ＝ - (a + b)
    ℝ-+-comm : a + b ＝ b + a
    ℝ-×-comm : a × b ＝ b × a
  infixl  -_
  infixl  _+_
  infixl  _×_
  ℝ-neg-2 : - a × b ＝ - (a × b)
  ℝ-neg-2 {a}{b} =
    - a × b   ＝⟨ ℝ-×-comm ⟩
    b × - a   ＝⟨ ℝ-neg-1 ⟩
    - (b × a) ＝⟨ ap -_ ℝ-×-comm ⟩
    - (a × b) ∎

矩陣可以看成由兩個索引指向某其 Field K 的元素的型別

  Matrix : (m n : ℕ) → (K : 𝓤 ̇) → 𝓤 ̇
  Matrix m n K = Fin m → Fin n → K

只定義 2 × 2 的矩陣乘法

  _⊗_ : Matrix   ℝ → Matrix   ℝ → Matrix   ℝ
  _⊗_ m n 𝟎 𝟎 = m 𝟎 𝟎 × n 𝟎 𝟎 + m 𝟎 𝟏 × n 𝟏 𝟎
  _⊗_ m n 𝟎 𝟏 = m 𝟎 𝟎 × n 𝟎 𝟏 + m 𝟎 𝟏 × n 𝟏 𝟏
  _⊗_ m n 𝟏 𝟎 = m 𝟏 𝟎 × n 𝟎 𝟎 + m 𝟏 𝟏 × n 𝟏 𝟎
  _⊗_ m n 𝟏 𝟏 = m 𝟏 𝟎 × n 𝟎 𝟏 + m 𝟏 𝟏 × n 𝟏 𝟏
  infixl  _⊗_

旋轉矩陣它本人，這個用來表示 R_θ，其中 θ ∈ ℝ 是角度的值

  R : ℝ → Matrix   ℝ
  R θ 𝟎 𝟎 = cos θ
  R θ 𝟎 𝟏 = sin θ
  R θ 𝟏 𝟎 = - sin θ
  R θ 𝟏 𝟏 = cos θ

證明目標：R_θR_φ = R_θ + φ

證明方式就是按 component 去證明等式成立。

  thm : {θ φ : ℝ} (i j : Fin ) → (R θ ⊗ R φ) i j ＝ R (θ + φ) i j
  thm {θ}{φ} 𝟎 𝟎 =
    (R θ ⊗ R φ) 𝟎 𝟎                   ＝⟨by-definition⟩
    cos θ × cos φ + sin θ × (- sin φ) ＝⟨ ap (cos θ × cos φ +_) ℝ-neg-1 ⟩
    cos θ × cos φ + - (sin θ × sin φ) ＝⟨ tri1 ⁻¹ ⟩
    cos (θ + φ)                       ＝⟨by-definition⟩
    R (θ + φ) 𝟎 𝟎 ∎
  thm {θ}{φ} 𝟎 𝟏 =
    (R θ ⊗ R φ) 𝟎 𝟏               ＝⟨by-definition⟩
    cos θ × sin φ + sin θ × cos φ ＝⟨ ℝ-+-comm ⟩
    sin θ × cos φ + cos θ × sin φ ＝⟨ ap (sin θ × cos φ +_) ℝ-×-comm ⟩
    sin θ × cos φ + sin φ × cos θ ＝⟨ tri2 ⁻¹ ⟩
    sin (θ + φ)                   ＝⟨by-definition⟩
    R (θ + φ) 𝟎 𝟏 ∎
  thm {θ}{φ} 𝟏 𝟎 =
    (R θ ⊗ R φ) 𝟏 𝟎                       ＝⟨by-definition⟩
    (- sin θ) × cos φ + cos θ × (- sin φ) ＝⟨ ap (_+ cos θ × - sin φ) ℝ-neg-2 ⟩
    - (sin θ × cos φ) + cos θ × (- sin φ) ＝⟨ ap (- (sin θ × cos φ) +_) ℝ-neg-1 ⟩
    - (sin θ × cos φ) + - (cos θ × sin φ) ＝⟨ ℝ-neg-add ⟩
    - (sin θ × cos φ + cos θ × sin φ)     ＝⟨ ap -_ (ap (sin θ × cos φ +_) ℝ-×-comm) ⟩
    - (sin θ × cos φ + sin φ × cos θ)     ＝⟨ ap -_ (tri2 ⁻¹) ⟩
    - sin (θ + φ)                         ＝⟨by-definition⟩
    R (θ + φ) 𝟏 𝟎 ∎
  thm {θ}{φ} 𝟏 𝟏 =
    (R θ ⊗ R φ) 𝟏 𝟏                   ＝⟨by-definition⟩
    - sin θ × sin φ + cos θ × cos φ   ＝⟨ ℝ-+-comm ⟩
    cos θ × cos φ + - sin θ × sin φ   ＝⟨ ap (cos θ × cos φ +_) ℝ-neg-2 ⟩
    cos θ × cos φ + - (sin θ × sin φ) ＝⟨ tri1 ⁻¹ ⟩
    R (θ + φ) 𝟏 𝟏 ∎

  addition : {θ φ : ℝ} (i j : Fin ) → (R θ ⊗ R φ) i j ＝ (R φ ⊗ R θ) i j
  addition {θ} {φ} i j =
    (R θ ⊗ R φ) i j ＝⟨ thm i j ⟩
    R (θ + φ) i j   ＝⟨ ap (λ x → R x i j) ℝ-+-comm ⟩
    R (φ + θ) i j   ＝⟨ thm i j ⁻¹ ⟩
    (R φ ⊗ R θ) i j ∎