Mechanizing Matching Logic In Coq

Mechanizing Matching Logic In Coq

Péter BereczkyEötvös Loránd University, Hungary Xiaohong ChenUniversity of Illinois Urbana-Champaign, USA Dániel HorpácsiEötvös Loránd University, Hungary Lucas PeñaUniversity of Illinois Urbana-Champaign, USA Jan TušilMasaryk University, Brno, Czech Republic

P. Bereczky et al.

Matching logic is a formalism for specifying, and reasoning about, mathematical structures, using patterns and pattern matching. Growing in popularity, it has been used to define many logical systems such as separation logic with recursive definitions and linear temporal logic. In addition, it serves as the logical foundation of the K semantic framework, which was used to build practical verifiers for a number of real-world languages. Despite being a fundamental formal system accommodating substantial theories, matching logic lacks a general-purpose, machine-checked formalization. Hence, we formalize matching logic using the Coq proof assistant. Specifically, we create a new representation of matching logic that uses a locally nameless encoding, and we formalize the syntax, semantics, and proof system of this representation in the Coq proof assistant. Crucially, we prove the soundness of the formalized proof system and provide a means to carry out interactive matching logic reasoning in Coq. We believe this work provides a previously unexplored avenue for reasoning about matching logic, its models, and the proof system.

§ INTRODUCTION

Matching logic [38, 14]
is a unifying logical
framework for defining the formal semantics of programming languages
and specifying their language tools.
Given a programming language $L$,
its formal semantics is defined by a matching logic theory $\Gamma^L$,
i.e., a set of axioms.
Many language tools, such as parsers, interpreters, compilers, and even deductive
program verifiers, are best-effort implementation
of matching logic reasoning.
The correctness of language tools is justified by matching logic proof objects,
checkable by a 240-line proof checker [25].

