simprocs

Stream: batteries

[Kim Morrison]

simprocs have landed in lean4:nightly-2024-01-10, and the adaptation PR for Std is at std4#496.

@Mario Carneiro and @Joe Hendrix, it would be great if this can be reviewed asap as there are corresponding PRs for aesop https://github.com/leanprover-community/aesop/pull/93 and #9500 waiting on it.

[Kevin Buzzard]

(deleted)

[Eric Rodriguez]

what's the vision for simprocs? The example given in the release note seems not that noteworthy.

[Kyle Miller]

@Eric Rodriguez They let you apply arbitrary kinds of transformations before or after descending into sub-terms. There are many more kinds of transformations you might want to do beyond just rewriting with lemmas.

[Kyle Miller]

It looks like core also has a couple extra examples: https://github.com/leanprover/lean4/blob/30693a2daefba3bb57432546bc5ef30669cf0a17/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Core.lean

These take if a then b else c, simplify a, see if it's True or False, and then reduce immediately to either b or c. That's an optimization you can't do with just simp lemmas.

[Mario Carneiro]

One simproc I have had in my back pocket for 4+ years is simplifying \forall x0 ... y ... xn, A1 -> ... -> y = e -> An -> B to \forall x0 ... xn, (A1 -> ... -> An -> B)[e/y]

[Mario Carneiro]

we have a few simple cases of this as simp lemmas but in general you need some logic to do it right

[Patrick Massot]

See also the classic https://github.com/leanprover/lean3/wiki/Simplifier-Features

[Yury G. Kudryashov]

Mario Carneiro said:

One simproc I have had in my back pocket for 4+ years is simplifying \forall x0 ... y ... xn, A1 -> ... -> y = e -> An -> B to \forall x0 ... xn, (A1 -> ... -> An -> B)[e/y]

Note that we'll need similar functions for ∃ with ∧ and iSup/iUnion/iInf/iInter.

[Yury G. Kudryashov]

(I guess, you know this better than me but let it be here in the chat history)