feat: same equational lemmas for recursive and non-recursive functions #5129
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
…to joachim/nonrec-eqns2
…to joachim/nonrec-eqns2
to avoid `id` checkpoints in the proof, which would make the lemma ineligible for dsmip
This reverts commit 9dc66bd.
nomeata
changed the title
leanprover-community-mathlib4-bot
added a commit
to leanprover-community/batteries
that referenced
this pull request
Aug 22, 2024
leanprover-community-mathlib4-bot
added a commit
to leanprover-community/mathlib4
that referenced
this pull request
Aug 22, 2024
leanprover-community-mathlib4-bot
added
the
breaks-mathlib
|
Srsly, no mathlib adaption needed (besides those for #4154)? If it weren’t for the test case in this PR I’d think I made a mistake. Maybe recursive functions with |
leanprover-community-mathlib4-bot
added
builds-mathlib
leanprover-community-mathlib4-bot
added a commit
to leanprover-community/batteries
that referenced
this pull request
Aug 24, 2024
leanprover-community-mathlib4-bot
added a commit
to leanprover-community/mathlib4
that referenced
this pull request
Aug 24, 2024
tobiasgrosser
pushed a commit
to opencompl/lean4
that referenced
this pull request
Aug 26, 2024
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
nomeata
added a commit
that referenced
this pull request
Aug 29, 2024
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 ```
github-merge-queue bot
pushed a commit
that referenced
this pull request
Aug 29, 2024
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 ```
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
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 nomatter how the function was defined.
The new option
eqns.deepRecursiveSplitcan be disabled to get the oldbehavior.
Breaking change
This can break existing code, as there now can be extra equational
lemmas:
Explicit uses of
f.eq_2might have to be adjusted if the numberingchanged.
Uses of
rw [f]orsimp [f]may no longer apply if they previouslymatched (and introduced a
matchstatement), when the equationallemmas got more fine-grained.
In this case either case analysis on the parameters before rewriting
helps, or setting the option
opt.deepRecursiveSplit falsewhiledefining the function