algorithmic documentation of simp

Stream: general

[Assia Mahboubi]

Hello, is there a place where I can read more about the algorithm(s) implemented by simp? For instance, I am interested in the specification of the matching strategy, for selecting subterms, and in the rewriting strategy. Thanks in advance!

[Johan Commelin]

I don't know about such descriptions of the algorithms. I think it's inspired by the Isabelle simplifier. Do you care about Lean 3 vs Lean 4? I think the simplifier changed.

I hope @Gabriel Ebner or @Mario Carneiro knows more. Maybe @Daniel Selsam also?

[Kyle Miller]

I'm no expert, but I've poked around the source code for Lean 3's simplifier. This is my understanding of how it works:

• When the simplifier is looking at an expression, it locates an applicable "congruence lemma." These come from either "user congruence lemmas" (those introduced by @[congr] for example) or from specialized congruence lemmas synthesized by simp. A congruence lemma is something like "if a = a' and b = b' then f a b = f a' b', which is applicable to expressions that unify with f a b with a and b metavariables.

• Given an applicable congruence lemma, the simplifier recursively turns the problem of simplifying f a b into the problem of simplifying a and b independently. If a simplifies to a' and b simplifies to b', then the congruence lemma is used to simplify f a b to f a' b'.

• After this, the simplifier looks for simplification lemmas (those introduced by @[simp] for example) that are applicable to f a b. The simplification lemmas are put into the form of a directed rules X --> Y, with conditions (for instance, "if x = 0 then x * y = 0" turns into the rule x * y --> 0 conditioned on x = 0), and it's looking to see if the current expression unifies with X. The simplifier tries to discharge the rule's conditions using the simplification procedure recursively, and if succeeds then the term is replaced with Y.

(The simplifier also has support for doing simplifications using general reflexive transitive relations, which can be triggered when congruence lemmas have hypotheses involving relations other than equality. I don't have a strong understanding for this feature, and there aren't too many examples of it.)

[Kyle Miller]

It's worth contrasting it with rw, which computes a "motive" for eq.rec to globally rewrite a term all at once. The simplifier instead sort of navigates into an expression using congruence lemmas.