Stream: Beginner Questions

Topic: Disable simp for IH

view this post on Zulip Bilel Ghorbel (Jul 13 2021 at 20:30):

As the topic says, It is getting annoying that the definition gets unfolded for the IH as well as the goal while performing an induction proof, and this makes the proof more complicated. Is there a way to make simp leave the IH as it is ?

view this post on Zulip Jakub Kądziołka (Jul 13 2021 at 20:32):

Not applicable in all cases, but you might want to chain the fact in with (simp add: IH) instead of Isar's using/from

view this post on Zulip Bilel Ghorbel (Jul 13 2021 at 20:39):

Let me reformulate the question as such:
I have a lemma in the form f x = g x
I apply induct x, the inductive case is now an implication. I only need to apply simp on the rhs of that implication, applying on the left side will just complicate the proof.

view this post on Zulip Kevin Kappelmann (Jul 13 2021 at 20:41):

check out the rewrite tactic https://isabelle.in.tum.de/library/HOL/HOL-ex/Rewrite_Examples.html

view this post on Zulip Jakub Kądziołka (Jul 13 2021 at 20:42):

What I have in mind is

proof (induct x)
  case (Suc x) (* or whatever *)
  note IH = this
  show ?case by (simp add: IH)
qed simp

view this post on Zulip Simon Roßkopf (Jul 13 2021 at 20:43):

If I understand you correctly you want to only simplify the conclusion?

view this post on Zulip Simon Roßkopf (Jul 13 2021 at 20:45):

In that case simp (no_asm_simp) might be what you want

view this post on Zulip Bilel Ghorbel (Jul 13 2021 at 23:19):

@Simon Roßkopf is there an alternative with auto, so that I could work on different goals simultaneously ?

view this post on Zulip Simon Roßkopf (Jul 13 2021 at 23:32):

I don't think so. auto does more than simplification, so I do not think it is possible to operate on just a part of the goal. If you just want to do simplification on multiple subgoals simp_all has the same modifiers(Or use all from Eisbach).

However, all of this is pretty much a hack imo. Similarly to what Jakub is suggesting, the correct thing would probably be to do a structured proof and only insert the information where you need it. Just throwing everything into the goal and hoping that automation works seems very brittle.

view this post on Zulip Bilel Ghorbel (Jul 13 2021 at 23:38):

It's not really hoping that automation would work. There's just a huge amount of subgoals while the procedure for each is the same. A structured proof would be a huge repeated code.

Last updated: Apr 18 2024 at 01:05 UTC