use does not work with the goal type
#5072
Labels
lean4-change-in-behaviour
Describes a known change in behaviour. No implication that it "needs fixing".
t-meta
Tactics, attributes or user commands
Comments
Ruben-VandeVelde
added
the
lean4-change-in-behaviour
|
This link searches for references to this issue in the source code. |
|
I've made a PR to make |
bors bot
pushed a commit
that referenced
this issue
Jul 27, 2023
…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>
adomani
pushed a commit
that referenced
this issue
Jul 28, 2023
…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>
semorrison
pushed a commit
that referenced
this issue
Aug 2, 2023
…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>
semorrison
pushed a commit
that referenced
this issue
Aug 14, 2023
…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>
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
This fails:
though it worked in mathlib3.
The text was updated successfully, but these errors were encountered: