Formal Proof of a Machine Closed Theorem in Coq
Hai Yang Wan, Anping He, Zhiyang You, Xibin Zhao · Journal of Applied Mathematics · 2014
The paper presents a formal proof of a machine closed theorem of TLA+in the theorem proving system Coq. A shallow embedding scheme is employed for the proof which is independent of concrete syntax. Fundamental concepts need to state that the machine closed theorems are addressed in the proof platform. A useful proof pattern of constructing a trace with desired properties is devised. A number of Coq reusable libraries are established.