Wingman feature request: Support for tactic subgoals via let

[s-zeng]

Feature request: there should be a tactic that allows the user to introduce arbitrary subgoals. Currently, subgoals are only introduced via destruct_all or similar tactics. But in general some subgoals are desired as helpers that cannot be produced from destruct and it's variants, so we should have a define tactic (or something similar) that let's use make arbitrary subgoals. For example, given:

_ :: a

and using a tactic define b :: b, we should be able to produce:

let b = (_ :: b) in (_ :: a)

This then should give us b as a subgoal, which when completed gives us b :: b as a hypothesis for completing the a goal.

[isovector]

Unfortunately, our parsing capabilities aren't good enough to allow for arbitrary types, and this unlikely to change anytime in the near future.

So what could we do instead? Maybe just a bare

define b

that then gets a fresh unification variable as its type. Subsequent tactics could unify that type. What do you think?

Also, it seems like we should be able to define multiple things here, so define a b c would produce

let a = (_ :: a0)
    b = (_ :: b0)
    c = (_ :: c0)
 in _

[isovector]

There's also the question of hole ordering. Should the main goal come first, or the bindings?

[isovector]

@s-zeng any opinions on this?

[s-zeng]

Sorry for missing this! I'm of the mind that if we want the things we define to be usable hypotheses for the main goal, we should have the define holes come first.

But that needs us to update the refinement type in other places it appears, which doesn't happen right now as far as I can tell. For instance if we refine the non-function hole we get from unary, the function hole isn't updated to match it.

If we can get that to happen, then I would be quite happy. But I'm not sure how feasible that is, or how to go about implementing it

[isovector]

if we refine the non-function hole we get from unary, the function hole isn't updated to match it.

Is it not? It should be!