simproc についてのブログ記事第三弾：simproc 自作のイントロダクション

[Seasawher]

leanprover-community/blog#100

[Seasawher]

Part III

This is the final post in our simproce series. In our first two posts, we gave an informal introduction to the concept of a simproc, and a brief overview of the inner workings of the simp tactic. The aim of this final post is to use build on this by demonstrating how Lean users can write their own simprocs.

As for the previous post, we will assume that the reader has some exposure to metaprogramming in Lean.
In addition, some familiarity with the Qq library will be helpful, but not necessary for most of this post.
Then we explain the syntax and general structure of a simproc.
Finally, we walk through an explicit example of a simproc for a simple custom function.

The simproc syntax

Let's see how to declare a simproc.

The basic syntax for declaring a simproc is

simproc_decl mySimproc (theExprToMatch _ _) := fun e ↦ do
  write_simproc_here

See the next section for how to actually replace write_simproc_here by the correct meta code.
To add mySimproc to the standard simp set, replace simproc_decl by simproc:

simproc mySimproc (theExprToMatch _ _) := fun e ↦ do
  write_simproc_here

When calling a simproc in simp (if it is not in the standard simp set), one can specify that this is a preprocedure by adding ↓ in front of the simproc identifier: simp [↓mySimproc] (note that this also works when passing lemmas to simp!)

To add mySimproc to the standard simp set as a preprocedure (recall that postprocedure is the default), do

simproc ↓ mySimproc (theExprToMatch _ _) := fun e ↦ do
  write_simproc_here

Note that being a pre/postprocedure is a property of simprocs in a simp set, not of bare simprocs.
Therefore, there is no corresponding simproc_decl ↓ syntax.

Simproc walkthrough

Let's write a simproc for a simple recursive function.
We choose a custom function revRange, which to a natural number n returns the list of the first n natural numbers in decreasing order:

def revRange : Nat → List Nat
  | 0     => []
  | n + 1 => n :: revRange n
#eval revRange 5 -- [4, 3, 2, 1, 0]

Our goal will be to make simp evaluate revRange when its input is an explicit numeral, eg

example : revRange 0 = [] := by simp [???]
example : revRange 2 = [1, 0] := by simp [???]
example : revRange 5 = [4, 3, 2, 1, 0] := by simp [???]

Note two features of revRange that one should not expect from all functions that one might want to evaluate on explicit inputs:

• It is recursive: One can compute revRange n by recursion on n.
  Even more precisely, revRange n represents its own partial computation.
• revRange is definitionally equal to what we want to unfold it to.
  This has two consequences:
  • The two examples in the code snippet above can be proved by rfl, but of course doing so defeats the point of this blogpost.
  • We could actually write a dsimproc for revRange, which is to dsimp what a simproc is to simp.
    Implementation-wise, the main difference is that a dsimproc requires the new simplified expression to be definitionally equal to the previous one.

Let's now present three approaches to evaluating revRange on numerals:

• The baseline simproc-less approach which only uses lemmas and no simproc.
• The dsimproc approach, where we (possibly recursively) construct in the meta world the evaluated expression, but leave the proof to be rfl (here the "d" stands for "definitional equality").
• The simproc approach, where we (possibly recursively) construct the evaluated expression and the proof simultaneously.

The simproc-less approach

Before writing a simproc, let us first see how one could approach the computation of revRange using only lemmas.

revRange is a recursive function.
Therefore it can be evaluated on numerals simply by writing out the recurrence relations we wish to reduce along:

lemma revRange_zero : revRange 0 = [] := rfl
lemma revRange_succ (n : Nat) : revRange (n + 1) = n :: revRange n := rfl

Then we can complete our code snippet like so:

example : revRange 0 = [] := by simp [revRange_zero, revRange_succ]
example : revRange 2 = [1, 0] := by simp [revRange_zero, revRange_succ]
example : revRange 5 = [4, 3, 2, 1, 0] := by simp [revRange_zero, revRange_succ]

Note: Since revRange is defined by recursion, simp [revRange] would also be a valid proof here.
But we are trying not to rely on the definition of revRange.

Pros:

• Doesn't require writing any meta code.
• Doesn't require the recursion relations to be definitional (although they are in the case of revRange).

Cons:

• Requires adding two lemmas to your simp call instead of one (assuming we do not want these lemmas in the default simp set).
• Simplifying revRange n for a big input numeral n might involve a lot of simplification steps.
  In this specific case, the number of simplification steps is linear in n.
  Simplification steps matter because each of them increases the size of the proof term.