The formal semantics of many real-world programming languages
have been completely defined as matching logic theories.
These languages include
C [23],
Java [7],
JavaScript [36],
Python [21],
Rust [26, 41],
Ethereum bytecode [24],
x86-64 [18],
and LLVM [27].
The framework (<https://kframework.org>)
is a best-effort implementation of matching logic.
From the formal semantics of these real-world languages,
automatically generates implementations and formal analysis tools,
some of which have been commercialized [22].
Ultimately, can be used as a tool for formally defining languages,
and as a tool for formally reasoning about properties of programming languages and programs.

currently provides the most comprehensive support for
automated reasoning for matching logic
by means of various algorithms that are specifically targeted at
the (automatic) generation of language tools
such as interpreters and deductive verifiers, which, respectively,
are specific forms of matching logic reasoning,
and an integration with the state-of-the-art SMT solvers such as
Z3 [19].
However, there is no “exit solution” in when
these automatic algorithms and external solvers fail,
in which case lemmas, whose correctness
is justified externally, often informally,
need to be manually added to fill in the reasoning gaps.

In this paper, we aim to bridge the aforementioned reasoning gaps
by bringing interactive reasoning to matching logic.
Specifically, we give, for the first time, a complete mechanization
of matching logic in Coq [6].

§.§ Contributions

In this work, we investigate the formal definition of matching logic in an interactive theorem prover, with the aim of enabling computer-aided reasoning about and within matching logic:

* Mechanize the soundness of the matching logic proof system—while matching logic has been proven sound on paper, its soundness has not been formalized yet. This soundness proof is crucial in providing the highest level of assurance for mechanized reasoning.

* Enable interactive, mechanically verified reasoning about matching logic theories—the formalization needs to leverage the full power of the theorem prover to encode matching logic theories in a modular way and do reasoning at the highest abstraction level possible.

Following upon similar formalization efforts (such as the solutions to the POPLMark Challenge [5]), we have decided to encode the logic in a widely used and mature system, the Coq proof assistant [6]. Furthermore, we carry out the embedding in a locally nameless [10, 31, 33, 20] representation, which, in contrast to named approaches, is more amenable to computer-aided verification. The entire formalization is open, and available online [2]. The paper shows the following main contributions:

* A locally nameless definition of the matching logic syntax, semantics, and proof system;

* The design of the embedding of the locally nameless matching logic in the Coq proof assistant;

* The first mechanized proof of the soundness of the matching logic proof system;

* Example theories with proofs about their semantic and proof-theoretical properties in the mechanized matching logic;

* A preliminary implementation of a matching logic proof mode to simplify interactive reasoning.

The paper is structured as follows.
Section <ref> introduces matching logic, in
a locally nameless representation. In Section <ref>, we outline the Coq
formalization, including some technical challenges faced.
Section <ref> discusses examples of meta-level reasoning and the soundness proof in particular.

Section <ref> presents an example interactive proof in our formalization.
Finally, Section <ref> discusses related
work, and
Section <ref> presents areas for future work and

§ INTRODUCTION TO MATCHING LOGIC

In this section, we present the syntax, semantics, and proof
system of matching logic.
Unlike in previous work [14, 16, 12],
here we introduce a
locally nameless presentation of matching logic.
This new presentation is more convenient to be formalized in proof assistants,
which is discussed in detail in <Ref>.

§.§ Matching Logic Locally Nameless Syntax

The syntax we present in this section is in literature known
as that of a locally nameless one [10, 31, 33, 20].
A locally nameless syntax is a combination of the traditional
named representation and the entirely nameless de Bruijn encoding,
using named variables if they occur free and de Bruijn encoding
if they are bound.
In particular, it distinguishes free and bound variables on the syntactic level,
enabling capture-avoiding substitutions without variable renaming.
This design decision eliminates the need for reasoning about $\alpha$-equivalence.

Firstly, we define matching logic signatures.
A signature provides us infinitely many named variables and a set of
(user-defined) constant symbols.

A matching logic signature is a tuple
$(\EVar,\SVar,\Sigma)$ where

* $\EVar$ is a set of element variables,
denoted $x$, $y$, …;

* $\SVar$ is a set of set variables,
denoted $X$, $Y$, …;

* $\Sigma$ is a set of (constant) symbols, denoted
$\sigma$, $f$, $g$, …
Both $\EVar$ and $\SVar$ are countably infinite sets.
$\Sigma$ is a countable set, possibly empty.
When the sets of variables are understood from the context,
we feel free to use $\Sigma$ to denote a matching logic signature.

Given a signature $\Sigma$, the syntax of matching logic
generates a set of well-formed formulas, called patterns.
In the following, we first define pseudo-patterns.

Given a signature $\Sigma$, the set of pseudo-patterns
is inductively defined by the following grammar:

\varphi \Coloneqq
x \mid X \mid \ee{n} \mid \se{N} \mid \sigma \mid
\varphi_1 \, \varphi_2 \mid \bot \mid \varphi_1 \to \varphi_2
\mid \exists \ld \varphi \mid \mu \ld \varphi

In the above grammar,
$x$ and $X$ are element and set variables, respectively;
$\ee{n}$ and $\se{N}$ are de Bruijn indices that represent
the bound element and set variables, respectively,
where $n,N \in \NN$;
$\sigma$ is any symbol in the given signature $\Sigma$;
$\varphi_1 \, \varphi_2$ is called application,
where $\varphi_1$ is applied to $\varphi_2$;
$\bot$ and $\varphi_1 \to \varphi_2$ are propositional operations;
$\exists \ld \varphi$ is the FOL (first-order logic)-style quantification;
and $\mu \ld \varphi$ is the least fixpoint pattern.
Both $\exists$ and $\mu$
use the nameless de Bruijn encoding for their bound variables.

We say that a pseudo-pattern $\psi$ is well-formed,
if (1) for any subpattern $\mu \ld \varphi$, the nameless variable bound by $\mu$ has no negative occurrences in $\varphi$; and
(2) all of its nameless variables (i.e., de Bruijn indices)
are correctly bound by the quantifiers $\exists$ and $\mu$, that is,
for any de Bruijn indices $n$ and $N$ that occur in $\psi$,

* $\ee{n}$ is in the scope of at least $n+1$ $\exists$-quantifiers;

* $\se{N}$ is in the scope of at least $N+1$ $\mu$-quantifiers.

A well-formed pseudo-pattern is called a pattern. For example, the definition of transitive closure in <Ref> is a pattern, but $\exists \ld \ee{0} \to \ee{1}$ is not, since $\ee{1}$ is not bound by any quantifier.

Opening quantified patterns.
In a locally nameless representation, we use both
named and unnamed variables.
Named variables are for free variables,
while unnamed variables are for bound variables.
Therefore, when we have a pattern $\exists \ld \varphi$
(similarly for $\mu \ld \varphi$) and want to extract its body,
we need to assign a fresh named variable to the unnamed variable
that corresponds to the topmost quantifier $\exists$ (resp. $\mu$).

This operation is called opening a (quantified) pattern [10].
We use $\opene(\varphi,x)$ and $\opens(\varphi,X)$
to denote the opening of the bodies of the quantified patterns
$\exists \ld \varphi$ and $\mu \ld \varphi$, respectively,
where $x$ and $X$ are the corresponding new named variables.

These opening operations are special instances of the general case of substitution,
which is defined in the usual way[We denote substitution with $\phi[\psi/x]$, where $x$ (a bound or free, set or element variable) is replaced by $\psi$ in $\phi$.].

§.§ Matching Logic Models and Semantics

In this section, we formally define the models and semantics of matching logic.
Intuitively speaking, matching logic has a pattern matching semantics.
A matching logic pattern is interpreted as the set
of elements that match it.

Firstly, we define the notion of matching logic models.

Let $\Sigma$ be a signature.
A $\Sigma$-model, or simply a model,
is a tuple $(M, @_M, \{\sigma_M\}_{\sigma \in \Sigma})$

* $M$ is a nonempty carrier set;

* $@_M \colon M \times M \to \mathcal{P}(M)$ is a binary application function,
where $\mathcal{P}(M)$ denotes the powerset of $M$;

* $\sigma_M \subseteq M$ is the interpretation of $\sigma$,
for each $\sigma \in \Sigma$.

We use the same letter $M$ to denote the model defined as above.

Next, we define valuations of variables.
Note that matching logic has both element and set variables.
As expected, a valuation assigns element variables to elements
and set variables to subsets of the underlying carrier set.

Given a signature $\Sigma$ and a $\Sigma$-model $M$,
a variable valuation $\rho$ is a mapping such that:

* $\rho(x) \in M$ for all $x \in \EVar$;

* $\rho(X) \subseteq M$ for all $X \in \SVar$.

We are now ready to define the semantics of matching
logic patterns.

Given a matching logic model $M$ and a variable valuation $\rho$,
we define the semantics of any (well-formed) pattern $\psi$,
written $\ev{\psi}{M,\rho}$, inductively as follows:

$\ev{x}{M,\rho} = \{ \rho(x) \}$;
$\ev{X}{M,\rho} = \rho(X)$;

$\ev{\sigma}{M,\rho} = \sigma_M$;
$\ev{\bot}{M,\rho} = \emptyset$;

$\ev{\varphi_1 \to \varphi_2}{M,\rho} = M \setminus ( \ev{\varphi_1}{M,\rho} \setminus \ev{\varphi_2}{M,\rho})$;

$\ev{\varphi_1 \, \varphi_2}{M,\rho} = \bigcup_{a_1 \in \ev{\varphi_1}{M,\rho}}\bigcup_{a_2 \in \ev{\varphi_2}{M,\rho}}
a_1 \apM a_2 $;

2c$\ev{\exists \ld \varphi}{M,\rho}
= \bigcup_{a \in M} \ev{\opene(\varphi,x)}{M,\rho[a/x]}$ for fresh $x \in \EVar$;

2c$\ev{\mu \ld \varphi}{M,\rho} = \lfp \ \FF^\rho_{\varphi,X}$,
where $\FF^\rho_{\varphi,X}(A) = \ev{\opens(\varphi,X)}{M,\rho[A/X]}$
for fresh $X \in \SVar$.

The above definition is well-defined ($\opene$ and $\opens$ are defined at the end of
<Ref>). For examples, we refer to the formalization [2] and to <cit.>.

In the following, we define validity and the semantic entailment relation
in matching logic.

For $M$ and $\varphi$, we write $M \models \varphi$ iff
$\ev{\varphi}{M,\rho} = M$ for all valuations $\rho$.
For a pattern set $\Gamma$, called a theory, we write $M \models \Gamma$ iff
$M \models \varphi$ for all $\varphi \in \Gamma$.
We write $\Gamma \models \varphi$ iff for any $M$,
$M \models \Gamma$ implies $M \models \varphi$.

§.§ Matching Logic Proof System

In this section, we present the proof system of matching logic.
Matching logic has a Hilbert-style proof system with
19 simple proof rules, making it small and easy to implement.
The proof system defines the provability relation
written as $\Gamma \vdash \varphi$, where
$\Gamma$ is a set of patterns
(often called a theory and the patterns are called axioms)
and $\varphi$ is a pattern that is said to be provable
from the axioms in $\Gamma$.

Matching Logic Proof System under Locally Nameless Representation

($C_1,C_2$ are application contexts, $FV(\varphi)$ denotes the set of free variables in $\varphi$)

Proof Rule Names     Proof Rules
Proof Rule Names     Proof Rules

Proposition 1     $\varphi_1 \to (\varphi_2 \to \varphi_1)$
Proposition 2

$(\varphi_1 \to (\varphi_2 \to \varphi_3)) \to$
1em$(\varphi_1 \to \varphi_2)\to (\varphi_1 \to \varphi_3)$

Proposition 3     $((\varphi \to \bot) \to \bot) \to \varphi$
Modus Ponens

φ_1 →φ_2

$\opene(\varphi,x) \to \exists \ld \varphi$ with $x \in \EVar$ -8em

(φ_1,x) →φ_2
1[with $x \not\in \FV{\varphi_2}$](∃φ_1) →φ_2

Propagation Left$_\bot$     $\bot \, \varphi \to \bot$
Propagation Right$_\bot$     $\varphi \, \bot \to \bot$

Propagation Left$_\vee$     $(\varphi_1 \vee \varphi_2) \, \varphi_3 \to (\varphi_1 \, \varphi_3) \vee (\varphi_2 \, \varphi_3)$ -10em

Propagation Right$_\vee$     $\varphi_1 \, (\varphi_2 \lor \varphi_3) \to (\varphi_1 \, \varphi_2) \vee (\varphi_1 \, \varphi_3)$ -10em

Propagation Left$_\exists$
$ (\exists \ld \varphi_1) \, \varphi_2 \to \exists \ld \varphi_1 \, \varphi_2$
Propagation Right$_\exists$
$ \varphi_1 \, (\exists \ld \varphi_2) \to \exists \ld \varphi_1 \, \varphi_2$

Framing Left

φ_1 →φ_2
1φ_1   φ_3 →φ_2   φ_3

Framing Right

φ_2 →φ_3
1φ_1   φ_2 →φ_1   φ_3

Pre-Fixpoint    -1em

$\varphi[(\mu \ld \varphi) / \se{0}]\to \mu \ld \varphi$

[rule margin=0pt]
φ_1[φ_2/0] →φ_2
1(μφ_1) →φ_2

Existence     $\exists \ld \ee{0}$
-2em$\neg(C_1[x \land \varphi] \wedge C_2[x \land \neg \varphi])$

We present the proof system of matching logic
in Table <ref>.
To understand it, we first need to define the notion of
contexts and a particular type of contexts called
application contexts.

A context $C$ is simply a pattern with one unique placeholder denoted $\hole$.
We write $C[\varphi]$ to mean the result of plugging $\varphi$ in $\hole$ in the context $C$.
We call $C$ an application context if from the root of $C$ to $\hole$
there are only applications; that is, $C$ is (inductively) constructed as follows:

* $C$ is $\hole$ itself, called the identity context; or

* $C\equiv C_1 \, \varphi$, where $C_1$ is an application context; or

* $C\equiv\varphi \, C_2$, where $C_2$ is an application context.

The proof rules in Table <ref> can be divided into four categories:

* FOL reasoning containing the standard proof rules as in FOL;

* Frame reasoning consisting of six propagation rules and two framing rules, which allow us to propagate formal reasoning that is carried out within an application context throughout the context. Note that we proved these rules equivalent to the ones in [14], where application contexts are not splitted into applications to the left and right;

* Fixpoint reasoning containing the fixpoint rules as in modal $\mu$-calculus;

* Miscellaneous rules.

Next, we state the soundness theorem of the proof system, which has been proved by induction over the structure of the proof $\Gamma \vdash \varphi$ in [14]. We elaborate on the mechanization of this proof in <Ref>.

$\Gamma \vdash \varphi$ implies $\Gamma \models \varphi$.

§.§ Example Matching Logic Theories

First-order logic.

It is easy to see that matching logic is at least as expressive as classical first-order logic, and Chen et al. [13] show that it is indeed more expressive than FOL. At the same time, they describe a direct and natural connection between FOL and matching logic.

A FOL term $t$ is interpreted as an element in the underlying carrier set.
From the matching logic point of view, $t$ is a pattern
that is matched by exactly one element.
We use the terminology functional patterns to refer to
patterns whose valuations are singleton sets.
Intuitively, FOL terms are functional patterns in matching logic.

FOL formulas are interpreted as two logical
values: true and false.
In matching logic, there is a 	simple analogy
where we use the empty set $\emptyset$ to represent the logical false
and the total carrier set to represent the logical true.
A pattern whose interpretation is always $\emptyset$ or the full set
is called a predicate pattern.
Intuitively, FOL formulas are predicate patterns in matching logic.

Although matching logic has no built-in notion of equality, it can be easily defined using a construct called definedness.
Formally, we define $\Sigma^\DEFINEDNESS=\{ \defined{\_} \}$, $\Gamma^\DEFINEDNESS=\{ \defined{x} \}$ ($\defined{x}$ denotes $\defined{\_}\, x$);
this axiom ensures that whenever a pattern $\varphi$ is matched by some model element, the pattern $\defined{\varphi}$ is matched by all elements of the model, and vice versa.
Equality is then defined as a notation $\varphi_1 = \varphi_2 \equiv \neg \defined{\neg (\varphi_1 \leftrightarrow \varphi_2 )}$,
intuitively saying that there is no element that would match only one of the two formulas.
It is easy to see that for any pattern $\varphi$, the pattern $\defined{\varphi}$ is a predicate pattern, and that equality of two patterns is a predicate.

With this, we can similarly define other notations, such as membership, subset, totality, etc. seen below.
To make things easier, we use the notion of matching logic specification introduced in [13].
The signature $\Sigma^\DEFINEDNESS$ and theory $\Gamma^\DEFINEDNESS$ are then defined by Spec. <ref>. For more details on definedness, we refer to <Ref>.

spec $\DEFINEDNESS$
$\Smbs$ $\defined{\_}$
\defined{\varphi} &\equiv& \defined{\_} \, \varphi&
\quad \total{\varphi} &\equiv& \neg \defined{ \neg \varphi} \\
\varphi_1 = \varphi_2 &\equiv& \total{\varphi_1 \leftrightarrow
\varphi_2} &
\quad \varphi_1 \neq \varphi_2 &\equiv& \neg (\varphi_1 = \varphi_2) \\
x \in \varphi &\equiv& \defined{x \wedge \varphi}&
\quad \varphi_1 \subseteq \varphi_2 &\equiv& \total{\varphi_1 \rightarrow
\varphi_2} \\
x \not\in \varphi &\equiv& \neg(x \in \varphi)&
\quad \varphi_1 \not\subseteq \varphi_2 &\equiv& \neg(\varphi_1
\subseteq \varphi_2)
\end{array}$
$\axname{Definedness}$ $\defined{x}$

Definedness and related notions

Induction and transitive closure.

Chen et al. show how matching logic, by using the application and least fixpoint operators, can not only axiomatize equality, but also product types ($\langle \_ , \_ \rangle$), and inductive types [13].

Hence, another notable example of matching logic's expressiveness is that it can specify the transitive closure of a binary relation $R$ the following way (where $\in$ is defined by Spec. <ref>):

\mu X \ld R \lor \exists x \ld \exists y \ld \exists z \ld \langle x,z \rangle \land \langle x, y \rangle \in X \land \langle y, z \rangle \in X

Or rather, the same matching logic pattern expressed in the locally nameless representation:

\mu \ld R \lor \exists \ld \exists \ld \exists \ld \langle \ee{2},\ee{0} \rangle \land \langle \ee{2}, \ee{1} \rangle \in \se{0} \land \langle \ee{1}, \ee{0} \rangle \in \se{0}

§.§ Example: Theory of Sorts

As in the case of equality, matching logic has no built-in support for sorts, but they can be axiomatized as in [13].
One defines a symbol $\mathit{inh}$, a notation $\brac{s} \equiv \mathit{inh}\ s$, and calls the pattern $\brac{s}$
the inhabitant set of $s$ (for any pattern $s$ that represents a sort).
Spec. <ref> then shows a straightforward way of encoding sorted quantification,
denoted as $\forall\left( s\right).\ \varphi$ (where $s$ represents a sort).

spec $\NAIVESORTS$
$\Impts$ $\DEFINEDNESS$
$\Smbs$ $\mathit{inh}$
\brac{s} &\equiv& \mathit{inh} \  s &
\quad \forall\left( s\right).\ \varphi &\equiv& \forall.\ \ee{0} \in \brac{s} \rightarrow \varphi \\
\neg_s \varphi &\equiv& (\neg \varphi) \land \brac{s} &
\quad \exists\left( s\right).\ \varphi &\equiv& \exists.\ \ee{0} \in \brac{s} \land \varphi
\end{array}$

A naive specification of sorts

That mostly works for many use-cases.
However, consider the mathematical (nominal-style) formula
$\forall x : s,\, P(x)$.
In this case we think of $s$ as an argument of the quantifier; $x$ is not yet bound in $s$.
We would want the matching logic pattern $\forall\left( s\right).\ \varphi$ to behave the same.
For example, we may have a dependent sort $\mathit{BV}\ n$ of bitvectors of lenght $n$,
and want to express that the symbol $\mathit{BV\_inc}$ is a function on this sort.
A natural way to express this in the locally nameless matching logic is

\begin{equation}\label{eqn:BVincfunc}
\forall (\mathit{nat}),\ \forall( \mathit{BV}\ \ee{0}),\ \exists( \mathit{BV}\ \ee{1}),\ \mathit{BV\_inc}\ \ee{1} = \ee{0} \, .
\end{equation}

But when using the notations from $\NAIVESORTS$, the above intuition breaks, because the sorts that are passed to the notations contain dangling bound variables.
The problem becomes visible when we expand the notations.
The expansion of the above formula looks like this:

\begin{align*}
&\forall.\ \ee{0} \in \brac{\mathit{nat}} \rightarrow
\forall.\ \ee{0} \in \brac{\mathit{BV}\ \ee{\bm{0}}} \rightarrow \exists.\ \ee{0} \in \brac{\mathit{BV}\ \ee{\bm{1}}} \land \mathit{BV\_inc}\ \ee{1} = \ee{0} \, .
\end{align*}

while we wanted to say rather something like

\begin{align*}
&\forall.\ \ee{0} \in \brac{\mathit{nat}} \rightarrow
\forall.\ \ee{0} \in \brac{\mathit{BV}\ \ee{\bm{1}}} \rightarrow \exists.\ \ee{0} \in \brac{\mathit{BV}\ \ee{\bm{2}}} \land \mathit{BV\_inc}\ \ee{1} = \ee{0} \, .
\end{align*}

(notice the bold de Bruijn indices).
There are multiple possible solutions to this problem: for example, to allow only well-formed patterns as sorts, or to require user to use higher indices in quantifier parameters.
However, the first limits the usefullness of $\NAIVESORTS$, while the second is unnatural and brittle.
We avoid this misunderstanding by defining a pattern-transforming function $\mathit{nest}_\exists$ (and similarly $\mathit{nest}_\mu$)
that increments dangling element (or set, respectively) de Bruijn indices, and
notations for sorted quantification as
in Spec. <ref>.

spec $\SORTS$
$\Impts$ $\DEFINEDNESS$
$\Smbs$ $\mathit{inh}$
\brac{s} &\equiv& \mathit{inh} \  s &
\quad \forall\left( s\right).\ \varphi &\equiv& \forall.\ \ee{0} \in \brac{\mathit{nest}_\exists(s)} \rightarrow \varphi \\
\neg_s \varphi &\equiv& (\neg \varphi) \land \brac{s} &
\quad \exists\left( s\right).\ \varphi &\equiv& \exists.\ \ee{0} \in \brac{\mathit{nest}_\exists(s)} \land \varphi
\end{array}$

A specification of sorts

Intuitively, $\opene(\varphi,x)$ (occuring in the semantics of quantifiers) and $\mathit{nest}_\exists$
cancels each other out.
Formally, we proved a lemma

For any pattern $\varphi$, any element variable $x$ fresh in $\varphi$,

\begin{equation*}
\opene(\mathit{nest}_\exists(\varphi),x) = \varphi  \, .
\end{equation*}

ensuring that a pattern nested inside a quantifier behaves as if it were not nested inside the quantifier,
but as if it were one quantifier level above its occurrence.
That way, we can use the pattern from <ref> to specify the desired property.

§ MATCHING LOGIC FORMALIZATION IN COQ

In this section, we describe how the locally nameless matching logic (as defined in <Ref>) has been encoded in Coq.
The formalization is distributed as a library including the definition of the
logic as well as that of some standard theories, with the two dependencies being the Std++ library [32] and the Equations plugin [39].

Some of our proofs rely on classical and extensionality axioms (namely, functional extensionality, propositional extensionality,
and the axiom of excluded middle), but these are known to be compatible with Coq's logic [9].

We implement matching logic in a deep embedding style; that is, formulas, models, and proofs are represented as data in Coq.

Presumably, a shallow embedding could provide a more lightweight implementation, but deep embedding has couple of advantages for our use cases; mainly, it allows us to inspect matching logic proofs without reflection, reason about them directly (for instance, when checking the side conditions of the deduction theorem from [15]) and to extract them from Coq (see <Ref>)
[It is beyond the scope of this work to tell if a shallow embedding would be more suitable for object-level reasoning.]

§.§ Syntax

We represent a matching logic signature $(\EVar,\SVar,\Sigma)$,
defined in <Ref>, as an instance of the Class Signature that encapsulates the sets of variables and the set of symbols. The sets for variables are required to be countable and infinite, and in addition, it is also required that equality on variables and symbols is decidable.

We also provide an off-the-shelf, string-based instance of the type class as a default option.
Although this instance will suffice for most applications, to prove the completeness of the matching logic proof system, a more general carrier set will be needed[We refer to the proof of the completeness of matching logic without $\mu$ and the extension lemma [15].].

The way we represent free variable names has some features in common with the concept of atoms used in nominal approaches [4] (e.g., any countably infinite set with decidable equality can be used for names), but in the locally nameless approach we do not rely on permutative renaming when implementing capture-avoidance.

We formalize (pseudo-)patterns (Definition <ref>) as the inductive definition
Inductive Pattern : Set.
Due to using a locally nameless embedding,
we have separate constructors for free variables (named
variables) and bound variables (de Bruijn indices).
The main advantage this provides is in the equivalence
of quantified patterns. Specifically, in a fully named representation,
the patterns $\exists x \ld x$ and $\exists y \ld y$ are equivalent,
yet not syntactically equal.
To formally prove their equivalence, we would need a notion of
$\alpha$-equivalence of patterns that is constantly applied.
However, in our locally nameless representation, both these can only
be represented by the pattern $\exists \ld \ee{0}$, and thus are
syntactically equal, so no additional notions of equality need to be
This is implicitly used throughout our soundness proof and in proving
properties of specifications.

For practical reasons, the type Pattern corresponds to the definition
of pseudo-patterns, while the restrictions on non-negativity and scoping defined for patterns (<Ref>) are
implemented as a pair of bool-valued auxiliary functions:

well_formed_positive : Pattern -> bool
well_formed_closed   : Pattern -> bool

where the first function performs a check for the positivity constraint and the second one checks the scoping requirements. The predicate well_formed_closed is constructed from two parts:

well_formed_closed_ex_aux : Pattern -> nat -> bool
well_formed_closed_mu_aux : Pattern -> nat -> bool

These predicates return true, when the parameter pattern contains only smaller unbound de Bruijn indices for element and set variables than the given number.
A pattern is well_formed if it satisfies both well_formed_closed and well_formed_positive.

Most of our functions operate on the type Pattern without the well-formedness constraint;
we use the constraint mainly for theorems.
This way we separate proofs from data.

Substitution and opening.
In the locally nameless representation, there are separate substitution functions for bound and free variables (both for element and set variables). In our formalization, we followed the footsteps of Leroy [31], so the bound variable substitution decrements the indices of those (bound) variables that are greater than the substituted index.

We define

Definition evar_open (k : db_index) (x : evar) (p : Pattern) : Pattern.
Definition svar_open (k : db_index) (X : svar) (p : Pattern) : Pattern.

which correspond to $\opene(\varphi,x)$ and
$\opens(\varphi,X)$ from Section <ref>, with a difference that this version of opening allows for
substitution of any de Bruijn index, not only the one corresponding
to the topmost quantifier (0 or 0).

Derived notations.

Matching logic is intentionally minimal.
As a consequence, any non-trivial theory is likely to heavily rely on notations that abbreviate common operations.
Besides basic notations for boolean operations, universal quantification and greatest fixpoint,
one also can define equality, subset and membership relations on top of the definedness symbol (as we did in Spec. <ref>),
which is not part of matching logic, but is usually considered as a part of
the “standard library” for the core logic.

Coq provides (at least) two ways to extend the syntax of the core logic with derived notations.
The first option is to use Coq's Notation mechanism. For example, the following would define the notations for negation, disjunction, and conjunction:

Notation "! p" := (p —> ?$\bot$?).
Notation "p or q" := (! p —> q).
Notation "p and q" := ! (! p or ! q).

The problem with this is that the pattern

(x —> ?$\bot$?) —> ?$\bot$?

could be interpreted either as ! (! x), or as x or ?$\bot$?,
which would be confusing to the user, having no control on which interpretation Coq chooses to display.

Therefore, we decided to opt for the other option, representing each derived notation as a Coq Definition, as in the following snippet:

Definition patt_not p := p —> ?$\bot$?.
Definition patt_or p q := patt_not p —> q.
Definition patt_and p q := patt_not (patt_or (patt_not p) (patt_not q))

We can define the notations on top of these definitions. This way, the user can fold/unfold derived notations as needed.
However, this representation of notations poses another problem: many functions, especially the substitutions
such as bevar_subst, preserve the structure of the given formula, but since they build a Pattern
from the low-level primitives, the information about derived notations is lost whenever such function is called.
We solve this by defining for each kind of syntactical construct (e.g., for unary operation, binary operation, element variable binder)
a type class containing a rewriting lemma for bevar_subst such as this one:

Class Binary (binary : Pattern -> Pattern -> Pattern) :=

binary_bevar_subst :
forall ?$\psi$?, well_formed_closed ?$\psi$? ->
forall n ?$\phi_1$? ?$\phi_2$?,
bevar_subst (binary ?$\phi_1$? ?$\phi_2$?) ?$\psi$? n
= binary (bevar_subst ?$\phi_1$? ?$\psi$? n) (bevar_subst ?$\phi_2$? ?$\psi$? n) ;
(* ... *)

The user of our library then can instantiate the class for their derived operations
and use the tactic simpl_bevar_subst to simplify the expressions containing bevar_subst and evar_open.

Fresh variables.
We say that a variable is fresh in a pattern $\varphi$ if it does not occur among the free variables of $\varphi$.
Sometimes (for example, in the semantics of existential and fixpoint patterns) it is necessary
to find a variable that does not occur in the given pattern.
We required the variable types (evar and svar) to be infinite, thus we can use the solution of the Coq Std++ library [32] for fresh variable generation.
We then have a function fresh_evar : Pattern -> evar and the following lemma:

Lemma set_evar_fresh_is_fresh ?$\varphi$? : fresh_evar ?$\varphi$? ?$\notin$? free_evars ?$\varphi$?.

§.§ Semantics

On the semantics side
we have a Record Model.
We do not require the carrier set of the model to have decidable equality.
We represent the variable valuation function defined in <Ref> as a record of two separate functions, one mapping element variables to domain elements
and another mapping set variables to sets of domain elements.
With this, we define the interpretation of patterns ($\ev{\_}{M,\rho}$ in
<Ref>) as expected, with two points worth noting:

* The interpretation of patterns cannot be defined using structural recursion on the formula,
because in the $\mu$ (and $\exists$) case,
one calls eval on svar_open 0 X p' (and evar_open 0 x p'), which is not a structural subformula

