walker (Aug 11 2022 at 10:45): 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?
Gaëtan Gilbert (Aug 11 2022 at 10:47):all: try solve [inversion H; subst; auto]
walker (Aug 11 2022 at 10:48):perfect! solve is the keyword I am looking for!
Last updated: Oct 13 2024 at 01:02 UTC