Stream: Beginner Questions

Topic: Disable simp for IH

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 ?

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`

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.

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

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
``````

Simon Roßkopf (Jul 13 2021 at 20:43):

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

Simon Roßkopf (Jul 13 2021 at 20:45):

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

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 ?

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.

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: Sep 25 2021 at 09:17 UTC