Stream: Ltac2

Topic: Replace the type of the goal


view this post on Zulip Michael Soegtrop (Nov 16 2022 at 19:17):

I wonder what the best way is to change the goal with something convertible. All I came up with is:

Ltac2 change_goal (new_goal : constr) :=
  ltac1:( a b |- change a with b ) (Ltac1.of_constr (Control.goal())) (Ltac1.of_constr new_goal).

As discussed the Ltac2 change doesn't work for me because the "from term" is a pattern and not a constr. But maybe there is a way to replace the complete goal.

view this post on Zulip Gaëtan Gilbert (Nov 16 2022 at 19:48):

why not

Ltac2 change_goal (new_goal : constr) :=
  ltac1:( b |- change b ) (Ltac1.of_constr new_goal).

?

view this post on Zulip Michael Soegtrop (Nov 17 2022 at 09:19):

@Gaëtan Gilbert : thanks - I didn't use change without with so far. But you also don't see a way around Ltac1?

@Pierre-Marie Pédrot once explained that change takes a pattern and that there is a rather obscure function to convert a term to a pattern. I wonder why there is no simple change function which changes a term with a term.

view this post on Zulip Pierre-Marie Pédrot (Nov 17 2022 at 09:28):

change and change with are actually pretty different tactics. There are no patterns involved in the former.

view this post on Zulip Pierre-Marie Pédrot (Nov 17 2022 at 09:35):

I checked and indeed it works as expected:

Ltac2 changef x := change $x.

Goal True.
changef constr:(id True).

view this post on Zulip Michael Soegtrop (Nov 17 2022 at 10:07):

Indeed simply change $new_goal works as expected! Thanks for point this out - as usual it is obvious once one knows it. I guess my main problem was that I didn't know a change without with existed at all.


Last updated: Jan 31 2023 at 09:01 UTC