Interactive Matching Logic Proofs in Coq
| Authors | |
|---|---|
| Year of publication | 2023 |
| Type | Article in Proceedings |
| Conference | Theoretical Aspects of Computing (ICTAC 2023) |
| MU Faculty or unit | |
| 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: |