feat: add `simp` configuration option `Simp.Config.instances` #3151

leodemoura · 2024-01-09T00:18:08Z

Depends on #3124

Mathlib adaptation PR is at leanprover-community/mathlib4#9572

…duced

The new test exposes a performance problem found in software verification applications.

See new test for example that takes exponential time without new simp theorems. TODO: replace auxiliary theorems with simprocs as soon as we implement them.

The example was looping with the new `simp` reduction strategy. Here is the looping trace. ``` List.reverseAux (List.reverseAux as []) bs ==> rewrite using reverseAux_reverseAux List.reverseAux [] (List.reverseAux (List.reverseAux as []) bs) ==> unfold reverseAux List.reverseAux (List.reverseAux as []) bs ==> rewrite using reverseAux_reverseAux List.reverseAux [] (List.reverseAux (List.reverseAux as []) bs) ==> ... ```

Motivations: - We can simplify the big mutual recursion and the implementation. - We can implement the support for `match`-expressions in the `pre` method. - It is easier to define and simplify `Simprocs`.

TODO: - `builtin_simproc` attribute - more tests

Allow `simproc`s to be declared without setting the `[simproc]` attribute. A `simproc` declaration is function + pattern. Motivation: allow them to be provided as arguments to `simp` **and** `simp only`. TODO: track their use in `simp`. TODO: builtin simprocs

`Origin.decl` constructor has an extra field.

It is true by default. Packages can set it to false to disable simplification procedue support for backward compatibility.

We can now disable `simproc`s using the same notation we use to disable rewriting rules in the simplifier.

Motivation: better `simp` cache behavior. Recall that `simp` cache uses `dischargeDepth`.

…nment

When `instances := false`, instance implicit arguments are not visited during `simp`. `Std` does not seem affected by this change.

leodemoura · 2024-01-09T00:19:04Z

!bench

leanprover-community-mathlib4-bot · 2024-01-09T00:39:24Z

❗ Mathlib CI can not be attempted yet, as the 'nightly-testing-2024-01-06' branch does not exist there yet. We will retry when you push more commits. It may be necessary to rebase onto 'nightly' tomorrow. (2024-01-09 00:39:23)
💥 Mathlib branch lean-pr-testing-3151 build failed against this PR. (2024-01-09 02:15:34) View Log
💥 Mathlib branch lean-pr-testing-3151 build failed against this PR. (2024-01-09 04:59:06) View Log
🟡 Mathlib branch lean-pr-testing-3151 build against this PR was cancelled. (2024-01-09 06:22:08) View Log
✅ Mathlib branch lean-pr-testing-3151 has successfully built against this PR. (2024-01-09 07:25:47) View Log
✅ Mathlib branch lean-pr-testing-3151 has successfully built against this PR. (2024-01-09 11:34:16) View Log
✅ Mathlib branch lean-pr-testing-3151 has successfully built against this PR. (2024-01-09 12:00:53) View Log

leanprover-bot · 2024-01-09T00:53:59Z

Here are the benchmark results for commit 9be86b5.
There were significant changes against commit 9034937:

  Benchmark                  Metric             Change
  ===============================================================
- import Lean                branches             1.8%  (105.8 σ)
- import Lean                instructions         1.8%  (136.9 σ)
- import Lean                maxrss               1.5%   (53.7 σ)
- lake startup               instructions         1.5%   (54.6 σ)
- libleanshared.so           binary size          2.0%
- reduceMatch                maxrss               1.3%  (101.8 σ)
- stdlib                     instructions         1.4% (1184.2 σ)
- stdlib                     wall-clock           1.6%   (18.8 σ)
- stdlib size                bytes .olean         1.4%
- stdlib size                lines C              2.5%
- tests/bench/ interpreted   maxrss               1.3%   (56.7 σ)
- tests/compiler             sum binary sizes     1.9%
- workspaceSymbols           instructions         2.2% (3266.8 σ)
- workspaceSymbols           maxrss               1.5%   (88.3 σ)

kim-em · 2024-01-09T03:12:45Z

~~This does cause a variety of Mathlib failures. Can we start out with this defaulting to true?~~

Maybe it's not so bad. I think we could proceed with this.

kim-em · 2024-01-09T06:33:38Z

I've created a discussion on zulip to forewarn users about this, and to discuss impact.

kim-em · 2024-04-22T00:04:18Z

This PR was superseded by #3507.

leodemoura added 30 commits January 7, 2024 10:05

perf: (try to) fix regression introduced by #3139

2ea2ef5

feat: add reduceStep, and try pre simp steps again if term was re…

7e2f93b

…duced

feat: add Expr.getAppPrefix

979a315

feat: add Expr.getAppArgsN

d2a40c8

feat: better support for match-application in the simplifier

cac7160

The new test exposes a performance problem found in software verification applications.

feat: add pre simp lemmas for if-then-else terms

81d4336