• revRange n could find itself (partially) evaluated even if n isn't a numeral.
  Eg simp [revRange_zero, revRange_succ] on ⊢ revRange (n + 3) = revRange (3 + n) will result in ⊢ n + 2 :: n + 1 :: n :: revRange n = revRange (3 + n).
  This is in general highly undesirable.

The definitional approach

In cases where the evaluation is definitionally equal to the original expression, one may write a dsimproc instead of a simproc.
The syntax to declare a dsimproc is rather to simprocs, with a small difference: we now need to return a DStep instead of a Step; in practice this amounts to providing the expression our program has produced without providing the proof (indeed, this is just rfl!)

TODO: We were explaining DStep before, but now it comes after.

To compute revRange using the dsimproc approach, we can do the following:

dsimproc_decl revRangeCompute (revRange _) := fun e => do
  -- Extract the natural number from the expression
  let_expr revRange m ← e | return .continue
  -- Recover the natural number as a term of type `Nat`
  let some n := m.nat? | return .continue
  let l := revRange n
  -- Convert the list to an `Expr`
  return .visit <| Lean.toExpr l

For a bit more on dsimprocs, see the extras below.

Pros:

• Requires writing a single simproc.
• Assuming the type of the expression to be evaluated implements ToExpr, there is no need to reevaluate the expression manually in the meta world.

Cons:

• The function needs to be computable to be evaluated automatically in the meta world.
• The produced rfl proof could be heavy.
• Only works when the evaluation and conversion back to an expression is definitionally equal to the original expression.

The propositional approach

A more general approach would be to manually construct the proof term we need to provide.
In our case, we can do this in a recursive manner.

open Qq
private theorem revRange_succ_eq_of_revRange_eq {n : ℕ} {l : List ℕ}
    (hl : revRange n = l) : revRange (n+1) = n :: l := by
  induction n with
  | zero => aesop
  | succ n h => rw [←hl]; rfl
open Qq in
simproc_decl revRangeComputeProp (revRange _) := fun e => do
  let_expr revRange m ← e | return .continue
  let some n ← Nat.fromExpr? m | return .continue
  let rec go (n : ℕ) : (l : Q(List ℕ)) × Q(revRange $n = $l) :=
    match n with
    | 0 => ⟨q(([] : List ℕ)), q(revRange_zero)⟩
    | n + 1 =>
      let ⟨l, pf⟩ := go n
      ⟨q($n :: $l), q(revRange_succ_eq_of_revRange_eq $pf)⟩
  let ⟨l, pf⟩ := go n
  return .visit { expr := l, proof? := pf }

Pros:

• Works regardless of definitional equalities.
  See Nat.reduceDvd introduced in the previous blog post for another compelling example:
  a ∣ b is not defined as a % b = 0, yet the Nat.reduceDvd simproc can decide a ∣ b by computing a % b = 0.

Cons:

• Might involve a fair bit of meta code, a lot of which could feel like evaluating the function.
• Simplifying revRange n for a big input numeral n might produce a large proof term.
  In this specific case, the size of the produced proof term will be linear in n.

Extras

How to discharge subgoals

Often, when applying a theorem, we may need to provide additional proof terms for the hypotheses of the result. One useful feature of
simprocs is that we can also call the discharger tactic provided to simp. Which discharger was provided by the user is part of the state stored by the SimpM monad, and can be access by the user via Methods (roughly speaking, the part of the state that encodes which methods simp can use to simplify an expression). Methods implements a function discharge? : Expr → Option Expr such that discharge? goal is equal to some pf if the discharger found a proof pf of goal, and none otherwise. Finally, to access the current "state" of Methods, one can use getMethods.

In the following example, we implement a simproc for Nat.factorization that simplifies expressions of the form (a * b).factorization to a.factorization + b.factorization whenever a proof that a and b are both non-zero can be found by the discharger.

