Zulip Chat Archive

Stream: new members

Topic: simplifier


view this post on Zulip 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.

view this post on Zulip 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)
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.)

view this post on Zulip Greg Price (Apr 06 2021 at 19:53):

Very informative, thanks!

view this post on Zulip 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?

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Apr 08 2021 at 06:22):

The simplifier doesn't use e-matching

view this post on Zulip Mario Carneiro (Apr 08 2021 at 06:22):

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

view this post on Zulip 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.

view this post on Zulip 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.)

view this post on Zulip Horatiu Cheval (Apr 08 2021 at 07:07):

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

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Horatiu Cheval (Apr 08 2021 at 08:43):

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

view this post on Zulip Greg Price (Apr 09 2021 at 05:16):

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?

view this post on Zulip Mario Carneiro (Apr 09 2021 at 05:18):

yes, this is showing how matching modulo reducibles works


Last updated: May 14 2021 at 02:15 UTC