fix(solve_by_elim): working with multiple goals#838
Conversation
|
(This is a preliminary step for |
|
Why do you need this behaviour? |
For |
|
Ah i see! How do you feel about making the behaviour optional? We could
write `solve_by_elim!` or `solve_by_elim all`.
On Thu, Mar 21, 2019 at 17:06 Scott Morrison ***@***.***> wrote:
Why do you need this behaviour?
For library_search, in #839
<#839>. It directly
calls apply on the library lemma, then solve_by_elim on the newly
introduced goals. It's important solve_by_elim looks at all of the goals
together so it can do proper backtracking.
—
You are receiving this because you were assigned.
Reply to this email directly, view it on GitHub
<#838 (comment)>,
or mute the thread
<https://github.com/notifications/unsubscribe-auth/AAEVYIpgqMydAaCdakuQGDlPwlo9IZ2Xks5vY_RdgaJpZM4cBBRa>
.
--
Simon
|
|
Hmm... I guess so. I'm a bit sad --- perhaps it would have been better if the default was that you should expect a tactic to consider all the goals presented to it, not necessarily just the first one, and that "goal management" should be done explicitly. But that ship has certainly sailed, and it seems silly to wish that I'll add |
|
Okay, now you have to run |
|
I went with |
|
(When one day |
docs/tactics.md
Outdated
| also attempts to discharge the goal using congruence closure before each round of applying assumptions. | ||
|
|
||
| `solve_by_elim*` tries to solve all goals together, using backtracking if a solution for one goal | ||
| make other goals impossible. |
src/tactic/interactive.lean
Outdated
| `solve_by_elim [-id]` removes a specified assumption. | ||
|
|
||
| `solve_by_elim*` tries to solve all goals together, using backtracking if a solution for one goal | ||
| make other goals impossible. |
|
@semorrison I like what you went with |
Slightly modify the behaviour of
solve_by_elim, so it works on all current goals (backtracking if bad choices are made on one goal, making later goals unsolvable). No changes in the library required. The old behaviour can be recovered simply with{ solve_by_elim }.