Jasmin Blanchette
email: jasmin.blanchette@ifi.lmu.de

Qi Qiu
email: qi.qiu@univ-lyon1.fr

Sophie Tourret
email: sophie.tourret@inria.fr

Verified Given Clause Procedures

Keywords: Saturation provers, Proof assistants, Stepwise refinement

Resolution and superpostion provers rely on the given clause procedure to saturate clause sets. Using Isabelle/HOL, we formally verify four variants of the procedure: the well-known Otter and DISCOUNT loops as well as the newer iProver and Zipperposition loops. For each of the variants, we show that the procedure guarantees saturation, given a fair data structure to store the formulas that wait to be selected. Our formalization of the Zipperposition loop clarifies some fine points previously misunderstood in the literature.

Introduction

Resolution [START_REF] Robinson | A machine-oriented logic based on the resolution principle[END_REF] and superposition [START_REF] Bachmair | Rewrite-based equational theorem proving with selection and simplification[END_REF] provers are based on saturation. In a first approximation, these provers perform all possible inferences between the available clauses. The full truth, however, is more complex: Provers may delete clauses that are considered redundant; for example, with resolution, if p(x) is in the clause set, then both p(a) and p(x) ∨ q(x) are redundant and could be deleted.

The procedure that saturates a set of clauses-or more generally, formulasup to redundancy is called the given clause procedure [START_REF] Mccune | Otter-the CADE-13 competition incarnations[END_REF]Sect. 2.3]. It has several variants. The two main variants are the Otter loop [START_REF] Mccune | Otter-the CADE-13 competition incarnations[END_REF] and the DISCOUNT loop [START_REF] Avenhaus | DISCOUNT: A system for distributed equational deduction[END_REF]. In this paper, we also consider the iProver [START_REF] Duarte | Implementing superposition in iProver (system description)[END_REF] and Zipperposition loops [START_REF] Vukmirović | Making higher-order superposition work[END_REF]; they are variants of the Otter and DISCOUNT loops, respectively.

In its simplest form, the procedure distinguishes between passive and active formulas. Formulas start as passive. One passive formula is selected as the given clause. 1 Deletions and simplifications with respect to other passive and active formulas are then performed; for example, if the given clause is redundant with respect to an active formula, the given clause can be deleted, and if the given clause makes an active formula redundant, that formula can be deleted. Moreover, simplifications can take place; for example, in a superposition prover, if the term order specifies b ≻ a, the given clause is b ≈ a, and p(b) is an active formula, the active formula can be simplified to p(a) and made passive again.

Next, if the given clause has not been deleted, it is moved to the active set. All inferences between the given clause and formulas in the active set are then performed, and the resulting conclusions are put in the passive set. This procedure is repeated, starting with the selection of a new given clause, until the distinguished formula ⊥ is derived or the passive set is empty.

The main metatheorem about this procedure states that if the given clause is chosen fairly (i.e., no passive formula is ignored forever), then the active set will be saturated (up to redundancy) at the limit. As a corollary, if the proof calculus is refutationally complete (i.e., it derives ⊥ from any inconsistent set), then the prover based on the calculus will be refutationally complete as well.

We present an Isabelle/HOL [START_REF] Nipkow | Isabelle/HOL: A Proof Assistant for Higher-Order Logic[END_REF] formalization of the Otter, DISCOUNT, iProver, and Zipperposition loops, culminating in a statement and proof of the main metatheorem for each one. We build on the pen-and-paper saturation framework developed by Waldmann, Tourret, Robillard, and Blanchette [START_REF] Waldmann | A comprehensive framework for saturation theorem proving[END_REF][START_REF] Waldmann | A comprehensive framework for saturation theorem proving[END_REF] and formalized in Isabelle/HOL by Tourret and Blanchette [START_REF] Tourret | A modular isabelle framework for verifying saturation provers[END_REF]. The framework is an elaboration of Bachmair-Ganzinger-style saturation [START_REF] Bachmair | Resolution theorem proving[END_REF]Sect. 4]. Waldmann et al. include descriptions of the four "loops" as instances of the framework, as Examples 71, 74, 81, and 82 [START_REF] Waldmann | A comprehensive framework for saturation theorem proving[END_REF]; our formalization follows these descriptions.

Among the four loops, the oldest one is the Otter loop. It originates from Otter, a resolution-based theorem prover for first-order logic introduced in 1988 [START_REF] Mccune | OTTER 3.0 reference manual and guide[END_REF]. Otter was the first prover to present the given clause algorithm, in its simplest form as described above.

The DISCOUNT loop followed a few years later as a byproduct of the DIS-COUNT system [START_REF] Denzinger | Das DISCOUNT-System: Benutzerhandbuch[END_REF], itself built to distribute proof tasks among processors. What distinguishes a DISCOUNT loop is that it really treats the passive set as passive. Its formulas serve only as the pool from which to choose the next given clause; they are never involved in deletions or other simplifications. Another key difference between the two loops is the decoupling of the scheduling of an inference and the production of its conclusion, which makes DISCOUNT able to propagate deletions and simplifications to discard inferences before their conclusions enter the passive set. For example, suppose that, in DISCOUNT, an inference p(x) ∨ p(a) ¬ p(y) ∨ q(y) p(x) ∨ q(y) called ι is scheduled, in a derivation using first-order resolution. Then suppose that, before ι is realized, p(a) is generated (e.g., as the result of the factorization of p(x) ∨ p(a)). This triggers the deletion of p(x) ∨ p(a), which has become redundant. Then ι becomes an orphan inference, since one of its premises is no longer in the active set. It can be deleted without threatening the procedure's completeness. In contrast, in an Otter loop, if ι is scheduled before p(a) is selected as the given clause, ι's conclusion p(x) ∨ q(y) is directly added to the passive set, where it can be simplified.

What we call the iProver loop [START_REF] Duarte | Implementing superposition in iProver (system description)[END_REF] is an extension of the Otter loop with a transition that removes a formula C if C is made redundant by a formula set M . This terminology is from Waldmann et al. [START_REF] Waldmann | A comprehensive framework for saturation theorem proving[END_REF]Example 74]. This rule, introduced when iProver was extended to handle the superposition calculus [START_REF] Duarte | Implementing superposition in iProver (system description)[END_REF], combines an inference step with a step that simplifies the active set.

The last and most elaborate loop variant we present is the Zipperposition loop. Zipperposition is a higher-order theorem prover based on λ-superposition [START_REF] Bentkamp | Superposition for full higher-order logic[END_REF]. Its given clause procedure is designed to work with higher-order logic. Due to the explosiveness of higher-order unification, a single pair of premises can yield infinitely many conclusions. For example, the higher-order resolution inference

p (f (y a)) ∨ q y ¬ p (z (f a)) q (λx. f (. . . (f x) . . .))
where y and z are variables, produces infinitely many conclusions of the form q(λx.f n x) for n ∈ N. Thus, the passive set must be able to store possibly infinite sequences of lazily performed inferences. The Zipperposition loop was described by Vukmirović et al. [START_REF] Vukmirović | Making higher-order superposition work[END_REF] and by Waldmann et al. [START_REF] Waldmann | A comprehensive framework for saturation theorem proving[END_REF]Example 82]. 2 Vukmirović et al. describe the loop's implementation in Zipperposition, which we believe to be correct. In contrast, Waldmann et al. present an abstract version of the loop and connect it, via stepwise refinement, to their saturation framework, obtaining the main metatheorem. However, in the latter work, the details are not worked out. Thanks to the Isabelle formalization, we note and address several issues such that we now have a first rigorous-in fact, fully formal-presentation of the essence of the Zipperposition loop including the metatheorem.

Our work is part of IsaFoL (Isabelle Formalization of Logic), an effort that aims at developing a formal library of results about logic and automated reasoning [START_REF] Blanchette | Formalizing the metatheory of logical calculi and automatic provers in Isabelle/HOL (invited talk)[END_REF]. The Isabelle files amount to about 7000 lines of code. They were developed using the 2022 edition of Isabelle and are available in the Archive of Formal Proofs (AFP ) [START_REF] Blanchette | Given clause loops. Archive of Formal Proofs 2023[END_REF], where they are updated to follow Isabelle's evolution.

This work joins a long list of verifications of calculi and provers. We refer to Blanchette [START_REF] Blanchette | Formalizing the metatheory of logical calculi and automatic provers in Isabelle/HOL (invited talk)[END_REF]Sect. 5] for an overview of such works. The most closely related works are the two proofs of completeness of Bachmair and Ganzinger's resolution prover RP, by Schlichtkrull, Blanchette, Traytel, and Waldmann [START_REF] Schlichtkrull | Formalizing Bachmair and Ganzinger's ordered resolution prover[END_REF] and by Tourret and Blanchette [START_REF] Tourret | A modular isabelle framework for verifying saturation provers[END_REF] as well as the proof of completeness of ordered (unfailing) completion by Hirokawa, Middeldorp, Sternagel, and Winkler [START_REF] Hirokawa | Infinite runs in abstract completion[END_REF]. Instead of focusing on a single prover, here we consider general prover architectures. Via refinement, our results can be applied to individual provers.

Abstract Given Clause Procedures

To prove the main metatheorem for each of the four loops, we build on the saturation framework. The framework defines two highly abstract given clause procedures, called GC ("given clause") and LGC ("lazy given clause") [START_REF] Waldmann | A comprehensive framework for saturation theorem proving[END_REF]Sect. 4]. They are formalized in the file Given_Clause_Architectures.thy of the AFP entry Saturation_Framework [START_REF] Tourret | A comprehensive framework for saturation theorem proving[END_REF].

GC is an idealized Otter-style loop. It operates on sets of labeled formulas. Formulas have the generic type ′ f, and labels have the generic type ′ l. One label, active, identifies active formulas, and the other labels correspond to passive formulas. GC is defined as a two-rule transition system ⇝ GC . In Isabelle syntax:

inductive (⇝ GC ) :: ( ′ f × ′ l) set ⇒ ( ′ f × ′ l) set ⇒ bool where process: N 1 = N ∪ M = ■ ⇒ N 2 = N ∪ M ′ = ■ ⇒ M ⊆ Red F (N ∪ M ′ ) = ■ ⇒ active_subset M ′ = ∅ = ■ ⇒ N 1 ⇝ GC N 2 | infer : N 1 = N ∪ {(C, L)} = ■ ⇒ N 2 = N ∪ {(C, active)} ∪ M = ■ ⇒ L ̸ = active = ■ ⇒ active_subset M = ∅ = ■ ⇒ Inf_between (fst ' active_subset N ) {C} ⊆ Red I (fst ' (N ∪ {(C, active)} ∪ M )) = ■ ⇒ N 1 ⇝ GC N 2
When presenting Isabelle code, we will focus on the main ideas and not explain all the Isabelle syntax or all the symbols that occur in the code. We refer to Waldmann et al. [START_REF] Waldmann | A comprehensive framework for saturation theorem proving[END_REF] for mathematical statements of the key concepts and to the Isabelle theory files for the formal definitions.

