[Merged by Bors] - feat(data/pfun): Remove unneeded assumption from pfun.fix_induction #12920
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.
Removed a hypothesis from
pfun.fix_induction
. Note that it was two "layers" deep, so this is actually a strengthening. The original can be recovered byNote that
eval_induction
copies this syntax, so the same argument was removed there as well.This allows for some simplifications of other parts of the code. Unfortunately, it was hard to figure out what was going on in the very dense parts of
tm_to_partrec.lean
andpartrec.lean
. I mostly just mechanically removed the hypotheses that were unnecessarily being supplied, and then checked if that caused some variable to be unused and removed that etc. But I cannot tell if this allows for greater simplifications.I also extracted two lemmas
fix_fwd
andfix_stop
that I thought would be useful on their own.