Zulip Chat Archive

Stream: general

Topic: deciding if `refl` would work

Scott Morrison (Apr 22 2018 at 11:13):

I have lhs rhs : expr, and I would like to know, if the goal were to be lhs = rhs, whether or not refl would succeed. I could temporarily make the goal actually lhs = rhs, and try refl, but I'm wondering if it can be done directly.

Scott Morrison (Apr 22 2018 at 11:14):

I'm only hesitant to overwrite the goal because the actual current goal may be something completely unrelated to what my tactic is thinking about that the moment it's wondering about lhs = rhs, and it feels kludgy to actually have to use set_goal.

Scott Morrison (Apr 22 2018 at 11:15):

The problem is that refl is basically just shorthand for mk_const `eq.refl >>= λ r, apply_core r, and apply_core only unifies with the goal.

Sebastian Ullrich (Apr 22 2018 at 11:32):

@Scott Morrison Take a look at tactic.solve_aux

Scott Morrison (Apr 22 2018 at 11:42):

Thanks @Sebastian Ullrich. Implicit in your answer is "get over it, just set_goal to whatever you want, it's how you're meant to do this"! Good to know.

Sebastian Ullrich (Apr 22 2018 at 11:48):

If you want to look at it like that, yes :)

Simon Hudon (Apr 22 2018 at 14:07):

What if you try to unify them directly? unify lhs rhs

Last updated: Aug 03 2023 at 10:10 UTC