of p. Therefore, we do recursion over the size of the formula,
implemented as an Equation:

Equations eval (?$\rho$? : @Valuation M) (?$\varphi$? : Pattern) : propset (@Domain M) by wf (size ?$\varphi$?) :=
(* ... *)
eval ?$\rho$? (patt_mu ?$\varphi'$?) := let X := fresh_svar ?$\varphi'$? in
@LeastFixpointOf _ OS L (fun S =>
let ?$\rho'$? := (update_svar_val X S ?$\rho$?) in
eval ?$\rho'$? (svar_open 0 X ?$\varphi'$?)).

* We decided to give semantics to patterns that are not well-formed, including arbitrary $\mu$ patterns.
This way, we do not have to supply the eval function
with the well-formedness constraint, which makes it easier to use.
We did that by
(1) defining the function LeastFixpointOf to return
the intersection of all prefixpoints;
(2) mechanizing the relevant part of the Knaster-Tarski fixpoint theorem [40], and
(3) proving that the function associated to a well-formed $\mu$ pattern is monotone.

§.§ Proof System

We formalize the proof system of matching logic as an inductive definition:

Inductive ML_proof_system theory : Pattern -> Set := (* ... *) .

The proof system is defined as expected; however, one may ask why the proof system lives in Set
and not in Prop.
The answer is that in our deep embedding we care about the internal structure of matching logic proofs, not only about provability.
We do not want two matching logic proofs to be considered identical only because they prove the same formula,
for at least two reasons.

