feat: fine-grained equational lemmas for non-recursive functions #4154

nomeata · 2024-05-13T17:08:19Z

This is part of #3983.

Fine-grained equational lemmas are useful even for non-recursive functions, so this adds them.

The new option eqns.nonrecursive can be set to false to have the old behavior.

Breaking channge

This is a breaking change: Previously, rw [Option.map] would rewrite Option.map f o to match o with … . Now this rewrite will fail because the equational lemmas require constructors here (like they do for, say, List.map).

Remedies:

Split on o before rewriting.
Use rw [Option.map.eq_def], which rewrites any (saturated) application of Option.map
Use set_option eqns.nonrecursive false when defining the function in question.

Interaction with simp

The simp tactic so far had a special provision for non-recursive functions so that simp [f] will try to use the equational lemmas, but will also unfold f else, so less breakage here (but maybe performance improvements with functions with many cases when applied to a constructor, as the simplifier will no longer unfold to a large match-statement and then collapse it right away).

For projection functions and functions marked [reducible], simp [f] won’t use the equational theorems, and will only use its internal unfolding machinery.

Implementation notes

It uses the same mkEqnTypes function as for recursive functions, so we are close to a consistency here. There is still the wrinkle that for recursive functions we don't split matches without an interesting recursive call inside. Unifying that is future work.

leanprover-community-mathlib4-bot · 2024-05-13T17:32:21Z

Mathlib CI status (docs):

💥 Mathlib branch lean-pr-testing-4154 build failed against this PR. (2024-05-13 17:32:20) View Log
💥 Mathlib branch lean-pr-testing-4154 build failed against this PR. (2024-05-13 18:19:14) View Log
💥 Mathlib branch lean-pr-testing-4154 build failed against this PR. (2024-06-03 15:30:34) View Log
💥 Mathlib branch lean-pr-testing-4154 build failed against this PR. (2024-08-15 10:38:45) View Log
💥 Mathlib branch lean-pr-testing-4154 build failed against this PR. (2024-08-15 11:38:17) View Log
💥 Mathlib branch lean-pr-testing-4154 build failed against this PR. (2024-08-15 11:53:34) View Log
💥 Mathlib branch lean-pr-testing-4154 build failed against this PR. (2024-08-15 12:50:37) View Log
🟡 Mathlib branch lean-pr-testing-4154 build against this PR was cancelled. (2024-08-15 14:00:02) View Log
💥 Mathlib branch lean-pr-testing-4154 build failed against this PR. (2024-08-15 14:17:44) View Log
🟡 Mathlib branch lean-pr-testing-4154 build against this PR was cancelled. (2024-08-16 06:17:28) View Log
💥 Mathlib branch lean-pr-testing-4154 build failed against this PR. (2024-08-16 06:34:24) View Log
💥 Mathlib branch lean-pr-testing-4154 build failed against this PR. (2024-08-16 09:17:27) View Log
💥 Mathlib branch lean-pr-testing-4154 build failed against this PR. (2024-08-16 10:09:54) View Log
💥 Mathlib branch lean-pr-testing-4154 build failed against this PR. (2024-08-16 10:58:04) View Log
💥 Mathlib branch lean-pr-testing-4154 build failed against this PR. (2024-08-16 12:04:07) View Log
🟡 Mathlib branch lean-pr-testing-4154 build this PR didn't complete normally. (2024-08-16 12:24:46) View Log
🟡 Mathlib branch lean-pr-testing-4154 build this PR didn't complete normally. (2024-08-16 12:40:56) View Log
🟡 Mathlib branch lean-pr-testing-4154 build against this PR was cancelled. (2024-08-16 12:55:45) View Log
🟡 Mathlib branch lean-pr-testing-4154 build against this PR was cancelled. (2024-08-16 13:03:27) View Log
💥 Mathlib branch lean-pr-testing-4154 build failed against this PR. (2024-08-16 13:26:19) View Log
🟡 Mathlib branch lean-pr-testing-4154 build against this PR was cancelled. (2024-08-16 15:33:04) View Log
💥 Mathlib branch lean-pr-testing-4154 build failed against this PR. (2024-08-16 16:28:27) View Log
💥 Mathlib branch lean-pr-testing-4154 build failed against this PR. (2024-08-19 08:32:11) View Log
💥 Mathlib branch lean-pr-testing-4154 build failed against this PR. (2024-08-19 08:56:05) View Log
💥 Mathlib branch lean-pr-testing-4154 build failed against this PR. (2024-08-19 09:13:58) View Log
✅ Mathlib branch lean-pr-testing-4154 has successfully built against this PR. (2024-08-19 09:26:44) View Log
✅ Mathlib branch lean-pr-testing-4154 has successfully built against this PR. (2024-08-19 14:13:34) View Log
💥 Mathlib branch lean-pr-testing-4154 build failed against this PR. (2024-08-21 09:41:00) View Log
✅ Mathlib branch lean-pr-testing-4154 has successfully built against this PR. (2024-08-21 10:51:53) View Log
✅ Mathlib branch lean-pr-testing-4154 has successfully built against this PR. (2024-08-22 11:26:13) View Log
💥 Mathlib branch lean-pr-testing-4154 build failed against this PR. (2024-08-22 12:16:38) View Log
✅ Mathlib branch lean-pr-testing-4154 has successfully built against this PR. (2024-08-22 13:20:44) View Log

