OrienRepr.Orien3D

Require Export MathBase.
Require Export AxisAngle EulerAngle.
Import V3Notations.

Preliminary math

v' = R(θ) * v

Lemma Rx_spec : forall (v : vec 3) (θ : R), rotaa (mkAA v3i θ) v = (Rx θ) *v v.
Proof.
  intros. rewrite <- aa2mat_eq_Rx, aa2mat_spec; auto; simpl. apply v3i_vunit.
Qed.

Lemma Ry_spec : forall (v : vec 3) (θ : R), rotaa (mkAA v3j θ) v = (Ry θ) *v v.
Proof.
  intros. rewrite <- aa2mat_eq_Ry, aa2mat_spec; auto; simpl. apply v3j_vunit.
Qed.

Lemma Rz_spec : forall (v : vec 3) (θ : R), rotaa (mkAA v3k θ) v = (Rz θ) *v v.
Proof.
  intros. rewrite <- aa2mat_eq_Rz, aa2mat_spec; auto; simpl. apply v3k_vunit.
Qed.

v = R(-θ) * v'

Lemma Rx_neg_spec : forall (v : vec 3) (θ : R), v = Rx (-θ) *v (rotaa (mkAA v3i θ) v).
Proof.
  intros. rewrite Rx_spec.
  rewrite <- mmulv_assoc, Rx_neg_mul_Rx, mmulv_1_l; auto.
Qed.

Lemma Ry_neg_spec : forall (v : vec 3) (θ : R), v = Ry (-θ) *v (rotaa (mkAA v3j θ) v).
Proof.
  intros. rewrite Ry_spec.
  rewrite <- mmulv_assoc, Ry_neg_mul_Ry, mmulv_1_l; auto.
Qed.

Lemma Rz_neg_spec : forall (v : vec 3) (θ : R), v = Rz (-θ) *v (rotaa (mkAA v3k θ) v).
Proof.
  intros. rewrite Rz_spec.
  rewrite <- mmulv_assoc, Rz_neg_mul_Rz, mmulv_1_l; auto.
Qed.

v = R(θ)\T * v'

Lemma Rx_trans_spec : forall (v : vec 3) (θ : R),
    v = (Rx θ)\T *v (rotaa (mkAA v3i θ) v).
Proof. intros. rewrite <- Rx_neg_eq_trans, <- Rx_neg_spec; auto. Qed.

Lemma Ry_trans_spec : forall (v : vec 3) (θ : R),
    v = (Ry θ)\T *v (rotaa (mkAA v3j θ) v).
Proof. intros. rewrite <- Ry_neg_eq_trans, <- Ry_neg_spec; auto. Qed.

Lemma Rz_trans_spec : forall (v : vec 3) (θ : R),
    v = (Rz θ)\T *v (rotaa (mkAA v3k θ) v).
Proof. intros. rewrite <- Rz_neg_eq_trans, <- Rz_neg_spec; auto. Qed.

The equivalence of Pre-/Post- multiplication, i.e., R *v u = u v* (R\T)

Lemma Rx_mmulv_eq_mvmul : forall (u : vec 3) (θ : R), (Rx θ) *v u = u v* ((Rx θ)\T).
Proof. intros. veq; ra. Qed.

Lemma Ry_mmulv_eq_mvmul : forall (u : vec 3) (θ : R), (Ry θ) *v u = u v* ((Ry θ)\T).
Proof. intros. veq; ra. Qed.

Lemma Rz_mmulv_eq_mvmul : forall (u : vec 3) (θ : R), (Rz θ) *v u = u v* ((Rz θ)\T).
Proof. intros. veq; ra. Qed.