Stream: Coq users

Topic: How to revert a tactic


view this post on Zulip walker (Aug 11 2022 at 10:45):

I am trying to solve induction with many trivial cases but I want a clean way to automate the solution of the easy case.
All the easy cases can be solved by

inversion H; subst; auto.

but inversion H will modify the non-trivial case by complicating the goal. So all: inversion H; subst; auto. does not work.

I thought about all: inversion H; subst; auto; reflexivity. but that does not feel clean. The idea was that reflexivity will fail which leafs the non trivial cases un-modified. Is there a nicer way to achieve the same results?

view this post on Zulip Gaƫtan Gilbert (Aug 11 2022 at 10:47):

all: try solve [inversion H; subst; auto]

view this post on Zulip walker (Aug 11 2022 at 10:48):

perfect! solve is the keyword I am looking for!


Last updated: Jan 29 2023 at 06:02 UTC