feat: Simp, made simple #98

YaelDillies · 2025-04-15T19:28:38Z

This is the second part of #97.

Co-authored-by: Paul Lezeau [email protected]

posts/how-to-write-a-simproc.md

This PR adds the first blog post in a series of three to introduce the concept of simprocs and explain how to write them. The second blog post can be found here: #98 Co-authored-by : Yaël Dillies <[email protected]>

bryangingechen · 2025-05-26T21:06:45Z

Part 1 references this post, so maybe it can also be updated to have working links pointing here too.

Ruben-VandeVelde · 2025-05-30T19:40:44Z

posts/simp-made-simple.md

+```
+Note: The above snippet is a simplification and the constructors as shown actually belong to `Lean.TransformStep`, which `Lean.Meta.Simp.DStep` is an `abbrev` of.
+
+<span style="color:red">**(Yaël): Why is there a mismatch in docstrings between `Step.continue` and `DStep.continue`? [Zulip](https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/Simp.2EStep.2Econtinue.20vs.20Simp.2EDStep.2Econtinue/with/509056271)**</span>


Do you want to remove this?

Co-authored-by: Paul Lezeau <[email protected]>

Co-authored-by: Eric Wieser <[email protected]>

Co-authored-by: Bhavik Mehta <[email protected]>

edegeltje

thx for writing this

posts/simp-made-simple.md

Co-authored-by: blizzard_inc <[email protected]>

posts/simp-made-simple.md

jcommelin · 2025-06-19T08:38:27Z

posts/simp-made-simple.md

+```
+
+`simp` does not consume bare elements of type `Simproc`.
+Instead, a simproc is an element of type `Simproc` annotated with tbe extra data mentioned in the overview subsection, like whether the simproc is `pre` or `post`.


The section on Step is great, and contains a lot of detail. These latter sections seem somewhat rushed and the ending of the blogpost feels abrupt to me.
For example, this sentence about annotations with extra data... could that be accompanied by a code block that shows exactly what is going on?

And would it make sense to give the exact definition of the simpM monad, and add a bit more detail on it?

Maybe you could even end with a little cliff hanger about what will happen in the final blogpost?

Sounds good! I'm planning on spending some extra time adding stuff about SimpM to the post this coming month.

🏓 @Paul-Lez and @YaelDillies, it would be great to get this out! :-)

@kim-em this is now ready to review if you fancy taking a look;)
If you're very busy, I think the first part is probably more ready/polished than the second one!

posts/simp-made-simple.md

Co-authored-by: Yaël Dillies <[email protected]>

Co-authored-by: Johan Commelin <[email protected]>

Co-authored-by: Paul Lezeau <[email protected]>

Co-authored-by: Yaël Dillies <[email protected]>

Vierkantor · 2025-10-22T16:13:11Z

posts/simp-made-simple.md

+- `continue`. 
+  It turns out that both `Nat.reduceDvd` and `reduceIte` also use the `continue` constructor. 
+  Indeed, both these simprocs rely on the fact that some part of the expression 
+  considered is simplifiable (e.g. the condition in the `if` statement). 
+  When this is not the case, the `continue` constructor signals to `simp` that it should 
+  *not* attempt to simplify the expression again using the same simproc to prevent 
+  the simplification procedure from looping around.
+  More generally, `continue` is used in most simprocs as the "default" output
+  produced when the simproc was not able to make any simplification.


I don't completely understand this explanation, it seems like there are two things being mixed up here. Step indicates what to do when the simproc is done, right? But here "some part of the expression considered is simplifiable (e.g. the condition in the if statement)." refers to simplifying before the logic of the simproc itself. And then you describe when not to use .continue instead of when you do want to use it. Also because the .visit/.continue distinction is only relevant for pre-simprocs, which is mentioned above, but not here.

If we want to rework this completely, I would do something like: open the list with .continue since .continue none is the default. Then say something like:

... .continue indicates that the simproc is done with this expression and its subexpressions. As a result, simp will not not attempt to simplify the expression again using the same simproc to prevent the simplification procedure from looping around.

Vierkantor · 2025-10-22T16:17:03Z

posts/simp-made-simple.md

+
+In the case where the two expressions `e` and `e'` are definitionally equal,
+one can actually describe a simplification step using a simple structure,
+namely `DStep` (where the "d" stands for "definitional"). 


DSimprocs are mentioned only later on. So it is weird to discuss DStep here, it will make the reader wonder how they can return a DStep instead of a Step from a simproc.

Vierkantor · 2025-10-22T16:33:29Z

posts/simp-made-simple.md