First, some theorems (e.g. the deduction theorem from [15]) can only be applied to a proof if that proof satisfies particular
conditions regarding its internal structure.
Second, when extracting OCaml or Haskell programs from this Coq formalization,
we need the manipulation of the proof system terms to be preserved;
that will allow us to extract Metamath proof objects in the future (see <Ref>).

Another point worth mentioning is that the rules in the formalization of the proof system
often require some well-formedness constraints.
A consequence of this is that only well-formed patterns are provable:

Lemma proved_impl_wf ?$\Gamma$? ?$\phi$?: ?$\Gamma$? ?$\vdash$? ?$\phi$? -> well_formed ?$\phi$?.

We discuss the soundness of the proof system in
Section <ref>.
Crucially, we rely on the $\mu$ patterns to be interpreted as
least fixpoints, as explained in Section <ref>.

§ REASONING ABOUT MATCHING LOGIC

After encoding matching logic in Coq, we overview some results it allows for concerning meta-level reasoning. In particular, we highlight some challenges we faced when proving the mechanized matching logic proof system sound, and we demonstrate semantics-based reasoning about the theory of equality.

§.§ Soundness of The Proof System

The most crucial result of the mechanization of matching logic is the proof of the soundness of its proof system (<Ref>). Even though this theorem has already been investigated in related publications, we have developed the first complete, machine-checked proof, which verifies the prior paper-based results.