…to joachim/nonrec-eqns2

to avoid `id` checkpoints in the proof, which would make the lemma ineligible for dsmip

…nrec-eqns2

This is part of #3983. After #4154 introduced equational lemmas for non-recursive functions and #5055 unififed the lemmas for structural and wf recursive funcitons, this now disables the special handling of recursive functions in `findMatchToSplit?`, so that the equational lemmas should be the same no matter how the function was defined. The new option `eqns.deepRecursiveSplit` can be disabled to get the old behavior. This can break existing code, as there now can be extra equational lemmas: * Explicit uses of `f.eq_2` might have to be adjusted if the numbering changed. * Uses of `rw [f]` or `simp [f]` may no longer apply if they previously matched (and introduced a `match` statement), when the equational lemmas got more fine-grained. In this case either case analysis on the parameters before rewriting helps, or setting the option `opt.deepRecursiveSplit false` while defining the function

commit 6d957dc Author: Joachim Breitner <[email protected]> Date: Thu Aug 22 15:10:57 2024 +0200 Fix proof commit 5b95381 Merge: 48bea5e bc78dd4 Author: leanprover-community-mathlib4-bot <[email protected]> Date: Thu Aug 22 11:24:01 2024 +0000 Trigger CI for leanprover/lean4#4154 commit 48bea5e Author: Joachim Breitner <[email protected]> Date: Wed Aug 21 18:35:50 2024 +0200 Switch to Mathlib.Init commit 4d38bbd Author: leanprover-community-mathlib4-bot <[email protected]> Date: Wed Aug 21 18:25:08 2024 +0000 Trigger CI for leanprover/lean4#4154 commit f84b84d Author: leanprover-community-mathlib4-bot <[email protected]> Date: Wed Aug 21 09:58:00 2024 +0000 Trigger CI for leanprover/lean4#4154 commit f958309 Author: leanprover-community-mathlib4-bot <[email protected]> Date: Wed Aug 21 09:39:13 2024 +0000 Trigger CI for leanprover/lean4#4154 commit 4b976ec Author: Joachim Breitner <[email protected]> Date: Wed Aug 21 10:54:32 2024 +0200 Try to remove some nolints commit 0cbb129 Author: Joachim Breitner <[email protected]> Date: Wed Aug 21 10:53:14 2024 +0200 Reduce diff commit a485ac8 Author: leanprover-community-mathlib4-bot <[email protected]> Date: Tue Aug 20 08:02:41 2024 +0000 Trigger CI for leanprover/lean4#4154 commit b5cb54a Author: leanprover-community-mathlib4-bot <[email protected]> Date: Mon Aug 19 13:09:14 2024 +0000 Trigger CI for leanprover/lean4#4154 commit 8b1ce21 Author: Joachim Breitner <[email protected]> Date: Mon Aug 19 12:56:07 2024 +0200 Like this? commit e6ce4b5 Author: Joachim Breitner <[email protected]> Date: Mon Aug 19 11:38:06 2024 +0200 nolint attributes commit e24f1c6 Author: Joachim Breitner <[email protected]> Date: Mon Aug 19 11:15:52 2024 +0200 Another simp only gone commit a9d54a8 Author: Joachim Breitner <[email protected]> Date: Mon Aug 19 11:11:30 2024 +0200 aesop_cat broke :-( commit b4edcec Author: Joachim Breitner <[email protected]> Date: Mon Aug 19 11:03:43 2024 +0200 Use dsimp only commit 8e66ddd Author: Joachim Breitner <[email protected]> Date: Mon Aug 19 10:28:04 2024 +0200 Fixes in ComposableArrows commit 471b000 Author: Joachim Breitner <[email protected]> Date: Mon Aug 19 10:18:56 2024 +0200 Use cond_false commit 8120390 Author: Joachim Breitner <[email protected]> Date: Mon Aug 19 10:14:41 2024 +0200 No rfl after simp needed anymore commit 0544693 Author: Joachim Breitner <[email protected]> Date: Mon Aug 19 10:13:00 2024 +0200 Less dsimp only commit 5cffe6e Author: Joachim Breitner <[email protected]> Date: Mon Aug 19 10:10:21 2024 +0200 More autoParam commit 8e019f8 Author: Joachim Breitner <[email protected]> Date: Fri Aug 16 17:16:43 2024 +0200 More fixes commit 7b6f094 Author: Joachim Breitner <[email protected]> Date: Fri Aug 16 17:13:46 2024 +0200 More fixes commit 3151f57 Author: Joachim Breitner <[email protected]> Date: Fri Aug 16 17:10:35 2024 +0200 More [autoParam] commit 54a6616 Author: Joachim Breitner <[email protected]> Date: Fri Aug 16 17:07:19 2024 +0200 Some fixes commit 9c41f64 Author: Joachim Breitner <[email protected]> Date: Fri Aug 16 12:15:03 2024 +0200 Check for cold cache commit 66ff376 Author: Joachim Breitner <[email protected]> Date: Fri Aug 16 14:54:25 2024 +0200 No longer needed dsimps? commit 2298410 Author: leanprover-community-mathlib4-bot <[email protected]> Date: Fri Aug 16 12:24:02 2024 +0000 Trigger CI for leanprover/lean4#4154 commit 8bca337 Author: Joachim Breitner <[email protected]> Date: Fri Aug 16 12:17:43 2024 +0200 Some reasonable fixes commit 14247a2 Author: Joachim Breitner <[email protected]> Date: Fri Aug 16 12:16:08 2024 +0200 Revert "work-around dsimp Function.eval" This reverts commit 8c36154. commit 0c86721 Author: leanprover-community-mathlib4-bot <[email protected]> Date: Fri Aug 16 10:35:28 2024 +0000 Trigger CI for leanprover/lean4#4154 commit 4b2124e Author: leanprover-community-mathlib4-bot <[email protected]> Date: Fri Aug 16 09:45:57 2024 +0000 Trigger CI for leanprover/lean4#4154 commit 125f713 Author: leanprover-community-mathlib4-bot <[email protected]> Date: Fri Aug 16 08:51:57 2024 +0000 Trigger CI for leanprover/lean4#4154 commit af7ab6c Author: Joachim Breitner <[email protected]> Date: Fri Aug 16 08:16:31 2024 +0200 Style exception commit f11401e Author: Joachim Breitner <[email protected]> Date: Fri Aug 16 08:08:49 2024 +0200 toAdditive: transport MatcherInfo commit 8c36154 Author: Joachim Breitner <[email protected]> Date: Thu Aug 15 18:27:00 2024 +0200 work-around dsimp Function.eval commit 5fcef86 Author: leanprover-community-mathlib4-bot <[email protected]> Date: Thu Aug 15 14:24:51 2024 +0000 Trigger CI for leanprover/lean4#4154 commit d4e2758 Author: leanprover-community-mathlib4-bot <[email protected]> Date: Thu Aug 15 13:59:06 2024 +0000 Trigger CI for leanprover/lean4#4154 commit af1456c Author: Joachim Breitner <[email protected]> Date: Thu Aug 15 15:49:23 2024 +0200 Fix call to getEqnsFor? commit c62ab2f Author: leanprover-community-mathlib4-bot <[email protected]> Date: Thu Aug 15 12:30:12 2024 +0000 Trigger CI for leanprover/lean4#4154 commit d9bc3e9 Author: leanprover-community-mathlib4-bot <[email protected]> Date: Thu Aug 15 11:47:22 2024 +0000 Trigger CI for leanprover/lean4#4154 commit 40bc4fe Author: Joachim Breitner <[email protected]> Date: Thu Aug 15 10:50:26 2024 +0000 chore: do not set release-ci label upon failed PR test (#15775) with leanprover/lean4#5022 the need for this should have disappeared commit 2ff3b31 Merge: 33a583e b8ad879 Author: leanprover-community-mathlib4-bot <[email protected]> Date: Thu Aug 15 10:32:05 2024 +0000 Trigger CI for leanprover/lean4#4154 commit 33a583e Merge: 1c951db 85647f2 Author: leanprover-community-mathlib4-bot <[email protected]> Date: Mon Jun 3 15:24:02 2024 +0000 Trigger CI for leanprover/lean4#4154 commit 1c951db Author: leanprover-community-mathlib4-bot <[email protected]> Date: Mon May 13 18:13:38 2024 +0000 Trigger CI for leanprover/lean4#4154 commit f05d463 Author: leanprover-community-mathlib4-bot <[email protected]> Date: Mon May 13 17:26:47 2024 +0000 Update lean-toolchain for testing leanprover/lean4#4154

