Formal Proof of a Machine Closed Theorem in Coq

الملخص EN

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.