We state our soundness theorem below:

Theorem Soundness : forall phi : Pattern, forall theory : Theory,
well_formed phi -> theory ?$\vdash$? phi -> theory ?$\vDash$? phi.

The proof of soundness begins via induction on the hypothesis
theory ?$\vdash$? phi, meaning we consider all cases from
the proof system which may have produced this hypothesis.
Many cases, such as the propositional proof rules, were straightforwardly discharged
using set reasoning. Other cases, like Modus Ponens, were discharged via
the application of the induction hypothesis.

The most involved cases were the proof rules involving quantification,
specifically the $\exists$-Quantifier, Prefixpoint, and
Knaster-Tarski rules.
For these rules, the key steps were to establish complex substitution lemmas (separate
lemmas for existential quantification and for $\mu$-quantification).
The proofs of these lemmas were very involved, and we note that the set substitution lemma was not proved in related work previously. For existential quantification, we adapt the
“element substitution lemma” which appears
in <cit.>.

For the soundness of the Pre-fixpoint and Knaster-Tarski rules with $\mu$-quantification,
we introduce a new similar lemma called
set substitution lemma, which
links syntactic substitution with semantic substitution,
stating that the
following two ways of plugging a pattern $\varphi_2$ into a pattern
$\varphi_1$ are equivalent:

* syntactically substitute $\varphi_2$ for a free set variable $X$ in $\varphi_1$ and interpret the resulting pattern;

* interpret $\varphi_2$ separately, then interpret $\varphi_1$ in a valuation where $X$ is mapped to the value of $\varphi_2$.

§.§ Theory of Equality

The formalization also allows for reasoning about matching logic models. We implemented the theory of definedness and equality as presented in [13, 38], and <Ref>. Then, we established some results about models that satisfy the definedness axiom, which provides support for common cases of semantic reasoning. This branch of the development showcases applications of our mechanization for reasoning about matching logic models.

Definedness and totality.

Definedness has the important property that, applied to any formula $\varphi$ which matches at least one model element, the result matches all elements of the model (represented by $\top$):

Lemma definedness_not_empty_iff : forall (M : @Model ?$\Sigma$?),
M ?$\vDash^T$? theory ->
forall (?$\phi$? : Pattern) (?$\rho_e$? : @EVarVal ?$\Sigma$? M) (?$\rho_s$? : @SVarVal ?$\Sigma$? M),
(@eval ?$\Sigma$? M ?$\rho_e$? ?$\rho_s$? ?$\phi$?) <> ?$\emptyset$? <-> (@eval ?$\Sigma$? M ?$\rho_e$? ?$\rho_s$? ?$\lceil$? ?$\phi$? ?$\rceil$? ) = ?$\top$?.

This is why it is called definedness: $\lceil \phi \rceil $ evaluates to full set if and only if $\phi$ is defined;
that is, matched by at least one element.
Note that one needs the definedness axiom only for the “if” part;
the “only if” part is guaranteed by the definition of the extension of application:
anything applied to the empty set results in the empty set.
The dual of definedness is called totality: a pattern $\phi$ is considered total iff it is matched by all elements of the model, and totality of a pattern ($\lfloor \phi \rfloor$) holds (is matched by all elements of the model) only in that case:

Lemma totality_not_full_iff : forall (M : @Model ?$\Sigma$?),
M ?$\vDash^T$? theory ->
forall (?$\phi$? : Pattern) (?$\rho_e$? : @EVarVal ?$\Sigma$? M) (?$\rho_s$? : @SVarVal ?$\Sigma$? M),
@eval ?$\Sigma$? M ?$\rho_e$? ?$\rho_s$? ?$\phi$? <> ?$\top$? <-> @eval ?$\Sigma$? M ?$\rho_e$? ?$\rho_s$? ?$\lfloor$? ?$\phi$? ?$\rfloor$? = ?$\emptyset$?.

As we have seen in <Ref>, equality is defined using totality.
We proved that equality defined this way indeed has the intended property, i.e., equality of two patterns holds iff the two patterns are interpreted to equal sets.

Lemma equal_iff_interpr_same : forall (M : @Model ?$\Sigma$?),
M ?$\vDash^T$? theory ->
forall (?$\phi1$? ?$\phi2$? : Pattern) (?$\rho_e$? : @EVarVal ?$\Sigma$? M) (?$\rho_s$? : @SVarVal ?$\Sigma$? M),
@eval ?$\Sigma$? M ?$\rho_e$? ?$\rho_s$? (?$\phi$?1 =ml ?$\phi$?2) = ?$\top$? <->
@eval ?$\Sigma$? M ?$\rho_e$? ?$\rho_s$? ?$\phi1$? = @eval ?$\Sigma$? M ?$\rho_e$? ?$\rho_s$? ?$\phi2$?.

Our formalization also demonstrates that in matching logic, one cannot simply use equivalence ($\leftrightarrow$) instead of equality.
As argued in [38], one could expect that the pattern
$\exists \ld f\ x \leftrightarrow \ee{0}$ specifies that $f$ behaves like a function;
however, there exists a model in which that is not the case.
In the model whose domain is exampleDomain and whose interpretation of
application is defined as example_app_interp below:

Inductive exampleDomain : Set := one | two | f.
Definition example_app_interp (d1 d2 : exampleDomain) : Power exampleDomain :=
match d1, d2 with
| f, one => ?$\top$?
| f, two => ?$\emptyset$?
| _, _ => ?$\emptyset$?

the pattern
$\exists.\, f\ x \leftrightarrow \ee{0}$ holds (in every interpretation of $x$),
even though the model does not implement $f$ as a function. For more technical details, we refer to the formalization [2].

§ REASONING IN MATCHING LOGIC

In <Ref>, we encoded matching logic and its proof system in Coq. With the minimal proof system, one can already reason about syntactic consequence by using Coq's apply tactic.
However, only using the presented rules to reason about derived operations and complex theories is not really productive: it is easy to get lost when facing a complex proof obligation expressed in vanilla matching logic after unfolding the derived notations.

Derived rules.

To support object-level reasoning, we proved several derived axioms and rules, essentially enriching the proof system with rules about derived constructs (commonly used operations that are not included in the syntax of matching logic) and common theories (such as definedness). These alone can shorten a typical matching logic proof script significantly. For example, think of destructing a disjunctive premise into two premises, which is naturally one step in an informal proof, but takes a couple of steps with the matching logic proof system. However, writing proofs with the derived rules is still cumbersome, because now we get lost in the details of combining and applying these theorems with the correct parameters. We tackle this problem with a dedicated Coq proof mode.

§.§ Matching Logic Proof Mode

To further simplify reasoning in the embedded logic, we conceptually separate the matching logic proof state from the Coq proof state, introduce a local proof context, and define a set of special Coq tactics that manipulate the dedicated proof state. We call these concepts together the matching logic proof mode[We borrow the term proof mode and the approach from the authors of the Iris proof mode [30], and the Coq reference manual [1].]. The ultimate goal with the proof mode is to make matching logic proofs simple to read and write, especially for users familiar with Coq.

The contents of this section are work-in-progress, but nicely demonstrate the potential that lies in carrying out interactive matching logic proofs in Coq.

Matching logic proof state.