Informally, the transition relation ⇝ GC is defined as an inductive predicate equipped with two introduction rules, process and infer. Both rules allow a transition from N 1 to N 2 under some conditions:

-The process rule replaces a subset M of N 1 by M ′ . This is possible only if the redundancy criterion (Red F ) justifies the replacement and the formulas in M ′ are all made passive (i.e., the active subset of M ′ is the empty set). This rule models formula simplification and deletion, but also replacing a passive label by another, "greater" passive label.

-The infer rule makes a passive formula C active and performs all inferences between this formula and active formulas, yielding M . Strictly speaking, the inferences need not be performed at all; it suffices that M makes the inferences redundant.

The main metatheorem for GC states that if the set of passive formulas is empty at the limit of a derivation, the active formula set is saturated at the limit. The lazy variant LGC generalizes the DISCOUNT loop. It operates on pairs (T, N ), where T :: ′ f inference set is a set of inferences that have been scheduled

but not yet performed and N :: ( ′ f× ′ l) set is a set of labeled formulas. It consists of four rules that can be summarized as follows:

-The process rule is essentially as in GC. It leaves the T component unchanged.

-The schedule_infer rule makes a passive formula active and schedules all the inferences between this formula and active formulas by adding them to the T component.

-The compute_infer rule actually performs a scheduled inference or otherwise ensures that it is made redundant by adding suitable formulas.

-The delete_orphan_infers rule can be used to delete a scheduled inference if one of its premises has been deleted.

The main metatheorem for LGC states that if the set of scheduled inferences and the set of passive formulas are empty at the limit of a derivation starting in an initial state, the active formula set is saturated at the limit.

Otter and iProver Loops

The Otter loop [START_REF] Mccune | Otter-the CADE-13 competition incarnations[END_REF] works on five-tuples (N, X, P, Y, A), where N is the set of new formulas; X is a subsingleton (i.e., the empty set or a singleton {C}) storing a formula moving from N to P ; P is the set of so-called passive formulas (although, strictly speaking, the formulas in N , X, and Y are also passive); Y is a subsingleton storing the given clause, which moves from P to A; and A is the set of active formulas. All the sets are finite in practice. Initial states have the form (N, ∅, ∅, ∅, ∅). Inferences are assumed to be finitary, meaning that the set of inferences with C and formulas from A as premises (formally written Inf_between A {C}) is finite if A is finite. Premiseless inferences are disallowed.

Otter Loop without Fairness. The first version of the Otter loop, formalized in Otter_Loop.thy, does not make any fairness assumption on the choice of the given clause. The guarantee it offers is correspondingly weak: If the sets N , X, P , and Y are empty at the limit of a derivation starting in an initial state, then A is saturated. But there is no guarantee that N , X, P , and Y are empty at the limit. Later in this section, we will show how to ensure this generically.

The transition system ⇝ OL for the Otter loop without fairness is as follows:

inductive (⇝ OL ) :: ( ′ f × OL_label) set ⇒ ( ′ f × OL_label) set ⇒ bool where choose_n: C / ∈ N = ■ ⇒ state (N ∪ {C}, ∅, P , ∅, A) ⇝ OL state (N , {C}, P , ∅, A) | delete_fwd : C ∈ Red F (P ∪ A) ∨ (∃C ′ ∈ P ∪ A. C ′ • ⪯ C) = ■ ⇒ state (N , {C}, P , ∅, A) ⇝ OL state (N , ∅, P , ∅, A) | simplify_fwd : C ∈ Red F (P ∪ A ∪ {C ′ }) = ■ ⇒ state (N , {C}, P , ∅, A) ⇝ OL state (N , {C ′ }, P , ∅, A) | delete_bwd_p: C ′ ∈ Red F {C} ∨ C • ⪯ C ′ = ■ ⇒ state (N , {C}, P ∪ {C ′ }, ∅, A) ⇝ OL state (N , {C}, P , ∅, A) | simplify_bwd_p: C ′ ∈ Red F C, C ′′ = ■ ⇒ state (N , {C}, P ∪ {C ′ }, ∅, A) ⇝ OL state (N ∪ {C ′′ }, {C}, P , ∅, A) | delete_bwd_a: C ′ ∈ Red F {C} ∨ C • ⪯ C ′ = ■ ⇒ state (N , {C}, P , ∅, A ∪ {C ′ }) ⇝ OL state (N , {C}, P , ∅, A) | simplify_bwd_a: C ′ ∈ Red F (C, C ′′ ) = ■ ⇒ state (N , {C}, P , ∅, A ∪ {C ′ }) ⇝ OL state (N ∪ {C ′′ }, {C}, P , ∅, A) | transfer : state (N , {C}, P , ∅, A) ⇝ OL state (N , ∅, P ∪ {C}, ∅, A) | choose_p: C / ∈ P = ■ ⇒ state (∅, ∅, P ∪ {C}, ∅, A) ⇝ OL state (∅, ∅, P , {C}, A) | infer : Inf_between A {C} ⊆ Red I (A ∪ {C} ∪ M ) = ■ ⇒ state (∅, ∅, P , {C}, A) ⇝ OL state (M , ∅, P , ∅, A ∪ {C})
The state function converts a five-tuple into a set of labeled formulas-an equivalent representation that is often more convenient formally. The labels are New (for N ), XX (for X), Passive (for P ), YY (for Y ), and Active (for A, corresponding to active in GC).

The first nine rules all refine GC's process rule, whereas the tenth rule, infer, refines GC's infer. More precisely: The first rule moves a formula from N to X. The second and third rules delete or simplify the formula in X. The fourth to seventh rules delete or simplify other formulas using the formula in X. The eight rule moves a formula from X to P . The ninth rule moves a formula from P to Y . And the tenth rule moves a formula from Y to A and performs all inferences with formulas in A or otherwise ensures that the inferences are made redundant.

Following Waldmann et al., the rules introducing new formulas-namely, the simplify rules and infer -allow adding arbitrary formulas to the state and are therefore not sound. Since the metatheorems are about completeness, there is no harm in allowing unsound steps, such as skolemization. If desired, soundness can be required simply by adding the assumption N |= N ′ for each step N ⇝ OL N ′ in a derivation.

Compared with most descriptions of the Otter loop in the literature, the above formalization (and Example 71 in Waldmann et al. [START_REF] Waldmann | A comprehensive framework for saturation theorem proving[END_REF] on which it is based) is abstract and nondeterministic, allowing arbitrary interleavings of deletions, simplifications, and inferences. By not commiting to a specific strategy, we keep our code widely applicable: Our abstract Otter loop can be used as the basis of refinement steps targetting a wide range of deterministic procedures implementing specific strategies. We will see the same approach used for all the loops. We note that Bachmair and Ganzinger made a similar choice for their ordered resolution prover RP [START_REF] Bachmair | Resolution theorem proving[END_REF]Sect. 4].

Otter Loop with Fairness. Below we introduce a fair version of the Otter loop, called ⇝ OLf and formalized in Fair_Otter_Loop_Def.thy. This new version is closer to an implementation.

inductive (⇝ OLf ) :: ( ′ p, ′ f) OLf _state ⇒ ( ′ p, ′ f) OLf _state ⇒ bool where choose_n: C / ∈ N = ■ ⇒ (N ∪ {C}, None, P , None, A) ⇝ OLf (N , Some C, P , None, A) | delete_fwd : C ∈ Red F (elems P ∪ A) ∨ (∃C ′ ∈ elems P ∪ A. C ′ • ⪯ C) = ■ ⇒ (N , Some C, P , None, A) ⇝ OLf (N , None, P , None, A) | simplify_fwd : C ′ ≺ S C = ■ ⇒ C ∈ Red F (elems P ∪ A ∪ {C ′ }) = ■ ⇒ (N , Some C, P , None, A) ⇝ OLf (N , Some C ′ , P , None, A) . . . | choose_p: P ̸ = empty = ■ ⇒ (∅, None, P , None, A) ⇝ OLf (∅, None, remove (select P ) P , Some (select P ), A) | infer : Inf_between A {C} ⊆ Red I (A ∪ {C} ∪ M ) = ■ ⇒ (∅, None, P , Some C, A) ⇝ OLf (M , None, P , None, A ∪ {C})
The definition of ⇝ OLf differs from that of ⇝ OL in two main respects:

-The set P is organized as some form of queue, with operations such as select, which chooses the queue's next element; remove, which removes all occurrences of an element from the queue; and elems, which returns the set of the queue's elements. The queue is assumed to be fair, meaning that if select is called infinitely often, every element in the queue will eventually be chosen and the limit of P will be empty.

-Simplification (e.g., in simplify_fwd ) is allowed only if the simplified formula C ′ is smaller than the original formula C according to some given wellfounded order ≺ S . In practice, simplifications are usually well founded, so this is not a severe restriction.

Also note that the state is now directly represented as a five-tuple (without the mediation of the state function), where the subsingletons are of type ′ f option, with values of the forms None and Some C.

Formula Queue. The queue that represents the passive formula set P is formalized in its own file, Prover_Queue.thy. The file defines an abstract type of queue and the operations on it (empty, select, add, remove, and elems). It also expresses the fairness assumption on the select function:

If a sequence of queue operations starting from an empty queue contains infinitely many removals of the selected element, then the queue is empty at the limit.

Moreover, the file contains an example implementation of the queue as a FIFO queue. This ensures that the abstract requirements on the queue, including fairness, are satisfiable.

iProver Loop with Fairness. To obtain an iProver loop from an Otter loop, only one extra rule is needed. The fair version of the iProver loop is formalized in Fair_iProver_Loop.thy as follows:

