feat: show tactic (full version) - #1749
Conversation
| try | ||
| mvarId.withContext do | ||
| let mvarIdNew ← mkFreshExprMVar (← Term.elabType e) | ||
| mvarId.assign (← Term.ensureHasType (← mvarId.getType) mvarIdNew "'show' tactic failed") |
There was a problem hiding this comment.
As you mentioned in the PR description, this will insert coercions if the types don't match.
I'm not sure if this such a good fit for a tactic that selects goals by type (as it is quite likely that it will just pick the first goal and insert a coercion).
There was a problem hiding this comment.
The coercion is not a subgoal, so I don't see how this would be a real concern unless both the source and target types are sufficiently known that the coercion can be fully synthesized. At least, it did not appear to be an issue in my tests.
There was a problem hiding this comment.
both the source and target types are sufficiently known that the coercion can be fully synthesized.
I think you have the wrong model of coercions: ensureHasType always succeeds unless it can show that types cannot be coerced. If it cannot coerce immediately, it will insert a "postponed" coercion (which works like postponed elaborators).
The standard for "cannot be coerced" is what type class synthesis returns. It can return either some coeInst, none, or undef. The ensureHasType function only fails if it gets none. I'm not completely sure under which circumstances we get undef though.
Practically speaking, this will only trigger if we 1) have coercions for goal types (i.e., propositions), and 2) the goal type or the show term has a metavariable.
There was a problem hiding this comment.
In that case, it sounds like it would suffice to call synthesizeSyntheticMVarsNoPostponing after the assignment, right?
There was a problem hiding this comment.
That might be a good idea anyhow, just to resolve things like show ⟨1,2⟩ = _.
I'm still not convinced by the automatic coercions. Do you have a use case for that?
There was a problem hiding this comment.
What do you mean by "resolve" there? Will show ⟨1,2⟩ = _ be rejected if we do that? (In particular, the _ should not be an error nor should it produce a subgoal.)
As for automatic coercions, no it's not a big deal to lose them, but it would be more consistent with term mode show, which will perform coercions. (I would like tactics to behave the same as their term mode counterparts where reasonable.) It's also what the original show macro tactic did, since it was implemented in terms of term mode show.
👍 |
|
Dev meeting summary: make Lean 4 |
|
This hasn't been touched in over a year, and has a merge conflict. I'm closing now; please re-open if you think appropriate. |
4 participants
This implements the TODO in the
showtactic:show ewill first try to change the goal toe, and if that doesn't work it will try to change one of the other open goals toeand select it. Note: This implementation allows the goal to change in a non-defeq way and will insert coercions. I plan to follow this up with an implementation ofchangewhich is only for strictly defeq changes, similar todsimp only.A thought: should the goal-selecting version of
showbe spelledshow e => tacinstead? It is a bit awkward that it acts like a move-to-front tactic but has nocase =>form so you have to doshow e; . tacto actually work on the selected goal.