The concept of the proof state allows us to nicely mimic Coq-style reasoning in matching logic by rendering matching logic proof goals as a list of named hypotheses and a goal pattern. Behind the scenes, the goal on provability is turned into a record that stores the list of the premises along with the conclusion.
The proof mode allows for moving left-hand sides of implication conclusions to the list of premises (the local context), which is essential in matching logic as the deduction theorem [15] can be applied to totality patterns only.

The proof mode provides a better overview on the state of the proof in the interactive mode. In particular, it contains the following sections:

* A meta-level context (such as hypotheses on the well-formedness of patterns)

* A global matching logic context (a set of patterns known to be valid);

* A local matching logic context (a named list of patterns assumed to be valid);

* A matching logic goal (a single pattern, the conclusion).

We provide a notation for this proof state, which also resembles the proof state in Coq (see <Ref>). In this
example, $\phi_1, \dots, \phi_n$ form the global matching logic context, while $\psi_1, \dots, \psi_n$ form the local one, and $\chi$ is the goal.
A matching logic proof state can automatically be converted to a syntactic provability statement as presented in <Ref>
which describes this conversion of the proof state in <Ref>.

?$\phi_1$?, ?$\dots$?, ?$\phi_n$?, ?$\psi_1$?, ?$\dots$?, ?$\psi_m$?, ?$\chi$? : Pattern
[?$\phi_1, \dots, \phi_n$?] ?$\vdash$?
"H1" : ?$\psi_1$?
"Hn" : ?$\psi_m$?

?$\phi_1$?, ?$\dots$?, ?$\phi_n$?, ?$\psi_1$?, ?$\dots$?, ?$\psi_m$?, ?$\chi$? : Pattern
[?$\phi_1, \dots, \phi_n$?] ?$\vdash$? ?$\psi_1$? —> ?$\dots$? —> ?$\psi_m$? —> ?$\chi$?

Matching logic proof state

The mapping between matching logic proof states and matching logic proofs of syntactic consequence is not injective: there can be multiple proof states that represent the same matching logic proof obligation when the the conclusion is an implication pattern.

Matching logic proof tactics.

To create proof tactics, we first lift the derived proof rules to work with matching logic proof states. By lifting,
we actually mean proving the derived rules for the new proof state. The created tactics can be divided into three main groups:

* Tactics that restructure the local context (e.g., mlIntro, mlRevertLast, mlClear).

* Tactics that apply lifted derived rules to the proof state (e.g., mlApply, mlApplyMeta, mlDestructOr).

* Miscellaneous tactics (e.g., mlRewrite which replaces parts of the matching logic goal, mlTauto which is a preliminary
tautology solver).

We can use these tactics in a similar way as their Coq counterparts (e.g., mlIntro mimics the effect of intro), and create matching logic syntactic proofs conveniently. For the sake of brevity, we do not go into details about the implementation of the tactics, but in the background, they expand to applications of the proof system rules, therefore they construct valid matching logic proofs.

§.§ An Interactive Proof

In this section, we show an interactive proof outline (<Ref>) with the matching logic proof mode. The complete proof is available in the
formalization [2] (moreover, there is also a short tutorial about the currently formalized tactics). We show an example proof state transformation from each tactic category, but first, we present two lemmas that
are essential to construct the proof.

?$1.$?  Lemma overlapping_variables_equal ?$\Sigma$? : Signature syntax : Syntax :
?$2.$?    forall x y ?$\Gamma$?, theory ?$\subseteq$? ?$\Gamma$? ->
?$3.$?    ?$\Gamma$? ?$\vdash$? ?$\lceil$? (patt_free_evar y) and (patt_free_evar x) ?$\rceil$? —>
?$4.$?           patt_free_evar y  =ml  patt_free_evar x.
?$5.$?  Proof.
?$6.$?    intros x y ?$\Gamma$? H?$\Gamma$?.
?$7.$?    remember (patt_free_evar x) as pX. assert (well_formed pX) by (rewrite HeqpX;auto).
?$8.$?    remember (patt_free_evar y) as pY. assert (well_formed pY) by (rewrite HeqpY;auto).
?$9.$?    toMLGoal. wf_auto2.
?$10.$?   unfold patt_equal, patt_iff.
?$\textlabel{11.}{l11}$?   mlRewrite (@patt_total_and ?$\Sigma$? syntax ?$\Gamma$?
?$12.$?                                 (pY —> pX)
?$13.$?                                 (pX —> pY) H?$\Gamma$?
?$14.$?                                 ltac:(wf_auto2) ltac:(wf_auto2)) at 1.
?$\textlabel{15.}{l15}$?   mlIntro "H0". mlIntro "H1". mlDestructOr "H1" as "H1'" "H1'".
?$\textlabel{16.}{l16}$?.   * mlApply "H1'". mlClear "H1'". mlIntro "H2".
?$17.$?     (* ... *)
?$18.$?   * (* ... *)
?$19.$? Defined.

Case Study for the Proof Mode

The first lemma is about the connection of conjunction and totality.

Lemma patt_total_and ?$\Sigma$? : Signature syntax : Syntax:
forall ?$\Gamma$? ?$\varphi$? ?$\psi$?, theory ?$\subseteq$? ?$\Gamma$? -> well_formed ?$\varphi$? -> well_formed ?$\psi$? ->
?$\Gamma$? ?$\vdash$? ?$\lfloor$? ?$\varphi$? and ?$\psi$? ?$\rfloor$? <—> ?$\lfloor$? ?$\varphi$? ?$\rfloor$? and ?$\lfloor$? ?$\psi$? ?$\rfloor$?.

The second lemma is the congruence lemma, which states that one can replace equivalent subpatterns in any context results in equivalent patterns.

Lemma prf_equiv_congruence ?$\Gamma$? p q C:
PC_wf C -> ?$\Gamma$? ?$\vdash$? (p <—> q) -> ?$\Gamma$? ?$\vdash$? ((C [p]) <—> (C [q])).

We implemented mlRewrite based on the congruence lemma. At line <ref> (<Ref>) we can use this tactic with the first lemma, since it states the equivalence of two patterns. With this, we are able to propagate totality to the subpatterns of the conjunction for our concrete patterns.

?$\Gamma$? ?$\vdash$?
?$\lceil$? pY and pX ?$\rceil$? —>
?$\lfloor$? (pY —> pX) and (pX —> pY) ?$\rfloor$?

?$\Gamma$? ?$\vdash$?
?$\lceil$? pY and pX ?$\rceil$? —>
?$\lfloor$? (pY —> pX) ?$\rfloor$? and ?$\lfloor$? (pX —> pY) ?$\rfloor$?

Next, in line <ref>, we reshape the structure of the matching logic proof state by using mlIntro twice. This tactic
moves the left-hand side of the implication in the goal to the local matching logic context (note that conjunction is a syntactic sugar).

?$\Gamma$? ?$\vdash$?
?$\lceil$? pY and pX ?$\rceil$? —>
?$\lfloor$? (pY —> pX) ?$\rfloor$? and ?$\lfloor$? (pX —> pY) ?$\rfloor$?

?$\Gamma$? ?$\vdash$?
"H0" : ?$\lceil$? pY and pX ?$\rceil$?,
"H1" : ! ?$\lfloor$? pY —> pX ?$\rfloor$? or ! ?$\lfloor$? pX —> pY ?$\rfloor$?,

Finally, we also show the usage of mlApply in line <ref>. The conclusion of "H1'" matches the goal,
thus we can apply it, and show its premise.

?$\Gamma$? ?$\vdash$?
"H0" : ?$\lceil$? pY and pX ?$\rceil$?,
"H1'" : ! ?$\lfloor$? pY —> pX ?$\rfloor$?,

?$\Gamma$? ?$\vdash$?
"H0" : ?$\lceil$? pY and pX ?$\rceil$?,
"H1'" : ?$\lfloor$? pY —> pX ?$\rfloor$? —> ?$\bot$?,
?$\lfloor$? pY —> pX ?$\rfloor$?

It can be observed that we used a number of standard Coq tactics, and explicit parameters during the proof (in <Ref>). It is ongoing work to continue refining the proof mode and adding new tactics on demand to formalize as many paper-based matching logic proofs in Coq as possible.

§ RELATED WORK

§.§ Embedding Logical Languages in Coq

Ideally, different sorts of problems are specified in different logical languages which fit the problem domain best. For instance, separation logics excel at describing algorithms manipulating shared and mutable states, temporal logics provide abstractions for specifying systems properties qualified in terms of time, whereas matching logic gives a fairly generic basis for reasoning about programming language semantics and program behavior. It is highly desired to carry out proofs in these domain-specific logical systems interactively and mechanically verified, but these logics tend to significantly diverge from the logics of general-purpose proof assistants such as Coq, leading to an abstraction gap.

