-
Notifications
You must be signed in to change notification settings - Fork 312
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
fix: let
use
provide last constructor argument, introduce mathlib3-…
…like flattening `use!` (#5350) Changes: * `use` now by default discharges with `try with_reducible use_discharger` with a custom discharger tactic rather than `try with_reducible rfl`, which makes it be closer to `exists` and the `use` in mathlib3. It doesn't go so far as to do `try with_reducible trivial` since that involves the `contradiction` tactic. * this discharger is configurable with `use (discharger := tacticSeq...)` * the `use` evaluation loop will try refining after constructor failure, so it can be used to fill in all arguments rather than all but the last, like in mathlib3 (closes #5072) but with the caveat that it only works so long as the last argument is not an inductive type (like `Eq`). * adds `use!`, which is nearly the same as the mathlib3 `use` and fills in constructor arguments along the nodes *and* leaves of the nested constructor expressions. This version tries refining before applying constructors, so it can be used like `exact` for the last argument. The difference between mathlib3 `use` and this `use!` is that (1) `use!` uses a different tactic to discharge goals (mathlib3 used `trivial'`, which did reducible refl, but also `contradiction`, which we don't emulate) (2) it does not rewrite using `exists_prop`. Regarding 2, this feature seems to be less useful now that bounded existentials encode the bound using a conjunction rather than with nested existentials. We do have `exists_prop` as part of `use_discharger` however. Co-authored-by: Floris van Doorn <fpvdoorn@gmail.com>
- Loading branch information
Showing
19 changed files
with
366 additions
and
65 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
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
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.