simplifier

Stream: new members

[Greg Price]

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]

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)
There is more information here:
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]

Very informative, thanks!

[Eric Wieser]

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]

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]

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]

The simplifier doesn't use e-matching

[Mario Carneiro]

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

[Greg Price]

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]

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]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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]

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]

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]

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

[Greg Price]

That's very helpful, thanks!

Mario Carneiro said:

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).

Do I understand right that this is a demo of getting the matching modulo reducibles to work? Or did you have something else in mind for what that meant?

[Mario Carneiro]

yes, this is showing how matching modulo reducibles works

[AnduinHS]

(deleted)