We present the design and implementation of the Small Scale Reflection proof methodology and tactic language (SSR) for the Lean 4 proof assistant.

Like its Coq predecessor ,

our Lean 4 implementation, dubbed , provides powerful rewriting principles and means for effective management of hypotheses in the proof context.

Unlike for Coq, does not require explicit switching between the logical and symbolic representation of a goal, allowing for even more concise proof scripts that seamlessly combine deduction steps with proofs by computation.

In this paper, we first provide a gentle introduction to the principles of structuring mechanised proofs using .

Next, we show how the native support for metaprogramming in Lean 4 makes it possible to develop entirely within the proof assistant, greatly improving the overall experience of both tactic implementers and proof engineers.

Finally, we demonstrate the utility of by conducting two case studies: (a) porting a collection of Coq lemmas about sequences from the widely used Mathematical Components library and (b) reimplementing proofs in the finite set library of Lean's mathlib4.

Both case studies show significant reduction in proof sizes.

§ INTRODUCTION

Small Scale Reflection (SSR) is a methodology for structuring
deductive machine-assisted proofs that promotes the pervasive use of
computable symbolic representations of data properties, in
addition to their more conventional logical definitions in the form of
inductive relations.

Small scale reflection emerged from the prominent effort to
mechanise the proof of the Four Colour Theorem in the Coq proof
assistant [9], in which the large number of cases to
be discharged posed a significant scalability challenge for a traditional
proof style based on tactics that operate directly with the logical
representation of a goal.

Support for small scale reflection in Coq has later been implemented
in the form of the plugin, which provides a concise tactic
language, and its associated library of lemmas [11],
becoming an indispensable tool for the working Coq user. has been
employed in many projects, including mechanisations of the foundations
of group theory [10], measure
theory [2], information theory [3], 3D
geometry [1],

programming language semantics [30], as well as proving the
correctness of heap-manipulating, concurrent and distributed
programs [20, 26, 27, 23],
and probabilistic data structures [12].

Two tutorials [18, 25] are
currently recommended amongst the basic learning materials for
Coq [6].

Lean 4 is a relatively new proof assistant and dependently typed
programming language [7].[In the rest of the paper, we
will refer to the latest version 4 of the framework simply as Lean.]

Like Coq, Lean is based on the Calculus of Constructions with
inductive types and is geared towards interactive proofs, coming with
extensive support for metaprogramming aimed at simplifying custom
proof automation and code generation.

Unlike Coq, Lean assumes axioms of classical logic, such as the law of
excluded middle.

Very much in the spirit of the SSR philosophy of reflecting
proofs about decidable propositions into Boolean-returning

Lean encourages the use of such propositions (implemented as an
instance of the Decidable type class) as if they were
Boolean expressions,

going as far as providing a program-level if-then-else operator
that performs conditioning on an instance of a decidable proposition.

Given this similarity of approaches, it was only natural for us to try
to bring the familiar SSR tactic language to Lean, as an alternative
to Lean's descriptive but verbose idiomatic approach to proof

Our secondary motivation was to put Lean's metaprogramming to the
test, implementing SSR entirely within the proof assistant, in
contrast with , which is implemented as a Coq plugin in OCaml.

In this paper, we present , a proof scripting language that
faithfully replicates the experience in Lean, yet provides
substantially better proof ergonomics, thanks to Lean's
distinctive features, improving on its Coq predecessor in the
following three aspects:

*  Usability: Compared to Coq/,
which only shows the proof context between complete series of
chained tactic applications, provides a more fine-grained
access to the proof state, displaying its changes after executing
each “atomic” step—a feature made possible by Lean's mechanism
of proof state annotations.

*  Expressivity: Unlike for Coq,
does not require the user to explicitly switch between
representation of facts as logical propositions or as symbolic
expressions to advance the proof.

In particular, this automation makes it possible to unify
simplifications via computation and via equality-based rewriting,
resulting in very concise proof scripts.

*  Extensibility: Since is
lightweight, , it is implemented entirely in Lean using
its metaprogramming facilities, it can be easily enhanced with
additional tactics and proof automation machineries specific to a
particular project that uses it.

In the rest of the paper, we showcase , substantiating the three
claims above.

Contributions and Outline.

In this work, we make the following contributions:

* An implementation of , an -style tactic language for
Lean.[The snapshot of development accompanying this
submission is available online [8].]

* A tutorial on using following a series of characteristic
proof examples (<ref>).

* A detailed overview of Lean metaprogramming features that we
consider essential for implementing and the effect of those
features on the end-user experience (<ref>).

* Two case studies demonstrating 's utility for proof
migration and evolution: (a) porting a collection of Coq lemmas
about finite sequences from the MathComp
library [18] to Lean and (b) reimplementing
proofs from the finite set library of Lean's mathlib4 in (<ref>).

While proof sizes reduce in both cases, we also comment on our
overall better mechanisation experience, compared to refactoring
original proofs in both Coq and Lean—thanks to the improved
usability aspect highlighted above.

§ IN ACTION

In this section we give a tutorial on the main elements of the proof language. We do not expect the reader to be familiar with the
standard Lean tactics. This section will also be informative for the
readers familiar with for Coq due to the improvements makes
over in terms of usability (<ref>) and expressivity

§.§ Managing the Context and the Goal in Backward Proofs

As customary for interactive proof assistants based on higher-order
logic, Lean represents the proof state as a logical sequent, as
depicted in <ref>.

c_i : T_i …

F_k : P_k …

∀x_l : T_l,  …,
P_n →…→C

Proof state as a sequent

The proof goal is the logical statement below the horizontal
line; above the line is the local context of the sequent, a set
of constants $c_i$ and facts (, hypotheses) $F_k$. The goal
statement itself can be decomposed into (a) goal context:
quantified variables $x_l : T_l$ and assumptions $P_n$,
and (b) the conclusion statement $C$.

Both local and goal contexts capture the bound variables (term-level
or hypotheses) of the overall proof term to be constructed, with the
only difference being the explicit names of the variables in the local

Lean tactics, such as apply, operate directly on the goal's
conclusion using variables from the local context referring to them by
their names, while tactics such as intro and revert move
variables/hypotheses between the local and the goal context.

In practice, such “bookkeeping” of variables and hypotheses
contributes most of the proof script burden; so, following ,
provides tactics to streamline it.

Specifically, provides mechanisms to operate directly with the
goal context, treating the goal as a stack, where the left-most
variable or assumption is the top of the stack, and the conclusion is
always at the bottom of the stack.

By convention, most of tactics, operate with the top element of
the goal stack.

As an example, defines sapply, a variant of the standard
Lean apply tactics (many tactics come with the prefix
s* to distinguish them from their standard Lean counterparts) to
simplify backward proofs <cit.>.