See new test for example that takes exponential time without new simp theorems. TODO: replace auxiliary theorems with simprocs as soon as we implement them.

refactor: use unsafe code to break recursion in simp implementation

7b2dc2a

Motivations: - We can simplify the big mutual recursion and the implementation. - We can implement the support for `match`-expressions in the `pre` method. - It is easier to define and simplify `Simprocs`.

chore: simplify mutual at simpImpl

0041d4d

refactor: simplify match-expressions at pre simp method

102928b

refactor: simplify simpImpl

8aac0fe

chore: address feedback

0055018

feat: add simprocs

312b8eb

TODO: - `builtin_simproc` attribute - more tests

feat: simp only should not use default simproc set

9f09264

feat: allow extra simprocs to be provided as simp arguments

6e9ea19

fix: simp.trace missing pre annotation

dc1d2c8

chore: update stage0

f7f73de

`Origin.decl` constructor has an extra field.

chore: fix test

88a0bbc

feat: add option simprocs

f275cce

It is true by default. Packages can set it to false to disable simplification procedue support for backward compatibility.

feat: trace simprocs

ea231ef

feat: add simp option - <simproc-name>

33bc436

We can now disable `simproc`s using the same notation we use to disable rewriting rules in the simplifier.

chore: missing copyright

04ce796

feat: add builtin simproc support

1f103b7

chore: update stage0

d86771b

feat: add basic simprocs for Nat

dd7e6e3

chore: remove bogus registerSimproc

a1d438c

chore: update stage0

4e6ec09

feat: add simprocs for Fin

e2c49b4

feat: replace ite and dite shortcircuit theorems with simproc

c2cbef1

Motivation: better `simp` cache behavior. Recall that `simp` cache uses `dischargeDepth`.

leodemoura and others added 13 commits January 8, 2024 13:51

chore: fix tests

b57fdc0

fix: trace used builtin simprocs even if they are not in the enviro…

789979e

…nment

chore: add another simproc test

9c16fed

chore: add default parameter value for (simprocs : Simprocs)

2d738dc

chore: better method names

8fbf408

chore: use mathlib naming convention

a23029a

chore: update stage0

2bab43e

chroe: fix tests

f4a213f

chore: cleanup builtin simprocs using OptionT

7c5a37b

test: test for panic in simprocs

72e5a94

fix: panic at ite and dite simprocs

e6ed385

test: timeout in Mathlib.Computability.PartrecCode

9b2b4aa

feat: add simp configuration option Simp.Config.instances

9be86b5

When `instances := false`, instance implicit arguments are not visited during `simp`. `Std` does not seem affected by this change.

leodemoura requested review from kim-em and Kha as code owners January 9, 2024 00:18

github-actions bot added the toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN label Jan 9, 2024

github-actions bot temporarily deployed to lean-lang.org/lean4/doc January 9, 2024 01:02 Inactive

kim-em added the full-ci label Jan 9, 2024

kim-em added a commit to leanprover-community/mathlib4 that referenced this pull request Jan 9, 2024

create Mathlib testing branch for leanprover/lean4#3151

b90df8e

kim-em mentioned this pull request Jan 9, 2024

chore: adaptations for leanprover/lean4#3151 leanprover-community/mathlib4#9572

Closed

1 task

leanprover-community-mathlib4-bot added the breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan label Jan 9, 2024

leanprover-community-mathlib4-bot added builds-mathlib CI has verified that Mathlib builds against this PR and removed breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan labels Jan 9, 2024

kim-em closed this Apr 22, 2024

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

feat: add `simp` configuration option `Simp.Config.instances` #3151

feat: add `simp` configuration option `Simp.Config.instances` #3151

leodemoura commented Jan 9, 2024 •

edited by kim-em

Loading

leodemoura commented Jan 9, 2024

leanprover-community-mathlib4-bot commented Jan 9, 2024 •

edited

Loading

leanprover-bot commented Jan 9, 2024

kim-em commented Jan 9, 2024 •

edited

Loading

kim-em commented Jan 9, 2024

kim-em commented Apr 22, 2024

feat: add simp configuration option Simp.Config.instances #3151

feat: add simp configuration option Simp.Config.instances #3151

Conversation

leodemoura commented Jan 9, 2024 • edited by kim-em Loading

leodemoura commented Jan 9, 2024

leanprover-community-mathlib4-bot commented Jan 9, 2024 • edited Loading

leanprover-bot commented Jan 9, 2024

kim-em commented Jan 9, 2024 • edited Loading

kim-em commented Jan 9, 2024

kim-em commented Apr 22, 2024

feat: add `simp` configuration option `Simp.Config.instances` #3151

feat: add `simp` configuration option `Simp.Config.instances` #3151

leodemoura commented Jan 9, 2024 •

edited by kim-em

Loading

leanprover-community-mathlib4-bot commented Jan 9, 2024 •

edited

Loading

kim-em commented Jan 9, 2024 •

edited

Loading