## Stream: new members

### Topic: simplifier

#### Greg Price (Apr 06 2021 at 19:17):

Is there a paper that describes the simplifier?

I recently read the ICFP paper https://leanprover.github.io/papers/tactic.pdf on the metaprogramming/tactic framework, and it was very informative. I'd love to read something similar about the simplifier.

#### Jeremy Avigad (Apr 06 2021 at 19:38):

Lean's simplifier is modeled after Isabelle's. You can read about Isabelle's simplifier here:
https://isabelle.in.tum.de/dist/Isabelle2021/doc/prog-prove.pdf (page 20)
https://isabelle.in.tum.de/dist/Isabelle2021/doc/tutorial.pdf (page 27, page 175)
Some of the issues that are specific to dependent type theory are described here:
https://leanprover.github.io/papers/congr.pdf
I hope that helps. (This is where my knowledge trails off.)

#### Greg Price (Apr 06 2021 at 19:53):

Very informative, thanks!

#### Eric Wieser (Apr 06 2021 at 20:05):

The discussion about safe_log in the congr paper is interesting. Do you know if there's anything else to read on the "e-matcher", or any lean examples demonstrating it?

#### Greg Price (Apr 08 2021 at 06:11):

An area I'd especially like to read more about is how the simplifier determines which simp lemmas have a LHS that matches the current expression.

IIUC that's where "e-matching" comes in. But I'm still working out what that means.

Are there papers people can recommend on e-matching as it's thought of in Lean?

#### Greg Price (Apr 08 2021 at 06:13):

One result I find from Google is a paper with Leo as an author, but that doesn't mention Lean:
http://leodemoura.github.io/files/ematching.pdf
because it's from 2007.

I'll certainly take a look at that but would be grateful if anyone knows of another helpful reference.

#### Mario Carneiro (Apr 08 2021 at 06:22):

The simplifier doesn't use e-matching

#### Mario Carneiro (Apr 08 2021 at 06:22):

The way the simplifier matches terms is just plain unification (modulo reducible definitions)

#### Greg Price (Apr 08 2021 at 06:43):

Ah OK, thanks!

Can you explain what "modulo reducible definitions" means? I've seen @[reducible] on definitions, but haven't quite put together what it means.

#### Mario Carneiro (Apr 08 2021 at 07:01):

It means that simp will unfold reducible definitions when they appear in the term to match, rather than attempting to find lemmas containing the reducible definition. (I think it does this with the simp lemmas themselves, so there won't be a mismatch even if both the goal and the lemma use the reducible definition.)

#### Horatiu Cheval (Apr 08 2021 at 07:07):

Does this mean that adding both @[reducible, simp] attributes to a definition is superfluous?

#### Mario Carneiro (Apr 08 2021 at 07:10):

No, you might still want to simp the definition away rather than just matching other lemmas modulo the definition

#### Mario Carneiro (Apr 08 2021 at 07:11):

(also I just tested it and I can't seem to get the matching modulo reducibles to work either)

#### Mario Carneiro (Apr 08 2021 at 07:13):

Since simp uses keyed matching, it will fail if the reducible definition is the head of the term to be matched:

-- abbreviation F (a b : ℕ) := a + b
@[reducible] def F (a b : ℕ) := a + b
theorem foo (a b : ℕ) : a + b = 0 := sorry
example (a b : ℕ) : F a b = 0 := by simp [foo] -- fails
theorem bar (a b : ℕ) : id (a + b) = 0 := sorry
example (a b : ℕ) : id (F a b) = 0 := by simp [bar] -- ok


#### Mario Carneiro (Apr 08 2021 at 07:18):

Here's a demonstration of the difference between @[reducible] and @[reducible, simp]:

def f := @id
@[reducible] def F (a b : ℕ) := a + b
@[simp] theorem bar (a : ℕ) : f (a + a) = 0 := sorry
example (a b : ℕ) : f (F a b) = 1 := by simp -- f (F a b) = 1
example (a b : ℕ) : f (F a a) = 1 := by simp -- 0 = 1
attribute [simp] F
example (a b : ℕ) : f (F a b) = 1 := by simp -- f (a + b) = 1


#### Mario Carneiro (Apr 08 2021 at 07:20):

Notice that in the first one, F was not unfolded, but in the second one it nevertheless was not an obstacle to matching the f (a + a) term against f (F a a). In the third one, since F is now @[simp], it is unfolded away in the goal

#### Horatiu Cheval (Apr 08 2021 at 08:43):

Ok, I get it, thank you for laying out all the different situations

#### Greg Price (Apr 09 2021 at 05:16):

Notice that in the first one, F was not unfolded, but in the second one it nevertheless was not an obstacle to matching the f (a + a) term against f (F a a).