Coq Formalization of Orientation Representation: Matrix, Euler Angles, Axis-Angle and Quaternion

Rotation matrices, Euler angles, axis-angle, and unit quaternions are common models for representing object pose in space. Each offers distinct advantages and disadvantages regarding handling singularities, computational complexity, and storage requirements, motivating their interchangeability and conversion algorithms. However, these models and their associated algorithms involve complex matrix operations, trigonometric computations, and geometric reasoning, making manual derivation and verification error-prone. To guarantee algorithm correctness, we present a formal verification of these models and their conversion algorithms within the Coq Proof Assistant, focusing on pure rotational orientation representation. We establish a formal foundational mathematical library, including vector and matrix theories on abstract elements, additional real matrix properties, and quaternion theory. Building upon this foundation, we formalize all four rotation models and their conversion algorithms, emphasizing invariants of special orthogonal groups, Rodrigues’ rotation formula, and the quaternion rotation formula. Our formally verified library offers excellent readability, usability, and simplicity, laying a foundation for developers to understand and verify advanced kinematics algorithms.