#5129) This is part of #3983. After #4154 introduced equational lemmas for non-recursive functions and #5055 unififed the lemmas for structural and wf recursive funcitons, this now disables the special handling of recursive functions in `findMatchToSplit?`, so that the equational lemmas should be the same no matter how the function was defined. The new option `eqns.deepRecursiveSplit` can be disabled to get the old behavior. ### Breaking change This can break existing code, as there now can be extra equational lemmas: * Explicit uses of `f.eq_2` might have to be adjusted if the numbering changed. * Uses of `rw [f]` or `simp [f]` may no longer apply if they previously matched (and introduced a `match` statement), when the equational lemmas got more fine-grained. In this case either case analysis on the parameters before rewriting helps, or setting the option `opt.deepRecursiveSplit false` while defining the function

leanprover#5129) This is part of leanprover#3983. After leanprover#4154 introduced equational lemmas for non-recursive functions and leanprover#5055 unififed the lemmas for structural and wf recursive funcitons, this now disables the special handling of recursive functions in `findMatchToSplit?`, so that the equational lemmas should be the same no matter how the function was defined. The new option `eqns.deepRecursiveSplit` can be disabled to get the old behavior. ### Breaking change This can break existing code, as there now can be extra equational lemmas: * Explicit uses of `f.eq_2` might have to be adjusted if the numbering changed. * Uses of `rw [f]` or `simp [f]` may no longer apply if they previously matched (and introduced a `match` statement), when the equational lemmas got more fine-grained. In this case either case analysis on the parameters before rewriting helps, or setting the option `opt.deepRecursiveSplit false` while defining the function