inductive (⇝ ILf ) :: ( ′ p, ′ f) OLf _state ⇒ ( ′ p, ′ f) OLf _state ⇒ bool where ol : St ⇝ OLf St ′ = ■ ⇒ St ⇝ ILf St ′ | red_by_children: C ∈ Red F (A ∪ M ) ∨ M = {C ′ } ∧ C ′ • ≺ C = ■ ⇒ (∅, None, P , Some C, A) ⇝ ILf (M , None, P , None, A)
The first rule, ol, executes any ⇝ OLf rule as an iProver loop rule. The second rule, red_by_children, replaces a formula C by a set of formulas M that make it redundant. As M , iProver would use a set of simplified formulas produced by inferences with C as a premise and formulas from A ∪ {C} as further premises. The rule is stated in a more general, unsound form.

We prove the main metatheorem first for the iProver loop. Then, since an Otter derivation is an iProver derivation (in which the second rule, red_by_ children, is not used), the result carries over directly to the Otter loop. The Isabelle statement, located in Fair_iProver_Loop.thy, is as follows:

theorem fair_IL_Liminf_saturated assumes full_chain (⇝ ILf ) Sts and is_initial_OLf_state (Sts ! 0) shows saturated (Liminf Sts)
Informally, this states that if Sts is a complete ⇝ ILf derivation starting in a state of the form (N, None, empty, None, ∅), then the limit is saturated. The limit (strictly speaking, limit inferior) is defined by

Liminf Xs = i<|Xs| j:i≤j∧j<|Xs| Xs ! j
where Xs ! j returns the element at index j of the finite or infinite sequence Xs.

In Isabelle, such sequences are represented by the type ′ a llist of "lazy lists." This metatheorem is proved within the scope of the passive set queue's fairness assumption. It is derived from the metatheorem about the transition system ⇝ IL without fairness, which is inherited from the abstract procedure GC.

Proof sketch. The main difficulty is to show that N , X, P , and Y are empty at the limit. Once this is shown, we can apply the main metatheorem for GC, which states that if there are no passive formulas at the limit, the active formula set is saturated.

Let St 0 ⇝ IL St 1 ⇝ IL • • • be a complete derivation, where St i = (N i , X i , P i , Y i , A i ). If the derivation is finite, it is easy to show that the final state, and hence the limit, must be of the form (∅, None, empty, None, A), as desired.

Otherwise, for an infinite derivation, we assume in turn that the limit of N , X, P , or Y is nonempty and show that this leads to a contradiction. We start with N . Let i be an index such that N i ∩ N i+1 ∩ • • • ̸ = ∅, which exists by the definition of limit. This means that N i , N i+1 , . . . are all nonempty. By invariance, we can show that Y i , Y i+1 , . . . are all empty. Thus, if we have a transition from St j to St j+1 for j ≥ i, it cannot be infer (via ol ) or red_by_children. It can be shown that for the remaining transition rules, we have St i ⊐ 1 St i+1 ⊐ 1 • • • , where ⊐ 1 is the converse of the lexicographic combination ⊏ 1 of three well-founded relations:

the multiset extension ≺ ≺ S of ≺ S on entire states-i.e., on unions N ∪ X ∪ P ∪ Y ∪ A; -as a tiebreaker, ≺ ≺ S on N components; -as a further tiebreaker, ≺ ≺ S on X components.

Since the lexicographic combination of well-founded relations is well founded, the chain St

i ⊐ 1 St i+1 ⊐ 1 • • • cannot be infinite, a contradiction.
Next, we consider the X component. If X is nonempty forever, the only possible transition rules are deletions and simplifications, and both make the entire state decrease with respect to ≺ ≺ S . Again, we get a contradiction.

Next, we consider the P component. The fairness assumption for the queue guarantees that P is empty at the limit, at the condition that the choose_p rule is executed infinitely often. Since P is assumed not to be empty at the limit, choose_p must be executed only finitely often. Let i be an index from which no choose_p step takes place. We then have St i ⊐ 2 St i+1 ⊐ 2 • • • , where ⊐ 2 is the converse of the lexicographic combination ⊏ 2 of two well-founded relations:

-≺ ≺ S on Y components; -as a tiebreaker, the relation ⊏ 1 on entire states.

Again, we get a contradiction.

Finally, for Y , the only two transitions possible, infer and red_by_children, are to a state where Y is empty afterward, contradicting the hypothesis that Y is nonempty forever.

⊓ ⊔

DISCOUNT Loop

The DISCOUNT loop [START_REF] Avenhaus | DISCOUNT: A system for distributed equational deduction[END_REF] works on four-tuples (T, P, Y, A), where T is the set of scheduled ("to do") inferences, P is the set of so-called passive formulas (although, strictly speaking, any formula in Y is also passive); Y is a subsingleton storing the given clause; and A is the set of active formulas. All the sets are finite. Initial states have the form (∅, P, ∅, ∅). Inferences are assumed to be finitary. We disallow premiseless inferences. Waldmann et al. [19, Example 81] allow them and let the T component of initial sets consist of all of them. However, in their "reasonable strategy," they implicitly assume that T is finite, in which case premiseless inferences can be immediately performed and replaced by the resulting formulas inserted in P .

DISCOUNT Loop without Fairness. The first version of the DISCOUNT loop, formalized in DISCOUNT_Loop.thy, does not make any fairness assumption on the choice of the inference to compute or the given clause. There is no guarantee that T , P , and Y are empty at the limit, but if they are, then A is saturated at the limit. Here is an extract of the definition, omitting the delete_bwd and simplify_fwd rules:

inductive (⇝ DL ) :: ′ f inference set × ( ′ f × DL_label ) set ⇒ ′ f inference set × ( ′ f × DL_label ) set ⇒ bool where compute_infer : ι ∈ Red I (A ∪ {C}) = ■ ⇒ state (T ∪ ι, P , ∅, A) ⇝ DL state (T , P , {C}, A) | choose_p: state (T , P ∪ {C}, ∅, A) ⇝ DL state (T , P , {C}, A) | delete_fwd : C ∈ Red F A ∨ (∃C ′ ∈ A. C ′ • ⪯ C) = ■ ⇒ state (T , P , {C}, A) ⇝ DL state (T , P , ∅, A) . . . | simplify_bwd : C ′ ∈ Red F {C, C ′′ } = ■ ⇒ state (T , P , C, A ∪ {C ′ }) ⇝ DL state (T , P ∪ {C ′′ }, {C}, A) | schedule_infer : T ′ = Inf_between A {C} = ■ ⇒ state (T , P , {C}, A) ⇝ DL state (T ∪ T ′ , P , ∅, A ∪ {C}) | delete_orphan_infers: T ′ ∩ Inf_from A = ∅ = ■ ⇒ state (T ∪ T ′ , P , Y , A) ⇝ DL state (T , P , Y , A)
The state function converts a four-tuple (T, P, Y, A) into a pair (T, N ), where N is a set of labeled formulas. The labels are Passive (for P ), YY (for Y ), and Active (for A, corresponding to active in LGC). The rules compute_infer, schedule_infer, and delete_orphan_infers refine the LGC rules of the same names; the other rules refine process.

DISCOUNT Loop with Fairness. In the fair version of the DISCOUNT loop, formalized in Fair_DISCOUNT_Loop.thy, the scheduled inferences and the passive formulas are organized as a single queue. A state is then a triple (P, Y, A), where P is the single queue that merges T and P from the above DISCOUNT loop, and Y and A are as above. Elements of P have the forms Passive_Inference ι and Passive_Formula C. The select function of P is assumed to be fair: If select is called infinitely often, every element in the queue will eventually be chosen and the limit of P will be empty.

The definition of the transition system is as follows:

inductive (⇝ DLf ) :: ( ′ p, ′ f) DLf _state ⇒ ( ′ p, ′ f) DLf _state ⇒ bool where compute_infer : P ̸ = empty = ■ ⇒ select P = Passive_Inference ι = ■ ⇒ ι ∈ Red I (A ∪ C) = ■ ⇒ (P , None, A) ⇝ DLf (remove (select P ) P , Some C, A) | choose_p: P ̸ = empty = ■ ⇒ select P = Passive_Formula C = ■ ⇒ (P , None, A) ⇝ DLf (remove (select P ) P , Some C, A) | delete_fwd : C ∈ Red F A ∨ (∃C ′ ∈ A. C ′ • ⪯ C) = ■ ⇒ (P , Some C, A) ⇝ DLf (P , None, A) . . . | simplify_bwd : C ′ / ∈ A = ■ ⇒ C ′′ ≺ S C ′ = ■ ⇒ C ′ ∈ Red F {C, C ′′ } =⇒ (P , Some C, A ∪ {C ′ }) ⇝ DLf (add (Passive_Formula C ′′ ) P , Some C, A) | schedule_infer : set ιs = Inf_between A {C} = ■ ⇒ (P , Some C, A) ⇝ DLf (fold (add • Passive_Inference) ιs P , None, A ∪ {C}) | delete_orphan_infers: ιs ̸ = [] = ■ ⇒ set ιs ⊆ passive_inferences_of P = ■ ⇒ set ιs ∩ Inf_from A = ∅ = ■ ⇒ (P , Y , A) ⇝ DLf (fold (remove • Passive_Inference) ιs P , Y , A)
We note the following:

-Inferences are added to P by schedule_infer. An inference can be deleted by delete_orphan_infers if one of the premises has been removed since the inference was scheduled.

-The next element from P is chosen by compute_infer or choose_p, depending on whether it is of the form Passive_Inference ι or Passive_Formula C.

-Formulas are added to P by simplify_bwd.

As with the Otter and iProver loops, the most important result is saturation at the limit: Proof sketch. The proof amounts to showing that the sets P and Y are empty at the limit. This is easy to show for finite derivations, so we focus on infinite ones. We proceed by contradiction. For P , the fairness assumption for the select function of the queue guarantees that P is empty at the limit, at the condition that the compute_infer and choose_p rules are collectively executed infinitely often. Since P is assumed not to be empty at the limit, these two rules must be executed only finitely often. Let i be an index from which no compute_infer or choose_p step takes place. We then have St i ⊐ St i+1 ⊐ • • • , where ⊐ is the converse of the lexicographic combination ⊏ of two well-founded relations:

-< on the cardinality of Y components (0 or 1); -as a tiebreaker, the multiset extension ≺ ≺ S of ≺ S on unions P ∪ Y ∪ A.

Since the lexicographic combination of well-founded relations is well founded, the chain

St i ⊐ St i+1 ⊐ • • • cannot be infinite, a contradiction.
Finally, we consider Y . If Y is nonempty forever, the only possible transitions make the entire state decrease with respect to ⊏. This yields a contradiction. ⊓ ⊔

Zipperposition Loop