import Mathlib
open Qq Lean.Meta.Simp
simproc_decl factorizationMul (Nat.factorization (_ * _)) := .ofQ fun u α e => do
  match u, α, e with
  | 1, ~q(ℕ →₀ ℕ), ~q(Nat.factorization ($a * $b)) =>
    -- Try to discharge the goal `a ≠ 0`
    let some ha ← ((← getMethods).discharge? q($a ≠ 0)) | return .continue
    --Convert the resulting proof to a `Qq` expression for convenience (see #23510)
    let ⟨0, ~q($a ≠ 0), ~q($ha)⟩ ← inferTypeQ ha | return .continue
    -- Try to discharge the goal `b ≠ 0`
    let some hb ← ((← getMethods).discharge? q($b ≠ 0)) | return .continue
    --Convert the resulting proof to a `Qq` expression for convenience
    let ⟨0, ~q($b ≠ 0), ~q($hb)⟩ ← inferTypeQ hb | return .continue
    let e' := q((Nat.factorization $a) + (Nat.factorization $b))
    let pf := q(Nat.factorization_mul $ha $hb)
    return .visit { expr := e', proof? := pf }
  | _, _, _ => return .continue
set_option trace.Meta.Tactic.simp true in
example : Nat.factorization (2 * 3) = fun₀ | 2 => 1 | 3 => 1 := by
  simp (disch := decide) only [factorizationMul]
  guard_target = Nat.factorization 2 + Nat.factorization 3 = fun₀ | 2 => 1 | 3 => 1
  sorry

How to match on numerals

Often when writing a simproc to perform a computation, it can be useful to extract quantities from the expression we are manipulating. The easiest case is perhaps that of Nat litterals. Given a numeral by e : Expr, there are various ways of recovering the corresponding term of type Nat:

• Lean.Expr.rawNatLit?.
• Lean.Expr.natLit!
• Lean.Expr.nat?
• Nat.fromExpr?

TODO(Paul): Let's explain the differences, and show some examples of where behaviour differs.

How to handle a non-recursive definition

Write a type of partial computations that is recursive.

TODO(Paul)

[Seasawher]

Part II

This is the second blog post in a series of three.
In the first blog post, we introduced the notion of a simproc, which can be thought of as a form of "modular" simp lemma.
In this sequel, we give a more detailed exposition of the inner workings of the simp tactic in preparation of our third post, where we will see how one can go about creating new simprocs.

Throughout this post, we will assume that the reader has at least a little exposure to some of the core concepts that underpin metaprogramming in Lean, e.g. Expr and the MetaM monad (for those that don't, the book Metaprogramming in Lean 4 is a great introduction to the topic)

First, we detail the inner workings of simp relevant to simprocs.

How simp works

In this section we present some of the inner workings of simp.

First we give an overview of the way simp works, then we delve into the specifics by introducing:

• The SimpM monad, which is the metaprogramming monad holding the information relevant to a simp call.
• Step, the Lean representation of a single simplification step.
• Simproc, the Lean representation of simprocs.

All the simp-specific declarations introduced in this section are in the Lean.Meta or Lean.Meta.Simp namespace.

Overview

When calling simp in a proof, we give it a simp context.
This is made of a few different things, but for our purposes think of it as the set of lemmas/simprocs simp is allowed to rewrite with, namely the default simp lemmas/simprocs plus the lemmas/simprocs added explicitly minus the lemmas/simprocs removed explicitly.
For example, simp [foo, -bar] means "Simplify using the standard simp lemmas/simprocs except bar, with foo added".

A perhaps surprising fact is that every simp lemma is internally turned into a simproc for simp's consumption.
From then on, we will refer to simp lemmas/simprocs as procedures.

Each procedure in a simp context comes annotated with extra data, such as priority.

The only such piece of data we explain in depth is the stage at which the procedure should be called:

• Postprocedures are called on an expression e after subexpressions of e are simplified.
  Procedures are by default postprocedures as oftentimes a procedure can only trigger after the inner expressions have been simplified.
• Preprocedures are called on an expression e before subexpressions of e are simplified.
  Preprocedures are mostly used when the simplification order induced by a postprocedure would otherwise be inefficient by visiting irrelevant subexpressions first.
  Preprocedures are associated with the ↓ symbol in several syntaxes throughout the simp codebase.

The general rule of thumb is that postprocedures simplify from the inside-out, while preprocedures simplify from the outside-in.

Roughly speaking, when traversing an expression e, simp does the following in order:

1. Run preprocedures on e;
2. Traverse subexpressions of e (note that the preprocedures might have changed e by this point);
3. Run postprocedures on e.

This is called the simplification loop.

The above loop is merely an approximation of the true simplification loop:
Each procedure actually gets to decide whether to go to step 1 or 3 after it was triggered.
See the continue and visit constructors of the Step inductive type as described in the next section for full details.

Step

Step is the type that represents a single step in the simplification loop.
At any given point, we can do three things:

1. Simplify an expression e to a new expression e' and stop there (i.e. don't visit any subexpressions in the case of a preprocedure)
2. Simplify an expression e to a new expression e' and continuing the process at e' (i.e. e' may be simplified further), before moving to subexpressions if this is a preprocedure.
3. Simplify an expression e to a new expression e' and continue the process on subexpressions of e' (if this is a preprocedure).

Note that the 2 and 3 are the same for post procedures.

Let's now look at this more formally.
To begin, simp has a custom structure to describe the result of a procedure called Result:

structure Result where
  expr   : Expr
  proof? : Option Expr := none
  cache  : Bool := true

This is used as follows: if a procedure simplified an expression e to a new expression e' and p is a proof that e = e' then we capture this by ⟨e', p⟩ : Result.
If e and e' are definitionally equal, one can in fact omit the proof? term.

The type Step has three constructors, which correspond to the three types of actions outlined above:

inductive Step where
  /--
  For `pre` procedures, it returns the result without visiting any subexpressions.

  For `post` procedures, it returns the result.
  -/
  | done (r : Result)
  /--
  For `pre` procedures, the resulting expression is passed to `pre` again.

  For `post` procedures, the resulting expression is passed to `pre` again IF
  `Simp.Config.singlePass := false` and resulting expression is not equal to initial expression.
  -/
  | visit (e : Result)
  /--
  For `pre` procedures, continue transformation by visiting subexpressions, and then
  executing `post` procedures.

  For `post` procedures, this is equivalent to returning `visit`.
  -/
  | continue (e? : Option Result := none)

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"). This is obtained by replacing each occurrence of Result in the definition of Step by Expr (intuitively, we no longer need to specify a proof that e and e' are equal since this is just rfl, so we only need to return the simplified expression e'):

inductive DStep where
  /-- Return expression without visiting any subexpressions. -/
  | done (e : Expr)
  /--
  Visit expression (which should be different from current expression) instead.
  The new expression `e` is passed to `pre` again.
  -/
  | visit (e : Expr)
  /--
  Continue transformation with the given expression (defaults to current expression).
  For `pre`, this means visiting the children of the expression.

  For `post`, this is equivalent to returning `done`. -/
  | continue (e? : Option Expr := none)
  deriving Inhabited, Repr

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.

The SimpM monad

SimpM is the monad that tracks the current context simp is running in (what simp theorems are available, etc) and what has been done so far (e.g. number of steps so far, theorems used).
In particular this also captures the MetaM context.

Simprocs

A simproc takes in an expression and outputs a simplification step, possibly after modifying the current simp state (e.g. by adding new goals to be closed by the discharger).
This behavior is formally encapsulated by the Simproc type:

abbrev Simproc  := Expr → SimpM  Step

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.

Similarly, there is a DSimproc type:

abbrev DSimproc := Expr → SimpM DStep

[Seasawher]

Part 1

Lean v4.6.0 (back in February 2024!) added support for custom simplification procedures, aka simprocs.
This blog post is the first in a series of two aimed at explaining what a simproc is, what kind of problems can be solved with simprocs, and what tools we have to write them.

This post describes purely informally what simprocs are and do.
The second post will be a walkthrough to writing a simple simproc in three different ways.

To understand what a simproc is and how it works, we will first explain how simp works.
Then we will give some examples and non-examples of simprocs.

How simp works

simp is made of two components.

The first component is rewriting rules.
A rewriting rule has a left hand side (either an expression or an expression pattern), which simp will use to decide when to use the rewriting rule, and a right hand side, which will be computed from the left hand side and must be equal to it as a mathematical object.
Most rewriting rules are lemmas tagged with @[simp] that are of the form LHS = RHS or LHS ↔ RHS (lemmas that prove P which is not of the form _ = _ or _ ↔ _ are turned into P = True), but we will soon see less straightforward examples.

The second one is the simp tactic, which we will refer to simply as simp.
When run on a goal ⊢ e, simp iteratively looks for a subexpression of e that matches the left hand side of some rewriting rule, and replaces that subexpression with the right hand side of that rule.

For example, here's the proof steps simp follows to close the goal 37 * (Nat.fib 0 + 0) = 0

⊢ 37 * (Nat.fib 0 + 0) = 0
⊢ 37 * (0 + 0) = 0
⊢ 37 * 0 = 0
⊢ 0 = 0
⊢ True

The order in which simp traverses an expression is relatively intricate.
As a simple approximation, simplification is performed from the inside-out.
See the next blog post for more details on the algorithm.
If you write set_option trace.Meta.Tactic.simp true in example : MyGoal := by simp, you will see the list of simplification steps simp performs on MyGoal.

What is a simproc?

In the previous section, we explained how simp uses rewriting rules of the form LHS = RHS or LHS ↔ RHS to simplify expressions.
Let's now talk about the rewriting rules that are not of this form, aka simprocs.

A simproc is a rewriting rule which, given an expression LHS matching its left hand side, computes a simpler expression RHS and constructs a proof of LHS = RHS on the fly.

The concept of a simproc is genuinely more powerful than that of a simp lemma.
Indeed, we will soon see an example of a simproc taking the place of infinitely many simp lemmas.

Examples of simprocs

In this section, we exemplify four simprocs that cover the following use cases:

• Avoiding combinatorial explosion of lemmas
• Computation
• Performance optimisation

Avoiding combinatorial explosion of lemmas: The existsAndEq simproc

The existsAndEq simproc is designed to simplify expressions of the form ∃ x, ... ∧ x = a ∧ ... where a is some quantity independent of x by removing the existential quantifier and replacing all occurences of x by a.

example (p : Nat → Prop) : ∃ x : Nat, p x ∧ x = 5 := by
  simp only [existsAndEq]
  -- Remaining goal: `⊢ p 5`
example (p q : Nat → Prop) : ∃ x : Nat, p x ∧ x = 5 ∧ q x := by
  simp only [existsAndEq]
  -- Remaining goal: `⊢ p 5 ∧ q 5`

To give simp this functionality without a simproc, one would have to write infinitely many simp lemmas.
Indeed, the equality x = a could be hidden arbitrarily deep inside the ∧.

Technically, one could implement this functionality using finitely many lemmas:
and_assoc to left-associate all the ∧, and_left_comm (b := _ = _) to move the = left-ward, exists_eq_left to eliminate the = when it reaches the ∃.
This is not useful in practice since it could possibly loop (e.g. if there are two =, they could be commuted forever) and modifies the expression in unwanted ways, such as reassociating all the ∧, even those outside an ∃.
When presented with a left hand side of the form ∃ x, P x, where P x is of the form _ ∧ ... ∧ _, existsAndEq does the following:

• Recursively traverse P x inside the existential quantifier looking for an equality x = a for some a.
• If an equality is found, construct a proof that ∀ x, p x → x = a.
• Return the right hand side P a together with the proof obtained from the following lemma:

  lemma exists_of_imp_eq {α : Sort u} {p : α → Prop} (a : α) (h : ∀ x, p x → x = a) :
      (∃ x, p x) = p a

Computation

Computations are an integral part of theorem proving, and as such there are many ways to perform them.
For example, you will find that the decide tactic closes most of the examples in this subsection.
There are a few reasons why simprocs are interesting for computation regardless:

• decide relies on decidability instances.
  Not everything one may want to compute is decidable, and not every decidability instance is efficient.
  In fact, most Decidable instances in Lean and Mathlib are very generic, and therefore unspecific and inefficient.
  Using a simproc gives the opportunity to use a domain-specific algorithm, which is more likely to be efficient and does not rely on the decidability machinery.
• decide cannot compute the right hand side, given the left hand side only.
  decide only works on goals that do not contain any metavariables or free variables.
  This rules out using decide to find out what a left hand side is equal to.
  One would need to write down the right hand side we are looking for in order for decide to show that it's equal to the left hand side.
  In particular, using a simproc means we can perform a computation and then continue to simplify the resulting expression within a single simp call.

The Nat.reduceDvd simproc

The Nat.reduceDvd simproc is designed to take expressions of the form a | b where a, b are numerals (i.e. actual numbers, like 0, 1, 37, as opposed to variables or expressions thereof), and simplify them to True or False.

example : 3 ∣ 9 := by
  simp only [Nat.reduceDvd]
-- `decide` cannot close this goal.
example (f : Prop → Prop) : f (2 ∣ 4) = f True := by
  simp only [Nat.reduceDvd]
example : ¬ 2 ∣ 49 := by
  simp only [Nat.reduceDvd]
  -- Remaining goal: `¬ False`
  simp
example (a b : Nat) : a ∣ a * b := by
  simp only [Nat.reduceDvd] --fails

To reiterate one of the points made earlier, this simproc is useful despite doing something that decide can already do, as it allows the simp tactic to get rid of certain expressions of the form a ∣ b, and then simplify the resulting goal (or hypothesis) further.

When presented with a left hand side of the form a ∣ b where a and b are natural numbers, Nat.reduceDvd does the following:

• Check that a and b are numerals.
• Compute b % a.
• If b % a is zero, then return the right hand side True together with the proof Nat.dvd_eq_true_of_mod_eq_zero a b rfl that (b % a = 0) = True.
• If b % a isn't zero, then return the right hand side False together with the proof Nat.dvd_eq_false_of_mod_ne_zero a b rfl that (b % a = 0) = False.

The Finset.Icc_ofNat_ofNat simproc

If a and b are in a (locally finite) partial order (if you don't know what this means, you can safely ignore these terms and think of the natural numbers instead), then Finset.Icc a b for a and b is the finite set of elements lying between a and b.

The Finset.Icc_ofNat_ofNat simproc is designed to take expressions of the form Finset.Icc a b where a and b are numerals, and simplify them to an explicit set.

example : Finset.Icc 1 0 = ∅ := by
  simp only [Icc_ofNat_ofNat]
example : Finset.Icc 1 1 = {1} := by
  simp only [Icc_ofNat_ofNat]
example : Finset.Icc 1 4 = {1, 2, 3, 4} := by
  simp only [Icc_ofNat_ofNat]
example (a : Nat) : Finset.Icc a (a + 2) = {a, a + 1, a + 2} := by
  -- fails: the bounds of the interval aren't numerals!
  simp only [Icc_ofNat_ofNat]

When presented with a left hand side of the form Finset.Icc a b where a and b are natural numbers, Finset.Icc_ofNat_ofNat does the following:

• Check that a and b are numerals.
• compute the expression {a, ..., b} recursively on b, along with the proof that it equals Finset.Icc a b.

Performance optimisation: The reduceIte simproc

The reduceIte simproc is designed to take expressions of the form if P then a else b (aka ite P a b) and replace them with a or b, depending on whether P simplifies to True or False.

This can be achieved with simp lemmas too, but it would be less efficient:
When encountering ite P a b, simp lemmas would first simplify b, then a, then P, and finally ite P a b.
Assuming P was simplified to True, ite P a b would be simplified to a and all the work spent on simplifying b would be lost.
If P was simplified to False, then the work spent on simplifying a would be lost instead.

The point of reduceIte is that it can be made to simplify P, then ite P a b, without simplifying a and b first.
For this to happen, one needs to call reduceIte as a preprocedure, which is done by adding ↓ in front of its name, i.e. simp only [↓reduceIte].

Recall that, as a simple approximation, simplification is performed from the inside-out.
What we just explained is a concrete example of simplification happening from the outside-in.
Let's see a few examples:

example : (if 37 * 0 = 0 then 1 else 2) = 1 := by
  -- Works since `simp` can simplify `37 * 0 = 0` to `True`
  -- because it knows the lemma `mul_zero a : a * 0 = 0`.
  simp only [↓reduceIte]
example (P : Prop) (a b : Nat) : (if P ∨ ¬ P then a else b) = a := by
  -- Works since `simp` can simplify `P ∨ ¬ P` to `True`.
  simp only [↓reduceIte]
open scoped Classical in -- Can be removed once Kevin Buzzard is done with the FLT project ;)
example : (if FermatLastTheorem then 1 else 2) = 1 := by
  --This fails because `simp` can't simplify `FermatLastTheorem` to `True` or `False`
  simp only [↓reduceIte]
  -- Remaining goal: `⊢ (if FermatLastTheorem then 1 else 2) = 1`
  sorry -- See https://imperialcollegelondon.github.io/FLT for how to solve this `sorry` ;)

When presented with a left hand side of the form ite P a b, reduceIte does the following:

• Call simp on P to get a simplified expression P' and a proof h that P = P'.
• If P' is True then return the right hand side a together with the proof ite_cond_eq_true r that ite P a b = a.
• If P' is False then return the right hand side b together with the proof ite_cond_eq_false r that ite P a b = b.

Many more applications!

In the second blog post, we will see how to build step by step a simproc for computing a variant of List.range when the parameter is a numeral.

A few caveats

The current design of simprocs comes with a few restrictions that are worth keeping in mind:

• By definition, a simproc can only be used in simp (and tactics that call simp under the hood, such as simp_rw, simpa, aesop, norm_num, etc...), even though the notion of a "modular lemma" could be useful in other rewriting tactics like rw.
• One cannot provide arguments to a simproc to restrict the occurrences it rewrites.
  In contrast, this is possible for lemmas in all rewriting tactics: e.g. rw [add_comm c] turns ⊢ a + b = c + d into ⊢ a + b = d + c where rw [add_comm] would instead have turned it into ⊢ b + a = c + d.