in #4154 and #5129 the rules for equational lemmas have changed, and new options were introduced that can be used to revert to the pre-4.12 behavior. Hopefully nobody really needs these options besides for backwards compatibility, therefore we put these options in the `backward` option name space. So the previous behavior can be achieved by setting ```lean set_option backward.eqns.nonrecursive false set_option backward.eqns.deepRecursiveSplit false ```

and with leanprover/lean4#4154 it actually complains, so let's remove them now.

nomeata added 4 commits May 13, 2024 18:16

remove unused getFixedPrefix

4cefae7

nonrec eqn tests

787b221

is simpMatchWF needed?

cbdc0c5

Use fine-grained equations for non-rec equations

5b1e503

nomeata force-pushed the joachim/nonrec-eqns2 branch from 142e1a2 to 5b1e503 Compare May 13, 2024 17:08

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

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

Update lean-toolchain for testing leanprover/lean4#4154

1b1f57c

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

Update lean-toolchain for testing leanprover/lean4#4154

f05d463

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

nomeata added 2 commits May 13, 2024 19:50

Some (enlightening) test fallout

a2d4866

More test fixes

66a500c

github-actions bot temporarily deployed to lean-lang.org/lean4/doc May 13, 2024 18:09 Inactive

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

Trigger CI for leanprover/lean4#4154

8b734eb

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

Trigger CI for leanprover/lean4#4154

1c951db

Merge branch 'nightly-with-mathlib' of github.com:leanprover/lean4 in…

ebb5ffe

…to joachim/nonrec-eqns2

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

Trigger CI for leanprover/lean4#4154

8be9e0e

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

Trigger CI for leanprover/lean4#4154

33a583e

leanprover-community-mathlib4-bot added the release-ci Enable all CI checks for a PR, like is done for releases label Jun 3, 2024

nomeata added a commit to nomeata/leansat that referenced this pull request Jun 3, 2024

