Handcrafted Coq Inversions Made Operational on Operational Semantics
When reasoning on formulas involving large-size inductively defined relations, such as the semantics of a real programming language, many steps require inversions of hypotheses. The built-in “inversion” Coq tactic can then be used, but it suffers from severe issues of controllability, maintenance and efficiency. This tactic is unusable in practice for large applications.
To circumvent that issue, we propose a proof technique based on the combination of an antidiagonal argument and the impredicative encoding of inductive data-structures. We can then encode suitable helper tactics in LTac, yielding shorter scripts, furthermore more robust against version updates in the background software. We illustrated it within correctness proofs of C programs according to the operational semantics of C defined in Leroy’s CompCert project.
Jean-Francois Monin worked at France Telecom R&D in applications of Formal Proofs to industrial software. He has been professor at Univ. Joseph Fourier, Grenoble, since 2003. He worked at LIAMA & Tsinghua University from 2009 to 2013.