-
Notifications
You must be signed in to change notification settings - Fork 438
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
feat: drop support for termination_by'
until around 7fe6881 the way to define well-founded recursions was to specify a `WellFoundedRelation` on the argument explicitly. This was rather low-level, for example one had to predict the packing of multiple arguments into `PProd`s, the packing of mutual functions into `PSum`s, and the cliques that were calculated. Then the current `termination_by` syntax was introduced, where you sepecify the termination argument at a higher level (one clause per functions, unpacked arguments), and the `WellFoundedRelation` is found using type class resolution. The old syntax was kept around as `termination_by'`. But at the time of writing, this is not used anywhere in the lean, std, mathlib or the theroem-proving-in-lean repositories. Also, should be possible to express anything that the old syntax supported also with the new one, possibly requiring a helper type with a suitable instance, or a very generic wrapper like ``` inductive WithWFRel {a : Type _} {rel : a → a → Prop} (h : WellFounded rel) where | mk : a -> WithWFRel h instance : WellFoundedRelation (WithWFRel h) := invImage (fun x => match x with | .mk x => x) ⟨_, h⟩ ``` Since the old syntax is unused, has an unhelpful name and relies on internals, this removes the support. Now is a good time before the refactoring that's planned in #2921. The test suite was updated without particular surprises. The parametric `terminationHint` parser is gone, which means we can match on syntax more easily now, in `expandDecreasingBy?`.
- Loading branch information
Showing
34 changed files
with
231 additions
and
343 deletions.
There are no files selected for viewing
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
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
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
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
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
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
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
Oops, something went wrong.