Partial fixes for leanprover/lean4#4154

a200b63

nomeata mentioned this pull request Jun 3, 2024

RFC: consistent (fine-grained?) equational lemmas #3983

Closed

leodemoura force-pushed the master branch from 32d60c5 to 696f70b Compare July 20, 2024 02:58

nomeata added 2 commits August 15, 2024 11:33

Merge branch 'nightly-with-mathlib' of github.com:leanprover/lean4 in…

3ed98ed

…to joachim/nonrec-eqns2

Introduce eqns.nonrecursive

65167f6

nomeata removed the release-ci Enable all CI checks for a PR, like is done for releases label Aug 15, 2024

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

Trigger CI for leanprover/lean4#4154

9a15e20

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

Trigger CI for leanprover/lean4#4154

2ff3b31

Try rfl before deltaLHS

4f14480

to avoid `id` checkpoints in the proof, which would make the lemma ineligible for dsmip

leanprover-community-mathlib4-bot added the release-ci Enable all CI checks for a PR, like is done for releases label Aug 15, 2024

nomeata removed the release-ci Enable all CI checks for a PR, like is done for releases label Aug 15, 2024

nomeata added 2 commits August 22, 2024 11:24

Fix c_without_negPivot_of_performRatCheck_success

7aec64e

Merge branch 'nightly' of github.com:leanprover/lean4 into joachim/no…

6d646c6

…nrec-eqns2

nomeata requested a review from TwoFX as a code owner August 22, 2024 09:29

nomeata disabled auto-merge August 22, 2024 09:29

github-actions bot temporarily deployed to lean-lang.org/lean4/doc August 22, 2024 09:42 Inactive

Do not use generateEagerEqns too early

10b081f

nomeata mentioned this pull request Aug 22, 2024

feat: same equational lemmas for recursive and non-recursive functions #5129

Merged

github-actions bot temporarily deployed to lean-lang.org/lean4/doc August 22, 2024 10:34 Inactive

nomeata mentioned this pull request Aug 22, 2024

[Merged by Bors] - feat: toAdditive to transfer MatcherInfo data leanprover-community/mathlib4#16026

Closed

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

Trigger CI for leanprover/lean4#4154

2806fac

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

Trigger CI for leanprover/lean4#4154

5b95381

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

nomeata changed the title ~~feat: fine-grained equational lemmas for non-recursive equations~~ feat: fine-grained equational lemmas for non-recursive functions Aug 22, 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 Aug 22, 2024

nomeata added this pull request to the merge queue Aug 22, 2024

Merged via the queue into master with commit d975e43 Aug 22, 2024
33 checks passed

nomeata deleted the joachim/nonrec-eqns2 branch August 25, 2024 15:14

nomeata mentioned this pull request Aug 29, 2024

refactor: put new eqns options into backward namespace #5207

Merged

bjoernkjoshanssen pushed a commit to leanprover-community/mathlib4 that referenced this pull request Sep 9, 2024

chore: no need to pass autoParam to simp or dsimp (#15968)

f4cd7f2

and with leanprover/lean4#4154 it actually complains, so let's remove them now.

bjoernkjoshanssen pushed a commit to leanprover-community/mathlib4 that referenced this pull request Sep 9, 2024

chore: no need to pass autoParam to simp or dsimp (#15968)

201b6d1

and with leanprover/lean4#4154 it actually complains, so let's remove them now.

bjoernkjoshanssen pushed a commit to leanprover-community/mathlib4 that referenced this pull request Sep 12, 2024

chore: no need to pass autoParam to simp or dsimp (#15968)

e7bcb82

and with leanprover/lean4#4154 it actually complains, so let's remove them now.

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

feat: fine-grained equational lemmas for non-recursive functions #4154

feat: fine-grained equational lemmas for non-recursive functions #4154

nomeata commented May 13, 2024 •

edited

Loading

leanprover-community-mathlib4-bot commented May 13, 2024 •

edited

Loading

feat: fine-grained equational lemmas for non-recursive functions #4154

feat: fine-grained equational lemmas for non-recursive functions #4154

Conversation

nomeata commented May 13, 2024 • edited Loading

Breaking channge

Interaction with simp

Implementation notes

leanprover-community-mathlib4-bot commented May 13, 2024 • edited Loading

nomeata commented May 13, 2024 •

edited

Loading

leanprover-community-mathlib4-bot commented May 13, 2024 •

edited

Loading