The Zipperposition loop [START_REF] Vukmirović | Making higher-order superposition work[END_REF] as described by Waldmann et al. [START_REF] Waldmann | A comprehensive framework for saturation theorem proving[END_REF]Example 82] works on four-tuples (T, P, Y, A), where the components have the same roles as in the DISCOUNT loop: T is the scheduled set, P is the passive set, Y is the given clause, if any, and A is the active set. For technical reasons, we need to enrich the state with a ghost component D ("done"), of type ′ f inference set, resulting in a five-tuple (T, D, P, Y, A). All the sets are finite. The hallmark of the Zipperposition loop is that it can handle infinitary inferences. We assume that Inf_between A {C} is countable if A is finite. (This assumption is implicit in Waldmann et al.) To store the infinitely many conclusions of an inference, T contains possibly infinite sequences of inferences, instead of individual inferences. Premiseless inferences are also allowed. Initial states have the form (T, P, ∅, ∅, ∅), where T contains all the premiseless inferences of the underlying proof calculus and only those.

The implementation in Zipperposition by Vukmirović et al. [START_REF] Vukmirović | Making higher-order superposition work[END_REF] deviates from Waldmann et al. in one important respect: Instead of sequences of inferences, Zipperposition works with sequences of subsingletons of inferences. The special value ∅ is returned when no progress is made in computing an inference, to give control back to the given clause procedure. In the setting of Waldmann et al., this special value can be replaced by a tautology (e.g., ⊤ or ⊤ ≈ ⊤), which the given clause procedure can delete as redundant.

Zipperposition Loop without Fairness. The first version of the Zipperposition loop, formalized in Zipperposition_Loop.thy, does not make any fairness assumption on the choice of the inference to compute or the given clause. Here is an extract of the definition: We use a multiset for the T component. Waldmann et al. use a set, but this is not very realistic because an implementation cannot in general detect duplicate infinite sequences.

inductive (⇝ ZL ) :: ′ f inference set × ( ′ f × DL_label) set ⇒ ′ f inference set × ( ′ f × DL_label) set ⇒ bool
| delete_fwd : C ∈ Red F A ∨ (∃C ′ ∈ A. C ′ • ⪯ C) = ■ ⇒ zl_state (T ,
The D component addresses a subtle issue in Waldmann et al. If we did not subtract D in the definition of U , the completeness theorem we would obtain from the LGC layer above would require the T component to be empty at the limit. However, a given inference ι might appear in T multiple times and hence always be present, even if we keep on removing copies of it, if new copies are continuously added. The issue goes away if we add ι to D whenever we compute it, in compute_infer -then the inference is not present in U (i.e., inferences_of T -D). In other words, computing an inference makes it momentarily disappear, even if there are multiple copies of it in T .

Admittedly, it is not easy to develop a robust intuitive understanding of how D works, but what matters ultimately is that D allows us to obtain a usable main metatheorem. The metatheorem states that if the set of scheduled inferences and the set of passive formulas are empty at the limit of a derivation starting in an initial state, the active formula set is saturated at the limit. We will also see, via an additional refinement layer, that the ghost component is truly a ghost and can be omitted once it has served its purpose.

Zipperposition Loop with Fairness. Unlike the fair DISCOUNT loop, the fair Zipperposition loop, formalized in Fair_Zipperposition_Loop.thy, keeps T and P separate. An extract of the Isabelle definition follows: The presence of two queues introduces some complications. Waldmann et al. [START_REF] Waldmann | A comprehensive framework for saturation theorem proving[END_REF]Example 82] claim that "to produce fair derivations, a prover needs to choose the sequence in ComputeInfer fairly and to choose the formula in ChooseP fairly." However, this does not suffice: A counterexample would apply compute_infer infinitely often in a fair fashion, retrieving elements from some infinite sequences, without ever applying choose_p (whose choice of formula would then be vacuously fair). The solution is to add a fairness assumption stating that compute_infer is applied at most finitely many times before choose_p is applied-or, in other words, that if compute_infer is applied infinitely often, then so is choose_p. This leads to the following main metatheorem: Proof sketch. Recall that zl_state maps (T, D, P, Y, A) to a pair (U, N ). In the abstract LGC layer, U and the passive subset of N are required to be empty at the limit. To obtain the same effect in ⇝ ZLf , we must show that the sets U , P , and Y are empty at the limit. This is easy to show for finite derivations, so we focus on infinite ones. We proceed by contradiction.

inductive (⇝ ZLf ) :: ( ′ t, ′ p, ′ f) ZLf _state ⇒ ( ′ t, ′ p, ′ f) ZLf _state ⇒ bool where compute_infer : (∃ιs ∈ t_llists T. ιs ̸ = LNil) = ■ ⇒ t_pick_elem T = (ι 0 , T ′ ) = ■ ⇒ ι 0 ∈ Red I (A ∪ {C}) = ■ ⇒ (T , D, P , None, A) ⇝ ZLf (T ′ , D ∪ {ι 0 }, p_add C P , None, A) | choose_p: P ̸ = p_empty = ■ ⇒ (T , D, P , None, A) ⇝ ZLf (T , D, p_remove (p_select P ) P , Some (p_select P ), A) | delete_fwd : C ∈ Red F A ∨ (∃C ′ ∈ A. C ′ • ⪯ C) = ■ ⇒ (T , D, P , Some C, A) ⇝ ZLf (T , D, P , None, A) . . .
We start with U . We first show that there must be infinitely many compute_ infer steps. Assume that there are finitely many. Then there exists an index i from which no more compute_infer steps take place. We then have St i ⊐ St i+1 ⊐ • • • , where ⊐ is the converse of the lexicographic combination ⊏ of four wellfounded relations:

the multiset extension ≺ ≺ S of ≺ S on unions P ∪ Y ∪ A; -as a tiebreaker, ≺ ≺ S on P components; -as a further tiebreaker, ≺ ≺ S on Y components; -as a further tiebreaker, < on the cardinality of T components.

We get a contradiction. Having shown that there are infinitely many compute_ infer steps, we exploit the queue's fairness to show that one of these steps will choose any given inference ι from the queue. Thanks to the D trick, ι will then momentarily vanish from U , ensuring that it is not in the limit. The same argument applies for any inference ι, showing that U is empty at the limit.

Next, we show that P is empty at the limit. We start by showing that there must be infinitely many choose_p steps. Assume that there are finitely many. Then, by the third assumption, there must be finitely many compute_infer steps as well. Let i be an index from which no more compute_infer steps take place. We then have St i ⊐ St i+1 ⊐ • • • , as above, yielding a contradiction.

Finally, we show that Y is empty at the limit. Let i be an index such that Y i ∩ Y i+1 ∩ • • • ̸ = ∅. Since a compute_infer step is possible only if Y is empty, no such steps are possible from index i. Again, we have St i ⊐ St i+1 ⊐ • • • , a contradiction.

⊓ ⊔

Queue of Formula Sequences. The queue data structure used for the T component of the Zipperposition loop needs to store a finite number of possibly infinite sequences of inferences. It is formalized in Prover_Lazy_List_Queue .thy. It provides the following operations on abstract queue and element types ′ q and ′ e: fixes empty :: ′ q and add_llist :: ′ e llist ⇒ ′ q ⇒ ′ q and remove_llist :: ′ e llist ⇒ ′ q ⇒ ′ q and pick_elem :: ′ q ⇒ ′ e × ′ q and llists :: ′ q ⇒ ′ e llist multiset

The fairness requirement on implementations of the abstract queue interface takes the following form:

If a sequence of queue operations contains infinitely many pick_elem steps and ι is at the head of one of the sequences stored in the queue, then either the sequence will be entirely removed (by orphan deletion) or ι will eventually be chosen.

A syntactically stronger formulation of fairness, where ι may occur anywhere in a sequence, is derived as a corollary:

If a sequence of queue operations contains infinitely many pick_elem steps and ι occurs in one of the sequences stored in the queue at some index in the sequence, then either the sequence (possibly amputated from its leading elements) will be entirely removed or ι will eventually be chosen.

As a proof of concept, the theory file contains an example implementation of the queue as a FIFO queue. The proof that this FIFO queue is fair is the most finicky proof of our entire development.

Zipperposition Loop without Ghost Fields. In the last step of our development, we remove the D state component. D is useful to retrieve a usable main metatheorem for ⇝ ZL , but it is not explicitly referenced in the metatheorem for the fair variant ⇝ ZLf . The resulting transition system ⇝ ZLfw , formalized in Fair_Zipperposition_Loop_without_Ghosts.thy, operates on four-tuples (T, P, Y, A). Each transition is identical to the corresponding ⇝ ZLf transition, omitting the D component. The main metatheorem is also essentially the same.

Conclusion

We presented an Isabelle/HOL formalization of four variants of the given clause procedure, starting from Tourret and Blanchette's formalization of two abstract given clause procedures [START_REF] Tourret | A modular isabelle framework for verifying saturation provers[END_REF]. We relied extensively on stepwise refinement to derive properties of more concrete transition systems from more abstract ones.

Our main findings concern the Zipperposition loop. We found that the refinement proof is not as straightforward as previously thought [START_REF] Waldmann | A comprehensive framework for saturation theorem proving[END_REF]Example 82] and requires a nontrivial abstraction function. In addition, we discovered a fairness condition-the necessity of avoiding computing inferences forever without selecting a formula-that was not mentioned before in the literature, and we clarified other fine points.

  theorem fair_DL_Liminf_saturated assumes full_chain (⇝ DLf ) Sts and is_initial_DLf_state (Sts ! 0) shows saturated (labeled_formulas_of (Liminf_fstate Sts))

  where compute_infer : ι 0 ∈ Red I (A ∪ {C}) = ■ ⇒ zl_state (T + {LCons ι 0 ιs}, D, P , ∅, A) ⇝ ZL zl_state (T + {ιs}, D ∪ {ι 0 }, P ∪ {C}, ∅, A) | choose_p: zl_state (T , D, P ∪ {C}, ∅, A) ⇝ ZL zl_state (T , D, P , {C}, A)

  D, P , C, A) ⇝ ZL zl_state (T , D, P , ∅, A) . . .| schedule_infer : inferences_of T ′ = Inf_between A {C} = ■ ⇒ zl_state (T , D, P , C, A) ⇝ ZL zl_state (T + T ′ , D -inferences_of T ′ , P , ∅, A ∪ {C}) | delete_orphan_infers: set ιs ∩ Inf_from A = ∅ = ■ ⇒ zl_state (T +{ιs}, D, P , Y , A) ⇝ ZL zl_state (T , D ∪ set ιs, P , Y , A) The zl_state function converts a five-tuple (T, D, P, Y, A) into a pair (U, N ), where -U consists of all the inferences contained in T minus those in D (formally written inferences_of T -D); and -N is a set of labeled formulas corresponding to P , Y , and A.

