feat: fine-grained equational lemmas for non-recursive functions#4154
Merged
feat: fine-grained equational lemmas for non-recursive functions#4154
Conversation
142e1a2 to
5b1e503
Compare
ghost
pushed a commit
to leanprover-community/batteries
that referenced
this pull request
May 13, 2024
ghost
pushed a commit
to leanprover-community/mathlib4
that referenced
this pull request
May 13, 2024
|
Mathlib CI status (docs):
|
ghost
pushed a commit
to leanprover-community/batteries
that referenced
this pull request
May 13, 2024
ghost
pushed a commit
to leanprover-community/mathlib4
that referenced
this pull request
May 13, 2024
…to joachim/nonrec-eqns2
ghost
pushed a commit
to leanprover-community/batteries
that referenced
this pull request
Jun 3, 2024
ghost
pushed a commit
to leanprover-community/mathlib4
that referenced
this pull request
Jun 3, 2024
nomeata
added a commit
to nomeata/leansat
that referenced
this pull request
Jun 3, 2024
…to joachim/nonrec-eqns2
ghost
pushed a commit
to leanprover-community/batteries
that referenced
this pull request
Aug 15, 2024
ghost
pushed a commit
to leanprover-community/mathlib4
that referenced
this pull request
Aug 15, 2024
to avoid `id` checkpoints in the proof, which would make the lemma ineligible for dsmip
ghost
pushed a commit
to leanprover-community/mathlib4
that referenced
this pull request
Aug 21, 2024
ghost
pushed a commit
to leanprover-community/batteries
that referenced
this pull request
Aug 21, 2024
ghost
pushed a commit
to leanprover-community/mathlib4
that referenced
this pull request
Aug 21, 2024
ghost
pushed a commit
to leanprover-community/batteries
that referenced
this pull request
Aug 21, 2024
ghost
pushed a commit
to leanprover-community/mathlib4
that referenced
this pull request
Aug 21, 2024
…to joachim/nonrec-eqns2
This was referenced Aug 22, 2024
This file contains hidden or 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
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
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.
Fine-grained equational lemmas are useful even for non-recursive functions, so this adds them.
The new option
eqns.nonrecursivecan be set tofalseto have the old behavior.Breaking channge
This is a breaking change: Previously,
rw [Option.map]would rewriteOption.map f otomatch o with …. Now this rewrite will fail because the equational lemmas require constructors here (like they do for, say,List.map).Remedies:
obefore rewriting.rw [Option.map.eq_def], which rewrites any (saturated) application ofOption.mapset_option eqns.nonrecursive falsewhen defining the function in question.Interaction with simp
The
simptactic so far had a special provision for non-recursive functions so thatsimp [f]will try to use the equational lemmas, but will also unfoldfelse, 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 largematch-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
mkEqnTypesfunction 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.