OrienRepr.RotationMatrix3D

Require Export MathBase.
Require Import AxisAngle.

Basic Rotation Matrics

Definitions of 3D basic rotation matrices

Give a column-vector v respect to this coordinate, when actively rotate it about the x-axes and reached v' respect to this coordinate, then: v' = Rx(θ) * v

Definition Rx (θ : R) : mat 3 3 :=
  l2m
    [[1; 0; 0];
     [0; cos θ ; - sin θ ];
     [0; sin θ ; cos θ ]]%R.

Give a column-vector v respect to this coordinate, when actively rotate it about the y-axes and reached v' respect to this coordinate, then: v' = Ry(θ) * v

Definition Ry (θ : R) : mat 3 3 :=
  l2m
    [[cos θ ; 0; sin θ ];
     [0; 1; 0];
     [- sin θ ; 0; cos θ ]]%R.

Give a column-vector v respect to this coordinate, when actively rotate it about the z-axes and reached v' respect to this coordinate, then: v' = Rz(θ) * v

Definition Rz (θ : R) : mat 3 3 :=
  l2m
    [[cos θ ; - sin θ ; 0];
     [sin θ ; cos θ ; 0];
     [0; 0; 1]]%R.

Properties of 3D basic rotation matrices

Rx,Ry,Rz are the special case of aa2mat.

Theorem aa2mat_eq_Rx : forall θ : R, aa2mat (mkAA v3i θ) = Rx θ.
Proof. intros; meq; ra. Qed.

Theorem aa2mat_eq_Ry : forall θ : R, aa2mat (mkAA v3j θ) = Ry θ.
Proof. intros; meq; ra. Qed.

Theorem aa2mat_eq_Rz : forall θ : R, aa2mat (mkAA v3k θ) = Rz θ.
Proof. intros; meq; ra. Qed.

Rx,Ry,Rz are orthogonal matrix

Lemma Rx_orth : forall (θ : R), morth (Rx θ).
Proof. intros; meq; ra. Qed.

Lemma Ry_orth : forall (θ : R), morth (Ry θ).
Proof. intros; meq; ra. Qed.

Lemma Rz_orth : forall (θ : R), morth (Rz θ).
Proof. intros; meq; ra. Qed.

Rx,Ry,Rz are invertible matrix

Lemma Rx_minvtble : forall (θ : R), minvtble (Rx θ).
Proof. intros. apply morth_minvtble. apply Rx_orth. Qed.

Lemma Ry_minvtble : forall (θ : R), minvtble (Ry θ).
Proof. intros. apply morth_minvtble. apply Ry_orth. Qed.

Lemma Rz_minvtble : forall (θ : R), minvtble (Rz θ).
Proof. intros. apply morth_minvtble. apply Rz_orth. Qed.

The determinant of Rx,Ry,Rz are 1

Lemma Rx_det1 : forall (θ : R), mdet (Rx θ) = 1.
Proof. intros; cbv; ra. Qed.

Lemma Ry_det1 : forall (θ : R), mdet (Ry θ) = 1.
Proof. intros; cbv; autorewrite with R; auto. Qed.

Lemma Rz_det1 : forall (θ : R), mdet (Rz θ) = 1.
Proof. intros; cbv; autorewrite with R; auto. Qed.

Rx,Ry,Rz are member of SO3

Lemma Rx_SOnP : forall θ : R, SOnP (Rx θ).
Proof. intros. hnf. split. apply Rx_orth. apply Rx_det1. Qed.
Lemma Ry_SOnP : forall θ : R, SOnP (Ry θ).
Proof. intros. hnf. split. apply Ry_orth. apply Ry_det1. Qed.
Lemma Rz_SOnP : forall θ : R, SOnP (Rz θ).
Proof. intros. hnf. split. apply Rz_orth. apply Rz_det1. Qed.

Definition Rx_SO3 (θ : R) : SO3 := mkSOn (Rx θ) (Rx_SOnP θ).
Definition Ry_SO3 (θ : R) : SO3 := mkSOn (Ry θ) (Ry_SOnP θ).
Definition Rz_SO3 (θ : R) : SO3 := mkSOn (Rz θ) (Rz_SOnP θ).

使用群 SOn 可以直接证明逆矩阵、旋转矩阵等有关的性质，并且比计算式证明的速度快

R(θ)⁻¹ = R(θ)\T

Lemma Rx_inv_eq_trans : forall θ : R, (Rx θ)\-1 = (Rx θ)\T.
Proof.
intros. apply (SOn_minv_eq_trans (Rx_SO3 θ)).
Qed.

Lemma Ry_inv_eq_trans : forall θ : R, (Ry θ)\-1 = (Ry θ)\T.
Proof. intros; apply (SOn_minv_eq_trans (Ry_SO3 θ)). Qed.

Lemma Rz_inv_eq_trans : forall θ : R, (Rz θ)\-1 = (Rz θ)\T.
Proof. intros; apply (SOn_minv_eq_trans (Rz_SO3 θ)). Qed.

R(-θ) = R(θ)\T

Lemma Rx_neg_eq_trans : forall θ : R, Rx (-θ) = (Rx θ)\T.
Proof. intros; meq; ra. Qed.

Lemma Ry_neg_eq_trans : forall θ : R, Ry (-θ) = (Ry θ)\T.
Proof. intros; meq; ra. Qed.

Lemma Rz_neg_eq_trans : forall θ : R, Rz (-θ) = (Rz θ)\T.
Proof. intros; meq; ra. Qed.

R(-θ) * R(θ) = I

Lemma Rx_neg_mul_Rx : forall θ : R, Rx (- θ) * Rx θ = mat1.
Proof.
  intros; rewrite Rx_neg_eq_trans, <- Rx_inv_eq_trans, mmul_minvAM_l; auto.
  apply Rx_minvtble.
Qed.

Lemma Ry_neg_mul_Ry : forall θ : R, Ry (- θ) * Ry θ = mat1.
Proof.
  intros; rewrite Ry_neg_eq_trans, <- Ry_inv_eq_trans, mmul_minvAM_l; auto.
  apply Ry_minvtble.
Qed.

Lemma Rz_neg_mul_Rz : forall θ : R, Rz (- θ) * Rz θ = mat1.
Proof.
  intros; rewrite Rz_neg_eq_trans, <- Rz_inv_eq_trans, mmul_minvAM_l; auto.
  apply Rz_minvtble.
Qed.

R(θ) * R(-θ) = I

Lemma Rx_mul_Rx_neg : forall θ : R, Rx θ * Rx (- θ) = mat1.
Proof.
  intros; rewrite Rx_neg_eq_trans, <- Rx_inv_eq_trans, mmul_minvAM_r; auto.
  apply Rx_minvtble.
Qed.

Lemma Ry_mul_Ry_neg : forall θ : R, Ry θ * Ry (- θ) = mat1.
Proof.
  intros; rewrite Ry_neg_eq_trans, <- Ry_inv_eq_trans, mmul_minvAM_r; auto.
  apply Ry_minvtble.
Qed.

Lemma Rz_mul_Rz_neg : forall θ : R, Rz θ * Rz (- θ) = mat1.
Proof.
  intros; rewrite Rz_neg_eq_trans, <- Rz_inv_eq_trans, mmul_minvAM_r; auto.
  apply Rz_minvtble.
Qed.