+3) The second monad transformer application: `ReaderT Simp.Context $ StateRefT Simp.State MetaM`. 
+  The `SimpM` monad should also be able to access the "context" that `simp` is running in, e.g. which simp theorems it has access to and so on. This is captured by the type `Simp.Context`.
+  Here, the situation is not quite the same as when we were adding a `Simp.State` state to `MetaM`: while we will often want to change the state during the `simp` call, the context should always be the same (in programmer lingo: _immutable_)
+  Thus, we use a different monad transformer called `ReaderT`, which is almost identical to `StateT`, but outputs a new monad that can only read the type passed as parameter.


Mildly pedantic, but ReaderT can change the value in the calls it makes (e.g. ReaderT.adapt as equivalent to modify for a Reader). In programming language nerd terms, State(Ref)T gives you a global variable, and ReaderT gives you dynamic scoping.

(Does simp in practice use that though?)

Vierkantor

A few places where things are not clear to me, but you did mention everything I was expecting to see. Did not yet read it closely for style.

YaelDillies

The first 140 lines flow really well! Let's make sure this is also the case for the other 200 lines after that.

YaelDillies · 2025-11-08T21:30:05Z

posts/simp-made-simple.md

+2. Traverse subexpressions of `e` (note that the preprocedures might have changed `e` by this point);
+3. Run postprocedures on `e`.
+
+We call it the *simplification loop*.


Suggested change

We call it the *simplification loop*.

We call this the *simplification loop*.

YaelDillies · 2025-11-08T21:36:45Z

posts/simp-made-simple.md

+  Both `visit` and `done` signify success.
+
+Whenever a simproc is called on a given expression, it outputs a `Step`, which determines what will happen next during the `simp` call. 
+Since every simproc call is running a metaprogram to produce the output `Step`, the constructor that ends up used may vary according to the input. 


Suggested change

Since every simproc call is running a metaprogram to produce the output `Step`, the constructor that ends up used may vary according to the input.

Since every simproc call is running a metaprogram to produce the output `Step`, the constructor that ends being up used may vary according to the input.

Suggested change

Since every simproc call is running a metaprogram to produce the output `Step`, the constructor that ends up used may vary according to the input.

Since every simproc call is running a metaprogram to produce the output `Step`, the constructor that ends up being used may vary according to the input.

YaelDillies · 2025-11-08T21:40:08Z

posts/simp-made-simple.md

+
+Whenever a simproc is called on a given expression, it outputs a `Step`, which determines what will happen next during the `simp` call. 
+Since every simproc call is running a metaprogram to produce the output `Step`, the constructor that ends up used may vary according to the input. 
+For example, a given simproc may in some cases use `visit` and in others use `continue`.


This sentence is quite strange to me: it bases itself off the assumption that people expect that a simproc always uses the same Step constructor, but four lines above we explain how to use the constructors according to whether the simproc has failed or not. Could you repackage the info in a way that acknowledges the previous sentence?

YaelDillies · 2025-11-08T21:40:30Z

posts/simp-made-simple.md

+
+The constructors do the following: 
+- `continue` indicates that the simproc is done with this expression.
+  As a result, simp will not not attempt to simplify the expression again using the same simproc to prevent the simplification procedure from looping around.


Suggested change

As a result, simp will not not attempt to simplify the expression again using the same simproc to prevent the simplification procedure from looping around.

As a result, simp will not attempt to simplify the expression again using the same simproc to prevent the simplification procedure from looping.

YaelDillies · 2025-11-08T21:43:54Z

posts/simp-made-simple.md

+  Recall from the first post the simproc `Nat.reduceDvd`. 
+  This takes expressions of the form `a | b` where `a`, `b` are explicit natural numbers, and returns `True` or `False`. 
+  Either way, the output is in simp normal form, so there is no need to attempt to simplify it further. 
+  Thus, the simproc uses `done` to this result.


You already recalled on L.156

Suggested change

Recall from the first post the simproc `Nat.reduceDvd`.

This takes expressions of the form `a | b` where `a`, `b` are explicit natural numbers, and returns `True` or `False`.

Either way, the output is in simp normal form, so there is no need to attempt to simplify it further.

Thus, the simproc uses `done` to this result.

When `Nat.reduceDvd` is called on an expression of the form `a | b` where `a`, `b` are explicit natural numbers, it simplifies it to `True` or `False`.

Either way, the output is in simp normal form and there is no need to simplify it further.

Thus `Nat.reducedDvd` uses `done` in such a case.

YaelDillies · 2025-11-08T22:24:02Z

posts/simp-made-simple.md

+## Exploring the `SimpM` monad via simprocs
+
+In the next blog post, we will cover in detail how to implement simprocs that are useful for proving theorems in Lean. 
+In the meantime, to whet the reader's appetite, let's have a go at exploring the `SimpM` monad's internals using simprocs.


Suggested change

In the meantime, to whet the reader's appetite, let's have a go at exploring the `SimpM` monad's internals using simprocs.