|

  schedule_infer : inferences_of ιss = Inf_between A {C} = ■ ⇒ (T , D, P , Some C, A) ⇝ ZLf (fold t_add_llist ιss T , D -inferences_of ιss, P , None, A ∪ {C}) | delete_orphan_infers: ιs ∈ t_llists T = ■ ⇒ set ιs ∩ Inf_from A = ∅ = ■ ⇒ (T , D, P , Y , A) ⇝ ZLf (t_remove_llist ιs T , D ∪ set ιs, P , Y , A)

  theorem fair_ZL_Liminf_saturated : assumes full_chain (⇝ ZLf ) Sts and is_initial_ZLf_state (Sts ! 0) and infinitely_often compute_infer_step Sts -■ → infinitely_often choose_p_step Sts shows saturated (labeled_formulas_of (Liminf_zl_fstate Sts))

We keep the traditional name "given clause" even though our formulas are not necessarily clauses.

Both groups of researchers include Blanchette and Tourret.

Acknowledgments. We thank Andrei Popescu for helping us with a coinductive proof that arose when removing the ghosts in the Zipperposition loop. We thank Uwe Waldmann for sharing with us his encyclopedic knowledge of the various given clause loops and their history. Finally, we thank Mark Summerfield and the anonymous reviewers for many helpful suggestions.

This research has received funding from the Netherlands Organization for Scientific Research (NWO) under the Vidi program (project No. 016.Vidi.189.037, Lean Forward).


Martin Dvorak

Jasmin Blanchette

Closure Properties of General Grammars -Formally Verified

Keywords: 2012 ACM Subject Classification Theory of computation → Formal languages and automata theory Lean, type-0 grammars, recursively enumerable languages, Kleene star Digital Object Identifier 10.4230/LIPIcs.ITP.2023.11

We formalized general (i.e., type-0) grammars using the Lean 3 proof assistant. We defined basic notions of rewrite rules and of words derived by a grammar, and used grammars to show closure of the class of type-0 languages under four operations: union, reversal, concatenation, and the Kleene star. The literature mostly focuses on Turing machine arguments, which are possibly more difficult to formalize. For the Kleene star, we could not follow the literature and came up with our own grammar-based construction.

Introduction

The notion of formal languages lies at the heart of computer science. There are several formalisms that recognize formal languages, including Turing machines and formal grammars.

In particular, both Turing machines and general grammars (also called type-0 grammars or unrestricted grammars) characterize the same class of languages, namely, the recursively enumerable or type-0 languages. There has been work on formalizing Turing machines in proof assistants [START_REF] Chen | Introduction to Turing Machines[END_REF][START_REF] Asperti | Formalizing Turing Machines[END_REF][START_REF] Xu | Mechanising Turing Machines and Computability Theory in Isabelle/HOL[END_REF][START_REF] Carneiro | Formalizing Computability Theory via Partial Recursive Functions[END_REF][START_REF] Forster | Verified Programming of Turing Machines in Coq[END_REF][START_REF] Frank | The Cook-Levin theorem[END_REF]. General grammars are an interesting alternative because they are easier to define than Turing machines, and some proofs about general grammars are much easier than the proofs of similar properties of Turing machines.

We therefore chose general grammars as the basis for our Lean 3 [START_REF] De Moura | The Lean Theorem Prover (System Description)[END_REF] library of results about recursively enumerable or type-0 languages. The definition of grammars consists of several layers of concepts (Section 2):

the type of symbols is the disjoint union of terminals and nonterminals; rewrite rules are pairs of the form u → v, where u and v are strings over symbols and u contains at least one nonterminal [START_REF] Aho | The Theory of Parsing, Translation, and Compiling[END_REF];

11:2

Closure Properties of General Grammars -Formally Verified a grammar is a tuple consisting of a type of terminals, a type of nonterminals, an initial symbol S, and a set of rewrite rules; application of a rewrite rule u → v to a string αuβ is written αuβ ⇒ αvβ; the derivation relation ⇒ * is the reflexive transitive closure of the ⇒ relation; a grammar derives a word w if S ⇒ * w; the language generated by a grammar is the set of words derived by it; a language is type 0 if there exists a grammar that generates it.

We formalized four closure properties of type-0 languages.

The first such property we present is closure of type-0 languages under union (Section 3). We followed the standard construction for context-free grammars, which incidentally works for general grammars as well.

The second closure property we formalized is closure under reversal (Section 4). This was straightforward.

The third closure property we formalized is closure under concatenation (Section 5). The main difficulty was to avoid matching strings on the boundary of the concatenation. This issue does not arise with context-free grammars because only single symbols are matched and these are tidily located on either side of the boundary.

The fourth and last closure property we formalized is closure under the Kleene star (Section 6). This was the most difficult part of our work. Because the literature mostly focuses on Turing machine arguments, we needed to invent our own construction. We first developed a detailed proof sketch and then formalized it. The sketch is included in this paper.

One closure property we did not formalize is closure under intersection. The reason is that we are not aware of any elegant construction based on grammars only. Recall that type-0 languages are not closed under complement, as witnessed by the halting problem [START_REF] Hopcroft | Introduction to Automata Theory, Languages, and Computation[END_REF].

Our development is freely available online. 1 It consists of about 12 500 lines of spaciously formatted Lean code. It uses the Lean 3 mathematical library mathlib [START_REF]The Lean Mathematical Library[END_REF]. 2 We also benefited from the metaprogramming framework [START_REF] Ebner | A Metaprogramming Framework for Formal Verification[END_REF], which allowed us to easily develop small-scale automation that helped make some proofs less verbose.

Although Lean is based on dependent type theory [START_REF] Luo | An Extended Calculus of Constructions[END_REF], our code uses only nondependent types for data. We still found dependent type theory useful for bound-checked indexing of lists using the function list.nth_le (which takes a list, an index, and a proof that the index is within bounds as arguments). We did not attempt to make our development constructive.

Definitions

Grammars

As outlined in the introduction, the definition of grammars consists of several layers of declarations. Symbols are essentially defined as a sum type of terminals T and nonterminals N. However, we want to refer to terminals and nonterminals by name (using symbol.terminal and symbol.nonterminal instead of sum.inl and sum.inr), so we define symbols as an inductive type:

inductive symbol ( T : Type ) ( N : Type ) | terminal : T → symbol | nonterminal : N → symbol
We do not require T and N to be finite. As a result, we do not need to copy the typeclass instances [fintype T] and [fintype N] alongside our type parameters (which would appear in almost every lemma statement). Instead, later we work in terms of a list of rewrite rules, which is finite by definition and from which we could infer that only a finite set of terminals and a finite set of nonterminals can occur.

The left-hand side u of a rewrite rule u → v consists of three parts (an arbitrary string α, a nonterminal A, and another arbitrary string β, such that u = αAβ):

structure grule ( T : Type ) ( N : Type ) := ( input_L : list ( symbol T N )) ( input_N : N ) ( input_R : list ( symbol T N )) ( output_string : list ( symbol T N ))

An advantage of this representation is that we do not need to carry the proposition "the left-hand side contains a nonterminal" around. A disadvantage is that we subsequently need to concatenate more terms.

A definition of a general grammar follows. Notice that only the type argument T is part of its type: structure grammar ( T : Type ) := ( nt : Type ) ( initial : nt ) ( rules : list ( grule T nt ))

Later we can use the dot notation to access individual fields. For example, if g is a term of the type grammar T, we can write g.nt to access the type of its nonterminals. By writing (g.rules.nth_le 0 _).output_string we obtain the right-hand side of the first rewrite rule in g. The underscore, when not inferred automatically, must be replaced by a term of the type 0 < g.rules.length, which is a proof that the list g.rules is not empty.

The next line adds an implicit type argument T to all declarations that come after:

variables { T : Type }
The following definition captures the application ⇒ of a rewrite rule:

def grammar_transforms ( g : grammar T ) ( w1 w2 : list ( symbol T g . nt )) :

Prop := ∃ r : grule T g . nt , r ∈ g . rules ∧ ∃ u v : list ( symbol T g . nt ) , w1 = u ++ r . input_L ++ [ symbol . nonterminal r . input_N ] ++ r . input_R ++ v ∧ w2 = u ++ r . output_string ++ v
The operator ++ concatenates two lists. We can view grammar_transforms as a function that takes a grammar g over the terminal type T and outputs a binary relation over strings of the type that g works internally with. I T P 2 0 2 3 11:4

Closure Properties of General Grammars -Formally Verified

The part r.input_L ++ [symbol.nonterminal r.input_N] ++ r.input_R represents the left-hand side of the rewrite rule r. Note that the terms r.input_L and r.input_N cannot be concatenated directly, since they have different types. The term r.input_N must first be wrapped in symbol.nonterminal to go from the type g.nt to the type symbol T g.nt and then surrounded by [ ] to become a (singleton) list.

The derivation relation ⇒ * is defined from grammar_transforms using the reflexive transitive closure: def grammar_derives ( g : grammar T ) : list ( symbol T g . nt ) → list ( symbol T g . nt ) → Prop := relation . refl_trans_gen ( grammar_transforms g )

Consequently, proofs about derivations will use structural induction.

The predicate "to be a word generated by the grammar g" is defined as the special case of the relation grammar_derives g where the left-hand side is fixed to be the singleton list made of the initial symbol of g and the right-hand side is required to consist of terminal symbols only:

def grammar_generates ( g : grammar T ) ( w : list T ) : Prop := grammar_derives g [ symbol . nonterminal g . initial ]

( list . map symbol . terminal w )

Languages

In our entire project, we work with the following definition of languages provided by mathlib in the computability package:

def language (α : Type *) := set ( list α)

The type argument α is instantiated by our terminal type T in all places where we work with languages. We do not mind restricting T to be Type since we are not interested in languages over types from Type 1 and higher universes.

The language of the grammar g is defined as the set of all w that satisfy the predicate grammar_generates g w declared above: def grammar_language ( g : grammar T ) : language T := set_of ( grammar_generates g ) Note that the type parameter T is preserved, but g.nt does not matter in the description of what words are generated. It corresponds to our intuition that the type of terminals is a part of the interface, but the type of nonterminals is an implementation matter. This is the first time that our custom types meet the standard mathlib type language, which is already connected to many useful types, such as the type of regular expressions.

Finally, we define the class of type-0 languages: def is_T0 ( L : language T ) : Prop := ∃ g : grammar T , grammar_language g = L

All top-level theorems about type-0 languages are expressed in terms of the is_T0 predicate. Note that the type system distinguishes between a list of terminals and a list of symbols that happen to be terminals. Languages are defined as sets of the former, whereas derivations in the grammar work with the latter.

In a similar way, we define CF_grammar, CF_transforms, CF_derives, CF_generates, CF_language, and the is_CF predicate for the formal definition of context-free languages.

The theorem CF_subclass_T0 connects the context-free languages to the type-0 languages. Type-0 languages remain the main focus of our work.

Operations

The operations under which we prove closure are defined below.

Union is defined in mathlib as follows:

protected def set . union ( s1 s2 : set α) : set α := { a | a ∈ s1 ∨ a ∈ s2 }
The following declaration in mathlib states that the union of languages is denoted by writing the + operator between two terms of the language type: instance : language . has_add ( language α) := ⟨set . union⟩

We define the reversal of a language as follows:

def reverse_lang ( L : language T ) : language T := λ w : list T , w . reverse ∈ L

We do not declare any syntactic sugar for reversal. Concatenation is defined using the following general mathlib definition:

def set . image2 ( f : α → β → γ ) ( s : set α) ( t : set β ) : set γ := { c | ∃ a b , a ∈ s ∧ b ∈ t ∧ f a b = c }
The next mathlib declaration states that concatenation of languages is denoted by writing the * operator between two terms of the language type: instance : language . has_mul ( language α) := ⟨set . image2 (++)⟩

The Kleene star of a language is defined in mathlib as follows:

def language . star ( l : language α) : language α := { x | ∃ S : list ( list α) , x = S . join ∧ ∀ y ∈ S , y ∈ l }

We do not declare any syntactic sugar for the Kleene star.

Closure under Union

In this section, we prove the following theorem:

theorem T0_of_T0_u_T0 ( L1 : language T ) ( L2 : language T ) :

is_T0 L1 ∧ is_T0 L2 → is_T0 ( L1 + L2 )
The proof of closure of type-0 languages under union consists of three main ingredients: (1) a construction of a new grammar g from any two given grammars g 1 and g 2 ;

(2) a proof that any word generated by g 1 or g 2 can also be generated by g;

(3) a proof that any word generated by g can be equally generated by g 1 or g 2 . Proofs of the other closure properties are organized analogously. We describe the proof of closure under union in more detail; it allows us to outline the main ideas of proving closure properties formally in a simple setting. Since (3) is usually much more difficult than (2), we refer to (2) as the "easy direction" and to (3) as the "hard direction". I T P 2 0 2 3 11:6

Closure Properties of General Grammars -Formally Verified

The proof of the closure of type-0 languages under union follows the standard construction, which usually states only (1) explicitly, and leaves ( 2) and (3) to the reader. We begin (1) by defining a new type of nonterminals. The nonterminals of g consist of the nonterminals of g 1 including a mark indicating their origin; the nonterminals of g 2 including a mark indicating their origin; one new distinguished nonterminal. The Lean type option (g 1 .nt ⊕ g 2 .nt) encodes this disjoint union. If m is a nonterminal of type g 1 .nt, its corresponding nonterminal of type g.nt is some (sum.inl m). If n is a nonterminal of type g 2 .nt, its corresponding nonterminal of type g.nt is some (sum.inr n). The new distinguished nonterminal is called none and becomes the initial symbol of g. The rewrite rules of g consist of the rewrite rules of g 1 with all nonterminals mapped to the larger nonterminal type; the rewrite rules of g 2 with all nonterminals mapped to the larger nonterminal type; two additional rules that rewrite the initial symbol of g to the initial symbol of g 1 or g 2 .

To reduce the amount of repeated code in the proof, we developed lemmas that allow us to "lift" a grammar with a certain type of nonterminals to a grammar with a larger type of nonterminals while preserving what the grammar derives. Under certain conditions, we can also "sink" the larger grammar to the original grammar and preserve its derivations.

These lemmas operate on a structure called lifted_grammar that consists of the following fields:

a smaller grammar g 0 that represents either g 1 or g 2 in case of the proof for union; a larger grammar g with the same type of terminals; a function lift_nt from g 0 .nt to g.nt; a partial function sink_nt from g.nt to g 0 .nt; a proposition lift_inj that guarantees that lift_nt is injective; a proposition sink_inj that guarantees that sink_nt is injective on inputs for which g 0 has a corresponding nonterminal; a proposition lift_nt_sink that guarantees that sink_nt is essentially an inverse of lift_nt; a proposition corresponding_rules that guarantees that g has a rewrite rule for each rewrite rule g 0 has (with different type but the same behavior); a proposition preimage_of_rules that guarantees that g 0 has a rewrite rule for each rewrite rule of g whose nonterminal has a preimage on the g 0 side.

Thanks to this structure, we can abstract from the specifics of how the larger grammar is constructed in concrete proofs and care only about the properties that are required to follow analogous derivations.

To illustrate how we work with this abstraction, we review the proof of the following lemma:

private lemma lift_tran { lg : lifted_grammar T } { w1 w2 : list ( symbol T lg . g0 . nt )} ( hyp : grammar_transforms lg . g0 w1 w2 ) : grammar_transforms lg . g ( lift_string lg . lift_nt w1 ) ( lift_string lg . lift_nt w2 )

We need to show that if g 0 has a rewrite rule that transforms w 1 to w 2 , then g has a rewrite rule that transforms lift_string lg.lift_nt w 1 to lift_string lg.lift_nt w 2 .

We start by deconstructing hyp according to the grammar_transforms definition. To go from g 0 to g, we first "lift" the rewrite rule (i.e., translate its nonterminals in all fields) that g 0 used. We call corresponding_rules to show that g has such a rule. Then we use the function lift_string to lift u and v, which are the parts of the string w 1 that were not matched by the rule. We are then left with the proof obligation These two obligations originate from the two identities in the definition grammar_transforms from Section 2. Essentially, we discharge them using the distributivity of lift_string over the ++ operation. The abstraction provided by lifted_grammar takes care of the vast majority of our proof of the closure of type-0 languages under union. It remains to separately analyze what was the first step of the derivation that g did in the hard direction. We need to exclude all rules that are inherited from g 1 and g 2 and perform a case analysis on the two special rules.

The two additional rules of g are context-free. Therefore, if g 1 and g 2 have context-free rules only, then all rules of g are context-free as well. As a consequence, our result about type-0 languages can easily be reused to prove the closure of context-free languages under union:

theorem CF_of_CF_u_CF ( L1 : language T ) ( L2 : language T ) : is_CF L1 ∧ is_CF L2 → is_CF ( L1 + L2 )

Not much Lean code needs to be duplicated to obtain the result about context-free grammars. We need to write the construction of g again and the main result again. The remaining parts are achieved by reusing lemmas from the proof for general grammars. The main overhead is proving private lemma u n i o n _ g r a m m a r _ e q _ u n i o n _ C F _ g r a m m a r { g1 g2 : CF_grammar T } : union_grammar ( grammar_of_cfg g1 ) ( grammar_of_cfg g2 ) = grammar_of_cfg ( union_CF_grammar g1 g2 )

Even though the statement might look complicated, the proof has only five lines, making it one of the shortest tactic-based proofs in our project.

Closure under Reversal

In this section, we prove the following theorem:

theorem T0_of_reverse_T0 ( L : language T ) : is_T0 L → is_T0 ( reverse_lang L )

The proof is very easy. Simply speaking, everything gets reversed. We start with the rewrite rules:

private def reversal_grule { N : Type } ( r : grule T N ) : grule T N := grule . mk r . input_R . reverse r . input_N r . input_L . reverse r . output_string . reverse

The constructor grule.mk takes arguments in the same order as they are written in the definition: its input_L is instantiated by r.input_R.reverse; its input_N is instantiated by r.input_N; its input_R is instantiated by r.input_L.reverse; its output_string is instantiated by r.output_string.reverse.

The new grammar is constructed as follows:

private def reversal_grammar ( g : grammar T ) : grammar T := grammar . mk g . nt g . initial ( list . map reversal_grule g . rules )

The rest is essentially a repeated application of lemma list.reverse_append_append, which is just a repeated application of lemma list.reverse_append, which states that reversing two concatenated lists is equivalent to reversing both parts and concatenating them in the opposite order, and lemma list.reverse_reverse, which states that list.reverse is a dual operation.

5

Closure under Concatenation

In this section, we prove the following theorem:

theorem T0_of_T0_c_T0 ( L1 : language T ) ( L2 : language T ) :

is_T0 L1 ∧ is_T0 L2 → is_T0 ( L1 * L2 )
Because the proof is highly technical, we only outline the main idea here. We first review the classical construction for context-free grammars. Let L 1 ⊆ T * be a language generated by a grammar G 1 = (N 1 , T, P 1 , S 1 ). Let L 2 ⊆ T * be a language generated by a grammar G 2 = (N 2 , T, P 2 , S 2 ). Without loss of generality, the sets N 1 and N 2 are disjoint. We create a new initial symbol S that appears only in the rule S → S 1 S 2 . The new grammar is (N 1 ∪ N 2 ∪ {S}, T, P 1 ∪ P 2 ∪ {S → S 1 S 2 }, S ). This construction works for context-free grammars because S 1 gives rise to a word from L 1 and, independently, S 2 gives rise to a word from L 2 .

For general grammars, the construction above does not work, as the following counterexample over T = {a, b} illustrates. Let the rule sets be P 1 = {S 1 → S 1 a, S 1 → ϵ} and

P 2 = {S 2 → S 2 a, S 2 → ϵ, aS 2 → b}. We obtain L 1 = L 2 = {a n | n ∈ N 0 } and so L 1 L 2 is {a n | n ∈ N 0 } as well. We can now derive S ⇒ S 1 S 2 ⇒ S 1 aS 2 ⇒ S 1 b ⇒ b / ∈ L 1 L 2 and obtain a contradiction.
We need to avoid matching strings that span across the boundary of the concatenation. Since the nonterminal sets are disjoint, the issue arises only with terminals in the left-hand side of rules, which are not present in context-free grammars. We provide a solution below.

Let g 1 and g 2 generate L 1 and L 2 respectively. The nonterminals of our new grammar g consist of the nonterminals of g 1 including a mark indicating their origin; the nonterminals of g 2 including a mark indicating their origin; a proxy nonterminal for every terminal from T marked for use by g 1 only; a proxy nonterminal for every terminal from T marked for use by g 2 only; one new distinguished nonterminal. The new nonterminal type is encoded by the Lean type option (g 1 .nt ⊕ g 2 .nt) ⊕ (T ⊕ T). The new distinguished nonterminal becomes the initial symbol of g.

In this we ensure that the nonterminals used by g to simulate g 1 are disjoint from the nonterminals used by g to simulate g 2 . There are still real terminals used by both grammars, but g never has these terminals on the left-hand side of a rule, since the rewrite rules of g consist of the rewrite rules of g 1 with all nonterminals mapped to the new nonterminal type and all terminals replaced by proxy nonterminals of the first kind; the rewrite rules of g 2 with all nonterminals mapped to the new nonterminal type and all terminals replaced by proxy nonterminals of the second kind; for every terminal from T, a rule that rewrites the proxy nonterminal of the first kind to the corresponding terminal and a rule that rewrites the proxy nonterminal of the second kind to the corresponding terminal; a special rule that rewrites g.initial to a two-symbol string [g 1 .initial, g 2 .initial] wrapped to use the new nonterminal type. Using this construction, we ensure that all rules of g avoid matching strings on the boundary of the concatenation.

Proving that g generates a superset of L 1 * L 2 is easy because we can apply the rewrite rules in the following order, regardless of the languages:

(1) use the special rule to obtain [g 1 .initial, g 2 .initial] with the necessary wrapping;

(2) generate the string of proxy nonterminals corresponding to the word from L 1 while g 2 .initial remains unchanged; (3) replace all proxy nonterminals of the first kind by the corresponding terminals, which results in deriving a word from L 1 followed by g 2 .initial as the last symbol; (4) generate the string of proxy nonterminals corresponding to the word from L 2 while the first part of the string remains unchanged; (5) replace all proxy nonterminals of the second kind by the corresponding terminals, which results in deriving a word from L 2 that follows the word from L 1 obtained before.

Step (1) is trivial. Steps (2) and ( 4) are done by following the derivations by g 1 and g 2 , respectively. Steps (3) and ( 5) are straightforward proofs by induction.

Proving that g generates a subset of L 1 * L 2 is much harder because we do not know in which order the rules of g are applied. We had to come up with an invariant that relates intermediate strings derived by g to strings that can be derived by g 1 and g 2 from their respective initial symbols.

Very roughly speaking, we prove that there are strings x and y for every string w that g can derive, such that the grammar g 1 can derive x, the grammar g 2 can derive y, and x ++ y corresponds to w. As usual, we employ structural induction. Looking at the last rule g used, I T P 2 0 2 3 11:10 Closure Properties of General Grammars -Formally Verified we update x or y or neither. In particular, we want to point out the following declarations in the formalization:

function nst provides the new symbol type which g operates with; functions wrap_symbol 1 and wrap_symbol 2 convert symbols for use by g; relation corresponding_strings built on top of relation corresponding_symbols is used to define how the strings x and y are precisely related to w after each step by g; lemma induction_step_for_lifted_rule_from_g 1 characterizes the x update; lemma induction_step_for_lifted_rule_from_g 2 characterizes the y update; lemma big_induction states the invariant for proving the hard direction; lemma in_concatenated_of_in_big puts the proof of the hard direction together.

Note that the added rules have only one symbol on the left-hand side. Therefore, if the two original grammars are context-free, our constructed grammar is also context-free. We thereby obtain, as a bonus, a proof that context-free languages are closed under concatenation. It is implemented in a similar fashion to the proof that context-free languages are closed under union.

6

Closure under Kleene Star

In this section, we prove the following theorem:

theorem T0_of_star_T0 ( L : language T ) : is_T0 L → is_T0 L . star This is usually demonstrated by a hand-waving argument about a two-tape nondeterministic Turing machine. The language to be iterated is given by a single-tape (nondeterministic) Turing machine. The new machine scans the input on the first tape, copying it onto the second tape as it progresses, and nondeterministically chooses where the first word ends. Next, the original machine is simulated on the second tape. If the simulated machine accepts the word on the second tape, the process is repeated with the current position of the first head instead of returning to the beginning of the input. Finally, when the first head reaches the end of the input, the second tape contains a suffix of the first tape. The original machine is simulated once more on the second tape. If it accepts, the new machine accepts.

Unfortunately, we did not find any proof based on grammars in the literature. Therefore, we had to invent our own construction. In Section 6.1, we present the construction and the idea underlying its correctness using traditional mathematical notation. In Section 6.2, we comment on its formalization.

Proof Sketch

Let L ⊆ T * be a language generated by the grammar G = (N, T, P, S). We construct a grammar G * = (N * , T, P * , Z) to generate the language L * . The new nonterminal set