To use a proof assistant to formalize reasoning in a specific logic, one needs to encode the logic as a theory in the proof assistant and then carry out reasoning at the meta-level with considerable overhead. Related works have been investigating different ways of embedding with the aim of reducing the overhead and facilitate productive object-level reasoning in various logical languages. To name a few, (focused) linear logic [37, 43], linear temporal logic [17], different dialects of separation logic [29, 34, 3] and differential dynamic logic [8] have been addressed in the past. Note that some of these encodings are full-featured proof modes, which create a properly separated proof environment and tactic language for the object logic. A slightly different idea worth mentioning is encoding one theorem prover’s logic in another to make the proofs portable, such as taking HOL proofs to Coq [42, 28].

The existing approaches show significant differences depending upon whether the formalization is aimed at proving the properties of the logic or at advocating reasoning in the logic. One particular consideration is to variable representation and the level of embedding. The majority of the cited formalizations apply a so-called shallow embedding, where they reuse core elements of the meta-logic; for instance, names are realized by using higher-order abstract syntax or the parametrized variant thereof, and exploit the binding and substitution mechanism built-in the proof assistant. With this, name binding, scopes, and substitution come for free, but the formalization is tied to the meta-logic’s semantics in this aspect, which may not be suitable in all cases. In fact, one of the main design decisions in our work was to use deep embedding facilitated by notations and locally nameless variable representation.

§.§ Matching Logic Implementations

This paper is not the only attempt that tries to formalize matching logic
using a formal system.
In [11], the authors propose a matching logic formalization based on Metamath [35], a formal language used to encode abstract mathematical axioms and theorems.
The syntax and proof system of matching logic are defined in Metamath
in a few hundreds lines of code [25].
Matching logic (meta)theorems can be formally stated in Metamath, and
their formal proofs can be encoded in Metamath as machine-checkable proof objects.
While the Metamath implementation is simpler with a smaller trust base, the
Coq formalization of matching logic is more versatile; in Coq one can
express a larger variety of metatheorems such as the deduction theorem.
In general, the Metamath formalization focuses only on proofs of explicit
matching logic theories, while our formalization, despite a larger trust-base,
focuses mostly on models, semantics, and metatheorems of matching logic.
This dichotomy allows for potential integration with the Metamath formalization (see <ref>).

Another matching logic implementation is through the framework.
The framework is a very robust engine for formalizing programming
language syntax and semantics. A version of matching logic, called
Kore, is used by to represent processed formal semantics. This is
how full large-scale languages can be simply represented as matching
logic theories. Admittedly, defining matching logic theories on the
scale of programming languages directly in Coq is not currently feasible.
However, our formalization brings more interactivity to matching logic reasoning,
which is currently missing in .

§ CONCLUSION AND FUTURE WORK

In this work, we defined a locally nameless representation of matching logic.
We also presented the first formal
definition of any version of matching logic using an interactive
theorem prover, namely Coq.
We mechanized the soundness theorem of matching logic, and presented some nontrivial matching logic theories and
interactive proofs with a preliminary matching logic proof mode.

We believe this paves the way for Coq and interactive theorem provers to be
used more frequently with matching logic. We discuss some areas for
future work below.

* Complete Coq Proof Mode for Matching Logic.
Proving formulas using the matching logic Hilbert-style proof system is not always convenient,
especially when compared to the way one can prove theorems in Coq.
For this reason we are working on the presented proof mode for matching logic in Coq,
that allows users to prove matching logic theorems using tactics that manipulate the goal
and local context.
We took the inspiration mainly from the Iris project, where the authors built a proof mode
for a variant of separation logic [30].

* Create Tactics for Type Class Instantiation.  While using the formalization with actual signatures or new derived notations,
the user needs to instantiate certain simple type classes. We plan to create tactics to carry out this work automatically.

* Exporting Metamath Proof Objects.
An interesting way of combining advantages of both our Coq
formalization and the Metamath formalization
in [11] would be the ability to convert matching
logic proofs in Coq to matching logic proofs in Metamath.
One challenge here is posed by the fact that Metamath uses the traditional named
representation of matching logic patterns, which is different from the
locally nameless representation used in our Coq development.

* Importing Definitions.
As mentioned in Section <ref>, the framework
is a matching logic (specifically Kore) implementation with the
advantage of being able to naturally define real large-scale
programming languages.
As future work, we plan to formalize Kore as a matching logic theory inside Coq
and write a translator from Kore files to Coq files using this theory,
thus giving framework a Coq-based backend.
This would allow languages defined in and properties of those
languages proved in to be automatically translated to Coq
definitions and theorems.

* Completeness.
For the fragment of matching logic without the $\mu$ operator, the proof system is complete.
We would like to formalize the proof of completeness from [15];
however, we expect the proof to be non-constructive, which implies we would not be able
to compute proof terms (and extract Metamath proofs) from proofs of semantic validity.

Acknowledgements. We warmly thank Runtime Verification Inc. for their generous funding support. Supported by the ÚNKP-21-4 New National Excellence Program of the Ministry for Innovation and Technology from the source of the National Research, Development and Innovation Fund.

[1]
titleCoq reference manual.
noteAccessed on 20th, July 2022.

[2]
titleMatching logic formalization.
noteAccessed on 12th, September 2022.

[3]
authorAndrew W. Appel &
authorSandrine Blazy
(year2007): titleSeparation logic for small-step
In: booktitleInternational Conference on Theorem
Proving in Higher Order Logics, organizationSpringer, pp.
pages5–21, 10.1007/978-3-540-74591-4_3.

[4]
authorBrian Aydemir,
authorAaron Bohannon &
authorStephanie Weirich
(year2007): titleNominal reasoning techniques in
journalElectron. Notes Theor. Comput. Sci.
volume174(number5), p. pages69–77,

[5]
authorBrian E. Aydemir et al.
(year2005): titleMechanized metatheory for the
masses: The PoplMark challenge.
In editorJoe Hurd &
editorTom Melham, editors: booktitleTheorem Proving in Higher Order Logics,
publisherSpringer Berlin Heidelberg, addressBerlin,
Heidelberg, pp. pages50–65, 10.1007/11541868_4.

[6]
authorYves Bertot &
authorPierre Casteran
(year2004): titleInteractive theorem proving and
program development: Coq'Art: The Calculus of Inductive
seriesTexts in Theoretical Computer Science An EATCS
Series, publisherSpringer Berlin Heidelberg,
addressBerlin, Heidelberg, 10.1007/978-3-662-07964-5.

[7]
authorDenis Bogdanas &
authorGrigore Roşu
(year2015): titleK-Java: A complete
semantics of Java.
In editorSriram K. Rajamani &
editorDavid Walker, editors: booktitleProceedings of the 42nd Annual ACM SIGPLAN-SIGACT
Symposium on Principles of Programming Languages, POPL 2015, Mumbai, India,
January 15-17, 2015, publisherACM, pp.
pages445–456, 10.1145/2676726.2676982.

[8]
authorBrandon Bohrer,
authorVincent Rahli,
authorIvana Vukotic,
authorMarcus Völp &
authorAndré Platzer
(year2017): titleFormally verified differential
dynamic logic.
In: booktitleProceedings of the 6th ACM SIGPLAN
Conference on Certified Programs and Proofs, seriesCPP 2017,
publisherAssociation for Computing Machinery,
addressNew York, NY, USA, p. pages208–221,

[9]
authorMario Carneiro
(year2019): titleThe type theory of Lean.
Master's thesis.
noteAccessed on 12th, September 2022.

[10]
authorArthur Charguéraud
(year2012): titleThe locally nameless
journalJ. Autom. Reason.
volume49(number3), pp. pages363–408,

[11]
authorXiaohong Chen,
authorZhengyao Lin,
authorMinh-Thai Trinh &
authorGrigore Roşu
(year2021): titleTowards a trustworthy
semantics-based language framework via proof generation.
In editorAlexandra Silva &
editorK. Rustan M. Leino, editors:
booktitleComputer Aided Verification - 33rd
International Conference, CAV 2021, Virtual Event, July 20-23, 2021,
Proceedings, Part II, seriesLecture Notes in
Computer Science volume12760, publisherSpringer,
pp. pages477–499, 10.1007/978-3-030-81688-9_23.

[12]
authorXiaohong Chen,
authorDorel Lucanu &
authorGrigore Roşu
(year2020): titleInitial algebra semantics in
matching logic.
typeTechnical Report.
noteAccessed on 12th, September 2022.

[13]
authorXiaohong Chen,
authorDorel Lucanu &
authorGrigore Roşu
(year2021): titleMatching logic explained.
journalJournal of Logical and Algebraic Methods
in Programming, p. pages100638,