In the meantime, to whet the reader's appetite, let's explore the internals of the `SimpM` monad using fake simprocs that print info instead of simplifying.

YaelDillies · 2025-11-08T22:24:24Z

posts/simp-made-simple.md

+In the next blog post, we will cover in detail how to implement simprocs that are useful for proving theorems in Lean. 
+In the meantime, to whet the reader's appetite, let's have a go at exploring the `SimpM` monad's internals using simprocs.
+
+> Throughout this section, all code will be assumed to have `open Lean Elab Meta Simp`.


Suggested change

> Throughout this section, all code will be assumed to have `open Lean Elab Meta Simp`.

> Throughout this section, all code is assumed to be prefaced with `open Lean Elab Meta Simp`.

YaelDillies · 2025-11-08T22:26:11Z

posts/simp-made-simple.md

+-- declare the simproc
+simproc_decl printExpr (_) := printExpressions
+```
+The last line is needed to "declare" the simproc officially - this is where we specify information like whether this is a pre/post procedure, and what expression we're matching on (here, we match on the pattern `_`, i.e. on everything!). 


Suggested change

The last line is needed to "declare" the simproc officially - this is where we specify information like whether this is a pre/post procedure, and what expression we're matching on (here, we match on the pattern `_`, i.e. on everything!).

The last line is needed to "declare" the simproc officially - this is where we can specify priority, whether this is a pre/post procedure and what expression we're matching on (here, we match on the pattern `_`, i.e. on everything!).

We didn't mention the pattern on L.46-47. Should we?

YaelDillies · 2025-11-08T22:27:03Z

posts/simp-made-simple.md

+The last line is needed to "declare" the simproc officially - this is where we specify information like whether this is a pre/post procedure, and what expression we're matching on (here, we match on the pattern `_`, i.e. on everything!). 
+More on this in the next post.
+
+Next, we could try an print out theorems that have used by `simp` "so far".


Suggested change

Next, we could try an print out theorems that have used by `simp` "so far".

Next, let's print out all the theorems that have been used by `simp` "so far".

YaelDillies · 2025-11-08T22:28:39Z

posts/simp-made-simple.md

+simproc_decl printThms (_) := printUsedTheorems
+```
+
+The reader can then call add these simprocs to simp calls to see what's happening within.


Suggested change

The reader can then call add these simprocs to simp calls to see what's happening within.

We encourage the reader to add these simprocs to their simp calls to see what's happening within.

eric-wieser reviewed Apr 15, 2025

View reviewed changes

posts/how-to-write-a-simproc.md Outdated Show resolved Hide resolved

eric-wieser reviewed Apr 15, 2025

View reviewed changes

posts/how-to-write-a-simproc.md Outdated Show resolved Hide resolved

Paul-Lez mentioned this pull request Apr 15, 2025

feat: Simprocs for the Working Mathematician #97

Merged

b-mehta reviewed Apr 15, 2025

View reviewed changes

eric-wieser reviewed Apr 15, 2025

View reviewed changes

posts/how-to-write-a-simproc.md Outdated Show resolved Hide resolved

posts/how-to-write-a-simproc.md Outdated Show resolved Hide resolved

posts/how-to-write-a-simproc.md Outdated Show resolved Hide resolved

YaelDillies force-pushed the how-to-write-a-simproc branch from 5ed721a to 2feca6c Compare April 16, 2025 10:30

b-mehta reviewed Apr 16, 2025

View reviewed changes

posts/how-to-write-a-simproc.md Outdated Show resolved Hide resolved

posts/how-to-write-a-simproc.md Outdated Show resolved Hide resolved

b-mehta reviewed Apr 16, 2025

View reviewed changes

posts/how-to-write-a-simproc.md Outdated Show resolved Hide resolved

posts/how-to-write-a-simproc.md Outdated Show resolved Hide resolved

posts/how-to-write-a-simproc.md Outdated Show resolved Hide resolved

b-mehta reviewed Apr 17, 2025

View reviewed changes

posts/how-to-write-a-simproc.md Outdated Show resolved Hide resolved

b-mehta reviewed Apr 17, 2025

View reviewed changes

posts/how-to-write-a-simproc.md Outdated Show resolved Hide resolved

Paul-Lez mentioned this pull request Apr 19, 2025

feat: Simproc series part III: A concrete intro to writing simprocs #100

Open

YaelDillies changed the title ~~feat: How to write a simproc~~ feat: Simp, made simple Apr 19, 2025

Ruben-VandeVelde reviewed May 30, 2025

View reviewed changes

YaelDillies force-pushed the how-to-write-a-simproc branch 2 times, most recently from ed3714e to 04f3d50 Compare June 3, 2025 17:52

YaelDillies and others added 13 commits June 8, 2025 15:05

feat: How to write a simproc

4488bd7

Co-authored-by: Paul Lezeau <[email protected]>