N * = N ∪ {Z, #, R}
expands N with three additional nonterminals: a new starting symbol (Z), a delimiter (#), and a marker for final rewriting (R). The new set of rules is

P * = P ∪ {Z → ZS#, Z → R#, R# → R, R# → ϵ} ∪ {Rt → tR | t ∈ T }
Intuitively, # builds compartments that isolate the words from the language L, and then R acts as a cleaner that traverses the string from beginning to end and removes the compartment delimiters #, thereby ensuring that only terminals are present to the left of R.

To see how G * works, consider the following grammar over T = {a, b}. Let N = {S} and P = {S → aSb, S → ϵ}. The set of rules becomes

P * = {S → aSb, S → ϵ, Z → ZS#, Z → R#, R# → R, R# → ϵ, Ra → aR, Rb → bR}
The following is an example of G * derivation: In the example above, case 1 arises when α = ZaaSbb#S#. We can check that m = 2, x 1 = aaSbb, x 2 = S, and condition 1 holds.

Z ⇒ ZS# ⇒ ZS#S# ⇒ ZaSb#S# ⇒ ZaaSbb#S# ⇒ ZS#aaSbb#S# ⇒ ZaSb#aaSbb#S# ⇒ ZaSb#aaaSbbb#S# ⇒ ZaSb#aaabbb#S# ⇒ R#aSb#aaabbb#S# ⇒ RaSb#aaabbb#S# ⇒ aRSb#aaabbb#S# ⇒ aRb#aaabbb#S# ⇒ abR#aaabbb#S# ⇒ abRaaabbb#S# ⇒ abaRaabbb#S# ⇒ abaaRabbb#S# ⇒ abaaaRbbb#S# ⇒ abaaabRbb#S# ⇒ abaaabRbb#aSb# ⇒ abaaabbRb#aSb# ⇒ abaaabbRb#ab# ⇒ abaaabbbR#ab# ⇒ abaaabbbRab# ⇒ abaaabbbaRb# ⇒ abaaabbbabR# ⇒ abaaabbbab ▶ Lemma 1. Let w 1 ,
∈ (T ∪ N ) * (∀i ∈ [m] (S ⇒ * x i ) ∧ α = Zx 1 #x 2 # . . . x m #); 2. ∃x 1 , x 2 , . . . , x m ∈ (T ∪ N ) * (∀i ∈ [m] (S ⇒ * x i ) ∧ α = R#x 1 #x 2 # . . . x m #); 3
In the example above, case 2 arises when α = R#aSb#aaabbb#S#. We can check that m = 3, x 1 = aSb, x 2 = aaabbb, x 3 = S, and condition 2 holds.

In the example above, case 3 arises when α = abaaabRbb#aSb#. We can check that n = 1, m = 1, w 1 = ab, β = aaab, γ = bb, x 1 = aSb, and condition 3 holds.

Case 4 arises only at the end of a successful computation, which is α = abaaabbbab in the example above.

The remaining two cases do not arise in the example above because they describe an unsuccessful computation (like taking a one-way street ending in a blind alley).

Case 5 arises if the rule R# → R is used in the final position (where R# → ϵ should be used instead). The nonterminal R in the final position prevents the derivation from terminating.

Case 6 arises if the rule R# → ϵ is used too early (that is, anywhere but the final # position). The nonterminal # in the final position during the absence of R and Z in α prevents the derivation from terminating.

Conclusion

We defined general grammars in Lean and used them to establish closure properties of recursively enumerable or type-0 languages. We found that closure under union and reversal were straightforward to formally prove, but had to invest considerable effort to prove closure under concatenation and the Kleene star. Despite the tedium of some of the proofs, we believe that grammars are probably a more convenient formalism than Turing machines for showing closure properties. On the other hand, since grammars do not define any of the important complexity classes (such as P), formalization of Turing machines and other computational models is needed to further develop the formal theory of computer science.

As future work, results about context-sensitive, context-free, and regular grammars could be incorporated into our library. A comprehensive Lean library encompassing the entire Chomsky hierarchy would be valuable. We already have some results about context-free grammars, and the mathlib results about regular languages could be connected to our library. As a more ambitious goal, we might attempt to prove the equivalence between general grammars and Turing machines.

. ∃w 1

 1 , w 2 , . . . , w n ∈ L (∃β ∈ T * (∃γ,x 1 , x 2 , . . . , x m ∈ (T ∪ N ) * (S ⇒ * βγ ∧ ∀i ∈ [m] (S ⇒ * x i ) ∧ α = w 1 w 2 . . . w n βRγ#x 1 #x 2 # . . . x m #))); 4. α ∈ L * ; 5. ∃σ ∈ (T ∪ N ) * (α = σR); 6. ∃ω ∈ (T ∪ N ∪ {#}) * (α = ω#).

  w 2 , . . , w n ∈ L. Then G * can derive Zw 1 #w 2 # . . . w n #. Proof. By induction on n. The base case Z ⇒ * Z is trivial. Now assume Z ⇒ * Zw 1 #w 2 # . . . w n # and S ⇒ * w n+1 . We start with the rule Z→ ZS#. We observe ZS# ⇒ * Zw 1 #w 2 # . . . w n #S# ⇒ * Zw 1 #w 2 # . . . w n #w n+1 #.By transitivity, we obtain Z ⇒ * Zw 1 #w 2 # . . . w n #w n+1 #.

◀ From now on, let [m] denote the set of m natural numbers {1, 2, . . . , m}. ▶ Lemma 2. If α ∈ (T ∪ N ) * can be derived by G * , then one of these conditions holds: 1. ∃x 1 , x 2 , . . . , x m

https://github.com/madvorak/grammars/tree/publish

https://github.com/leanprover-community/mathlib/tree/7ed4f2cec2

Funding Jasmin Blanchette: This research has received funding from the Netherlands Organization for Scientific Research (NWO) under the Vidi program (project No. 016.Vidi.189.037, Lean Forward). collaboration possible. We thank Václav Končický for discussing ideas about the Kleene star construction. We thank Patrick Johnson,

//github.com/madvorak/grammars/tree/publish

Proof. By induction on G * derivation steps. The base case α = Z satisfies condition 1 by setting m = 0. Now assume Z ⇒ * α ⇒ α ′ and proceed by case analysis on the conditions. 1. ∃x 1 , x 2 , . . . , x m ∈ (T ∪ N ) * (∀i ∈ [m] (S ⇒ * x i ) ∧ α = Zx 1 #x 2 # . . . x m #):

If α ⇒ α ′ used a rule from P , it could be applied only in some x i . Hence S ⇒ * x i ⇒ x ′ , so the same condition holds after replacing x i by x ′ i . If α ⇒ α ′ used the rule Z → ZS#, it was applied at the beginning of α. Therefore, we set m ′ := m + 1, we set x ′ 1 := S, and we increase all indices by one, that is, x ′ 2 := x 1 , x ′ 3 := x 2 , . . . , x ′ m ′ := x m . The same condition holds. If α ⇒ α ′ used the rule Z → R#, we keep all variables the same and condition 2 holds. The rules R# → R, R# → ϵ, and Rt → tR are not applicable (since α does not contain R).

If α ⇒ α ′ used a rule from P , it could be applied only in some x i . Hence S ⇒ * x i ⇒ x ′ i , so the same condition holds after replacing x i by x ′ i . The rules Z → ZS# and Z → R# are not applicable (since α does not contain Z). If α ⇒ α ′ used the rule R# → R, it was applied at the beginning of α. If m = 0, condition 5 holds (a dead end). Otherwise, we set m ′ := m -1 ≥ 0 and γ := x 1 , and we decrease all indices by one, that is,

Since there is nothing before the nonterminal R, we set n := 0 and β := ϵ. Now, condition 3 holds. If α ⇒ α ′ used the rule R# → ϵ then: if m = 0, we obtain the empty word (which belongs to L * , satisfying condition 4); if m > 0, condition 6 holds (because # remained at the end of α ′ ; at the same time R disappeared, and Z did not appear). The rule Rt → tR is not applicable (the only R in α is immediately followed by #).

a rule from P , it could be applied in γ or in some x i . In the first case, γ ⇒ γ ′ implies βγ ⇒ βγ ′ , hence S ⇒ * βγ ⇒ β ′ γ ′ . In the remaining cases, we observe S ⇒ * x i ⇒ x ′ i as we did at the beginning of our case analysis. As a result, the same condition still holds. The rules Z → ZS# and Z → R# are not applicable (α does not contain Z). If α ⇒ α ′ used the rule R# → R, then γ must have been empty. If m = 0, condition 5 holds (a dead end). Otherwise, we set n ′ := n + 1, w n ′ := β, β ′ := ϵ, γ ′ := x 1 , and m ′ := m -1, and we decrease the indices of x i by one, that is,

now holds (because # remained at the end of α ′ ; at the same time R disappeared, and Z did not appear). If α ⇒ α ′ used a rule of the form Rt → tR (t ∈ T ), we have δ ∈ (T ∪ N ) * such that γ = tδ. We put β ′ := βt and γ ′ := δ. Since βγ = βtδ = β ′ γ ′ , the same condition holds.

α ∈ L * :

No rule is applicable (since α contains only terminals). The step α ⇒ α ′ cannot have happened.

∃σ ∈ (T ∪ N ) * (α = σR):

No matter which rule was applied, it happened within σ. No rule could match the final R. The same condition holds for α ′ = σ ′ R.

11:13

If α ⇒ α ′ used a rule from P , the same condition still holds because # is not on the left-hand side of any rule from P and neither Z nor R is on the right-hand side of any rule from P . The rules

For "⊆ L * ", we use Lemma 2 and observe that if G * generates α ∈ T * , then α ∈ L * because all the remaining cases require α to contain a nonterminal. ◀

Formalization

The formalization closely follows the proof sketch. The main difference between the two is that where the proof sketch states that an expression belongs to a set, the formalization specifies a type for a term and sometimes a condition that further restricts the term's values. Lemma 1 is implemented by lemma short_induction, which takes w in reverse order for technical reasons. Its proof uses the lifted_grammar approach outlined in Section 3. The part R#w 1 #w 2 # . . . w n # ⇒ * w 1 w 2 . . . w n R# is implemented by lemma terminal_scan_ind, which employs a nested induction to pass R to the right. The final step of the easy direction is performed inside the theorem T0_of_star_T0 itself.

Lemma 2 is implemented by lemma star_induction, whose formal proof spans over 3000 lines. The base case is discharged immediately. For the induction step, we developed six lemmas star_case_1 to star_case_6 distinguished by which of the six conditions α satisfies. In each of them, except for star_case_4, which took only four lines to prove, we perform a case analysis on which rule was used for the α ⇒ α ′ transition.

For each case, unless a short ex-falso-quodlibet proof suffices, we need to narrow down where in α the rule could be applied. This analysis is challenging for the rules that were inherited from the original grammar. Consider case_1_match_rule, where the informal argument literally says: "If α ⇒ α ′ used a rule from P , it could be applied only in some x i ."

It turns out that this deduction is so complicated that it was worth creating an auxiliary lemma cases_1_and_2_and_3a_match_aux to detach the head Z from α and perform the analysis on x 1 #x 2 # . . . x m # in order to make the proof easier. As a useful side effect, the auxiliary lemma becomes applicable to similar situations in star_case_2 and star_case_3, as shown in case_2_match_rule and case_3_match_rule, where more adaptations are needed but the same core argument is used.

From a formal point of view, we abused the symbol '. . .' in the proof sketch. Replacing it by a formal statement usually leads to list.join of list.map of something. For example, compare case 1 in the proof sketch The nonterminal # is represented by the letter H in the code. Notice how easy it is to write the quantification ∃x 1 , x 2 , . . . , x m ∈ (T ∪ N ) * in Lean. The part ∀i ∈ [m] (S ⇒ * x i ) is also elegant. However, the expression Zx 1 #x 2 # . . . x m # leads to a fairly complicated Lean term. Because many lemmas need to work with expressions like the above, it is important to master how to manipulate terms that combine list.join with other functions. For example, the following lemma is useful: lemma append_join_append { s : list α} ( L : list ( list α)) :

s ++ ( list . map (λ l , l ++ s ) L ). join = ( list . map (λ l , s ++ l ) L ). join ++ s

This lemma allows us to move the parentheses in s(l 1 s)(l 2 s) . . . (l n s) to get (sl 1 )(sl 2 ) . . . (sl n )s and vice versa.

Working with expressions such as Zx 1 #x 2 # . . . x m # is tedious in Lean. We see this, however, not as a weakness of Lean but rather as an indication that the '. . .' notation is highly informal. Mathematical expressions with '. . .' tend to be ambiguous and require the reader's cooperation to make sense of them. In the absence of support for '. . .' in the proof assistant [START_REF] Horozal | Flexary Operators for Formalized Mathematics[END_REF], it is natural that formalizing such expressions leads to verbose code.

In contrast to concatenation, the above proof cannot be reused to establish the closure of context-free languages under the Kleene star because our construction adds rules with two symbols on their left-hand side. However, there exists an easier construction for context-free languages that could be formalized separately if desired.

Related Work

To our knowledge, no one has formalized general grammars before. Context-free grammars were formalized by Carlson et al. [START_REF] Carlson | Context-Free Grammar -Part 1[END_REF] using Mizar, by Minamide [START_REF] Minamide | Verified Decision Procedures on Context-Free Grammars[END_REF] using Isabelle/HOL, by Barthwal and Norrish [START_REF] Barthwal | Mechanisation of PDA and Grammar Equivalence for Context-Free Languages[END_REF] using HOL4, by Firsov and Uustalu [START_REF] Firsov | Certified Normalization of Context-Free Grammars[END_REF] using Agda, and by Ramos [START_REF] Vinícius | Formalization of Context-Free Language Theory[END_REF] using Coq. Finite automata have often been subjected to verification. In particular, Thompson and Dillies [START_REF]The Lean Mathematical Library[END_REF] formalized finite automata, which recognize regular languages, using Lean. Thomson [START_REF]The Lean Mathematical Library[END_REF] also formalized regular expressions, which recognize regular languages as well.

There is ample verification work also for other models of computation: Turing machines were formalized using Mizar [START_REF] Chen | Introduction to Turing Machines[END_REF], Matita [START_REF] Asperti | Formalizing Turing Machines[END_REF], Isabelle/HOL [START_REF] Xu | Mechanising Turing Machines and Computability Theory in Isabelle/HOL[END_REF], Lean [START_REF] Carneiro | Formalizing Computability Theory via Partial Recursive Functions[END_REF], Coq [START_REF] Forster | Verified Programming of Turing Machines in Coq[END_REF], and recently again Isabelle/HOL [START_REF] Frank | The Cook-Levin theorem[END_REF]. Of these, the most impressive development is probably the last one, by Balbach. It uses multi-tape Turing machines and culminates with a proof of the Cook-Levin theorem, which states that SAT is NP-complete. The λ-calculus was formalized by Norrish [START_REF] Norrish | Mechanised Computability Theory[END_REF] using HOL4 and later by Forster, Kunze, and their colleagues [START_REF] Forster | Weak Call-by-Value Lambda Calculus as a Model of Computation in Coq[END_REF][START_REF] Kunze | Formal Small-Step Verification of a Call-by-Value Lambda Calculus Machine[END_REF]12,[START_REF] Forster | The Weak Call-by-Value Lambda-Calculus is Reasonable for Both Time and Space[END_REF][START_REF] Forster | A Mechanised Proof of the Time Invariance Thesis for the Weak Call-By-Value In[END_REF][START_REF] Gäher | Mechanising Complexity Theory: The Cook-Levin Theorem in Coq[END_REF] using Coq. The latter group of authors proposed an untyped call-by-value λ-calculus as a convenient basis for computability and complexity theory because it naturally supports compositionality. The partial recursive functions were formalized by Norrish [START_REF] Norrish | Mechanised Computability Theory[END_REF] using HOL4 and by Carneiro [START_REF] Carneiro | Formalizing Computability Theory via Partial Recursive Functions[END_REF] using Lean. Random access machines were formalized by Coen [START_REF] Sacerdoti | A Constructive Proof of the Soundness of the Encoding of Random Access Machines in a Linda Calculus with Ordered Semantics[END_REF] using Coq.