Interactive Matching Logic Proofs in Coq

Warning

This publication doesn't include Faculty of Economics and Administration. It includes Faculty of Informatics. Official publication website can be found on muni.cz.
Authors

TUŠIL Jan PÉTER Bereczky DÁNIEL Horpácsi

Year of publication 2023
Type Article in Proceedings
Conference Theoretical Aspects of Computing (ICTAC 2023)
MU Faculty or unit

Faculty of Informatics

Citation
Doi http://dx.doi.org/10.1007/978-3-031-47963-2_10
Keywords Matching logic; Sequent calculus; Coq; Interactive reasoning
Attached files
Description Matching logic (ML) is a formalism for specifying and reasoning about mathematical structures by means of patterns and pattern matching. Previously, it has been used to capture a number of other logics, e.g., separation logic with recursive definitions and linear temporal logic. ML has also been formalized in the Coq Proof Assistant, and the soundness of its Hilbert-style proof system has been mechanized. However, using a Hilbert-style system for interactive reasoning is challenging - even more so in ML, which lacks a general deduction theorem. Therefore, we propose a single-conclusion sequent calculus for ML that is more amenable to interactive proving. Based on this sequent calculus, we implement a proof mode for interactive reasoning in ML, which significantly simplifies the construction of ML proofs in Coq. The proof mode is a mechanism for displaying intermediate proof states and an extensible set of proof tactics that implement the rules of the sequent calculus. We evaluate our proof mode on a collection of examples, showing a substantial improvement in proof script size and readability.
Related projects:

You are running an old browser version. We recommend updating your browser to its latest version.