A Formalization of Elements of Special Relativity in Coq

Abstract

We present a formalization of elements of special relativity in Coq beginning from a set of first-order axioms, towards demonstrating that Coq may be used to formalize physical reasoning at the level of introductory physics. We find that Coq’s logic may be adapted to formalize practical physical reasoning found in the literature. Furthermore, we demonstrate that Coq’s automation mechanism can significantly reduce programmer effort for formalizing physical reasoning. We describe our experience in developing this automation along the formalization.