As <ref> shows, sapply applies the first element
on the goal stack (, the hypothesis of type $\alpha$) to the rest
of the stack (, the goal's conclusion $\alpha$).

example: α -> α :=
by sapply

Using sapply tactic

example: @a -> @b -> @a :=
by move=> hA ?
move: hA; sapply
Basic proof script

example: @a -> (@a -> @b) -> @b :=
by move=> /[swap] hAiB
sapply: hAiB

A proof using /[swap] intro pattern

proof scripts using the sapply tactic,
=> and : tacticals, and intro patterns.

A typical proof in is done by moving variables and assumptions
back and forth between the local context and the goal context, placing
the terms to be used in a current proof step on top of the goal

Such proof context management is done via two complementary
tacticals: => and :.

The former one (=>) moves facts above the sequent line, whereas
the latter one moves facts below, “pushing” them to the goal stack.

<ref> and <ref> showcase the usage of
=> and :.

The proof in <ref> starts with move=> hA ?,
where move essentially does nothing: its goal is to serve as a no-op
tactic, to be followed by either => or :.

What follows ( => hA ?) is an example of an intro
pattern (more patterns will be shown below) that introduces the first
two elements of the goal context, the first named hA and the
second with an auto-generated name.

To apply the introduced assumption hA we have to revert it back
to the top of the proof context; the next line move: hA does
exactly that.

Lean users might notice that => and : are similar to the
standard intro and revert Lean tactics.

<ref> demonstrates the versatility of the tacticals when combined with different intro patterns.

For instance, to swap the first two elements of the proof stack,
<ref> makes use of the /[swap] intro pattern.

This will turn our goal to (@a -> @b) -> @a -> @b.

Other useful -inspired intro patterns include * for
introducing all elements on the proof stack,  for
discarding the first element on the proof stack, and /[dup] for
duplicating the first element on the stack.

Furthermore, as the purpose of tacticals is to “massage” the
shape of the goal, they can be smoothly combined with other tactics that operate directly on the goal stack.

In particular, <ref> combines sapply
with : (, sapply: hAiB), with the effect of first
pushing hAiB : @a -> @b to the goal stack and then executing
the sapply tactic, discharging the goal similarly to the example
from <ref>.

§.§ Induction, Case Analysis, and Last-Mile Automation

example (m n : Nat): n <= m ->
m - n + n = m := by
elim: n m=> [| n IHn [| m']] //==
move=> ?; srw -[2](IHn m') //
A proof by mathematical induction

combines the tacticals for the goal context management and intro
patterns with tactics for proofs by induction and case analysis.

In particular, introduces a variant of a standard
induction tactic called elim, which expects no explicit
arguments and simply applies the induction principle of
the top element of the goal stack.

As an example, consider the proof by induction in <ref>
of a simple property of natural addition and subtraction.

As its first step, the proof generalises the two natural constants,
n and m by pushing them onto the goal, making it
@all n m, n <= m -> m - n + n = m;

it is followed by an invocation of the induction principle for natural
numbers on n, with m being universally quantified; all
that expressed simply as elim: n m.

Unlike Lean's induction tactic, elim does not introduce
new variables and facts to the local context, leaving those
universally quantified in the respective subgoals.

In our example, using elim on a natural number introduces two
subgoals, one for the base zero and one for the inductive step
succ, with the latter featuring a predecessor variable and an
inductive hypothesis.

Naming variables in subgoals can be done using the alternation
separator intro pattern of the form [ ... | ... | ... ]
where each  section corresponds to introductions in a
respective subgoal.

We can, thus, revise our proof to be elim: n m=>[| n IHn],
introducing the variable and the hypothesis step to the local context
as n and IHn, respectively.

Let us focus on the second subgoal (, the inductive step), which
now looks as follows:

\begin{equation}
\forall m,\, n + 1 \leq m \to m - (n + 1) + (n + 1) = m
\label{eq:goal}
\end{equation}

The proof of (<ref>) can be finished by the case analysis
on m using 's scase tactic, which will generate two
subgoals, one for zero and one for succ. The latter will
introduce yet another universally-quantified variable, which can be
suitably named and moved to the local context: scase=> [| m'].

Such nested deconstructions of a goal's top variable into cases are so
frequent that overloads the alternation separator intro pattern
to perform case analyses with simultaneous naming. Hence, we can now
revise our proof to first perform top-level induction on n and
then do case analysis on m in the resulting second subgoal via
elim: n m=> [| n IHn [| m']].

Having executed this proof script line, we are left with three
subgoals to discharge:

\begin{align}
\forall m : \mathbb{N},\, 0 \leq m &\to m - 0 + 0 = m \label{eq:goal2}
\\
n + 1 \leq 0 &\to 0 - (n + 1) + (n + 1) = 0 \label{eq:goal3}
\\
(n + 1) \leq (m + 1) &\to (m + 1) - (n + 1) + (n + 1) = (m + 1) \label{eq:goal4}
\end{align}

This would be a good time to make use of Lean's famous automation to
solve (<ref>) and (<ref>), and simplify

provides the following intro patterns for such “last-mile”

* /= for simplification by evaluation (Lean's dsimp)
and /== for proofs by rewriting (simp)

* // for a lightweight automation combining Lean tactics
trivial and simp_all

* //= abbreviating dsimp=> //, and //==
abbreviating simp=> //

In this case, using //== on all generated subgoals leaves us
with only one obligation to prove:

\begin{equation}\label{eq:goal5}
n \leq m' \to m' - n + (n + 1) = (\gbm{m'} + 1)
\end{equation}

§.§ Targeted Rewriting using Equality Hypotheses

The remaining goal (<ref>) can be proven using the previously
introduced induction hypothesis IHn : @all (m : Nat), n ≤ m → m
- n + n = m.

Intuitively, the proof can be completed by replacing the
highlighted second occurrence of $m'$ in
(<ref>) with $m' - n + n$ using the right-hand side of the
equality in IHn, and then finish the proof by the properties of
linear arithmetic and reflexivity.

This can be achieved by rewriting tactic srw allowing one
to specify the term occurrence to be rewritten.

The proof script in <ref> ends with moving the inequality
n ≤ m' to the local context via move=>?, followed by
srw -[2](IHn m') //, where - stands for the
right-to-left rewrite direction and [2] denotes the specific
occurrence of m'.

Performing this rewrite generates the obligation n ≤ m', which
is discharged via //.

The srw tactic generalises Lean's vanilla rw, allowing
for constructions such as:

\[
\text{\code{srw (drop_nth _ lt_i_m) //== -[1]h nth_index //
\]

that interleave rewrites with simplifications, resolving the appearing
subgoals with //.

§.§ Fine-Grained Proof State Exploration and Error

As our examples so far demonstrate, proofs in tend to be quite
compact, thanks to the concise nature of the tactic language that
chains multiple manipulations with the goal and the proof context into
a single line of a proof script.

The downside of this style is that proofs often become difficult to
follow and refactor—a frequent complaint by newcomers to
Coq/who are familiar with the vanilla Coq proof mode.

The problem of proof script understanding and maintenance in is
exacerbated by the fact that Coq can only display the proof context
between complete series of chained tactic applications
separated by periods.

When a mistake is made in the middle of a line in an proof script, one typically has to manually break the line into
period-terminated parts, performing a binary search-style debugging.

In addition to that, if a particular intro pattern cannot be applied
in , say we write [| | m] with three alternations instead
of two in the proof of <ref>, Coq will report an error
for the entire script line, further complicating the search for a fix.

The proof view before introducig IHn

The proof view after introducig IHn

Visual support for fine-grained proof state exploration
with proof scripts.

overcomes these hurdles, providing an improved (compared to
) experience to the users, thereby substantiating the usability
claim (<ref>) from <ref>.

First, the better proof debugging is made possible by the powerful
feature of Lean that allows the DSL designer to annotate each symbol
in the tactic definition with the proof state before and after its

For instance, if the user puts the pointer in the text buffer with her
proof script before the IHn token in <ref>, the
goal display will be as in <ref>, highlighting the
upcoming change in the goal in red.

For the pointer positioned right after IHn, the goal display
shows the proof context as in <ref>.

Second, Lean provides a tunable mechanism for precise error
highlighting, so if we write [| | m] with three alternations
instead of two, only highlight the [| | m] part of the script
will be marked as an error.

§.§ Forward Reasoning via Views

example (A B C : Prop) :
(A → B) → (B → C) → A → C :=
by intro AiB BiC Ha
apply BiC
apply AiB
exact Ha
A backward proof in vanilla Lean

So-called backward proofs, in which a conclusion of a goal is
gradually strengthened to be eventually discharged from the available
hypotheses or axioms, are prevalent in interactive proofs.

A very simple example of such a proof is given in <ref>,
which proves the conclusion C using the reverse-order
applications of the assumptions BiC, AiB, and,
eventually, .

example (A B C : Prop) :
(A → B) → (B → C) → (A → C) :=
fun AiB BiC Ha ↦
have Hb : B := AiB Ha
have Hc : C := BiC Hb
show C from Hc
A forward proof in vanilla Lean

That said, proof engineers trained in a tradition of purely
mathematical proofs often prefer the complementary forward
style, in which the assumptions are gradually weakened to eventually
imply the conclusion <cit.>.

A typical forward proof in Lean follows the so-called
assume/have/show pattern, which explicitly states
the $\forall$-quantified variables and hypotheses as parameters of the
proof term (assume) and the proof is comprises a number of
established auxiliary facts (have) that make the derivation of
the conclusion trivial (show).

An example of such a forward proof in the conventional Lean notation
is shown in <ref>.

offers an alternative way to construct forward proofs using the
idea of view intro patterns or simply views, adopted
from the original  [11].

The proof of the fact from <ref> and <ref> can
be achieved in by the following single line:

by sby move=> AiB BiC /AiB/BiC

Ignoring sby for a moment, notice that the proof first moves
the hypotheses AiB : A → B and BiC : B → C to the

What follows is an application of AiB to the leading (, top)
assumption of the goal A, which “switches” it to B,
making the goal to be B → C.

The subsequent view /BiC switches the leading assumption from
B to C.

The remaining goal C → C can be discharged by trivial
(or 's //).

This is done by the sby tactical at the beginning of the line,
which either completes the proof via // or fails.

In fact, this makes the second view redundant, so the proof can be
shortened to by sby move=> AiB ? /AiB.

§.§ Proofs by Computational Reflection

The demonstration in <ref>–<ref> was
merely a build-up to the true essence of the framework: mechanised
reasoning that features both deduction and proof via
computation by manipulating with equivalent logical and
symbolic representations of decidable facts.

inductive even : Nat → Prop
| ev0 : even 0
| ev2 : ∀ n, even n → even (n + 2)

Even numbers as a logical predicate

def evenb : Nat → Bool
| 0     => true
| 1     => false
| n + 2 => evenb n

Even numbers via a Boolean function

@[reflect] instance evenP n : Reflect (even n) (evenb n) := ...
#reflect even evenb

example n m : even n → even (m + n) = even m := by
elim=> // n' _ <-
srw -Nat.add_assoc /==

A proof using reflection between the logical (even)
and symbolic (evenb) definition of even numbers.

Two equivalent definitions of even numbers (top), and a proof
by reflection (bottom).

As a motivating example showing how to unify both these proof styles
in , consider the following simple proposition: assuming
$n$ is even, $n + m$ is even if and only if $m$ is even.

How should we express a decidable property, such as evenness?

Proof assistants based on higher-order logic, such as Coq,
Isabelle/HOL, and Lean provide two conceptual ways to do so: as a
predicate ( <ref>) and as a function
( <ref>).

The former style comes with an advantage of providing a richer
knowledge when a property occurs in a goal's assumption, ,
by assuming even n we can deduce that it's either zero or
another even number plus two.

The latter comes with a set of reduction/rewrite principles, such as, evenb n + 2 = evenb n, which is advantageous for
simplifying the conclusion of a goal.

One can indeed establish an equivalence between the definitions
even and evenb, proving that @all n, even n ↔
(evenb n = true).

Such an equivalence, when expressed as an instance of the
Decidable type class in Lean, can be exploited by allowing the
user to define computations that explicitly feature a predicate
instead of its computable version, such as:

def even_indicator (n: Nat) : Nat := if even n then 1 else 0

This treatment of decidability also explains the somewhat frivolous
phrasing of our proposition of interest in terms equality instead of
bi-implication (<->) in the statement in <ref>.

To summarise, for Decidable properties, Lean aggressively
promotes the logical definitions to be considered as “primary”,
while the symbolic ones serving merely as helpers for defining
computations and, occasionally, for simplifying goals in the proofs
about equivalent predicates.

This is exactly where comes into play, making such simplifications
transparent to the user. Consider the proof of the example in

The first line initiates the induction on the even n premise,
discharging the first trivial subgoal (for the case ev0),
binding the first argument n' of the case ev2, ignoring
the even n' assumption (via ), and performing the
right-to-left rewrite using the induction hypothesis even (m +
n') = even m in the conclusion (via the <- intro pattern),
leaving us with the following goal to prove:

even (m + (n' + 2)) = even (m + n')

The remaining goal is not difficult to prove by using associativity of
addition and showing that @all x, even (x + 2) = even x.

But also, this is an equality that we should have “for free”, as it
can be derived from the last clause of the definition of evenb
in <ref>!

To account for scenarios like this one, provides a machinery
that allows one to inherit reduction rules of a recursive (symbolic)
boolean definition b to simplify instances of the equivalent
logical proposition P.

To achieve that, one must prove an instance of the Reflect P
b predicate, which is essentially equivalent to proving P ↔
(b = true) (we postpone the details of the Reflect
definition until <ref>) and register this
equivalence using the pragma #reflect P b, which is exactly
what is done by the first two lines of <ref>.

In this case, doing so will add three simplification rules for
even into a database of rewrites used by simplification tactics
such as simp and the corresponding patterns, ,

even 0 = True     even 1 = False     @all n, even (n + 2) = even n

These equalities allow us to finish the proof by /==, rewriting
even as if it were evenb.

's Reflect type class is well integrated with the current Lean
ecosystem. Once one has proven Reflect P b, the corresponding
Decidable instance is automatically derived for P.

Readers familiar with for Coq could notice that a proof of the
statement from <ref> in it would be more verbose, as
it would require an explicit switching between the logical
predicate and its symbolic counterpart in the conclusion by
ing a special Reflect-lemma to the goal.

This is not necessary in thanks to Lean's ability to use the
derived rewriting principles (, the three above for even)
directly on logical representations.

We believe this example supports the expressivity claim
(<ref>) from <ref>.

§.§ Putting It All Together

We conclude this tutorial by showing how all the features of introduced in <ref>–<ref> work in tandem in a
proof of an interesting property: transitivity of the subsequence
relation on lists of elements with decidable equality.

<ref> presents two ways to define the relation.

The first one is via a predicate and an auxiliary mask
function. The mask function takes two lists: a list of Boolean
values m and a list s of elements of some type

For each element of s, mask removes it if an element in
m at the same position is either false or not
present (, m is shorter than s).

Then the representation of subsequence as a logical predicate states
that s1 is a subsequence of s2, if mask m s2 = s1
for some mask m.

The second definition is via a total recursive function subseqb
returning a Boolean.

This definition we checks that each element in the first list
corresponds to some element in the second list using the decidable
equality on the values of type $\alpha$, whose existence is postulated
in the first line of the listing.

For the propositional and Boolean representations above, we can prove
a Reflect instance ( <ref>), and transport
reduction principles of subseqb to subseq by adding the
#reflect pragma as at the line 1 of <ref>.

variable α : Type [DecidableEq α]

def mask: List Bool → List α → List α
| b :: m, x :: s =>
if b then x :: mask m s else mask m s
| _, _ => []

def subseq (s1 s2 : List α) : Prop :=
∃ m, length m = length s2 /
s1 = mask m s2

def subseqb: List α → List α → Bool
| [], _ :: _          => true
| s, []               => s = []
| s@(x :: s'), y :: r =>
subseqb (if x = y then s' else s) r

Two representations of the subsequence relation

#reflect subseq subseqb

def transitive (R: α → α → Prop) :=
∀x y z, R x y → R y z → R x z

example: transitive (@subseq α) := by
move=> ?? s ![m2 _ ->] ![m1 _ ->]
elim: s m1 m2=> [// |x s IHs1]
scase=> [// | [] m1 /= m2]
– m1's head is false
scase!: (IHs1 m1 m2)=> m sz_m ->
sby exists (false :: m)
– m1's head is true
scase: m2=> [|[] m2] //=
scase!: (IHs1 m1 m2)=> m sz_m ->
sby exists (false :: m)

Proof that subseq is transitive

A subsequence relation and the proof of its transitivity in

<ref> shows the entire transitivity proof.

At line 7, it introduces a new intro pattern ![...], which is
an advanced version of the case analysis [...]: not only does
it destruct the structure on top of the proof stack, but also does so
for its nested structures.

For instance, the second occurrence of ![...] will turn the
goal (∃m, length m = length s ∧ w = mask m s) → ... into
@all m, length m = length s → w = mask m s → ... by destructing
both the existential quantifier (, the dependent product) and its
nested conjunction.

The remaining in-place rewrites (via ->) at the line 7 turn the
goal into:

\begin{equation}
\text{\code{subseq (mask m2 (mask m1 s)) s}}
\label{eq:goal-trans}
\end{equation}

In plain text, we have to show that if we apply mask to some
sequence s with two arbitrary masks, m1 and m2,
the resulting sequences would be a subsequence of s.

Line 8 advances the proof by induction on s, after generalising
the goal over m1 and m2 and discharging the base case
with //, which implicitly uses the rewrites allowed by the
definition of mask.

Next, line 9 performs the case analysis on m1. When it is empty, goal
(<ref>) becomes subseq [] s, which can be automatically
reduced to True by employing the reflection between subseq and

The case when m2 is empty is handled automatically in a similar
fashion at line 14.

We are now left with the following two remaining goals:

* If m1 is non-empty and its first element is false (lines
11-12), then after all simplifications, goal (<ref>)
is reduced to subseq (mask m2 (mask m1 s)) (x :: s),

where x is a head of the initial list s.

Here we employ the induction hypothesis IHs1 at line 11, to
state that mask m2 (mask m1 s) is a subsequence of s,
which means that mask m2 (mask m1 s) is just mask m s,
for some mask m.

To finish the proof we instantiate the existential quantifier in the
definition of subseq by taking false :: m, which, when
applied to x :: s produces exactly mask m s (line 12).

* If the first element of m1 is true, we perform case analysis
on m2 (line 14), dispatching the empty case in a way similar to dealing
with m1 at line 9.

When m2's first element is also true is
trivial as in this case neither of the masks removes the head of
s and our goal will simplify to subseq (x :: mask
m2 (mask m1 s)) (x :: s) and then, by reflection, to subseq
(mask m2 (mask m1 s)) s, which is trivially implied by the
induction hypothesis.

All this is done by //= at the end of line 14.

Finally, the case when m2's head is false
(lines 15-16) is similar to the proof at lines 11-12.

The proof in <ref> comes from our case study:
migrating the MathComp library seq from Coq/to Lean.

In <ref> we will further elaborate on this
mechanisation effort.

§ IMPLEMENTING USING LEAN METAPROGRAMMING

In this section we shed light on the implementation of , which
makes extensive use of Lean's metaprogramming facilities.

Despite the abundance of available tutorials on implementing tactics
in Lean, it still took significant effort to understand how to compose
different features to achieve the desired behaviour,

following examples from the Lean Metaprogramming Book [22],
several research papers [24, 29], Lean
source code, and online meetings with Lean developers.

This makes us believe that our report on this experience might be of
interest even for seasoned Lean users who consider developing their
own tactics.

Besides the new -specific tactics, such as elim,
scase, sapply, ., the three essential enhancements
made by over the vanilla Lean tactic language are:

* Intro patterns: the set of commands that can follow =>

* Rewrite patterns: the set of commands that can follow srw

* Revert patterns: the set of commands that can follow :

We refer to those commands as patterns because they are meant to
(partially) match some part of the goal.

The first set, , intro patterns, includes ?, *, [..
| ... | ..], .

The second set, rewrite patterns, includes eq, [i j
...]eq, -[i j ...]eq, , where eq is an arbitrary
equality fact.

For the sake of space, we do not detail revert patterns in this paper,
but they are fully documented in the  file of the
accompanying code repository [8].

The characterisation of the three pattern categories is non-exclusive:
some commands, , // and /==, can be used
both as intro patterns (following =>) and rewrite patterns
(following srw).

To avoid code duplication, those “last-mile automation” commands
themself form a set of automation patterns that are implemented
separately and then registered to work in positions of both intro and
rewrite patterns.

High-level structure of

An informal depiction of patterns can be found in
<ref>. Each box stands for a separate set of pattens, the
arrows denote the dependencies between those sets.

In <ref>–<ref>, we discuss the implementation of
the components highlighted by grey boxes, concluding with a discussion
on support for computational reflection in

We do not assume the reader to be familiar with metaprogramming in
Lean and will explain the required notions as we progress with our

§.§ Syntax, Macros, and Elaboration for the Last-Mile Automation

We start by discussing the three key features of Lean metaprogramming
essential for our embedding: (1) syntactic categories,
(2) macro-expansion, and (3) elaboration rules, using the
implementation of automation patterns as an example.

The implementation is shown in <ref>. At the high
level, we first define a syntax for a sequence of such patterns (lines
1-8), then tell Lean how to execute such a sequence (lines 10-22),
concluding with the definition of sby tactical.

More detailed explanation of the code follows below.

declare_syntax_cat ssrTriv
syntax "//" : ssrTriv
syntax "/=" : ssrTriv
syntax "/==" : ssrTriv
syntax "//=" : ssrTriv
syntax "//==" : ssrTriv
declare_syntax_cat ssrTrivs
syntax (ppSpace colGt ssrTriv)* : ssrTrivs

elab_rules : tactic
| `(ssrTriv|  /=) =>
run `(tactic| try dsimp)
| `(ssrTriv| /==) =>
run `(tactic| try simp)
| `(ssrTriv|  //) => ... – omitted

| `(ssrTriv| //= ) => `(ssrTrivs| /= // )
| `(ssrTriv| //==) => `(ssrTrivs| /== //)

elab_rules : tactic
| `(ssrTrivs| $ts : ssrTriv *) =>
for t in ts do allGoals $ evalTactic t

elab sby:"sby " ts : tacticSeq : tactic => do
evalTactic ts
unless (<- getUnsolvedGoals).length = 0 do
allGoals $ run `(ssrTriv| //)
unless (<- getUnsolvedGoals).length = 0 do
throwErrorAt sby "No applicable tactic"
\end{lstlisting}%$
\end{subfigure}
\captionsetup{aboveskip=2pt}
\captionsetup{belowskip=-10pt}
\caption{Implementing of last-mile automation in \lssr using Lean
\label{fig:ssrTriv}
\end{figure}

Line 1 defines a \emph{syntactic category} called \code{ssrTriv} for
the \lssr automation patterns. One can think of a syntactic category as
of a set of syntax expressions grouped together under a single name, for
which interpretations can be given.
Next, lines 2-6 define elements of this category: \code{//},
\code{/=}, \code{/==}, \code{//=} and \code{//==}.
At line~7, we define yet another syntax category \code{ssrTrivs} for
sequencing automation patterns.
Elements of this category are iterated sequences of \code{ssrTriv}
separated with a space~\code{ppSpace}.
To ensure that Lean does not try to parse the next line after a
sequence of the patterns \code{ssrTriv} as a its continuation, we also
insert the \code{colGt} element, which allows for line breaks, but
only if the column number of the pattern on a new line is greater than
the column number of the last pattern on the line above, in the spirit
of Landin’s Offside Rule~[15].

Having defined the syntax for the automation pattern, we proceed
to ascribe semantics to it.
Lines 10-15 give a meaning to basic automation patterns by using
Lean's standard mechanism of elaboration rules via the
\code{elab_rules} directive.
Each elaboration rule maps a piece of a syntax into an execution
inside Lean's \code{TacticM} monad~\cite[\S{8.3}]{love},
% \footnote{In general, elaboration rules might elaborate syntax into
% four objects: tactics, commands, expressions, and attributes. For
% our purposes we only need tactic elaboration rules (specified with
% \fcode{: tactic}).}
thus defining a tactic in terms of other Lean tactics, with
access to the global proof state.
For example, \code{/=} is elaborated into executing the standard
\code{try dsimp} tactic (lines~11-12).
The remaining automation patterns, \code{//=} and \code{//==} are
defined in terms of the more primitive elements of \code{ssrTriv}.
This is done using Lean's rules for macro-expansions, following the
\code{macro_rules} directive.
Macro-expansion rules in Lean map elements of syntax into executions
within the~\code{MacroM} monad, returning another element of syntax as a
Those rules are applied by the Lean interpreter after the parsing
stage, but before the elaboration stage.
Here, we simply expand \code{//=} to \code{/= //}, and \code{//==} to
\code{/== //}, as shown at lines~16-18 of \autoref{fig:ssrTriv}.

% elab_rules : tactic
%     | `(ssrTrivs| $ts:ssrTriv *) =>
%         for t in ts do allGoals $ evalTactic t

Since both \code{//=} and \code{//==} are represented as elements of
the \code{ssrTrivs} category, we have to tell Lean how to elaborate
them as well.
For the sake of demonstration, we are going to do it by employing
one of the most powerful tools in Lean's metaprogramming toolbox: the
\code{evalTactic} directive.
This directive takes an arbitrary piece of syntax and tries to
elaborate it into a sequence of tactics to be executed, using a set of
macro-expansion and elaboration rules available in the \emph{dynamic}
context, \ie, the rules available at the \emph{usage site} in a
particular proof script.
% It is extremely convenient for defining tactics in terms of other
% tactics, as it will automatically execute the constituents in the
% respective proof contexts without requiring the DSL designer to set up
% such executions explicitly.
%In particular,
We will get to experience \code{evalTactic} in its full glory in
\autoref{sec:intropats}. For now, let us highlight one of its most
useful features: annotating each token in the given syntax with a
correspondent proof state.
That is, when elaborating and executing its argument,
\code{evalTactic} saves the goal before and after executing each
% in a dedicated place of the overall environment.
allowing for the interactive fine-grained proof state exploration we
presented in~\autoref{sec:debug}.
% \code{evalTactic} will also try all different combinations of
% macro-expansions and elaboration rules to interpret the given syntax.
% We detail this aspect of \code{evalTactic} at \autoref{sec:intropats}.
% %
% All in all, \code{evalTactic} is a hidden gem of Lean metaprogramming
% that takes care of a substantial amount of implementation burden
% required for tactic engineering.

Finally, lines~24-30 implement the \code{sby} tactical
(\autoref{sec:views}). Line~24 defines both its syntax and elaboration
using the \code{elab} directive.
The tactical starts with the string ``sby'' (its position in a
concrete syntax tree is bound as \code{sby}), followed by a sequence
of tactics \code{ts}.
We first run this tactic sequence (line~15), then, unless it has
solved all goals, we run \code{//} (lines~26-27).
Otherwise, if there are unsolved goals, an error is reported at the
\code{sby} position.

\vspace{-5pt}

\subsection{Intro Patterns, Modularity, and Extensibility}
\label{sec:intropats}

Let us now briefly go through the high-level structure of
the implementation of intro patterns.
While to a large extent similar to that of last-mile automation,
this part of our development showcases two new noteworthy aspects of
\lssr internals.
First, we will demonstrate the \emph{modular} nature of pattern
definitions by showing how the intro pattens incorporate those for
Second, we will show how the intro patterns that come with \lssr can
be easily \emph{extended} for domain-specific proofs, thus addressing
claim~(\ref{label:ext}) from \autoref{sec:intro}---an aspect of our
implementation made possible by the dynamic nature of the
\code{evalTactic} directive.

\begin{figure}[h]
\centering
\begin{subfigure}{0.45\textwidth}
\begin{lstlisting}[basicstyle=\scriptsize\ttfamily,numbers=left,numberstyle=\tiny\color{ACMRed}]
declare_syntax_cat ssrIntro
syntax ssrTriv : ssrIntro
syntax ident : ssrIntro
syntax "?" : ssrIntro
declare_syntax_cat ssrIntros
syntax (ppSpace colGt ssrIntro)* : ssrIntros

elab_rules : tactic
| `(ssrIntro| $t:ssrTriv) => evalTactic t
| `(ssrIntro|$i:ident) =>
run `(tactic| intro $i:ident)
| `(ssrIntro| ?) =>
run `(tactic| intro _)
\end{lstlisting}
\end{subfigure}
\hspace{4mm}
\begin{subfigure}{0.45\textwidth}
\begin{lstlisting}[basicstyle=\scriptsize\ttfamily,firstnumber=16,numbers=left,numberstyle=\tiny\color{ACMRed}]
elab_rules : tactic
| `(ssrIntros| $is:ssrIntro*) =>
for i in is do allGoal $ evalTactic i

elab t:tactic "=> " is:ssrIntros : tactic =>
do evalTactic t; evalTactic is

| `(ssrTriv| //) => `(tactic| omega)
syntax "!" : ssrIntro
elab_rules : tactic
| `(ssrIntro| !$i:ident) =>
run `(tactic| ext)\end{lstlisting}
\end{subfigure}
\captionsetup{aboveskip=2pt}
\captionsetup{belowskip=-10pt}
\caption{Implementation of \lssr intro patterns and their extensions.}
\label{fig:ssrIntro}
\end{figure}

\noindent
\autoref{fig:ssrIntro} presents a fragment of the implementation of
intro patterns for \lssr.
Following the template outlined in \autoref{sec:auto}, it defines the
syntax for a single intro pattern (lines 1-6) and multiple intro patterns
(lines 5-7).
% embedding all \code{ssrTriv} patterns to \code{ssrIntro} at line~5.
Now, to allow for last-mile automation within intro patterns, we only
have to explicitly add line~10, which, intuitively, says: once
you meet a \code{ssrTriv} inside some \code{ssrIntro}, just handle it
with the already defined macro/elaboration rules.
Lines~11-14 provide examples of an intro pattern elaboration rule: a
constant introduction with an explicit name~\code{i} (lines~11-12) and
with an autogenerated name (lines~13-14), handled using Lean's
\code{intro} tactic.
Lines~16-18 handle a sequence of intro patterns.
Finally, a new tactic \code{=>} is defined at lines~20-21 to allow use of
intro pattens in a proof script.

Lines 24-25 of \autoref{fig:ssrIntro} show the first example of
extensibility afforded by Lean metaprogramming: augmenting the
automation pattern \code{//} to discharge arithmetic facts by calling
the standard \code{omega} tactic.
This definition \emph{enhances} the behaviour of the pattern in the
entire scope below the macro-expansion rule (keep reading to learn why
it does not \emph{replace} the original behaviour of \code{//}).
Another example of extensibility is presented at lines~27-30,
integrating a domain-specific tactic into \lssr patterns.
The mathlib's \code{ext} tactic automaticallly applies extensionality
axioms, \eg, turning a goal of the form \code{f = g}, where both
\code{f} and \code{g} are functions, into \code{@all x, f x = g x},
followed by introduction of~\code{x}.
We integrate it into \lssr intro patterns by definining the syntax
\code{!} for it as a new \code{ssrIntro} pattern at line~27, and by
elaborating the \code{!} pattern to the \code{ext} tactic at lines
% \is{From the paragraph above, it is not clear why with this
%   elaboration, \code{ext} is going to be run \emph{before} (not after
%   or instead) of the corresponding introduction tactic, since the rule
%   also mentions the identifier, as in \code{i:ident}. Please, add a
%   sentence explaining what's going to happen \wrt the old logic.}

The desired effect in both scenarios outlined above is achieved by the
two somewhat non-obvious practices we follow in our implementation of
\lssr patterns:
\begin{enumerate}[(a),topsep=2pt]
\item The semantics of the patterns is implemented exclusively using
the \code{macro_rules} and \code{elab_rules} commands, while their
evaluation is \emph{always} done using \code{evalTactic}, which is
invoked from the definitions of pattern sequences, as appear in
\autoref{fig:ssrTriv} as \autoref{fig:ssrIntro}.
\item Elaboration rules for each particular pattern are defined
separately from others.
\end{enumerate}

\noindent
Following these practices makes it possible to extend \lssr with new
\code{macro_rules} and \code{elab_rules} in a modular fashion.
To extend \lssr with a new pattern or add a new behaviour, it suffices
to just add a new elaboration/macro rule for it.
The reason why it works follows from the way \code{evalTactic}
performs the bookkeeping of the macro/elaboration rules and their
Any new such rule is added at the top of a \emph{rule database stack}.
Whenever \code{evalTactic} is invoked (\eg, when elaborating and
executing a particular sequence of intro patterns as per line~18 of
\autoref{fig:ssrIntro}), it will go through the stack of the saved
rules, starting from the top, until it either finds the first one that
executes without errors (\ie,~without throwing an exception as in
\autoref{fig:ssrTriv} at line~29), or exhausts the stack.%
\footnote{It is a good practice to put elaboration into tactics, which
either fully solve the goal or fail otherwise, closer to the top of
the stack, so they would not be preempted by elaboration into
tactics that never fail.}

In particular, in case of \code{//} supplied with the rule at the
lines~24-25 of \autoref{fig:ssrIntro}, \code{evalTactic} will first
try to expand it into \code{omega}.
If \code{omega} executes without errors (this is only possible if it
solves the goal completely), \code{evalTactic} looks no further.
If \code{omega} fails, leaving the goal unchanged, \code{evalTactic}
proceeds with the next option on the rule stack, \ie the one at
line~15 of \autoref{fig:ssrTriv} (assuming no other registered rules
for \code{//}).
%  As we have no macro
% rules for \code{omega} anymore, \code{evalTactic} will try to
% elaborate it with the only elaboration rule we have at this point
% (\autoref{fig:ssrTriv} line 15).
This is the reason why lines~24-25 of
\autoref{fig:ssrIntro} \emph{do not alter} the behavior of \code{//}
but augment it with \code{omega}.

\vspace{-8pt}

\subsection{Rewrite Patterns and Custom Environment Extensions}
\label{sec:srw}

The implementation of \lssr rewrite patterns relies on yet another
very useful feature of Lean metaprogramming: \emph{custom environment
state extensions}.
% We decided to dedicate a separate subsection for this
% feature as it is not specifically documented anywhere else. Let's
% first discuss a motivation for environment state extensions.
The need for environment state extensions comes from the rather
restrictive format of \code{evalTactic}, which takes only one
argument: the syntax of the tactic to elaborate and run.
Therefore, the execution of a tactic implemented via \code{evalTactic}
can only depend on the general proof environment, \ie, the proof
context and the set of all available definitions available at the
point of its invocation.
So far, this has been sufficient for our needs to implement patterns
for automation and introduction that were ``context-independent''.
The behaviour of a useful tactic for rewriting is a bit more complex,
since this tactic is expected to take a rewrite \emph{location}, \ie,
a local hypothesis or the goal (its default behaviour).
While the location of a rewrite is accessible at the level of the
entire tactic command, it cannot be directly passed to
\code{evalTactic} when elaborating each individual rewrite pattern, as
the pattern itself is \code{evalTactic}'s sole argument.
Custom environment state extensions solve this issue by providing
access to \emph{additional state} that can be used to store such
data when elaborating a top-level command, making its accessible for
the elaboration rules of its inner components (\ie, the patterns).

\begin{figure}[t]
\centering
\begin{subfigure}{0.42\textwidth}
\begin{lstlisting}[basicstyle=\scriptsize\ttfamily,numbers=left,numberstyle=\tiny\color{ACMRed}]
declare_syntax_cat ssrRw
syntax ssrTriv : ssrRw
syntax term:max : ssrRw
declare_syntax_cat ssrRws
syntax (ppSpace colGt (ssrRw))* : ssrRws

abbrev LocationExtState := Option
(TSyntax `Lean.Parser.Tactic.location)

initialize locExt :
EnvExtension LocationExtState ←
registerEnvExtension (pure none)
\end{lstlisting}
\end{subfigure}
\hspace{4mm}
\begin{subfigure}{0.48\textwidth}
\begin{lstlisting}[basicstyle=\scriptsize\ttfamily,firstnumber=16,numbers=left,numberstyle=\tiny\color{ACMRed}]
elab_rules : tactic
| `(ssrRw| $t:ssrTriv) =>
evalTactic t
| `(ssrRw| $i:term) => do
let l <- locExt.get
run `(tactic| rw [$i:term] $(l)?)

elab "srw" rs:ssrRws l:(location)? : tactic => do
locExt.set l
evalTactic rs
\end{lstlisting}
\end{subfigure}
\captionsetup{aboveskip=2pt}
\captionsetup{belowskip=-10pt}
\caption{Implementing rewrite patterns by passing the rewrite location
in a local state extension.}
\label{fig:ssrRw}
\end{figure}

To demonstrate the use of this technique, \autoref{fig:ssrRw} shows an
implementation of a restricted version of \lssr rewriting, which only
supports rewrites of the form:
\vspace{-3pt}
\begin{center}
\code{srw Eq1 // Eq2 Eq3 // ...}
\end{center}
\vspace{-3pt}
In other words, it only allows for rewriting with equality facts (\ie,
\code{Eq1}, \code{Eq2}, \etc.) and for employing last-mile automation
to solve the generated sub-goals.
Importantly, our example also allows for rewriting at a specified
hypothesis \code{H} from the local context using \code{srw ... at H}
The syntactic category for rewrite patterns is defined at lines~1-5 of
\autoref{fig:ssrRw}.
It includes automation (line~2) and ordinary Lean terms (line~3).
Preparing to pass the rewrite location around as an additional state
component, we first define a type of the state extension
\code{LocationExtState} (lines~7-8). It is an option, where \code{some
...} denotes a local hypothesis to rewrite at, and \code{none}
stands for the goal.
Next, the \code{initialize} command registers the custom state
component of the type \code{LocationExtState} with the name
\code{locExt}, storing \code{none} to it as a default value
Fast-forward to lines~24-26, the elaboration rule for \code{srw} first
sets the value \code{locExt} to the optional argument \code{l}, \ie,
the hypothesis passed after \code{at} or the goal, if that part is
Finally, the elaboration rule for named rewrite patterns (\ie,
equality facts) at lines~19-21 first fetches the location from the
\code{locExt} component of the extended state, and then executes
Lean's native rewrite tactic \code{rw} at that location.

\vspace{-6pt}

\subsection{Computational Reflection via Type Classes}
\label{sec:ssrimpl}

We conclude this section by discussing the implementation of
computational reflection in \lssr via Lean type classes and its
interaction with \code{Decidable} instances.
% In \autoref{sec:refl} and~\ref{sec:putting-it-all} we have shown how
% \lssr performs simplification of inductive propositional predicates as
% they were recursive Boolean functions.
% %
% Now we explain how this is implemented.

Lines~1-4 of \autoref{fig:ssrimpl} provide the definition of the
\code{Reflect} predicate adopted almost verbatim from \ssr (we will
explain the \code{outParam} keyword below).
Lean users can notice that \code{Reflect} is very similar to
\code{Decidable} with the only difference being that the former mentions the
Boolean representation of the decidable predicate explicitly.
The \code{#reflect} command at line~10 will use this explicit Boolean
representation~\code{b} to generate reduction/rewrite rules for the
respective predicate \code{P}. This simplification machinery for
propositions is generated from their corresponding symbolic
counterparts in two steps:
\begin{enumerate}[(i),topsep=2pt,leftmargin=17pt]
\item\label{step1} The reduction principles of symbolic representations
are retrieved as quantified equalities.
\item\label{step2} Boolean functions in those equalities are replaced
with their corresponding propositions.
\end{enumerate}
Step~\ref{step1} comes ``for free'':
to partially evaluate recursive definitions, Lean automatically
generates lemmas in the form of quantified equalities representing the
available reductions.
For example, for the \code{evenb} definition from \autoref{fig:refl}
in \autoref{sec:refl} Lean will generate tree lemmas:
\begin{center}
\code{eq1: evenb 0 = true} \quad\quad
\code{eq2: evenb 1 = false} \quad\quad
\code{eq3: @all n, evenb (n + 2) = evenb n}
\end{center}
Those lemmas are then implicitly used by the \code{simp} and
\code{dsimp} tactics in Lean proofs.

\begin{figure}[t]
\centering
\begin{subfigure}{0.47\textwidth}
\begin{lstlisting}[basicstyle=\scriptsize\ttfamily,numbers=left,numberstyle=\tiny\color{ACMRed}]
class inductive Reflect (P : Prop) :
(b: outParam Bool) -> Type
| T (_ : P) : Reflect P true
| F (_ : ¬ P) : Reflect P false

theorem toPropEq (_: b1 = b2)
[Reflect P1 b1] [Reflect P2 b2] :
P1 = P2 := ...

elab "#reflect" P:term b:term : command => ...
\end{lstlisting}
\end{subfigure}
\hspace{4mm}
\begin{subfigure}{0.50\textwidth}
\begin{lstlisting}[basicstyle=\scriptsize\ttfamily,firstnumber=11,numbers=left,numberstyle=\tiny\color{ACMRed}]
macro "reflect" : attr => `(attr| default_instance)
@[reflect] instance tP : Reflect True true := ...
@[reflect] instance : Reflect False false := ...
@[reflect] instance [Reflect P1 b1] [Reflect P2 b2]
: Reflect (P1 ∧ P2) (b1 && b2) := ...
@[reflect] instance [Reflect P1 b1] [Reflect P2 b2]
: Reflect (P1 ∨ P2) (b1 || b2) := ...
... -- other basic reflect predicates

instance [Reflect P b] : Decidable P := ...
\end{lstlisting}
\end{subfigure}
\captionsetup{aboveskip=2pt}
\captionsetup{belowskip=-15pt}
\caption{A fragment of computational reflection implementation in
\lssr.}
\label{fig:ssrimpl}
\end{figure}

With all those equalities at hand, step~\ref{step2} is achieved
with the help of the \code{toPropEq} lemma (lines~6-8) that derives the
equalities on propositions out of equalities on their Boolean
For example, applying \code{toPropEq} to the quality \code{eq1} above
will give us the equality \code{even 0 = True}, assuming we also
somehow synthesise its two implicit \code{Reflect} instance arguments.
The synthesis is enabled by the following \lssr components.

The first one is a library of \code{Reflect}-lemmas connecting
standard logic connectives, such as $\wedge$ and $\vee$ with their
computational counterparts, \ie, \code{&&} and \code{||}.
The need for those lemmas arises when we need to synthesise a
propositional version of a symbolic expression that does not have an
application of the function in question at the top level.
In particular, while the left-hand side of all retrieved equalities is
always a function applied to some arguments (\eg, \code{evenb (n +
2)}), the right-hand-side might be an arbitrary expression
containing other symbolic logical constants and connectives.
The various \code{Reflect}-lemmas (lines~12-18 of
\autoref{fig:ssrimpl}) provide recipes for synthesising \emph{proofs}
for the corresponding logical counterparts in a way similar to
type class instance resolution in Haskell.
\lssr provides a collection of such lemmas, and the user can add their
own, extending the reflection in a modular fashion.

Alas, the type class resolution mechanism of Lean will not immediately
work as desired.
For example, when we apply \code{toPropEq} to \code{eq1}, it will have
to work out two instantiations (\ie, proofs): for \code{Reflect ?P
(evenb 0)} with \code{?P := even 0} and for \code{Reflect ?Q true}
with \code{?Q := True} (line~12).
By default, Lean's algorithm for synthesising instances will fail due
to a simple reason: to construct an instance of, \eg, \code{Reflect ?P
(evenb 0)} it \emph{must know} what that \code{?P} is.
That is, the algorithm will only attempt to synthesise an inhabitant
for a fully instantiated type class signature, but not for the one
that has variables.
To fix this, we use the mechanism of \emph{default instances}, \ie,
proof terms that are available for instance search even when not
all type class arguments are known~\cite[\S{4.3}]{funlean}.
For example, marking \code{tP : Reflect True true} as a default
instance will make the type class resolution algorithm aware of it,
thus, finding a suitable instantiation for \code{?Q} in the process.
For readability, \lssr provides a \code{reflect} notation for the
\code{default_instance} attribute, so that \code{Reflect} instances
can be marked as default ones simply by tagging them with \code{@[reflect]}.

The last bit of our implementation is a link between \code{Reflect}
and \code{Decidable}.
Once a \code{Reflect} instance for a logical predicate \code{P} is
provided, \lssr also generates its decidable instance (line~20 of
\autoref{fig:ssrimpl}), \eg, to use this \code{P} in any position that
requires a Boolean expression.
Marking the parameter~\code{b} of \code{Reflect} as \code{outParam}
(line~2) is essential for this: it tells the instance search algorithm
that \code{b} is not required for finding the instance (since \code{P}
already provides enough information), and should be treated as the
output of the synthesis.

% \is{Stopped here.}
% %
% The problem, however, is that in this case, Lean has also to
% synthesise a boolean representation \code{b} as well. To make it
% possible we just mark \code{b} to be an \code{outParam}, when defining
% \code{Reflect} type class (line 2).

\section{\lssr in the Wild: Case Studies}
\label{sec:case}

% This section demonstrates a little bit more examples of Lean version
% of SSReflect in anger. We, first, show a little bit more proofs from
% Mathlib/Mathcomp ported to SSRLean and explain how did they become
% better.

In this section, we showcase two examples that support our claims from
\autoref{sec:intro}, by demonstrating \lssr's expressivity compared to
Coq/\ssr and to vanilla Lean, highlighting the more compact proof
scripts we obtain, as well as the overall usability of our approach.

\subsection{Migrating MathComp Sequences to \lssr}
\label{sec:ssrseq}

To evaluate \lssr against \ssr, we ported a small subset (approximately 10\%) of
the finite sequences file from the Mathematical Components
library Coq~[18], amounting to 31 definitions, 72 theorems,
and 3 reflection predicates.
As the logics of Lean and Coq are similar, and MathComp is implemented in \ssr,
which is syntactically very similar to \lssr, most proofs can be translated
almost mechanically, with minimal changes.

\begin{figure}[t]
\begin{lstlisting}[language=SSR,basicstyle=\footnotesize\ttfamily,numbers=left,numberstyle=\tiny\color{ACMRed},
Lemma subseq_trans: transitive subseq.
move=> _ _ s `/subseqP` [m2 _ ->] `/subseqP` [m1 _ ->].
elim: s m1 m2 => [*|x s IHs]; @first by rewrite !mask0.@
case=> [*|[] m1 m2]; @first by rewrite !mask0.@
{ case: m2=> [/=|[] m2] //; @first by rewrite /= eqxx IHs.@
case `/subseqP`: (IHs m1 m2) => m sz_m ?; `apply/subseqP.`
by exists (false :: m); @rewrite //= sz_m.@ }
case`/subseqP`: (IHs m1 m2)=> m sz_m ?; `apply/subseqP.`
by exists (false:: m); @rewrite //= sz_m.@
\end{lstlisting}
\captionsetup{aboveskip=0pt}
\captionsetup{belowskip=-10pt}
\caption{\ssr proof of the theorem in \autoref{fig:trans}. Parts not needed in \lssr are highlighted.}
\label{fig:subseqCoq}
\end{figure}

Our proofs are nonetheless more compact than the originals for two reasons:
(a) the user does not need to explicitly switch between logical and symbolic
representations of the goal (claim~\ref{label:express})
and (b) many rewrites can be performed by \lssr's simplification mechanism, due
to its extensibility (claim~\ref{label:ext}), and do not need to be invoked
A representative example can be seen in \autoref{fig:subseqCoq}, which shows a
\ssr proof (slightly modified from the original for presentation purposes) of
the fact that the subsequence relation is transitive.
The \lssr equivalent was shown previously in \autoref{fig:trans}.
The Lean version is more compact as it requires neither the explicit invocations
of the reflection predicate (highlighted in \redbox{red} in
\autoref{fig:subseqCoq}) nor various trivial rewrites (highlighted in
\orangebox{orange}), which can be performed automatically by \lssr's powerful
and extensible \code{//} automation.
Overall, this amounts to a reduction in half of the size of each line of proof,
and we argue, to a reduction of the cognitive effort required of the user, who
can now focus on the essential aspects of the proof, delegating trivial details
to automation.
Indeed, many simple statements can be proven in \lssr by \code{elim:
s=>//=}, reminiscent of the \code{induct-and-simplify} tactic of
PVS~[21, 28].

\subsection{Refactoring mathlib}
\label{sec:mathlib}

To evaluate \lssr against proofs in mathlib~[19],
we ported a few facts about cardinalities of finite sets.
\autoref{fig:lssr-vs-mathlib} presents two proofs of \emph{a subgoal} for
the \code{card\_eq\_of\_bijective} lemma from mathlib: the original proof and
one ported to \lssr. The subgoal states that for a bijective
function~\code{f} from a range of all natural number less
than~\code{n}, each element in this range has a pre-image
\wrt~\code{f}.
Notably, mathlib proofs frequently build a proof term explicitly,
rather than via tactics.
In cases like the one in \autoref{fig:lssr-vs-mathlib}, such
manual proof term construction tends to be more concise than the
respective proof script, hence the ubiquity of this mechanisation
style in mathlib.
% That is exactly what is done at
% \autoref{fig:mathlib}.
The same proof ported to \lssr is shown in \autoref{fig:lssr-mathlib}.
Here, the \code{@langle .. | ... | .. ⟩} pattern is similar to \code{[ .. | ...
| .. ]}, but instead of matching on the top element of the goal
stack, it applies the \code{constructor} tactic to the goal, and runs
nested tactics on the generated subgoals.
The main difference between those two proofs is that instead of the
somewhat awkward backward-style reasoning with explicitly constructed
proof terms (\eg, line 10 in \autoref{fig:mathlib}), \lssr allows for natural
forward-style proofs using \lssr views (\cf \autoref{sec:views}).
% In particular, comparing lines~7 in both proofs one can notes that
% the order of lemmas applications in \lssr is reversed compared to
% the original one.
Specifically, the mathlib proof of the second component of the
bi-implication from the conclusion (\ie, right-to-left) first
destructs the hypothesis \code{@ex i, ∃ (hi : i ∈ range n), f i _ = a},
and then gradually reduces the goal (\code{a ∈ s}) to the assumption
\code{hi : i ∈ range n} by first rewriting \code{eq}, then applying
\code{hf'} and finally \code{mem_range : n ∈ range m ↔ n < m}.
In contrast,the  \lssr proof adapts \code{hi} to solve the goal
automatically at line~8 of \autoref{fig:lssr-mathlib}, by first
applying \code{mem_range} to its second existential, then \code{hf'}
to the result, and then rewriting \code{eq} in it via the special form
of the view pattern \code{/[swap]}, followed by \code{->}.

\begin{figure}[t]
\centering
\begin{subfigure}{0.51\textwidth}
\begin{lstlisting}[basicstyle=\scriptsize\ttfamily,numbers=left,numberstyle=\tiny\color{ACMRed}]
(hf : ∀ a ∈ s, ∃ i (h : i < n), f i h = a)
(hf' : ∀ i (h : i < n), f i h ∈ s) :
∀ (a : α), a ∈ s ↔
∃ i, ∃ (hi : i ∈ range n), f i _ = a :=
fun a =>
⟨fun ha =>
let ⟨i, hi, eq⟩ := hf a ha
⟨i, mem_range.2 hi, eq⟩,
fun ⟨i, hi, eq⟩ => eq ▸ hf' i (mem_range.1 hi)⟩
\end{lstlisting}
\caption{Original mathlib proof script}
\label{fig:mathlib}
\end{subfigure}
\hspace{4mm}
\begin{subfigure}{0.44\textwidth}
\begin{lstlisting}[basicstyle=\scriptsize\ttfamily,numbers=left,numberstyle=\tiny\color{ACMRed}]
(hf: ∀ a ∈ s, ∃ i (h : i < n), f i h = a)
(hf' : ∀ i (h : i < n), f i h ∈ s) :
∀ (a : α), a ∈ s ↔
∃ i, ∃ (hi : i ∈ range n), f i _ = a :=
by move=> a
⟨/hf ![i /mem_range ? <-] // |
![i /mem_range /hf' /[swap]->] //⟩
\end{lstlisting}
\vspace{16pt}
\caption{\lssr proof script}
\label{fig:lssr-mathlib}
\end{subfigure}
\caption{Two proofs of the same fact from mathlib: the vanilla one and
the one in \lssr.}
\label{fig:lssr-vs-mathlib}
\end{figure}

We claim that the presented \lssr proof has certain advantages compared to
the one from mathlib.
First, views will automatically infer dependent arguments when
applying a lemma, \eg, \code{i} in \code{hf' i mem_range.1 hi} at
line~10 of \autoref{fig:mathlib}.
Second, \lssr organically incorporates last-mile automation (using
\code{//} and other automation patterns) to the forward-style proof
script, thus, sparing the user the effort of building yet another
collection of proof terms to dispatch the subgoals.
Finally, unlike the proof terms constructed holistically, \lssr proofs
are interactive: one can check the intermediate subgoals by simply
pointing to the specific location in the text buffer, resulting in a
better overall proof experience.
In summary, our experiment demonstrates that \lssr proofs are not only shorter
compared to the original mathlib ones, but also easier to follow
and debug.
The latter aspect is crucial for the long-term maintainability of large
formal Lean developments such as mathlib.

\section{Related Work and Conclusion}

% \todo{Enumerate some frameworks for tactic programming from the past.
%   The key message: Lean is better!}

% \begin{itemize}
% \item VeriML~\cite{StampoulisS10}
% \item Exploiting canonical structures~\cite{GonthierZND13,MahboubiT13}
% \item Mtac~\cite{ZilianiDKNV15} and MTac2~\cite{KaiserZKRD18}
% \item Ltac2~\cite{ltac2}
% \item Elpi~\cite{Tassi19,CohenST20}
% \item MetaCoq~\cite{SozeauABCFKMTW20}
% \end{itemize}

% \todo{Say what we consider porting and what next we'll do with Lean
%   metaprogramming. How about Iris proof
%   mode~[13]?}

% In this work, we implemented \lssr a tactic language for the Small
% Scale Reflection proof methodology in Lean~4.

Prior to our effort, Lean 4's metaprogramming facilities have been
used to implement white-box automation via proof search in the popular
Aesop package~[17].
In particular, mathlib~[19] uses Aesop to build
domain-specific solvers such as \code{measurability} and
\code{continuity}, and uses metaprogramming extensively to define its
own tactics and automation facilities (\eg, \code{split_ifs} and
\code{linarith}).
Closer in spirit to our work, K\"{o}nig developed a proof interface in
Lean in the stlye of Iris proof mode~[13],
featuring a specialised tactic language for proofs in Separation
In Lean~3, Limperg built an induction tactic that is friendlier for
novices by giving the most general induction

We believe that our implementation of \lssr provides an instructive
example of using Lean~4 metaprogramming features for implementing a
non-trivial tactic language, and adds one more arrow to the quiver of
tools and techniques for proof construction in Lean.

%% Acknowledgements:
%% * Kiran Gopinathan
%% * Yunjeong Lee

\begin{thebibliography}{10}

[1]
Reynald Affeldt and Cyril Cohen.
\newblock {Formal foundations of 3D geometry to model robot manipulators}.
\newblock In {\em CPP}, pages 30--42. {ACM}, 2017.
\newblock \href {https://doi.org/10.1145/3018610.3018629}

[2]
Reynald Affeldt and Cyril Cohen.
\newblock Measure construction by extension in dependent type theory with
application to integration.
\newblock {\em J. Autom. Reason.}, 67(3):28, 2023.
\newblock \href {https://doi.org/10.1007/S10817-023-09671-5}

[3]
Reynald Affeldt, Manabu Hagiwara, and Jonas S{\'{e}}nizergues.
\newblock {Formalization of Shannon's Theorems}.
\newblock {\em J. Autom. Reason.}, 53(1):63--103, 2014.
\newblock \href {https://doi.org/10.1007/S10817-013-9298-1}

[4]
Anne Baanen, Alexander Bentkamp, Jasmin Blanchette, Johannes Ho\"{o}lzl, and
Jannis Limperg.
\newblock {The Hitchhiker’s Guide to Logical Verification}, November 2023.
\newblock Available at
\url{https://lean-forward.github.io/hitchhikers-guide/2023}.

[5]
David~Thrane {Christiansen}.
\newblock {Functional Programming in Lean}, 2023.
\newblock Online book; available at
\url{https://lean-lang.org/functional_programming_in_lean/}.

[6]
{Coq Development Team}.
\newblock {The Coq Proof Assistant: Documentation (Books and long tutorials)},
March 2024.
\newblock Available at \url{https://coq.inria.fr/documentation}.

[7]
Leonardo de~Moura and Sebastian Ullrich.
\newblock {The Lean 4 Theorem Prover and Programming Language}.
\newblock In {\em CADE}, volume 12699 of {\em LNCS}, pages 625--635. Springer,
\newblock \href {https://doi.org/10.1007/978-3-030-79876-5\_37}

[8]
Vladimir Gladshtein, George P\^{i}rlea, and Ilya Sergey.
\newblock {LeanSSR: an SSReflect-Like Tactic Language for Lean (v1.0)}, March
\newblock An artefact accompanying the ITP'24 submission.
\newblock \href {https://doi.org/10.5281/zenodo.10836842}

[9]
Georges Gonthier.
\newblock {Formal Proof---The Four Color Theorem}.
\newblock {\em Notices of the AMS}, 55(11):1382--1393, 2008.

[10]
Georges Gonthier, Andrea Asperti, Jeremy Avigad, Yves Bertot, Cyril Cohen,
Fran{\c{c}}ois Garillot, St{\'{e}}phane~Le Roux, Assia Mahboubi, Russell
O'Connor, Sidi~Ould Biha, Ioana Pasca, Laurence Rideau, Alexey Solovyev,
Enrico Tassi, and Laurent Th{\'{e}}ry.
\newblock A machine-checked proof of the odd order theorem.
\newblock In {\em ITP}, volume 7998 of {\em LNCS}, pages 163--179. Springer,
\newblock \href {https://doi.org/10.1007/978-3-642-39634-2\_14}

[11]
Georges Gonthier, Assia Mahboubi, and Enrico Tassi.
\newblock {A Small Scale Reflection Extension for the Coq system}.
\newblock Technical Report 6455, Microsoft Research -- Inria Joint Centre,
\newblock \url{https://inria.hal.science/inria-00258384v16/document}.

[12]
Kiran Gopinathan and Ilya Sergey.
\newblock {Certifying Certainty and Uncertainty in Approximate Membership Query
\newblock In {\em CAV}, volume 12225 of {\em LNCS}, pages 279--303. Springer,
\newblock \href {https://doi.org/10.1007/978-3-030-53291-8\_16}

[13]
Robbert Krebbers, Jacques{-}Henri Jourdan, Ralf Jung, Joseph Tassarotti,
Jan{-}Oliver Kaiser, Amin Timany, Arthur Chargu{\'{e}}raud, and Derek Dreyer.
\newblock {MoSeL: a general, extensible modal framework for interactive proofs
in separation logic}.
\newblock {\em Proc. {ACM} Program. Lang.}, 2({ICFP}):77:1--77:30, 2018.
\newblock \href {https://doi.org/10.1145/3236772} {\path{doi:10.1145/3236772}}.

[14]
Lars König.
\newblock An {Improved} {Interface} for {Interactive} {Proofs} in {Separation}
\newblock Master's thesis, Karlsruhe Institute of Technology, September 2022.
\newblock URL:
\url{https://pp.ipd.kit.edu/uploads/publikationen/koenig22masterarbeit.pdf}.

[15]
Peter~J. Landin.
\newblock The next 700 programming languages.
\newblock {\em Commun. {ACM}}, 9(3):157--166, 1966.
\newblock \href {https://doi.org/10.1145/365230.365257}

[16]
Jannis Limperg.
\newblock {A novice-friendly induction tactic for Lean}.
\newblock In {\em CPP}, pages 199--211. ACM, 2021.
\newblock \href {https://doi.org/10.1145/3437992.3439928}

[17]
Jannis Limperg and Asta~Halkj\ae{}r From.
\newblock {Aesop: White-Box Best-First Proof Search for Lean}.
\newblock In {\em CPP}, pages 253--266. ACM, 2023.
\newblock \href {https://doi.org/10.1145/3573105.3575671}

[18]
Assia Mahboubi and Enrico Tassi.
\newblock {\em Mathematical Components}.
\newblock 2022.
\newblock \href {https://doi.org/10.5281/zenodo.7118596}

[19]
The {mathlib Community}.
\newblock {The Lean mathematical library}.
\newblock In {\em CPP}, pages 367--381. {ACM}, 2020.
\newblock \url{https://github.com/leanprover-community/mathlib4}.
\newblock \href {https://doi.org/10.1145/3372885.3373824}

[20]
Aleksandar Nanevski, Viktor Vafeiadis, and Josh Berdine.
\newblock {Structuring the Verification of Heap-Manipulating Programs}.
\newblock In {\em POPL}, pages 261--274, 2010.
\newblock \href {https://doi.org/10.1145/1706299.1706331}

[21]
Sam Owre, John~M. Rushby, and Natarajan Shankar.
\newblock {PVS:} {A} prototype verification system.
\newblock In Deepak Kapur, editor, {\em CADE}, volume 607 of {\em LNCS}, pages
748--752. Springer, 1992.
\newblock \href {https://doi.org/10.1007/3-540-55602-8\_217}

[22]
Arthur Paulino, Damiano Testa, Edward Ayers, Evgenia Karunus, Henrik Bövinga,
Jannis Limperg, Siddhartha Gadgil, and Siddharth Bhat.
\newblock {Metaprogramming in Lean 4}, 2024.
\newblock Available at
\url{https://leanprover-community.github.io/lean4-metaprogramming-book/}.

[23]
George P{\^{\i}}rlea and Ilya Sergey.
\newblock {Mechanising Blockchain Consensus}.
\newblock In {\em CPP}, pages 78--90. {ACM}, 2018.
\newblock \href {https://doi.org/10.1145/3167086} {\path{doi:10.1145/3167086}}.

[24]
Daniel Selsam, Sebastian Ullrich, and Leonardo de~Moura.
\newblock Tabled typeclass resolution.
\newblock {\em CoRR}, abs/2001.04301, 2020.
\newblock URL: \url{https://arxiv.org/abs/2001.04301}.

[25]
Ilya Sergey.
\newblock {Programs and Proofs: Mechanizing Mathematics with Dependent Types},
\newblock Lecture notes with exercises.
\newblock \href {https://doi.org/10.5281/zenodo.4996238}

[26]
Ilya Sergey, Aleksandar Nanevski, and Anindya Banerjee.
\newblock Mechanized verification of fine-grained concurrent programs.
\newblock In {\em PLDI}, pages 77--87. {ACM}, 2015.
\newblock \href {https://doi.org/10.1145/2737924.2737964}

[27]
Ilya Sergey, James~R. Wilcox, and Zachary Tatlock.
\newblock {Programming and Proving with Distributed Protocols}.
\newblock {\em Proc. {ACM} Program. Lang.}, 2({POPL}):28:1--28:30, 2018.
\newblock \href {https://doi.org/10.1145/3158116} {\path{doi:10.1145/3158116}}.

[28]
Natarajan Shankar, Sam Owre, John~M Rushby, and Dave~WJ Stringer-Calvert.
\newblock {PVS Prover Guide}.
\newblock Technical report, Computer Science Laboratory, SRI International,
Menlo Park, CA, August 2020.
\newblock Version 7.1.

[29]
Sebastian Ullrich and Leonardo de~Moura.
\newblock Beyond notations: Hygienic macro expansion for theorem proving
\newblock {\em Log. Methods Comput. Sci.}, 18(2), 2022.
\newblock \href {https://doi.org/10.46298/LMCS-18(2:1)2022}

[30]
Stephanie Weirich, Antoine Voizard, Pedro Henrique~Azevedo de~Amorim, and
Richard~A. Eisenberg.
\newblock {A specification for dependent types in Haskell}.
\newblock {\em Proc. {ACM} Program. Lang.}, 1({ICFP}):31:1--31:29, 2017.
\newblock \href {https://doi.org/10.1145/3110275} {\path{doi:10.1145/3110275}}.

\end{thebibliography}

\end{document}