[14]
authorXiaohong Chen &
authorGrigore Roşu
(year2019): titleMatching \(\mu\)-Logic.
In: booktitle34th Annual ACM/IEEE Symposium on
Logic in Computer Science, LICS 2019, Vancouver, BC, Canada, June 24-27,
2019, publisherIEEE, pp. pages1–13,

[15]
authorXiaohong Chen &
authorGrigore Roşu
(year2019): titleMatching mu-logic.
typeTechnical Report, institutionUniversity of
Illinois at Urbana-Champaign.
noteAccessed on 12th, September 2022.

[16]
authorXiaohong Chen &
authorGrigore Roşu
(year2020): titleA general approach to define
binders using matching logic.
journalProc. ACM Program. Lang.
volume4(numberICFP), pp.
pages88:1–88:32, 10.1145/3408970.

[17]
authorSolange Coupet-Grimal
(year2003): titleAn axiomatization of linear
temporal logic in the Calculus of Inductive Constructions.
journalJournal of Logic and Computation
volume13(number6), pp. pages801–813,

[18]
authorSandeep Dasgupta,
authorDaejun Park,
authorTheodoros Kasampalis,
authorVikram S. Adve &
authorGrigore Roşu:
titleA complete formal semantics of x86-64 user-level
instruction set architecture.
In: booktitleProceedings of the
40th ACM SIGPLAN Conference on Programming Language Design
and Implementation (PLDI'19), publisherACM, pp.
pages1133–1148, 10.1145/3314221.3314601.

[19]
authorLeonardo De Moura &
authorNikolaj Bjørner:
titleZ3: An efficient SMT solver.
In: booktitleProceedings of the
14th International Conference on Tools and Algorithms for
the Construction and Analysis of Systems (TACAS'08),
publisherSpringer, pp. pages337–340,

[20]
authorAndrew D. Gordon
(year1993): titleA mechanisation of
name-carrying syntax up to alpha-conversion.
In editorJeffrey J. Joyce &
editorCarl-Johan H. Seger, editors:
booktitleHigher Order Logic Theorem Proving and its
Applications, 6th International Workshop, HUG '93, Vancouver, BC, Canada,
August 11-13, 1993, Proceedings, seriesLecture Notes
in Computer Science volume780, publisherSpringer,
pp. pages413–425, 10.1007/3-540-57826-9_152.

[21]
authorDwight Guth: titleA
formal semantics of Python 3.3.
noteAccessed on 12th, September 2022.

[22]
authorDwight Guth, authorChris
Hathhorn, authorManasvi Saxena & authorGrigore Roşu: titleRV-Match: Practical
semantics-based program analysis.
In: booktitleProceedings of the
28th International Conference on Computer Aided
Verification (CAV'16), volume9779,
publisherSpringer, pp. pages447–453,

[23]
authorChris Hathhorn,
authorChucky Ellison &
authorGrigore Roşu:
titleDefining the undefinedness of C.
In: booktitleProceedings of the
36th annual ACM SIGPLAN Conference on Programming Language
Design and Implementation (PLDI'15), publisherACM, pp.
pages336–345, 10.1145/2813885.2737979.

[24]
authorEverett Hildenbrandt,
authorManasvi Saxena,
authorXiaoran Zhu,
authorNishant Rodrigues,
authorPhilip Daian,
authorDwight Guth,
authorBrandon Moore,
authorYi Zhang, authorDaejun
Park, authorAndrei Ştefănescu & authorGrigore Roşu: titleKEVM: A complete semantics of
the Ethereum virtual machine.
In: booktitleProceedings of the 2018 IEEE
Computer Security Foundations Symposium (CSF'18),
publisherIEEE, pp. pages204–217,

[25]
authorK Team:
titleMatching logic proof checker.
noteAccessed on 29th, April 2022.

[26]
authorShuanglong Kan,
authorDavid Sanan,
authorShang-Wei Lin &
authorYang Liu:
titleKRust: An executable formal semantics for Rust,

[27]
authorTheodoros Kasampalis,
authorDaejun Park,
authorZhengyao Lin,
authorVikram S. Adve &
authorGrigore Roşu:
titleLanguage-parametric compiler validation with
application to LLVM.
In: booktitleProceedings of the
26th ACM International Conference on Architectural Support
for Programming Languages and Operating Systems, seriesASPLOS
2021, publisherAssociation for Computing Machinery,
addressNew York, NY, USA, pp. pages1004–1019,

[28]
authorChantal Keller &
authorBenjamin Werner
(year2010): titleImporting HOL Light into
In: booktitleInternational Conference on
Interactive Theorem Proving, organizationSpringer, pp.
pages307–322, 10.1007/978-3-642-14052-5_22.

[29]
authorRobbert Krebbers,
authorJacques-Henri Jourdan,
authorRalf Jung, authorJoseph
Tassarotti, authorJan-Oliver
Kaiser, authorAmin Timany, authorArthur Charguéraud & authorDerek Dreyer (year2018): titleMoSeL: A
general, extensible modal framework for interactive proofs in separation
journalProceedings of the ACM on Programming
Languages volume2(numberICFP), pp.
pages1–30, 10.1145/3236772.

[30]
authorRobbert Krebbers,
authorAmin Timany &
authorLars Birkedal
(year2017): titleInteractive proofs in
higher-order concurrent separation logic.
In editorGiuseppe Castagna &
editorAndrew D. Gordon, editors:
booktitleProceedings of the 44th ACM SIGPLAN
Symposium on Principles of Programming Languages, POPL 2017, Paris, France,
January 18-20, 2017, publisherACM, pp.
pages205–217, 10.1145/3009837.3009855.

[31]
authorXavier Leroy (year2007):
titleA locally nameless solution to the POPLmark
noteAccessed on 12th, September 2022.

[32]
authorMax Planck Institute for Software
Systems: titleCoq-std++: An extended
"standard library" for Coq.
noteAccessed on 12th, September 2022.

[33]
authorConor McBride &
authorJames McKinna
(year2004): titleFunctional pearl: I am not a
number-I am a free variable.
In editorHenrik Nilsson, editor:
booktitleProceedings of the ACM SIGPLAN Workshop on
Haskell, Haskell 2004, Snowbird, UT, USA, September 22-22, 2004,
publisherACM, pp. pages1–9,

[34]
authorAndrew McCreight
(year2009): titlePractical tactics for
separation logic.
In: booktitleInternational Conference on Theorem
Proving in Higher Order Logics, organizationSpringer, pp.
pages343–358, 10.1007/978-3-642-03359-9_24.

[35]
authorNorman Megill &
authorDavid A. Wheeler:
titleMetamath: A computer language for mathematical
noteAccessed on 12th, September 2022.

[36]
authorDaejun Park, authorAndrei
Stefanescu & authorGrigore
Roşu (year2015):
titleKJS: a complete formal semantics of JavaScript.
In editorDavid Grove &
editorSteve Blackburn, editors:
booktitleProceedings of the 36th ACM SIGPLAN
Conference on Programming Language Design and Implementation, Portland, OR,
USA, June 15-17, 2015, publisherACM, pp.
pages346–356, 10.1145/2737924.2737991.

[37]
authorJames F Power &
authorCaroline Webster
(year1999): titleWorking with linear logic in
noteAccessed on 12th, September 2022.

[38]
authorGrigore Roşu
(year2017): titleMatching logic.
journalLog. Methods Comput. Sci.
volume13(number4), 10.23638/LMCS-13(4:28)2017.

[39]
authorMatthieu Sozeau &
authorCyprien Mangin
(year2019): titleEquations reloaded: high-level
dependently-typed functional programming and proving in Coq.
journalProc. ACM Program. Lang.
volume3(numberICFP), 10.1145/3341690.

[40]
authorAlfred Tarski
(year1955): titleA lattice-theoretical fixpoint
theorem and its applications.
journalPacific J. Math.
volume5(number2), pp. pages285–309,

[41]
authorFeng Wang,
authorFu Song, authorMin
Zhang, authorXiaoran Zhu & authorJun Zhang:
titleKRust: A formal executable semantics of Rust.
In: booktitleProceedings of the
12th International Symposium on Theoretical Aspects of
Software Engineering (TASE'18), publisherIEEE, pp.
pages44–51, 10.1109/TASE.2018.00014.

[42]
authorFreek Wiedijk
(year2007): titleEncoding the HOL Light
logic in Coq.
<https://www.cs.ru.nl/ freek/notes/holl2coq.pdf>.
noteAccessed on 12th, September 2022.

[43]
authorBruno Xavier,
authorCarlos Olarte,
authorGiselle Reis &
authorVivek Nigam
(year2018): titleMechanizing focused linear
logic in Coq.
journalElectronic Notes in Theoretical Computer
Science volume338, pp. pages219–236,