Update posts/how-to-write-a-simproc.md

9ea0b05

Co-authored-by: Eric Wieser <[email protected]>

Apply suggestions from code review

1464e92

Co-authored-by: Bhavik Mehta <[email protected]>

A few edits here and there

eccf13d

Rename revRangeInduct to revRange_succ_eq_of_revRange_eq

8380156

Use revRange_zero instead of rfl

49eb356

Mention toExpr

faad659

Use Simproc.ofQ

569159d

Use guard_target in the example

8f6c745

Render the code snippet working

c7822ed

to to

728b926

Co-authored-by: Bhavik Mehta <[email protected]>

Link to the docs

9001f17

Use Expr.nat?

5984b80

Update slugs, forward ref

f7aa206

YaelDillies force-pushed the how-to-write-a-simproc branch from 04f3d50 to f7aa206 Compare June 8, 2025 14:06

remove todo

b370b57

edegeltje reviewed Jun 11, 2025

View reviewed changes

posts/simp-made-simple.md Outdated Show resolved Hide resolved

whoops!

104322a

Co-authored-by: blizzard_inc <[email protected]>

jcommelin reviewed Jun 19, 2025

View reviewed changes

Paul-Lez added 2 commits July 12, 2025 22:46

WIP: draft additional content about the SimpM monad

8f5a7e6

WIP: add SimpM demo code section

93b4595

YaelDillies commented Jul 13, 2025

View reviewed changes

posts/simp-made-simple.md Outdated Show resolved Hide resolved

Paul-Lez and others added 12 commits July 13, 2025 10:12

WIP: more content about SimpM and general monadic stuff

05a02e4

Update posts/simp-made-simple.md

f445f86

Co-authored-by: Yaël Dillies <[email protected]>

Update posts/simp-made-simple.md

9f65391

Co-authored-by: Johan Commelin <[email protected]>

Add examples of the use of Simp.Step

06e4962

review overview

1255b98

A few edits here and there (more on their way)

a5e9898

Add extra stuff

0a263db

Co-authored-by: Paul Lezeau <[email protected]>

Bit more cleanup

2e329e1

Few more changes

0258aa5

reformulate

1bdf8c1

Linebreaks

52924e9

More edits

3ac5a4c

Co-authored-by: Yaël Dillies <[email protected]>

Paul-Lez force-pushed the how-to-write-a-simproc branch from 206fa34 to 3ac5a4c Compare September 10, 2025 18:17

Vierkantor reviewed Oct 22, 2025

View reviewed changes

fpvandoorn approved these changes Nov 6, 2025

View reviewed changes

Paul-Lez added 2 commits November 7, 2025 23:22

Apply review suggestions

abb72f9

A few small fixes

94d6b58

YaelDillies commented Nov 8, 2025

View reviewed changes

	We call it the simplification loop.
	We call this the simplification loop.

	Since every simproc call is running a metaprogram to produce the output `Step`, the constructor that ends up used may vary according to the input.
	Since every simproc call is running a metaprogram to produce the output `Step`, the constructor that ends being up used may vary according to the input.

	As a result, simp will not not attempt to simplify the expression again using the same simproc to prevent the simplification procedure from looping around.
	As a result, simp will not attempt to simplify the expression again using the same simproc to prevent the simplification procedure from looping.

	In the meantime, to whet the reader's appetite, let's have a go at exploring the `SimpM` monad's internals using simprocs.
	In the meantime, to whet the reader's appetite, let's explore the internals of the `SimpM` monad using fake simprocs that print info instead of simplifying.

	> Throughout this section, all code will be assumed to have `open Lean Elab Meta Simp`.
	> Throughout this section, all code is assumed to be prefaced with `open Lean Elab Meta Simp`.

	The last line is needed to "declare" the simproc officially - this is where we specify information like whether this is a pre/post procedure, and what expression we're matching on (here, we match on the pattern `_`, i.e. on everything!).
	The last line is needed to "declare" the simproc officially - this is where we can specify priority, whether this is a pre/post procedure and what expression we're matching on (here, we match on the pattern `_`, i.e. on everything!).

	Next, we could try an print out theorems that have used by `simp` "so far".
	Next, let's print out all the theorems that have been used by `simp` "so far".

	The reader can then call add these simprocs to simp calls to see what's happening within.
	We encourage the reader to add these simprocs to their simp calls to see what's happening within.

feat: Simp, made simple #98

Are you sure you want to change the base?

feat: Simp, made simple #98

Uh oh!

Conversation

YaelDillies commented Apr 15, 2025

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

bryangingechen commented May 26, 2025

Uh oh!

Choose a reason for hiding this comment

Uh oh!

edegeltje left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Vierkantor left a comment

Choose a reason for hiding this comment

Uh oh!

YaelDillies left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects