feat: `Simp.Config.implicitDefEqProofs` #4595

leodemoura · 2024-06-30T23:31:22Z

This PR implements Simp.Config.implicitDefEqsProofs. When true (default: true), simp will not create a proof term for a rewriting rule associated with an rfl-theorem. Rewriting rules are provided by users by annotating theorems with the attribute @[simp]. If the proof of the theorem is just rfl (reflexivity), and implicitDefEqProofs := true, simp will not create a proof term which is an application of the annotated theorem.

The default setting does change the existing behavior. Users can use simp -implicitDefEqProofs to force simp to create a proof term for rfl-theorems. This can positively impact proof checking time in the kernel.

This PR also fixes an issue in the split tactic that has been exposed by this feature. It was looking for split candidates in proofs and implicit arguments. See new test for issue exposed by the previous feature.

leanprover-community-mathlib4-bot · 2024-06-30T23:53:26Z

Mathlib CI status (docs):

💥 Mathlib branch lean-pr-testing-4595 build failed against this PR. (2024-06-30 23:53:25) View Log
💥 Mathlib branch lean-pr-testing-4595 build failed against this PR. (2024-07-01 01:05:01) View Log
💥 Mathlib branch lean-pr-testing-4595 build failed against this PR. (2024-07-01 20:08:46) View Log
💥 Mathlib branch lean-pr-testing-4595 build failed against this PR. (2024-07-02 01:03:55) View Log
💥 Mathlib branch lean-pr-testing-4595 build failed against this PR. (2024-07-02 02:15:53) View Log
💥 Mathlib branch lean-pr-testing-4595 build failed against this PR. (2024-07-02 10:48:30) View Log
💥 Mathlib branch lean-pr-testing-4595 build failed against this PR. (2024-07-02 12:27:44) View Log
🟡 Mathlib branch lean-pr-testing-4595 build against this PR was cancelled. (2024-07-11 01:05:03) View Log
💥 Mathlib branch lean-pr-testing-4595 build failed against this PR. (2024-07-11 01:27:10) View Log
🟡 Mathlib branch lean-pr-testing-4595 build against this PR was cancelled. (2024-07-11 02:36:32) View Log
❌ Mathlib branch lean-pr-testing-4595 built against this PR, but linting failed. (2024-07-11 03:05:41) View Log
❗ Mathlib CI can not be attempted yet, as the nightly-testing-2024-07-19 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-mathlib, Mathlib CI should run now. (2024-07-19 16:05:14)

(With leanprover/lean4#4595, `aesop` goes astray here, and this proof is better anyway.)

Defensive change preparing for leanprover/lean4#4595.

Motivation: unblock PR #4595 `Simp.Config.implicitDefEqProofs := false` is currently creating too many issues in Mathlib.

leanprover-community-bot · 2024-11-29T02:18:57Z

Mathlib CI status (docs):

🟡 Mathlib branch lean-pr-testing-4595 build this PR didn't complete normally. (2024-11-29 02:18:57) View Log
💥 Mathlib branch lean-pr-testing-4595 build failed against this PR. (2024-11-29 04:53:14) View Log
💥 Mathlib branch lean-pr-testing-4595 build failed against this PR. (2024-11-29 07:32:15) View Log
✅ Mathlib branch lean-pr-testing-4595 has successfully built against this PR. (2024-11-29 08:38:39) View Log
✅ Mathlib branch lean-pr-testing-4595 has successfully built against this PR. (2024-11-29 22:30:46) View Log

We want to overhead of processing every single partial application.

This PR implements `Simp.Config.implicitDefEqsProofs`. When `true` (default: `true`), `simp` will **not** create a proof term for a rewriting rule associated with an `rfl`-theorem. Rewriting rules are provided by users by annotating theorems with the attribute `@[simp]`. If the proof of the theorem is just `rfl` (reflexivity), and `implicitDefEqProofs := true`, `simp` will **not** create a proof term which is an application of the annotated theorem. The default setting does change the existing behavior. Users can use `simp -implicitDefEqProofs` to force `simp` to create a proof term for `rfl`-theorems. This can positively impact proof checking time in the kernel. This PR also fixes an issue in the `split` tactic that has been exposed by this feature. It was looking for `split` candidates in proofs and implicit arguments. See new test for issue exposed by the previous feature. --------- Co-authored-by: Kim Morrison <kim@tqft.net>

github-actions bot temporarily deployed to lean-lang.org/lean4/doc June 30, 2024 23:39 Inactive

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

leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Jun 30, 2024

Update lean-toolchain for testing leanprover/lean4#4595

2370110

leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Jun 30, 2024

Update lean-toolchain for testing leanprover/lean4#4595

5be9405

leanprover-community-mathlib4-bot added breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan release-ci Enable all CI checks for a PR, like is done for releases labels Jun 30, 2024

github-actions bot temporarily deployed to lean-lang.org/lean4/doc July 1, 2024 00:11 Inactive

leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Jul 1, 2024

Trigger CI for leanprover/lean4#4595

5c58761

leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Jul 1, 2024

Trigger CI for leanprover/lean4#4595

814e965

kim-em mentioned this pull request Jul 1, 2024

chore: remove nonterminal simps in UnionFind leanprover-community/batteries#868

Merged

leodemoura force-pushed the simp_rfl_thm branch from b06cc0d to 1479d41 Compare July 1, 2024 19:12

github-actions bot temporarily deployed to lean-lang.org/lean4/doc July 1, 2024 19:23 Inactive

leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Jul 1, 2024

Trigger CI for leanprover/lean4#4595

0253420

leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Jul 1, 2024

Trigger CI for leanprover/lean4#4595

96672ed

github-actions bot temporarily deployed to lean-lang.org/lean4/doc July 2, 2024 01:15 Inactive

leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Jul 2, 2024

Trigger CI for leanprover/lean4#4595

b6e86b1

leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Jul 2, 2024

Trigger CI for leanprover/lean4#4595

28456c1

This was referenced Jul 11, 2024

[Merged by Bors] - chore: robustify proof in CategoryTheory.GlueData leanprover-community/mathlib4#14634

Closed

[Merged by Bors] - chore: robustify proof in CategoryTheory.Limit.VanKampen leanprover-community/mathlib4#14635

Closed

mathlib-bors bot pushed a commit to leanprover-community/mathlib4 that referenced this pull request Jul 11, 2024

chore: robustify proof in CategoryTheory.GlueData (#14634)

ea58bd5

(With leanprover/lean4#4595, `aesop` goes astray here, and this proof is better anyway.)

mathlib-bors bot pushed a commit to leanprover-community/mathlib4 that referenced this pull request Jul 11, 2024

chore: robustify proof in CategoryTheory.Limit.VanKampen (#14635)

17a1a34

Defensive change preparing for leanprover/lean4#4595.

mathlib-bors bot pushed a commit to leanprover-community/mathlib4 that referenced this pull request Jul 11, 2024

chore: robustify proof in CategoryTheory.Limit.VanKampen (#14635)

e4e6ef5

Defensive change preparing for leanprover/lean4#4595.

kim-em added a commit that referenced this pull request Jul 16, 2024

feat: test minimizing slowdown from #4595

86e08b7

kim-em mentioned this pull request Jul 16, 2024

feat: test minimizing slowdown from #4595 #4755

Closed

leodemoura added a commit that referenced this pull request Jul 18, 2024

chore: Simp.Config.implicitDefEqProofs := true by default

bf73a26

Motivation: unblock PR #4595 `Simp.Config.implicitDefEqProofs := false` is currently creating too many issues in Mathlib.

leodemoura mentioned this pull request Jul 18, 2024

chore: Simp.Config.implicitDefEqProofs := true by default #4784

Merged

github-merge-queue bot pushed a commit that referenced this pull request Jul 18, 2024

chore: Simp.Config.implicitDefEqProofs := true by default (#4784)

5526ff6

Motivation: unblock PR #4595 `Simp.Config.implicitDefEqProofs := false` is currently creating too many issues in Mathlib.

leodemoura force-pushed the simp_rfl_thm branch from d51e86b to 9702909 Compare July 19, 2024 15:15

github-actions bot temporarily deployed to lean-lang.org/lean4/doc July 19, 2024 15:24 Inactive

kim-em force-pushed the simp_rfl_thm branch from 509d698 to e4d4dc4 Compare November 29, 2024 01:48

github-actions bot temporarily deployed to lean-lang.org/lean4/doc November 29, 2024 01:56 Inactive

kim-em added 2 commits November 29, 2024 13:35

chore: add test for split

26a3368

chore: fix for FindSplitImpl.visit.visitApp?

165fb2d

github-actions bot temporarily deployed to lean-lang.org/lean4/doc November 29, 2024 03:27 Inactive

kim-em removed breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN labels Nov 29, 2024

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

leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Nov 29, 2024

Trigger CI for leanprover/lean4#4595

995c4a2

leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Nov 29, 2024

Trigger CI for leanprover/lean4#4595

a1e39b3

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

check for loose bvars

2048172

kim-em removed breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN labels Nov 29, 2024

github-actions bot temporarily deployed to lean-lang.org/lean4/doc November 29, 2024 06:03 Inactive

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

leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Nov 29, 2024

Trigger CI for leanprover/lean4#4595

2d39f12

leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Nov 29, 2024

Trigger CI for leanprover/lean4#4595

fc5a74a

chore: ensures getFunInfo is used effectively

28b5141

We want to overhead of processing every single partial application.

github-actions bot temporarily deployed to lean-lang.org/lean4/doc November 29, 2024 20:51 Inactive

leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Nov 29, 2024

Trigger CI for leanprover/lean4#4595

85a82b4

leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Nov 29, 2024

Trigger CI for leanprover/lean4#4595

3cc143e

leodemoura added this pull request to the merge queue Nov 29, 2024

Merged via the queue into master with commit 27df5e9 Nov 29, 2024
24 checks passed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

feat: `Simp.Config.implicitDefEqProofs` #4595

feat: `Simp.Config.implicitDefEqProofs` #4595

leodemoura commented Jun 30, 2024 •

edited

Loading

leanprover-community-mathlib4-bot commented Jun 30, 2024 •

edited

Loading

leanprover-community-bot commented Nov 29, 2024 •

edited

Loading

feat: Simp.Config.implicitDefEqProofs #4595

feat: Simp.Config.implicitDefEqProofs #4595

Conversation

leodemoura commented Jun 30, 2024 • edited Loading

leanprover-community-mathlib4-bot commented Jun 30, 2024 • edited Loading

leanprover-community-bot commented Nov 29, 2024 • edited Loading

feat: `Simp.Config.implicitDefEqProofs` #4595

feat: `Simp.Config.implicitDefEqProofs` #4595

leodemoura commented Jun 30, 2024 •

edited

Loading

leanprover-community-mathlib4-bot commented Jun 30, 2024 •

edited

Loading

leanprover-community-bot commented Nov 29, 2024 •

edited

Loading